aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml57
-rw-r--r--pretyping/cases.mli6
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/coercion.ml60
-rw-r--r--pretyping/coercion.mli9
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/pretype_errors.ml24
-rw-r--r--pretyping/pretype_errors.mli41
-rw-r--r--pretyping/pretyping.ml157
-rw-r--r--pretyping/pretyping.mli12
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/typing.ml191
-rw-r--r--pretyping/typing.mli10
-rw-r--r--pretyping/unification.ml8
16 files changed, 348 insertions, 239 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 92bd1e389..b43e2193a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -89,9 +89,6 @@ let list_try_compile f l =
let force_name =
let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
-let make_judge c ty =
- make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
-
(************************************************************************)
(* Pattern-matching compilation (Cases) *)
(************************************************************************)
@@ -265,7 +262,7 @@ type 'a pattern_matching_problem =
mat : 'a matrix;
caseloc : Loc.t;
casestyle : case_style;
- typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
+ typing_function: type_constraint -> env -> evar_map ref -> 'a option -> EConstr.unsafe_judgment }
(*--------------------------------------------------------------------------*
* A few functions to infer the inductive type from the patterns instead of *
@@ -366,12 +363,12 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
let j = typing_fun tycon env evdref tomatch in
let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in
evdref := evd;
- let typ = EConstr.of_constr (nf_evar !evdref j.uj_type) in
+ let typ = EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr j.uj_type)) in
let t =
try try_find_ind env !evdref typ realnames
with Not_found ->
unify_tomatch_with_patterns evdref env loc typ pats realnames in
- (EConstr.of_constr j.uj_val,t)
+ (j.uj_val,t)
let coerce_to_indtype typing_fun evdref env matx tomatchl =
let pats = List.map (fun r -> r.patterns) matx in
@@ -415,7 +412,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
let _ = e_cumul pb.env pb.evdref indt typ in
current
else
- EConstr.of_constr (evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env)
+ (evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env)
pb.evdref (make_judge current typ) indt).uj_val in
let sigma = !(pb.evdref) in
(current,try_find_ind pb.env sigma indt names))
@@ -1002,7 +999,7 @@ let adjust_impossible_cases pb pred tomatch submat =
| Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
if not (Evd.is_defined !(pb.evdref) evk) then begin
let evd, default = use_unit_judge !(pb.evdref) in
- pb.evdref := Evd.define evk default.uj_type evd
+ pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd
end;
add_assert_false_case pb tomatch
| _ ->
@@ -1411,8 +1408,8 @@ and match_current pb (initial,tomatch) =
make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
in
Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
- { uj_val = EConstr.Unsafe.to_constr (applist (case, inst));
- uj_type = EConstr.Unsafe.to_constr (prod_applist !(pb.evdref) typ inst) }
+ { uj_val = applist (case, inst);
+ uj_type = prod_applist !(pb.evdref) typ inst }
(* Building the sub-problem when all patterns are variables. Case
@@ -1429,8 +1426,8 @@ and shift_problem ((current,t),_,na) pb =
history = pop_history pb.history;
mat = List.map (push_current_pattern (current,ty)) pb.mat } in
let j = compile pb in
- { uj_val = EConstr.Unsafe.to_constr (subst1 current (EConstr.of_constr j.uj_val));
- uj_type = EConstr.Unsafe.to_constr (subst1 current (EConstr.of_constr j.uj_type)) }
+ { uj_val = subst1 current j.uj_val;
+ uj_type = subst1 current j.uj_type }
(* Building the sub-problem when all patterns are variables,
non-initial case. Variables which appear as subterms of constructor
@@ -1453,7 +1450,7 @@ and compile_all_variables initial cur pb =
(* Building the sub-problem when all patterns are variables *)
and compile_branch initial current realargs names deps pb arsign eqns cstr =
let sign, pb = build_branch initial current realargs deps names pb arsign eqns cstr in
- sign, EConstr.of_constr (compile pb).uj_val
+ sign, (compile pb).uj_val
(* Abstract over a declaration before continuing splitting *)
and compile_generalization pb i d rest =
@@ -1463,8 +1460,8 @@ and compile_generalization pb i d rest =
tomatch = rest;
mat = List.map (push_generalized_decl_eqn pb.env i d) pb.mat } in
let j = compile pb in
- { uj_val = Term.mkLambda_or_LetIn d j.uj_val;
- uj_type = Term.mkProd_wo_LetIn d j.uj_type }
+ { uj_val = mkLambda_or_LetIn d j.uj_val;
+ uj_type = mkProd_wo_LetIn d j.uj_type }
(* spiwack: the [initial] argument keeps track whether the alias has
been introduced by a toplevel branch ([true]) or a deep one
@@ -1482,11 +1479,11 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
let j = compile pb in
let sigma = !(pb.evdref) in
{ uj_val =
- if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) (EConstr.of_constr j.uj_val) <= 1 then
- EConstr.Unsafe.to_constr (subst1 c (EConstr.of_constr j.uj_val))
+ if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
+ subst1 c j.uj_val
else
- EConstr.Unsafe.to_constr (mkLetIn (na,c,t,EConstr.of_constr j.uj_val));
- uj_type = EConstr.Unsafe.to_constr (subst1 c (EConstr.of_constr j.uj_type)) } in
+ mkLetIn (na,c,t,j.uj_val);
+ uj_type = subst1 c j.uj_type } in
(* spiwack: when an alias appears on a deep branch, its non-expanded
form is automatically a variable of the same name. We avoid
introducing such superfluous aliases so that refines are elegant. *)
@@ -1726,7 +1723,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
(t,tt) in
let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
if not b then anomaly (Pp.str "Build_tycon: should be a type");
- { uj_val = EConstr.Unsafe.to_constr t; uj_type = EConstr.Unsafe.to_constr tt }
+ { uj_val = t; uj_type = tt }
(* For a multiple pattern-matching problem Xi on t1..tn with return
* type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
@@ -1851,7 +1848,7 @@ let build_inversion_problem loc env sigma tms t =
caseloc = loc;
casestyle = RegularStyle;
typing_function = build_tycon loc env pb_env s subst} in
- let pred = EConstr.of_constr (compile pb).uj_val in
+ let pred = (compile pb).uj_val in
(!evdref,pred)
(* Here, [pred] is assumed to be in the context built from all *)
@@ -1905,7 +1902,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
let inh_conv_coerce_to_tycon loc env evdref j tycon =
match tycon with
| Some p ->
- let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j (EConstr.of_constr p) in
+ let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in
evdref := evd';
j
| None -> j
@@ -2029,7 +2026,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let evdref = ref sigma in
let predcclj = typing_fun (mk_tycon (EConstr.mkSort newt)) envar evdref rtntyp in
let sigma = !evdref in
- let predccl = EConstr.of_constr (j_nf_evar sigma predcclj).uj_val in
+ let predccl = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr predcclj.uj_val)) in
[sigma, predccl]
in
List.map
@@ -2095,7 +2092,7 @@ let constr_of_pat env evdref arsign pat avoid =
let IndType (indf, _) =
try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
with Not_found -> error_case_not_inductive env !evdref
- {uj_val = EConstr.Unsafe.to_constr ty; uj_type = Typing.unsafe_type_of env !evdref ty}
+ {uj_val = ty; uj_type = EConstr.of_constr (Typing.unsafe_type_of env !evdref ty)}
in
let (ind,u), params = dest_ind_family indf in
let params = List.map EConstr.of_constr params in
@@ -2297,8 +2294,8 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
in
let rhs_env = push_rel_context rhs_rels' env in
let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
- let bbody = it_mkLambda_or_LetIn (EConstr.of_constr j.uj_val) rhs_rels'
- and btype = it_mkProd_or_LetIn (EConstr.of_constr j.uj_type) rhs_rels' in
+ let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
+ and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
let branch_decl = local_def (Name branch_name, lift !i bbody, lift !i btype) in
@@ -2554,10 +2551,10 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
let j = compile pb in
(* We check for unused patterns *)
List.iter (check_unused_pattern env) matx;
- let body = it_mkLambda_or_LetIn (applist (EConstr.of_constr j.uj_val, args)) lets in
+ let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
let j =
- { uj_val = EConstr.Unsafe.to_constr (it_mkLambda_or_LetIn body tomatchs_lets);
- uj_type = EConstr.to_constr !evdref tycon; }
+ { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
+ uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); }
in j
(**************************************************************************)
@@ -2632,7 +2629,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
let j = compile pb in
(* We coerce to the tycon (if an elim predicate was provided) *)
- let j = inh_conv_coerce_to_tycon loc env myevdref j (Option.map EConstr.Unsafe.to_constr tycon) in
+ let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in
evdref := !myevdref;
j in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9016ca5f3..9f26ae9ce 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -8,9 +8,9 @@
open Names
open Term
-open EConstr
open Evd
open Environ
+open EConstr
open Inductiveops
open Glob_term
open Evarutil
@@ -111,11 +111,11 @@ type 'a pattern_matching_problem =
typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
-val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
+val compile : 'a pattern_matching_problem -> unsafe_judgment
val prepare_predicate : Loc.t ->
(Evarutil.type_constraint ->
- Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
+ Environ.env -> Evd.evar_map ref -> 'a -> unsafe_judgment) ->
Environ.env ->
Evd.evar_map ->
(types * tomatch_type) list ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ad43bf322..9011186a3 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -319,7 +319,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx;
let subst, ctx = Universes.fresh_universe_context_set_instance ctx in
let c' = Vars.subst_univs_level_constr subst c
and t' = Vars.subst_univs_level_constr subst t in
- (make_judge c' t', b, b'), ctx
+ (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx
(* pretty-print functions are now in Pretty *)
(* rajouter une coercion dans le graphe *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 9fb70534f..a1d030f12 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -8,9 +8,9 @@
open Names
open Term
+open Environ
open EConstr
open Evd
-open Environ
open Mod_subst
(** {6 This is the type of class kinds } *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index b9f14aa43..2d4296fe4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -53,16 +53,16 @@ let apply_coercion_args env evd check isproj argl funj =
let rec apply_rec acc typ = function
| [] ->
if isproj then
- let cst = fst (destConst !evdref (EConstr.of_constr (j_val funj))) in
+ let cst = fst (destConst !evdref (j_val funj)) in
let p = Projection.make cst false in
let pb = lookup_projection p env in
let args = List.skipn pb.Declarations.proj_npars argl in
let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
- { uj_val = EConstr.Unsafe.to_constr (applist (mkProj (p, hd), tl));
- uj_type = EConstr.Unsafe.to_constr typ }
+ { uj_val = applist (mkProj (p, hd), tl);
+ uj_type = typ }
else
- { uj_val = EConstr.Unsafe.to_constr (applist (EConstr.of_constr (j_val funj),argl));
- uj_type = EConstr.Unsafe.to_constr typ }
+ { uj_val = applist (j_val funj,argl);
+ uj_type = typ }
| h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
| Prod (_,c1,c2) ->
@@ -71,7 +71,7 @@ let apply_coercion_args env evd check isproj argl funj =
apply_rec (h::acc) (Vars.subst1 h c2) restl
| _ -> anomaly (Pp.str "apply_coercion_args")
in
- let res = apply_rec [] (EConstr.of_constr funj.uj_type) argl in
+ let res = apply_rec [] funj.uj_type argl in
!evdref, res
(* appliquer le chemin de coercions de patterns p *)
@@ -367,7 +367,7 @@ let apply_coercion env sigma p hj typ_cl =
(fun (ja,typ_cl,sigma) i ->
let ((fv,isid,isproj),ctx) = coercion_value i in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- let argl = (class_args_of env sigma typ_cl)@[EConstr.of_constr ja.uj_val] in
+ let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
let sigma, jres =
apply_coercion_args env sigma true isproj argl fv
in
@@ -375,7 +375,7 @@ let apply_coercion env sigma p hj typ_cl =
{ uj_val = ja.uj_val; uj_type = jres.uj_type }
else
jres),
- EConstr.of_constr jres.uj_type,sigma)
+ jres.uj_type,sigma)
(hj,typ_cl,sigma) p
in evd, j
with NoCoercion as e -> raise e
@@ -383,23 +383,23 @@ let apply_coercion env sigma p hj typ_cl =
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
- let t = whd_all env evd (EConstr.of_constr j.uj_type) in
+ let t = whd_all env evd j.uj_type in
let t = EConstr.of_constr t in
match EConstr.kind evd t with
| Prod (_,_,_) -> (evd,j)
| Evar ev ->
let (evd',t) = Evardefine.define_evar_as_product evd ev in
- (evd',{ uj_val = j.uj_val; uj_type = EConstr.Unsafe.to_constr t })
+ (evd',{ uj_val = j.uj_val; uj_type = t })
| _ ->
try let t,p =
- lookup_path_to_fun_from env evd (EConstr.of_constr j.uj_type) in
+ lookup_path_to_fun_from env evd j.uj_type in
apply_coercion env evd p j t
with Not_found | NoCoercion ->
if Flags.is_program_mode () then
try
let evdref = ref evd in
let coercef, t = mu env evdref t in
- let res = { uj_val = EConstr.Unsafe.to_constr (app_opt env evdref coercef (EConstr.of_constr j.uj_val)); uj_type = EConstr.Unsafe.to_constr t } in
+ let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
(!evdref, res)
with NoSubtacCoercion | NoCoercion ->
(evd,j)
@@ -415,17 +415,23 @@ let inh_app_fun resolve_tc env evd j =
try inh_app_fun_core env (saturate_evd env evd) j
with NoCoercion -> (evd, j)
+let type_judgment env sigma j =
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma j.uj_type)) with
+ | Sort s -> {utj_val = j.uj_val; utj_type = s }
+ | _ -> error_not_a_type env sigma j
+
let inh_tosort_force loc env evd j =
try
- let t,p = lookup_path_to_sort_from env evd (EConstr.of_constr j.uj_type) in
+ let t,p = lookup_path_to_sort_from env evd j.uj_type in
let evd,j1 = apply_coercion env evd p j t in
+ let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in
let j2 = on_judgment_type (whd_evar evd) j1 in
- (evd,type_judgment env j2)
+ (evd,type_judgment env evd j2)
with Not_found | NoCoercion ->
error_not_a_type ~loc env evd j
let inh_coerce_to_sort loc env evd j =
- let typ = whd_all env evd (EConstr.of_constr j.uj_type) in
+ let typ = whd_all env evd j.uj_type in
match EConstr.kind evd (EConstr.of_constr typ) with
| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
| Evar ev ->
@@ -437,10 +443,10 @@ let inh_coerce_to_sort loc env evd j =
let inh_coerce_to_base loc env evd j =
if Flags.is_program_mode () then
let evdref = ref evd in
- let ct, typ' = mu env evdref (EConstr.of_constr j.uj_type) in
+ let ct, typ' = mu env evdref j.uj_type in
let res =
- { uj_val = EConstr.Unsafe.to_constr (app_coercion env evdref ct (EConstr.of_constr j.uj_val));
- uj_type = EConstr.Unsafe.to_constr typ' }
+ { uj_val = (app_coercion env evdref ct j.uj_val);
+ uj_type = typ' }
in !evdref, res
else (evd, j)
@@ -463,8 +469,8 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
| Some v ->
let evd,j =
apply_coercion env evd p
- {uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr t} t2 in
- evd, Some (EConstr.of_constr j.uj_val), (EConstr.of_constr j.uj_type)
+ {uj_val = v; uj_type = t} t2 in
+ evd, Some j.uj_val, j.uj_type
| None -> evd, None, t
with Not_found -> raise NoCoercion
in
@@ -510,27 +516,27 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
let (evd', val') =
try
- inh_conv_coerce_to_fail loc env evd rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+ inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
with NoCoercionNoUnifier (best_failed_evd,e) ->
try
if Flags.is_program_mode () then
- coerce_itf loc env evd (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+ coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
else raise NoSubtacCoercion
with
| NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion ->
- error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+ error_actual_type ~loc env best_failed_evd cj t e
| NoSubtacCoercion ->
let evd' = saturate_evd env evd in
try
if evd' == evd then
- error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+ error_actual_type ~loc env best_failed_evd cj t e
else
- inh_conv_coerce_to_fail loc env evd' rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+ inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
with NoCoercionNoUnifier (_evd,_error) ->
- error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+ error_actual_type ~loc env best_failed_evd cj t e
in
let val' = match val' with Some v -> v | None -> assert(false) in
- (evd',{ uj_val = EConstr.Unsafe.to_constr val'; uj_type = EConstr.Unsafe.to_constr t })
+ (evd',{ uj_val = val'; uj_type = t })
let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false
let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 62d4fb004..bc63d092d 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -10,6 +10,7 @@ open Evd
open Names
open Term
open Environ
+open EConstr
open Glob_term
(** {6 Coercions. } *)
@@ -36,7 +37,7 @@ val inh_coerce_to_base : Loc.t ->
(** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
val inh_coerce_to_prod : Loc.t ->
- env -> evar_map -> EConstr.types -> evar_map * EConstr.types
+ env -> evar_map -> types -> evar_map * types
(** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an
object of type [t]; i.e. it inserts a coercion into [j], if needed, in such
@@ -44,16 +45,16 @@ val inh_coerce_to_prod : Loc.t ->
applicable. resolve_tc=false disables resolving type classes (as the last
resort before failing) *)
val inh_conv_coerce_to : bool -> Loc.t ->
- env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
val inh_conv_coerce_rigid_to : bool -> Loc.t ->
- env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
is coercible to an object of type [t'] adding evar constraints if needed;
it fails if no coercion exists *)
val inh_conv_coerces_to : Loc.t ->
- env -> evar_map -> EConstr.types -> EConstr.types -> evar_map
+ env -> evar_map -> types -> types -> evar_map
(** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3b420347b..639d6260e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1266,8 +1266,8 @@ let solve_unconstrained_impossible_cases env evd =
let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in
let ty = j_type j in
let conv_algo = evar_conv_x full_transparent_state in
- let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) conv_algo in
- Evd.define evk ty evd'
+ let evd' = check_evar_instance evd' evk ty conv_algo in
+ Evd.define evk (EConstr.Unsafe.to_constr ty) evd'
| _ -> evd') evd evd
let consider_remaining_unif_problems env
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 14b25ab36..673554005 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -31,11 +31,13 @@ type position_reporting = (position * int) * EConstr.t
type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
+type type_error = (EConstr.constr, EConstr.types) ptype_error
+
type pretype_error =
(* Old Case *)
- | CantFindCaseType of constr
+ | CantFindCaseType of EConstr.constr
(* Type inference unification *)
- | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+ | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
(* Tactic unification *)
| UnifOccurCheck of existential_key * EConstr.constr
| UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
@@ -50,7 +52,7 @@ type pretype_error =
| NonLinearUnification of Name.t * EConstr.constr
(* Pretyping *)
| VarNotFound of Id.t
- | UnexpectedType of constr * constr
+ | UnexpectedType of EConstr.constr * EConstr.constr
| NotProduct of EConstr.constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
@@ -75,14 +77,19 @@ let error_actual_type ?loc env sigma {uj_val=c;uj_type=actty} expty reason =
raise_pretype_error ?loc
(env, sigma, ActualTypeNotCoercible (j, expty, reason))
+let error_actual_type_core ?loc env sigma {uj_val=c;uj_type=actty} expty =
+ let j = {uj_val=c;uj_type=actty} in
+ raise_type_error ?loc
+ (env, sigma, ActualType (j, expty))
+
let error_cant_apply_not_functional ?loc env sigma rator randl =
raise_type_error ?loc
- (env, sigma, CantApplyNonFunctional (rator, Array.of_list randl))
+ (env, sigma, CantApplyNonFunctional (rator, randl))
let error_cant_apply_bad_type ?loc env sigma (n,c,t) rator randl =
raise_type_error ?loc
(env, sigma,
- CantApplyBadType ((n,c,t), rator, Array.of_list randl))
+ CantApplyBadType ((n,c,t), rator, randl))
let error_ill_formed_branch ?loc env sigma c i actty expty =
raise_type_error
@@ -98,9 +105,16 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys =
raise_type_error ?loc
(env, sigma, IllTypedRecBody (i, na, jl, tys))
+let error_elim_arity ?loc env sigma pi s c j a =
+ raise_type_error ?loc
+ (env, sigma, ElimArity (pi, s, c, j, a))
+
let error_not_a_type ?loc env sigma j =
raise_type_error ?loc (env, sigma, NotAType j)
+let error_assumption ?loc env sigma j =
+ raise_type_error ?loc (env, sigma, BadAssumption j)
+
(*s Implicit arguments synthesis errors. It is hard to find
a precise location. *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 2e707a0ff..0ebe4817c 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -32,11 +32,13 @@ type position_reporting = (position * int) * EConstr.t
type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
+type type_error = (EConstr.constr, EConstr.types) ptype_error
+
type pretype_error =
(** Old Case *)
- | CantFindCaseType of constr
+ | CantFindCaseType of EConstr.constr
(** Type inference unification *)
- | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+ | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
(** Tactic Unification *)
| UnifOccurCheck of existential_key * EConstr.constr
| UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
@@ -51,7 +53,7 @@ type pretype_error =
| NonLinearUnification of Name.t * EConstr.constr
(** Pretyping *)
| VarNotFound of Id.t
- | UnexpectedType of constr * constr
+ | UnexpectedType of EConstr.constr * EConstr.constr
| NotProduct of EConstr.constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
@@ -65,34 +67,45 @@ val precatchable_exception : exn -> bool
(** Raising errors *)
val error_actual_type :
- ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
+ ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr ->
unification_error -> 'b
+val error_actual_type_core :
+ ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b
+
val error_cant_apply_not_functional :
?loc:Loc.t -> env -> Evd.evar_map ->
- unsafe_judgment -> unsafe_judgment list -> 'b
+ EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
val error_cant_apply_bad_type :
- ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr ->
- unsafe_judgment -> unsafe_judgment list -> 'b
+ ?loc:Loc.t -> env -> Evd.evar_map -> int * EConstr.constr * EConstr.constr ->
+ EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
val error_case_not_inductive :
- ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+ ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
val error_ill_formed_branch :
?loc:Loc.t -> env -> Evd.evar_map ->
- constr -> pconstructor -> constr -> constr -> 'b
+ EConstr.constr -> pconstructor -> EConstr.constr -> EConstr.constr -> 'b
val error_number_branches :
?loc:Loc.t -> env -> Evd.evar_map ->
- unsafe_judgment -> int -> 'b
+ EConstr.unsafe_judgment -> int -> 'b
val error_ill_typed_rec_body :
?loc:Loc.t -> env -> Evd.evar_map ->
- int -> Name.t array -> unsafe_judgment array -> types array -> 'b
+ int -> Name.t array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b
+
+val error_elim_arity :
+ ?loc:Loc.t -> env -> Evd.evar_map ->
+ pinductive -> sorts_family list -> EConstr.constr ->
+ EConstr.unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b
val error_not_a_type :
- ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+ ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
+
+val error_assumption :
+ ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b
@@ -124,12 +137,12 @@ val error_non_linear_unification : env -> Evd.evar_map ->
(** {6 Ml Case errors } *)
val error_cant_find_case_type :
- ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
+ ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b
(** {6 Pretyping errors } *)
val error_unexpected_type :
- ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
+ ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'b
val error_not_product :
?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cac31a1c5..49a0bccee 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -34,6 +34,7 @@ open Reductionops
open Environ
open Type_errors
open Typeops
+open Typing
open Globnames
open Nameops
open Evarutil
@@ -124,7 +125,7 @@ let e_new_evar env evdref ?src ?naming typ =
let sigma = Sigma.Unsafe.of_evar_map !evdref in
let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in
evdref := Sigma.to_evar_map sigma;
- e
+ EConstr.of_constr e
let push_rec_types (lna,typarray,_) env =
let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in
@@ -425,21 +426,19 @@ let invert_ltac_bound_name lvar env id0 id =
str " which is not bound in current context.")
let protected_get_type_of env sigma c =
- try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
+ try EConstr.of_constr (Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c)
with Retyping.RetypeError _ ->
user_err
(str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++
str " in the current environment.")
-let j_val j = EConstr.of_constr (j_val j)
-
let pretype_id pretype k0 loc env evdref lvar id =
let sigma = !evdref in
(* Look for the binder of [id] *)
try
let (n,_,typ) = lookup_rel_id id (rel_context env) in
let typ = EConstr.of_constr typ in
- { uj_val = EConstr.Unsafe.to_constr (mkRel n); uj_type = EConstr.Unsafe.to_constr (lift n typ) }
+ { uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
let env = ltac_interp_name_env k0 lvar env in
(* Check if [id] is an ltac variable *)
@@ -447,7 +446,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
let (ids,c) = Id.Map.find id lvar.ltac_constrs in
let subst = List.map (invert_ltac_bound_name lvar env id) ids in
let c = substl subst (EConstr.of_constr c) in
- { uj_val = EConstr.Unsafe.to_constr c; uj_type = protected_get_type_of env sigma c }
+ { uj_val = c; uj_type = protected_get_type_of env sigma c }
with Not_found -> try
let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in
let lvar = {
@@ -472,7 +471,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
end;
(* Check if [id] is a section or goal variable *)
try
- { uj_val = Constr.mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) }
+ { uj_val = mkVar id; uj_type = EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) }
with Not_found ->
(* [id] not found, standard error message *)
error_var_not_found ~loc id
@@ -511,9 +510,6 @@ let pretype_global loc rigid env evd gr us =
let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
(sigma, EConstr.of_constr c)
-let make_judge c t =
- make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t)
-
let pretype_ref loc evdref env ref us =
match ref with
| VarRef id ->
@@ -527,14 +523,14 @@ 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
let ty = EConstr.of_constr ty in
make_judge c ty
let judge_of_Type loc evd s =
let evd, s = interp_universe ~loc evd s in
let judge =
- { uj_val = Constr.mkSort (Type s); uj_type = Constr.mkSort (Type (Univ.super s)) }
+ { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
in
evd, judge
@@ -550,7 +546,7 @@ let new_type_evar env evdref loc =
univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
in
evdref := Sigma.to_evar_map sigma;
- e
+ EConstr.of_constr e
let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
@@ -591,25 +587,25 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let env = ltac_interp_name_env k0 lvar env in
let ty =
match tycon with
- | Some ty -> EConstr.Unsafe.to_constr ty
+ | Some ty -> ty
| None -> new_type_evar env evdref loc in
let k = Evar_kinds.MatchingVar (someta,n) in
- { uj_val = e_new_evar env evdref ~src:(loc,k) (EConstr.of_constr ty); uj_type = ty }
+ { 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 ty =
match tycon with
- | Some ty -> EConstr.Unsafe.to_constr ty
+ | Some ty -> ty
| None ->
new_type_evar env evdref loc in
- { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming (EConstr.of_constr ty); uj_type = ty }
+ { 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 ty =
match tycon with
- | Some ty -> EConstr.Unsafe.to_constr ty
+ | Some ty -> ty
| None ->
new_type_evar env evdref loc in
let ist = lvar.ltac_genargs in
@@ -622,14 +618,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
[] -> ctxt
| (na,bk,None,ty)::bl ->
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
+ let dcl = local_assum (na, ty'.utj_val) in
+ let dcl' = local_assum (ltac_interp_name lvar na,ty'.utj_val) in
type_bl (push_rel 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 (EConstr.of_constr 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
+ let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
+ let dcl = local_def (na, bd'.uj_val, ty'.utj_val) in
+ let dcl' = local_def (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
let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
let larj =
@@ -637,8 +633,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
(fun e ar ->
pretype_type empty_valcon (push_rel_context e env) evdref lvar ar)
ctxtv lar in
- let lara = Array.map (fun a -> EConstr.of_constr a.utj_val) larj in
- let ftys = Array.map2 (fun e a -> EConstr.it_mkProd_or_LetIn a e) ctxtv lara 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
let nbfix = Array.length lar in
let names = Array.map (fun id -> Name id) names in
let _ =
@@ -662,8 +658,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
(lift nbfix ftys.(i)) in
let nenv = push_rel_context ctxt newenv in
let j = pretype (mk_tycon ty) nenv evdref lvar def in
- { uj_val = Termops.it_mkLambda_or_LetIn j.uj_val ctxt;
- uj_type = Termops.it_mkProd_or_LetIn j.uj_type ctxt })
+ { 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 nf c = nf_evar !evdref c in
@@ -714,11 +710,11 @@ 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 !evdref (EConstr.of_constr 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 !evdref (EConstr.of_constr 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
@@ -731,7 +727,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
else []
in
let app_f =
- match EConstr.kind !evdref (EConstr.of_constr 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
@@ -746,7 +742,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| c::rest ->
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 (EConstr.of_constr resj.uj_type) in
+ let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in
let resty = EConstr.of_constr resty in
match EConstr.kind !evdref resty with
| Prod (na,c1,c2) ->
@@ -761,18 +757,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
else [], j_val hj
in
let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
- let j = { uj_val = EConstr.Unsafe.to_constr value; uj_type = EConstr.Unsafe.to_constr typ } in
+ let j = { uj_val = value; uj_type = typ } in
apply_rec env (n+1) j candargs rest
| _ ->
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 EConstr.kind !evdref (EConstr.of_constr resj.uj_val) with
+ match EConstr.kind !evdref resj.uj_val with
| App (f,args) ->
if is_template_polymorphic env.ExtraEnv.env !evdref f then
(* Special case for inductive type applications that must be
@@ -804,7 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
(* The name specified by ltac is used also to create bindings. So
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 var = local_assum (name, j.utj_val) in
let j' = pretype rng (push_rel 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
@@ -818,9 +814,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j' = match name with
| Anonymous ->
let j = pretype_type empty_valcon env evdref lvar c2 in
- { j with utj_val = EConstr.Unsafe.to_constr (lift 1 (EConstr.of_constr j.utj_val)) }
+ { j with utj_val = lift 1 j.utj_val }
| Name _ ->
- let var = LocalAssum (name, j.utj_val) in
+ let var = local_assum (name, j.utj_val) in
let env' = push_rel var env in
pretype_type empty_valcon env' evdref lvar c2
in
@@ -839,27 +835,27 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
match c1 with
| GCast (loc, c, CastConv t) ->
let tj = pretype_type empty_valcon env evdref lvar t in
- pretype (mk_tycon (EConstr.of_constr tj.utj_val)) env evdref lvar c
+ pretype (mk_tycon tj.utj_val) env evdref lvar c
| _ -> pretype empty_tycon env evdref lvar c1
in
let t = evd_comb1 (Evarsolve.refresh_universes
~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
- evdref (EConstr.of_constr j.uj_type) in
+ evdref j.uj_type in
+ let t = EConstr.of_constr t in
(* The name specified by ltac is used also to create bindings. So
the substitution must also be applied on variables before they are
looked up in the rel context. *)
- let var = LocalDef (name, j.uj_val, t) in
- let t = EConstr.of_constr t in
+ let var = local_def (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 name = ltac_interp_name lvar name in
- { uj_val = EConstr.Unsafe.to_constr (mkLetIn (name, EConstr.of_constr j.uj_val, t, EConstr.of_constr j'.uj_val)) ;
- uj_type = EConstr.Unsafe.to_constr (subst1 (EConstr.of_constr j.uj_val) (EConstr.of_constr j'.uj_type)) }
+ { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
+ uj_type = subst1 j.uj_val j'.uj_type }
| GLetTuple (loc,nal,(na,po),c,d) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
- try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type)
+ try find_rectype env.ExtraEnv.env !evdref cj.uj_type
with Not_found ->
let cloc = loc_of_glob_constr c in
error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj
@@ -883,7 +879,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| na :: names, (LocalAssum (_,t) :: l) ->
let t = EConstr.of_constr t in
let proj = Projection.make ps.(cs.cs_nargs - k) true in
- local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, EConstr.of_constr cj.uj_val)), t)
+ local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t)
:: aux (n+1) (k + 1) names l
| na :: names, (decl :: l) ->
set_name na decl :: aux (n+1) k names l
@@ -897,7 +893,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let fsign = List.map2 set_name nal fsign in
let f = it_mkLambda_or_LetIn f fsign in
let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in
- mkCase (ci, p, EConstr.of_constr cj.uj_val,[|f|])
+ mkCase (ci, p, cj.uj_val,[|f|])
else it_mkLambda_or_LetIn f fsign
in
let env_f = push_rel_context fsign env in
@@ -914,7 +910,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| Some p ->
let env_p = push_rel_context psign env in
let pj = pretype_type empty_valcon env_p evdref lvar p in
- let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in
+ let ccl = nf_evar !evdref pj.utj_val in
let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *)
let p = it_mkLambda_or_LetIn ccl psign in
let inst =
@@ -922,18 +918,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
@[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 (EConstr.of_constr fty)) env_f evdref lvar d in
+ let fty = EConstr.of_constr fty in
+ let fj = pretype (mk_tycon fty) env_f evdref lvar d in
let v =
let ind,_ = dest_ind_family indf in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p;
- obj ind p cj.uj_val (EConstr.of_constr fj.uj_val)
+ 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 = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr (substl (realargs@[EConstr.of_constr 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 (EConstr.of_constr fj.uj_type) in
+ let ccl = nf_evar !evdref fj.uj_type in
let ccl =
if noccur_between !evdref 1 cs.cs_nargs ccl then
lift (- cs.cs_nargs) ccl
@@ -944,14 +941,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
let v =
let ind,_ = dest_ind_family indf in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p;
- obj ind p cj.uj_val (EConstr.of_constr fj.uj_val)
- in { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr ccl })
+ 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 = ccl })
| GIf (loc,c,(na,po),b1,b2) ->
let cj = pretype empty_tycon env evdref lvar c in
let (IndType (indf,realargs)) =
- try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type)
+ try find_rectype env.ExtraEnv.env !evdref cj.uj_type
with Not_found ->
let cloc = loc_of_glob_constr c in
error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in
@@ -973,16 +970,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| Some p ->
let env_p = push_rel_context psign env in
let pj = pretype_type empty_valcon env_p evdref lvar p in
- let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in
+ let ccl = nf_evar !evdref pj.utj_val in
let pred = it_mkLambda_or_LetIn ccl psign in
- let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[EConstr.of_constr cj.uj_val]))) in
+ let typ = lift (- nar) (EConstr.of_constr (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
- EConstr.of_constr (new_type_evar env evdref loc)
+ new_type_evar env evdref loc
in
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar !evdref pred in
@@ -991,6 +988,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let n = Context.Rel.length cs.cs_args in
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
+ let pi = EConstr.of_constr pi in
let csgn =
if not !allow_anonymous_refs then
List.map (set_name Anonymous) cs.cs_args
@@ -1000,18 +998,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
cs.cs_args
in
let env_c = push_rel_context csgn env in
- let bj = pretype (mk_tycon (EConstr.of_constr pi)) env_c evdref lvar b in
- it_mkLambda_or_LetIn (EConstr.of_constr bj.uj_val) cs.cs_args in
+ let bj = pretype (mk_tycon pi) env_c evdref lvar b in
+ it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
let b1 = f cstrs.(0) b1 in
let b2 = f cstrs.(1) b2 in
let v =
let ind,_ = dest_ind_family indf in
let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in
let pred = nf_evar !evdref pred in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) pred;
- mkCase (ci, pred, EConstr.of_constr cj.uj_val, [|b1;b2|])
+ Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred;
+ mkCase (ci, pred, cj.uj_val, [|b1;b2|])
in
- let cj = { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr p } in
+ let cj = { uj_val = v; uj_type = p } in
inh_conv_coerce_to_tycon loc env evdref cj tycon
| GCases (loc,sty,po,tml,eqns) ->
@@ -1030,36 +1028,36 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let tj = pretype_type empty_valcon env evdref lvar t in
let tval = evd_comb1 (Evarsolve.refresh_universes
~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
- evdref (EConstr.of_constr tj.utj_val) in
+ evdref tj.utj_val in
let tval = EConstr.of_constr tval in
let tval = nf_evar !evdref tval in
let cj, tval = match k with
| VMcast ->
let cj = pretype empty_tycon env evdref lvar c in
- let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in
+ let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
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
- error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval)
+ error_actual_type ~loc env.ExtraEnv.env !evdref cj tval
(ConversionFailed (env.ExtraEnv.env,cty,tval))
else user_err ~loc (str "Cannot check cast with vm: " ++
str "unresolved arguments remain.")
| NATIVEcast ->
let cj = pretype empty_tycon env evdref lvar c in
- let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in
+ let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
begin
let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
if b then (evdref := evd; cj, tval)
else
- error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval)
+ error_actual_type ~loc env.ExtraEnv.env !evdref cj tval
(ConversionFailed (env.ExtraEnv.env,cty,tval))
end
| _ ->
pretype (mk_tycon tval) env evdref lvar c, tval
in
- let v = mkCast (EConstr.of_constr cj.uj_val, k, tval) in
- { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr tval }
+ let v = mkCast (cj.uj_val, k, tval) in
+ { uj_val = v; uj_type = tval }
in inh_conv_coerce_to_tycon loc env evdref cj tycon
and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
@@ -1070,7 +1068,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
try
let c = List.assoc id update in
let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in
- EConstr.of_constr c.uj_val, List.remove_assoc id update
+ c.uj_val, List.remove_assoc id update
with Not_found ->
try
let (n,_,t') = lookup_rel_id id (rel_context env) in
@@ -1103,13 +1101,14 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
let s =
let sigma = !evdref in
let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
- match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t))) with
+ let t = EConstr.of_constr t in
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma t)) with
| Sort s -> 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")
in
- { utj_val = EConstr.Unsafe.to_constr v;
+ { utj_val = v;
utj_type = s }
| None ->
let env = ltac_interp_name_env k0 lvar env in
@@ -1123,10 +1122,10 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
match valcon with
| None -> tj
| Some v ->
- if e_cumul env.ExtraEnv.env evdref v (EConstr.of_constr tj.utj_val) then tj
+ if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
else
error_unexpected_type
- ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val (EConstr.Unsafe.to_constr v)
+ ~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
@@ -1140,7 +1139,7 @@ let ise_pretype_gen flags env sigma lvar kind c =
| IsType ->
(pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val
in
- process_inference_flags flags env.ExtraEnv.env sigma (!evdref,EConstr.of_constr c')
+ process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c')
let default_inference_flags fail = {
use_typeclasses = true;
@@ -1167,9 +1166,9 @@ let empty_lvar : ltac_var_map = {
}
let on_judgment sigma f j =
- let c = mkCast(EConstr.of_constr j.uj_val,DEFAULTcast, EConstr.of_constr j.uj_type) in
+ let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
let (c,_,t) = destCast sigma (f c) in
- {uj_val = EConstr.Unsafe.to_constr c; uj_type = EConstr.Unsafe.to_constr t}
+ {uj_val = c; uj_type = t}
let understand_judgment env sigma c =
let env = make_env env in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 603b9f9ea..2f3ce3afa 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -110,11 +110,11 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
(** Idem but returns the judgment of the understood term *)
val understand_judgment : env -> evar_map ->
- glob_constr -> unsafe_judgment Evd.in_evar_universe_context
+ glob_constr -> EConstr.unsafe_judgment Evd.in_evar_universe_context
(** Idem but do not fail on unresolved evars (type cl*)
val understand_judgment_tcc : env -> evar_map ref ->
- glob_constr -> unsafe_judgment
+ glob_constr -> EConstr.unsafe_judgment
val type_uconstr :
?flags:inference_flags ->
@@ -145,11 +145,11 @@ val check_evars : env -> evar_map -> evar_map -> EConstr.constr -> unit
(** Internal of Pretyping... *)
val pretype :
int -> bool -> type_constraint -> env -> evar_map ref ->
- ltac_var_map -> glob_constr -> unsafe_judgment
+ ltac_var_map -> glob_constr -> EConstr.unsafe_judgment
val pretype_type :
int -> bool -> val_constraint -> env -> evar_map ref ->
- ltac_var_map -> glob_constr -> unsafe_type_judgment
+ ltac_var_map -> glob_constr -> EConstr.unsafe_type_judgment
val ise_pretype_gen :
inference_flags -> env -> evar_map ->
@@ -163,5 +163,5 @@ val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
val interp_elimination_sort : glob_sort -> sorts_family
val genarg_interp_hook :
- (types -> env -> evar_map -> unbound_ltac_var_map ->
- Genarg.glob_generic_argument -> constr * evar_map) Hook.t
+ (EConstr.types -> env -> evar_map -> unbound_ltac_var_map ->
+ Genarg.glob_generic_argument -> EConstr.constr * evar_map) Hook.t
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 2efb02417..a7ccf98a6 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -244,7 +244,7 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
if lax then EConstr.Unsafe.to_constr (f env c) else EConstr.Unsafe.to_constr (anomaly_on_error (f env) c)
(* Makes an unsafe judgment from a constr *)
-let get_judgment_of env evc c = { uj_val = EConstr.Unsafe.to_constr c; uj_type = get_type_of env evc c }
+let get_judgment_of env evc c = { uj_val = c; uj_type = EConstr.of_constr (get_type_of env evc c) }
(* Returns sorts of a context *)
let sorts_of_context env evc ctxt =
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 08f750287..c84403890 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -35,7 +35,7 @@ val get_sort_family_of :
?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts_family
(** Makes an unsafe judgment from a constr *)
-val get_judgment_of : env -> evar_map -> EConstr.constr -> unsafe_judgment
+val get_judgment_of : env -> evar_map -> EConstr.constr -> EConstr.unsafe_judgment
val type_of_global_reference_knowing_parameters : env -> evar_map -> EConstr.constr ->
EConstr.constr array -> types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c948f9b9a..17adea5f2 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,20 +6,31 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+module CVars = Vars
+
open Pp
open CErrors
open Util
open Term
+open EConstr
open Vars
open Environ
open Reductionops
-open Type_errors
open Inductive
open Inductiveops
open Typeops
open Arguments_renaming
+open Pretype_errors
open Context.Rel.Declaration
+let local_assum (na, t) =
+ let inj = EConstr.Unsafe.to_constr in
+ LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+ let inj = EConstr.Unsafe.to_constr in
+ LocalDef (na, inj b, inj t)
+
let push_rec_types pfix env =
let (i, c, t) = pfix in
let inj c = EConstr.Unsafe.to_constr c in
@@ -31,57 +42,57 @@ let meta_type evd mv =
with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
meta_instance evd ty
-let constant_type_knowing_parameters env cst jl =
- let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
+let constant_type_knowing_parameters env sigma cst jl =
+ let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
-let inductive_type_knowing_parameters env (ind,u) jl =
+let inductive_type_knowing_parameters env sigma (ind,u) jl =
let mspec = lookup_mind_specif env ind in
- let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
+ let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
let e_type_judgment env evdref j =
- match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
+ match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref j.uj_type)) with
| Sort s -> {utj_val = j.uj_val; utj_type = s }
| Evar ev ->
let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
evdref := evd; { utj_val = j.uj_val; utj_type = s }
- | _ -> error_not_type env j
+ | _ -> error_not_a_type env !evdref j
let e_assumption_of_judgment env evdref j =
- try EConstr.of_constr (e_type_judgment env evdref j).utj_val
- with TypeError _ ->
- error_assumption env j
+ try (e_type_judgment env evdref j).utj_val
+ with Type_errors.TypeError _ | PretypeError _ ->
+ error_assumption env !evdref j
let e_judge_of_apply env evdref funj argjv =
let open EConstr in
let rec apply_rec n typ = function
| [] ->
- { uj_val = Constr.mkApp (j_val funj, Array.map j_val argjv);
- uj_type = EConstr.Unsafe.to_constr typ }
+ { uj_val = mkApp (j_val funj, Array.map j_val argjv);
+ uj_type = typ }
| hj::restjl ->
match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
| Prod (_,c1,c2) ->
- if Evarconv.e_cumul env evdref (EConstr.of_constr hj.uj_type) c1 then
- apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
+ if Evarconv.e_cumul env evdref hj.uj_type c1 then
+ apply_rec (n+1) (subst1 hj.uj_val c2) restjl
else
- error_cant_apply_bad_type env (n, EConstr.Unsafe.to_constr c1, hj.uj_type) funj argjv
+ error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
| Evar ev ->
let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
evdref := evd';
let (_,_,c2) = destProd evd' t in
- apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
+ apply_rec (n+1) (subst1 hj.uj_val c2) restjl
| _ ->
- error_cant_apply_not_functional env funj argjv
+ error_cant_apply_not_functional env !evdref funj argjv
in
- apply_rec 1 (EConstr.of_constr funj.uj_type) (Array.to_list argjv)
+ apply_rec 1 funj.uj_type (Array.to_list argjv)
let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
if not (Int.equal (Array.length lfj) (Array.length explft)) then
- error_number_branches env cj (Array.length explft);
+ error_number_branches env !evdref cj (Array.length explft);
for i = 0 to Array.length explft - 1 do
- if not (Evarconv.e_cumul env evdref (EConstr.of_constr lfj.(i).uj_type) (EConstr.of_constr explft.(i))) then
- error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
+ if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
+ error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
done
let max_sort l =
@@ -92,13 +103,13 @@ let e_is_correct_arity env evdref c pj ind specif params =
let open EConstr in
let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
let allowed_sorts = elim_sorts specif in
- let error () = error_elim_arity env ind allowed_sorts c pj None in
+ let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
let rec srec env pt ar =
let pt' = EConstr.of_constr (whd_all env !evdref pt) in
match EConstr.kind !evdref pt', ar with
| Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
- srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar'
+ srec (push_rel (local_assum (na1,a1)) env) t ar'
| Sort s, [] ->
if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
then error ()
@@ -106,27 +117,43 @@ let e_is_correct_arity env evdref c pj ind specif params =
let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
evdref := Evd.define ev (Constr.mkSort s) evd
| _, (LocalDef _ as d)::ar' ->
- srec (push_rel d env) (Vars.lift 1 pt') ar'
+ srec (push_rel d env) (lift 1 pt') ar'
| _ ->
error ()
in
- srec env (EConstr.of_constr pj.uj_type) (List.rev arsign)
+ srec env pj.uj_type (List.rev arsign)
+
+let lambda_applist_assum sigma n c l =
+ let open EConstr in
+ let rec app n subst t l =
+ if Int.equal n 0 then
+ if l == [] then substl subst t
+ else anomaly (Pp.str "Not enough arguments")
+ else match EConstr.kind sigma t, l with
+ | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+ | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+ app n [] c l
let e_type_case_branches env evdref (ind,largs) pj c =
let specif = lookup_mind_specif env (fst ind) in
let nparams = inductive_params specif in
let (params,realargs) = List.chop nparams largs in
let p = pj.uj_val in
+ let realargs = List.map EConstr.of_constr realargs in
let () = e_is_correct_arity env evdref c pj ind specif params in
- let lc = build_branches_type ind specif params p in
+ let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
+ let lc = Array.map EConstr.of_constr lc in
let n = (snd specif).Declarations.mind_nrealdecls in
- let ty = whd_betaiota !evdref (EConstr.of_constr (lambda_applist_assum (n+1) p (realargs@[c]))) in
+ let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
+ let ty = EConstr.of_constr ty in
(lc, ty)
let e_judge_of_case env evdref ci pj cj lfj =
+ let open EConstr in
let indspec =
- try find_mrectype env !evdref (EConstr.of_constr cj.uj_type)
- with Not_found -> error_case_not_inductive env cj in
+ try find_mrectype env !evdref cj.uj_type
+ with Not_found -> error_case_not_inductive env !evdref cj in
let _ = check_case_info env (fst indspec) ci in
let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
e_check_branch_types env evdref (fst indspec) cj (lfj,bty);
@@ -138,27 +165,28 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
let lt = Array.length vdefj in
if Int.equal (Array.length lar) lt then
for i = 0 to lt-1 do
- if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
- (Vars.lift lt lar.(i))) then
- Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
- i lna vdefj (Array.map EConstr.Unsafe.to_constr lar)
+ if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
+ (lift lt lar.(i))) then
+ error_ill_typed_rec_body ~loc env !evdref
+ i lna vdefj lar
done
(* FIXME: might depend on the level of actual parameters!*)
let check_allowed_sort env sigma ind c p =
let pj = Retyping.get_judgment_of env sigma p in
- let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
+ let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
let specif = Global.lookup_inductive (fst ind) in
let sorts = elim_sorts specif in
if not (List.exists ((==) ksort) sorts) then
let s = inductive_sort_family (snd specif) in
- error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj
- (Some(ksort,s,error_elim_explain ksort s))
+ error_elim_arity env sigma ind sorts c pj
+ (Some(ksort,s,Type_errors.error_elim_explain ksort s))
let e_judge_of_cast env evdref cj k tj =
+ let open EConstr in
let expected_type = tj.utj_val in
- if not (Evarconv.e_cumul env evdref (EConstr.of_constr cj.uj_type) (EConstr.of_constr expected_type)) then
- error_actual_type env cj expected_type;
+ if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
+ error_actual_type_core env !evdref cj expected_type;
{ uj_val = mkCast (cj.uj_val, k, expected_type);
uj_type = expected_type }
@@ -178,11 +206,56 @@ let check_cofix env sigma pcofix =
let (idx, (ids, cs, ts)) = pcofix in
check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts))
-let make_judge c ty =
- make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
-
(* The typing machine with universes and existential variables. *)
+let judge_of_prop =
+ { uj_val = EConstr.mkProp;
+ uj_type = EConstr.mkSort type1_sort }
+
+let judge_of_set =
+ { uj_val = EConstr.mkSet;
+ uj_type = EConstr.mkSort type1_sort }
+
+let judge_of_prop_contents = function
+ | Null -> judge_of_prop
+ | Pos -> judge_of_set
+
+let judge_of_type u =
+ let uu = Univ.Universe.super u in
+ { uj_val = EConstr.mkType u;
+ uj_type = EConstr.mkType uu }
+
+let judge_of_relative env v =
+ Termops.on_judgment EConstr.of_constr (judge_of_relative env v)
+
+let judge_of_variable env id =
+ Termops.on_judgment EConstr.of_constr (judge_of_variable env id)
+
+let judge_of_projection env sigma p cj =
+ let pb = lookup_projection p env in
+ let (ind,u), args =
+ try find_mrectype env sigma cj.uj_type
+ with Not_found -> error_case_not_inductive env sigma cj
+ in
+ let args = List.map EConstr.of_constr args in
+ let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in
+ let ty = substl (cj.uj_val :: List.rev args) ty in
+ {uj_val = EConstr.mkProj (p,cj.uj_val);
+ uj_type = ty}
+
+let judge_of_abstraction env name var j =
+ { uj_val = mkLambda (name, var.utj_val, j.uj_val);
+ uj_type = mkProd (name, var.utj_val, j.uj_type) }
+
+let judge_of_product env name t1 t2 =
+ let s = sort_of_product env t1.utj_type t2.utj_type in
+ { uj_val = mkProd (name, t1.utj_val, t2.utj_val);
+ uj_type = mkSort s }
+
+let judge_of_letin env name defj typj j =
+ { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
+ uj_type = subst1 defj.uj_val j.uj_type }
+
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
where both the term and type are in n.f. *)
let rec execute env evdref cstr =
@@ -190,13 +263,13 @@ let rec execute env evdref cstr =
let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
match EConstr.kind !evdref cstr with
| Meta n ->
- { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n }
+ { uj_val = cstr; uj_type = EConstr.of_constr (meta_type !evdref n) }
| Evar ev ->
let ty = EConstr.existential_type !evdref ev in
let jty = execute env evdref ty in
let jty = e_assumption_of_judgment env evdref jty in
- { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty }
+ { uj_val = cstr; uj_type = jty }
| Rel n ->
judge_of_relative env n
@@ -239,7 +312,7 @@ let rec execute env evdref cstr =
| Proj (p, c) ->
let cj = execute env evdref c in
- judge_of_projection env p (Evarutil.j_nf_evar !evdref cj)
+ judge_of_projection env !evdref p cj
| App (f,args) ->
let jl = execute_array env evdref args in
@@ -248,13 +321,11 @@ let rec execute env evdref cstr =
| Ind ind when Environ.template_polymorphic_pind ind env ->
(* Sort-polymorphism of inductive types *)
make_judge f
- (inductive_type_knowing_parameters env ind
- (Evarutil.jv_nf_evar !evdref jl))
+ (inductive_type_knowing_parameters env !evdref ind jl)
| Const cst when Environ.template_polymorphic_pconstant cst env ->
(* Sort-polymorphism of inductive types *)
make_judge f
- (constant_type_knowing_parameters env cst
- (Evarutil.jv_nf_evar !evdref jl))
+ (constant_type_knowing_parameters env !evdref cst jl)
| _ ->
execute env evdref f
in
@@ -263,14 +334,14 @@ let rec execute env evdref cstr =
| Lambda (name,c1,c2) ->
let j = execute env evdref c1 in
let var = e_type_judgment env evdref j in
- let env1 = push_rel (LocalAssum (name, var.utj_val)) env in
+ let env1 = push_rel (local_assum (name, var.utj_val)) env in
let j' = execute env1 evdref c2 in
judge_of_abstraction env1 name var j'
| Prod (name,c1,c2) ->
let j = execute env evdref c1 in
let varj = e_type_judgment env evdref j in
- let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in
+ let env1 = push_rel (local_assum (name, varj.utj_val)) env in
let j' = execute env1 evdref c2 in
let varj' = e_type_judgment env1 evdref j' in
judge_of_product env name varj varj'
@@ -280,7 +351,7 @@ let rec execute env evdref cstr =
let j2 = execute env evdref c2 in
let j2 = e_type_judgment env evdref j2 in
let _ = e_judge_of_cast env evdref j1 DEFAULTcast j2 in
- let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in
+ let env1 = push_rel (local_def (name, j1.uj_val, j2.utj_val)) env in
let j3 = execute env1 evdref c3 in
judge_of_letin env name j1 j2 j3
@@ -295,7 +366,7 @@ and execute_recdef env evdref (names,lar,vdef) =
let lara = Array.map (e_assumption_of_judgment env evdref) larj in
let env1 = push_rec_types (names,lara,vdef) env in
let vdefj = execute_array env1 evdref vdef in
- let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in
+ let vdefv = Array.map j_val vdefj in
let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
(names,lara,vdefv)
@@ -304,8 +375,8 @@ and execute_array env evdref = Array.map (execute env evdref)
let e_check env evdref c t =
let env = enrich_env env evdref in
let j = execute env evdref c in
- if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then
- error_actual_type env j (EConstr.to_constr !evdref t)
+ if not (Evarconv.e_cumul env evdref j.uj_type t) then
+ error_actual_type_core env !evdref j t
(* Type of a constr *)
@@ -313,7 +384,7 @@ let unsafe_type_of env evd c =
let evdref = ref evd in
let env = enrich_env env evdref in
let j = execute env evdref c in
- j.uj_type
+ EConstr.Unsafe.to_constr j.uj_type
(* Sort of a type *)
@@ -331,23 +402,23 @@ let type_of ?(refresh=false) env evd c =
let j = execute env evdref c in
(* side-effect on evdref *)
if refresh then
- Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type)
- else !evdref, j.uj_type
+ Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
+ else !evdref, EConstr.Unsafe.to_constr j.uj_type
let e_type_of ?(refresh=false) env evdref c =
let env = enrich_env env evdref in
let j = execute env evdref c in
(* side-effect on evdref *)
if refresh then
- let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) in
+ let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
let () = evdref := evd in
c
- else j.uj_type
+ else EConstr.Unsafe.to_constr j.uj_type
let e_solve_evars env evdref c =
let env = enrich_env env evdref in
let c = (execute env evdref c).uj_val in
(* side-effect on evdref *)
- nf_evar !evdref c
+ nf_evar !evdref (EConstr.Unsafe.to_constr c)
let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 3c1c4324d..1fb414906 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Names
open Term
open Environ
open Evd
@@ -43,4 +44,11 @@ val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> ECon
(** Raise an error message if bodies have types not unifiable with the
expected ones *)
val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
- Names.Name.t array -> EConstr.types array -> unsafe_judgment array -> unit
+ Names.Name.t array -> EConstr.types array -> EConstr.unsafe_judgment array -> unit
+
+val judge_of_prop : EConstr.unsafe_judgment
+val judge_of_set : EConstr.unsafe_judgment
+val judge_of_abstraction : Environ.env -> Name.t ->
+ EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
+val judge_of_product : Environ.env -> Name.t ->
+ EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c5c19b49b..1b209fa77 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -120,6 +120,9 @@ let abstract_list_all env evd typ c l =
| UserError _ ->
error_cannot_find_well_typed_abstraction env evd p l None
| Type_errors.TypeError (env',x) ->
+ (** FIXME: plug back the typing information *)
+ error_cannot_find_well_typed_abstraction env evd p l None
+ | Pretype_errors.PretypeError (env',evd,TypingError x) ->
error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
let typp = EConstr.of_constr typp in
evd,(p,typp)
@@ -1255,15 +1258,12 @@ let is_mimick_head sigma ts f =
| (Rel _|Construct _|Ind _) -> true
| _ -> false
-let make_judge c t =
- make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t)
-
let try_to_coerce env evd c cty tycon =
let j = make_judge c cty in
let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
let evd' = Evarconv.consider_remaining_unif_problems env evd' in
let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
- (evd',EConstr.of_constr j'.uj_val)
+ (evd',j'.uj_val)
let w_coerce_to_type env evd c cty mvty =
let evd,tycon = pose_all_metas_as_evars env evd mvty in
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 05:25:47 +0000