aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml15
-rw-r--r--pretyping/detyping.ml104
-rw-r--r--pretyping/detyping.mli7
-rw-r--r--pretyping/evardefine.ml2
-rw-r--r--pretyping/indrec.ml20
-rw-r--r--pretyping/inductiveops.ml32
-rw-r--r--pretyping/inductiveops.mli6
-rw-r--r--pretyping/pretyping.ml75
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/typing.ml3
-rw-r--r--pretyping/unification.ml5
11 files changed, 143 insertions, 128 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a5a5fe6d2..490bc2801 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -708,7 +708,7 @@ let merge_name get_name obj = function
let merge_names get_name = List.map2 (merge_name get_name)
-let get_names env sign eqns =
+let get_names env sigma sign eqns =
let names1 = List.make (Context.Rel.length sign) Anonymous in
(* If any, we prefer names used in pats, from top to bottom *)
let names2,aliasname =
@@ -727,7 +727,7 @@ let get_names env sign eqns =
(fun (l,avoid) d na ->
let na =
merge_name
- (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env (EConstr.Unsafe.to_constr t) na) avoid))
+ (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid))
d na
in
(na::l,(out_name na)::avoid))
@@ -924,7 +924,7 @@ let rec extract_predicate ccl = function
ccl
let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
- let sign = make_arity_signature env true indf in
+ let sign = make_arity_signature env sigma true indf in
(* n is the number of real args + 1 (+ possible let-ins in sign) *)
let n = List.length sign in
(* Before abstracting we generalize over cur and on those realargs *)
@@ -945,7 +945,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
let pred = extract_predicate ccl tms in
(* Build the predicate properly speaking *)
let sign = List.map2 set_name (na::names) sign in
- EConstr.of_constr (it_mkLambda_or_LetIn_name env (EConstr.Unsafe.to_constr pred) sign)
+ it_mkLambda_or_LetIn_name env sigma pred sign
(* [expand_arg] is used by [specialize_predicate]
if Yk denotes [Xk;xk] or [Xk],
@@ -1238,7 +1238,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
(* that had matched constructor C *)
let cs_args = const_info.cs_args in
let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs_args in
- let names,aliasname = get_names pb.env cs_args eqns in
+ let names,aliasname = get_names pb.env !(pb.evdref) cs_args eqns in
let typs = List.map2 RelDecl.set_name names cs_args
in
@@ -1714,7 +1714,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
let build_inversion_problem loc env sigma tms t =
let make_patvar t (subst,avoid) =
- let id = next_name_away (named_hd env (EConstr.Unsafe.to_constr t) Anonymous) avoid in
+ let id = next_name_away (named_hd env sigma t Anonymous) avoid in
PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in
let rec reveal_pattern t (subst,avoid as acc) =
match EConstr.kind sigma (whd_all env sigma t) with
@@ -1733,8 +1733,7 @@ let build_inversion_problem loc env sigma tms t =
let patl,acc = List.fold_map' reveal_pattern realargs acc in
let pat,acc = make_patvar t acc in
let indf' = lift_inductive_family n indf in
- let sign = make_arity_signature env true indf' in
- let sign = List.map (fun d -> map_rel_decl EConstr.of_constr d) sign in
+ let sign = make_arity_signature env sigma true indf' in
let patl = pat :: List.rev patl in
let patl,sign = recover_and_adjust_alias_names patl sign in
let p = List.length patl in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c8d945c0b..1adda14ab 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,14 +6,17 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+module CVars = Vars
+
open Pp
open CErrors
open Util
open Names
open Term
+open Environ
+open EConstr
open Vars
open Inductiveops
-open Environ
open Glob_term
open Glob_ops
open Termops
@@ -188,7 +191,7 @@ let _ = declare_bool_option
(* Auxiliary function for MutCase printing *)
(* [computable] tries to tell if the predicate typing the result is inferable*)
-let computable p k =
+let computable sigma p k =
(* We first remove as many lambda as the arity, then we look
if it remains a lambda for a dependent elimination. This function
works for normal eta-expanded term. For non eta-expanded or
@@ -205,31 +208,29 @@ let computable p k =
sinon on perd la réciprocité de la synthèse (qui, lui,
engendrera un prédicat non dépendant) *)
- let sign,ccl = decompose_lam_assum p in
+ let sign,ccl = decompose_lam_assum sigma p in
Int.equal (Context.Rel.length sign) (k + 1)
&&
- noccur_between 1 (k+1) ccl
+ noccur_between sigma 1 (k+1) ccl
-let pop t = Vars.lift (-1) t
-
-let lookup_name_as_displayed env t s =
- let rec lookup avoid n c = match kind_of_term c with
+let lookup_name_as_displayed env sigma t s =
+ let rec lookup avoid n c = match EConstr.kind sigma c with
| Prod (name,_,c') ->
- (match compute_displayed_name_in RenamingForGoal avoid name c' with
+ (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with
| (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
| (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
| LetIn (name,_,_,c') ->
- (match compute_displayed_name_in RenamingForGoal avoid name c' with
+ (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with
| (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
| (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
| Cast (c,_,_) -> lookup avoid n c
| _ -> None
in lookup (ids_of_named_context (named_context env)) 1 t
-let lookup_index_as_renamed env t n =
- let rec lookup n d c = match kind_of_term c with
+let lookup_index_as_renamed env sigma t n =
+ let rec lookup n d c = match EConstr.kind sigma c with
| Prod (name,_,c') ->
- (match compute_displayed_name_in RenamingForGoal [] name c' with
+ (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
(Name _,_) -> lookup n (d+1) c'
| (Anonymous,_) ->
if Int.equal n 0 then
@@ -239,7 +240,7 @@ let lookup_index_as_renamed env t n =
else
lookup (n-1) (d+1) c')
| LetIn (name,_,_,c') ->
- (match compute_displayed_name_in RenamingForGoal [] name c' with
+ (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
| (Name _,_) -> lookup n (d+1) c'
| (Anonymous,_) ->
if Int.equal n 0 then
@@ -256,9 +257,9 @@ let lookup_index_as_renamed env t n =
(**********************************************************************)
(* Fragile algorithm to reverse pattern-matching compilation *)
-let update_name na ((_,(e,_)),c) =
+let update_name sigma na ((_,(e,_)),c) =
match na with
- | Name _ when force_wildcard () && noccurn (List.index Name.equal na e) c ->
+ | Name _ when force_wildcard () && noccurn sigma (List.index Name.equal na e) c ->
Anonymous
| _ ->
na
@@ -269,7 +270,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
| [] -> (List.rev nal,(e,c))
| b::tags ->
let na,c,f,body,t =
- match kind_of_term (EConstr.Unsafe.to_constr (strip_outer_cast sigma (EConstr.of_constr c))), b with
+ match EConstr.kind sigma (strip_outer_cast sigma c), b with
| Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t
| LetIn (na,b,t,c),true ->
na,c,compute_displayed_name_in,Some b,Some t
@@ -279,12 +280,12 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
| _, true ->
Anonymous,lift 1 c,compute_displayed_name_in,None,None
in
- let na',avoid' = f flag avoid na c in
+ let na',avoid' = f sigma flag avoid na c in
decomp_branch tags (na'::nal) b
(avoid', add_name_opt na' body t env) sigma c
let rec build_tree na isgoal e sigma ci cl =
- let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
+ let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name sigma na rhs) in
let cnl = ci.ci_pp_info.cstr_tags in
let cna = ci.ci_cstr_nargs in
List.flatten
@@ -294,12 +295,12 @@ let rec build_tree na isgoal e sigma ci cl =
and align_tree nal isgoal (e,c as rhs) sigma = match nal with
| [] -> [[],rhs]
| na::nal ->
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Case (ci,p,c,cl) when
- eq_constr sigma (EConstr.of_constr c) (EConstr.mkRel (List.index Name.equal na (fst (snd e))))
+ eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e))))
&& not (Int.equal (Array.length cl) 0)
&& (* don't contract if p dependent *)
- computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
+ computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
let clauses = build_tree na isgoal e sigma ci cl in
List.flatten
(List.map (fun (pat,rhs) ->
@@ -307,7 +308,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
List.map (fun (hd,rest) -> pat::hd,rest) lines)
clauses)
| _ ->
- let pat = PatVar(dl,update_name na rhs) in
+ let pat = PatVar(dl,update_name sigma na rhs) in
let mat = align_tree nal isgoal rhs sigma in
List.map (fun (hd,rest) -> pat::hd,rest) mat
@@ -320,11 +321,11 @@ and contract_branch isgoal e sigma (cdn,can,mkpat,b) =
(* Transform internal representation of pattern-matching into list of *)
(* clauses *)
-let is_nondep_branch c l =
+let is_nondep_branch sigma c l =
try
(* FIXME: do better using tags from l *)
- let sign,ccl = decompose_lam_n_decls (List.length l) c in
- noccur_between 1 (Context.Rel.length sign) ccl
+ let sign,ccl = decompose_lam_n_decls sigma (List.length l) c in
+ noccur_between sigma 1 (Context.Rel.length sign) ccl
with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *)
false
@@ -441,7 +442,7 @@ let detype_instance sigma l =
else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
let rec detype flags avoid env sigma t =
- match kind_of_term (EConstr.Unsafe.to_constr (collapse_appl sigma (EConstr.of_constr t))) with
+ match EConstr.kind sigma (collapse_appl sigma t) with
| Rel n ->
(try match lookup_name_of_rel n (fst env) with
| Name id -> GVar (dl, id)
@@ -503,11 +504,11 @@ let rec detype flags avoid env sigma t =
try
let pb = Environ.lookup_projection p (snd env) in
let body = pb.Declarations.proj_body in
- let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in
+ let ty = Retyping.get_type_of (snd env) sigma c in
let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
- let args = List.map EConstr.Unsafe.to_constr args in
let body' = strip_lam_assum body in
- let body' = subst_instance_constr u body' in
+ let body' = CVars.subst_instance_constr u body' in
+ let body' = EConstr.of_constr body' in
substl (c :: List.rev args) body'
with Retyping.RetypeError _ | Not_found ->
anomaly (str"Cannot detype an unfolded primitive projection.")
@@ -515,8 +516,7 @@ let rec detype flags avoid env sigma t =
else
if print_primproj_params () then
try
- let c = Retyping.expand_projection (snd env) sigma p (EConstr.of_constr c) [] in
- let c = EConstr.Unsafe.to_constr c in
+ let c = Retyping.expand_projection (snd env) sigma p c [] in
detype flags avoid env sigma c
with Retyping.RetypeError _ -> noparams ()
else noparams ()
@@ -527,8 +527,8 @@ let rec detype flags avoid env sigma t =
| LocalDef _ -> true
| LocalAssum (id,_) ->
try let n = List.index Name.equal (Name id) (fst env) in
- isRelN n c
- with Not_found -> isVarId id c
+ isRelN sigma n c
+ with Not_found -> isVarId sigma id c
in
let id,l =
try
@@ -537,8 +537,8 @@ let rec detype flags avoid env sigma t =
| Some id -> id
in
let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
- let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
- let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
+ let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match EConstr.kind sigma c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
+ let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in
id,l
with Not_found ->
Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
@@ -551,10 +551,10 @@ let rec detype flags avoid env sigma t =
| Construct (cstr_sp,u) ->
GRef (dl, ConstructRef cstr_sp, detype_instance sigma u)
| Case (ci,p,c,bl) ->
- let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in
+ let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
detype_case comp (detype flags avoid env sigma)
(detype_eqns flags avoid env sigma ci comp)
- is_nondep_branch avoid
+ (is_nondep_branch sigma) avoid
(ci.ci_ind,ci.ci_pp_info.style,
ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
(Some p) c bl
@@ -594,7 +594,7 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) =
Array.map (fun (_,bd,_) -> bd) v)
and share_names flags n l avoid env sigma c t =
- match kind_of_term c, kind_of_term t with
+ match EConstr.kind sigma c, EConstr.kind sigma t with
(* factorize even when not necessary to have better presentation *)
| Lambda (na,t,c), Prod (na',t',c') ->
let na = match (na,na') with
@@ -641,15 +641,15 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
let make_pat x avoid env b body ty ids =
- if force_wildcard () && noccurn 1 b then
+ if force_wildcard () && noccurn sigma 1 b then
PatVar (dl,Anonymous),avoid,(add_name Anonymous body ty env),ids
else
let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
- let na,avoid' = compute_displayed_name_in flag avoid x b in
+ let na,avoid' = compute_displayed_name_in sigma flag avoid x b in
PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na
in
let rec buildrec ids patlist avoid env l b =
- match kind_of_term b, l with
+ match EConstr.kind sigma b, l with
| _, [] ->
(dl, Id.Set.elements ids,
[PatCstr(dl, constr, List.rev patlist,Anonymous)],
@@ -684,8 +684,8 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in
let na',avoid' = match bk with
- | BLetIn -> compute_displayed_let_name_in flag avoid na c
- | _ -> compute_displayed_name_in flag avoid na c in
+ | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c
+ | _ -> compute_displayed_name_in sigma flag avoid na c in
let r = detype flags avoid' (add_name na' body ty env) sigma c in
match bk with
| BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
@@ -693,13 +693,13 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
| BLetIn ->
let c = detype (lax,false) avoid env sigma (Option.get body) in
(* Heuristic: we display the type if in Prop *)
- let s = try Retyping.get_sort_family_of (snd env) sigma (EConstr.of_constr ty) with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
+ let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
let c = if s != InProp then c else
GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in
GLetIn (dl, na', c, r)
let detype_rel_context ?(lax=false) where avoid env sigma sign =
- let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
+ let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
let rec aux avoid env = function
| [] -> []
| decl::rest ->
@@ -711,10 +711,10 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign =
| None -> na,avoid
| Some c ->
if is_local_def decl then
- compute_displayed_let_name_in
+ compute_displayed_let_name_in sigma
(RenamingElsewhereFor (fst env,c)) avoid na c
else
- compute_displayed_name_in
+ compute_displayed_name_in sigma
(RenamingElsewhereFor (fst env,c)) avoid na c in
let b = match decl with
| LocalAssum _ -> None
@@ -731,6 +731,7 @@ let detype ?(lax=false) isgoal avoid env sigma t =
detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t
let detype_closed_glob ?lax isgoal avoid env sigma t =
+ let open Context.Rel.Declaration in
let convert_id cl id =
try Id.Map.find id cl.idents
with Not_found -> id
@@ -748,12 +749,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
with Not_found -> try
(* assumes [detype] does not raise [Not_found] exceptions *)
let (b,c) = Id.Map.find id cl.typed in
- let c = EConstr.Unsafe.to_constr c in
(* spiwack: I'm not sure it is the right thing to do,
but I'm computing the detyping environment like
[Printer.pr_constr_under_binders_env] does. *)
- let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) b in
- let env = Termops.push_rels_assum assums env in
+ let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in
+ let env = push_rel_context assums env in
detype ?lax isgoal avoid env sigma c
(* if [id] is bound to a [closed_glob_constr]. *)
with Not_found -> try
@@ -808,7 +808,7 @@ let rec subst_glob_constr subst raw =
| GRef (loc,ref,u) ->
let ref',t = subst_global subst ref in
if ref' == ref then raw else
- detype false [] (Global.env()) Evd.empty t
+ detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)
| GVar _ -> raw
| GEvar _ -> raw
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index c51cb0f44..4c6f9129f 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -9,6 +9,7 @@
open Names
open Term
open Environ
+open EConstr
open Glob_term
open Termops
open Mod_subst
@@ -45,13 +46,13 @@ val detype_case :
val detype_sort : evar_map -> sorts -> glob_sort
val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) ->
- evar_map -> Context.Rel.t -> glob_decl list
+ evar_map -> rel_context -> glob_decl list
val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr
(** look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_displayed : env -> constr -> Id.t -> int option
-val lookup_index_as_renamed : env -> constr -> int -> int option
+val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option
+val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit
val force_wildcard : unit -> bool
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index faf34baf7..20d86f81b 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -140,7 +140,7 @@ let define_pure_evar_as_lambda env evd evk =
| _ -> error_not_product env evd typ in
let avoid = ids_of_named_context (evar_context evi) in
let id =
- next_name_away_with_default_using_types "x" na avoid (EConstr.Unsafe.to_constr (Reductionops.whd_evar evd dom)) in
+ next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
let newenv = push_named (LocalAssum (id, dom)) evenv in
let filter = Filter.extend 1 (evar_filter evi) in
let src = evar_source evk evd1 in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 431d1ff16..c4a74d990 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -40,6 +40,18 @@ type recursion_scheme_error =
exception RecursionSchemeError of recursion_scheme_error
+let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na
+let name_assumption env = function
+| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t)
+| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t)
+
+let mkLambda_or_LetIn_name env d b = mkLambda_or_LetIn (name_assumption env d) b
+let mkProd_or_LetIn_name env d b = mkProd_or_LetIn (name_assumption env d) b
+let mkLambda_name env (n,a,b) = mkLambda_or_LetIn_name env (LocalAssum (n,a)) b
+let mkProd_name env (n,a,b) = mkProd_or_LetIn_name env (LocalAssum (n,a)) b
+let it_mkProd_or_LetIn_name env b l = List.fold_left (fun c d -> mkProd_or_LetIn_name env d c) b l
+let it_mkLambda_or_LetIn_name env b l = List.fold_left (fun c d -> mkLambda_or_LetIn_name env d c) b l
+
let make_prod_dep dep env = if dep then mkProd_name env else mkProd
let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
@@ -118,12 +130,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
it_mkLambda_or_LetIn_name env' obj deparsign
else
let cs = lift_constructor (k+1) constrs.(k) in
- let t = build_branch_type env dep (mkRel (k+1)) cs in
+ let t = build_branch_type env (Sigma.to_evar_map sigma) dep (mkRel (k+1)) cs in
mkLambda_string "f" t
(add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1))
in
let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
- let typP = make_arity env' dep indf s in
+ let typP = make_arity env' (Sigma.to_evar_map sigma) dep indf s in
+ let typP = EConstr.Unsafe.to_constr typP in
let c =
it_mkLambda_or_LetIn_name env
(mkLambda_string "P" typP
@@ -443,7 +456,8 @@ let mis_make_indrec env sigma listdepkind mib u =
Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env)
evdref kinds
in
- let typP = make_arity env dep indf s in
+ let typP = make_arity env !evdref dep indf s in
+ let typP = EConstr.Unsafe.to_constr typP in
mkLambda_string "P" typP
(put_arity (push_rel (LocalAssum (Anonymous,typP)) env) (i+1) rest)
| [] ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3191a58ff..9e823ab4c 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -422,26 +422,29 @@ let build_dependent_inductive env ((ind, params) as indf) =
(* builds the arity of an elimination predicate in sort [s] *)
-let make_arity_signature env dep indf =
+let make_arity_signature env sigma dep indf =
let (arsign,_) = get_arity env indf in
+ let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
if dep then
(* We need names everywhere *)
- Namegen.name_context env
- ((LocalAssum (Anonymous,build_dependent_inductive env indf))::arsign)
+ Namegen.name_context env sigma
+ ((LocalAssum (Anonymous,EConstr.of_constr (build_dependent_inductive env indf)))::arsign)
(* Costly: would be better to name once for all at definition time *)
else
(* No need to enforce names *)
arsign
-let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s)
+let make_arity env sigma dep indf s =
+ let open EConstr in
+ it_mkProd_or_LetIn (mkSort s) (make_arity_signature env sigma dep indf)
(* [p] is the predicate and [cs] a constructor summary *)
-let build_branch_type env dep p cs =
+let build_branch_type env sigma dep p cs =
let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
if dep then
- Namegen.it_mkProd_or_LetIn_name env
- (applist (base,[build_dependent_constructor cs]))
- cs.cs_args
+ EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma
+ (EConstr.of_constr (applist (base,[build_dependent_constructor cs])))
+ (List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) cs.cs_args))
else
Term.it_mkProd_or_LetIn base cs.cs_args
@@ -542,11 +545,12 @@ let is_elim_predicate_explicitly_dependent env sigma pred indf =
let arsign,_ = get_arity env indf in
is_predicate_explicitly_dep env sigma pred arsign
-let set_names env n brty =
- let (ctxt,cl) = decompose_prod_n_assum n brty in
- Namegen.it_mkProd_or_LetIn_name env cl ctxt
+let set_names env sigma n brty =
+ let open EConstr in
+ let (ctxt,cl) = decompose_prod_n_assum sigma n brty in
+ EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt)
-let set_pattern_names env ind brv =
+let set_pattern_names env sigma ind brv =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let arities =
Array.map
@@ -554,7 +558,7 @@ let set_pattern_names env ind brv =
Context.Rel.length ((prod_assum c)) -
mib.mind_nparams)
mip.mind_nf_lc in
- Array.map2 (set_names env) arities brv
+ Array.map2 (set_names env sigma) arities brv
let type_case_branches_with_names env sigma indspec p c =
let (ind,args) = indspec in
@@ -567,7 +571,7 @@ let type_case_branches_with_names env sigma indspec p c =
let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
(* Adjust names *)
if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then
- (set_pattern_names env (fst ind) lbrty, conclty)
+ (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty)
else (lbrty, conclty)
(* Type of Case predicates *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 4bb484759..ab470a540 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -156,9 +156,9 @@ val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family
val build_dependent_constructor : constructor_summary -> constr
val build_dependent_inductive : env -> inductive_family -> constr
-val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t
-val make_arity : env -> bool -> inductive_family -> sorts -> types
-val build_branch_type : env -> bool -> constr -> constructor_summary -> types
+val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context
+val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types
+val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types
(** Raise [Not_found] if not given a valid inductive type *)
val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2470decdd..563769df5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -79,26 +79,26 @@ type t = {
(** Delay the computation of the evar extended environment *)
}
-let get_extra env =
+let get_extra env sigma =
let open Context.Named.Declaration in
let ids = List.map get_id (named_context env) in
let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
- Context.Rel.fold_outside push_rel_decl_to_named_context
+ Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
(rel_context env) ~init:(empty_csubst, [], avoid, named_context env)
-let make_env env = { env = env; extra = lazy (get_extra env) }
+let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) }
let rel_context env = rel_context env.env
-let push_rel d env = {
+let push_rel sigma d env = {
env = push_rel d env.env;
- extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra));
+ extra = lazy (push_rel_decl_to_named_context sigma d (Lazy.force env.extra));
}
-let pop_rel_context n env = make_env (pop_rel_context n env.env)
+let pop_rel_context n env sigma = make_env (pop_rel_context n env.env) sigma
-let push_rel_context ctx env = {
+let push_rel_context sigma ctx env = {
env = push_rel_context ctx env.env;
- extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra));
+ extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx (Lazy.force env.extra));
}
let lookup_named id env = lookup_named id env.env
@@ -117,9 +117,9 @@ let e_new_evar env evdref ?src ?naming typ =
evdref := Sigma.to_evar_map sigma;
e
-let push_rec_types (lna,typarray,_) env =
+let push_rec_types sigma (lna,typarray,_) env =
let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
- Array.fold_left (fun e assum -> push_rel assum e) env ctxt
+ Array.fold_left (fun e assum -> push_rel sigma assum e) env ctxt
end
@@ -391,7 +391,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
str"It cannot be used in a binder.")
else n
-let ltac_interp_name_env k0 lvar env =
+let ltac_interp_name_env k0 lvar env sigma =
(* envhd is the initial part of the env when pretype was called first *)
(* (in practice is is probably 0, but we have to grant the
specification of pretype which accepts to start with a non empty
@@ -402,7 +402,7 @@ let ltac_interp_name_env k0 lvar env =
let open Context.Rel.Declaration in
let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in
if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
- else push_rel_context ctxt' (pop_rel_context n env)
+ else push_rel_context sigma ctxt' (pop_rel_context n env sigma)
let invert_ltac_bound_name lvar env id0 id =
let id' = Id.Map.find id lvar.ltac_idents in
@@ -426,7 +426,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
let (n,_,typ) = lookup_rel_id id (rel_context env) in
{ uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
- let env = ltac_interp_name_env k0 lvar env in
+ let env = ltac_interp_name_env k0 lvar env !evdref in
(* Check if [id] is an ltac variable *)
try
let (ids,c) = Id.Map.find id lvar.ltac_constrs in
@@ -569,7 +569,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
inh_conv_coerce_to_tycon loc env evdref j tycon
| GPatVar (loc,(someta,n)) ->
- let env = ltac_interp_name_env k0 lvar env in
+ let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
@@ -578,7 +578,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (loc, k, naming, None) ->
- let env = ltac_interp_name_env k0 lvar env in
+ let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
@@ -587,7 +587,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
| GHole (loc, k, _naming, Some arg) ->
- let env = ltac_interp_name_env k0 lvar env in
+ let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
@@ -605,18 +605,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let ty' = pretype_type empty_valcon env evdref lvar ty in
let dcl = LocalAssum (na, ty'.utj_val) in
let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in
- type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl
+ type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl
| (na,bk,Some bd,ty)::bl ->
let ty' = pretype_type empty_valcon env evdref lvar ty in
let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in
- type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in
+ type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl in
let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
let larj =
Array.map2
(fun e ar ->
- pretype_type empty_valcon (push_rel_context e env) evdref lvar ar)
+ pretype_type empty_valcon (push_rel_context !evdref e env) evdref lvar ar)
ctxtv lar in
let lara = Array.map (fun a -> a.utj_val) larj in
let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -632,7 +632,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| None -> true
in
(* Note: bodies are not used by push_rec_types, so [||] is safe *)
- let newenv = push_rec_types (names,ftys,[||]) env in
+ let newenv = push_rec_types !evdref (names,ftys,[||]) env in
let vdefj =
Array.map2_i
(fun i ctxt def ->
@@ -641,7 +641,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let (ctxt,ty) =
decompose_prod_n_assum !evdref (Context.Rel.length ctxt)
(lift nbfix ftys.(i)) in
- let nenv = push_rel_context ctxt newenv in
+ let nenv = push_rel_context !evdref ctxt newenv in
let j = pretype (mk_tycon ty) nenv evdref lvar def in
{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
@@ -783,7 +783,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
the substitution must also be applied on variables before they are
looked up in the rel context. *)
let var = LocalAssum (name, j.utj_val) in
- let j' = pretype rng (push_rel var env) evdref lvar c2 in
+ let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in
let name = ltac_interp_name lvar name in
let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in
inh_conv_coerce_to_tycon loc env evdref resj tycon
@@ -799,7 +799,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ j with utj_val = lift 1 j.utj_val }
| Name _ ->
let var = LocalAssum (name, j.utj_val) in
- let env' = push_rel var env in
+ let env' = push_rel !evdref var env in
pretype_type empty_valcon env' evdref lvar c2
in
let name = ltac_interp_name lvar name in
@@ -828,7 +828,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
looked up in the rel context. *)
let var = LocalDef (name, j.uj_val, t) in
let tycon = lift_tycon 1 tycon in
- let j' = pretype tycon (push_rel var env) evdref lvar c2 in
+ let j' = pretype tycon (push_rel !evdref var env) evdref lvar c2 in
let name = ltac_interp_name lvar name in
{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
@@ -877,7 +877,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
mkCase (ci, p, cj.uj_val,[|f|])
else it_mkLambda_or_LetIn f fsign
in
- let env_f = push_rel_context fsign env in
+ let env_f = push_rel_context !evdref fsign env in
(* Make dependencies from arity signature impossible *)
let arsgn =
let arsgn,_ = get_arity env.ExtraEnv.env indf in
@@ -890,11 +890,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let nar = List.length arsgn in
(match po with
| Some p ->
- let env_p = push_rel_context psign env in
+ let env_p = push_rel_context !evdref psign env in
let pj = pretype_type empty_valcon env_p evdref lvar p in
let ccl = nf_evar !evdref pj.utj_val in
- let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *)
- let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
+ let psign = make_arity_signature env.ExtraEnv.env !evdref true indf in (* with names *)
let p = it_mkLambda_or_LetIn ccl psign in
let inst =
(Array.map_to_list EConstr.of_constr cs.cs_concl_realargs)
@@ -951,7 +950,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
let pred,p = match po with
| Some p ->
- let env_p = push_rel_context psign env in
+ let env_p = push_rel_context !evdref psign env in
let pj = pretype_type empty_valcon env_p evdref lvar p in
let ccl = nf_evar !evdref pj.utj_val in
let pred = it_mkLambda_or_LetIn ccl psign in
@@ -961,7 +960,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let p = match tycon with
| Some ty -> ty
| None ->
- let env = ltac_interp_name_env k0 lvar env in
+ let env = ltac_interp_name_env k0 lvar env !evdref in
new_type_evar env evdref loc
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
@@ -980,7 +979,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| Anonymous -> Name Namegen.default_non_dependent_ident))
cs_args
in
- let env_c = push_rel_context csgn env in
+ let env_c = push_rel_context !evdref csgn env in
let bj = pretype (mk_tycon pi) env_c evdref lvar b in
it_mkLambda_or_LetIn bj.uj_val cs_args in
let b1 = f cstrs.(0) b1 in
@@ -997,7 +996,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| GCases (loc,sty,po,tml,eqns) ->
Cases.compile_cases loc sty
- ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref)
+ ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref)
tycon env.ExtraEnv.env (* loc *) (po,tml,eqns)
| GCast (loc,c,k) ->
@@ -1090,7 +1089,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
{ utj_val = v;
utj_type = s }
| None ->
- let env = ltac_interp_name_env k0 lvar env in
+ let env = ltac_interp_name_env k0 lvar env !evdref in
let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
{ utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
utj_type = s})
@@ -1107,7 +1106,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
let ise_pretype_gen flags env sigma lvar kind c =
- let env = make_env env in
+ let env = make_env env sigma in
let evdref = ref sigma in
let k0 = Context.Rel.length (rel_context env) in
let c' = match kind with
@@ -1150,7 +1149,7 @@ let on_judgment sigma f j =
{uj_val = c; uj_type = t}
let understand_judgment env sigma c =
- let env = make_env env in
+ let env = make_env env sigma in
let evdref = ref sigma in
let k0 = Context.Rel.length (rel_context env) in
let j = pretype k0 true empty_tycon env evdref empty_lvar c in
@@ -1160,7 +1159,7 @@ let understand_judgment env sigma c =
in j, Evd.evar_universe_context !evdref
let understand_judgment_tcc env evdref c =
- let env = make_env env in
+ let env = make_env env !evdref in
let k0 = Context.Rel.length (rel_context env) in
let j = pretype k0 true empty_tycon env evdref empty_lvar c in
on_judgment !evdref (fun c ->
@@ -1217,7 +1216,7 @@ let type_uconstr ?(flags = constr_flags)
end }
let pretype k0 resolve_tc typcon env evdref lvar t =
- pretype k0 resolve_tc typcon (make_env env) evdref lvar t
+ pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t
let pretype_type k0 resolve_tc valcon env evdref lvar t =
- pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t
+ pretype_type k0 resolve_tc valcon (make_env env !evdref) evdref lvar t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9f3f3c7e5..ef9f39d77 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1141,7 +1141,7 @@ let compute = cbv_betadeltaiota
let abstract_scheme env sigma (locc,a) (c, sigma) =
let ta = Retyping.get_type_of env sigma a in
- let na = named_hd env (EConstr.to_constr sigma ta) Anonymous in
+ let na = named_hd env sigma ta Anonymous in
if occur_meta sigma ta then error "Cannot find a type for the generalisation.";
if occur_meta sigma a then
mkLambda (na,ta,c), sigma
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bdd3663d1..dec22ecd0 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -92,8 +92,7 @@ let max_sort l =
if Sorts.List.mem InSet l then InSet else InProp
let e_is_correct_arity env evdref c pj ind specif params =
- let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
- let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
+ let arsign = make_arity_signature env !evdref true (make_ind_family (ind,params)) in
let allowed_sorts = elim_sorts specif in
let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
let rec srec env pt ar =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 589201fe2..baa12db08 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -85,7 +85,7 @@ let occur_meta_evd sigma mv c =
let abstract_scheme env evd c l lname_typ =
let mkLambda_name env (n,a,b) =
- mkLambda (named_hd env (EConstr.Unsafe.to_constr a) n, a, b)
+ mkLambda (named_hd env evd a n, a, b)
in
List.fold_left2
(fun (t,evd) (locc,a) decl ->
@@ -1617,8 +1617,7 @@ let make_eq_test env evd c =
let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let id =
let t = match ty with Some t -> t | None -> get_type_of env sigma c in
- let t = EConstr.Unsafe.to_constr t in
- let x = id_of_name_using_hdchar (Global.env()) t name in
+ let x = id_of_name_using_hdchar (Global.env()) sigma t name in
let ids = ids_of_named_context (named_context env) in
if name == Anonymous then next_ident_away_in_goal x ids else
if mem_named_context_val x (named_context_val env) then
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 11:48:12 +0000