aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml24
-rw-r--r--pretyping/class.ml6
-rw-r--r--pretyping/coercion.ml106
-rw-r--r--pretyping/coercion.mli18
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/evarutil.ml2
-rw-r--r--pretyping/pretyping.ml83
-rw-r--r--pretyping/retyping.ml15
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/tacred.ml8
-rw-r--r--pretyping/typing.ml18
-rw-r--r--pretyping/typing.mli4
12 files changed, 129 insertions, 161 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 176a3c3e9..413ea152a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -135,11 +135,7 @@ let inductive_of_rawconstructor c =
inductive_of_constructor (constructor_of_rawconstructor c)
(* Environment management *)
-let push_rel_type sigma (na,t) env =
- push_rel_assum (na,get_assumption_of env sigma t) env
-
-let push_rels vars env =
- List.fold_right (fun nvar env -> push_rel_type Evd.empty nvar env) vars env
+let push_rels vars env = List.fold_right push_rel_assum vars env
(**********************************************************************)
(* Structures used in compiling pattern-matching *)
@@ -670,8 +666,7 @@ let abstract_predicate env sigma indf = function
let dep = copt <> None in
let sign' =
if dep then
- let ind=get_assumption_of env sigma (build_dependent_inductive indf)
- in (Anonymous,None,ind)::sign
+ (Anonymous,None,build_dependent_inductive indf) :: sign
else sign in
(dep, it_mkLambda_or_LetIn_name env (extract_predicate pred) sign')
@@ -764,7 +759,7 @@ let build_branch pb defaults eqns const_info =
let _,typs' =
List.fold_right
(fun (na,t) (env,typs) ->
- (push_rel_assum (na,outcast_type t) env,
+ (push_rel_assum (na,t) env,
((na,to_mutind env !(pb.isevars) t),t)::typs))
typs (pb.env,[]) in
let tomatchs =
@@ -834,7 +829,7 @@ and match_current pb (n,tm) =
pb.pred brtyps cstrs current indt in
let ci = make_case_info mis None tags in
{ uj_val = mkMutCase (ci, (*eta_reduce_if_rel*)pred,current,brvals);
- uj_type = make_typed typ s }
+ uj_type = typ }
and compile_further pb firstnext rest =
(* We pop as much as possible tomatch not dependent one of the other *)
@@ -855,7 +850,7 @@ and compile_further pb firstnext rest =
let j = compile pb' in
{ uj_val = lam_it j.uj_val sign;
uj_type = (* Pas d'univers ici: imprédicatif si Prop/Set, dummy si Type *)
- typed_app (fun t -> prod_it t sign) j.uj_type }
+ type_app (fun t -> prod_it t sign) j.uj_type }
(* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -923,9 +918,8 @@ let inh_coerce_to_ind isevars env ty tyi =
let (_,evarl) =
List.fold_right
(fun (na,ty) (env,evl) ->
- let aty = get_assumption_of env Evd.empty ty in
- (push_rel_assum (na,aty) env,
- (new_isevar isevars env (incast_type aty) CCI)::evl))
+ (push_rel_assum (na,ty) env,
+ (new_isevar isevars env ty CCI)::evl))
ntys (env,[]) in
let expected_typ = applist (mkMutInd tyi,evarl) in
(* devrait être indifférent d'exiger leq ou pas puisque pour
@@ -1105,7 +1099,5 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
let j = compile pb in
match tycon with
- | Some p ->
- let p = get_assumption_of env !isevars p in
- Coercion.inh_conv_coerce_to loc env isevars j p
+ | Some p -> Coercion.inh_conv_coerce_to loc env isevars j p
| None -> j
diff --git a/pretyping/class.ml b/pretyping/class.ml
index b83eb3608..0f201d004 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -285,14 +285,12 @@ lorque source est None alors target est None aussi.
let try_add_new_coercion_core idf stre source target isid =
let env = Global.env () in
let v = construct_reference env CCI idf in
- let t = Retyping.get_type_of env Evd.empty v in
- let k = Retyping.get_sort_of env Evd.empty t in
- let vj = {uj_val=v; uj_type= make_typed t k} in
+ let vj = Retyping.get_judgment_of env Evd.empty v in
let f_vardep,coef = coe_of_reference v in
if coercion_exists coef then
errorlabstrm "try_add_coercion"
[< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
- let lp = prods_of t in
+ let lp = prods_of (vj.uj_type) in
let llp = List.length lp in
if llp <= 1 then
errorlabstrm "try_add_coercion"
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9040ce3eb..a4dfa3683 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -19,15 +19,15 @@ let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t)
let j_nf_ise env sigma {uj_val=v;uj_type=t} =
{ uj_val = nf_ise1 sigma v;
- uj_type = typed_app (nf_ise1 sigma) t }
+ uj_type = nf_ise1 sigma t }
let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
(* Here, funj is a coercion therefore already typed in global context *)
let apply_coercion_args env argl funj =
let rec apply_rec acc typ = function
- | [] -> { uj_val=applist(j_val_only funj,argl);
- uj_type= typed_app (fun _ -> typ) funj.uj_type }
+ | [] -> { uj_val = applist (j_val funj,argl);
+ uj_type = typ }
| h::restl ->
(* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
@@ -36,11 +36,13 @@ let apply_coercion_args env argl funj =
apply_rec (h::acc) (subst1 h c2) restl
| _ -> anomaly "apply_coercion_args"
in
- apply_rec [] (body_of_type funj.uj_type) argl
+ apply_rec [] funj.uj_type argl
(* appliquer le chemin de coercions p a` hj *)
-let apply_pcoercion env p hj typ_cl =
+exception NoCoercion
+
+let apply_coercion env p hj typ_cl =
if !compter then begin
nbpathc := !nbpathc +1;
nbcoer := !nbcoer + (List.length p)
@@ -48,79 +50,74 @@ let apply_pcoercion env p hj typ_cl =
try
fst (List.fold_left
(fun (ja,typ_cl) i ->
- let fv,b= coe_value i in
+ let fv,b = coe_value i in
let argl = (class_args_of typ_cl)@[ja.uj_val] in
let jres = apply_coercion_args env argl fv in
(if b then
{ uj_val=ja.uj_val; uj_type=jres.uj_type }
else
jres),
- (body_of_type jres.uj_type))
+ jres.uj_type)
(hj,typ_cl) p)
- with _ -> anomaly "apply_pcoercion"
+ with _ -> anomaly "apply_coercion"
let inh_app_fun env isevars j =
- let t = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
+ let t = whd_betadeltaiota env !isevars j.uj_type in
match kind_of_term t with
| IsProd (_,_,_) -> j
| _ ->
(try
- let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
+ let t,i1 = class_of1 env !isevars j.uj_type in
let p = lookup_path_to_fun_from i1 in
- apply_pcoercion env p j t
+ apply_coercion env p j t
with Not_found -> j)
let inh_tosort_force env isevars j =
try
- let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
+ let t,i1 = class_of1 env !isevars j.uj_type in
let p = lookup_path_to_sort_from i1 in
- apply_pcoercion env p j t
+ apply_coercion env p j t
with Not_found ->
j
let inh_tosort env isevars j =
- let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
+ let typ = whd_betadeltaiota env !isevars j.uj_type in
match kind_of_term typ with
| IsSort _ -> j (* idem inh_app_fun *)
| _ -> inh_tosort_force env isevars j
let inh_ass_of_j env isevars j =
- let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
+ let typ = whd_betadeltaiota env !isevars j.uj_type in
match kind_of_term typ with
| IsSort s -> { utj_val = j.uj_val; utj_type = s }
| _ ->
let j1 = inh_tosort_force env isevars j in
type_judgment env !isevars j1
-exception NoCoercion
-
let inh_coerce_to_fail env isevars c1 hj =
let hj' =
try
let t1,i1 = class_of1 env !isevars c1 in
- let t2,i2 = class_of1 env !isevars (body_of_type hj.uj_type) in
+ let t2,i2 = class_of1 env !isevars hj.uj_type in
let p = lookup_path_between (i2,i1) in
- apply_pcoercion env p hj t2
+ apply_coercion env p hj t2
with Not_found -> raise NoCoercion
in
- if the_conv_x_leq env isevars (body_of_type hj'.uj_type) c1 then
+ if the_conv_x_leq env isevars hj'.uj_type c1 then
hj'
else
raise NoCoercion
let rec inh_conv_coerce_to_fail env isevars c1 hj =
let {uj_val = v; uj_type = t} = hj in
- let t = body_of_type t in
if the_conv_x_leq env isevars t c1 then hj
else
try
inh_coerce_to_fail env isevars c1 hj
with NoCoercion -> (* try ... with _ -> ... is BAD *)
- (* (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*)
(match kind_of_term (whd_betadeltaiota env !isevars t),
kind_of_term (whd_betadeltaiota env !isevars c1) with
| IsProd (_,t1,t2), IsProd (name,u1,u2) ->
- (* let v' = hnf_constr !isevars v in *)
let v' = whd_betadeltaiota env !isevars v in
if (match kind_of_term v' with
| IsLambda (_,v1,v2) ->
@@ -128,50 +125,48 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
| _ -> false)
then
let (x,v1,v2) = destLambda v' in
- (* let jv1 = exemeta_rec def_vty_con env isevars v1 in
- let assv1 = assumption_of_judgement env !isevars jv1 in *)
- let assv1 = outcast_type v1 in
- let env1 = push_rel_assum (x,assv1) env in
+ let env1 = push_rel_assum (x,v1) env in
let h2 = inh_conv_coerce_to_fail env isevars u2
- {uj_val = v2;
- uj_type = get_assumption_of env1 !isevars t2 } in
- fst (abs_rel env !isevars x assv1 h2)
+ {uj_val = v2; uj_type = t2 } in
+ fst (abs_rel env !isevars x v1 h2)
else
- let assu1 = get_assumption_of env !isevars u1 in
let name = (match name with
| Anonymous -> Name (id_of_string "x")
| _ -> name) in
- let env1 = push_rel_assum (name,assu1) env in
+ let env1 = push_rel_assum (name,u1) env in
let h1 =
inh_conv_coerce_to_fail env isevars t1
{uj_val = mkRel 1;
- uj_type = typed_app (fun _ -> u1) assu1 } in
+ uj_type = u1 } in
let h2 = inh_conv_coerce_to_fail env isevars u2
{ uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
- uj_type = get_assumption_of env1 !isevars
- (subst1 h1.uj_val t2) }
+ uj_type = subst1 h1.uj_val t2 }
in
- fst (abs_rel env !isevars name assu1 h2)
+ fst (abs_rel env !isevars name u1 h2)
| _ -> raise NoCoercion)
-let inh_conv_coerce_to loc env isevars cj tj =
+let inh_conv_coerce_to loc env isevars cj t =
let cj' =
try
- inh_conv_coerce_to_fail env isevars (body_of_type tj) cj
+ inh_conv_coerce_to_fail env isevars t cj
with NoCoercion ->
let rcj = j_nf_ise env !isevars cj in
- let at = nf_ise1 !isevars (body_of_type tj) in
- error_actual_type_loc loc env rcj.uj_val (body_of_type rcj.uj_type) at
+ let at = nf_ise1 !isevars t in
+ error_actual_type_loc loc env rcj.uj_val rcj.uj_type at
in
{ uj_val = cj'.uj_val;
- uj_type = tj }
+ uj_type = t }
+
+(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
+ args)] of type [tycon] (if any) by inserting coercions in front of
+ each arg$_i$, if necessary *)
-let inh_apply_rel_list nocheck apploc env isevars argjl funj tycon =
+let inh_apply_rel_list apploc env isevars argjl funj tycon =
let rec apply_rec n acc typ = function
| [] ->
let resj =
- { uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc));
- uj_type= typed_app (fun _ -> typ) funj.uj_type }
+ { uj_val = applist (j_val funj, List.rev acc);
+ uj_type = typ }
in
(match tycon with
| Some typ' ->
@@ -183,22 +178,19 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj tycon =
match kind_of_term (whd_betadeltaiota env !isevars typ) with
| IsProd (_,c1,c2) ->
let hj' =
- if nocheck then
- hj
- else
- (try
- inh_conv_coerce_to_fail env isevars c1 hj
- with NoCoercion ->
- error_cant_apply_bad_type_loc apploc env
- (n,nf_ise1 !isevars c1,
- nf_ise1 !isevars (body_of_type hj.uj_type))
- (j_nf_ise env !isevars funj)
- (jl_nf_ise env !isevars argjl))
+ (try
+ inh_conv_coerce_to_fail env isevars c1 hj
+ with NoCoercion ->
+ error_cant_apply_bad_type_loc apploc env
+ (n,nf_ise1 !isevars c1,
+ nf_ise1 !isevars hj.uj_type)
+ (j_nf_ise env !isevars funj)
+ (jl_nf_ise env !isevars argjl))
in
- apply_rec (n+1) (hj'::acc) (subst1 hj'.uj_val c2) restjl
+ apply_rec (n+1) ((j_val hj')::acc) (subst1 hj'.uj_val c2) restjl
| _ ->
error_cant_apply_not_functional_loc apploc env
(j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)
in
- apply_rec 1 [] (body_of_type funj.uj_type) argjl
+ apply_rec 1 [] funj.uj_type argjl
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 52cdabc06..0969387fb 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -9,20 +9,30 @@ open Environ
open Evarutil
(*i*)
-(* Coercions. *)
+(*s Coercions. *)
val inh_app_fun :
env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
val inh_tosort_force :
env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
+
+(* [inh_tosort env sigma j] insert a coercion into [j], if needed, in
+ such a way [t] reduces to a sort; it fails if no coercion is applicable *)
val inh_tosort :
env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
-val inh_ass_of_j :
+
+val inh_ass_of_j :
env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment
+(* [inh_conv_coerce_to loc env sigma j t] insert a coercion into [j],
+ if needed, in such a way it [t] and [j.uj_type] are convertible; it
+ fails if no coercion is applicable *)
val inh_conv_coerce_to : Rawterm.loc ->
- env -> 'a evar_defs -> unsafe_judgment -> typed_type -> unsafe_judgment
+ env -> 'a evar_defs -> unsafe_judgment -> constr -> unsafe_judgment
-val inh_apply_rel_list : bool -> Rawterm.loc -> env -> 'a evar_defs ->
+(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
+ args)] of type [tycon] (if any) by inserting coercions in front of
+ each arg$_i$, if necessary *)
+val inh_apply_rel_list : Rawterm.loc -> env -> 'a evar_defs ->
unsafe_judgment list -> unsafe_judgment -> constr option
-> unsafe_judgment
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f4e9d01b7..15151ca9b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -263,8 +263,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] ->
evar_conv_x env isevars CONV c1 c2
&
- (let d = Retyping.get_assumption_of env !isevars (nf_ise1 !isevars c1)
- in evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2)
+ (let d = nf_ise1 !isevars c1 in
+ evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2)
| IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
sp1=sp2
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8aac75e39..3f0570dc9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -76,7 +76,7 @@ let split_evar_to_arrow sigma c =
let (sigma1,dom) = new_type_var evenv sigma in
let hyps = named_context evenv in
let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
- let newenv = push_named_assum (nvar,make_typed dom (Type dummy_univ)) evenv in
+ let newenv = push_named_assum (nvar, dom) evenv in
let (sigma2,rng) = new_type_var newenv sigma1 in
let prod = mkProd (named_hd newenv dom Anonymous, dom, subst_var nvar rng) in
let sigma3 = Evd.define sigma2 ev prod in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9caab6bcc..ff10083ff 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -95,10 +95,10 @@ let ctxt_of_ids cl = cl
let mt_evd = Evd.empty
-let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
let j_nf_ise sigma {uj_val=v;uj_type=t} =
- {uj_val=nf_ise1 sigma v;uj_type=typed_app (nf_ise1 sigma) t}
+ {uj_val=nf_ise1 sigma v;uj_type=type_app (nf_ise1 sigma) t}
let jv_nf_ise sigma = Array.map (j_nf_ise sigma)
@@ -112,23 +112,13 @@ let evar_type_fixpoint env isevars lna lar vdefj =
if Array.length lar = lt then
for i = 0 to lt-1 do
if not (the_conv_x_leq env isevars
- (body_of_type (vdefj.(i)).uj_type)
- (lift lt (body_of_type lar.(i)))) then
+ (vdefj.(i)).uj_type
+ (lift lt lar.(i))) then
error_ill_typed_rec_body CCI env i lna
(jv_nf_ise !isevars vdefj)
- (Array.map (typed_app (nf_ise1 !isevars)) lar)
+ (Array.map (type_app (nf_ise1 !isevars)) lar)
done
-
-(* Inutile ?
-let cast_rel isevars env cj tj =
- if the_conv_x_leq isevars env cj.uj_type tj.uj_val then
- {uj_val=j_val_only cj;
- uj_type=tj.uj_val;
- uj_kind = hnf_constr !isevars tj.uj_type}
- else error_actual_type CCI env (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)
-
-*)
let let_path = make_path ["Core"] (id_of_string "let") CCI
let wrong_number_of_cases_message loc env isevars (c,ct) expn =
@@ -156,7 +146,7 @@ let pretype_id loc env lvar id =
with Not_found ->
try
let (n,typ) = lookup_rel_id id (rel_context env) in
- { uj_val = mkRel n; uj_type = typed_app (lift n) typ }
+ { uj_val = mkRel n; uj_type = type_app (lift n) typ }
with Not_found ->
try
let typ = lookup_id_type id (named_context env) in
@@ -183,7 +173,7 @@ let pretype_ref pretype loc isevars env lvar = function
mkEvar ev
in
let typ = existential_type !isevars ev in
- make_judge body (Retyping.get_assumption_of env !isevars typ)
+ make_judge body typ
| RInd (ind_sp,ctxt) ->
let ind = (ind_sp,Array.map pretype ctxt) in
@@ -198,7 +188,7 @@ let pretype_sort = function
| RProp c -> judge_of_prop_contents c
| RType ->
{ uj_val = dummy_sort;
- uj_type = make_typed dummy_sort (Type Univ.dummy_univ) }
+ uj_type = dummy_sort }
(* pretype tycon isevars env constr tries to solve the *)
(* existential variables in constr in environment env with the *)
@@ -223,9 +213,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
| RHole loc ->
if !compter then nbimpl:=!nbimpl+1;
(match tycon with
- | Some ty ->
- let c = new_isevar isevars env ty CCI in
- {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
+ | Some ty -> { uj_val = new_isevar isevars env ty CCI; uj_type = ty }
| None ->
(match loc with
None -> anomaly "There is an implicit argument I cannot solve"
@@ -249,14 +237,13 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars lvar
lmeta def) vdef in
(evar_type_fixpoint env isevars lfi lara vdefj;
- let larav = Array.map body_of_type lara in
match fixkind with
| RFix (vn,i as vni) ->
- let fix = (vni,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+ let fix = (vni,(lara,List.rev lfi,Array.map j_val vdefj)) in
check_fix env !isevars fix;
make_judge (mkFix fix) lara.(i)
| RCoFix i ->
- let cofix = (i,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+ let cofix = (i,(lara,List.rev lfi,Array.map j_val vdefj)) in
check_cofix env !isevars cofix;
make_judge (mkCoFix cofix) lara.(i))
@@ -271,14 +258,14 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let rng_tycon = option_app (subst1 cj.uj_val) rng in
(rng_tycon,cj::jl) in
let jl = List.rev (snd (List.fold_left apply_one_arg
- (mk_tycon (body_of_type j.uj_type),[]) args)) in
- inh_apply_rel_list false loc env isevars jl j tycon
+ (mk_tycon j.uj_type,[]) args)) in
+ inh_apply_rel_list loc env isevars jl j tycon
| RBinder(loc,BLambda,name,c1,c2) ->
let (dom,rng) = split_tycon loc env isevars tycon in
let dom_valcon = valcon_of_tycon dom in
let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
- let assum = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
+ let assum = (inh_ass_of_j env isevars j).utj_val in
let var = (name,assum) in
let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2
in
@@ -287,7 +274,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
| RBinder(loc,BProd,name,c1,c2) ->
let j = pretype empty_tycon env isevars lvar lmeta c1 in
let assum = inh_ass_of_j env isevars j in
- let var = (name,assumption_of_type_judgment assum) in
+ let var = (name,assum.utj_val) in
let j' = pretype empty_tycon (push_rel_assum var env) isevars lvar lmeta c2 in
(try fst (gen_rel env !isevars name assum j')
with TypeError _ as e -> Stdpp.raise_with_loc loc e)
@@ -296,15 +283,15 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let j = pretype empty_tycon env isevars lvar lmeta c1 in
let var = (name,j.uj_val,j.uj_type) in
let j' = pretype tycon (push_rel_def var env) isevars lvar lmeta c2 in
- { uj_val = mkLetIn (name, j.uj_val, body_of_type j.uj_type, j'.uj_val) ;
- uj_type = typed_app (subst1 j.uj_val) j'.uj_type }
+ { uj_val = mkLetIn (name, j.uj_val, j.uj_type, j'.uj_val) ;
+ uj_type = type_app (subst1 j.uj_val) j'.uj_type }
| ROldCase (loc,isrec,po,c,lf) ->
let cj = pretype empty_tycon env isevars lvar lmeta c in
let (IndType (indf,realargs) as indt) =
- try find_rectype env !isevars (body_of_type cj.uj_type)
+ try find_rectype env !isevars cj.uj_type
with Induc -> error_case_not_inductive CCI env
- (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars (body_of_type cj.uj_type)) in
+ (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
let pj = match po with
| Some p -> pretype empty_tycon env isevars lvar lmeta p
| None ->
@@ -323,34 +310,34 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let expti = expbr.(i) in
let fj =
pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
- let efjt = nf_ise1 !isevars (body_of_type fj.uj_type) in
+ let efjt = nf_ise1 !isevars fj.uj_type in
let pred =
Cases.pred_case_ml_onebranch env !isevars isrec indt
(i,fj.uj_val,efjt) in
if has_ise !isevars pred then findtype (i+1)
else
let pty = Retyping.get_type_of env !isevars pred in
- { uj_val=pred;
- uj_type = Retyping.get_assumption_of env !isevars pty }
+ { uj_val = pred;
+ uj_type = pty }
with UserError _ -> findtype (i+1) in
findtype 0 in
- let evalct = find_rectype env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
- and evalPt = nf_ise1 !isevars (body_of_type pj.uj_type) in
+ let evalct = find_rectype env !isevars cj.uj_type (*Pour normaliser evars*)
+ and evalPt = nf_ise1 !isevars pj.uj_type in
let (bty,rsty) =
Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
if Array.length bty <> Array.length lf then
wrong_number_of_cases_message loc env isevars
- (cj.uj_val,nf_ise1 !isevars (body_of_type cj.uj_type))
+ (cj.uj_val,nf_ise1 !isevars cj.uj_type)
(Array.length bty)
else
let lfj =
array_map2
(fun tyc f -> pretype (mk_tycon tyc) env isevars lvar lmeta f) bty
lf in
- let lfv = (Array.map (fun j -> j.uj_val) lfj) in
- let lft = (Array.map (fun j -> body_of_type j.uj_type) lfj) in
+ let lfv = Array.map j_val lfj in
+ let lft = Array.map (fun j -> j.uj_type) lfj in
check_branches_message loc env isevars cj.uj_val (bty,lft);
let v =
if isrec
@@ -361,9 +348,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let ci = make_default_case_info mis in
mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map (fun j-> j.uj_val) lfj)
in
- let s = snd (splay_arity env !isevars evalPt) in
{uj_val = v;
- uj_type = make_typed rsty s }
+ uj_type = rsty }
| RCases (loc,prinfo,po,tml,eqns) ->
Cases.compile_cases loc
@@ -376,9 +362,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let cj = pretype (mk_tycon tj.utj_val) env isevars lvar lmeta c in
match tycon with
| None -> cj
- | Some t' ->
- let tj' = Retyping.get_assumption_of env !isevars t' in
- inh_conv_coerce_to loc env isevars cj tj'
+ | Some t' -> inh_conv_coerce_to loc env isevars cj t'
and pretype_type valcon env isevars lvar lmeta = function
| RHole loc ->
@@ -386,9 +370,8 @@ and pretype_type valcon env isevars lvar lmeta = function
(match valcon with
| Some v -> Retyping.get_judgment_of env !isevars v
| None ->
- let ty = dummy_sort in
- let c = new_isevar isevars env ty CCI in
- { uj_val = c ; uj_type = make_typed ty (Type Univ.dummy_univ) })
+ { uj_val = new_isevar isevars env dummy_sort CCI;
+ uj_type = dummy_sort })
| c ->
let j = pretype empty_tycon env isevars lvar lmeta c in
let tj = inh_tosort env isevars j in
@@ -453,7 +436,7 @@ let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in
let metamap = ref [] in
let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
- let t = typed_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
+ let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
!metamap, {uj_val = v; uj_type = t }
let ise_resolve_casted sigma env typ c =
@@ -468,7 +451,7 @@ let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c =
let j = unsafe_infer tycon isevars env lvar lmeta c in
let metamap = ref [] in
let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
- let t = typed_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
+ let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
!metamap, {uj_val = v; uj_type = t }
let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 4f36fbbdd..53bf5b08a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -63,11 +63,9 @@ let rec type_of env cstr=
then realargs@[c] else realargs in
whd_betadeltaiota env sigma (applist (p,al))
| IsLambda (name,c1,c2) ->
- let var = make_typed c1 (sort_of env c1) in
- mkProd (name, c1, type_of (push_rel_assum (name,var) env) c2)
+ mkProd (name, c1, type_of (push_rel_assum (name,c1) env) c2)
| IsLetIn (name,b,c1,c2) ->
- let var = make_typed c1 (sort_of env c1) in
- subst1 b (type_of (push_rel_def (name,b,var) env) c2)
+ subst1 b (type_of (push_rel_def (name,b,c1) env) c2)
| IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
| IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
| IsApp(f,args)->
@@ -83,8 +81,7 @@ and sort_of env t =
| IsSort (Prop c) -> type_0
| IsSort (Type u) -> Type Univ.dummy_univ
| IsProd (name,t,c2) ->
- let var = make_typed t (sort_of env t) in
- (match (sort_of (push_rel_assum (name,var) env) c2) with
+ (match (sort_of (push_rel_assum (name,t) env) c2) with
| Prop _ as s -> s
| Type u2 -> Type Univ.dummy_univ)
| IsApp(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
@@ -99,10 +96,8 @@ let get_sort_of env sigma t = snd (typeur sigma []) env t
let get_type_of_with_meta env sigma metamap = fst (typeur sigma metamap) env
(* Makes an assumption from a constr *)
-let get_assumption_of env evc c = make_typed_lazy c (get_sort_of env evc)
+let get_assumption_of env evc c = c
(* Makes an unsafe judgment from a constr *)
-let get_judgment_of env evc c =
- let typ = get_type_of env evc c in
- { uj_val = c; uj_type = get_assumption_of env evc typ }
+let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 379a03956..4d472c19c 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -21,7 +21,7 @@ val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr
val get_sort_of : env -> 'a evar_map -> constr -> sorts
(* Makes an assumption from a constr *)
-val get_assumption_of : env -> 'a evar_map -> constr -> typed_type
+val get_assumption_of : env -> 'a evar_map -> constr -> types
(* Makes an unsafe judgment from a constr *)
val get_judgment_of : env -> 'a evar_map -> constr -> unsafe_judgment
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c1fa26c5f..3d58b6a24 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -625,12 +625,8 @@ let reduce_to_mind env sigma t =
elimrec t' l
with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
[< 'sTR"Not an inductive product." >])
- | IsProd (n,ty,t') ->
- let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
- elimrec t' ((n,None,ty')::l)
- | IsLetIn (n,b,ty,t') ->
- let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
- elimrec t' ((n,Some b,ty')::l)
+ | IsProd (n,ty,t') -> elimrec t' ((n,None,ty)::l)
+ | IsLetIn (n,b,ty,t') -> elimrec t' ((n,Some b,ty)::l)
| _ -> error "Not an inductive product"
in
elimrec t []
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ebab35c2c..23028cc62 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -11,7 +11,7 @@ open Type_errors
open Typeops
let vect_lift = Array.mapi lift
-let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
type 'a mach_flags = {
fix : bool;
@@ -94,8 +94,7 @@ let rec execute mf env sigma cstr =
| IsProd (name,c1,c2) ->
let j = execute mf env sigma c1 in
let varj = type_judgment env sigma j in
- let var = assumption_of_type_judgment varj in
- let env1 = push_rel_assum (name,var) env in
+ let env1 = push_rel_assum (name,varj.utj_val) env in
let j' = execute mf env1 sigma c2 in
let (j,_) = gen_rel env1 sigma name varj j' in
j
@@ -103,15 +102,18 @@ let rec execute mf env sigma cstr =
| IsLetIn (name,c1,c2,c3) ->
let j1 = execute mf env sigma c1 in
let j2 = execute mf env sigma c2 in
- let { uj_val = b; uj_type = t } = cast_rel env sigma j1 j2 in
+ let tj2 = assumption_of_judgment env sigma j2 in
+ let { uj_val = b; uj_type = t },_ = cast_rel env sigma j1 tj2 in
let j3 = execute mf (push_rel_def (name,b,t) env) sigma c3 in
- { uj_val = mkLetIn (name, j1.uj_val, j2.uj_val, j3.uj_val) ;
- uj_type = typed_app (subst1 j1.uj_val) j3.uj_type }
+ { uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ;
+ uj_type = type_app (subst1 j1.uj_val) j3.uj_type }
| IsCast (c,t) ->
let cj = execute mf env sigma c in
let tj = execute mf env sigma t in
- cast_rel env sigma cj tj
+ let tj = assumption_of_judgment env sigma tj in
+ let j, _ = cast_rel env sigma cj tj in
+ j
| IsXtra _ -> anomaly "Typing: found an Extra"
@@ -123,7 +125,7 @@ and execute_fix mf env sigma lar lfi vdef =
let env1 =
List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in
let vdefj = execute_array mf env1 sigma vdef in
- let vdefv = Array.map j_val_only vdefj in
+ let vdefv = Array.map j_val vdefj in
let cst3 = type_fixpoint env1 sigma lfi lara vdefj in
(lara,vdefv)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index ee68e518f..eaad2791f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -14,7 +14,7 @@ val unsafe_machine : env -> 'a evar_map -> constr -> unsafe_judgment
val type_of : env -> 'a evar_map -> constr -> constr
-val execute_type : env -> 'a evar_map -> constr -> typed_type
+val execute_type : env -> 'a evar_map -> constr -> types
-val execute_rec_type : env -> 'a evar_map -> constr -> typed_type
+val execute_rec_type : env -> 'a evar_map -> constr -> types
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-23 20:58:23 +0000