aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/recdef.ml5
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/tacred.ml24
-rw-r--r--pretyping/tacred.mli3
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--proofs/tacmach.ml6
-rw-r--r--tactics/extratactics.ml45
-rw-r--r--tactics/rewrite.ml4
-rw-r--r--tactics/tacinterp.ml5
-rw-r--r--tactics/tactics.ml74
-rw-r--r--toplevel/command.ml13
-rw-r--r--toplevel/vernacentries.ml8
13 files changed, 90 insertions, 63 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6c6caa628..555f08fa8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -690,9 +690,8 @@ let mkDestructEq :
[generalize new_hyps;
(fun g2 ->
let changefun patvars = { run = fun sigma ->
- let sigma = Sigma.to_evar_map sigma in
- let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in
- Sigma.Unsafe.of_pair (c, sigma)
+ let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
+ redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2)
} in
Proofview.V82.of_tactic (change_in_concl None changefun) g2);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5e21154a6..a677458da 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -572,7 +572,7 @@ type state = constr * constr Stack.t
type contextual_reduction_function = env -> evar_map -> constr -> constr
type reduction_function = contextual_reduction_function
type local_reduction_function = evar_map -> constr -> constr
-type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e65ab83b2..b38252e97 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -108,7 +108,7 @@ type contextual_reduction_function = env -> evar_map -> constr -> constr
type reduction_function = contextual_reduction_function
type local_reduction_function = evar_map -> constr -> constr
-type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 085aaf78a..be95de873 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -963,10 +963,12 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
| _ -> mkApp (app', [| a' |]))
| _ -> map_constr_with_binders_left_to_right g f acc c
-let e_contextually byhead (occs,c) f env sigma t =
+let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
let (nowhere_except_in,locs) = Locusops.convert_occs occs in
let maxocc = List.fold_right max locs 0 in
let pos = ref 1 in
+ let sigma = Sigma.to_evar_map sigma in
+ (** FIXME: we do suspicious things with this evarmap *)
let evd = ref sigma in
let rec traverse nested (env,c as envc) t =
if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t
@@ -985,8 +987,8 @@ let e_contextually byhead (occs,c) f env sigma t =
(* Skip inner occurrences for stable counting of occurrences *)
if locs != [] then
ignore (traverse_below (Some (!pos-1)) envc t);
- let evm, t = f subst env !evd t in
- (evd := evm; t)
+ let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) t in
+ (evd := Sigma.to_evar_map evm; t)
end
else
traverse_below nested envc t
@@ -1005,11 +1007,15 @@ let e_contextually byhead (occs,c) f env sigma t =
in
let t' = traverse None (env,c) t in
if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
- !evd, t'
+ Sigma.Unsafe.of_pair (t', !evd)
+ end }
let contextually byhead occs f env sigma t =
- let f' subst env sigma t = sigma, f subst env sigma t in
- snd (e_contextually byhead occs f' env sigma t)
+ let f' subst = { e_redfun = begin fun env sigma t ->
+ Sigma.here (f subst env (Sigma.to_evar_map sigma) t) sigma
+ end } in
+ let Sigma (c, _, _) = (e_contextually byhead occs f').e_redfun env (Sigma.Unsafe.of_evar_map sigma) t in
+ c
(* linear bindings (following pretty-printer) of the value of name in c.
* n is the number of the next occurrence of name.
@@ -1128,13 +1134,15 @@ let abstract_scheme env (locc,a) (c, sigma) =
let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
mkLambda (na,ta,c'), sigma'
-let pattern_occs loccs_trm env sigma c =
+let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
+ let sigma = Sigma.to_evar_map sigma in
let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in
try
let _ = Typing.unsafe_type_of env sigma abstr_trm in
- sigma, applist(abstr_trm, List.map snd loccs_trm)
+ Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
with Type_errors.TypeError (env',t) ->
raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
+ end }
(* Used in several tactics. *)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 6a7248e19..195b21bbf 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -61,8 +61,7 @@ val unfoldn :
val fold_commands : constr list -> reduction_function
(** Pattern *)
-val pattern_occs : (occurrences * constr) list -> env -> evar_map -> constr ->
- evar_map * constr
+val pattern_occs : (occurrences * constr) list -> e_reduction_function
(** Rem: Lazy strategies are defined in Reduction *)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 818805a56..2d886b8e1 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -194,7 +194,7 @@ let out_arg = function
let out_with_occurrences (occs,c) =
(Locusops.occurrences_map (List.map out_arg) occs, c)
-let e_red f env evm c = evm, f env evm c
+let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm }
let head_style = false (* Turn to true to have a semantics where simpl
only reduce at the head when an evaluable reference is given, e.g.
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a1ebacea8..a10d8fd2f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -18,6 +18,7 @@ open Tacred
open Proof_type
open Logic
open Refiner
+open Sigma.Notations
let re_sig it gc = { it = it; sigma = gc; }
@@ -70,7 +71,10 @@ let pf_get_new_ids ids gls =
let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
let pf_reduction_of_red_expr gls re c =
- (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c
+ let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
+ let sigma = Sigma.Unsafe.of_evar_map (project gls) in
+ let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
+ (Sigma.to_evar_map sigma, c)
let pf_apply f gls = f (pf_env gls) (project gls)
let pf_eapply f gls x =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 930cfebf4..cdf29e4c6 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -724,8 +724,9 @@ let mkCaseEq a : unit Proofview.tactic =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
- change_concl
- (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl))
+ (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
+ let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in
+ change_concl c
end };
simplest_case a]
end }
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 8b71affff..4fa5ccf35 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1370,7 +1370,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
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 73aa4c337..edad75339 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -805,7 +805,10 @@ let interp_may_eval f ist env sigma = function
| ConstrEval (r,c) ->
let (sigma,redexp) = interp_red_expr ist env sigma r in
let (sigma,c_interp) = f ist env sigma c in
- (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp)
+ let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma c_interp in
+ (Sigma.to_evar_map sigma, c)
| ConstrContext ((loc,s),c) ->
(try
let (sigma,ic) = f ist env sigma c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e36353847..6d589f46f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -569,29 +569,30 @@ let reduct_option ?(check=false) redfun = function
(** Tactic reduction modulo evars (for universes essentially) *)
let pf_e_reduce_decl redfun where (id,c,ty) gl =
- let sigma = Tacmach.New.project gl in
- let redfun = redfun (Tacmach.New.pf_env gl) in
+ let sigma = Proofview.Goal.sigma gl in
+ let redfun sigma c = redfun.e_redfun (Tacmach.New.pf_env gl) sigma c in
match c with
| None ->
if where == InHypValueOnly then
errorlabstrm "" (pr_id id ++ str " has no value.");
- let sigma, ty' = redfun sigma ty in
- sigma, (id,None,ty')
+ let Sigma (ty', sigma, p) = redfun sigma ty in
+ Sigma ((id, None, ty'), sigma, p)
| Some b ->
- let sigma, b' = if where != InHypTypeOnly then redfun sigma b else sigma, b in
- let sigma, ty' = if where != InHypValueOnly then redfun sigma ty else sigma, ty in
- sigma, (id,Some b',ty')
+ let Sigma (b', sigma, p) = if where != InHypTypeOnly then redfun sigma b else Sigma.here b sigma in
+ let Sigma (ty', sigma, q) = if where != InHypValueOnly then redfun sigma ty else Sigma.here ty sigma in
+ Sigma ((id, Some b', ty'), sigma, p +> q)
let e_reduct_in_concl (redfun, sty) =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
- let sigma, c' = Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl) in
- Sigma.Unsafe.of_pair (convert_concl_no_check c' sty, sigma)
+ let sigma = Proofview.Goal.sigma gl in
+ let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
+ Sigma (convert_concl_no_check c' sty, sigma, p)
end }
let e_reduct_in_hyp ?(check=false) redfun (id, where) =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
- let sigma, decl' = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
- Sigma.Unsafe.of_pair (convert_hyp ~check decl', sigma)
+ let Sigma (decl', sigma, p) = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
+ Sigma (convert_hyp ~check decl', sigma, p)
end }
let e_reduct_option ?(check=false) redfun = function
@@ -604,9 +605,8 @@ let e_reduct_option ?(check=false) redfun = function
let e_change_in_concl (redfun,sty) =
Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- let sigma = Sigma.to_evar_map sigma in
- let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in
- Sigma.Unsafe.of_pair (convert_concl_no_check c sty, sigma)
+ let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in
+ Sigma (convert_concl_no_check c sty, sigma, p)
end }
let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma =
@@ -614,24 +614,23 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
| None ->
if where == InHypValueOnly then
errorlabstrm "" (pr_id id ++ str " has no value.");
- let sigma',ty' = redfun false env sigma ty in
- sigma', (id,None,ty')
+ let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
+ Sigma ((id, None, ty'), sigma, p)
| Some b ->
- let sigma',b' =
- if where != InHypTypeOnly then redfun true env sigma b else sigma, b
+ let Sigma (b', sigma, p) =
+ if where != InHypTypeOnly then (redfun true).e_redfun env sigma b else Sigma.here b sigma
in
- let sigma',ty' =
- if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty
+ let Sigma (ty', sigma, q) =
+ if where != InHypValueOnly then (redfun false).e_redfun env sigma ty else Sigma.here ty sigma
in
- sigma', (id,Some b',ty')
+ Sigma ((id, Some b', ty'), sigma, p +> q)
let e_change_in_hyp redfun (id,where) =
Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- let sigma = Sigma.to_evar_map sigma in
let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in
- let sigma, c = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
- Sigma.Unsafe.of_pair (convert_hyp c, sigma)
+ let Sigma (c, sigma, p) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
+ Sigma (convert_hyp c, sigma, p)
end }
type change_arg = Pattern.patvar_map -> constr Sigma.run
@@ -661,32 +660,33 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
else sigma
(* Now we introduce different instances of the previous tacticals *)
-let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
- let sigma = Sigma.Unsafe.of_evar_map sigma in
+let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun env sigma c ->
let Sigma (t', sigma, p) = t.run sigma in
let sigma = Sigma.to_evar_map sigma in
let sigma = check_types env sigma mayneedglobalcheck deep t' c in
let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
- sigma, t'
+ Sigma.Unsafe.of_pair (t', sigma)
+end }
(* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm cv_pb deep t where env sigma c =
+let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c ->
let mayneedglobalcheck = ref false in
- let sigma,c = match where with
- | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+ let Sigma (c, sigma, p) = match where with
+ | None -> (change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty)).e_redfun env sigma c
| Some occl ->
- e_contextually false occl
+ (e_contextually false occl
(fun subst ->
- change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
+ change_and_check Reduction.CONV mayneedglobalcheck true (t subst))).e_redfun
env sigma c in
if !mayneedglobalcheck then
begin
- try ignore (Typing.unsafe_type_of env sigma c)
+ try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) c)
with e when catchable_exception e ->
error "Replacement would lead to an ill-typed term."
end;
- sigma,c
+ Sigma (c, sigma, p)
+end }
let change_in_concl occl t =
e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
@@ -924,9 +924,9 @@ let lookup_hypothesis_as_renamed_gen red h gl =
let rec aux ccl =
match lookup_hypothesis_as_renamed env ccl h with
| None when red ->
- aux
- (snd ((fst (Redexpr.reduction_of_red_expr env (Red true)))
- env (Sigma.to_evar_map (Proofview.Goal.sigma gl)) ccl))
+ let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in
+ let Sigma (c, _, _) = redfun.e_redfun env (Proofview.Goal.sigma gl) ccl in
+ aux c
| x -> x
in
try aux (Proofview.Goal.concl gl)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b6313cdba..aa5f7a692 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -36,12 +36,13 @@ open Evarconv
open Indschemes
open Misctypes
open Vernacexpr
+open Sigma.Notations
let do_universe poly l = Declare.do_universe poly l
let do_constraint poly l = Declare.do_constraint poly l
let rec under_binders env sigma f n c =
- if Int.equal n 0 then snd (f env sigma c) else
+ if Int.equal n 0 then f env sigma c else
match kind_of_term c with
| Lambda (x,t,c) ->
mkLambda (x,t,under_binders (push_rel (x,None,t) env) sigma f (n-1) c)
@@ -71,10 +72,14 @@ let red_constant_entry n ce sigma = function
| Some red ->
let proof_out = ce.const_entry_body in
let env = Global.env () in
+ let (redfun, _) = reduction_of_red_expr env red in
+ let redfun env sigma c =
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma (c, _, _) = redfun.e_redfun env sigma c in
+ c
+ in
{ ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
- (fun ((body,ctx),eff) ->
- (under_binders env sigma
- (fst (reduction_of_red_expr env red)) n body,ctx),eff) }
+ (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
let interp_definition pl bl p red_option c ctypopt =
let env = Global.env() in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0f81943e2..60aab09fd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -32,6 +32,7 @@ open Redexpr
open Lemmas
open Misctypes
open Locality
+open Sigma.Notations
let debug = false
let prerr_endline =
@@ -1537,7 +1538,12 @@ let vernac_check_may_eval redexp glopt rc =
| Some r ->
Tacintern.dump_glob_red_expr r;
let (sigma',r_interp) = interp_redexp env sigma' r in
- let redfun env evm c = snd (fst (reduction_of_red_expr env r_interp) env evm c) in
+ let redfun env evm c =
+ let (redfun, _) = reduction_of_red_expr env r_interp in
+ let evm = Sigma.Unsafe.of_evar_map evm in
+ let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in
+ c
+ in
msg_notice (print_eval redfun env sigma' rc j)
let vernac_declare_reduction locality s r =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 12:19:15 +0000