diff options
Diffstat (limited to 'tactics/rewrite.ml')
-rw-r--r-- | tactics/rewrite.ml | 350 |
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 |