diff options
-rw-r--r-- | dev/top_printers.ml | 9 | ||||
-rw-r--r-- | kernel/declarations.ml | 2 | ||||
-rw-r--r-- | kernel/declarations.mli | 2 | ||||
-rw-r--r-- | kernel/environ.ml | 9 | ||||
-rw-r--r-- | kernel/environ.mli | 7 | ||||
-rw-r--r-- | kernel/indtypes.ml | 3 | ||||
-rw-r--r-- | kernel/indtypes.mli | 2 | ||||
-rw-r--r-- | kernel/inductive.ml | 10 | ||||
-rw-r--r-- | kernel/inductive.mli | 2 | ||||
-rw-r--r-- | kernel/reduction.ml | 6 | ||||
-rw-r--r-- | kernel/reduction.mli | 4 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 31 | ||||
-rw-r--r-- | kernel/safe_typing.mli | 5 | ||||
-rw-r--r-- | kernel/term.ml | 17 | ||||
-rw-r--r-- | kernel/term.mli | 2 | ||||
-rw-r--r-- | kernel/typeops.ml | 130 | ||||
-rw-r--r-- | kernel/typeops.mli | 13 | ||||
-rw-r--r-- | parsing/pretty.ml | 46 | ||||
-rw-r--r-- | parsing/printer.ml | 4 | ||||
-rw-r--r-- | pretyping/cases.ml | 166 | ||||
-rw-r--r-- | pretyping/cases.mli | 13 | ||||
-rw-r--r-- | pretyping/class.ml | 4 | ||||
-rw-r--r-- | pretyping/coercion.ml | 68 | ||||
-rw-r--r-- | pretyping/coercion.mli | 2 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 18 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 83 | ||||
-rw-r--r-- | pretyping/retyping.ml | 9 | ||||
-rw-r--r-- | pretyping/typing.ml | 15 |
29 files changed, 395 insertions, 289 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 35cd38acb..a67f15e8e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -38,13 +38,10 @@ let prvar ((id,a)) = pP [< 'sTR"#" ; 'sTR(string_of_id id) ; 'sTR":" ; term0 (gLOB nil_sign) a >] -let genprj f j = [< (f (gLOB nil_sign)j.uj_val); - 'sTR " : "; - (f (gLOB nil_sign)j.uj_type); - 'sTR " : "; - (f (gLOB nil_sign)j.uj_kind)>] +let genprj f j = + let (c,t) = Termast.with_casts f j in [< c; 'sTR " : "; t >] -let prj j = pP (genprj term0 j) +let prj j = pP (genprj prjudge j) let prsp sp = pP[< 'sTR(string_of_path sp) >] diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d97bb916b..a48384389 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -47,7 +47,7 @@ type recarg = type one_inductive_body = { mind_consnames : identifier array; mind_typename : identifier; - mind_lc : constr array; + mind_lc : typed_type array; mind_arity : typed_type; mind_sort : sorts; mind_nrealargs : int; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index d05c07f14..eab3cb0e4 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -53,7 +53,7 @@ type recarg = type one_inductive_body = { mind_consnames : identifier array; mind_typename : identifier; - mind_lc : constr array; + mind_lc : typed_type array; mind_arity : typed_type; mind_sort : sorts; mind_nrealargs : int; diff --git a/kernel/environ.ml b/kernel/environ.ml index 4f9d4e957..73a8c6487 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -297,9 +297,8 @@ let import cenv env = type unsafe_judgment = { uj_val : constr; - uj_type : constr; - uj_kind : constr } + uj_type : typed_type } -let cast_of_judgment = function - | { uj_val = DOP2 (Cast,_,_) as c } -> c - | { uj_val = c; uj_type = ty } -> mkCast c ty +type unsafe_type_judgment = { + utj_val : constr; + utj_type : sorts } diff --git a/kernel/environ.mli b/kernel/environ.mli index 8f73b9779..c8e3642be 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -96,7 +96,8 @@ val import : compiled_env -> env -> env type unsafe_judgment = { uj_val : constr; - uj_type : constr; - uj_kind : constr } + uj_type : typed_type } -val cast_of_judgment : unsafe_judgment -> constr +type unsafe_type_judgment = { + utj_val : constr; + utj_type : sorts } diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5cedd542c..979d24536 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -293,6 +293,7 @@ let listrec_mconstr env ntypes nparams i indlc = let lna = it_dbenv (fun l na t -> na::l) [] (context env) in Array.map (fun c -> + let c = body_of_type c in try check_construct true (1+nparams) (decomp_par nparams c) with IllFormedInd err -> @@ -330,7 +331,7 @@ let cci_inductive env env_ar kind nparams finite inds cst = (fun acc (_,ar,_,_,_,lc) -> Idset.union (global_vars_set (body_of_type ar)) (Array.fold_left - (fun acc c -> Idset.union (global_vars_set c) acc) + (fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc) acc lc)) Idset.empty inds diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index c35459454..5a7f040d9 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -60,7 +60,7 @@ val mind_check_arities : env -> mutual_inductive_entry -> unit val cci_inductive : env -> env -> path_kind -> int -> bool -> - (identifier * typed_type * identifier list * bool * bool * constr array) + (identifier * typed_type * identifier list * bool * bool * typed_type array) list -> constraints -> mutual_inductive_body diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 85ea816e6..80b60f2ad 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -35,12 +35,14 @@ let mis_typepath mis = let mis_consnames mis = mis.mis_mip.mind_consnames let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args) -let mis_lc mis = +let mis_typed_lc mis = let ids = ids_of_sign mis.mis_mib.mind_hyps in let args = Array.to_list mis.mis_args in - Array.map (fun t -> Instantiate.instantiate_constr ids t args) + Array.map (fun t -> Instantiate.instantiate_type ids t args) mis.mis_mip.mind_lc +let mis_lc mis = Array.map body_of_type (mis_typed_lc mis) + (* gives the vector of constructors and of types of constructors of an inductive definition correctly instanciated *) @@ -57,12 +59,12 @@ let mis_type_mconstructs mispec = Array.map (substl (list_tabulate make_Ik ntypes)) specif) let mis_type_mconstruct i mispec = - let specif = mis_lc mispec + let specif = mis_typed_lc mispec and ntypes = mis_ntypes mispec and nconstr = mis_nconstr mispec in let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in if i > nconstr then error "Not enough constructors in the type"; - substl (list_tabulate make_Ik ntypes) specif.(i-1) + typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1) let mis_typed_arity mis = let idhyps = ids_of_sign mis.mis_mib.mind_hyps diff --git a/kernel/inductive.mli b/kernel/inductive.mli index fa989110c..936c9093a 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -45,7 +45,7 @@ val mis_inductive : inductive_instance -> inductive val mis_arity : inductive_instance -> constr val mis_lc : inductive_instance -> constr array val mis_type_mconstructs : inductive_instance -> constr array * constr array -val mis_type_mconstruct : int -> inductive_instance -> constr +val mis_type_mconstruct : int -> inductive_instance -> typed_type val mis_params_ctxt : inductive_instance -> (name * constr) list val mis_sort : inductive_instance -> sorts diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 85a335ee8..88e42fc86 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1191,11 +1191,12 @@ let is_type_arity env sigma = srec let is_info_type env sigma t = - let s = level_of_type t in + let s = t.utj_type in (s = Prop Pos) || (s <> Prop Null && - try info_arity env sigma (body_of_type t) with IsType -> true) + try info_arity env sigma t.utj_val with IsType -> true) +(* Pour l'extraction let is_info_cast_type env sigma c = match c with | DOP2(Cast,c,t) -> @@ -1205,6 +1206,7 @@ let is_info_cast_type env sigma c = let contents_of_cast_type env sigma c = if is_info_cast_type env sigma c then Pos else Null +*) let is_info_sort = is_info_arity diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9be27fb7c..0d2c39c5f 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -115,9 +115,11 @@ val is_info_arity : env -> 'a evar_map -> constr -> bool val is_info_sort : env -> 'a evar_map -> constr -> bool val is_logic_arity : env -> 'a evar_map -> constr -> bool val is_type_arity : env -> 'a evar_map -> constr -> bool -val is_info_type : env -> 'a evar_map -> typed_type -> bool +val is_info_type : env -> 'a evar_map -> unsafe_type_judgment -> bool +(*i Pour l'extraction val is_info_cast_type : env -> 'a evar_map -> constr -> bool val contents_of_cast_type : env -> 'a evar_map -> constr -> contents +i*) val poly_args : env -> 'a evar_map -> constr -> int list val whd_programs : 'a reduction_function diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 19bf52c84..231aea23a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -19,8 +19,7 @@ open Indtypes type judgment = unsafe_judgment let j_val j = j.uj_val -let j_type j = j.uj_type -let j_kind j = j.uj_kind +let j_type j = body_of_type j.uj_type let vect_lift = Array.mapi lift let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) @@ -68,8 +67,7 @@ let rec execute mf env cstr = (make_judge cstr (type_of_inductive env Evd.empty ind), cst0) | IsMutConstruct c -> - let (typ,kind) =destCast (type_of_constructor env Evd.empty c) in - ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0) + (make_judge cstr (type_of_constructor env Evd.empty c), cst0) | IsMutCase (ci,p,c,lf) -> let (cj,cst1) = execute mf env c in @@ -118,10 +116,11 @@ let rec execute mf env cstr = | IsProd (name,c1,c2) -> let (j,cst1) = execute mf env c1 in - let var = assumption_of_judgment env Evd.empty j in + let varj = type_judgment env Evd.empty j in + let var = assumption_of_type_judgment varj in let env1 = push_rel (name,var) env in let (j',cst2) = execute mf env1 c2 in - let (j,cst3) = gen_rel env1 Evd.empty name var j' in + let (j,cst3) = gen_rel env1 Evd.empty name varj j' in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) @@ -158,12 +157,11 @@ and execute_list mf env = function let (jr,cst2) = execute_list mf env r in (j::jr, Constraint.union cst1 cst2) - (* The typed type of a judgment. *) let execute_type mf env constr = let (j,cst) = execute mf env constr in - (assumption_of_judgment env Evd.empty j, cst) + (type_judgment env Evd.empty j, cst) (* Exported machines. First safe machines, with no general fixpoint @@ -202,7 +200,7 @@ let unsafe_machine_type env constr = (* ``Type of'' machines. *) let type_of env c = - let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type + let (j,_) = safe_machine env c in nf_betaiota env Evd.empty (body_of_type j.uj_type) (* obsolètes let type_of_type env c = @@ -280,12 +278,12 @@ let add_constant_with_value sp body typ env = let (jt,cst') = safe_machine env ty in let env'' = add_constraints cst' env' in try - let cst'' = conv env'' Evd.empty jb.uj_type jt.uj_val in + let cst'' = conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val in let env'' = add_constraints cst'' env'' in (env'', assumption_of_judgment env'' Evd.empty jt, Constraint.union cst' cst'') with NotConvertible -> - error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val + error_actual_type CCI env jb.uj_val (body_of_type jb.uj_type) jt.uj_val in let ids = Idset.union (global_vars_set body) (global_vars_set (body_of_type ty)) @@ -353,12 +351,13 @@ let max_universe (s1,cst1) (s2,cst2) g = let rec infos_and_sort env t = match kind_of_term t with | IsProd (name,c1,c2) -> - let (var,cst1) = safe_machine_type env c1 in + let (varj,cst1) = safe_machine_type env c1 in + let var = assumption_of_type_judgment varj in let env1 = Environ.push_rel (name,var) env in let (infos,smax,cst) = infos_and_sort env1 c2 in - let s1 = level_of_type var in + let s1 = varj.utj_type in let smax',cst' = max_universe (s1,cst1) (smax,cst) (universes env) in - let logic = not (is_info_type env Evd.empty var) in + let logic = not (is_info_type env Evd.empty varj) in let small = is_small s1 in ((logic,small) :: infos, smax', cst') | IsCast (c,t) -> infos_and_sort env c @@ -400,7 +399,7 @@ let type_one_constructor env_ar nparams arsort c = let (j,cst2) = safe_machine_type env_ar c in (*C'est idiot, cst1 et cst2 sont essentiellement des copies l'un de l'autre*) let cst3 =enforce_type_constructor arsort max (Constraint.union cst1 cst2) in - (infos, j, cst3) + (infos, assumption_of_type_judgment j, cst3) let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) = let arsort = sort_of_arity env_ar ar in @@ -412,7 +411,7 @@ let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) = vc ([],[],Constraint.empty) in - let vc' = Array.of_list (List.map incast_type jlc) in + let vc' = Array.of_list jlc in let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in let (_,tyar) = lookup_rel (ninds+1-i) env_ar in ((id,tyar,cnames,issmall,isunit,vc'), cst') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 07857dea9..4ed912d4c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -53,13 +53,12 @@ val import : compiled_env -> safe_environment -> safe_environment val env_of_safe_env : safe_environment -> env +(*i For debug (*s Typing without information. *) - type judgment val j_val : judgment -> constr val j_type : judgment -> constr -val j_kind : judgment -> constr val safe_machine : safe_environment -> constr -> judgment * constraints val safe_machine_type : safe_environment -> constr -> typed_type * constraints @@ -81,5 +80,5 @@ i*) (*s Typing with information (extraction). *) type information = Logic | Inf of judgment - +i*) diff --git a/kernel/term.ml b/kernel/term.ml index 6b8e094b9..e97a2b219 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -68,7 +68,7 @@ type constr = sorts oper term type 'a judge = { body : constr; typ : 'a } -(**) +(* type typed_type = sorts judge type typed_term = typed_type judge @@ -84,8 +84,10 @@ let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ))) let outcast_type = function DOP2 (Cast, b, DOP0 (Sort s)) -> {body=b; typ=s} | _ -> anomaly "outcast_type: Not an in-casted type judgement" -(**) -(* + +let typed_combine f g t u = { f t.body u.body ; g t.typ u.typ} +*) + type typed_type = constr type typed_term = typed_type judge @@ -98,7 +100,8 @@ let level_of_type t = failwith "N'existe plus" let incast_type tty = tty let outcast_type x = x -*) +let typed_combine f g t u = f t u +(**) (****************************************************************************) (* Functions for dealing with constr terms *) @@ -1481,14 +1484,14 @@ module Htype = struct type t = typed_type type u = (constr -> constr) * (sorts -> sorts) -(**) +(* let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ} let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ +*) (**) -(* let hash_sub (hc,hs) j = hc j let equal j1 j2 = j1==j2 -*) +(**) let hash = Hashtbl.hash end) diff --git a/kernel/term.mli b/kernel/term.mli index cc5a8954d..787f51c63 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -65,6 +65,8 @@ type typed_term = typed_type judge val make_typed : constr -> sorts -> typed_type val typed_app : (constr -> constr) -> typed_type -> typed_type +val typed_combine : (constr -> constr -> constr) -> (sorts -> sorts -> sorts) + -> (typed_type -> typed_type -> typed_type) val body_of_type : typed_type -> constr val level_of_type : typed_type -> sorts diff --git a/kernel/typeops.ml b/kernel/typeops.ml index e227111d0..0a53f6b77 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -17,34 +17,36 @@ open Type_errors let make_judge v tj = { uj_val = v; - uj_type = body_of_type tj; - uj_kind= DOP0 (Sort (level_of_type tj)) } + uj_type = tj } let j_val_only j = j.uj_val (* Faut-il caster ? *) let j_val = j_val_only -let j_val_cast j = mkCast j.uj_val j.uj_type - -let typed_type_of_judgment env sigma j = - match whd_betadeltaiota env sigma j.uj_kind with - | DOP0(Sort s) -> make_typed j.uj_type s - | _ -> error_not_type CCI env j.uj_type +let j_val_cast j = mkCast j.uj_val (body_of_type j.uj_type) +let typed_type_of_judgment env sigma j = j.uj_type let assumption_of_judgment env sigma j = - match whd_betadeltaiota env sigma j.uj_type with + match whd_betadeltaiota env sigma (body_of_type j.uj_type) with | DOP0(Sort s) -> make_typed j.uj_val s | _ -> error_assumption CCI env j.uj_val +let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type + +let type_judgment env sigma j = + match whd_betadeltaiota env sigma (body_of_type j.uj_type) with + | DOP0(Sort s) -> {utj_val = j.uj_val; utj_type = s } + | _ -> error_assumption CCI env j.uj_val + + (* Type of a de Bruijn index. *) let relative env n = try let (_,typ) = lookup_rel n env in { 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 } with Not_found -> error_unbound_rel CCI env n @@ -99,8 +101,10 @@ let type_of_inductive env sigma i = (* Constructors. *) +(* let type_mconstructs env sigma mind = mis_type_mconstructs (lookup_mind_specif mind env) +*) let type_mconstruct env sigma i mind = mis_type_mconstruct i (lookup_mind_specif mind env) @@ -110,10 +114,6 @@ let type_of_constructor env sigma cstr = (index_of_constructor cstr) (inductive_of_constructor cstr) -let type_inst_construct i (IndFamily (mis,globargs)) = - let tc = mis_type_mconstruct i mis in - prod_applist tc globargs - let type_of_existential env sigma c = Instantiate.existential_type sigma (destEvar c) @@ -121,7 +121,7 @@ let type_of_existential env sigma c = let rec mysort_of_arity env sigma c = match whd_betadeltaiota env sigma c with - | DOP0(Sort( _)) as c' -> c' + | DOP0(Sort(s)) -> s | DOP2(Prod,_,DLAM(_,c2)) -> mysort_of_arity env sigma c2 | _ -> invalid_arg "mysort_of_arity" @@ -209,29 +209,27 @@ let check_branches_message env sigma (c,ct) (explft,lft) = done let type_of_case env sigma ci pj cj lfj = - 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 let indspec = - try find_inductive env sigma cj.uj_type - with Induc -> error_case_not_inductive CCI env cj.uj_val cj.uj_type in + try find_inductive env sigma (body_of_type cj.uj_type) + with Induc -> + error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in let (bty,rslty) = - type_case_branches env sigma indspec pj.uj_type pj.uj_val cj.uj_val in - let kind = mysort_of_arity env sigma pj.uj_type in - check_branches_message env sigma (cj.uj_val,cj.uj_type) (bty,lft); + type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in + let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in + check_branches_message env sigma (cj.uj_val,body_of_type cj.uj_type) (bty,lft); { uj_val = mkMutCaseA ci (j_val pj) (j_val cj) (Array.map j_val lfj); - uj_type = rslty; - uj_kind = kind } + uj_type = make_typed rslty kind } (* Prop and Set *) let judge_of_prop = { uj_val = DOP0(Sort prop); - uj_type = DOP0(Sort type_0); - uj_kind = DOP0(Sort type_1) } + uj_type = make_typed (DOP0(Sort type_0)) type_1 } let judge_of_set = { uj_val = DOP0(Sort spec); - uj_type = DOP0(Sort type_0); - uj_kind = DOP0(Sort type_1) } + uj_type = make_typed (DOP0(Sort type_0)) type_1 } let judge_of_prop_contents = function | Null -> judge_of_prop @@ -242,14 +240,13 @@ let judge_of_prop_contents = function let judge_of_type u = let (uu,uuu,c) = super_super u in { uj_val = DOP0 (Sort (Type u)); - uj_type = DOP0 (Sort (Type uu)); - uj_kind = DOP0 (Sort (Type uuu)) }, + uj_type = make_typed (DOP0(Sort (Type uu))) (Type uuu) }, c let type_of_sort c = match c with - | DOP0 (Sort (Type u)) -> let (uu,cst) = super u in mkType uu, cst - | DOP0 (Sort (Prop _)) -> mkType prop_univ, Constraint.empty + | DOP0 (Sort (Type u)) -> let (uu,cst) = super u in Type uu, cst + | DOP0 (Sort (Prop _)) -> Type prop_univ, Constraint.empty | _ -> invalid_arg "type_of_sort" (* Type of a lambda-abstraction. *) @@ -273,46 +270,52 @@ let sort_of_product_without_univ domsort rangsort = | Prop _ -> rangsort | Type u1 -> Type dummy_univ) +let typed_product_without_universes name var c = + typed_combine (mkProd name) sort_of_product_without_univ var c + +let typed_product env name var c = + (* Gros hack ! *) + let rcst = ref Constraint.empty in + let hacked_sort_of_product s1 s2 = + let (s,cst) = sort_of_product s1 s2 (universes env) in (rcst:=cst; s) in + typed_combine (mkProd name) hacked_sort_of_product var c, !rcst + let abs_rel env sigma name var j = - let rngtyp = whd_betadeltaiota env sigma j.uj_kind in let cvar = incast_type var in - let (s,cst) = - sort_of_product (level_of_type var) (destSort rngtyp) (universes env) in + let typ,cst = typed_product env name var j.uj_type in { uj_val = mkLambda name cvar (j_val j); - uj_type = mkProd name cvar j.uj_type; - uj_kind = mkSort s }, + uj_type = typ }, cst (* Type of a product. *) -let gen_rel env sigma name var j = - let jtyp = whd_betadeltaiota env sigma j.uj_type in - let jkind = whd_betadeltaiota env sigma j.uj_kind in - let j = { uj_val = j.uj_val; uj_type = jtyp; uj_kind = jkind } in - if isprop jkind then - error "Proof objects can only be abstracted" - else - match jtyp with - | DOP0(Sort s) -> - let (s',g) = sort_of_product (level_of_type var) s (universes env) in - let res_type = mkSort s' in - let (res_kind,g') = type_of_sort res_type in - { uj_val = - mkProd name (incast_type var) (j_val_cast j); - uj_type = res_type; - uj_kind = res_kind }, g' - | _ -> +let gen_rel env sigma name varj j = + let var = assumption_of_type_judgment varj in + match whd_betadeltaiota env sigma (body_of_type j.uj_type) with + | DOP0(Sort s) as ts -> + let t = mkCast j.uj_val ts in + let (s',g) = sort_of_product varj.utj_type s (universes env) in + let res_type = mkSort s' in + let (res_kind,g') = type_of_sort res_type in + { uj_val = mkProd name (incast_type var) t; + uj_type = make_typed res_type res_kind }, + g' + | _ -> +(* if is_small (level_of_type j.uj_type) then (* message historique ?? *) + error "Proof objects can only be abstracted" + else +*) error_generalization CCI env (name,var) j.uj_val (* Type of a cast. *) let cast_rel env sigma cj tj = - if is_conv_leq env sigma cj.uj_type tj.uj_val then + let tj = assumption_of_judgment env sigma tj in + if is_conv_leq env sigma (body_of_type cj.uj_type) (body_of_type tj) then { uj_val = j_val_only cj; - uj_type = tj.uj_val; - uj_kind = whd_betadeltaiota env sigma tj.uj_type } + uj_type = tj } else - error_actual_type CCI env cj.uj_val cj.uj_type tj.uj_val + error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) (body_of_type tj) (* Type of an application. *) @@ -320,8 +323,7 @@ let apply_rel_list env sigma nocheck argjl funj = let rec apply_rec n typ cst = function | [] -> { uj_val = applist (j_val_only funj, List.map j_val_only argjl); - uj_type = typ; - uj_kind = funj.uj_kind }, + uj_type = typed_app (fun _ -> typ) funj.uj_type }, cst | hj::restjl -> match whd_betadeltaiota env sigma typ with @@ -330,16 +332,16 @@ let apply_rel_list env sigma nocheck argjl funj = apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl else (try - let c = conv_leq env sigma hj.uj_type c1 in + let c = conv_leq env sigma (body_of_type hj.uj_type) c1 in let cst' = Constraint.union cst c in apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl with NotConvertible -> - error_cant_apply_bad_type CCI env (n,hj.uj_type,c1) + error_cant_apply_bad_type CCI env (n,body_of_type hj.uj_type,c1) funj argjl) | _ -> error_cant_apply_not_functional CCI env funj argjl in - apply_rec 1 funj.uj_type Constraint.empty argjl + apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl (* Fixpoints. *) @@ -808,7 +810,7 @@ let type_fixpoint env sigma lna lar vdefj = try conv_leq env sigma def (lift lt ar) with NotConvertible -> raise (IllBranch i)) env sigma - (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar) + (Array.map (fun j -> body_of_type j.uj_type) vdefj) (Array.map body_of_type lar) with IllBranch i -> error_ill_typed_rec_body CCI env i lna vdefj lar diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 3d2074c97..625a33193 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -25,6 +25,9 @@ val typed_type_of_judgment : env -> 'a evar_map -> unsafe_judgment -> typed_type val assumption_of_judgment : env -> 'a evar_map -> unsafe_judgment -> typed_type +val assumption_of_type_judgment : unsafe_type_judgment -> typed_type +val type_judgment : + env -> 'a evar_map -> unsafe_judgment -> unsafe_type_judgment val relative : env -> int -> unsafe_judgment @@ -32,7 +35,7 @@ val type_of_constant : env -> 'a evar_map -> constant -> typed_type val type_of_inductive : env -> 'a evar_map -> inductive -> typed_type -val type_of_constructor : env -> 'a evar_map -> constructor -> constr +val type_of_constructor : env -> 'a evar_map -> constructor -> typed_type val type_of_existential : env -> 'a evar_map -> constr -> constr @@ -48,12 +51,15 @@ val judge_of_prop_contents : contents -> unsafe_judgment val judge_of_type : universe -> unsafe_judgment * constraints +val typed_product_without_universes : + name -> typed_type -> typed_type -> typed_type + val abs_rel : env -> 'a evar_map -> name -> typed_type -> unsafe_judgment -> unsafe_judgment * constraints val gen_rel : - env -> 'a evar_map -> name -> typed_type -> unsafe_judgment + env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment * constraints val sort_of_product : sorts -> sorts -> universes -> sorts * constraints @@ -79,9 +85,6 @@ open Inductive val find_case_dep_nparams : env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool -(* Returns the type of the [i]$^{th}$ constructor of the inductive family *) -val type_inst_construct : int -> inductive_family -> constr - val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool val keep_hyps : var_context -> Idset.t -> var_context diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 55664cf1e..c7fcbd729 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -44,7 +44,7 @@ let print_closed_sections = ref false let print_typed_value_in_env env (trm,typ) = let sign = Environ.var_context env in [< prterm_env (gLOB sign) trm ; 'fNL ; - 'sTR " : "; prterm_env (gLOB sign) typ ; 'fNL >] + 'sTR " : "; prtype_env (gLOB sign) typ ; 'fNL >] let print_typed_value x = print_typed_value_in_env (Global.env ()) x @@ -142,7 +142,9 @@ let print_mutual sp mib = let ass_name = assumptions_for_print (lparsname@(Array.to_list lna)) in let lidC = Array.to_list - (array_map2 (fun id c -> (id,snd (decomp_n_prod env evd nparams c))) + (array_map2 + (fun id c -> + (id,snd (decomp_n_prod env evd nparams (body_of_type c)))) mip.mind_consnames lC) in let plidC = prlist_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >]) (prass ass_name) lidC in @@ -332,14 +334,15 @@ let list_filter_vec f vec = of the object, the assumptions that will make it possible to print its type, and the constr term that represent its type. *) -let print_constructors_head +(* +let print_constructors_head (fn : string -> unit assumptions -> constr -> unit) c lna mip = let lC = mip.mind_lc in let ass_name = assumptions_for_print lna in let lidC = array_map2 (fun id c_0 -> (id,c_0)) mip.mind_consnames lC in - let flid = list_filter_vec (fun (_,c_0) -> head_const c_0 = c) lidC in + let flid = list_filter_vec (fun (_,c_0) -> head_const (body_of_type c_0) = c) lidC in List.iter - (function (id,c_0) -> fn (string_of_id id) ass_name c_0) flid + (function (id,c_0) -> fn (string_of_id id) ass_name (body_of_type c_0)) flid let print_all_constructors_head fn c mib = let mipvec = mib.mind_packets @@ -353,8 +356,17 @@ let print_constructors_rel fn lna mip = let lC = mip.mind_lc in let ass_name = assumptions_for_print lna in let lidC = array_map2 (fun id c -> (id,c)) mip.mind_consnames lC in - let flid = list_filter_vec (fun (_,c) -> isRel (head_const c)) lidC in - List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid + let flid = list_filter_vec (fun (_,c) -> isRel (head_const (body_of_type c))) lidC in + List.iter (function (id,c) -> fn (string_of_id id) ass_name (body_of_type c)) + flid +*) + +let print_constructors fn lna mip = + let ass_name = assumptions_for_print lna in + let _ = + array_map2 (fun id c -> fn (string_of_id id) ass_name (body_of_type c)) + mip.mind_consnames mip.mind_lc + in () let crible (fn : string -> unit assumptions -> constr -> unit) name = let hyps = gLOB (Global.var_context()) in @@ -380,9 +392,10 @@ let crible (fn : string -> unit assumptions -> constr -> unit) name = (fun mip -> Name mip.mind_typename) mib.mind_packets in (match const with | (DOPN(MutInd(sp',tyi),_)) -> - if sp = objsp_of sp' then print_constructors_rel fn lna - (mind_nth_type_packet mib tyi) - | _ -> print_all_constructors_head fn const mib); + if sp = objsp_of sp' then + print_constructors fn lna + (mind_nth_type_packet mib tyi) + | _ -> ()); crible_rec rest | _ -> crible_rec rest) @@ -420,12 +433,11 @@ let print_val env {uj_val=trm;uj_type=typ} = print_typed_value_in_env env (trm,typ) let print_type env {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env (trm, nf_betaiota env Evd.empty typ) + print_typed_value_in_env env (trm, typed_app (nf_betaiota env Evd.empty) typ) let print_eval red_fun env {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env Evd.empty trm - and ntyp = nf_betaiota env Evd.empty typ in - [< 'sTR " = "; print_typed_value_in_env env (ntrm, ntyp) >] + let ntrm = red_fun env Evd.empty trm in + [< 'sTR " = "; print_type env {uj_val = ntrm; uj_type = typ} >] let print_name name = let str = string_of_id name in @@ -471,14 +483,14 @@ let print_opaque_name name = let cb = Global.lookup_constant sp in if is_defined cb then let typ = constant_type env Evd.empty cst in - print_typed_value (constant_value env x, body_of_type typ) + print_typed_value (constant_value env x, typ) else anomaly "print_opaque_name" | IsMutInd ((sp,_),_) -> print_mutual sp (Global.lookup_mind sp) | IsMutConstruct cstr -> let ty = Typeops.type_of_constructor env sigma cstr in - print_typed_value(x, ty) + print_typed_value (x, ty) | IsVar id -> let a = snd(lookup_sign id sign) in print_var (string_of_id id) a @@ -521,7 +533,7 @@ let fprint_var name typ = [< 'sTR ("*** [" ^ name ^ " :"); fprtype typ; 'sTR "]"; 'fNL >] let fprint_judge {uj_val=trm;uj_type=typ} = - [< fprterm trm; 'sTR" : " ; fprterm typ >] + [< fprterm trm; 'sTR" : " ; fprterm (body_of_type typ) >] let unfold_head_fconst = let rec unfrec = function diff --git a/parsing/printer.ml b/parsing/printer.ml index 5a4f8ae5b..89bbdb2e9 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -95,6 +95,10 @@ let prterm = prterm_env (gLOB nil_sign) let prtype_env env typ = prterm_env env (incast_type typ) let prtype = prtype_env (gLOB nil_sign) +let prjudge_env env j = + (prterm_env env j.uj_val, prterm_env env (incast_type j.uj_type)) +let prjudge = prjudge_env (gLOB nil_sign) + (* Plus de "k"... let gentermpr k = gentermpr_core false let gentermpr_at_top k = gentermpr_core true 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. *) |