aboutsummaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/rewrite.ml')
-rw-r--r--tactics/rewrite.ml126
1 files changed, 75 insertions, 51 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 803e187ff5..9532354632 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -34,6 +34,9 @@ open Elimschemes
open Environ
open Termops
open Libnames
+open Sigma.Notations
+open Proofview.Notations
+open Context.Named.Declaration
(** Typeclass-based generalized rewriting. *)
@@ -66,8 +69,10 @@ type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
let find_global dir s =
let gr = lazy (try_find_global_reference dir s) in
- fun (evd,cstrs) ->
- let evd, c = Evarutil.new_global evd (Lazy.force gr) in
+ fun (evd,cstrs) ->
+ let sigma = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in
+ let evd = Sigma.to_evar_map sigma in
(evd, cstrs), c
(** Utility for dealing with polymorphic applications *)
@@ -88,7 +93,9 @@ let cstrevars evars = snd evars
let new_cstr_evar (evd,cstrs) env t =
let s = Typeclasses.set_resolvable Evd.Store.empty false in
- let evd', t = Evarutil.new_evar ~store:s env evd t in
+ let evd = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in
+ let evd' = Sigma.to_evar_map evd' in
let ev, _ = destEvar t in
(evd', Evar.Set.add ev cstrs), t
@@ -105,7 +112,7 @@ let extends_undefined evars evars' =
let app_poly_check env evars f args =
let (evars, cstrs), fc = f evars in
let evdref = ref evars in
- let t = Typing.solve_evars env evdref (mkApp (fc, args)) in
+ let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in
(!evdref, cstrs), t
let app_poly_nocheck env evars f args =
@@ -134,6 +141,7 @@ module GlobalBindings (M : sig
val arrow : evars -> evars * constr
end) = struct
open M
+ open Context.Rel.Declaration
let relation : evars -> evars * constr = find_global (fst relation) (snd relation)
let reflexive_type = find_global relation_classes "Reflexive"
@@ -172,13 +180,17 @@ end) = struct
let proper_type =
let l = lazy (Lazy.force proper_class).cl_impl in
fun (evd,cstrs) ->
- let evd, c = Evarutil.new_global evd (Lazy.force l) in
+ let sigma = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
+ let evd = Sigma.to_evar_map sigma in
(evd, cstrs), c
let proper_proxy_type =
let l = lazy (Lazy.force proper_proxy_class).cl_impl in
fun (evd,cstrs) ->
- let evd, c = Evarutil.new_global evd (Lazy.force l) in
+ let sigma = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
+ let evd = Sigma.to_evar_map sigma in
(evd, cstrs), c
let proper_proof env evars carrier relation x =
@@ -219,8 +231,8 @@ end) = struct
let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
else
- let (evars, b, arg, cstrs) =
- aux (Environ.push_rel (na, None, ty) env) evars b cstrs
+ let (evars, b, arg, cstrs) =
+ aux (Environ.push_rel (LocalAssum (na, ty)) env) evars b cstrs
in
let ty = Reductionops.nf_betaiota (goalevars evars) ty in
let pred = mkLambda (na, ty, b) in
@@ -318,7 +330,7 @@ end) = struct
let evars, rb = aux evars env b' (pred n) in
app_poly env evars pointwise_relation [| ty; b'; rb |]
else
- let evars, rb = aux evars (Environ.push_rel (na, None, ty) env) b (pred n) in
+ let evars, rb = aux evars (Environ.push_rel (LocalAssum (na, ty)) env) b (pred n) in
app_poly env evars forall_relation
[| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
| _ -> raise Not_found
@@ -347,7 +359,9 @@ end) = struct
(try
let params, args = Array.chop (Array.length args - 2) args in
let env' = Environ.push_rel_context rels env in
- let evars, (evar, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
+ let evars = Sigma.to_evar_map sigma in
let evars, inst =
app_poly env (evars,Evar.Set.empty)
rewrite_relation_class [| evar; mkApp (c, params) |] in
@@ -407,7 +421,9 @@ module TypeGlobal = struct
let inverse env (evd,cstrs) car rel =
- let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
+ let sigma = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (sort, sigma, _) = Evarutil.new_Type ~rigid:Evd.univ_flexible env sigma in
+ let evd = Sigma.to_evar_map sigma in
app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
end
@@ -478,6 +494,7 @@ let decompose_app_rel env evd t =
(rel, t1, t2)
let decompose_applied_relation env sigma (c,l) =
+ let open Context.Rel.Declaration in
let ctype = Retyping.get_type_of env sigma c in
let find_rel ty =
let sigma, cl = Clenv.make_evar_clause env sigma ty in
@@ -500,7 +517,7 @@ let decompose_applied_relation env sigma (c,l) =
| Some c -> c
| None ->
let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
- match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> n, None, t) ctx)) with
+ match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
| Some c -> c
| None -> error "Cannot find an homogeneous relation to rewrite."
@@ -775,9 +792,9 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation
in
Environ.push_named
- (Id.of_string "do_subrelation",
- Some (snd (app_poly_sort b env evars dosub [||])),
- snd (app_poly_nocheck env evars appsub [||]))
+ (LocalDef (Id.of_string "do_subrelation",
+ snd (app_poly_sort b env evars dosub [||]),
+ snd (app_poly_nocheck env evars appsub [||])))
env
in
let evars, morph = new_cstr_evar evars env' app in
@@ -1119,8 +1136,9 @@ 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 unfresh id env) n in
- let env' = Environ.push_rel (n', None, t) env in
+ let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
+ let open Context.Rel.Declaration in
+ let env' = Environ.push_rel (LocalAssum (n', 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.strategy { state ; env = env' ; unfresh ;
@@ -1369,7 +1387,9 @@ module Strategies =
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
+ let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in
+ let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma t in
+ let evars' = Sigma.to_evar_map sigma in
if eq_constr t' t then
state, Identity
else
@@ -1451,7 +1471,7 @@ type result = (evar_map * constr option * types) option option
let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
let evdref = ref sigma in
- let sort = Typing.sort_of env evdref concl in
+ let sort = Typing.e_sort_of env evdref concl in
let evars = (!evdref, Evar.Set.empty) in
let evars, cstr =
let prop, (evars, arrow) =
@@ -1504,31 +1524,34 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
(** Insert a declaration after the last declaration it depends on *)
let rec insert_dependent env decl accu hyps = match hyps with
| [] -> List.rev_append accu [decl]
-| (id, _, _ as ndecl) :: rem ->
- if occur_var_in_decl env id decl then
+| ndecl :: rem ->
+ if occur_var_in_decl env (get_id ndecl) decl then
List.rev_append accu (decl :: hyps)
else
insert_dependent env decl (ndecl :: accu) rem
let assert_replacing id newt tac =
- let prf = Proofview.Goal.nf_enter begin fun gl ->
+ let prf = Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let ctx = Environ.named_context env in
- let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in
+ let after, before = List.split_when (Id.equal id % get_id) ctx in
let nc = match before with
| [] -> assert false
- | (id, b, _) :: rem -> insert_dependent env (id, None, newt) [] after @ rem
+ | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem
in
let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
- Proofview.Refine.refine ~unsafe:false begin fun sigma ->
- let sigma, ev = Evarutil.new_evar env' sigma concl in
- let sigma, ev' = Evarutil.new_evar env sigma newt in
- let map (n, _, _) = if Id.equal n id then ev' else mkVar n in
+ Proofview.Refine.refine ~unsafe:false { run = begin fun sigma ->
+ let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
+ let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
+ let map d =
+ let n = get_id d in
+ if Id.equal n id then ev' else mkVar n
+ in
let (e, _) = destEvar ev in
- sigma, mkEvar (e, Array.map_of_list map nc)
- end
- end in
+ Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q)
+ end }
+ end } in
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
let newfail n s =
@@ -1547,36 +1570,36 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let gls = List.rev (Evd.fold_undefined fold undef []) in
match clause, prf with
| Some id, Some p ->
- let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
+ let tac = Proofview.Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
Proofview.Unsafe.tclEVARS undef <*>
assert_replacing id newt tac
| Some id, None ->
Proofview.Unsafe.tclEVARS undef <*>
- convert_hyp_no_check (id, None, newt)
+ convert_hyp_no_check (LocalAssum (id, newt))
| None, Some p ->
Proofview.Unsafe.tclEVARS undef <*>
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let make sigma =
- let (sigma, ev) = Evarutil.new_evar env sigma newt in
- sigma, mkApp (p, [| ev |])
- in
+ let make = { run = begin fun sigma ->
+ let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in
+ Sigma (mkApp (p, [| ev |]), sigma, q)
+ end } in
Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
- end
+ end }
| None, None ->
Proofview.Unsafe.tclEVARS undef <*>
convert_concl_no_check newt DEFAULTcast
in
let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
- let beta = Proofview.V82.tactic (Tactics.reduct_in_concl (beta_red, DEFAULTcast)) in
+ let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
let opt_beta = match clause with
| None -> Proofview.tclUNIT ()
- | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp))
+ | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp)
in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let ty = match clause with
| None -> concl
| Some id -> Environ.named_type id env
@@ -1601,7 +1624,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
with
| PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
- end
+ end }
let tactic_init_setoid () =
try init_setoid (); tclIDTAC
@@ -1724,7 +1747,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
new_instance (Flags.is_universe_polymorphism ())
- binders instance (Some (true, CRecord (Loc.ghost,None,fields)))
+ binders instance (Some (true, CRecord (Loc.ghost,fields)))
~global ~generalize:false None
let declare_instance_refl global binders a aeq n lemma =
@@ -1939,7 +1962,7 @@ let add_morphism glob binders m s n =
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
ignore(new_instance ~global:glob poly binders instance
- (Some (true, CRecord (Loc.ghost,None,[])))
+ (Some (true, CRecord (Loc.ghost,[])))
~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
(** Bind to "rewrite" too *)
@@ -2054,17 +2077,18 @@ let not_declared env ty rel =
str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
let setoid_proof ty fn fallback =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
Proofview.tclORELSE
begin
try
let rel, _, _ = decompose_app_rel env sigma concl in
+ let open Context.Rel.Declaration in
let (sigma, t) = Typing.type_of env sigma rel in
- let car = pi3 (List.hd (fst (Reduction.dest_prod env t))) in
- (try init_relation_classes () with _ -> raise Not_found);
+ let car = get_type (List.hd (fst (Reduction.dest_prod env t))) in
+ (try init_setoid () with _ -> raise Not_found);
fn env sigma car rel
with e -> Proofview.tclZERO e
end
@@ -2083,7 +2107,7 @@ let setoid_proof ty fn fallback =
| e' -> Proofview.tclZERO ~info e'
end
end
- end
+ end }
let tac_open ((evm,_), c) tac =
Proofview.V82.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:14:26 +0000