aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorfilliatr1999-10-18 13:51:32 +0000
committerfilliatr1999-10-18 13:51:32 +0000
commit154f0fc69c79383cc75795554eb7e0256c8299d8 (patch)
treed39ed1dbe4d0c555a8373592162eee3043583a1a /kernel
parent22e4ceb13d18c8b941f6a27cc83f547dd90104b8 (diff)
- déplacement (encore une fois !) des variables existentielles : elles sont
toujours dans le noyau (en ce sens que Reduction et Typeops les connaissent) mais dans un argument supplémentaire A COTE de l'environnement (de type unsafe_env) - Indtypes et Typing n'utilisent strictement que Evd.empty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r--kernel/closure.ml17
-rw-r--r--kernel/closure.mli5
-rw-r--r--kernel/environ.ml4
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/evd.ml15
-rw-r--r--kernel/evd.mli32
-rw-r--r--kernel/indtypes.ml21
-rw-r--r--kernel/instantiate.ml10
-rw-r--r--kernel/instantiate.mli5
-rw-r--r--kernel/reduction.ml319
-rw-r--r--kernel/reduction.mli169
-rw-r--r--kernel/typeops.ml221
-rw-r--r--kernel/typeops.mli35
-rw-r--r--kernel/typing.ml57
14 files changed, 479 insertions, 433 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index a7ee12c3e4..f6c27a8be6 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -10,7 +10,7 @@ open Inductive
open Environ
open Instantiate
open Univ
-
+open Evd
let stats = ref false
let share = ref true
@@ -136,6 +136,7 @@ type ('a, 'b) infos = {
i_flags : flags;
i_repr : ('a, 'b) infos -> constr -> 'a;
i_env : unsafe_env;
+ i_evc : 'b evar_map;
i_tab : (constr, 'a) Hashtbl.t }
let const_value_cache info c =
@@ -149,8 +150,12 @@ let const_value_cache info c =
Some v
| None -> None
-let infos_under { i_flags = flg; i_repr = rfun; i_env = env; i_tab = tab } =
- { i_flags = flags_under flg; i_repr = rfun; i_env = env; i_tab = tab }
+let infos_under infos =
+ { i_flags = flags_under infos.i_flags;
+ i_repr = infos.i_repr;
+ i_env = infos.i_env;
+ i_evc = infos.i_evc;
+ i_tab = infos.i_tab }
(**** Call by value reduction ****)
@@ -464,10 +469,11 @@ and cbv_norm_value info = function (* reduction under binders *)
type 'a cbv_infos = (cbv_value, 'a) infos
(* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env =
+let create_cbv_infos flgs env sigma =
{ i_flags = flgs;
i_repr = (fun old_info c -> cbv_stack_term old_info TOP ESID c);
i_env = env;
+ i_evc = sigma;
i_tab = Hashtbl.create 17 }
@@ -847,10 +853,11 @@ let search_frozen_cst info op vars =
(* cache of constants: the body is computed only when needed. *)
type 'a clos_infos = (fconstr, 'a) infos
-let create_clos_infos flgs env =
+let create_clos_infos flgs env sigma =
{ i_flags = flgs;
i_repr = (fun old_info c -> inject c);
i_env = env;
+ i_evc = sigma;
i_tab = Hashtbl.create 17 }
let clos_infos_env infos = infos.i_env
diff --git a/kernel/closure.mli b/kernel/closure.mli
index ea7defa201..b928851ecb 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,6 +6,7 @@ open Pp
open Names
open Generic
open Term
+open Evd
open Environ
(*i*)
@@ -82,7 +83,7 @@ val fixp_reducible :
(* normalization of a constr: the two functions to know... *)
type 'a cbv_infos
-val create_cbv_infos : flags -> unsafe_env -> 'a cbv_infos
+val create_cbv_infos : flags -> unsafe_env -> 'a evar_map -> 'a cbv_infos
val cbv_norm : 'a cbv_infos -> constr -> constr
(* recursive functions... *)
@@ -158,7 +159,7 @@ type case_status =
(* Constant cache *)
type 'a clos_infos
-val create_clos_infos : flags -> unsafe_env -> 'a clos_infos
+val create_clos_infos : flags -> unsafe_env -> 'a evar_map -> 'a clos_infos
val clos_infos_env : 'a clos_infos -> unsafe_env
(* Reduction function *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e431c1b374..004ef8e536 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -9,7 +9,6 @@ open Sign
open Univ
open Generic
open Term
-open Evd
open Constant
open Inductive
open Abstraction
@@ -30,7 +29,6 @@ type globals = {
type unsafe_env = {
env_context : context;
env_globals : globals;
- env_evar_map : evar_map;
env_universes : universes }
let empty_env = {
@@ -41,12 +39,10 @@ let empty_env = {
env_abstractions = Spmap.empty;
env_locals = [];
env_imports = [] };
- env_evar_map = mt_evd;
env_universes = initial_universes }
let universes env = env.env_universes
let context env = env.env_context
-let evar_map env = env.env_evar_map
let metamap env = failwith "Environ.metamap: TODO: unifier metas et VE"
(* Construction functions. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 684758d1e2..61fb4b64a6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -23,8 +23,6 @@ val empty_env : unsafe_env
val universes : unsafe_env -> universes
val context : unsafe_env -> context
-val evar_map : unsafe_env -> evar_map
-val metamap : unsafe_env -> (int * constr) list
val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
val push_rel : name * typed_type -> unsafe_env -> unsafe_env
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 9295d35872..270ad1f2e4 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -18,14 +18,15 @@ type evar_body =
| Evar_empty
| Evar_defined of constr
-type evar_info = {
+type 'a evar_info = {
evar_concl : constr;
evar_hyps : typed_type signature;
- evar_body : evar_body }
+ evar_body : evar_body;
+ evar_info : 'a }
-type evar_map = evar_info Intmap.t
+type 'a evar_map = 'a evar_info Intmap.t
-let mt_evd = Intmap.empty
+let empty = Intmap.empty
let to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc []
let dom evc = Intmap.fold (fun ev _ acc -> ev::acc) evc []
@@ -41,7 +42,8 @@ let define evd ev body =
let newinfo =
{ evar_concl = oldinfo.evar_concl;
evar_hyps = oldinfo.evar_hyps;
- evar_body = Evar_defined body }
+ evar_body = Evar_defined body;
+ evar_info = oldinfo.evar_info }
in
match oldinfo.evar_body with
| Evar_empty -> Intmap.add ev newinfo evd
@@ -61,3 +63,6 @@ let is_evar sigma ev = in_dom sigma ev
let is_defined sigma ev =
let info = map sigma ev in
not (info.evar_body = Evar_empty)
+
+let metamap sigma = failwith "metamap : NOT YET IMPLEMENTED"
+
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 89cefcab11..80e767fa85 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -21,28 +21,30 @@ type evar_body =
| Evar_empty
| Evar_defined of constr
-type evar_info = {
+type 'a evar_info = {
evar_concl : constr;
evar_hyps : typed_type signature;
- evar_body : evar_body }
+ evar_body : evar_body;
+ evar_info : 'a }
-type evar_map
+type 'a evar_map
-val add : evar_map -> evar -> evar_info -> evar_map
+val empty : 'a evar_map
-val dom : evar_map -> evar list
-val map : evar_map -> evar -> evar_info
-val rmv : evar_map -> evar -> evar_map
-val remap : evar_map -> evar -> evar_info -> evar_map
-val in_dom : evar_map -> evar -> bool
-val to_list : evar_map -> (evar * evar_info) list
+val add : 'a evar_map -> evar -> 'a evar_info -> 'a evar_map
-val mt_evd : evar_map
+val dom : 'a evar_map -> evar list
+val map : 'a evar_map -> evar -> 'a evar_info
+val rmv : 'a evar_map -> evar -> 'a evar_map
+val remap : 'a evar_map -> evar -> 'a evar_info -> 'a evar_map
+val in_dom : 'a evar_map -> evar -> bool
+val to_list : 'a evar_map -> (evar * 'a evar_info) list
-val define : evar_map -> evar -> constr -> evar_map
+val define : 'a evar_map -> evar -> constr -> 'a evar_map
-val non_instantiated : evar_map -> (evar * evar_info) list
-val is_evar : evar_map -> evar -> bool
+val non_instantiated : 'a evar_map -> (evar * 'a evar_info) list
+val is_evar : 'a evar_map -> evar -> bool
-val is_defined : evar_map -> evar -> bool
+val is_defined : 'a evar_map -> evar -> bool
+val metamap : 'a evar_map -> (int * constr) list
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b6a7c0a3e4..db5458211d 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -10,15 +10,20 @@ open Environ
open Instantiate
open Reduction
+(* In the following, each time an [evar_map] is required, then [Evd.empty]
+ is given, since inductive types are typed in an environment without
+ existentials. *)
+
let mind_check_arities env mie =
let check_arity id c =
- if not (is_arity env c) then raise (InductiveError (NotAnArity id))
+ if not (is_arity env Evd.empty c) then
+ raise (InductiveError (NotAnArity id))
in
List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
let sort_of_arity env c =
let rec sort_of ar =
- match whd_betadeltaiota env ar with
+ match whd_betadeltaiota env Evd.empty ar with
| DOP0 (Sort s) -> s
| DOP2 (Prod, _, DLAM (_, c)) -> sort_of c
| _ -> error "not an arity"
@@ -47,7 +52,7 @@ let check_correct_par env nparams ntypes n l largs =
if Array.length largs < nparams then raise (InductiveError (NotEnoughArgs l));
let (lpar,largs') = array_chop nparams largs in
for k = 0 to nparams - 1 do
- if not ((Rel (n-k-1))= whd_betadeltaiotaeta env lpar.(k)) then
+ if not ((Rel (n-k-1))= whd_betadeltaiotaeta env Evd.empty lpar.(k)) then
raise (InductiveError (NonPar (k+1,l)))
done;
if not (array_for_all (noccur_bet n ntypes) largs') then
@@ -62,14 +67,14 @@ let abstract_mind_lc env ntyps npars lc =
list_tabulate
(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
in
- Array.map (compose (nf_beta env) (substl make_abs)) lC
+ Array.map (compose (nf_beta env Evd.empty) (substl make_abs)) lC
let decomp_par n c = snd (decompose_prod_n n c)
let listrec_mconstr env ntypes nparams i indlc =
(* check the inductive types occur positively in C *)
let rec check_pos n c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env Evd.empty c with
| DOP2(Prod,b,DLAM(na,d)) ->
if not (noccur_bet n ntypes b) then raise (InductiveError (NonPos n));
check_pos (n+1) d
@@ -117,7 +122,7 @@ let listrec_mconstr env ntypes nparams i indlc =
(* when substituted *)
Array.map
(function c ->
- let c' = hnf_prod_appvect env "is_imbr_pos" c
+ let c' = hnf_prod_appvect env Evd.empty "is_imbr_pos" c
(Array.map (lift auxntyp) lpar) in
check_construct false newidx c')
auxlcvect
@@ -139,7 +144,7 @@ let listrec_mconstr env ntypes nparams i indlc =
not sure if they make sense in a form of constructor. This is why I
chose to duplicated the code. Eduardo 13/7/99. *)
and check_param_pos n c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env Evd.empty c with
(* The extra case *)
| DOP2(Lambda,b,DLAM(na,d)) ->
if noccur_bet n ntypes b
@@ -179,7 +184,7 @@ let listrec_mconstr env ntypes nparams i indlc =
and check_construct check =
let rec check_constr_rec lrec n c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env Evd.empty c with
| DOP2(Prod,b,DLAM(na,d)) ->
let recarg = (check_pos n b) in
check_constr_rec (recarg::lrec) (n+1) d
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 09265c988f..acc48bcb05 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -68,18 +68,18 @@ let mis_lc env mis =
let name_of_existential n = id_of_string ("?" ^ string_of_int n)
-let existential_type env c =
+let existential_type sigma c =
let (n,args) = destEvar c in
- let info = Evd.map (evar_map env) n in
+ let info = Evd.map sigma n in
let hyps = info.evar_hyps in
instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
-let existential_value env c =
+let existential_value sigma c =
let (n,args) = destEvar c in
- let info = Evd.map (evar_map env) n in
+ let info = Evd.map sigma n in
let hyps = info.evar_hyps in
match info.evar_body with
- | Evar_defined c ->
+ | Evar_defined c ->
instantiate_constr (ids_of_sign hyps) c (Array.to_list args)
| Evar_empty ->
anomaly "a defined existential with no body"
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 8ea57f0887..27bd8191ec 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -5,6 +5,7 @@
open Names
open Term
open Inductive
+open Evd
open Environ
(*i*)
@@ -18,8 +19,8 @@ val instantiate_type :
val constant_value : unsafe_env -> constr -> constr
val constant_type : unsafe_env -> constr -> typed_type
-val existential_value : unsafe_env -> constr -> constr
-val existential_type : unsafe_env -> constr -> constr
+val existential_value : 'a evar_map -> constr -> constr
+val existential_type : 'a evar_map -> constr -> constr
val const_abst_opt_value : unsafe_env -> constr -> constr option
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index e3b2d9f09f..ac32e2eabd 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -7,6 +7,7 @@ open Names
open Generic
open Term
open Univ
+open Evd
open Constant
open Inductive
open Environ
@@ -17,29 +18,30 @@ exception Redelimination
exception Induc
exception Elimconst
-type reduction_function = unsafe_env -> constr -> constr
-type stack_reduction_function =
- unsafe_env -> constr -> constr list -> constr * constr list
+type 'a reduction_function = unsafe_env -> 'a evar_map -> constr -> constr
+
+type 'a stack_reduction_function =
+ unsafe_env -> 'a evar_map -> constr -> constr list -> constr * constr list
(*************************************)
(*** Reduction Functions Operators ***)
(*************************************)
-let rec under_casts f env = function
- | DOP2(Cast,c,t) -> DOP2(Cast,under_casts f env c, t)
- | c -> f env c
+let rec under_casts f env sigma = function
+ | DOP2(Cast,c,t) -> DOP2(Cast,under_casts f env sigma c, t)
+ | c -> f env sigma c
-let rec whd_stack env x stack =
+let rec whd_stack env sigma x stack =
match x with
- | DOPN(AppL,cl) -> whd_stack env cl.(0) (array_app_tl cl stack)
- | DOP2(Cast,c,_) -> whd_stack env c stack
+ | DOPN(AppL,cl) -> whd_stack env sigma cl.(0) (array_app_tl cl stack)
+ | DOP2(Cast,c,_) -> whd_stack env sigma c stack
| _ -> (x,stack)
-let stack_reduction_of_reduction red_fun env x stack =
- let t = red_fun env (applistc x stack) in
- whd_stack env t []
+let stack_reduction_of_reduction red_fun env sigma x stack =
+ let t = red_fun env sigma (applistc x stack) in
+ whd_stack env sigma t []
-let strong whdfun env =
+let strong whdfun env sigma =
let rec strongrec = function
| DOP0 _ as t -> t
(* Cas ad hoc *)
@@ -54,10 +56,10 @@ let strong whdfun env =
in
strongrec
-let rec strong_prodspine redfun env c =
- match redfun env c with
+let rec strong_prodspine redfun env sigma c =
+ match redfun env sigma c with
| DOP2(Prod,a,DLAM(na,b)) ->
- DOP2(Prod,a,DLAM(na,strong_prodspine redfun env b))
+ DOP2(Prod,a,DLAM(na,strong_prodspine redfun env sigma b))
| x -> x
@@ -67,8 +69,8 @@ let rec strong_prodspine redfun env c =
(* call by value reduction functions *)
-let cbv_norm_flags flags env t =
- cbv_norm (create_cbv_infos flags env) t
+let cbv_norm_flags flags env sigma t =
+ cbv_norm (create_cbv_infos flags env sigma) t
let cbv_beta env = cbv_norm_flags beta env
let cbv_betaiota env = cbv_norm_flags betaiota env
@@ -78,8 +80,8 @@ let compute = cbv_betadeltaiota
(* lazy reduction functions. The infos must be created for each term *)
-let clos_norm_flags flgs env t =
- norm_val (create_clos_infos flgs env) (inject t)
+let clos_norm_flags flgs env sigma t =
+ norm_val (create_clos_infos flgs env sigma) (inject t)
let nf_beta env = clos_norm_flags beta env
let nf_betaiota env = clos_norm_flags betaiota env
@@ -88,12 +90,12 @@ let nf_betadeltaiota env = clos_norm_flags betadeltaiota env
(* lazy weak head reduction functions *)
(* Pb: whd_val parcourt tout le terme, meme si aucune reduction n'a lieu *)
-let whd_flags flgs env t =
- whd_val (create_clos_infos flgs env) (inject t)
+let whd_flags flgs env sigma t =
+ whd_val (create_clos_infos flgs env sigma) (inject t)
(* Red reduction tactic: reduction to a product *)
-let red_product env c =
+let red_product env sigma c =
let rec redrec x =
match x with
| DOPN(AppL,cl) ->
@@ -104,7 +106,7 @@ let red_product env c =
| DOP2(Prod,a,DLAM(x,b)) -> DOP2(Prod, a, DLAM(x, redrec b))
| _ -> error "Term not reducible"
in
- nf_betaiota env (redrec c)
+ nf_betaiota env sigma (redrec c)
(* Substitute only a list of locations locs, the empty list is interpreted
@@ -266,39 +268,39 @@ let rec substlin env name n ol c =
| _ -> (n,ol,c)
-let unfold env name =
+let unfold env sigma name =
let flag =
(UNIFORM,{ r_beta = true;
r_delta = (fun op -> op=(Const name) or op=(Abst name));
r_iota = true })
in
- clos_norm_flags flag env
+ clos_norm_flags flag env sigma
(* unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)
* Unfolds the constant name in a term c following a list of occurrences occl.
* at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
* Performs a betaiota reduction after unfolding. *)
-let unfoldoccs env (occl,name) c =
+let unfoldoccs env sigma (occl,name) c =
match occl with
- | [] -> unfold env name c
+ | [] -> unfold env sigma name c
| l ->
match substlin env name 1 (Sort.list (<) l) c with
- | (_,[],uc) -> nf_betaiota env uc
+ | (_,[],uc) -> nf_betaiota env sigma uc
| (1,_,_) -> error ((string_of_path name)^" does not occur")
| _ -> error ("bad occurrence numbers of "^(string_of_path name))
(* Unfold reduction tactic: *)
-let unfoldn loccname env c =
- List.fold_left (fun c occname -> unfoldoccs env occname c) c loccname
+let unfoldn loccname env sigma c =
+ List.fold_left (fun c occname -> unfoldoccs env sigma occname c) c loccname
(* Re-folding constants tactics: refold com in term c *)
-let fold_one_com com env c =
- let rcom = red_product env com in
+let fold_one_com com env sigma c =
+ let rcom = red_product env sigma com in
subst1 com (subst_term rcom c)
-let fold_commands cl env c =
- List.fold_right (fun com -> fold_one_com com env) (List.rev cl) c
+let fold_commands cl env sigma c =
+ List.fold_right (fun com -> fold_one_com com env sigma) (List.rev cl) c
(* Pattern *)
@@ -316,7 +318,7 @@ let abstract_scheme env (locc,a,ta) t =
DOP2(Lambda, ta, DLAM(na,subst_term_occ locc a t))
-let pattern_occs loccs_trm_typ env c =
+let pattern_occs loccs_trm_typ env sigma c =
let abstr_trm = List.fold_right (abstract_scheme env) loccs_trm_typ c in
applist(abstr_trm, List.map (fun (_,t,_) -> t) loccs_trm_typ)
@@ -337,7 +339,7 @@ let rec stacklam recfun env t stack =
let beta_applist (c,l) = stacklam (fun c l -> applist(c,l)) [] c l
-let whd_beta_stack env =
+let whd_beta_stack env sigma =
let rec whrec x stack = match x with
| DOP2(Lambda,c1,DLAM(name,c2)) ->
(match stack with
@@ -350,12 +352,12 @@ let whd_beta_stack env =
in
whrec
-let whd_beta env x = applist (whd_beta_stack env x [])
+let whd_beta env sigma x = applist (whd_beta_stack env sigma x [])
(* 2. Delta Reduction *)
-let whd_const_stack namelist env =
+let whd_const_stack namelist env sigma =
let rec whrec x l =
match x with
| DOPN(Const sp,_) as c ->
@@ -382,9 +384,10 @@ let whd_const_stack namelist env =
in
whrec
-let whd_const namelist env c = applist(whd_const_stack namelist env c [])
+let whd_const namelist env sigma c =
+ applist(whd_const_stack namelist env sigma c [])
-let whd_delta_stack env =
+let whd_delta_stack env sigma =
let rec whrec x l =
match x with
| DOPN(Const _,_) as c ->
@@ -403,10 +406,10 @@ let whd_delta_stack env =
in
whrec
-let whd_delta env c = applist(whd_delta_stack env c [])
+let whd_delta env sigma c = applist(whd_delta_stack env sigma c [])
-let whd_betadelta_stack env =
+let whd_betadelta_stack env sigma =
let rec whrec x l =
match x with
| DOPN(Const _,_) ->
@@ -429,10 +432,10 @@ let whd_betadelta_stack env =
in
whrec
-let whd_betadelta env c = applist(whd_betadelta_stack env c [])
+let whd_betadelta env sigma c = applist(whd_betadelta_stack env sigma c [])
-let whd_betadeltat_stack env =
+let whd_betadeltat_stack env sigma =
let rec whrec x l =
match x with
| DOPN(Const _,_) ->
@@ -455,9 +458,9 @@ let whd_betadeltat_stack env =
in
whrec
-let whd_betadeltat env c = applist(whd_betadeltat_stack env c [])
+let whd_betadeltat env sigma c = applist(whd_betadeltat_stack env sigma c [])
-let whd_betadeltaeta_stack env =
+let whd_betadeltaeta_stack env sigma =
let rec whrec x stack =
match x with
| DOPN(Const _,_) ->
@@ -493,7 +496,8 @@ let whd_betadeltaeta_stack env =
in
whrec
-let whd_betadeltaeta env x = applist(whd_betadeltaeta_stack env x [])
+let whd_betadeltaeta env sigma x =
+ applist(whd_betadeltaeta_stack env sigma x [])
(* 3. Iota reduction *)
@@ -572,7 +576,7 @@ let reduce_fix whfun fix stack =
--------------------
qui coute cher dans whd_betadeltaiota *)
-let whd_betaiota_stack env =
+let whd_betaiota_stack env sigma =
let rec whrec x stack =
match x with
| DOP2(Cast,c,_) -> whrec c stack
@@ -597,10 +601,10 @@ let whd_betaiota_stack env =
in
whrec
-let whd_betaiota env x = applist (whd_betaiota_stack env x [])
+let whd_betaiota env sigma x = applist (whd_betaiota_stack env sigma x [])
-let whd_betadeltatiota_stack env =
+let whd_betadeltatiota_stack env sigma =
let rec whrec x stack =
match x with
| DOPN(Const _,_) ->
@@ -634,9 +638,10 @@ let whd_betadeltatiota_stack env =
in
whrec
-let whd_betadeltatiota env x = applist(whd_betadeltatiota_stack env x [])
+let whd_betadeltatiota env sigma x =
+ applist(whd_betadeltatiota_stack env sigma x [])
-let whd_betadeltaiota_stack env =
+let whd_betadeltaiota_stack env sigma =
let rec bdi_rec x stack =
match x with
| DOPN(Const _,_) ->
@@ -670,10 +675,11 @@ let whd_betadeltaiota_stack env =
in
bdi_rec
-let whd_betadeltaiota env x = applist(whd_betadeltaiota_stack env x [])
+let whd_betadeltaiota env sigma x =
+ applist(whd_betadeltaiota_stack env sigma x [])
-let whd_betadeltaiotaeta_stack env =
+let whd_betadeltaiotaeta_stack env sigma =
let rec whrec x stack =
match x with
| DOPN(Const _,_) ->
@@ -723,7 +729,8 @@ let whd_betadeltaiotaeta_stack env =
in
whrec
-let whd_betadeltaiotaeta env x = applist(whd_betadeltaiotaeta_stack env x [])
+let whd_betadeltaiotaeta env sigma x =
+ applist(whd_betadeltaiotaeta_stack env sigma x [])
(********************************************************************)
(* Conversion *)
@@ -739,7 +746,8 @@ let pb_equal = function
| CONV_LEQ -> CONV
| CONV -> CONV
-type conversion_function = unsafe_env -> constr -> constr -> constraints
+type 'a conversion_function =
+ unsafe_env -> 'a evar_map -> constr -> constr -> constraints
(* Conversion utility functions *)
@@ -905,43 +913,43 @@ and eqappr cv_pb infos appr1 appr2 =
| _ -> (fun _ -> raise NotConvertible)
-let fconv cv_pb env t1 t2 =
- let t1 = strong (fun _ -> strip_outer_cast) env t1
- and t2 = strong (fun _ -> strip_outer_cast) env t2 in
+let fconv cv_pb env sigma t1 t2 =
+ let t1 = strong (fun _ -> strip_outer_cast) env sigma t1
+ and t2 = strong (fun _ -> strip_outer_cast) env sigma t2 in
if eq_constr t1 t2 then
Constraint.empty
else
- let infos = create_clos_infos hnf_flags env in
+ let infos = create_clos_infos hnf_flags env sigma in
ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
let conv env = fconv CONV env
let conv_leq env = fconv CONV_LEQ env
-let conv_forall2 f env v1 v2 =
+let conv_forall2 f env sigma v1 v2 =
array_fold_left2
- (fun c x y -> let c' = f env x y in Constraint.union c c')
+ (fun c x y -> let c' = f env sigma x y in Constraint.union c c')
Constraint.empty
v1 v2
-let conv_forall2_i f env v1 v2 =
+let conv_forall2_i f env sigma v1 v2 =
array_fold_left2_i
- (fun i c x y -> let c' = f i env x y in Constraint.union c c')
+ (fun i c x y -> let c' = f i env sigma x y in Constraint.union c c')
Constraint.empty
v1 v2
-let test_conversion f env x y =
- try let _ = f env x y in true with NotConvertible -> false
+let test_conversion f env sigma x y =
+ try let _ = f env sigma x y in true with NotConvertible -> false
-let is_conv env = test_conversion conv env
-let is_conv_leq env = test_conversion conv_leq env
+let is_conv env sigma = test_conversion conv env sigma
+let is_conv_leq env sigma = test_conversion conv_leq env sigma
(********************************************************************)
(* Special-Purpose Reduction *)
(********************************************************************)
-let whd_meta env = function
- | DOP0(Meta p) as u -> (try List.assoc p (metamap env) with Not_found -> u)
+let whd_meta env sigma = function
+ | DOP0(Meta p) as u -> (try List.assoc p (metamap sigma) with Not_found -> u)
| x -> x
(* Try to replace all metas. Does not replace metas in the metas' values
@@ -960,8 +968,8 @@ let plain_instance s c =
if s = [] then c else irec c
(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
-let instance s env c =
- if s = [] then c else nf_betaiota env (plain_instance s c)
+let instance s env sigma c =
+ if s = [] then c else nf_betaiota env sigma (plain_instance s c)
(* pseudo-reduction rule:
@@ -970,46 +978,52 @@ let instance s env c =
* if this does not work, then we use the string S as part of our
* error message. *)
-let hnf_prod_app env s t n =
- match whd_betadeltaiota env t with
+let hnf_prod_app env sigma s t n =
+ match whd_betadeltaiota env sigma t with
| DOP2(Prod,_,b) -> sAPP b n
| _ ->
errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
'sTR s ; 'fNL >]
-let hnf_prod_appvect env s t nL = Array.fold_left (hnf_prod_app env s) t nL
-let hnf_prod_applist env s t nL = List.fold_left (hnf_prod_app env s) t nL
+let hnf_prod_appvect env sigma s t nl =
+ Array.fold_left (hnf_prod_app env sigma s) t nl
+
+let hnf_prod_applist env sigma s t nl =
+ List.fold_left (hnf_prod_app env sigma s) t nl
-let hnf_lam_app env s t n =
- match whd_betadeltaiota env t with
+let hnf_lam_app env sigma s t n =
+ match whd_betadeltaiota env sigma t with
| DOP2(Lambda,_,b) -> sAPP b n
| _ ->
errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
'sTR s ; 'fNL >]
-let hnf_lam_appvect env s t nL = Array.fold_left (hnf_lam_app env s) t nL
-let hnf_lam_applist env s t nL = List.fold_left (hnf_lam_app env s) t nL
+let hnf_lam_appvect env sigma s t nl =
+ Array.fold_left (hnf_lam_app env sigma s) t nl
-let splay_prod env =
+let hnf_lam_applist env sigma s t nl =
+ List.fold_left (hnf_lam_app env sigma s) t nl
+
+let splay_prod env sigma =
let rec decrec m c =
- match whd_betadeltaiota env c with
- | DOP2(Prod,a,DLAM(n,c_0)) -> decrec ((n,a)::m) c_0
+ match whd_betadeltaiota env sigma c with
+ | DOP2(Prod,a,DLAM(n,c_0)) -> decrec ((n,a)::m) c_0
| t -> m,t
in
decrec []
-let decomp_prod env =
+let decomp_prod env sigma =
let rec decrec m c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env sigma c with
| DOP0(Sort _) as x -> m,x
- | DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m+1) c_0
- | _ -> error "decomp_prod: Not a product"
+ | DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m+1) c_0
+ | _ -> error "decomp_prod: Not a product"
in
decrec 0
-let decomp_n_prod env n =
+let decomp_n_prod env sigma n =
let rec decrec m ln c = if m = 0 then (ln,c) else
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env sigma c with
| DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m-1) ((n,a)::ln) c_0
| _ -> error "decomp_n_prod: Not enough products"
in
@@ -1102,9 +1116,9 @@ an equivalent of Fix(f|t)[xi<-ai] as
with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1]
*)
-let compute_consteval env c =
+let compute_consteval env sigma c =
let rec srec n labs c =
- match whd_betadeltaeta_stack env c [] with
+ match whd_betadeltaeta_stack env sigma c [] with
| (DOP2(Lambda,t,DLAM(_,g)),[]) -> srec (n+1) (t::labs) g
| (DOPN(Fix((nv,i)),bodies),l) ->
if List.length l > n then
@@ -1134,25 +1148,25 @@ let compute_consteval env c =
(* One step of approximation *)
-let rec apprec env c stack =
- let (t,stack) = whd_betaiota_stack env c stack in
+let rec apprec env sigma c stack =
+ let (t,stack) = whd_betaiota_stack env sigma c stack in
match t with
| DOPN(MutCase _,_) ->
let (ci,p,d,lf) = destCase t in
- let (cr,crargs) = whd_betadeltaiota_stack env d [] in
+ let (cr,crargs) = whd_betadeltaiota_stack env sigma d [] in
let rslt = mkMutCaseA ci p (applist(cr,crargs)) lf in
if reducible_mind_case cr then
- apprec env rslt stack
+ apprec env sigma rslt stack
else
(t,stack)
| DOPN(Fix _,_) ->
let (reduced,(fix,stack)) =
- reduce_fix (whd_betadeltaiota_stack env) t stack
+ reduce_fix (whd_betadeltaiota_stack env sigma) t stack
in
- if reduced then apprec env fix stack else (fix,stack)
+ if reduced then apprec env sigma fix stack else (fix,stack)
| _ -> (t,stack)
-let hnf env c = apprec env c []
+let hnf env sigma c = apprec env sigma c []
(* A reduction function like whd_betaiota but which keeps casts
* and does not reduce redexes containing meta-variables.
@@ -1160,7 +1174,7 @@ let hnf env c = apprec env c []
* Used in Programs.
* Added by JCF, 29/1/98. *)
-let whd_programs_stack env =
+let whd_programs_stack env sigma =
let rec whrec x stack =
match x with
| DOPN(AppL,cl) ->
@@ -1191,45 +1205,45 @@ let whd_programs_stack env =
in
whrec
-let whd_programs env x = applist (whd_programs_stack env x [])
+let whd_programs env sigma x = applist (whd_programs_stack env sigma x [])
-let find_mrectype env c =
- let (t,l) = whd_betadeltaiota_stack env c [] in
+let find_mrectype env sigma c =
+ let (t,l) = whd_betadeltaiota_stack env sigma c [] in
match t with
| DOPN(MutInd (sp,i),_) -> (t,l)
| _ -> raise Induc
-let find_minductype env c =
- let (t,l) = whd_betadeltaiota_stack env c [] in
+let find_minductype env sigma c =
+ let (t,l) = whd_betadeltaiota_stack env sigma c [] in
match t with
| DOPN(MutInd (sp,i),_)
when mind_type_finite (lookup_mind sp env) i -> (t,l)
| _ -> raise Induc
-let find_mcoinductype env c =
- let (t,l) = whd_betadeltaiota_stack env c [] in
+let find_mcoinductype env sigma c =
+ let (t,l) = whd_betadeltaiota_stack env sigma c [] in
match t with
| DOPN(MutInd (sp,i),_)
when not (mind_type_finite (lookup_mind sp env) i) -> (t,l)
| _ -> raise Induc
-let minductype_spec env c =
+let minductype_spec env sigma c =
try
- let (x,l) = find_minductype env c in
+ let (x,l) = find_minductype env sigma c in
if l<>[] then anomaly "minductype_spec: Not a recursive type 1" else x
with Induc ->
anomaly "minductype_spec: Not a recursive type 2"
-let mrectype_spec env c =
+let mrectype_spec env sigma c =
try
- let (x,l) = find_mrectype env c in
+ let (x,l) = find_mrectype env sigma c in
if l<>[] then anomaly "mrectype_spec: Not a recursive type 1" else x
with Induc ->
anomaly "mrectype_spec: Not a recursive type 2"
-let check_mrectype_spec env c =
+let check_mrectype_spec env sigma c =
try
- let (x,l) = find_mrectype env c in
+ let (x,l) = find_mrectype env sigma c in
if l<>[] then error "check_mrectype: Not a recursive type 1" else x
with Induc ->
error "check_mrectype: Not a recursive type 2"
@@ -1237,9 +1251,9 @@ let check_mrectype_spec env c =
exception IsType
-let is_arity env =
+let is_arity env sigma =
let rec srec c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env sigma c with
| DOP0(Sort _) -> true
| DOP2(Prod,_,DLAM(_,c')) -> srec c'
| DOP2(Lambda,_,DLAM(_,c')) -> srec c'
@@ -1247,9 +1261,9 @@ let is_arity env =
in
srec
-let info_arity env =
+let info_arity env sigma =
let rec srec c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env sigma c with
| DOP0(Sort(Prop Null)) -> false
| DOP0(Sort(Prop Pos)) -> true
| DOP2(Prod,_,DLAM(_,c')) -> srec c'
@@ -1258,15 +1272,15 @@ let info_arity env =
in
srec
-let is_logic_arity env c =
- try (not (info_arity env c)) with IsType -> false
+let is_logic_arity env sigma c =
+ try (not (info_arity env sigma c)) with IsType -> false
-let is_info_arity env c =
- try (info_arity env c) with IsType -> true
+let is_info_arity env sigma c =
+ try (info_arity env sigma c) with IsType -> true
-let is_type_arity env =
+let is_type_arity env sigma =
let rec srec c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env sigma c with
| DOP0(Sort(Type _)) -> true
| DOP2(Prod,_,DLAM(_,c')) -> srec c'
| DOP2(Lambda,_,DLAM(_,c')) -> srec c'
@@ -1274,21 +1288,21 @@ let is_type_arity env =
in
srec
-let is_info_type env t =
+let is_info_type env sigma t =
let s = t.typ in
(s = Prop Pos) ||
(s <> Prop Null &&
- try info_arity env t.body with IsType -> true)
+ try info_arity env sigma t.body with IsType -> true)
-let is_info_cast_type env c =
+let is_info_cast_type env sigma c =
match c with
| DOP2(Cast,c,t) ->
- (try info_arity env t
- with IsType -> try info_arity env c with IsType -> true)
- | _ -> try info_arity env c with IsType -> true
+ (try info_arity env sigma t
+ with IsType -> try info_arity env sigma c with IsType -> true)
+ | _ -> try info_arity env sigma c with IsType -> true
-let contents_of_cast_type env c =
- if is_info_cast_type env c then Pos else Null
+let contents_of_cast_type env sigma c =
+ if is_info_cast_type env sigma c then Pos else Null
let is_info_sort = is_info_arity
@@ -1320,64 +1334,61 @@ let add_free_rels_until depth m acc =
(* calcule la liste des arguments implicites *)
-let poly_args env t =
- let rec aux n t = match (whd_betadeltaiota env t) with
+let poly_args env sigma t =
+ let rec aux n t = match (whd_betadeltaiota env sigma t) with
| DOP2(Prod,a,DLAM(_,b)) -> add_free_rels_until n a (aux (n+1) b)
| DOP2(Cast,t',_) -> aux n t'
| _ -> []
in
- match (strip_outer_cast (whd_betadeltaiota env t)) with
+ match (strip_outer_cast (whd_betadeltaiota env sigma t)) with
| DOP2(Prod,a,DLAM(_,b)) -> aux 1 b
| _ -> []
(* Expanding existential variables (trad.ml, progmach.ml) *)
(* 1- whd_ise fails if an existential is undefined *)
-let rec whd_ise env = function
+let rec whd_ise env sigma = function
| DOPN(Evar sp,_) as k ->
- let evm = evar_map env in
- if Evd.in_dom evm sp then
- if Evd.is_defined evm sp then
- whd_ise env (constant_value env k)
+ if Evd.in_dom sigma sp then
+ if Evd.is_defined sigma sp then
+ whd_ise env sigma (existential_value sigma k)
else
errorlabstrm "whd_ise"
[< 'sTR"There is an unknown subterm I cannot solve" >]
else
k
- | DOP2(Cast,c,_) -> whd_ise env c
- | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ)))
+ | DOP2(Cast,c,_) -> whd_ise env sigma c
+ | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
| c -> c
(* 2- undefined existentials are left unchanged *)
-let rec whd_ise1 env = function
+let rec whd_ise1 env sigma = function
| (DOPN(Evar sp,_) as k) ->
- let evm = evar_map env in
- if Evd.in_dom evm sp & Evd.is_defined evm sp then
- whd_ise1 env (existential_value env k)
+ if Evd.in_dom sigma sp & Evd.is_defined sigma sp then
+ whd_ise1 env sigma (existential_value sigma k)
else
k
- | DOP2(Cast,c,_) -> whd_ise1 env c
+ | DOP2(Cast,c,_) -> whd_ise1 env sigma c
| DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
| c -> c
-let nf_ise1 env = strong (whd_ise1 env) env
+let nf_ise1 env sigma = strong (whd_ise1 env sigma) env sigma
(* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
* Similarly we have is_fmachine1_metas and is_resolve1_metas *)
-let rec whd_ise1_metas env = function
+let rec whd_ise1_metas env sigma = function
| (DOPN(Evar n,_) as k) ->
- let evm = evar_map env in
- if Evd.in_dom evm n then
- if Evd.is_defined evm n then
- whd_ise1_metas env (existential_value env k)
+ if Evd.in_dom sigma n then
+ if Evd.is_defined sigma n then
+ whd_ise1_metas env sigma (existential_value sigma k)
else
let m = DOP0(Meta (new_meta())) in
- DOP2(Cast,m,existential_type env k)
+ DOP2(Cast,m,existential_type sigma k)
else
k
- | DOP2(Cast,c,_) -> whd_ise1_metas env c
+ | DOP2(Cast,c,_) -> whd_ise1_metas env sigma c
| c -> c
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 771899fad8..421aa9aaf2 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -6,6 +6,7 @@ open Names
open Generic
open Term
open Univ
+open Evd
open Environ
open Closure
(*i*)
@@ -16,97 +17,99 @@ exception Redelimination
exception Induc
exception Elimconst
-type reduction_function = unsafe_env -> constr -> constr
+type 'a reduction_function = unsafe_env -> 'a evar_map -> constr -> constr
-type stack_reduction_function =
- unsafe_env -> constr -> constr list -> constr * constr list
+type 'a stack_reduction_function =
+ unsafe_env -> 'a evar_map -> constr -> constr list -> constr * constr list
-val whd_stack : stack_reduction_function
+val whd_stack : 'a stack_reduction_function
(*s Reduction Function Operators *)
-val under_casts : reduction_function -> reduction_function
-val strong : reduction_function -> reduction_function
-val strong_prodspine : reduction_function -> reduction_function
+val under_casts : 'a reduction_function -> 'a reduction_function
+val strong : 'a reduction_function -> 'a reduction_function
+val strong_prodspine : 'a reduction_function -> 'a reduction_function
val stack_reduction_of_reduction :
- reduction_function -> stack_reduction_function
+ 'a reduction_function -> 'a stack_reduction_function
(*s Generic Optimized Reduction Functions using Closures *)
(* 1. lazy strategy *)
-val clos_norm_flags : Closure.flags -> reduction_function
+val clos_norm_flags : Closure.flags -> 'a reduction_function
(* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *)
-val nf_beta : reduction_function
-val nf_betaiota : reduction_function
-val nf_betadeltaiota : reduction_function
+val nf_beta : 'a reduction_function
+val nf_betaiota : 'a reduction_function
+val nf_betadeltaiota : 'a reduction_function
(* 2. call by value strategy *)
-val cbv_norm_flags : flags -> reduction_function
-val cbv_beta : reduction_function
-val cbv_betaiota : reduction_function
-val cbv_betadeltaiota : reduction_function
+val cbv_norm_flags : flags -> 'a reduction_function
+val cbv_beta : 'a reduction_function
+val cbv_betaiota : 'a reduction_function
+val cbv_betadeltaiota : 'a reduction_function
(* 3. lazy strategy, weak head reduction *)
-val whd_beta : reduction_function
-val whd_betaiota : reduction_function
-val whd_betadeltaiota : reduction_function
+val whd_beta : 'a reduction_function
+val whd_betaiota : 'a reduction_function
+val whd_betadeltaiota : 'a reduction_function
-val whd_beta_stack : stack_reduction_function
-val whd_betaiota_stack : stack_reduction_function
-val whd_betadeltaiota_stack : stack_reduction_function
+val whd_beta_stack : 'a stack_reduction_function
+val whd_betaiota_stack : 'a stack_reduction_function
+val whd_betadeltaiota_stack : 'a stack_reduction_function
(*s Head normal forms *)
-val whd_const_stack : section_path list -> stack_reduction_function
-val whd_const : section_path list -> reduction_function
-val whd_delta_stack : stack_reduction_function
-val whd_delta : reduction_function
-val whd_betadelta_stack : stack_reduction_function
-val whd_betadelta : reduction_function
-val whd_betadeltat_stack : stack_reduction_function
-val whd_betadeltat : reduction_function
-val whd_betadeltatiota_stack : stack_reduction_function
-val whd_betadeltatiota : reduction_function
-val whd_betadeltaiotaeta_stack : stack_reduction_function
-val whd_betadeltaiotaeta : reduction_function
+val whd_const_stack : section_path list -> 'a stack_reduction_function
+val whd_const : section_path list -> 'a reduction_function
+val whd_delta_stack : 'a stack_reduction_function
+val whd_delta : 'a reduction_function
+val whd_betadelta_stack : 'a stack_reduction_function
+val whd_betadelta : 'a reduction_function
+val whd_betadeltat_stack : 'a stack_reduction_function
+val whd_betadeltat : 'a reduction_function
+val whd_betadeltatiota_stack : 'a stack_reduction_function
+val whd_betadeltatiota : 'a reduction_function
+val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
+val whd_betadeltaiotaeta : 'a reduction_function
val beta_applist : (constr * constr list) -> constr
-val hnf_prod_app : unsafe_env -> string -> constr -> constr -> constr
+val hnf_prod_app :
+ unsafe_env -> 'a evar_map -> string -> constr -> constr -> constr
val hnf_prod_appvect :
- unsafe_env -> string -> constr -> constr array -> constr
+ unsafe_env -> 'a evar_map -> string -> constr -> constr array -> constr
val hnf_prod_applist :
- unsafe_env -> string -> constr -> constr list -> constr
+ unsafe_env -> 'a evar_map -> string -> constr -> constr list -> constr
val hnf_lam_app :
- unsafe_env -> string -> constr -> constr -> constr
+ unsafe_env -> 'a evar_map -> string -> constr -> constr -> constr
val hnf_lam_appvect :
- unsafe_env -> string -> constr -> constr array -> constr
+ unsafe_env -> 'a evar_map -> string -> constr -> constr array -> constr
val hnf_lam_applist :
- unsafe_env -> string -> constr -> constr list -> constr
-val splay_prod : unsafe_env -> constr -> (name * constr) list * constr
-val decomp_prod : unsafe_env -> constr -> int * constr
+ unsafe_env -> 'a evar_map -> string -> constr -> constr list -> constr
+val splay_prod :
+ unsafe_env -> 'a evar_map -> constr -> (name * constr) list * constr
+val decomp_prod : unsafe_env -> 'a evar_map -> constr -> int * constr
val decomp_n_prod :
- unsafe_env -> int -> constr -> ((name * constr) list) * constr
+ unsafe_env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
-val is_arity : unsafe_env -> constr -> bool
-val is_info_arity : unsafe_env -> constr -> bool
-val is_info_sort : unsafe_env -> constr -> bool
-val is_logic_arity : unsafe_env -> constr -> bool
-val is_type_arity : unsafe_env -> constr -> bool
-val is_info_type : unsafe_env -> typed_type -> bool
-val is_info_cast_type : unsafe_env -> constr -> bool
-val contents_of_cast_type : unsafe_env -> constr -> contents
-val poly_args : unsafe_env -> constr -> int list
+val is_arity : unsafe_env -> 'a evar_map -> constr -> bool
+val is_info_arity : unsafe_env -> 'a evar_map -> constr -> bool
+val is_info_sort : unsafe_env -> 'a evar_map -> constr -> bool
+val is_logic_arity : unsafe_env -> 'a evar_map -> constr -> bool
+val is_type_arity : unsafe_env -> 'a evar_map -> constr -> bool
+val is_info_type : unsafe_env -> 'a evar_map -> typed_type -> bool
+val is_info_cast_type : unsafe_env -> 'a evar_map -> constr -> bool
+val contents_of_cast_type : unsafe_env -> 'a evar_map -> constr -> contents
+val poly_args : unsafe_env -> 'a evar_map -> constr -> int list
-val whd_programs : reduction_function
+val whd_programs : 'a reduction_function
val unfoldn :
- (int list * section_path) list -> reduction_function
-val fold_one_com : constr -> reduction_function
-val fold_commands : constr list -> reduction_function
+ (int list * section_path) list -> 'a reduction_function
+val fold_one_com : constr -> 'a reduction_function
+val fold_commands : constr list -> 'a reduction_function
val subst_term_occ : int list -> constr -> constr -> constr
-val pattern_occs : (int list * constr * constr) list -> reduction_function
-val compute : reduction_function
+val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
+val compute : 'a reduction_function
(*s Conversion Functions (uses closures, lazy strategy) *)
@@ -131,51 +134,55 @@ val convert_or : conversion_test -> conversion_test -> conversion_test
val convert_forall2 :
('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test
-type conversion_function = unsafe_env -> constr -> constr -> constraints
+type 'a conversion_function =
+ unsafe_env -> 'a evar_map -> constr -> constr -> constraints
-val fconv : conv_pb -> conversion_function
+val fconv : conv_pb -> 'a conversion_function
(* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and
[conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *)
-val conv : conversion_function
-val conv_leq : conversion_function
+val conv : 'a conversion_function
+val conv_leq : 'a conversion_function
val conv_forall2 :
- conversion_function -> unsafe_env -> constr array
+ 'a conversion_function -> unsafe_env -> 'a evar_map -> constr array
-> constr array -> constraints
val conv_forall2_i :
- (int -> conversion_function) -> unsafe_env
+ (int -> 'a conversion_function) -> unsafe_env -> 'a evar_map
-> constr array -> constr array -> constraints
-val is_conv : unsafe_env -> constr -> constr -> bool
-val is_conv_leq : unsafe_env -> constr -> constr -> bool
+val is_conv : unsafe_env -> 'a evar_map -> constr -> constr -> bool
+val is_conv_leq : unsafe_env -> 'a evar_map -> constr -> constr -> bool
(*s Special-Purpose Reduction Functions *)
-val whd_meta : reduction_function
+val whd_meta : 'a reduction_function
val plain_instance : (int * constr) list -> constr -> constr
-val instance : (int * constr) list -> reduction_function
+val instance : (int * constr) list -> 'a reduction_function
-val whd_ise : reduction_function
-val whd_ise1 : reduction_function
-val nf_ise1 : reduction_function
-val whd_ise1_metas : reduction_function
+val whd_ise : 'a reduction_function
+val whd_ise1 : 'a reduction_function
+val nf_ise1 : 'a reduction_function
+val whd_ise1_metas : 'a reduction_function
(*s Obsolete Reduction Functions *)
-val hnf : unsafe_env -> constr -> constr * constr list
-val apprec : stack_reduction_function
-val red_product : reduction_function
-val find_mrectype : unsafe_env -> constr -> constr * constr list
-val find_minductype : unsafe_env -> constr -> constr * constr list
-val find_mcoinductype : unsafe_env -> constr -> constr * constr list
-val check_mrectype_spec : unsafe_env -> constr -> constr
-val minductype_spec : unsafe_env -> constr -> constr
-val mrectype_spec : unsafe_env -> constr -> constr
+val hnf : unsafe_env -> 'a evar_map -> constr -> constr * constr list
+val apprec : 'a stack_reduction_function
+val red_product : 'a reduction_function
+val find_mrectype :
+ unsafe_env -> 'a evar_map -> constr -> constr * constr list
+val find_minductype :
+ unsafe_env -> 'a evar_map -> constr -> constr * constr list
+val find_mcoinductype :
+ unsafe_env -> 'a evar_map -> constr -> constr * constr list
+val check_mrectype_spec : unsafe_env -> 'a evar_map -> constr -> constr
+val minductype_spec : unsafe_env -> 'a evar_map -> constr -> constr
+val mrectype_spec : unsafe_env -> 'a evar_map -> constr -> constr
(* Special function, which keep the key casts under Fix and MutCase. *)
val strip_all_casts : constr -> constr
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 405b139bac..010dde8e27 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -26,13 +26,13 @@ let j_val = j_val_only
let j_val_cast j = mkCast j.uj_val j.uj_type
-let typed_type_of_judgment env j =
- match whd_betadeltaiota env j.uj_kind with
+let typed_type_of_judgment env sigma j =
+ match whd_betadeltaiota env sigma j.uj_kind with
| DOP0(Sort s) -> { body = j.uj_type; typ = s }
| _ -> error_not_type CCI env j.uj_type
-let assumption_of_judgment env j =
- match whd_betadeltaiota env j.uj_type with
+let assumption_of_judgment env sigma j =
+ match whd_betadeltaiota env sigma j.uj_type with
| DOP0(Sort s) -> { body = j.uj_val; typ = s }
| _ -> error_assumption CCI env j.uj_val
@@ -51,7 +51,7 @@ let relative env n =
(* Checks if a context of variable is included in another one. *)
-let hyps_inclusion env (idl1,tyl1) (idl2,tyl2) =
+let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) =
let rec aux = function
| ([], [], _, _) -> true
| (_, _, [], []) -> false
@@ -60,7 +60,7 @@ let hyps_inclusion env (idl1,tyl1) (idl2,tyl2) =
| ([], []) -> false
| ((id2::idl2), (ty2::tyl2)) ->
if id1 = id2 then
- (is_conv env (body_of_type ty1) (body_of_type ty2))
+ (is_conv env sigma (body_of_type ty1) (body_of_type ty2))
& aux (idl1,tyl1,idl2,tyl2)
else
search (idl2,tyl2)
@@ -74,25 +74,25 @@ let hyps_inclusion env (idl1,tyl1) (idl2,tyl2) =
(* Checks if the given context of variables [hyps] is included in the
current context of [env]. *)
-let construct_reference id env hyps =
+let construct_reference id env sigma hyps =
let hyps' = get_globals (context env) in
- if hyps_inclusion env hyps hyps' then
+ if hyps_inclusion env sigma hyps hyps' then
Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))
else
error_reference_variables CCI env id
-let check_hyps id env hyps =
+let check_hyps id env sigma hyps =
let hyps' = get_globals (context env) in
- if not (hyps_inclusion env hyps hyps') then
+ if not (hyps_inclusion env sigma hyps hyps') then
error_reference_variables CCI env id
(* Instantiation of terms on real arguments. *)
-let type_of_constant env c =
+let type_of_constant env sigma c =
let (sp,args) = destConst c in
let cb = lookup_constant sp env in
let hyps = cb.const_hyps in
- check_hyps (basename sp) env hyps;
+ check_hyps (basename sp) env sigma hyps;
instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args)
(* Inductive types. *)
@@ -104,10 +104,10 @@ let instantiate_arity mis =
{ body = instantiate_constr ids arity.body args;
typ = arity.typ }
-let type_of_inductive env i =
+let type_of_inductive env sigma i =
let mis = lookup_mind_specif i env in
let hyps = mis.mis_mib.mind_hyps in
- check_hyps (basename mis.mis_sp) env hyps;
+ check_hyps (basename mis.mis_sp) env sigma hyps;
instantiate_arity mis
(* Constructors. *)
@@ -117,12 +117,12 @@ let instantiate_lc mis =
let lc = mis.mis_mip.mind_lc in
instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args)
-let type_of_constructor env c =
+let type_of_constructor env sigma c =
let (sp,i,j,args) = destMutConstruct c in
let mind = DOPN (MutInd (sp,i), args) in
- let recmind = check_mrectype_spec env mind in
+ let recmind = check_mrectype_spec env sigma mind in
let mis = lookup_mind_specif recmind env in
- check_hyps (basename mis.mis_sp) env (mis.mis_mib.mind_hyps);
+ check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps);
let specif = instantiate_lc mis in
let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in
if j > mis_nconstr mis then
@@ -145,21 +145,21 @@ let mis_type_mconstructs mis =
(Array.init nconstr make_ck,
sAPPVList specif (list_tabulate make_ik ntypes))
-let type_mconstructs env mind =
- let redmind = check_mrectype_spec env mind in
+let type_mconstructs env sigma mind =
+ let redmind = check_mrectype_spec env sigma mind in
let mis = lookup_mind_specif redmind env in
mis_type_mconstructs mis
(* Case. *)
-let rec sort_of_arity env c =
- match whd_betadeltaiota env c with
+let rec sort_of_arity env sigma c =
+ match whd_betadeltaiota env sigma c with
| DOP0(Sort( _)) as c' -> c'
- | DOP2(Prod,_,DLAM(_,c2)) -> sort_of_arity env c2
+ | DOP2(Prod,_,DLAM(_,c2)) -> sort_of_arity env sigma c2
| _ -> invalid_arg "sort_of_arity"
-let make_arity_dep env k =
- let rec mrec c m = match whd_betadeltaiota env c with
+let make_arity_dep env sigma k =
+ let rec mrec c m = match whd_betadeltaiota env sigma c with
| DOP0(Sort _) -> mkArrow m k
| DOP2(Prod,b,DLAM(n,c_0)) ->
prod_name env (n,b,mrec c_0 (applist(lift 1 m,[Rel 1])))
@@ -167,16 +167,16 @@ let make_arity_dep env k =
in
mrec
-let make_arity_nodep env k =
- let rec mrec c = match whd_betadeltaiota env c with
+let make_arity_nodep env sigma k =
+ let rec mrec c = match whd_betadeltaiota env sigma c with
| DOP0(Sort _) -> k
| DOP2(Prod,b,DLAM(x,c_0)) -> DOP2(Prod,b,DLAM(x,mrec c_0))
| _ -> invalid_arg "make_arity_nodep"
in
mrec
-let error_elim_expln env kp ki =
- if is_info_sort env kp && not (is_info_sort env ki) then
+let error_elim_expln env sigma kp ki =
+ if is_info_sort env sigma kp && not (is_info_sort env sigma ki) then
"non-informative objects may not construct informative ones."
else
match (kp,ki) with
@@ -186,24 +186,24 @@ let error_elim_expln env kp ki =
exception Arity of (constr * constr * string) option
-let is_correct_arity env kelim (c,p) =
+let is_correct_arity env sigma kelim (c,p) =
let rec srec ind (pt,t) =
try
- (match whd_betadeltaiota env pt, whd_betadeltaiota env t with
+ (match whd_betadeltaiota env sigma pt, whd_betadeltaiota env sigma t with
| DOP2(Prod,a1,DLAM(_,a2)), DOP2(Prod,a1',DLAM(_,a2')) ->
- if is_conv env a1 a1' then
+ if is_conv env sigma a1 a1' then
srec (applist(lift 1 ind,[Rel 1])) (a2,a2')
else
raise (Arity None)
| DOP2(Prod,a1,DLAM(_,a2)), ki ->
- let k = whd_betadeltaiota env a2 in
+ let k = whd_betadeltaiota env sigma a2 in
let ksort = (match k with DOP0(Sort s) -> s
| _ -> raise (Arity None)) in
- if is_conv env a1 ind then
+ if is_conv env sigma a1 ind then
if List.exists (base_sort_cmp CONV ksort) kelim then
(true,k)
else
- raise (Arity (Some(k,ki,error_elim_expln env k ki)))
+ raise (Arity (Some(k,ki,error_elim_expln env sigma k ki)))
else
raise (Arity None)
| k, DOP2(Prod,_,_) ->
@@ -214,11 +214,13 @@ let is_correct_arity env kelim (c,p) =
if List.exists (base_sort_cmp CONV ksort) kelim then
false,k
else
- raise (Arity (Some(k,ki,error_elim_expln env k ki))))
+ raise (Arity (Some(k,ki,error_elim_expln env sigma k ki))))
with Arity kinds ->
let listarity =
- (List.map (fun s -> make_arity_dep env (DOP0(Sort s)) t ind) kelim)
- @(List.map (fun s -> make_arity_nodep env (DOP0(Sort s)) t) kelim)
+ (List.map
+ (fun s -> make_arity_dep env sigma (DOP0(Sort s)) t ind) kelim)
+ @(List.map
+ (fun s -> make_arity_nodep env sigma (DOP0(Sort s)) t) kelim)
in error_elim_arity CCI env ind listarity c p pt kinds
in srec
@@ -226,20 +228,20 @@ let cast_instantiate_arity mis =
let tty = instantiate_arity mis in
DOP2 (Cast, tty.body, DOP0 (Sort tty.typ))
-let find_case_dep_nparams env (c,p) (mind,largs) typP =
+let find_case_dep_nparams env sigma (c,p) (mind,largs) typP =
let mis = lookup_mind_specif mind env in
let nparams = mis_nparams mis
and kelim = mis_kelim mis
and t = cast_instantiate_arity mis in
let (globargs,la) = list_chop nparams largs in
- let glob_t = hnf_prod_applist env "find_elim_boolean" t globargs in
+ let glob_t = hnf_prod_applist env sigma "find_elim_boolean" t globargs in
let arity = applist(mind,globargs) in
- let (dep,_) = is_correct_arity env kelim (c,p) arity (typP,glob_t) in
+ let (dep,_) = is_correct_arity env sigma kelim (c,p) arity (typP,glob_t) in
(dep, (nparams, globargs,la))
-let type_one_branch_dep (env,nparams,globargs,p) co t =
+let type_one_branch_dep env sigma (nparams,globargs,p) co t =
let rec typrec n c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env sigma c with
| DOP2(Prod,a1,DLAM(x,a2)) -> prod_name env (x,a1,typrec (n+1) a2)
| x -> let lAV = destAppL (ensure_appl x) in
let (_,vargs) = array_chop (nparams+1) lAV in
@@ -247,17 +249,17 @@ let type_one_branch_dep (env,nparams,globargs,p) co t =
(appvect ((lift n p),vargs),
[applist(co,((List.map (lift n) globargs)@(rel_list 0 n)))])
in
- typrec 0 (hnf_prod_applist env "type_case" t globargs)
+ typrec 0 (hnf_prod_applist env sigma "type_case" t globargs)
-let type_one_branch_nodep (env,nparams,globargs,p) t =
+let type_one_branch_nodep env sigma (nparams,globargs,p) t =
let rec typrec n c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env sigma c with
| DOP2(Prod,a1,DLAM(x,a2)) -> DOP2(Prod,a1,DLAM(x,typrec (n+1) a2))
| x -> let lAV = destAppL(ensure_appl x) in
let (_,vargs) = array_chop (nparams+1) lAV in
appvect (lift n p,vargs)
in
- typrec 0 (hnf_prod_applist env "type_case" t globargs)
+ typrec 0 (hnf_prod_applist env sigma "type_case" t globargs)
(* type_case_branches type un <p>Case c of ... end
ct = type de c, si inductif il a la forme APP(mI,largs), sinon raise Induc
@@ -266,45 +268,45 @@ let type_one_branch_nodep (env,nparams,globargs,p) t =
attendus dans les branches du Case; lr est le type attendu du resultat
*)
-let type_case_branches env ct pt p c =
+let type_case_branches env sigma ct pt p c =
try
- let ((mI,largs) as indt) = find_mrectype env ct in
+ let ((mI,largs) as indt) = find_mrectype env sigma ct in
let (dep,(nparams,globargs,la)) =
- find_case_dep_nparams env (c,p) indt pt
+ find_case_dep_nparams env sigma (c,p) indt pt
in
- let (lconstruct,ltypconstr) = type_mconstructs env mI in
+ let (lconstruct,ltypconstr) = type_mconstructs env sigma mI in
if dep then
(mI,
- array_map2 (type_one_branch_dep (env,nparams,globargs,p))
+ array_map2 (type_one_branch_dep env sigma (nparams,globargs,p))
lconstruct ltypconstr,
beta_applist (p,(la@[c])))
else
(mI,
- Array.map (type_one_branch_nodep (env,nparams,globargs,p))
+ Array.map (type_one_branch_nodep env sigma (nparams,globargs,p))
ltypconstr,
beta_applist (p,la))
with Induc ->
error_case_not_inductive CCI env c ct
-let check_branches_message env (c,ct) (explft,lft) =
+let check_branches_message env sigma (c,ct) (explft,lft) =
let n = Array.length explft
and expn = Array.length lft in
let rec check_conv i =
if not (i = n) then
- if not (is_conv_leq env lft.(i) (explft.(i))) then
- error_ill_formed_branch CCI env c i (nf_betaiota env lft.(i))
- (nf_betaiota env explft.(i))
+ if not (is_conv_leq env sigma lft.(i) (explft.(i))) then
+ error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i))
+ (nf_betaiota env sigma explft.(i))
else
check_conv (i+1)
in
if n<>expn then error_number_branches CCI env c ct expn else check_conv 0
-let type_of_case env pj cj lfj =
+let type_of_case env sigma pj cj lfj =
let lft = Array.map (fun j -> j.uj_type) lfj in
let (mind,bty,rslty) =
- type_case_branches env cj.uj_type pj.uj_type pj.uj_val cj.uj_val in
- let kind = sort_of_arity env pj.uj_type in
- check_branches_message env (cj.uj_val,cj.uj_type) (bty,lft);
+ type_case_branches env sigma cj.uj_type pj.uj_type pj.uj_val cj.uj_val in
+ let kind = sort_of_arity env sigma pj.uj_type in
+ check_branches_message env sigma (cj.uj_val,cj.uj_type) (bty,lft);
{ uj_val =
mkMutCaseA (ci_of_mind mind) (j_val pj) (j_val cj) (Array.map j_val lfj);
uj_type = rslty;
@@ -345,8 +347,8 @@ let sort_of_product domsort rangsort g =
(* Product rule (Type_i,Type_i,Type_i) *)
| Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst)
-let abs_rel env name var j =
- let rngtyp = whd_betadeltaiota env j.uj_kind in
+let abs_rel env sigma name var j =
+ let rngtyp = whd_betadeltaiota env sigma j.uj_kind in
let cvar = incast_type var in
let (s,cst) = sort_of_product var.typ (destSort rngtyp) (universes env) in
{ uj_val = mkLambda name cvar (j_val j);
@@ -356,9 +358,9 @@ let abs_rel env name var j =
(* Type of a product. *)
-let gen_rel env name var j =
- let jtyp = whd_betadeltaiota env j.uj_type in
- let jkind = whd_betadeltaiota env j.uj_kind in
+let gen_rel env sigma name var j =
+ let jtyp = whd_betadeltaiota env sigma j.uj_type in
+ let jkind = whd_betadeltaiota env sigma j.uj_kind in
let j = { uj_val = j.uj_val; uj_type = jtyp; uj_kind = jkind } in
if isprop jkind then
error "Proof objects can only be abstracted"
@@ -377,17 +379,17 @@ let gen_rel env name var j =
(* Type of a cast. *)
-let cast_rel env cj tj =
- if is_conv_leq env cj.uj_type tj.uj_val then
+let cast_rel env sigma cj tj =
+ if is_conv_leq env sigma cj.uj_type tj.uj_val then
{ uj_val = j_val_only cj;
uj_type = tj.uj_val;
- uj_kind = whd_betadeltaiota env tj.uj_type }
+ uj_kind = whd_betadeltaiota env sigma tj.uj_type }
else
error_actual_type CCI env cj.uj_val cj.uj_type tj.uj_val
(* Type of an application. *)
-let apply_rel_list env nocheck argjl funj =
+let apply_rel_list env sigma nocheck argjl funj =
let rec apply_rec typ cst = function
| [] ->
{ uj_val = applist (j_val_only funj, List.map j_val_only argjl);
@@ -395,13 +397,13 @@ let apply_rel_list env nocheck argjl funj =
uj_kind = funj.uj_kind },
cst
| hj::restjl ->
- match whd_betadeltaiota env typ with
+ match whd_betadeltaiota env sigma typ with
| DOP2(Prod,c1,DLAM(_,c2)) ->
if nocheck then
apply_rec (subst1 hj.uj_val c2) cst restjl
else
(try
- let c = conv_leq env hj.uj_type c1 in
+ let c = conv_leq env sigma hj.uj_type c1 in
let cst' = Constraint.union cst c in
apply_rec (subst1 hj.uj_val c2) cst' restjl
with NotConvertible ->
@@ -421,7 +423,7 @@ let apply_rel_list env nocheck argjl funj =
which may contain the CoFix variables. These occurrences of CoFix variables
are not considered *)
-let noccur_with_meta sigma n m term =
+let noccur_with_meta lc n m term =
let rec occur_rec n = function
| Rel p -> if n<=p & p<n+m then raise Occur
| VAR _ -> ()
@@ -429,7 +431,7 @@ let noccur_with_meta sigma n m term =
(match strip_outer_cast cl.(0) with
| DOP0 (Meta _) -> ()
| _ -> Array.iter (occur_rec n) cl)
- | DOPN(Const sp, cl) when Spset.mem sp sigma -> ()
+ | DOPN(Const sp, cl) when Spset.mem sp lc -> ()
| DOPN(op,cl) -> Array.iter (occur_rec n) cl
| DOPL(_,cl) -> List.iter (occur_rec n) cl
| DOP0(_) -> ()
@@ -489,14 +491,14 @@ let check_term env mind_recvec f =
in
crec
-let is_inst_var env k c =
- match whd_betadeltaiota_stack env c [] with
+let is_inst_var env sigma k c =
+ match whd_betadeltaiota_stack env sigma c [] with
| (Rel n,_) -> n=k
| _ -> false
-let is_subterm_specif env lcx mind_recvec =
+let is_subterm_specif env sigma lcx mind_recvec =
let rec crec n lst c =
- match whd_betadeltaiota_stack env c [] with
+ match whd_betadeltaiota_stack env sigma c [] with
| ((Rel k),_) -> find_sorted_assoc k lst
| (DOPN(MutCase _,_) as x,_) ->
let ( _,_,c,br) = destCase x in
@@ -505,7 +507,7 @@ let is_subterm_specif env lcx mind_recvec =
else
let lcv =
(try
- if is_inst_var env n c then lcx else (crec n lst c)
+ if is_inst_var env sigma n c then lcx else (crec n lst c)
with Not_found -> (Array.create (Array.length br) []))
in
assert (Array.length br = Array.length lcv);
@@ -552,16 +554,16 @@ let is_subterm_specif env lcx mind_recvec =
in
crec
-let is_subterm env lcx mind_recvec n lst c =
+let is_subterm env sigma lcx mind_recvec n lst c =
try
- let _ = is_subterm_specif env lcx mind_recvec n lst c in true
+ let _ = is_subterm_specif env sigma lcx mind_recvec n lst c in true
with Not_found ->
false
(* Auxiliary function: it checks a condition f depending on a deBrujin
index for a certain number of abstractions *)
-let rec check_subterm_rec_meta env sigma vectn k def =
+let rec check_subterm_rec_meta env sigma lc vectn k def =
(k < 0) or
(let nfi = Array.length vectn in
(* check fi does not appear in the k+1 first abstractions,
@@ -569,14 +571,14 @@ let rec check_subterm_rec_meta env sigma vectn k def =
let rec check_occur n def =
(match strip_outer_cast def with
| DOP2(Lambda,a,DLAM(_,b)) ->
- if noccur_with_meta sigma n nfi a then
+ if noccur_with_meta lc n nfi a then
if n = k+1 then (a,b) else check_occur (n+1) b
else
error "Bad occurrence of recursive call"
| _ -> error "Not enough abstractions in the definition") in
let (c,d) = check_occur 1 def in
let (mI, largs) =
- (try find_minductype env c
+ (try find_minductype env sigma c
with Induc -> error "Recursive definition on a non inductive type") in
let (sp,tyi,_) = destMutInd mI in
let mind_recvec = mis_recargs (lookup_mind_specif mI env) in
@@ -587,9 +589,9 @@ let rec check_subterm_rec_meta env sigma vectn k def =
*)
let rec check_rec_call n lst t =
(* n gives the index of the recursive variable *)
- (noccur_with_meta sigma (n+k+1) nfi t) or
+ (noccur_with_meta lc (n+k+1) nfi t) or
(* no recursive call in the term *)
- (match whd_betadeltaiota_stack env t [] with
+ (match whd_betadeltaiota_stack env sigma t [] with
| (Rel p,l) ->
if n+k+1 <= p & p < n+k+nfi+1 then
(* recursive call *)
@@ -598,7 +600,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
if List.length l > np then
(match list_chop np l with
(la,(z::lrest)) ->
- if (is_subterm env lcx mind_recvec n lst z)
+ if (is_subterm env sigma lcx mind_recvec n lst z)
then List.for_all (check_rec_call n lst) (la@lrest)
else error "Recursive call applied to an illegal term"
| _ -> assert false)
@@ -608,10 +610,10 @@ let rec check_subterm_rec_meta env sigma vectn k def =
let (ci,p,c_0,lrest) = destCase mc in
let lc =
(try
- if is_inst_var env n c_0 then
+ if is_inst_var env sigma n c_0 then
lcx
else
- is_subterm_specif env lcx mind_recvec n lst c_0
+ is_subterm_specif env sigma lcx mind_recvec n lst c_0
with Not_found ->
Array.create (Array.length lrest) [])
in
@@ -646,8 +648,10 @@ let rec check_subterm_rec_meta env sigma vectn k def =
else
let theDecrArg = List.nth l decrArg in
let recArgsDecrArg =
- try (is_subterm_specif env lcx mind_recvec n lst theDecrArg)
- with Not_found -> Array.create 0 []
+ try
+ is_subterm_specif env sigma lcx mind_recvec n lst theDecrArg
+ with Not_found ->
+ Array.create 0 []
in
if (Array.length recArgsDecrArg)=0 then
array_for_all (check_rec_call n lst) la
@@ -698,7 +702,7 @@ nvect is [|n1;..;nk|] which gives for each recursive definition
the inductive-decreasing index
the function checks the convertibility of ti with Ai *)
-let check_fix env sigma = function
+let check_fix env sigma lc = function
| DOPN(Fix(nvect,j),vargs) ->
let nbfix = let nv = Array.length vargs in
if nv < 2 then error "Ill-formed recursive definition" else nv-1 in
@@ -714,7 +718,7 @@ let check_fix env sigma = function
let check_type i =
try
let _ =
- check_subterm_rec_meta env sigma nvect nvect.(i) vdefs.(i) in
+ check_subterm_rec_meta env sigma lc nvect nvect.(i) vdefs.(i) in
()
with UserError (s,str) ->
error_ill_formed_rec_body CCI env str lna i vdefs
@@ -728,12 +732,12 @@ let check_fix env sigma = function
let mind_nparams env i =
let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
-let check_guard_rec_meta env sigma nbfix def deftype =
+let check_guard_rec_meta env sigma lc nbfix def deftype =
let rec codomain_is_coind c =
- match whd_betadeltaiota env (strip_outer_cast c) with
+ match whd_betadeltaiota env sigma (strip_outer_cast c) with
| DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b
| b ->
- (try find_mcoinductype env b
+ (try find_mcoinductype env sigma b
with
| Induc -> error "The codomain is not a coinductive type"
| _ -> error "Type of Cofix function not as expected")
@@ -743,17 +747,17 @@ let check_guard_rec_meta env sigma nbfix def deftype =
let lvlra = (mis_recargs (lookup_mind_specif mI env)) in
let vlra = lvlra.(tyi) in
let rec check_rec_call alreadygrd n vlra t =
- if noccur_with_meta sigma n nbfix t then
+ if noccur_with_meta lc n nbfix t then
true
else
- match whd_betadeltaiota_stack env t [] with
+ match whd_betadeltaiota_stack env sigma t [] with
| (DOP0 (Meta _), l) -> true
| (Rel p,l) ->
if n <= p && p < n+nbfix then
(* recursive call *)
if alreadygrd then
- if List.for_all (noccur_with_meta sigma n nbfix) l then
+ if List.for_all (noccur_with_meta lc n nbfix) l then
true
else
error "Nested recursive occurrences"
@@ -792,14 +796,14 @@ let check_guard_rec_meta env sigma nbfix def deftype =
(process_args_of_constr lr lrar)
| _::lrar ->
- if (noccur_with_meta sigma n nbfix t)
+ if (noccur_with_meta lc n nbfix t)
then (process_args_of_constr lr lrar)
else error "Recursive call inside a non-recursive argument of constructor")
in (process_args_of_constr realargs lra)
| (DOP2(Lambda,a,DLAM(_,b)),[]) ->
- if (noccur_with_meta sigma n nbfix a) then
+ if (noccur_with_meta lc n nbfix a) then
check_rec_call alreadygrd (n+1) vlra b
else
error "Recursive call in the type of an abstraction"
@@ -817,7 +821,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
let (lna,vdefs) = decomp_DLAMV_name la ldef in
let vlna = Array.of_list lna
in
- if (array_for_all (noccur_with_meta sigma n nbfix) varit) then
+ if (array_for_all (noccur_with_meta lc n nbfix) varit) then
(array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
&&
(List.for_all (check_rec_call alreadygrd (n+1) vlra) l)
@@ -826,9 +830,9 @@ let check_guard_rec_meta env sigma nbfix def deftype =
| (DOPN(MutCase _,_) as mc,l) ->
let (_,p,c,vrest) = destCase mc in
- if (noccur_with_meta sigma n nbfix p) then
- if (noccur_with_meta sigma n nbfix c) then
- if (List.for_all (noccur_with_meta sigma n nbfix) l) then
+ if (noccur_with_meta lc n nbfix p) then
+ if (noccur_with_meta lc n nbfix c) then
+ if (List.for_all (noccur_with_meta lc n nbfix) l) then
(array_for_all (check_rec_call alreadygrd n vlra) vrest)
else
error "Recursive call in the argument of a function defined by cases"
@@ -845,7 +849,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
(* The function which checks that the whole block of definitions
satisfies the guarded condition *)
-let check_cofix env sigma f =
+let check_cofix env sigma lc f =
match f with
| DOPN(CoFix(j),vargs) ->
let nbfix = let nv = Array.length vargs in
@@ -862,7 +866,7 @@ let check_cofix env sigma f =
let check_type i =
try
let _ =
- check_guard_rec_meta env sigma nbfix vdefs.(i) varit.(i) in
+ check_guard_rec_meta env sigma lc nbfix vdefs.(i) varit.(i) in
()
with UserError (s,str) ->
error_ill_formed_rec_body CCI env str lna i vdefs
@@ -876,7 +880,7 @@ let check_cofix env sigma f =
exception IllBranch of int
-let type_fixpoint env lna lar vdefj =
+let type_fixpoint env sigma lna lar vdefj =
let lt = Array.length vdefj in
assert (Array.length lar = lt);
try
@@ -884,6 +888,7 @@ let type_fixpoint env lna lar vdefj =
(fun i e def ar ->
try conv_leq e def (lift lt ar)
with NotConvertible -> raise (IllBranch i))
- env (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
+ env sigma
+ (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
with IllBranch i ->
error_ill_typed_rec_body CCI env i lna vdefj lar
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 0a4419a608..f876012996 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -5,6 +5,7 @@
open Names
open Univ
open Term
+open Evd
open Environ
(*i*)
@@ -19,22 +20,25 @@ val j_val_only : unsafe_judgment -> constr
constructs the typed type $t:s$, while [assumption_of_judgement env j]
cosntructs the type type $c:t$, checking that $t$ is a sort. *)
-val typed_type_of_judgment : unsafe_env -> unsafe_judgment -> typed_type
-val assumption_of_judgment : unsafe_env -> unsafe_judgment -> typed_type
+val typed_type_of_judgment :
+ unsafe_env -> 'a evar_map -> unsafe_judgment -> typed_type
+val assumption_of_judgment :
+ unsafe_env -> 'a evar_map -> unsafe_judgment -> typed_type
val relative : unsafe_env -> int -> unsafe_judgment
-val type_of_constant : unsafe_env -> constr -> typed_type
+val type_of_constant : unsafe_env -> 'a evar_map -> constr -> typed_type
-val type_of_inductive : unsafe_env -> constr -> typed_type
+val type_of_inductive : unsafe_env -> 'a evar_map -> constr -> typed_type
-val type_of_constructor : unsafe_env -> constr -> constr
+val type_of_constructor : unsafe_env -> 'a evar_map -> constr -> constr
-val type_of_case : unsafe_env -> unsafe_judgment -> unsafe_judgment
- -> unsafe_judgment array -> unsafe_judgment
+val type_of_case : unsafe_env -> 'a evar_map
+ -> unsafe_judgment -> unsafe_judgment
+ -> unsafe_judgment array -> unsafe_judgment
val type_case_branches :
- unsafe_env -> constr -> constr -> constr -> constr
+ unsafe_env -> 'a evar_map -> constr -> constr -> constr -> constr
-> constr * constr array * constr
val type_of_prop_or_set : contents -> unsafe_judgment
@@ -42,22 +46,23 @@ val type_of_prop_or_set : contents -> unsafe_judgment
val type_of_type : universe -> unsafe_judgment * constraints
val abs_rel :
- unsafe_env -> name -> typed_type -> unsafe_judgment
+ unsafe_env -> 'a evar_map -> name -> typed_type -> unsafe_judgment
-> unsafe_judgment * constraints
val gen_rel :
- unsafe_env -> name -> typed_type -> unsafe_judgment
+ unsafe_env -> 'a evar_map -> name -> typed_type -> unsafe_judgment
-> unsafe_judgment * constraints
val cast_rel :
- unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+ unsafe_env -> 'a evar_map -> unsafe_judgment -> unsafe_judgment
+ -> unsafe_judgment
val apply_rel_list :
- unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment
+ unsafe_env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
-> unsafe_judgment * constraints
-val check_fix : unsafe_env -> Spset.t -> constr -> unit
-val check_cofix : unsafe_env -> Spset.t -> constr -> unit
+val check_fix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
+val check_cofix : unsafe_env -> 'a evar_map -> Spset.t -> constr -> unit
-val type_fixpoint : unsafe_env -> name list -> typed_type array
+val type_fixpoint : unsafe_env -> 'a evar_map -> name list -> typed_type array
-> unsafe_judgment array -> constraints
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 071403d628..8a18c1e2b5 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -58,13 +58,13 @@ let rec execute mf env cstr =
error "Cannot typecheck an unevaluable abstraction"
| IsConst _ ->
- (make_judge cstr (type_of_constant env cstr), cst0)
+ (make_judge cstr (type_of_constant env Evd.empty cstr), cst0)
| IsMutInd _ ->
- (make_judge cstr (type_of_inductive env cstr), cst0)
+ (make_judge cstr (type_of_inductive env Evd.empty cstr), cst0)
| IsMutConstruct _ ->
- let (typ,kind) = destCast (type_of_constructor env cstr) in
+ let (typ,kind) = destCast (type_of_constructor env Evd.empty cstr) in
({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0)
| IsMutCase (_,p,c,lf) ->
@@ -72,20 +72,20 @@ let rec execute mf env cstr =
let (pj,cst2) = execute mf env p in
let (lfj,cst3) = execute_array mf env lf in
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
- (type_of_case env pj cj lfj, cst)
+ (type_of_case env Evd.empty pj cj lfj, cst)
| IsFix (vn,i,lar,lfi,vdef) ->
if (not mf.fix) && array_exists (fun n -> n < 0) vn then
error "General Fixpoints not allowed";
let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
let fix = mkFix vn i larv lfi vdefv in
- check_fix env Spset.empty fix;
+ check_fix env Evd.empty Spset.empty fix;
(make_judge fix larv.(i), cst)
| IsCoFix (i,lar,lfi,vdef) ->
let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in
let cofix = mkCoFix i larv lfi vdefv in
- check_cofix env Spset.empty cofix;
+ check_cofix env Evd.empty Spset.empty cofix;
(make_judge cofix larv.(i), cst)
| IsSort (Prop c) ->
@@ -101,25 +101,25 @@ let rec execute mf env cstr =
and tl = Array.to_list (Array.sub a 1 (la - 1)) in
let (j,cst1) = execute mf env hd in
let (jl,cst2) = execute_list mf env tl in
- let (j,cst3) = apply_rel_list env mf.nocheck jl j in
+ let (j,cst3) = apply_rel_list env Evd.empty mf.nocheck jl j in
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
(j, cst)
| IsLambda (name,c1,c2) ->
let (j,cst1) = execute mf env c1 in
- let var = assumption_of_judgment env j in
+ let var = assumption_of_judgment env Evd.empty j in
let env1 = push_rel (name,var) env in
let (j',cst2) = execute mf env1 c2 in
- let (j,cst3) = abs_rel env1 name var j' in
+ let (j,cst3) = abs_rel env1 Evd.empty name var j' in
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
(j, cst)
| IsProd (name,c1,c2) ->
let (j,cst1) = execute mf env c1 in
- let var = assumption_of_judgment env j in
+ let var = assumption_of_judgment env Evd.empty j in
let env1 = push_rel (name,var) env in
let (j',cst2) = execute mf env1 c2 in
- let (j,cst3) = gen_rel env1 name var j' in
+ let (j,cst3) = gen_rel env1 Evd.empty name var j' in
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
(j, cst)
@@ -127,20 +127,20 @@ let rec execute mf env cstr =
let (cj,cst1) = execute mf env c in
let (tj,cst2) = execute mf env t in
let cst = Constraint.union cst1 cst2 in
- (cast_rel env cj tj, cst)
+ (cast_rel env Evd.empty cj tj, cst)
| _ -> error_cant_execute CCI env cstr
and execute_fix mf env lar lfi vdef =
let (larj,cst1) = execute_array mf env lar in
- let lara = Array.map (assumption_of_judgment env) larj in
+ let lara = Array.map (assumption_of_judgment env Evd.empty) larj in
let nlara =
List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
let env1 =
List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
let (vdefj,cst2) = execute_array mf env1 vdef in
let vdefv = Array.map j_val_only vdefj in
- let cst3 = type_fixpoint env1 lfi lara vdefj in
+ let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
(lara,vdefv,cst)
@@ -161,7 +161,7 @@ and execute_list mf env = function
let execute_type mf env constr =
let (j,_) = execute mf env constr in
- assumption_of_judgment env j
+ assumption_of_judgment env Evd.empty j
(* Exported machines. First safe machines, with no general fixpoint
@@ -200,13 +200,13 @@ let unsafe_machine_type env constr =
(* ``Type of'' machines. *)
let type_of env c =
- let (j,_) = safe_machine env c in nf_betaiota env j.uj_type
+ let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type
let type_of_type env c =
let tt = safe_machine_type env c in DOP0 (Sort tt.typ)
let unsafe_type_of env c =
- let (j,_) = unsafe_machine env c in nf_betaiota env j.uj_type
+ let (j,_) = unsafe_machine env c in nf_betaiota env Evd.empty j.uj_type
let unsafe_type_of_type env c =
let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
@@ -250,7 +250,7 @@ let lookup_mind_specif = lookup_mind_specif
let push_rel_or_var push (id,c) env =
let (j,cst) = safe_machine env c in
let env' = add_constraints cst env in
- let var = assumption_of_judgment env' j in
+ let var = assumption_of_judgment env' Evd.empty j in
push (id,var) env'
let push_var nvar env = push_rel_or_var push_var nvar env
@@ -271,14 +271,15 @@ let add_constant sp ce env =
let (env'',ty,cst') =
match ce.const_entry_type with
| None ->
- env', typed_type_of_judgment env' jb, Constraint.empty
+ env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty
| Some ty ->
let (jt,cst') = safe_machine env ty in
let env'' = add_constraints cst' env' in
try
- let cst'' = conv env'' jb.uj_type jt.uj_val in
+ let cst'' = conv env'' Evd.empty jb.uj_type jt.uj_val in
let env'' = add_constraints cst'' env'' in
- env'', assumption_of_judgment env'' jt, Constraint.union cst' cst''
+ (env'', assumption_of_judgment env'' Evd.empty jt,
+ Constraint.union cst' cst'')
with NotConvertible ->
error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
in
@@ -298,7 +299,7 @@ let add_parameter sp t env =
let cb = {
const_kind = kind_of_path sp;
const_body = None;
- const_type = assumption_of_judgment env' jt;
+ const_type = assumption_of_judgment env' Evd.empty jt;
const_hyps = get_globals (context env);
const_constraints = cst;
const_opaque = false }
@@ -312,7 +313,7 @@ let add_parameter sp t env =
function taking a value of type [typed_type] as argument. *)
let rec for_all_prods p env c =
- match whd_betadeltaiota env c with
+ match whd_betadeltaiota env Evd.empty c with
| DOP2(Prod, DOP2(Cast,t,DOP0 (Sort s)), DLAM(name,c)) ->
(p (make_typed t s)) &&
(let ty = { body = t; typ = s } in
@@ -320,7 +321,7 @@ let rec for_all_prods p env c =
for_all_prods p env' c)
| DOP2(Prod, b, DLAM(name,c)) ->
let (jb,cst) = unsafe_machine env b in
- let var = assumption_of_judgment env jb in
+ let var = assumption_of_judgment env Evd.empty jb in
(p var) &&
(let env' = Environ.push_rel (name,var) (add_constraints cst env) in
for_all_prods p env' c)
@@ -329,7 +330,7 @@ let rec for_all_prods p env c =
let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c
let enforce_type_constructor env univ j cst =
- match whd_betadeltaiota env j.uj_type with
+ match whd_betadeltaiota env Evd.empty j.uj_type with
| DOP0 (Sort (Type uc)) ->
Constraint.add (univ,Geq,uc) cst
| _ -> error "Type of Constructor not well-formed"
@@ -347,11 +348,13 @@ let type_one_constructor env_ar nparams ar c =
((issmall,j), Constraint.union cst' cst'')
let logic_constr env c =
- for_all_prods (fun t -> not (is_info_type env t)) env c
+ for_all_prods (fun t -> not (is_info_type env Evd.empty t)) env c
let logic_arity env c =
for_all_prods
- (fun t -> (not (is_info_type env t)) or (is_small_type env t.body)) env c
+ (fun t ->
+ (not (is_info_type env Evd.empty t)) or (is_small_type env t.body))
+ env c
let is_unit env_par nparams ar spec =
match decomp_all_DLAMV_name spec with
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 03:36:13 +0000