aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml166
-rw-r--r--pretyping/cases.mli13
-rw-r--r--pretyping/class.ml4
-rw-r--r--pretyping/coercion.ml68
-rw-r--r--pretyping/coercion.mli2
-rw-r--r--pretyping/evarutil.ml18
-rw-r--r--pretyping/evarutil.mli2
-rw-r--r--pretyping/pretyping.ml83
-rw-r--r--pretyping/retyping.ml9
-rw-r--r--pretyping/typing.ml15
10 files changed, 229 insertions, 151 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 67d279867..7d61c7a82 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -24,37 +24,97 @@ open Evarconv
let mkExistential isevars env =
new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI
-let norec_branch_scheme env isevars typc =
- let rec crec typc = match whd_betadeltaiota env !isevars typc with
- | DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,crec t))
- | _ -> mkExistential isevars env
- in
- crec typc
+let norec_branch_scheme env isevars cstr =
+ prod_it (mkExistential isevars env) cstr.cs_args
+
+let lift_args l = list_map_i (fun i (name,c) -> (name,liftn 1 i c)) 1 l
-let rec_branch_scheme env isevars ((sp,j),_) typc recargs =
- let rec crec (typc,recargs) =
- match whd_betadeltaiota env !isevars typc, recargs with
- | (DOP2(Prod,c,DLAM(name,t)),(ra::reca)) ->
- DOP2(Prod,c,
+let rec_branch_scheme env isevars ((sp,j),_) recargs cstr =
+ let rec crec (args,recargs) =
+ match args, recargs with
+ | (name,c)::rea,(ra::reca) ->
+ DOP2(Prod,c,DLAM(name,
match ra with
- | Mrec k ->
- if k=j then
- DLAM(name,mkArrow (mkExistential isevars env)
- (crec (lift 1 t,reca)))
- else
- DLAM(name,crec (t,reca))
- | _ -> DLAM(name,crec (t,reca)))
- | (_,_) -> mkExistential isevars env
+ | Mrec k when k=j ->
+ mkArrow (mkExistential isevars env)
+ (crec (lift_args rea,reca))
+ | _ -> crec (rea,reca)))
+ | [],[] -> mkExistential isevars env
+ | _ -> anomaly "rec_branch_scheme"
in
- crec (typc,recargs)
+ crec (List.rev cstr.cs_args,recargs)
-let branch_scheme env isevars isrec i (IndFamily (mis,params) as indf) =
- let typc = type_inst_construct i indf in
+let branch_scheme env isevars isrec (IndFamily (mis,params) as indf) =
+ let cstrs = get_constructors indf in
if isrec then
- let recarg = (mis_recarg mis).(i-1) in
- rec_branch_scheme env isevars (mis_inductive mis) typc recarg
+ array_map2
+ (rec_branch_scheme env isevars (mis_inductive mis))
+ (mis_recarg mis) cstrs
else
- norec_branch_scheme env isevars typc
+ Array.map (norec_branch_scheme env isevars) cstrs
+
+(***************************************************)
+(* Building ML like case expressions without types *)
+
+let concl_n env sigma =
+ let rec decrec m c = if m = 0 then c else
+ match whd_betadeltaiota env sigma c with
+ | DOP2(Prod,_,DLAM(n,c_0)) -> decrec (m-1) c_0
+ | _ -> failwith "Typing.concl_n"
+ in
+ decrec
+
+let count_rec_arg j =
+ let rec crec i = function
+ | [] -> i
+ | (Mrec k::l) -> crec (if k=j then (i+1) else i) l
+ | (_::l) -> crec i l
+ in
+ crec 0
+
+(* Used in Program only *)
+let make_case_ml isrec pred c ci lf =
+ if isrec then
+ DOPN(XTRA("REC"),Array.append [|pred;c|] lf)
+ else
+ mkMutCaseA ci pred c lf
+
+(* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the
+ * K parameters. Then then build_notdep builds the predicate
+ * [a_bar:A'_bar](lift k pred)
+ * where A'_bar = A_bar[p_bar <- globargs] *)
+
+let build_notdep_pred env sigma indf pred =
+ let arsign,_ = get_arity env sigma indf in
+ let nar = List.length arsign in
+ it_lambda_name env (lift nar pred) arsign
+
+let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) =
+ let pred =
+ let mispec,_ = dest_ind_family indf in
+ let recargs = mis_recarg mispec in
+ assert (Array.length recargs <> 0);
+ let recargi = recargs.(i) in
+ let j = mis_index mispec in
+ let nbrec = if isrec then count_rec_arg j recargi else 0 in
+ let nb_arg = List.length (recargs.(i)) + nbrec in
+ let pred = concl_n env sigma nb_arg ft in
+ if noccur_between 1 nb_arg pred then
+ lift (-nb_arg) pred
+ else
+ failwith "Dependent"
+ in
+ if realargs = [] then
+ pred
+ else (* we try with [_:T1]..[_:Tn](lift n pred) *)
+ build_notdep_pred env sigma indf pred
+
+let pred_case_ml env sigma isrec indt lf (i,ft) =
+ pred_case_ml_fail env sigma isrec indt (i,ft)
+
+(* similar to pred_case_ml but does not expect the list lf of braches *)
+let pred_case_ml_onebranch env sigma isrec indt (i,f,ft) =
+ pred_case_ml_fail env sigma isrec indt (i,ft)
(************************************************************************)
(* Pattern-matching compilation (Cases) *)
@@ -429,7 +489,7 @@ let rec recover_pat_names = function
| _,[] -> anomaly "Cases.recover_pat_names: Not enough patterns"
let push_rels_eqn sign eqn =
- let sign' = recover_pat_names (List.rev sign, eqn.patterns) in
+ let sign' = recover_pat_names (sign, eqn.patterns) in
{eqn with
rhs = {eqn.rhs with
rhs_env = push_rels sign' eqn.rhs.rhs_env} }
@@ -563,8 +623,8 @@ let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) =
| Some p -> abstract_predicate env !isevars indf p
| None -> infer_predicate env isevars typs cstrs indf in
let typ = applist (pred, realargs) in
- if dep then (pred, applist (typ, [current]), dummy_sort)
- else (pred, typ, dummy_sort)
+ if dep then (pred, applist (typ, [current]), Type Univ.dummy_univ)
+ else (pred, typ, Type Univ.dummy_univ)
(************************************************************************)
(* Sorting equation by constructor *)
@@ -617,8 +677,7 @@ let build_leaf pb =
let j = pb.typing_function tycon rhs.rhs_env rhs.it in
let subst = (*List.map (fun id -> (id,make_substituend (List.assoc id rhs.subst))) rhs.user_ids *)[] in
{uj_val = replace_vars subst j.uj_val;
- uj_type = replace_vars subst j.uj_type;
- uj_kind = j.uj_kind}
+ uj_type = typed_app (replace_vars subst) j.uj_type }
(* Building the sub-problem when all patterns are variables *)
let shift_problem pb =
@@ -703,14 +762,13 @@ and match_current pb (n,tm) =
let tags = Array.map (pattern_status defaults) eqns in
let brs = Array.map compile pbs in
let brvals = Array.map (fun j -> j.uj_val) brs in
- let brtyps = Array.map (fun j -> j.uj_type) brs in
+ let brtyps = Array.map (fun j -> body_of_type j.uj_type) brs in
let (pred,typ,s) =
find_predicate pb.env pb.isevars
pb.pred brtyps cstrs current indt in
let ci = make_case_info mis None tags in
{ uj_val = mkMutCaseA ci (*eta_reduce_if_rel*) pred current brvals;
- uj_type = typ;
- uj_kind = s }
+ uj_type = make_typed typ s }
and compile_further pb firstnext rest =
(* We pop as much as possible tomatch not dependent one of the other *)
@@ -718,20 +776,21 @@ and compile_further pb firstnext rest =
(* the next pattern to match is at the end of [nexts], it has ref (Rel n)
where n is the length of nexts *)
let sign = List.map (fun ((na,t),_) -> (na,type_of_tomatch_type t)) nexts in
+ let revsign = List.rev sign in
let currents =
list_map_i
(fun i ((na,t),(_,rhsdep)) ->
Pushed (insert_lifted ((Rel i, lift_tomatch_type i t), rhsdep)))
1 nexts in
let pb' = { pb with
- env = push_rels sign pb.env;
+ env = push_rels revsign pb.env;
tomatch = List.rev_append currents future;
pred= option_app (weaken_predicate (List.length sign)) pb.pred;
- mat = List.map (push_rels_eqn sign) pb.mat } in
+ mat = List.map (push_rels_eqn revsign) pb.mat } in
let j = compile pb' in
{ uj_val = lam_it j.uj_val sign;
- uj_type = prod_it j.uj_type sign;
- uj_kind = j.uj_kind }
+ 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 }
(* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -799,25 +858,26 @@ let inh_coerce_to_ind isevars env ty tyi =
let coerce_row typing_fun isevars env row tomatch =
let j = typing_fun empty_tycon env tomatch in
+ let typ = body_of_type j.uj_type in
let t =
match find_row_ind row with
Some (cloc,(cstr,_ as c)) ->
(let tyi = inductive_of_rawconstructor c in
try
- let indtyp = inh_coerce_to_ind isevars env j.uj_type tyi in
- IsInd (j.uj_type,find_inductive env !isevars j.uj_type)
- with NotCoercible ->
- (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
- try
- let mind,_ = find_minductype env !isevars j.uj_type in
- error_bad_constructor_loc cloc CCI
- (constructor_of_rawconstructor c) mind
- with Induc ->
- error_case_not_inductive_loc
- (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type)
+ let indtyp = inh_coerce_to_ind isevars env typ tyi in
+ IsInd (typ,find_inductive env !isevars typ)
+ with NotCoercible ->
+ (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
+ try
+ let mind,_ = find_minductype env !isevars typ in
+ error_bad_constructor_loc cloc CCI
+ (constructor_of_rawconstructor c) mind
+ with Induc ->
+ error_case_not_inductive_loc
+ (loc_of_rawconstr tomatch) CCI env j.uj_val typ)
| None ->
- try IsInd (j.uj_type,find_inductive env !isevars j.uj_type)
- with Induc -> NotInd (j.uj_type)
+ try IsInd (typ,find_inductive env !isevars typ)
+ with Induc -> NotInd typ
in (j.uj_val,t)
let coerce_to_indtype typing_fun isevars env matx tomatchl =
@@ -895,9 +955,9 @@ let case_dependent env sigma loc predj tomatchs =
| (c,NotInd t) ->
errorlabstrm "case_dependent" (error_case_not_inductive CCI env c t)
in
- let etapred = eta_expand env sigma predj.uj_val predj.uj_type in
+ let etapred = eta_expand env sigma predj.uj_val (body_of_type predj.uj_type) in
let n = nb_lam etapred in
- let _,sort = decomp_prod env sigma predj.uj_type in
+ let _,sort = decomp_prod env sigma (body_of_type predj.uj_type) in
let ndepv = List.map nb_dep_ity tomatchs in
let sum = List.fold_right (fun i j -> i+j) ndepv 0 in
let depsum = sum + List.length tomatchs in
@@ -915,7 +975,7 @@ let prepare_predicate typing_fun isevars env tomatchs = function
let cdep,arity = case_dependent env !isevars loc predj1 tomatchs in
(* We got the expected arity of pred and relaunch pretype with it *)
let predj = typing_fun (mk_tycon arity) env pred in
- let etapred = eta_expand env !isevars predj.uj_val predj.uj_type in
+ let etapred = eta_expand env !isevars predj.uj_val (body_of_type predj.uj_type) in
Some (build_initial_predicate cdep etapred tomatchs)
(**************************************************************************)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index fbf77e402..2beb7441c 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -14,7 +14,18 @@ open Evarutil
(* Used for old cases in pretyping *)
val branch_scheme :
- env -> 'a evar_defs -> bool -> int -> inductive_family -> constr
+ env -> 'a evar_defs -> bool -> inductive_family -> constr array
+
+val pred_case_ml_onebranch : env -> 'c evar_map -> bool ->
+ inductive_type -> int * constr * constr -> constr
+
+(*i Utilisés dans Program
+val pred_case_ml : env -> 'c evar_map -> bool ->
+ constr * (inductive * constr list * constr list)
+ -> constr array -> int * constr ->constr
+val make_case_ml :
+ bool -> constr -> constr -> case_info -> constr array -> constr
+i*)
(* Compilation of pattern-matching. *)
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 0d011fcce..db67ac2be 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -294,8 +294,8 @@ 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_type_of env Evd.empty t in
- let vj = {uj_val=v; uj_type=t; uj_kind = k} 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 f_vardep,coef = coe_of_reference v in
if coercion_exists coef then
errorlabstrm "try_add_coercion"
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6141d3025..81d8d2cf4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -18,10 +18,9 @@ open Retyping
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_kind=k} =
+let j_nf_ise env sigma {uj_val=v;uj_type=t} =
{ uj_val = nf_ise1 sigma v;
- uj_type = nf_ise1 sigma t;
- uj_kind = k }
+ uj_type = typed_app (nf_ise1 sigma) t }
let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
@@ -29,8 +28,7 @@ let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
let apply_coercion_args env argl funj =
let rec apply_rec acc typ = function
| [] -> { uj_val=applist(j_val_only funj,argl);
- uj_type= typ;
- uj_kind = funj.uj_kind }
+ uj_type= typed_app (fun _ -> typ) funj.uj_type }
| h::restl ->
(* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
match whd_betadeltaiota env Evd.empty typ with
@@ -39,7 +37,7 @@ let apply_coercion_args env argl funj =
apply_rec (h::acc) (subst1 h c2) restl
| _ -> anomaly "apply_coercion_args"
in
- apply_rec [] funj.uj_type argl
+ apply_rec [] (body_of_type funj.uj_type) argl
(* appliquer le chemin de coercions p a` hj *)
@@ -55,20 +53,20 @@ let apply_pcoercion env p hj typ_cl =
let argl = (class_args_of typ_cl)@[ja.uj_val] in
let jres = apply_coercion_args env argl fv in
(if b then
- {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val}
+ { uj_val=ja.uj_val; uj_type=jres.uj_type }
else
jres),
- jres.uj_type)
+ (body_of_type jres.uj_type))
(hj,typ_cl) p)
with _ ->
failwith "apply_pcoercion"
let inh_app_fun env isevars j =
- match whd_betadeltaiota env !isevars j.uj_type with
+ match whd_betadeltaiota env !isevars (body_of_type j.uj_type) with
| DOP2(Prod,_,DLAM(_,_)) -> j
| _ ->
(try
- let t,i1 = class_of1 env !isevars j.uj_type in
+ let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
let p = lookup_path_to_fun_from i1 in
apply_pcoercion env p j t
with _ -> j)
@@ -76,38 +74,39 @@ let inh_app_fun env isevars j =
let inh_tosort_force env isevars j =
try
- let t,i1 = class_of1 env !isevars j.uj_type in
+ let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
let p = lookup_path_to_sort_from i1 in
apply_pcoercion env p j t
with Not_found ->
j
let inh_tosort env isevars j =
- let typ = whd_betadeltaiota env !isevars j.uj_type in
+ let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
match typ with
| DOP0(Sort _) -> j (* idem inh_app_fun *)
| _ -> (try inh_tosort_force env isevars j with _ -> j)
let inh_ass_of_j env isevars j =
- let typ = whd_betadeltaiota env !isevars j.uj_type in
+ let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
match typ with
- | DOP0(Sort s) -> make_typed j.uj_val s
+ | DOP0(Sort s) -> { utj_val = j.uj_val; utj_type = s }
| _ ->
let j1 = inh_tosort_force env isevars j in
- assumption_of_judgment env !isevars j1
+ type_judgment env !isevars j1
let inh_coerce_to env isevars c1 hj =
let t1,i1 = class_of1 env !isevars c1 in
- let t2,i2 = class_of1 env !isevars hj.uj_type in
+ let t2,i2 = class_of1 env !isevars (body_of_type hj.uj_type) in
let p = lookup_path_between (i2,i1) in
let hj' = apply_pcoercion env p hj t2 in
- if the_conv_x_leq env isevars hj'.uj_type c1 then
+ if the_conv_x_leq env isevars (body_of_type hj'.uj_type) c1 then
hj'
else
failwith "inh_coerce_to"
let rec inh_conv_coerce_to env isevars c1 hj =
- let {uj_val = v; uj_type = t; uj_kind = k} = hj in
+ 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
@@ -130,8 +129,9 @@ let rec inh_conv_coerce_to env isevars c1 hj =
let assv1 = outcast_type v1 in
let env1 = push_rel (x,assv1) env in
let h2 = inh_conv_coerce_to env isevars u2
- {uj_val = v2; uj_type = t2;
- uj_kind = mkSort (get_sort_of env !isevars t2) } in
+ {uj_val = v2;
+ uj_type =
+ make_typed t2 (get_sort_of env !isevars t2) } in
fst (abs_rel env !isevars x assv1 h2)
else
(* let ju1 = exemeta_rec def_vty_con env isevars u1 in
@@ -146,36 +146,36 @@ let rec inh_conv_coerce_to env isevars c1 hj =
let env1 = push_rel (name,assu1) env in
let h1 =
inh_conv_coerce_to env isevars t1
- {uj_val = Rel 1; uj_type = u1;
- uj_kind = mkSort (level_of_type assu1) } in
+ {uj_val = Rel 1;
+ uj_type = typed_app (fun _ -> u1) assu1 } in
let h2 = inh_conv_coerce_to env isevars u2
{ uj_val = DOPN(AppL,[|(lift 1 v);h1.uj_val|]);
- uj_type = subst1 h1.uj_val t2;
- uj_kind = mkSort (get_sort_of env !isevars t2) }
+ uj_type =
+ make_typed (subst1 h1.uj_val t2)
+ (get_sort_of env !isevars t2) }
in
fst (abs_rel env !isevars name assu1 h2)
| _ -> failwith "inh_coerce_to")
let inh_cast_rel loc env isevars cj tj =
+ let tj = assumption_of_judgment env !isevars tj in
let cj' =
try
- inh_conv_coerce_to env isevars tj.uj_val cj
+ inh_conv_coerce_to env isevars (body_of_type tj) cj
with Not_found | Failure _ ->
let rcj = j_nf_ise env !isevars cj in
- let atj = j_nf_ise env !isevars tj in
- error_actual_type_loc loc env rcj.uj_val rcj.uj_type atj.uj_type
+ let atj = nf_ise1 !isevars (body_of_type tj) in
+ error_actual_type_loc loc env rcj.uj_val (body_of_type rcj.uj_type) atj
in
- { uj_val = mkCast cj'.uj_val tj.uj_val;
- uj_type = tj.uj_val;
- uj_kind = whd_betadeltaiota env !isevars tj.uj_type }
+ { uj_val = mkCast cj'.uj_val (body_of_type tj);
+ uj_type = tj }
let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
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= typ;
- uj_kind = funj.uj_kind }
+ uj_type= typed_app (fun _ -> typ) funj.uj_type }
in
(match vtcon with
| (_,(_,Some typ')) ->
@@ -193,7 +193,7 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
(try
inh_conv_coerce_to env isevars c1 hj
with Failure _ | Not_found ->
- error_cant_apply_bad_type_loc apploc env (n,c1,hj.uj_type)
+ error_cant_apply_bad_type_loc apploc env (n,c1,(body_of_type hj.uj_type))
(j_nf_ise env !isevars funj)
(jl_nf_ise env !isevars argjl))
in
@@ -202,5 +202,5 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
error_cant_apply_not_functional_loc apploc env
(j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)
in
- apply_rec 1 [] funj.uj_type argjl
+ apply_rec 1 [] (body_of_type funj.uj_type) argjl
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index cb892ed7c..ec1ab927b 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -18,7 +18,7 @@ val inh_tosort_force :
val inh_tosort :
env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
val inh_ass_of_j :
- env -> 'a evar_defs -> unsafe_judgment -> typed_type
+ env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment
val inh_coerce_to :
env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment
val inh_conv_coerce_to :
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 863843d4f..1b2d287b1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -81,7 +81,7 @@ let split_evar_to_arrow sigma c =
let dsp = num_of_evar (body_of_type dom) in
let rsp = num_of_evar (body_of_type rng) in
(sigma3,
- make_typed (mkEvar dsp args) (Type dummy_univ),
+ { utj_val = mkEvar dsp args; utj_type = Type dummy_univ },
mkCast (mkEvar rsp (array_cons (mkRel 1) args)) dummy_sort)
@@ -377,7 +377,7 @@ let status_changed lev (pbty,t1,t2) =
(* Operations on value/type constraints used in trad and progmach *)
-type trad_constraint = bool * (typed_type option * constr option)
+type trad_constraint = bool * (unsafe_type_judgment option * constr option)
(* Basically, we have the following kind of constraints (in increasing
* strength order):
@@ -416,8 +416,12 @@ let prod_dom_tycon_unif env isevars = function
| DOP2(Prod,c1,_) ->
let t =
match c1 with
- | DOP2 (Cast,cc1,DOP0 (Sort s)) -> make_typed cc1 s
- | _ -> make_typed c1 (Retyping.get_sort_of env !isevars c1)
+ | DOP2 (Cast,cc1,DOP0 (Sort s)) ->
+ { utj_val = cc1;
+ utj_type = s }
+ | _ ->
+ { utj_val = c1;
+ utj_type = Retyping.get_sort_of env !isevars c1 }
in Some t
| t ->
if (ise_undefined isevars t) then begin
@@ -431,7 +435,11 @@ let prod_dom_tycon_unif env isevars = function
* first argument. *)
let app_dom_tycon env isevars (_,(_,tyc)) =
- (false,(None, option_app incast_type (prod_dom_tycon_unif env isevars tyc)))
+ (false,
+ (None,
+ option_app
+ (fun x -> incast_type (Typeops.assumption_of_type_judgment x))
+ (prod_dom_tycon_unif env isevars tyc)))
(* Given a constraint on a term, returns the constraint corresponding to this
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 0758210b1..d9d3dc41b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -50,7 +50,7 @@ val status_changed : int list -> conv_pb * constr * constr -> bool
(* Value/Type constraints *)
-type trad_constraint = bool * (typed_type option * constr option)
+type trad_constraint = bool * (unsafe_type_judgment option * constr option)
val empty_tycon : trad_constraint
val def_vty_con : trad_constraint
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 72eed91c5..23e7b5682 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -136,8 +136,8 @@ let mt_evd = Evd.empty
let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
-let j_nf_ise sigma {uj_val=v;uj_type=t;uj_kind=k} =
- {uj_val=nf_ise1 sigma v;uj_type=nf_ise1 sigma t;uj_kind=k}
+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}
let jv_nf_ise sigma = Array.map (j_nf_ise sigma)
@@ -151,7 +151,8 @@ 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
- (vdefj.(i)).uj_type (lift lt (body_of_type lar.(i)))) then
+ (body_of_type (vdefj.(i)).uj_type)
+ (lift lt (body_of_type 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)
@@ -197,12 +198,10 @@ let pretype_var loc env lvar id =
match lookup_id id (context env) with
| RELNAME (n,typ) ->
{ uj_val = Rel n;
- uj_type = lift n (body_of_type typ);
- uj_kind = DOP0 (Sort (level_of_type typ)) }
+ uj_type = typed_app (lift n) typ }
| GLOBNAME (id,typ) ->
{ uj_val = VAR id;
- uj_type = body_of_type typ;
- uj_kind = DOP0 (Sort (level_of_type typ)) }
+ uj_type = typ }
with Not_found ->
error_var_not_found_loc loc CCI id);;
@@ -251,12 +250,14 @@ let pretype_ref pretype loc isevars env lvar = function
| RConstruct (cstr_sp,ctxt) ->
let cstr = (cstr_sp,Array.map pretype ctxt) in
- let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in
- {uj_val=mkMutConstruct cstr; uj_type=typ; uj_kind=kind}
+ let typ = type_of_constructor env !isevars cstr in
+ { uj_val=mkMutConstruct cstr; uj_type=typ }
let pretype_sort = function
| RProp c -> judge_of_prop_contents c
- | RType -> { uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort}
+ | RType ->
+ { uj_val = dummy_sort;
+ uj_type = make_typed dummy_sort (Type Univ.dummy_univ) }
(* pretype vtcon isevars env constr tries to solve the *)
(* existential variables in constr in environment env with the *)
@@ -284,26 +285,22 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
in
(match kind_of_term metaty with
IsCast (typ,kind) ->
- {uj_val=DOP0 (Meta n); uj_type=typ; uj_kind=kind}
- | _ ->
- {uj_val=DOP0 (Meta n);
- uj_type=metaty;
- uj_kind=failwith "should be casted"}))
+ { uj_val=DOP0 (Meta n); uj_type = outcast_type metaty }
+ | _ -> failwith "should be casted"))
(* hnf_constr !isevars (exemeta_hack metaty).uj_type}) *)
| RHole loc ->
if !compter then nbimpl:=!nbimpl+1;
(match vtcon with
(true,(Some v, _)) ->
- let (valc,typc) = (body_of_type v,mkSort (level_of_type v)) in
- {uj_val=valc; uj_type=typc; uj_kind=dummy_sort}
+ {uj_val=v.utj_val; uj_type=make_typed (mkSort v.utj_type) (Type Univ.dummy_univ)}
| (false,(None,Some ty)) ->
let c = new_isevar isevars env ty CCI in
- {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
+ {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
| (true,(None,None)) ->
let ty = mkCast dummy_sort dummy_sort in
let c = new_isevar isevars env ty CCI in
- {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
+ {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
| (false,(None,None)) ->
(match loc with
None -> anomaly "There is an implicit argument I cannot solve"
@@ -351,13 +348,13 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let rtc = app_rng_tycon env isevars cj.uj_val tycon in
(rtc,cj::jl) in
let jl = List.rev (snd (List.fold_left apply_one_arg
- (mk_tycon j.uj_type,[]) args)) in
+ (mk_tycon (incast_type j.uj_type),[]) args)) in
inh_apply_rel_list !trad_nocheck loc env isevars jl j vtcon
| RBinder(loc,BLambda,name,c1,c2) ->
let j =
pretype (abs_dom_valcon env isevars vtcon) env isevars lvar lmeta c1 in
- let assum = inh_ass_of_j env isevars j in
+ let assum = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
let var = (name,assum) in
let j' =
pretype (abs_rng_tycon env isevars vtcon) (push_rel var env) isevars lvar
@@ -368,7 +365,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
| RBinder(loc,BProd,name,c1,c2) ->
let j = pretype def_vty_con env isevars lvar lmeta c1 in
let assum = inh_ass_of_j env isevars j in
- let var = (name,assum) in
+ let var = (name,assumption_of_type_judgment assum) in
let j' = pretype def_vty_con (push_rel var env) isevars lvar lmeta c2 in
let j'' = inh_tosort env isevars j' in
fst (gen_rel env !isevars name assum j'')
@@ -376,47 +373,50 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
| 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_inductive env !isevars cj.uj_type
+ try find_inductive env !isevars (body_of_type cj.uj_type)
with Induc -> error_case_not_inductive CCI env
- (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
+ (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars (body_of_type cj.uj_type)) in
let pj = match po with
| Some p -> pretype empty_tycon env isevars lvar lmeta p
| None ->
try match vtcon with
(_,(_,Some pred)) ->
let (predc,predt) = destCast pred in
- let predj = {uj_val=predc;uj_type=predt;uj_kind=dummy_sort} in
+ let predj =
+ { uj_val=predc;
+ uj_type=make_typed predt (Type Univ.dummy_univ) } in
inh_tosort env isevars predj
| _ -> error "notype"
with UserError _ -> (* get type information from type of branches *)
+ let expbr = Cases.branch_scheme env isevars isrec indf in
let rec findtype i =
- if i > Array.length lf
+ if i >= Array.length lf
then error_cant_find_case_type_loc loc env cj.uj_val
else
try
- let expti = Cases.branch_scheme env isevars isrec i indf in
+ let expti = expbr.(i) in
let fj =
- pretype (mk_tycon expti) env isevars lvar lmeta lf.(i-1) in
- let efjt = nf_ise1 !isevars fj.uj_type in
+ pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
+ let efjt = nf_ise1 !isevars (body_of_type fj.uj_type) in
let pred =
- Indrec.pred_case_ml_onebranch env !isevars isrec indt
+ 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
- let k = Retyping.get_type_of env !isevars pty in
- {uj_val=pred;uj_type=pty;uj_kind=k}
+ let k = Retyping.get_sort_of env !isevars pty in
+ { uj_val=pred; uj_type=make_typed pty k }
with UserError _ -> findtype (i+1) in
- findtype 1 in
+ findtype 0 in
- let evalct = find_inductive env !isevars cj.uj_type (*Pour normaliser evars*)
- and evalPt = nf_ise1 !isevars pj.uj_type in
+ let evalct = find_inductive env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
+ and evalPt = nf_ise1 !isevars (body_of_type 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 cj.uj_type)
+ (cj.uj_val,nf_ise1 !isevars (body_of_type cj.uj_type))
(Array.length bty)
else
let lfj =
@@ -424,7 +424,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
(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 -> j.uj_type) lfj) in
+ let lft = (Array.map (fun j -> body_of_type j.uj_type) lfj) in
check_branches_message loc env isevars cj.uj_val (bty,lft);
let v =
if isrec
@@ -435,9 +435,9 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let ci = make_default_case_info mis in
mkMutCaseA ci pj.uj_val cj.uj_val (Array.map (fun j-> j.uj_val) lfj)
in
+ let s = destSort (snd (splay_prod env !isevars evalPt)) in
{uj_val = v;
- uj_type = rsty;
- uj_kind = snd (splay_prod env !isevars evalPt)}
+ uj_type = make_typed rsty s }
| RCases (loc,prinfo,po,tml,eqns) ->
Cases.compile_cases
@@ -482,8 +482,7 @@ let j_apply f env sigma j =
| DOP2 (Cast,b,t) -> DOP2 (Cast,f env sigma b,f env sigma t)
| c -> f env sigma c in
{ uj_val=strong (under_outer_cast f) env sigma j.uj_val;
- uj_type=strong f env sigma j.uj_type;
- uj_kind=strong f env sigma j.uj_kind}
+ uj_type= typed_app (strong f env sigma) j.uj_type }
(* TODO: comment faire remonter l'information si le typage a resolu des
variables du sigma original. il faudrait que la fonction de typage
@@ -509,7 +508,7 @@ let ise_resolve fail_evar sigma metamap env lvar lmeta c =
let ise_resolve_type fail_evar sigma metamap env c =
let isevars = ref sigma in
let j = unsafe_fmachine def_vty_con false isevars metamap env [] [] c in
- let tj = inh_ass_of_j env isevars j in
+ let tj = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj
let ise_resolve_nocheck sigma metamap env c =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index e4554527d..b90dc602b 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -46,11 +46,10 @@ let rec type_of env cstr=
| IsRel n -> lift n (body_of_type (snd (lookup_rel n env)))
| IsVar id -> body_of_type (snd (lookup_var id env))
| IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*)
- | IsConst c -> (body_of_type (type_of_constant env sigma c))
+ | IsConst c -> body_of_type (type_of_constant env sigma c)
| IsEvar _ -> type_of_existential env sigma cstr
- | IsMutInd ind -> (body_of_type (type_of_inductive env sigma ind))
- | IsMutConstruct cstr ->
- let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ
+ | IsMutInd ind -> body_of_type (type_of_inductive env sigma ind)
+ | IsMutConstruct cstr -> body_of_type (type_of_constructor env sigma cstr)
| IsMutCase (_,p,c,lf) ->
let IndType (indf,realargs) =
try find_inductive env sigma (type_of env c)
@@ -97,4 +96,4 @@ let get_type_of_with_meta env sigma metamap = fst (typeur sigma metamap) env
let mk_unsafe_judgment env evc c=
let typ=get_type_of env evc c
in
- {uj_val=c;uj_type=typ;uj_kind=(mkSort (get_sort_of env evc typ))};;
+ {uj_val=c;uj_type=make_typed typ (get_sort_of env evc typ)};;
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 92ad4cf5c..873939c91 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -28,7 +28,8 @@ let rec execute mf env sigma cstr =
| IsEvar _ ->
let ty = type_of_existential env sigma cstr in
let jty = execute mf env sigma ty in
- { uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type }
+ let jty = assumption_of_judgment env sigma jty in
+ { uj_val = cstr; uj_type = jty }
| IsRel n ->
relative env n
@@ -49,8 +50,7 @@ let rec execute mf env sigma cstr =
make_judge cstr (type_of_inductive env sigma ind)
| IsMutConstruct cstruct ->
- let (typ,kind) = destCast (type_of_constructor env sigma cstruct) in
- { uj_val = cstr; uj_type = typ; uj_kind = kind }
+ make_judge cstr (type_of_constructor env sigma cstruct)
| IsMutCase (ci,p,c,lf) ->
let cj = execute mf env sigma c in
@@ -88,7 +88,7 @@ let rec execute mf env sigma cstr =
| IsLambda (name,c1,c2) ->
let j = execute mf env sigma c1 in
- let var = assumption_of_judgment env sigma j in
+ let var = assumption_of_judgment env sigma j in
let env1 = push_rel (name,var) env in
let j' = execute mf env1 sigma c2 in
let (j,_) = abs_rel env1 sigma name var j' in
@@ -96,10 +96,11 @@ let rec execute mf env sigma cstr =
| IsProd (name,c1,c2) ->
let j = execute mf env sigma c1 in
- let var = assumption_of_judgment env sigma j in
+ let varj = type_judgment env sigma j in
+ let var = assumption_of_type_judgment varj in
let env1 = push_rel (name,var) env in
let j' = execute mf env1 sigma c2 in
- let (j,_) = gen_rel env1 sigma name var j' in
+ let (j,_) = gen_rel env1 sigma name varj j' in
j
| IsCast (c,t) ->
@@ -146,7 +147,7 @@ let unsafe_machine env sigma constr =
let type_of env sigma c =
let j = safe_machine env sigma c in
- nf_betaiota env sigma j.uj_type
+ nf_betaiota env sigma (body_of_type j.uj_type)
(* The typed type of a judgment. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 03:25:25 +0000