aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml208
1 files changed, 113 insertions, 95 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 27144b279f..a042b73c28 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -27,12 +27,14 @@ open Util
open Names
open Evd
open Term
-open Vars
open Termops
-open Reductionops
open Environ
+open EConstr
+open Vars
+open Reductionops
open Type_errors
open Typeops
+open Typing
open Globnames
open Nameops
open Evarutil
@@ -59,7 +61,7 @@ type ltac_var_map = {
ltac_genargs : unbound_ltac_var_map;
}
type glob_constr_ltac_closure = ltac_var_map * glob_constr
-type pure_open_constr = evar_map * constr
+type pure_open_constr = evar_map * EConstr.constr
(************************************************************************)
(* This concerns Cases *)
@@ -77,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
- (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env)
+ 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
@@ -115,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
@@ -127,6 +129,10 @@ open ExtraEnv
exception Found of int array
+let nf_fix sigma (nas, cs, ts) =
+ let inj c = EConstr.to_constr sigma c in
+ (nas, Array.map inj cs, Array.map inj ts)
+
let search_guard loc env possible_indexes fixdefs =
(* Standard situation with only one possibility for each fix. *)
(* We treat it separately in order to get proper error msg. *)
@@ -304,7 +310,7 @@ let apply_inference_hook hook evdref frozen = match frozen with
then
try
let sigma, c = hook sigma evk in
- Evd.define evk c sigma
+ Evd.define evk (EConstr.Unsafe.to_constr c) sigma
with Exit ->
sigma
else
@@ -337,17 +343,15 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with
let check_evars env initial_sigma sigma c =
let rec proc_rec c =
- match kind_of_term c with
- | Evar (evk,_ as ev) ->
- (match existential_opt_value sigma ev with
- | Some c -> proc_rec c
- | None ->
- if not (Evd.mem initial_sigma evk) then
- let (loc,k) = evar_source evk sigma in
- match k with
- | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
- | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None)
- | _ -> Constr.iter proc_rec c
+ match EConstr.kind sigma c with
+ | Evar (evk, _) ->
+ if not (Evd.mem initial_sigma evk) then
+ let (loc,k) = evar_source evk sigma in
+ begin match k with
+ | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+ | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None
+ end
+ | _ -> EConstr.iter sigma proc_rec c
in proc_rec c
let check_evars_are_solved env current_sigma frozen =
@@ -411,7 +415,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
@@ -422,7 +426,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
@@ -446,7 +450,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
@@ -482,9 +486,6 @@ let pretype_id pretype k0 loc env evdref lvar id =
(* [id] not found, standard error message *)
error_var_not_found ~loc id
-let evar_kind_of_term sigma c =
- kind_of_term (whd_evar sigma c)
-
(*************************************************************************)
(* Main pretyping function *)
@@ -516,7 +517,8 @@ let pretype_global loc rigid env evd gr us =
str " universe instances must be greater or equal to Set.");
evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
in
- Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr
+ let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
+ (sigma, EConstr.of_constr c)
let pretype_ref loc evdref env ref us =
match ref with
@@ -531,7 +533,7 @@ let pretype_ref loc evdref env ref us =
| ref ->
let evd, c = pretype_global loc univ_flexible env !evdref ref us in
let () = evdref := evd in
- let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in
+ let ty = unsafe_type_of env.ExtraEnv.env evd c in
make_judge c ty
let judge_of_Type loc evd s =
@@ -591,7 +593,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
@@ -600,7 +602,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
@@ -609,7 +611,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
@@ -627,18 +629,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
@@ -654,23 +656,24 @@ 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 ->
(* we lift nbfix times the type in tycon, because of
* the nbfix variables pushed to newenv *)
let (ctxt,ty) =
- decompose_prod_n_assum (Context.Rel.length ctxt)
+ 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 })
ctxtv vdef in
Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj;
- let ftys = Array.map (nf_evar !evdref) ftys in
- let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
+ let nf c = nf_evar !evdref c in
+ let ftys = Array.map nf ftys in (** FIXME *)
+ let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in
let fixj = match fixkind with
| GFix (vn,i) ->
(* First, let's find the guard indexes. *)
@@ -689,12 +692,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let fixdecls = (names,ftys,fdefs) in
let indexes =
search_guard
- loc env.ExtraEnv.env possible_indexes fixdecls
+ loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls)
in
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i ->
- let cofix = (i,(names,ftys,fdefs)) in
- (try check_cofix env.ExtraEnv.env cofix
+ let fixdecls = (names,ftys,fdefs) in
+ let cofix = (i, fixdecls) in
+ (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls)
with reraise ->
let (e, info) = CErrors.push reraise in
let info = Loc.add_loc info loc in
@@ -715,24 +719,24 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
(* Bidirectional typechecking hint:
parameters of a constructor are completely determined
by a typing constraint *)
- if Flags.is_program_mode () && length > 0 && isConstruct fj.uj_val then
+ if Flags.is_program_mode () && length > 0 && isConstruct !evdref fj.uj_val then
match tycon with
| None -> []
| Some ty ->
- let ((ind, i), u) = destConstruct fj.uj_val in
+ let ((ind, i), u) = destConstruct !evdref fj.uj_val in
let npars = inductive_nparams ind in
if Int.equal npars 0 then []
else
try
let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in
let ((ind',u'),pars) = dest_ind_family indf in
- if eq_ind ind ind' then pars
+ if eq_ind ind ind' then List.map EConstr.of_constr pars
else (* Let the usual code throw an error *) []
with Not_found -> []
else []
in
let app_f =
- match kind_of_term fj.uj_val with
+ match EConstr.kind !evdref fj.uj_val with
| Const (p, u) when Environ.is_projection p env.ExtraEnv.env ->
let p = Projection.make p false in
let pb = Environ.lookup_projection p env.ExtraEnv.env in
@@ -748,7 +752,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let argloc = loc_of_glob_constr c in
let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in
let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in
- match kind_of_term resty with
+ match EConstr.kind !evdref resty with
| Prod (na,c1,c2) ->
let tycon = Some c1 in
let hj = pretype tycon env evdref lvar c in
@@ -768,18 +772,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let hj = pretype empty_tycon env evdref lvar c in
error_cant_apply_not_functional
~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref
- resj [hj]
+ resj [|hj|]
in
let resj = apply_rec env 1 fj candargs args in
let resj =
- match evar_kind_of_term !evdref resj.uj_val with
+ match EConstr.kind !evdref resj.uj_val with
| App (f,args) ->
- let f = whd_evar !evdref f in
- if is_template_polymorphic env.ExtraEnv.env f then
+ if is_template_polymorphic env.ExtraEnv.env !evdref f then
(* Special case for inductive type applications that must be
refreshed right away. *)
- let sigma = !evdref in
- let c = mkApp (f,Array.map (whd_evar sigma) args) in
+ let c = mkApp (f, args) in
let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in
let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in
make_judge c (* use this for keeping evars: resj.uj_val *) t
@@ -805,7 +807,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
@@ -821,7 +823,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
@@ -850,7 +852,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 }
@@ -872,6 +874,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
user_err ~loc:loc (str "Destructing let on this type expects " ++
int cs.cs_nargs ++ str " variables.");
let fsign, record =
+ let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in
match get_projections env.ExtraEnv.env indf with
| None ->
List.map2 set_name (List.rev nal) cs.cs_args, false
@@ -879,6 +882,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let rec aux n k names l =
match names, l with
| na :: names, (LocalAssum (_,t) :: l) ->
+ let t = EConstr.of_constr t in
let proj = Projection.make ps.(cs.cs_nargs - k) true in
LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t)
:: aux (n+1) (k + 1) names l
@@ -897,7 +901,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
@@ -906,17 +910,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
else arsgn
in
let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
+ let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
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 = make_arity_signature env.ExtraEnv.env !evdref true indf in (* with names *)
let p = it_mkLambda_or_LetIn ccl psign in
let inst =
- (Array.to_list cs.cs_concl_realargs)
- @[build_dependent_constructor cs] in
+ (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs)
+ @[EConstr.of_constr (build_dependent_constructor cs)] in
let lp = lift cs.cs_nargs p in
let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in
let fj = pretype (mk_tycon fty) env_f evdref lvar d in
@@ -925,14 +930,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
obj ind p cj.uj_val fj.uj_val
in
- { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+ { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) }
| None ->
let tycon = lift_tycon cs.cs_nargs tycon in
let fj = pretype tycon env_f evdref lvar d in
let ccl = nf_evar !evdref fj.uj_type in
let ccl =
- if noccur_between 1 cs.cs_nargs ccl then
+ if noccur_between !evdref 1 cs.cs_nargs ccl then
lift (- cs.cs_nargs) ccl
else
error_cant_find_case_type ~loc env.ExtraEnv.env !evdref
@@ -966,19 +971,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
in
let nar = List.length arsgn in
let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in
+ 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
- let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
+ let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in
pred, typ
| None ->
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
@@ -987,18 +993,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let f cs b =
let n = Context.Rel.length cs.cs_args in
let pi = lift n pred in (* liftn n 2 pred ? *)
- let pi = beta_applist (pi, [build_dependent_constructor cs]) in
+ let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
+ let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
let csgn =
if not !allow_anonymous_refs then
- List.map (set_name Anonymous) cs.cs_args
+ List.map (set_name Anonymous) cs_args
else
List.map (map_name (function Name _ as n -> n
| Anonymous -> Name Namegen.default_non_dependent_ident))
- cs.cs_args
+ 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.cs_args in
+ it_mkLambda_or_LetIn bj.uj_val cs_args in
let b1 = f cstrs.(0) b1 in
let b2 = f cstrs.(1) b2 in
let v =
@@ -1013,7 +1020,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) ->
@@ -1033,7 +1040,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| VMcast ->
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
- if not (occur_existential cty || occur_existential tval) then
+ if not (occur_existential !evdref cty || occur_existential !evdref tval) then
let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
if b then (evdref := evd; cj, tval)
else
@@ -1061,7 +1068,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
let f decl (subst,update) =
let id = NamedDecl.get_id decl in
- let t = replace_vars subst (NamedDecl.get_type decl) in
+ let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in
let c, update =
try
let c = List.assoc id update in
@@ -1087,13 +1094,22 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
| GHole (loc, knd, naming, None) ->
+ let rec is_Type c = match EConstr.kind !evdref c with
+ | Sort s ->
+ begin match ESorts.kind !evdref s with
+ | Type _ -> true
+ | Prop _ -> false
+ end
+ | Cast (c, _, _) -> is_Type c
+ | _ -> false
+ in
(match valcon with
| Some v ->
let s =
let sigma = !evdref in
let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
- match kind_of_term (whd_all env.ExtraEnv.env sigma t) with
- | Sort s -> s
+ match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
+ | Sort s -> ESorts.kind sigma s
| Evar ev when is_Type (existential_type sigma ev) ->
evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
| _ -> anomaly (Pp.str "Found a type constraint which is not a type")
@@ -1101,7 +1117,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})
@@ -1118,7 +1134,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
@@ -1155,33 +1171,33 @@ let empty_lvar : ltac_var_map = {
ltac_genargs = Id.Map.empty;
}
-let on_judgment f j =
+let on_judgment sigma f j =
let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
- let (c,_,t) = destCast (f c) in
+ let (c,_,t) = destCast sigma (f c) in
{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
- let j = on_judgment (fun c ->
+ let j = on_judgment sigma (fun c ->
let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in
evdref := evd; c) j
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 (fun c ->
+ on_judgment !evdref (fun c ->
let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in
evdref := evd; c) j
let ise_pretype_gen_ctx flags env sigma lvar kind c =
let evd, c = ise_pretype_gen flags env sigma lvar kind c in
let evd, f = Evarutil.nf_evars_and_universes evd in
- f c, Evd.evar_universe_context evd
+ f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd
(** Entry points of the high-level type synthesis algorithm *)
@@ -1192,7 +1208,8 @@ let understand
ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c
let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c =
- ise_pretype_gen flags env sigma empty_lvar expected_type c
+ let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in
+ (sigma, c)
let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c =
let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in
@@ -1200,7 +1217,8 @@ let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=W
c
let understand_ltac flags env sigma lvar kind c =
- ise_pretype_gen flags env sigma lvar kind c
+ let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in
+ (sigma, c)
let constr_flags = {
use_typeclasses = true;
@@ -1226,7 +1244,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 17:12:48 +0000