diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 37 |
1 files changed, 20 insertions, 17 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b2fa631cd..16eeaa293 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -55,9 +55,11 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib typ params = - let s = ind_subst mind mib in +let type_constructor mind mib u typ params = + let s = ind_subst mind mib u in let ctyp = substl s typ in + let usubst = make_inductive_subst mib u in + let ctyp = subst_univs_constr usubst ctyp in let nparams = Array.length params in if Int.equal nparams 0 then ctyp else @@ -67,11 +69,11 @@ let type_constructor mind mib typ params = let construct_of_constr const env tag typ = - let (mind,_ as ind), allargs = find_rectype_a env typ in + let ((mind,_ as ind), u) as indu, allargs = find_rectype_a env typ in (* spiwack : here be a branch for specific decompilation handled by retroknowledge *) try if const then - ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag), + ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag), typ) (*spiwack: this may need to be changed in case there are parameters in the type which may cause a constant value to have an arity. (type_constructor seems to be all about parameters actually) @@ -84,18 +86,19 @@ let construct_of_constr const env tag typ = let nparams = mib.mind_nparams in let i = invert_tag const tag mip.mind_reloc_tbl in let params = Array.sub allargs 0 nparams in - let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in - (mkApp(mkConstruct(ind,i), params), ctyp) + let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in + (mkApp(mkConstructUi(indu,i), params), ctyp) let construct_of_constr_const env tag typ = fst (construct_of_constr true env tag typ) let construct_of_constr_block = construct_of_constr false +(* FIXME: treatment of universes *) let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> - mkConst cst, Typeops.type_of_constant env cst + mkConst cst, (Environ.lookup_constant cst env).const_type | VarKey id -> let (_,_,ty) = lookup_named id env in mkVar id, ty @@ -104,17 +107,17 @@ let constr_type_of_idkey env idkey = let (_,_,ty) = lookup_rel n env in mkRel n, lift n ty -let type_of_ind env ind = - type_of_inductive env (Inductive.lookup_mind_specif env ind) +let type_of_ind env ind u = + type_of_inductive env (Inductive.lookup_mind_specif env ind, u) -let build_branches_type env (mind,_ as _ind) mib mip params dep p = +let build_branches_type env (mind,_ as _ind) mib mip u params dep p = let rtbl = mip.mind_reloc_tbl in (* [build_one_branch i cty] construit le type de la ieme branche (commence a 0) et les lambda correspondant aux realargs *) let build_one_branch i cty = - let typi = type_constructor mind mib cty params in + let typi = type_constructor mind mib u cty params in let decl,indapp = decompose_prod_assum typi in - let ind,cargs = find_rectype_a env indapp in + let ((ind,u),cargs) = find_rectype_a env indapp in let nparams = Array.length params in let carity = snd (rtbl.(i)) in let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in @@ -123,7 +126,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p = if dep then let cstr = ith_constructor_of_inductive ind (i+1) in let relargs = Array.init carity (fun i -> mkRel (carity-i)) in - let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in + let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in mkApp(papp,[|dep_cstr|]) else papp in @@ -170,7 +173,7 @@ and nf_whd env whd typ = | Vatom_stk(Aiddef(idkey,v), stk) -> nf_whd env (whd_stack v stk) typ | Vatom_stk(Aind ind, stk) -> - nf_stk env (mkInd ind) (type_of_ind env ind) stk + nf_stk env (mkInd ind) (type_of_ind env ind Univ.Instance.empty (*FIXME*)) stk and nf_stk env c t stk = match stk with @@ -183,16 +186,16 @@ and nf_stk env c t stk = let _,_,codom = try decompose_prod env typ with DestKO -> exit 120 in nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> - let (mind,_ as ind),allargs = find_rectype_a env t in + let ((mind,_ as ind), u), allargs = find_rectype_a env t in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in let pT = - hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in + hnf_prod_applist env (type_of_ind env ind u) (Array.to_list params) in let pT = whd_betadeltaiota env pT in let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in (* Calcul du type des branches *) - let btypes = build_branches_type env ind mib mip params dep p in + let btypes = build_branches_type env ind mib mip u params dep p in (* calcul des branches *) let bsw = branch_of_switch (nb_rel env) sw in let mkbranch i (n,v) = |