aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-18 09:36:50 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-18 09:36:50 +0100
commit0168ee0b6463a9ef44d768b0020b34785986c1cb (patch)
treec3bb1d2eef4fa5edfd2d431669015db896e08633
parent50bd89748af03bb28ad7024f2ceef500489a91b0 (diff)
parent53f5cc210da4debd5264d6d8651a76281b0b4256 (diff)
Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.
-rw-r--r--API/API.mli17
-rw-r--r--dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh4
-rw-r--r--dev/doc/changes.md5
-rw-r--r--engine/eConstr.ml23
-rw-r--r--engine/eConstr.mli7
-rw-r--r--interp/constrintern.ml55
-rw-r--r--interp/constrintern.mli29
-rw-r--r--lib/cList.ml35
-rw-r--r--lib/cList.mli7
-rw-r--r--plugins/derive/derive.ml5
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/recdef.ml28
-rw-r--r--tactics/leminv.ml8
-rw-r--r--vernac/classes.ml32
-rw-r--r--vernac/command.ml411
-rw-r--r--vernac/lemmas.ml66
-rw-r--r--vernac/lemmas.mli5
-rw-r--r--vernac/record.ml91
18 files changed, 453 insertions, 379 deletions
diff --git a/API/API.mli b/API/API.mli
index 8f46a5832..6326247f8 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4620,6 +4620,9 @@ end
module Constrintern :
sig
+
+ open Evd
+
type ltac_sign = {
ltac_vars : Names.Id.Set.t;
ltac_bound : Names.Id.Set.t;
@@ -4635,11 +4638,11 @@ sig
| Variable
type internalization_env = var_internalization_data Names.Id.Map.t
- val interp_constr_evars : Environ.env -> Evd.evar_map ref ->
- ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.constr
+ val interp_constr_evars : Environ.env -> evar_map ->
+ ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.constr
- val interp_type_evars : Environ.env -> Evd.evar_map ref ->
- ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types
+ val interp_type_evars : Environ.env -> Evd.evar_map ->
+ ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.types
val empty_ltac_sign : ltac_sign
val intern_gen : Pretyping.typing_constraint -> Environ.env ->
@@ -4657,10 +4660,12 @@ sig
val locate_reference : Libnames.qualid -> Globnames.global_reference
val interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env ->
Constrexpr.constr_expr -> Constr.types Evd.in_evar_universe_context
+
val interp_context_evars :
?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
- Environ.env -> Evd.evar_map ref -> Constrexpr.local_binder_expr list ->
- internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits)
+ Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list ->
+ evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits))
+
val compute_internalization_data : Environ.env -> var_internalization_type ->
Constr.types -> Impargs.manual_explicitation list -> var_internalization_data
val empty_internalization_env : internalization_env
diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
new file mode 100644
index 000000000..8aea7dee3
--- /dev/null
+++ b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then
+ Equations_CI_BRANCH=interp+less_impstyle_p2
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index c69be4f4d..01aa6b599 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -46,6 +46,11 @@ We changed the type of the following functions:
- `Global.body_of_constant`: same as above.
+- `Constrinterp.*` generally, many functions that used to take an
+ `evar_map ref` have been now switched to functions that will work in
+ a functional way. The old style of passing `evar_map`s as references
+ is not supported anymore.
+
We have changed the representation of the following types:
- `Lib.object_prefix` is now a record instead of a nested tuple.
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 53123c933..a65b3941e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -770,6 +770,20 @@ let rec isArity sigma c =
| Sort _ -> true
| _ -> false
+type arity = rel_context * ESorts.t
+
+let destArity sigma =
+ let open Context.Rel.Declaration in
+ let rec prodec_rec l c =
+ match kind sigma c with
+ | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c
+ | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
+ | Cast (c,_,_) -> prodec_rec l c
+ | Sort s -> l,s
+ | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.")
+ in
+ prodec_rec []
+
let mkProd_or_LetIn decl c =
let open Context.Rel.Declaration in
match decl with
@@ -817,6 +831,15 @@ let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
+let map_rel_context_in_env f env sign =
+ let rec aux env acc = function
+ | d::sign ->
+ aux (push_rel d env) (Context.Rel.Declaration.map_constr (f env) d :: acc) sign
+ | [] ->
+ acc
+ in
+ aux env [] (List.rev sign)
+
let fresh_global ?loc ?rigid ?names env sigma reference =
let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
evd, of_constr t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 6f2a30f4a..30de748a1 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -146,7 +146,11 @@ val isFix : Evd.evar_map -> t -> bool
val isCoFix : Evd.evar_map -> t -> bool
val isCase : Evd.evar_map -> t -> bool
val isProj : Evd.evar_map -> t -> bool
+
+type arity = rel_context * ESorts.t
+val destArity : Evd.evar_map -> types -> arity
val isArity : Evd.evar_map -> t -> bool
+
val isVarId : Evd.evar_map -> Id.t -> t -> bool
val isRelN : Evd.evar_map -> int -> t -> bool
@@ -262,6 +266,9 @@ val lookup_rel : int -> env -> rel_declaration
val lookup_named : variable -> env -> named_declaration
val lookup_named_val : variable -> named_context_val -> named_declaration
+val map_rel_context_in_env :
+ (env -> constr -> constr) -> env -> rel_context -> rel_context
+
(* XXX Missing Sigma proxy *)
val fresh_global :
?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 14234b311..61b33aa41 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2098,39 +2098,36 @@ let interp_open_constr env sigma c =
(* Not all evars expected to be resolved and computation of implicit args *)
-let interp_constr_evars_gen_impls env evdref
+let interp_constr_evars_gen_impls env sigma
?(impls=empty_internalization_env) expected_type c =
let c = intern_gen expected_type ~impls env c in
let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
- let evd, c = understand_tcc env !evdref ~expected_type c in
- evdref := evd;
- c, imps
+ let sigma, c = understand_tcc env sigma ~expected_type c in
+ sigma, (c, imps)
-let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c =
+ interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c
let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ =
interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c
-let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen_impls env evdref ~impls IsType c
+let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c =
+ interp_constr_evars_gen_impls env sigma ~impls IsType c
(* Not all evars expected to be resolved, with side-effect on evars *)
-let interp_constr_evars_gen env evdref ?(impls=empty_internalization_env) expected_type c =
+let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c =
let c = intern_gen expected_type ~impls env c in
- let evd, c = understand_tcc env !evdref ~expected_type c in
- evdref := evd;
- c
+ understand_tcc env sigma ~expected_type c
let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
-let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ =
- interp_constr_evars_gen env evdref ~impls (OfType typ) c
+let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ =
+ interp_constr_evars_gen env sigma ~impls (OfType typ) c
-let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen env evdref IsType ~impls c
+let interp_type_evars env sigma ?(impls=empty_internalization_env) c =
+ interp_constr_evars_gen env sigma IsType ~impls c
(* Miscellaneous *)
@@ -2185,17 +2182,16 @@ let intern_context global_level env impl_env binders =
with InternalizationError (loc,e) ->
user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
-let interp_glob_context_evars env evdref k bl =
+let interp_glob_context_evars env sigma k bl =
let open EConstr in
- let (env, par, _, impls) =
+ let env, sigma, par, _, impls =
List.fold_left
- (fun (env,params,n,impls) (na, k, b, t) ->
+ (fun (env,sigma,params,n,impls) (na, k, b, t) ->
let t' =
if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
else t
in
- let (evd,t) = understand_tcc env !evdref ~expected_type:IsType t' in
- evdref := evd;
+ let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in
match b with
None ->
let d = LocalAssum (na,t) in
@@ -2205,16 +2201,15 @@ let interp_glob_context_evars env evdref k bl =
(ExplByPos (n, na), (true, true, true)) :: impls
else impls
in
- (push_rel d env, d::params, succ n, impls)
+ (push_rel d env, sigma, d::params, succ n, impls)
| Some b ->
- let (evd,c) = understand_tcc env !evdref ~expected_type:(OfType t) b in
- evdref := evd;
+ let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in
let d = LocalDef (na, c, t) in
- (push_rel d env, d::params, n, impls))
- (env,[],k+1,[]) (List.rev bl)
- in (env, par), impls
+ (push_rel d env, sigma, d::params, n, impls))
+ (env,sigma,[],k+1,[]) (List.rev bl)
+ in sigma, ((env, par), impls)
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
let int_env,bl = intern_context global_level env impl_env params in
- let x = interp_glob_context_evars env evdref shift bl in
- int_env, x
+ let sigma, x = interp_glob_context_evars env sigma shift bl in
+ sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index af4e4a9c5..632b423b0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -112,29 +112,28 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.co
(** Accepting unresolved evars *)
-val interp_constr_evars : env -> evar_map ref ->
- ?impls:internalization_env -> constr_expr -> EConstr.constr
+val interp_constr_evars : env -> evar_map ->
+ ?impls:internalization_env -> constr_expr -> evar_map * EConstr.constr
+val interp_casted_constr_evars : env -> evar_map ->
+ ?impls:internalization_env -> constr_expr -> EConstr.types -> evar_map * EConstr.constr
-val interp_casted_constr_evars : env -> evar_map ref ->
- ?impls:internalization_env -> constr_expr -> EConstr.types -> EConstr.constr
-
-val interp_type_evars : env -> evar_map ref ->
- ?impls:internalization_env -> constr_expr -> EConstr.types
+val interp_type_evars : env -> evar_map ->
+ ?impls:internalization_env -> constr_expr -> evar_map * EConstr.types
(** Accepting unresolved evars and giving back the manual implicit arguments *)
-val interp_constr_evars_impls : env -> evar_map ref ->
+val interp_constr_evars_impls : env -> evar_map ->
?impls:internalization_env -> constr_expr ->
- EConstr.constr * Impargs.manual_implicits
+ evar_map * (EConstr.constr * Impargs.manual_implicits)
-val interp_casted_constr_evars_impls : env -> evar_map ref ->
+val interp_casted_constr_evars_impls : env -> evar_map ->
?impls:internalization_env -> constr_expr -> EConstr.types ->
- EConstr.constr * Impargs.manual_implicits
+ evar_map * (EConstr.constr * Impargs.manual_implicits)
-val interp_type_evars_impls : env -> evar_map ref ->
+val interp_type_evars_impls : env -> evar_map ->
?impls:internalization_env -> constr_expr ->
- EConstr.types * Impargs.manual_implicits
+ evar_map * (EConstr.types * Impargs.manual_implicits)
(** Interprets constr patterns *)
@@ -159,8 +158,8 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst
val interp_context_evars :
?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
- env -> evar_map ref -> local_binder_expr list ->
- internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits)
+ env -> evar_map -> local_binder_expr list ->
+ evar_map * (internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits))
(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
(* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
diff --git a/lib/cList.ml b/lib/cList.ml
index ca69628af..0ef7c3d8b 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -96,6 +96,8 @@ sig
val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
+ val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+ val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
@@ -446,6 +448,12 @@ let rec fold_left3 f accu l1 l2 l3 =
| (a1::l1, a2::l2, a3::l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3
| (_, _, _) -> invalid_arg "List.fold_left3"
+let rec fold_left4 f accu l1 l2 l3 l4 =
+ match (l1, l2, l3, l4) with
+ ([], [], [], []) -> accu
+ | (a1::l1, a2::l2, a3::l3, a4::l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4
+ | (_,_, _, _) -> invalid_arg "List.fold_left4"
+
(* [fold_right_and_left f [a1;...;an] hd =
f (f (... (f (f hd
an
@@ -765,12 +773,13 @@ let share_tails l1 l2 =
in
shr_rev [] (List.rev l1, List.rev l2)
+(* Poor man's monadic map *)
let rec fold_left_map f e = function
- | [] -> (e,[])
- | h::t ->
- let e',h' = f e h in
- let e'',t' = fold_left_map f e' t in
- e'',h'::t'
+ | [] -> (e,[])
+ | h::t ->
+ let e',h' = f e h in
+ let e'',t' = fold_left_map f e' t in
+ e'',h'::t'
let fold_map = fold_left_map
@@ -790,12 +799,26 @@ let fold_right_map f l e =
let fold_map' = fold_right_map
+let on_snd f (x,y) = (x,f y)
+
let fold_left2_map f e l l' =
- List.fold_left2 (fun (e,l) x x' -> let (e,y) = f e x x' in (e,y::l)) (e,[]) l l'
+ on_snd List.rev @@
+ List.fold_left2 (fun (e,l) x x' ->
+ let (e,y) = f e x x' in
+ (e, y::l)
+ ) (e, []) l l'
let fold_right2_map f l l' e =
List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e)
+let fold_left3_map f e l l' l'' =
+ on_snd List.rev @@
+ fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l''
+
+let fold_left4_map f e l1 l2 l3 l4 =
+ on_snd List.rev @@
+ fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4
+
let map_assoc f = List.map (fun (x,a) -> (x,f a))
let rec assoc_f f a = function
diff --git a/lib/cList.mli b/lib/cList.mli
index 8cb07da79..f87db04cf 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -211,7 +211,14 @@ sig
val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
(** Same with two lists, folding on the right *)
+ val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+ (** Same with three lists, folding on the left *)
+
+ val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
+ (** Same with four lists, folding on the left *)
+
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+ (* [@@ocaml.deprecated "Same as [fold_left_map]"] *)
(** @deprecated Same as [fold_left_map] *)
val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index fb65a8639..c8c4c2dad 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -38,9 +38,8 @@ let start_deriving f suchthat lemma =
let f_type = EConstr.Unsafe.to_constr f_type in
let ef = EConstr.Unsafe.to_constr ef in
let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
- let evdref = ref sigma in
- let suchthat = Constrintern.interp_type_evars env' evdref suchthat in
- TCons ( env' , !evdref , suchthat , (fun sigma _ ->
+ let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in
+ TCons ( env' , sigma , suchthat , (fun sigma _ ->
TNil sigma))))))
in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9e22ad306..357755e46 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -158,8 +158,8 @@ let build_newrecursive
(fun (env,impls) (((_,recname),_),bl,arityc,_) ->
let arityc = Constrexpr_ops.mkCProdN bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
- let evdref = ref (Evd.from_env env0) in
- let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
+ let evd = Evd.from_env env0 in
+ let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
let open Context.Named.Declaration in
(Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 766adfc63..363ad5dfc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1427,7 +1427,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
- let evmap, env = Pfedit.get_current_context () in
+ let evd, env = Pfedit.get_current_context () in
Lemmas.start_proof thm_name
(Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
@@ -1479,13 +1479,13 @@ let (com_eqn : int -> Id.t ->
| ConstRef c -> is_opaque_constant c
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
- let evmap, env = Pfedit.get_current_context () in
- let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
+ let evd, env = Pfedit.get_current_context () in
+ let evd = Evd.from_ctx (Evd.evar_universe_context evd) in
let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(Lemmas.start_proof eq_name (Global, false, Proof Lemma)
~sign:(Environ.named_context_val env)
- evmap
+ evd
(EConstr.of_constr equation_lemma_type)
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (by
@@ -1528,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let open Constr in
let open CVars in
let env = Global.env() in
- let evd = ref (Evd.from_env env) in
- let function_type = interp_type_evars env evd type_of_f in
+ let evd = Evd.from_env env in
+ let evd, function_type = interp_type_evars env evd type_of_f in
let function_type = EConstr.Unsafe.to_constr function_type in
let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
(* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
- let ty = interp_type_evars env evd ~impls:rec_impls eq in
+ let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
let ty = EConstr.Unsafe.to_constr ty in
- let evm, nf = Evarutil.nf_evars_and_universes !evd in
+ let evd, nf = Evarutil.nf_evars_and_universes evd in
let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in
let function_type = nf function_type in
let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
@@ -1560,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
- let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in
+ let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in
declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
in
(* Refresh the global universes, now including those of _F *)
- let evm = Evd.from_env (Global.env ()) in
+ let evd = Evd.from_env (Global.env ()) in
let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
let relation, evuctx =
- interp_constr env_with_pre_rec_args evm r
+ interp_constr env_with_pre_rec_args evd r
in
- let evm = Evd.from_ctx evuctx in
+ let evd = Evd.from_ctx evuctx in
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
@@ -1599,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
and functional_ref = destConst (constr_of_global functional_ref)
and eq_ref = destConst (constr_of_global eq_ref) in
generate_induction_principle f_ref tcc_lemma_constr
- functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation);
+ functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation);
Flags.if_verbose
msgnl (h 1 (Ppconstr.pr_id function_name ++
spc () ++ str"is defined" )++ fnl () ++
@@ -1618,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- evm (Lemmas.mk_hook hook))
+ evd (Lemmas.mk_hook hook))
()
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1ae3577ed..01065868d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -249,11 +249,11 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
let add_inversion_lemma_exn na com comsort bool tac =
let env = Global.env () in
- let evd = ref (Evd.from_env env) in
- let c = Constrintern.interp_type_evars env evd com in
- let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in
+ let sigma = Evd.from_env env in
+ let sigma, c = Constrintern.interp_type_evars env sigma com in
+ let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in
try
- add_inversion_lemma na env evd c sort bool tac
+ add_inversion_lemma na env sigma c sort bool tac
with
| UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
user_err ~hdr:"Inv needs Nodep Prop Set" s
diff --git a/vernac/classes.ml b/vernac/classes.ml
index fd43c6041..efaf6c0c0 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -82,18 +82,18 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m
let type_ctx_instance env sigma ctx inst subst =
let open Vars in
- let rec aux (subst, instctx) l = function
+ let rec aux (sigma, subst, instctx) l = function
decl :: ctx ->
let t' = substl subst (RelDecl.get_type decl) in
- let c', l =
+ let (sigma, c'), l =
match decl with
| LocalAssum _ -> interp_casted_constr_evars env sigma (List.hd l) t', List.tl l
- | LocalDef (_,b,_) -> substl subst b, l
+ | LocalDef (_,b,_) -> (sigma, substl subst b), l
in
let d = RelDecl.get_name decl, Some c', t' in
- aux (c' :: subst, d :: instctx) l ctx
- | [] -> subst
- in aux (subst, []) inst (List.rev ctx)
+ aux (sigma, c' :: subst, d :: instctx) l ctx
+ | [] -> sigma, subst
+ in aux (sigma, subst, []) inst (List.rev ctx)
let id_of_class cl =
match cl.cl_impl with
@@ -153,10 +153,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
else tclass
in
let sigma, k, u, cty, ctx', ctx, len, imps, subst =
- let _evd = ref sigma in
- let impls, ((env', ctx), imps) = interp_context_evars env _evd ctx in
- let c', imps' = interp_type_evars_impls ~impls env' _evd tclass in
- let sigma = !_evd in
+ let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
+ let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
let len = List.length ctx in
let imps = imps @ Impargs.lift_implicits len imps' in
let ctx', c = decompose_prod_assum sigma c' in
@@ -225,9 +223,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
| None ->
(if List.is_empty k.cl_props then Some (Inl subst) else None), sigma
| Some (Inr term) ->
- let _evd = ref sigma in
- let c = interp_casted_constr_evars env' _evd term cty in
- Some (Inr (c, subst)), !_evd
+ let sigma, c = interp_casted_constr_evars env' sigma term cty in
+ Some (Inr (c, subst)), sigma
| Some (Inl props) ->
let get_id =
function
@@ -265,9 +262,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
unbound_method env' k.cl_impl (get_id n)
| _ ->
let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
- let _evd = ref sigma in
- let r_term = type_ctx_instance (push_rel_context ctx' env') _evd kcl_props props subst in
- Some (Inl r_term), !_evd
+ let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in
+ Some (Inl res), sigma
in
let term, termtype =
match subst with
@@ -367,9 +363,7 @@ let named_of_rel_context l =
let context poly l =
let env = Global.env() in
let sigma = Evd.from_env env in
- let _evd = ref sigma in
- let _, ((env', fullctx), impls) = interp_context_evars env _evd l in
- let sigma = !_evd in
+ let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in
(* Note, we must use the normalized evar from now on! *)
let sigma,_ = Evarutil.nf_evars_and_universes sigma in
let ce t = Pretyping.check_evars env Evd.empty sigma t in
diff --git a/vernac/command.ml b/vernac/command.ml
index 64412b20f..837785ff0 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -91,33 +91,32 @@ let warn_implicits_in_term =
let interp_definition pl bl poly red_option c ctypopt =
let env = Global.env() in
let evd, decl = Univdecls.interp_univ_decl_opt env pl in
- let evdref = ref evd in
- let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
+ let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
let nb_args = Context.Rel.nhyps ctx in
- let imps,ce =
+ let evd,imps,ce =
match ctypopt with
None ->
- let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let evd, subst = Evd.nf_univ_variables evd in
let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
- let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
+ let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in
let c = EConstr.Unsafe.to_constr c in
- let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
+ let evd,nf = Evarutil.nf_evars_and_universes evd in
let body = nf (it_mkLambda_or_LetIn c ctx) in
- let vars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in
- let () = evdref := Evd.restrict_universe_context !evdref vars in
- let uctx = Evd.check_univ_decl ~poly !evdref decl in
- imps1@(Impargs.lift_implicits nb_args imps2),
+ let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
+ let evd = Evd.restrict_universe_context evd vars in
+ let uctx = Evd.check_univ_decl ~poly evd decl in
+ evd, imps1@(Impargs.lift_implicits nb_args imps2),
definition_entry ~univs:uctx body
| Some ctyp ->
- let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
- let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in
+ let evd, subst = Evd.nf_univ_variables evd in
let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
- let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
+ let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
let c = EConstr.Unsafe.to_constr c in
- let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+ let evd, nf = Evarutil.nf_evars_and_universes evd in
let body = nf (it_mkLambda_or_LetIn c ctx) in
let ty = EConstr.Unsafe.to_constr ty in
let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in
@@ -130,15 +129,15 @@ let interp_definition pl bl poly red_option c ctypopt =
in
if not (try List.for_all chk imps2 with Not_found -> false)
then warn_implicits_in_term ();
- let bodyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr body) in
- let tyvars = EConstr.universes_of_constr env !evdref (EConstr.of_constr ty) in
+ let bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in
+ let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in
let vars = Univ.LSet.union bodyvars tyvars in
- let () = evdref := Evd.restrict_universe_context !evdref vars in
- let uctx = Evd.check_univ_decl ~poly !evdref decl in
- imps1@(Impargs.lift_implicits nb_args impsty),
+ let evd = Evd.restrict_universe_context evd vars in
+ let uctx = Evd.check_univ_decl ~poly evd decl in
+ evd, imps1@(Impargs.lift_implicits nb_args impsty),
definition_entry ~types:typ ~univs:uctx body
in
- (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps)
+ (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps)
let check_definition (ce, evd, _, imps) =
check_evars_are_solved (Global.env ()) evd Evd.empty;
@@ -232,11 +231,11 @@ match local with
in
(gr,inst,Lib.is_modtype_strict ())
-let interp_assumption evdref env impls bl c =
+let interp_assumption sigma env impls bl c =
let c = mkCProdN ?loc:(local_binders_loc bl) bl c in
- let ty, impls = interp_type_evars_impls env evdref ~impls c in
+ let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in
let ty = EConstr.Unsafe.to_constr ty in
- (ty, impls)
+ sigma, (ty, impls)
(* When monomorphic the universe constraints are declared with the first declaration only. *)
let next_uctx =
@@ -285,10 +284,7 @@ let do_assumptions kind nl l =
let open Context.Named.Declaration in
let env = Global.env () in
let udecl, l = process_assumptions_udecls kind l in
- let evdref, udecl =
- let evd, udecl = Univdecls.interp_univ_decl_opt env udecl in
- ref evd, udecl
- in
+ let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
let l =
if pi2 kind (* poly *) then
(* Separate declarations so that A B : Type puts A and B in different levels. *)
@@ -299,29 +295,29 @@ let do_assumptions kind nl l =
else l
in
(* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
- let _,l = List.fold_left_map (fun (env,ienv) (is_coe,(idl,c)) ->
- let t,imps = interp_assumption evdref env ienv [] c in
+ let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
+ let sigma,(t,imps) = interp_assumption sigma env ienv [] c in
let env =
push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in
let ienv = List.fold_right (fun (_,id) ienv ->
let impls = compute_internalization_data env Variable t imps in
Id.Map.add id impls ienv) idl ienv in
- ((env,ienv),((is_coe,idl),t,imps)))
- (env,empty_internalization_env) l
+ ((sigma,env,ienv),((is_coe,idl),t,imps)))
+ (sigma,env,empty_internalization_env) l
in
- let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in
+ let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in
(* The universe constraints come from the whole telescope. *)
- let evd = Evd.nf_constraints evd in
- let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in
+ let sigma = Evd.nf_constraints sigma in
+ let nf_evar c = EConstr.to_constr sigma (EConstr.of_constr c) in
let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
let t = nf_evar t in
let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in
uvars, (coe,t,imps))
Univ.LSet.empty l
in
- let evd = Evd.restrict_universe_context evd uvars in
- let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd udecl in
- let ubinders = Evd.universe_binders evd in
+ let sigma = Evd.restrict_universe_context sigma uvars in
+ let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in
+ let ubinders = Evd.universe_binders sigma in
pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
let t = replace_vars subst t in
let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
@@ -375,8 +371,8 @@ let check_all_names_different indl =
| [] -> ()
| _ -> raise (InductiveError (SameNamesOverlap l))
-let mk_mltype_data evdref env assums arity indname =
- let is_ml_type = is_sort env !evdref (EConstr.of_constr arity) in
+let mk_mltype_data sigma env assums arity indname =
+ let is_ml_type = is_sort env sigma (EConstr.of_constr arity) in
(is_ml_type,indname,assums)
let prepare_param = function
@@ -400,40 +396,43 @@ let rec check_anonymous_type ind =
| GCast (e, _) -> check_anonymous_type e
| _ -> false
-let make_conclusion_flexible evdref ty poly =
+let make_conclusion_flexible sigma ty poly =
if poly && Term.isArity ty then
let _, concl = Term.destArity ty in
match concl with
| Type u ->
(match Univ.universe_level u with
| Some u ->
- evdref := Evd.make_flexible_variable !evdref ~algebraic:true u
- | None -> ())
- | _ -> ()
- else ()
-
-let is_impredicative env u =
+ Evd.make_flexible_variable sigma ~algebraic:true u
+ | None -> sigma)
+ | _ -> sigma
+ else sigma
+
+let is_impredicative env u =
u = Prop Null || (is_impredicative_set env && u = Prop Pos)
-let interp_ind_arity env evdref ind =
+let interp_ind_arity env sigma ind =
let c = intern_gen IsType env ind.ind_arity in
let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
- let (evd,t) = understand_tcc env !evdref ~expected_type:IsType c in
- evdref := evd;
+ let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
let pseudo_poly = check_anonymous_type c in
- let () = if not (Reductionops.is_arity env !evdref t) then
+ let () = if not (Reductionops.is_arity env sigma t) then
user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
in
let t = EConstr.Unsafe.to_constr t in
- t, pseudo_poly, impls
+ sigma, (t, pseudo_poly, impls)
-let interp_cstrs evdref env impls mldata arity ind =
+let interp_cstrs env sigma impls mldata arity ind =
let cnames,ctyps = List.split ind.ind_lc in
(* Complete conclusions of constructor types if given in ML-style syntax *)
let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
(* Interpret the constructor types *)
- let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls %> on_fst EConstr.Unsafe.to_constr) ctyps') in
- (cnames, ctyps'', cimpls)
+ let sigma, (ctyps'', cimpls) =
+ on_snd List.split @@
+ List.fold_left_map (fun sigma l ->
+ on_snd (on_fst EConstr.Unsafe.to_constr) @@
+ interp_type_evars_impls env sigma ~impls l) sigma ctyps' in
+ sigma, (cnames, ctyps'', cimpls)
let sign_level env evd sign =
fst (List.fold_right
@@ -461,7 +460,7 @@ let is_flexible_sort evd u =
| Some l -> Evd.is_flexible_level evd l
| None -> false
-let inductive_levels env evdref poly arities inds =
+let inductive_levels env evd poly arities inds =
let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
let levels = List.map (fun (x,(ctx,a)) ->
if a = Prop Null then None
@@ -480,11 +479,11 @@ let inductive_levels env evdref poly arities inds =
let minlev =
(** Indices contribute. *)
if Indtypes.is_indices_matter () && List.length ctx > 0 then (
- let ilev = sign_level env !evdref ctx in
+ let ilev = sign_level env evd ctx in
Univ.sup ilev minlev)
else minlev
in
- let clev = extract_level env !evdref minlev tys in
+ let clev = extract_level env evd minlev tys in
(clev, minlev, len)) inds destarities)
in
(* Take the transitive closure of the system of constructors *)
@@ -529,8 +528,8 @@ let inductive_levels env evdref poly arities inds =
else Evd.set_eq_sort env evd (Type cu) du
in
(evd, arity :: arities))
- (!evdref,[]) (Array.to_list levels') destarities sizes
- in evdref := evd; List.rev arities
+ (evd,[]) (Array.to_list levels') destarities sizes
+ in evd, List.rev arities
let check_named (loc, na) = match na with
| Name _ -> ()
@@ -551,20 +550,19 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
List.iter check_param paramsl;
let env0 = Global.env() in
let pl = (List.hd indl).ind_univs in
- let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
- let evdref = ref evd in
- let impls, ((env_params, ctx_params), userimpls) =
- interp_context_evars env0 evdref paramsl
+ let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+ let sigma, (impls, ((env_params, ctx_params), userimpls)) =
+ interp_context_evars env0 sigma paramsl
in
let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in
let indnames = List.map (fun ind -> ind.ind_name) indl in
-
+
(* Names of parameters as arguments of the inductive type (defs removed) *)
let assums = List.filter is_local_assum ctx_params in
let params = List.map (RelDecl.get_name %> Name.get_id) assums in
(* Interpret the arities *)
- let arities = List.map (interp_ind_arity env_params evdref) indl in
+ let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in
let env_ar = push_types env0 indnames fullarities in
@@ -576,36 +574,34 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in
- let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
+ let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
- let constructors =
+ let sigma, constructors =
Metasyntax.with_syntax_protection (fun () ->
(* Temporary declaration of notations and scopes *)
List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations;
(* Interpret the constructor types *)
- List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl)
+ List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl)
() in
(* Try further to solve evars, and instantiate them *)
- let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in
- evdref := sigma;
+ let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
(* Compute renewed arities *)
- let nf,_ = e_nf_evars_and_universes evdref in
+ let sigma, nf = nf_evars_and_universes sigma in
let arities = List.map nf arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
- let _ = List.iter2 (fun ty poly -> make_conclusion_flexible evdref ty poly) arities aritypoly in
- let arities = inductive_levels env_ar_params evdref poly arities constructors in
- let nf',_ = e_nf_evars_and_universes evdref in
+ let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
+ let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
+ let sigma, nf' = nf_evars_and_universes sigma in
let nf x = nf' (nf x) in
let arities = List.map nf' arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
let ctx_params = Context.Rel.map nf ctx_params in
- let evd = !evdref in
- let uctx = Evd.check_univ_decl ~poly evd decl in
- List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
- Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
+ let uctx = Evd.check_univ_decl ~poly sigma decl in
+ List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities;
+ Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
- List.iter (fun c -> check_evars env_ar_params Evd.empty evd (EConstr.of_constr c)) ctyps)
+ List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (EConstr.of_constr c)) ctyps)
constructors;
(* Build the inductive entries *)
@@ -642,8 +638,8 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
}
in
(if poly && cum then
- Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
- else mind_ent), Evd.universe_binders evd, impls
+ Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent
+ else mind_ent), Evd.universe_binders sigma, impls
(* Very syntactical equality *)
let eq_local_binders bl1 bl2 =
@@ -830,23 +826,22 @@ type structured_fixpoint_expr = {
fix_type : constr_expr
}
-let interp_fix_context env evdref isfix fix =
+let interp_fix_context env sigma isfix fix =
let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
- let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
- let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in
+ let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars env sigma before in
+ let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in
let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
- ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
+ sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
-let interp_fix_ccl evdref impls (env,_) fix =
- let (c, impl) = interp_type_evars_impls ~impls env evdref fix.fix_type in
- (c, impl)
+let interp_fix_ccl sigma impls (env,_) fix =
+ interp_type_evars_impls ~impls env sigma fix.fix_type
-let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
+let interp_fix_body env_rec sigma impls (_,ctx) fix ccl =
let open EConstr in
- Option.map (fun body ->
+ Option.cata (fun body ->
let env = push_rel_context ctx env_rec in
- let body = interp_casted_constr_evars env evdref ~impls body ccl in
- it_mkLambda_or_LetIn body ctx) fix.fix_body
+ let sigma, body = interp_casted_constr_evars env sigma ~impls body ccl in
+ sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body
let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
@@ -883,56 +878,58 @@ let fixsub_module = subtac_dir @ ["Wf"]
let tactics_module = subtac_dir @ ["Tactics"]
let init_reference dir s () = Coqlib.coq_reference "Command" dir s
-let init_constant dir s evdref =
- let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s)
- in evdref := sigma; c
+let init_constant dir s sigma =
+ Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s)
let make_ref l s = init_reference l s
let fix_proto = init_constant tactics_module "fix_proto"
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
-let mkSubset evdref name typ prop =
+let mkSubset sigma name typ prop =
let open EConstr in
- mkApp (Evarutil.e_new_global evdref (delayed_force build_sigma).typ,
- [| typ; mkLambda (name, typ, prop) |])
+ let sigma, h_term = Evarutil.new_global sigma (delayed_force build_sigma).typ in
+ sigma, mkApp (h_term, [| typ; mkLambda (name, typ, prop) |])
+
let sigT = Lazy.from_fun build_sigma_type
let make_qref s = Qualid (Loc.tag @@ qualid_of_string s)
let lt_ref = make_qref "Init.Peano.lt"
-let rec telescope evdref l =
+let rec telescope sigma l =
let open EConstr in
let open Vars in
match l with
| [] -> assert false
- | [LocalAssum (n, t)] -> t, [LocalDef (n, mkRel 1, t)], mkRel 1
+ | [LocalAssum (n, t)] ->
+ sigma, t, [LocalDef (n, mkRel 1, t)], mkRel 1
| LocalAssum (n, t) :: tl ->
- let ty, tys, (k, constr) =
+ let sigma, ty, tys, (k, constr) =
List.fold_left
- (fun (ty, tys, (k, constr)) decl ->
+ (fun (sigma, ty, tys, (k, constr)) decl ->
let t = RelDecl.get_type decl in
let pred = mkLambda (RelDecl.get_name decl, t, ty) in
- let ty = Evarutil.e_new_global evdref (Lazy.force sigT).typ in
- let intro = Evarutil.e_new_global evdref (Lazy.force sigT).intro in
+ let sigma, ty = Evarutil.new_global sigma (Lazy.force sigT).typ in
+ let sigma, intro = Evarutil.new_global sigma (Lazy.force sigT).intro in
let sigty = mkApp (ty, [|t; pred|]) in
let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
- (sigty, pred :: tys, (succ k, intro)))
- (t, [], (2, mkRel 1)) tl
+ (sigma, sigty, pred :: tys, (succ k, intro)))
+ (sigma, t, [], (2, mkRel 1)) tl
in
- let (last, subst) = List.fold_right2
- (fun pred decl (prev, subst) ->
+ let sigma, last, subst = List.fold_right2
+ (fun pred decl (sigma, prev, subst) ->
let t = RelDecl.get_type decl in
- let p1 = Evarutil.e_new_global evdref (Lazy.force sigT).proj1 in
- let p2 = Evarutil.e_new_global evdref (Lazy.force sigT).proj2 in
+ let sigma, p1 = Evarutil.new_global sigma (Lazy.force sigT).proj1 in
+ let sigma, p2 = Evarutil.new_global sigma (Lazy.force sigT).proj2 in
let proj1 = applist (p1, [t; pred; prev]) in
let proj2 = applist (p2, [t; pred; prev]) in
- (lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
- (List.rev tys) tl (mkRel 1, [])
- in ty, (LocalDef (n, last, t) :: subst), constr
+ (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
+ (List.rev tys) tl (sigma, mkRel 1, [])
+ in sigma, ty, (LocalDef (n, last, t) :: subst), constr
- | LocalDef (n, b, t) :: tl -> let ty, subst, term = telescope evdref tl in
- ty, (LocalDef (n, b, t) :: subst), lift 1 term
+ | LocalDef (n, b, t) :: tl ->
+ let sigma, ty, subst, term = telescope sigma tl in
+ sigma, ty, (LocalDef (n, b, t) :: subst), lift 1 term
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
@@ -943,56 +940,59 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
Coqlib.check_required_library ["Coq";"Program";"Wf"];
let env = Global.env() in
- let evd, decl = Univdecls.interp_univ_decl_opt env pl in
- let evdref = ref evd in
- let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
+ let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
+ let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in
let len = List.length binders_rel in
let top_env = push_rel_context binders_rel env in
- let top_arity = interp_type_evars top_env evdref arityc in
+ let sigma, top_arity = interp_type_evars top_env sigma arityc in
let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
- let argtyp, letbinders, make = telescope evdref binders_rel in
+ let sigma, argtyp, letbinders, make = telescope sigma binders_rel in
let argname = Id.of_string "recarg" in
let arg = LocalAssum (Name argname, argtyp) in
let binders = letbinders @ [arg] in
let binders_env = push_rel_context binders_rel env in
- let rel, _ = interp_constr_evars_impls env evdref r in
- let relty = Typing.unsafe_type_of env !evdref rel in
+ let sigma, (rel, _) = interp_constr_evars_impls env sigma r in
+ let relty = Typing.unsafe_type_of env sigma rel in
let relargty =
let error () =
user_err ?loc:(constr_loc r)
~hdr:"Command.build_wellfounded"
- (Printer.pr_econstr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
+ (Printer.pr_econstr_env env sigma rel ++ str " is not an homogeneous binary relation.")
in
try
- let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in
- match ctx, EConstr.kind !evdref ar with
+ let ctx, ar = Reductionops.splay_prod_n env sigma 2 relty in
+ match ctx, EConstr.kind sigma ar with
| [LocalAssum (_,t); LocalAssum (_,u)], Sort s
- when Sorts.is_prop (ESorts.kind !evdref s) && Reductionops.is_conv env !evdref t u -> t
+ when Sorts.is_prop (ESorts.kind sigma s) && Reductionops.is_conv env sigma t u -> t
| _, _ -> error ()
with e when CErrors.noncritical e -> error ()
in
- let measure = interp_casted_constr_evars binders_env evdref measure relargty in
- let wf_rel, wf_rel_fun, measure_fn =
+ let sigma, measure = interp_casted_constr_evars binders_env sigma measure relargty in
+ let sigma, wf_rel, wf_rel_fun, measure_fn =
let measure_body, measure =
it_mkLambda_or_LetIn measure letbinders,
it_mkLambda_or_LetIn measure binders
in
- let comb = Evarutil.e_new_global evdref (delayed_force measure_on_R_ref) in
+ let sigma, comb = Evarutil.new_global sigma (delayed_force measure_on_R_ref) in
let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
let wf_rel_fun x y =
mkApp (rel, [| subst1 x measure_body;
subst1 y measure_body |])
- in wf_rel, wf_rel_fun, measure
+ in sigma, wf_rel, wf_rel_fun, measure
in
- let wf_proof = mkApp (well_founded evdref, [| argtyp ; wf_rel |]) in
+ let sigma, wf_term = well_founded sigma in
+ let wf_proof = mkApp (wf_term, [| argtyp ; wf_rel |]) in
let argid' = Id.of_string (Id.to_string argname ^ "'") in
- let wfarg len = LocalAssum (Name argid',
- mkSubset evdref (Name argid') argtyp
- (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
+ let wfarg sigma len =
+ let sigma, ss_term = mkSubset sigma (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1))) in
+ sigma, LocalAssum (Name argid', ss_term)
+ in
+ let sigma, intern_bl =
+ let sigma, wfa = wfarg sigma 1 in
+ sigma, wfa :: [arg]
in
- let intern_bl = wfarg 1 :: [arg] in
let _intern_env = push_rel_context intern_bl env in
- let proj = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.proj1 in
+ let sigma, proj = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.proj1 in
let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
let projection = (* in wfarg :: arg :: before *)
mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
@@ -1001,82 +1001,90 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let intern_arity = substl [projection] top_arity_let in
(* substitute the projection of wfarg for something,
now intern_arity is in wfarg :: arg *)
- let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
+ let sigma, wfa = wfarg sigma 1 in
+ let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfa] in
let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
- let curry_fun =
+ let sigma, curry_fun =
let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
- let intro = Evarutil.e_new_global evdref (delayed_force build_sigma).Coqlib.intro in
+ let sigma, intro = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.intro in
let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
let rcurry = mkApp (rel, [| measure; lift len measure |]) in
let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in
let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
- LocalDef (Name recname, body, ty)
+ sigma, LocalDef (Name recname, body, ty)
in
let fun_bl = intern_fun_binder :: [arg] in
let lift_lets = lift_rel_context 1 letbinders in
- let intern_body =
+ let sigma, intern_body =
let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
let (r, l, impls, scopes) =
Constrintern.compute_internalization_data env
Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls
in
let newimpls = Id.Map.singleton recname
- (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
- scopes @ [None]) in
- interp_casted_constr_evars (push_rel_context ctx env) evdref
- ~impls:newimpls body (lift 1 top_arity)
+ (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
+ scopes @ [None]) in
+ interp_casted_constr_evars (push_rel_context ctx env) sigma
+ ~impls:newimpls body (lift 1 top_arity)
in
let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
let prop = mkLambda (Name argname, argtyp, top_arity_let) in
- let def =
- mkApp (Evarutil.e_new_global evdref (delayed_force fix_sub_ref),
- [| argtyp ; wf_rel ;
- Evarutil.e_new_evar env evdref
- ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
- prop |])
+ (* XXX: Previous code did parallel evdref update, so possible old
+ weak ordering semantics may bite here. *)
+ let sigma, def =
+ let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in
+ let sigma, h_e_term = Evarutil.new_evar env sigma
+ ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in
+ sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |])
in
- let def = Typing.e_solve_evars env evdref def in
- let _ = evdref := Evarutil.nf_evar_map !evdref in
+ let _evd = ref sigma in
+ let def = Typing.e_solve_evars env _evd def in
+ let sigma = !_evd in
+ let sigma = Evarutil.nf_evar_map sigma in
let def = mkApp (def, [|intern_body_lam|]) in
- let binders_rel = nf_evar_context !evdref binders_rel in
- let binders = nf_evar_context !evdref binders in
- let top_arity = Evarutil.nf_evar !evdref top_arity in
+ let binders_rel = nf_evar_context sigma binders_rel in
+ let binders = nf_evar_context sigma binders in
+ let top_arity = Evarutil.nf_evar sigma top_arity in
let hook, recname, typ =
if List.length binders_rel > 1 then
let name = add_suffix recname "_func" in
- let hook l gr _ =
- let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
+ (* XXX: Mutating the evar_map in the hook! *)
+ (* XXX: Likely the sigma is out of date when the hook is called .... *)
+ let hook sigma l gr _ =
+ let sigma, h_body = Evarutil.new_global sigma gr in
+ let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ty = EConstr.Unsafe.to_constr ty in
- let univs = Evd.check_univ_decl ~poly !evdref decl in
+ let univs = Evd.check_univ_decl ~poly sigma decl in
(*FIXME poly? *)
- let ce = definition_entry ~types:ty ~univs (EConstr.to_constr !evdref body) in
+ let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
- let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in
+ let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in
let typ = it_mkProd_or_LetIn top_arity binders in
- hook, name, typ
- else
+ hook, name, typ
+ else
let typ = it_mkProd_or_LetIn top_arity binders_rel in
- let hook l gr _ =
+ let hook sigma l gr _ =
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in hook, recname, typ
in
- let hook = Lemmas.mk_hook hook in
- let fullcoqc = EConstr.to_constr !evdref def in
- let fullctyp = EConstr.to_constr !evdref typ in
- Obligations.check_evars env !evdref;
- let evars, _, evars_def, evars_typ =
- Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp
+ (* XXX: Capturing sigma here... bad bad *)
+ let hook = Lemmas.mk_hook (hook sigma) in
+ let fullcoqc = EConstr.to_constr sigma def in
+ let fullctyp = EConstr.to_constr sigma typ in
+ Obligations.check_evars env sigma;
+ let evars, _, evars_def, evars_typ =
+ Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
in
- let ctx = Evd.evar_universe_context !evdref in
+ let ctx = Evd.evar_universe_context sigma in
ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
evars_typ ctx evars ~hook)
@@ -1097,31 +1105,36 @@ let interp_recursive isfix fixl notations =
if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then
user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
Some us) fixl None in
- let evd, decl = Univdecls.interp_univ_decl_opt env all_universes in
- let evdref = ref evd in
- let fixctxs, fiximppairs, fixannots =
- List.split3 (List.map (interp_fix_context env evdref isfix) fixl) in
+ let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in
+ let sigma, (fixctxs, fiximppairs, fixannots) =
+ on_snd List.split3 @@
+ List.fold_left_map (fun sigma -> interp_fix_context env sigma isfix) sigma fixl in
let fixctximpenvs, fixctximps = List.split fiximppairs in
- let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in
+ let sigma, (fixccls,fixcclimps) =
+ on_snd List.split @@
+ List.fold_left3_map interp_fix_ccl sigma fixctximpenvs fixctxs fixl in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
- let fixtypes = List.map (fun c -> nf_evar !evdref c) fixtypes in
+ let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
let fiximps = List.map3
(fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
fixctximps fixcclimps fixctxs in
- let rec_sign =
+ let sigma, rec_sign =
List.fold_left2
- (fun env' id t ->
- if Flags.is_program_mode () then
- let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in
- let fixprot =
- try
- let app = mkApp (fix_proto evdref, [|sort; t|]) in
- Typing.e_solve_evars env evdref app
- with e when CErrors.noncritical e -> t
- in
- LocalAssum (id,fixprot) :: env'
- else LocalAssum (id,t) :: env')
- [] fixnames fixtypes
+ (fun (sigma, env') id t ->
+ if Flags.is_program_mode () then
+ let sigma, sort = Typing.type_of ~refresh:true env sigma t in
+ let sigma, fixprot =
+ try
+ let sigma, h_term = fix_proto sigma in
+ let app = mkApp (h_term, [|sort; t|]) in
+ let _evd = ref sigma in
+ let res = Typing.e_solve_evars env _evd app in
+ !_evd, res
+ with e when CErrors.noncritical e -> sigma, t
+ in
+ sigma, LocalAssum (id,fixprot) :: env'
+ else sigma, LocalAssum (id,t) :: env')
+ (sigma,[]) fixnames fixtypes
in
let env_rec = push_named_context rec_sign env in
@@ -1130,24 +1143,24 @@ let interp_recursive isfix fixl notations =
let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
(* Interp bodies with rollback because temp use of notations/implicit *)
- let fixdefs =
+ let sigma, fixdefs =
Metasyntax.with_syntax_protection (fun () ->
List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations;
- List.map4
- (fun fixctximpenv -> interp_fix_body env_rec evdref (Id.Map.fold Id.Map.add fixctximpenv impls))
- fixctximpenvs fixctxs fixl fixccls)
+ List.fold_left4_map
+ (fun sigma fixctximpenv -> interp_fix_body env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls))
+ sigma fixctximpenvs fixctxs fixl fixccls)
() in
(* Instantiate evars and check all are resolved *)
- let evd = solve_unif_constraints_with_heuristics env_rec !evdref in
- let evd, nf = nf_evars_and_universes evd in
+ let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
+ let sigma, nf = nf_evars_and_universes sigma in
let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in
let fixdefs = List.map (Option.map nf) fixdefs in
let fixtypes = List.map nf fixtypes in
let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
(* Build the fix declaration block *)
- (env,rec_sign,decl,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+ (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
let check_recursive isfix env evd (fixnames,fixdefs,_) =
check_evars_are_solved env evd Evd.empty;
@@ -1170,7 +1183,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
+ List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
@@ -1205,7 +1218,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
- List.map3 (fun id t (ctx,imps,_) -> (id,(t,(List.map RelDecl.get_name ctx,imps))))
+ List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 200c2260e..27a680b9b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -13,12 +13,10 @@ open CErrors
open Util
open Pp
open Names
-open Term
open Constr
open Declarations
open Declareops
open Entries
-open Environ
open Nameops
open Globnames
open Decls
@@ -88,28 +86,28 @@ let adjust_guardness_conditions const = function
(mkFix ((indexes,0),fixdecls), ctx), eff
| _ -> (body, ctx), eff) }
-let find_mutually_recursive_statements thms =
+let find_mutually_recursive_statements sigma thms =
let n = List.length thms in
let inds = List.map (fun (id,(t,impls)) ->
- let (hyps,ccl) = decompose_prod_assum t in
+ let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in
let x = (id,(t,impls)) in
- let whnf_hyp_hds = map_rel_context_in_env
- (fun env c -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c))))
+ let whnf_hyp_hds = EConstr.map_rel_context_in_env
+ (fun env c -> fst (Reductionops.whd_all_stack env sigma c))
(Global.env()) hyps in
let ind_hyps =
List.flatten (List.map_i (fun i decl ->
let t = RelDecl.get_type decl in
- match Constr.kind t with
+ match EConstr.kind sigma t with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
mind.mind_finite <> Decl_kinds.CoFinite ->
[ind,x,i]
| _ ->
- []) 0 (List.rev (List.filter RelDecl.is_local_assum whnf_hyp_hds))) in
+ []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in
let ind_ccl =
- let cclenv = push_rel_context hyps (Global.env()) in
- let whnf_ccl,_ = whd_all_stack cclenv Evd.empty (EConstr.of_constr ccl) in
- match Constr.kind (EConstr.Unsafe.to_constr whnf_ccl) with
+ let cclenv = EConstr.push_rel_context hyps (Global.env()) in
+ let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
+ match EConstr.kind sigma whnf_ccl with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
@@ -163,14 +161,14 @@ let find_mutually_recursive_statements thms =
in
(finite,guard,None), ordered_inds
-let look_for_possibly_mutual_statements = function
+let look_for_possibly_mutual_statements sigma = function
| [id,(t,impls)] ->
(* One non recursively proved theorem *)
None,[id,(t,impls)],None
| _::_ as thms ->
(* More than one statement and/or an explicit decreasing mark: *)
(* we look for a common inductive hyp or a common coinductive conclusion *)
- let recguard,ordered_inds = find_mutually_recursive_statements thms in
+ let recguard,ordered_inds = find_mutually_recursive_statements sigma thms in
let thms = List.map pi2 ordered_inds in
Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
| [] -> anomaly (Pp.str "Empty list of theorems.")
@@ -377,7 +375,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
let rec_tac_initializer finite guard thms snl =
if finite then
- match List.map (fun (id,(t,_)) -> (id,EConstr.of_constr t)) thms with
+ match List.map (fun (id,(t,_)) -> (id,t)) thms with
| (id,_)::l -> Tactics.mutual_cofix id l 0
| _ -> assert false
else
@@ -385,11 +383,11 @@ let rec_tac_initializer finite guard thms snl =
let nl = match snl with
| None -> List.map succ (List.map List.last guard)
| Some nl -> nl
- in match List.map2 (fun (id,(t,_)) n -> (id,n, EConstr.of_constr t)) thms nl with
+ in match List.map2 (fun (id,(t,_)) n -> (id,n, t)) thms nl with
| (id,n,_)::l -> Tactics.mutual_fix id n l 0
| _ -> assert false
-let start_proof_with_initialization kind ctx decl recguard thms snl hook =
+let start_proof_with_initialization kind sigma decl recguard thms snl hook =
let intro_tac (_, (_, (ids, _))) =
Tacticals.New.tclMAP (function
| Name id -> Tactics.intro_mustbe_force id
@@ -424,16 +422,15 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
if List.is_empty other_thms then [] else
(* there are several theorems defined mutually *)
let body,opaq = retrieve_first_recthm ctx ref in
- let subst = Evd.evar_universe_context_subst ctx in
- let norm c = Universes.subst_opt_univs_constr subst c in
- let body = Option.map norm body in
+ let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
+ let body = Option.map EConstr.of_constr body in
let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook (fun exn -> exn) hook strength ref) thms_data in
- start_proof_univs id ~pl:decl kind ctx (EConstr.of_constr t) ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+ start_proof_univs id ~pl:decl kind sigma t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
let start_proof_com ?inference_hook kind thms hook =
let env0 = Global.env () in
@@ -442,22 +439,24 @@ let start_proof_com ?inference_hook kind thms hook =
match decl with
| None -> Evd.from_env env0, Univdecls.default_univ_decl
| Some decl ->
- Univdecls.interp_univ_decl_opt env0 (snd decl) in
- let evdref = ref evd in
- let thms = List.map (fun (sopt,(bl,t)) ->
- let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
- let t', imps' = interp_type_evars_impls ~impls env evdref t in
+ Univdecls.interp_univ_decl_opt env0 (snd decl) in
+ let evd, thms = List.fold_left_map (fun evd (sopt,(bl,t)) ->
+ let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in
+ let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
let flags = all_and_fail_flags in
let flags = { flags with use_hook = inference_hook } in
- evdref := solve_remaining_evars flags env !evdref Evd.empty;
+ let evd = solve_remaining_evars flags env evd Evd.empty in
let ids = List.map RelDecl.get_name ctx in
- (compute_proof_name (pi1 kind) sopt,
- (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
- (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
- thms in
- let recguard,thms,snl = look_for_possibly_mutual_statements thms in
- let evd, nf = Evarutil.nf_evars_and_universes !evdref in
- let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
+ (* XXX: The nf_evar is critical !! *)
+ evd, (compute_proof_name (pi1 kind) sopt,
+ (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
+ (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
+ evd thms in
+ let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in
+ let evd, _nf = Evarutil.nf_evars_and_universes evd in
+ (* XXX: This nf_evar is critical too!! We are normalizing twice if
+ you look at the previous lines... *)
+ let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
let () =
let open Misctypes in
if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
@@ -470,7 +469,6 @@ let start_proof_com ?inference_hook kind thms hook =
in
start_proof_with_initialization kind evd decl recguard thms snl hook
-
(* Saving a proof *)
let keep_admitted_vars = ref true
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a4854b4a6..ca92e856b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Constr
open Decl_kinds
type 'a declaration_hook
@@ -37,11 +36,11 @@ val start_proof_com :
goal_kind -> Vernacexpr.proof_expr list ->
unit declaration_hook -> unit
-val start_proof_with_initialization :
+val start_proof_with_initialization :
goal_kind -> Evd.evar_map -> Univdecls.universe_decl ->
(bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
(Id.t (* name of thm *) *
- (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+ (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
-> int list option -> unit declaration_hook -> unit
val universe_proof_terminator :
diff --git a/vernac/record.ml b/vernac/record.ml
index 1cdc538b5..d97a5149d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -60,23 +60,25 @@ let _ =
optread = (fun () -> !typeclasses_unique);
optwrite = (fun b -> typeclasses_unique := b); }
-let interp_fields_evars env evars impls_env nots l =
+let interp_fields_evars env sigma impls_env nots l =
List.fold_left2
- (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
- let t', impl = interp_type_evars_impls env evars ~impls t in
- let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in
+ (fun (env, sigma, uimpls, params, impls) no ((loc, i), b, t) ->
+ let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in
+ let sigma, b' =
+ Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
+ interp_casted_constr_evars_impls env sigma ~impls x t') (sigma,None) b in
let impls =
match i with
| Anonymous -> impls
- | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr !evars t') impl) impls
+ | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr sigma t') impl) impls
in
let d = match b' with
| None -> LocalAssum (i,t')
| Some b' -> LocalDef (i,b',t')
in
List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
- (EConstr.push_rel d env, impl :: uimpls, d::params, impls))
- (env, [], [], impls_env) nots l
+ (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
+ (env, sigma, [], [], impls_env) nots l
let compute_constructor_level evars env l =
List.fold_right (fun d (env, univ) ->
@@ -97,10 +99,9 @@ let binders_of_decls = List.map binder_of_decl
let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let env0 = Global.env () in
- let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
- let evars = ref evd in
- let _ =
- let error bk (loc, name) =
+ let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+ let _ =
+ let error bk (loc, name) =
match bk, name with
| Default _, Anonymous ->
user_err ?loc ~hdr:"record" (str "Record parameters must be named")
@@ -112,63 +113,65 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
| CLocalPattern (loc,(_,_)) ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
in
- let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
- let typ, sort, template = match t with
+ let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in
+ let sigma, typ, sort, template = match t with
| Some t ->
let env = EConstr.push_rel_context newps env0 in
let poly =
match t with
| { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in
- let s = interp_type_evars env evars ~impls:empty_internalization_env t in
- let sred = Reductionops.whd_all env !evars s in
- (match EConstr.kind !evars sred with
+ let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in
+ let sred = Reductionops.whd_all env sigma s in
+ (match EConstr.kind sigma sred with
| Sort s' ->
- let s' = EConstr.ESorts.kind !evars s' in
+ let s' = EConstr.ESorts.kind sigma s' in
(if poly then
- match Evd.is_sort_variable !evars s' with
- | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l;
- s, s', true
- | None -> s, s', false
- else s, s', false)
+ match Evd.is_sort_variable sigma s' with
+ | Some l ->
+ let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
+ sigma, s, s', true
+ | None ->
+ sigma, s, s', false
+ else sigma, s, s', false)
| _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
| None ->
let uvarkind = Evd.univ_flexible_alg in
- let s = Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars in
- EConstr.mkSort s, s, true
+ let sigma, s = Evd.new_sort_variable uvarkind sigma in
+ sigma, EConstr.mkSort s, s, true
in
let arity = EConstr.it_mkProd_or_LetIn typ newps in
let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
let assums = List.filter is_local_assum newps in
let params = List.map (RelDecl.get_name %> Name.get_id) assums in
let ty = Inductive (params,(finite != BiFinite)) in
- let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in
- let env2,impls,newfs,data =
- interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
+ let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in
+ let env2,sigma,impls,newfs,data =
+ interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
in
- let evars =
- Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in
- let typ, evars =
- let _, univ = compute_constructor_level evars env_ar newfs in
+ let sigma =
+ Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma Evd.empty in
+ let sigma, typ =
+ let _, univ = compute_constructor_level sigma env_ar newfs in
if not def && (Sorts.is_prop sort ||
(Sorts.is_set sort && is_impredicative_set env0)) then
- typ, evars
+ sigma, typ
else
- let evars = Evd.set_leq_sort env_ar evars (Type univ) sort in
+ let sigma = Evd.set_leq_sort env_ar sigma (Type univ) sort in
if Univ.is_small_univ univ &&
- Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars sort) then
+ Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
(* We can assume that the level in aritysort is not constrained
and clear it, if it is flexible *)
- EConstr.mkSort (Sorts.sort_of_univ univ),
- Evd.set_eq_sort env_ar evars (Prop Pos) sort
- else typ, evars
+ Evd.set_eq_sort env_ar sigma (Prop Pos) sort,
+ EConstr.mkSort (Sorts.sort_of_univ univ)
+ else sigma, typ
in
- let evars, nf = Evarutil.nf_evars_and_universes evars in
- let newfs = List.map (EConstr.to_rel_decl evars) newfs in
- let newps = List.map (EConstr.to_rel_decl evars) newps in
- let typ = EConstr.to_constr evars typ in
- let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
- let univs = Evd.check_univ_decl ~poly evars decl in
- let ubinders = Evd.universe_binders evars in
+ let sigma, _ = Evarutil.nf_evars_and_universes sigma in
+ let newfs = List.map (EConstr.to_rel_decl sigma) newfs in
+ let newps = List.map (EConstr.to_rel_decl sigma) newps in
+ let typ = EConstr.to_constr sigma typ in
+ let ce t = Pretyping.check_evars env0 Evd.empty sigma (EConstr.of_constr t) in
+ let univs = Evd.check_univ_decl ~poly sigma decl in
+ let ubinders = Evd.universe_binders sigma in
List.iter (iter_constr ce) (List.rev newps);
List.iter (iter_constr ce) (List.rev newfs);
ubinders, univs, typ, template, imps, newps, impls, newfs