summaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/rewrite.ml')
-rw-r--r--tactics/rewrite.ml350
1 files changed, 191 insertions, 159 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ac8b4923..e8a7c0f6 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -52,7 +52,7 @@ let try_find_global_reference dir s =
let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
try Nametab.global_of_path sp
with Not_found ->
- anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting"))
+ anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting")
let find_reference dir s =
let gr = lazy (try_find_global_reference dir s) in
@@ -76,25 +76,6 @@ let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
let coq_all = find_global ["Init"; "Logic"] "all"
let impl = find_global ["Program"; "Basics"] "impl"
-(* let coq_inverse = lazy (gen_constant ["Program"; "Basics"] "flip") *)
-
-(* let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |]) *)
-
-(* let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation") *)
-(* let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation") *)
-(* let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") *)
-(* let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation") *)
-(* let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation") *)
-(* let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation") *)
-(* let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation") *)
-(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
-(* let mk_relation a = mkApp (Lazy.force coq_relation, [| a |]) *)
-
-(* let proper_type = lazy (Universes.constr_of_global (Lazy.force proper_class).cl_impl) *)
-(* let proper_proxy_type = lazy (Universes.constr_of_global (Lazy.force proper_proxy_class).cl_impl) *)
-
-
-
(** Bookkeeping which evars are constraints so that we can
remove them at the end of the tactic. *)
@@ -226,6 +207,7 @@ end) = struct
let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in
match kind_of_term t, l with
| Prod (na, ty, b), obj :: cstrs ->
+ let b = Reductionops.nf_betaiota (goalevars evars) b in
if noccurn 1 b (* non-dependent product *) then
let ty = Reductionops.nf_betaiota (goalevars evars) ty in
let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
@@ -380,7 +362,7 @@ end
let type_app_poly env env evd f args =
let evars, c = app_poly_nocheck env evd f args in
- let evd', t = Typing.e_type_of env (goalevars evars) c in
+ let evd', t = Typing.type_of env (goalevars evars) c in
(evd', cstrevars evars), c
module PropGlobal = struct
@@ -452,7 +434,6 @@ let convertible env evd x y =
Reductionops.is_conv_leq env evd x y
type hypinfo = {
- env : env;
prf : constr;
car : constr;
rel : constr;
@@ -472,7 +453,7 @@ let rec decompose_app_rel env evd t =
| App (f, [||]) -> assert false
| App (f, [|arg|]) ->
let (f', argl, argr) = decompose_app_rel env evd arg in
- let ty = Typing.type_of env evd argl in
+ let ty = Typing.unsafe_type_of env evd argl in
let f'' = mkLambda (Name default_dependent_ident, ty,
mkLambda (Name (Id.of_string "y"), lift 1 ty,
mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
@@ -498,7 +479,7 @@ let decompose_applied_relation env sigma (c,l) =
let sort = sort_of_rel env sigma equiv in
let args = Array.map_of_list (fun h -> h.Clenv.hole_evar) holes in
let value = mkApp (c, args) in
- Some (sigma, { env=env; prf=value;
+ Some (sigma, { prf=value;
car=ty1; rel = equiv; sort = Sorts.is_prop sort;
c1=c1; c2=c2; holes })
in
@@ -510,10 +491,6 @@ let decompose_applied_relation env sigma (c,l) =
| Some c -> c
| None -> error "Cannot find an homogeneous relation to rewrite."
-let decompose_applied_relation_expr env sigma (is, (c,l)) =
- let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in
- decompose_applied_relation env sigma cbl
-
let rewrite_db = "rewrite"
let conv_transparent_state = (Id.Pred.empty, Cpred.full)
@@ -588,24 +565,12 @@ let general_rewrite_unif_flags () =
Unification.resolve_evars = true
}
-let refresh_hypinfo env sigma hypinfo c =
- let sigma, hypinfo = match hypinfo with
- | None ->
- decompose_applied_relation_expr env sigma c
- | Some hypinfo ->
- if hypinfo.env != env then
- (* If the lemma actually generates existential variables, we cannot
- use it here as it will polute the evar map with existential variables
- that might not ever get instantiated (e.g. if we rewrite under a
- binder and need to refresh [c] again) *)
- (* TODO: remove bindings in sigma corresponding to c *)
- decompose_applied_relation_expr env sigma c
- else sigma, hypinfo
- in
+let refresh_hypinfo env sigma (is, cb) =
+ let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma cb in
+ let sigma, hypinfo = decompose_applied_relation env sigma cbl in
let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
sigma, (car, rel, prf, c1, c2, holes, sort)
-
(** FIXME: write this in the new monad interface *)
let solve_remaining_by env sigma holes by =
match by with
@@ -647,13 +612,19 @@ let poly_inverse sort =
type rewrite_proof =
| RewPrf of constr * constr
+ (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)
| RewCast of cast_kind
+ (** A proof of convertibility (with casts) *)
type rewrite_result_info = {
- rew_car : constr;
- rew_from : constr;
- rew_to : constr;
- rew_prf : rewrite_proof;
+ rew_car : constr ;
+ (** A type *)
+ rew_from : constr ;
+ (** A term of type rew_car *)
+ rew_to : constr ;
+ (** A term of type rew_car *)
+ rew_prf : rewrite_proof ;
+ (** A proof of rew_from == rew_to *)
rew_evars : evars;
}
@@ -662,9 +633,17 @@ type rewrite_result =
| Identity
| Success of rewrite_result_info
-type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
- (bool (* prop *) * constr option) -> evars ->
- 'a * rewrite_result
+type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
+ env : Environ.env ;
+ unfresh : Id.t list ; (* Unfresh names *)
+ term1 : constr ;
+ ty1 : types ; (* first term and its type (convertible to rew_from) *)
+ cstr : (bool (* prop *) * constr option) ;
+ evars : evars }
+
+type 'a pure_strategy = { strategy :
+ 'a strategy_input ->
+ 'a * rewrite_result (* the updated state and the "result" *) }
type strategy = unit pure_strategy
@@ -719,7 +698,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
let rew_prf = RewPrf (rel, prf) in
let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in
let rew = if l2r then rew else symmetry env sort rew in
- Some ((), rew)
+ Some rew
with
| e when Class_tactics.catchable e -> None
| Reduction.NotConvertible -> None
@@ -763,7 +742,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let morphargs, morphobjs = Array.chop first args in
let morphargs', morphobjs' = Array.chop first args' in
let appm = mkApp(m, morphargs) in
- let appmtype = Typing.type_of env (goalevars evars) appm in
+ let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
let cstrs = List.map
(Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
(Array.to_list morphobjs')
@@ -829,42 +808,47 @@ let coerce env avoid cstr res =
let rel, prf = get_rew_prf res in
apply_constraint env avoid res.rew_car rel prf cstr res
-let apply_rule unify loccs : ('a * int) pure_strategy =
+let apply_rule unify loccs : int pure_strategy =
let (nowhere_except_in,occs) = convert_occs loccs in
let is_occ occ =
if nowhere_except_in
then List.mem occ occs
else not (List.mem occ occs)
in
- fun (hypinfo, occ) env avoid t ty cstr evars ->
- let unif = if isEvar t then None else unify hypinfo env evars t in
+ { strategy = fun { state = occ ; env ; unfresh ;
+ term1 = t ; ty1 = ty ; cstr ; evars } ->
+ let unif = if isEvar t then None else unify env evars t in
match unif with
- | None -> ((hypinfo, occ), Fail)
- | Some (hypinfo', rew) ->
+ | None -> (occ, Fail)
+ | Some rew ->
let occ = succ occ in
- if not (is_occ occ) then ((hypinfo, occ), Fail)
- else if eq_constr t rew.rew_to then ((hypinfo, occ), Identity)
+ if not (is_occ occ) then (occ, Fail)
+ else if eq_constr t rew.rew_to then (occ, Identity)
else
let res = { rew with rew_car = ty } in
let rel, prf = get_rew_prf res in
- let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in
- ((hypinfo', occ), res)
-
-let apply_lemma l2r flags oc by loccs : strategy =
- fun () env avoid t ty cstr (sigma, cstrs) ->
+ let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in
+ (occ, res)
+ }
+
+let apply_lemma l2r flags oc by loccs : strategy = { strategy =
+ fun ({ state = () ; env ; term1 = t ; evars = (sigma, cstrs) } as input) ->
let sigma, c = oc sigma in
let sigma, hypinfo = decompose_applied_relation env sigma c in
let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
let rew = (car, rel, prf, c1, c2, holes, sort) in
let evars = (sigma, cstrs) in
- let unify () env evars t =
+ let unify env evars t =
let rew = unify_eqn rew l2r flags env evars by t in
match rew with
| None -> None
- | Some rew -> Some ((), rew)
+ | Some rew -> Some rew
in
- let _, res = apply_rule unify loccs ((), 0) env avoid t ty cstr evars in
+ let _, res = (apply_rule unify loccs).strategy { input with
+ state = 0 ;
+ evars } in
(), res
+ }
let e_app_poly env evars f args =
let evars', c = app_poly_nocheck env !evars f args in
@@ -944,7 +928,8 @@ let unfold_match env sigma sk app =
let is_rew_cast = function RewCast _ -> true | _ -> false
let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
- let rec aux state env avoid t ty (prop, cstr) evars =
+ let rec aux { state ; env ; unfresh ;
+ term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
match kind_of_term t with
| App (m, args) ->
@@ -956,7 +941,11 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
state, (None :: acc, evars, progress)
else
let argty = Retyping.get_type_of env (goalevars evars) arg in
- let state, res = s state env avoid arg argty (prop,None) evars in
+ let state, res = s.strategy { state ; env ;
+ unfresh ;
+ term1 = arg ; ty1 = argty ;
+ cstr = (prop,None) ;
+ evars } in
let res' =
match res with
| Identity ->
@@ -980,7 +969,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Some r -> not (is_rew_cast r.rew_prf)) args'
then
let evars', prf, car, rel, c1, c2 =
- resolve_morphism env avoid t m args args' (prop, cstr') evars'
+ resolve_morphism env unfresh t m args args' (prop, cstr') evars'
in
let res = { rew_car = ty; rew_from = c1;
rew_to = c2; rew_prf = RewPrf (rel, prf);
@@ -1008,7 +997,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
evars, Some cstr', m, mty, args, Array.of_list args
| None -> evars, None, m, mty, argsl, args
in
- let state, m' = s state env avoid m mty (prop, cstr') evars in
+ let state, m' = s.strategy { state ; env ; unfresh ;
+ term1 = m ; ty1 = mty ;
+ cstr = (prop, cstr') ; evars } in
match m' with
| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
| Identity -> rewrite_args state (Some false)
@@ -1031,7 +1022,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let res =
match prf with
| RewPrf (rel, prf) ->
- Success (apply_constraint env avoid res.rew_car
+ Success (apply_constraint env unfresh res.rew_car
rel prf (prop,cstr) res)
| _ -> Success res
in state, res
@@ -1045,7 +1036,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
else TypeGlobal.arrow_morphism
in
let (evars', mor), unfold = arr env evars tx tb x b in
- let state, res = aux state env avoid mor ty (prop,cstr) evars' in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = mor ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars = evars' } in
let res =
match res with
| Success r -> Success { r with rew_to = unfold r.rew_to }
@@ -1075,7 +1068,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
(app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall
in
- let state, res = aux state env avoid app ty (prop,cstr) evars' in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = app ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars = evars' } in
let res =
match res with
| Success r -> Success { r with rew_to = unfold r.rew_to }
@@ -1111,11 +1106,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
(* | _ -> b') *)
| Lambda (n, t, b) when flags.under_lambdas ->
- let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in
+ let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
let env' = Environ.push_rel (n', None, t) env in
let bty = Retyping.get_type_of env' (goalevars evars) b in
let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
- let state, b' = s state env' avoid b bty (prop, unlift env evars cstr) evars in
+ let state, b' = s.strategy { state ; env = env' ; unfresh ;
+ term1 = b ; ty1 = bty ;
+ cstr = (prop, unlift env evars cstr) ;
+ evars } in
let res =
match b' with
| Success r ->
@@ -1140,13 +1138,15 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let cty = Retyping.get_type_of env (goalevars evars) c in
let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
let cstr' = Some eqty in
- let state, c' = s state env avoid c cty (prop, cstr') evars' in
+ let state, c' = s.strategy { state ; env ; unfresh ;
+ term1 = c ; ty1 = cty ;
+ cstr = (prop, cstr') ; evars = evars' } in
let state, res =
match c' with
| Success r ->
let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
let res = make_leibniz_proof env case ty r in
- state, Success (coerce env avoid (prop,cstr) res)
+ state, Success (coerce env unfresh (prop,cstr) res)
| Fail | Identity ->
if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
@@ -1156,7 +1156,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
if not (Option.is_empty found) then
(state, found, fun x -> lift 1 br :: acc x)
else
- let state, res = s state env avoid br ty (prop,cstr) evars in
+ let state, res = s.strategy { state ; env ; unfresh ;
+ term1 = br ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } in
match res with
| Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
| Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
@@ -1171,7 +1173,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
| None -> state, c'
| Some (cst, _, t', eff (*FIXME*)) ->
- let state, res = aux state env avoid t' ty (prop,cstr) evars in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = t' ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } in
let res =
match res with
| Success prf ->
@@ -1185,11 +1189,11 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
match res with
| Success r ->
let rel, prf = get_rew_prf r in
- Success (apply_constraint env avoid r.rew_car rel prf (prop,cstr) r)
+ Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r)
| Fail | Identity -> res
in state, res
| _ -> state, Fail
- in aux
+ in { strategy = aux }
let all_subterms = subterm true default_flags
let one_subterm = subterm false default_flags
@@ -1197,11 +1201,13 @@ let one_subterm = subterm false default_flags
(** Requires transitivity of the rewrite step, if not a reduction.
Not tail-recursive. *)
-let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pure_strategy) :
+let transitivity state env unfresh prop (res : rewrite_result_info) (next : 'a pure_strategy) :
'a * rewrite_result =
let state, nextres =
- next state env avoid res.rew_to res.rew_car
- (prop, get_opt_rew_rel res.rew_prf) res.rew_evars
+ next.strategy { state ; env ; unfresh ;
+ term1 = res.rew_to ; ty1 = res.rew_car ;
+ cstr = (prop, get_opt_rew_rel res.rew_prf) ;
+ evars = res.rew_evars }
in
let res =
match nextres with
@@ -1238,15 +1244,16 @@ module Strategies =
struct
let fail : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- state, Fail
+ { strategy = fun { state } -> state, Fail }
let id : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- state, Identity
+ { strategy = fun { state } -> state, Identity }
let refl : 'a pure_strategy =
- fun state env avoid t ty (prop,cstr) evars ->
+ { strategy =
+ fun { state ; env ;
+ term1 = t ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } ->
let evars, rel = match cstr with
| None ->
let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
@@ -1265,38 +1272,43 @@ module Strategies =
let res = Success { rew_car = ty; rew_from = t; rew_to = t;
rew_prf = RewPrf (rel, proof); rew_evars = evars }
in state, res
+ }
- let progress (s : 'a pure_strategy) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = s state env avoid t ty cstr evars in
+ let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy =
+ fun input ->
+ let state, res = s.strategy input in
match res with
| Fail -> state, Fail
| Identity -> state, Fail
| Success r -> state, Success r
+ }
- let seq first snd : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = first state env avoid t ty cstr evars in
+ let seq first snd : 'a pure_strategy = { strategy =
+ fun ({ env ; unfresh ; cstr } as input) ->
+ let state, res = first.strategy input in
match res with
| Fail -> state, Fail
- | Identity -> snd state env avoid t ty cstr evars
- | Success res -> transitivity state env avoid (fst cstr) res snd
+ | Identity -> snd.strategy { input with state }
+ | Success res -> transitivity state env unfresh (fst cstr) res snd
+ }
- let choice fst snd : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = fst state env avoid t ty cstr evars in
+ let choice fst snd : 'a pure_strategy = { strategy =
+ fun input ->
+ let state, res = fst.strategy input in
match res with
- | Fail -> snd state env avoid t ty cstr evars
+ | Fail -> snd.strategy { input with state }
| Identity | Success _ -> state, res
+ }
let try_ str : 'a pure_strategy = choice str id
- let check_interrupt str s e l c t r ev =
+ let check_interrupt str input =
Control.check_for_interrupt ();
- str s e l c t r ev
-
+ str input
+
let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
- let rec aux state = f (fun state -> check_interrupt aux state) state in aux
+ let rec aux input = (f { strategy = fun input -> check_interrupt aux input }).strategy input in
+ { strategy = aux }
let any (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun any -> try_ (seq s any))
@@ -1332,16 +1344,17 @@ module Strategies =
(List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r,
hint.Autorewrite.rew_tac)) rules)
- let hints (db : string) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let hints (db : string) : 'a pure_strategy = { strategy =
+ fun ({ term1 = t } as input) ->
let rules = Autorewrite.find_matches db t in
let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
hint.Autorewrite.rew_tac) in
let lems = List.map lemma rules in
- lemmas lems state env avoid t ty cstr evars
+ (lemmas lems).strategy input
+ }
- let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy =
+ fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
let rfn, ckind = Redexpr.reduction_of_red_expr env r in
let evars', t' = rfn env (goalevars evars) t in
if eq_constr t' t then
@@ -1350,9 +1363,10 @@ module Strategies =
state, Success { rew_car = ty; rew_from = t; rew_to = t';
rew_prf = RewCast ckind;
rew_evars = evars', cstrevars evars }
+ }
- let fold_glob c : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let fold_glob c : 'a pure_strategy = { strategy =
+ fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
let unfolded =
@@ -1367,23 +1381,23 @@ module Strategies =
rew_prf = RewCast DEFAULTcast;
rew_evars = (sigma, snd evars) }
with e when Errors.noncritical e -> state, Fail
+ }
end
-(** The strategy for a single rewrite, dealing with occurences. *)
+(** The strategy for a single rewrite, dealing with occurrences. *)
(** A dummy initial clauseenv to avoid generating initial evars before
even finding a first application of the rewriting lemma, in setoid_rewrite
mode *)
-let rewrite_with l2r flags c occs : strategy =
- fun () env avoid t ty cstr (sigma, cstrs) ->
- let hypinfo = None in
- let unify hypinfo env evars t =
+let rewrite_with l2r flags c occs : strategy = { strategy =
+ fun ({ state = () } as input) ->
+ let unify env evars t =
let (sigma, cstrs) = evars in
let ans =
- try Some (refresh_hypinfo env sigma hypinfo c)
+ try Some (refresh_hypinfo env sigma c)
with e when Class_tactics.catchable e -> None
in
match ans with
@@ -1392,19 +1406,22 @@ let rewrite_with l2r flags c occs : strategy =
let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in
match rew with
| None -> None
- | Some rew -> Some (None, rew) (** reset the hypinfo cache *)
+ | Some rew -> Some rew
in
let app = apply_rule unify occs in
let strat =
Strategies.fix (fun aux ->
Strategies.choice app (subterm true default_flags aux))
in
- let _, res = strat (hypinfo, 0) env avoid t ty cstr (sigma, cstrs) in
- ((), res)
+ let _, res = strat.strategy { input with state = 0 } in
+ ((), res)
+ }
-let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
+let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
let ty = Retyping.get_type_of env (goalevars evars) concl in
- let _, res = s () env avoid concl ty (prop, Some cstr) evars in
+ let _, res = s.strategy { state = () ; env ; unfresh ;
+ term1 = concl ; ty1 = ty ;
+ cstr = (prop, Some cstr) ; evars } in
res
let solve_constraints env (evars,cstrs) =
@@ -1506,7 +1523,7 @@ let newfail n s =
let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
let open Proofview.Notations in
- let treat sigma (res, is_hyp) =
+ let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
| Some None -> Proofview.tclUNIT ()
@@ -1514,7 +1531,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
let gls = List.rev (Evd.fold_undefined fold undef []) in
- match is_hyp, prf with
+ match clause, prf with
| Some id, Some p ->
let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
Proofview.Unsafe.tclEVARS undef <*>
@@ -1546,17 +1563,25 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let ty, is_hyp =
- match clause with
- | Some id -> Environ.named_type id env, Some id
- | None -> concl, None
+ let ty = match clause with
+ | None -> concl
+ | Some id -> Environ.named_type id env
+ in
+ let env = match clause with
+ | None -> env
+ | Some id ->
+ (** Only consider variables not depending on [id] *)
+ let ctx = Environ.named_context env in
+ let filter decl = not (occur_var_in_decl env id decl) in
+ let nctx = List.filter filter ctx in
+ Environ.reset_with_named_context (Environ.val_of_named_context nctx) env
in
try
let res =
- cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
+ cl_rewrite_clause_aux ?abs strat env [] sigma ty clause
in
let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
- treat sigma (res, is_hyp) <*>
+ treat sigma res <*>
(** For compatibility *)
beta <*> opt_beta <*> Proofview.shelve_unifiable
with
@@ -1583,13 +1608,13 @@ let cl_rewrite_clause l left2right occs clause gl =
let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
cl_rewrite_clause_strat strat clause gl
-let apply_glob_constr c l2r occs = (); fun () env avoid t ty cstr evars ->
+let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
let c sigma =
let (sigma, c) = Pretyping.understand_tcc env sigma c in
(sigma, (c, NoBindings))
in
let flags = general_rewrite_unif_flags () in
- apply_lemma l2r flags c None occs () env avoid t ty cstr evars
+ (apply_lemma l2r flags c None occs).strategy input
let interp_glob_constr_list env =
let make c = (); fun sigma ->
@@ -1653,16 +1678,18 @@ let rec strategy_of_ast = function
| Compose -> Strategies.seq
| Choice -> Strategies.choice
in f' s' t'
- | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences
+ | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
| StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
- | StratTerms l ->
- (fun () env avoid t ty cstr evars ->
+ | StratTerms l -> { strategy =
+ (fun ({ state = () ; env } as input) ->
let l' = interp_glob_constr_list env (List.map fst l) in
- Strategies.lemmas l' () env avoid t ty cstr evars)
- | StratEval r ->
- (fun () env avoid t ty cstr evars ->
+ (Strategies.lemmas l').strategy input)
+ }
+ | StratEval r -> { strategy =
+ (fun ({ state = () ; env ; evars } as input) ->
let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
- Strategies.reduce r_interp () env avoid t ty cstr (sigma,cstrevars evars))
+ (Strategies.reduce r_interp).strategy { input with
+ evars = (sigma,cstrevars evars) }) }
| StratFold c -> Strategies.fold_glob (fst c)
@@ -1751,11 +1778,13 @@ let proper_projection r ty =
it_mkLambda_or_LetIn app ctx
let declare_projection n instance_id r =
- let c,uctx = Universes.fresh_global_instance (Global.env()) r in
let poly = Global.is_polymorphic r in
- let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let evd,c = Evd.fresh_global env sigma r in
+ let ty = Retyping.get_type_of env sigma c in
let term = proper_projection c ty in
- let typ = Typing.type_of (Global.env ()) Evd.empty term in
+ let typ = Typing.unsafe_type_of env sigma term in
let ctx, typ = decompose_prod_assum typ in
let typ =
let n =
@@ -1777,18 +1806,19 @@ let declare_projection n instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
+ let pl, ctx = Evd.universe_context sigma in
let cst =
- Declare.definition_entry ~types:typ ~poly ~univs:(Univ.ContextSet.to_context uctx)
- term
+ Declare.definition_entry ~types:typ ~poly ~univs:ctx term
in
ignore(Declare.declare_constant n
(Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
let build_morphism_signature m =
let env = Global.env () in
- let m,ctx = Constrintern.interp_constr env Evd.empty m in
- let sigma = Evd.from_env ~ctx env in
- let t = Typing.type_of env sigma m in
+ let sigma = Evd.from_env env in
+ let m,ctx = Constrintern.interp_constr env sigma m in
+ let sigma = Evd.from_ctx ctx in
+ let t = Typing.unsafe_type_of env sigma m in
let cstrs =
let rec aux t =
match kind_of_term t with
@@ -1798,7 +1828,7 @@ let build_morphism_signature m =
in aux t
in
let evars, t', sig_, cstrs =
- PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t cstrs None in
+ PropGlobal.build_signature (sigma, Evar.Set.empty) env t cstrs None in
let evd = ref evars in
let _ = List.iter
(fun (ty, rel) ->
@@ -1815,9 +1845,10 @@ let build_morphism_signature m =
let default_morphism sign m =
let env = Global.env () in
- let t = Typing.type_of env Evd.empty m in
+ let sigma = Evd.from_env env in
+ let t = Typing.unsafe_type_of env sigma m in
let evars, _, sign, cstrs =
- PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign)
+ PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
in
let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
@@ -1848,9 +1879,9 @@ let add_morphism_infer glob m n =
let poly = Flags.is_universe_polymorphism () in
let instance_id = add_suffix n "_Proper" in
let instance = build_morphism_signature m in
- let evd = Evd.empty (*FIXME *) in
+ let evd = Evd.from_env (Global.env ()) in
if Lib.is_modtype () then
- let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
+ let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
(Entries.ParameterEntry
(None,poly,(instance,Univ.UContext.empty),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
@@ -1967,13 +1998,14 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
(** Setoid rewriting when called with "rewrite" *)
let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
- let unify () env evars t = unify_abs res l2r sort env evars t in
+ let unify env evars t = unify_abs res l2r sort env evars t in
let app = apply_rule unify occs in
let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
let substrat = Strategies.fix recstrat in
- let strat () env avoid t ty cstr evars =
- let _, res = substrat ((), 0) env avoid t ty cstr evars in
+ let strat = { strategy = fun ({ state = () } as input) ->
+ let _, res = substrat.strategy { input with state = 0 } in
(), res
+ }
in
let origsigma = project gl in
init_setoid ();
@@ -2011,7 +2043,7 @@ let setoid_proof ty fn fallback =
try
let rel, _, _ = decompose_app_rel env sigma concl in
let evm = sigma in
- let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
+ let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in
(try init_setoid () with _ -> raise Not_found);
fn env sigma car rel
with e -> Proofview.tclZERO e
@@ -2070,7 +2102,7 @@ let setoid_transitivity c =
let setoid_symmetry_in id =
Proofview.V82.tactic (fun gl ->
- let ctype = pf_type_of gl (mkVar id) in
+ let ctype = pf_unsafe_type_of gl (mkVar id) in
let binders,concl = decompose_prod_assum ctype in
let (equiv, args) = decompose_app concl in
let rec split_last_two = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 21:17:09 +0000