diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/vnorm.ml | 96 |
1 files changed, 72 insertions, 24 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 46af784dda..b9c1a5a1c7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -93,19 +93,6 @@ let construct_of_constr_const env tag typ = let construct_of_constr_block = construct_of_constr false -let constr_type_of_idkey env idkey = - match idkey with - | ConstKey cst -> - let const_type = Typeops.type_of_constant_in env cst in - mkConstU cst, const_type - | VarKey id -> - let (_,_,ty) = lookup_named id env in - mkVar id, ty - | RelKey i -> - let n = (nb_rel env - i) in - let (_,_,ty) = lookup_rel n env in - mkRel n, lift n ty - let type_of_ind env (ind, u) = type_of_inductive env (Inductive.lookup_mind_specif env ind, u) @@ -164,9 +151,11 @@ and nf_whd env whd typ = let t = ta.(i) in let _, args = nf_args env vargs t in mkApp(cfd,args) - | Vconstr_const n -> construct_of_constr_const env n typ + | Vconstr_const n -> + construct_of_constr_const env n typ | Vconstr_block b -> let tag = btag b in + let x = tag in let (tag,ofs) = if tag = Cbytecodes.last_variant_tag then match whd_val (bfield b 0) with @@ -177,22 +166,80 @@ and nf_whd env whd typ = let args = nf_bargs env b ofs ctyp in mkApp(capp,args) | Vatom_stk(Aid idkey, stk) -> - let c,typ = constr_type_of_idkey env idkey in - nf_stk env c typ stk - | Vatom_stk(Aind ind, stk) -> - nf_stk env (mkIndU ind) (type_of_ind env ind) stk + constr_type_of_idkey env idkey stk nf_stk +(*let c,typ = constr_type_of_idkey env idkey in + nf_stk env c typ stk *) + | Vatom_stk(Aind ((mi,i) as ind), stk) -> + if Environ.polymorphic_ind ind env then + let mib = Environ.lookup_mind mi env in + let ulen = Univ.UContext.size mib.mind_universes in + match stk with + | Zapp args :: stk' -> + assert (ulen <= nargs args) ; + let inst = + Array.init ulen (fun i -> Vm.uni_lvl_val (arg args i)) + in + let pind = (ind, Univ.Instance.of_array inst) in + nf_stk ~from:ulen env (mkIndU pind) (type_of_ind env pind) stk + | _ -> assert false + else + let pind = (ind, Univ.Instance.empty) in + nf_stk env (mkIndU pind) (type_of_ind env pind) stk + | Vatom_stk(Atype u, stk) -> + mkSort (Type (Vm.instantiate_universe u stk)) + | Vuniv_level lvl -> + assert false + +and constr_type_of_idkey env (idkey : Vars.id_key) stk cont = + match idkey with + | ConstKey cst -> + if Environ.polymorphic_constant cst env then + let cbody = Environ.lookup_constant cst env in + match stk with + | Zapp vargs :: stk' -> + let uargs = Univ.UContext.size cbody.const_universes in + assert (Vm.nargs vargs >= uargs) ; + let uary = Array.init uargs (fun i -> Vm.uni_lvl_val (Vm.arg vargs i)) in + let ui = Univ.Instance.of_array uary in + let ucst = (cst, ui) in + let const_type = Typeops.type_of_constant_in env ucst in + if uargs < Vm.nargs vargs then + let t, args = nf_args env vargs ~from:uargs const_type in + cont env (mkApp (mkConstU ucst, args)) t stk' + else + cont env (mkConstU ucst) const_type stk' + | _ -> assert false + else + begin + let ucst = (cst, Univ.Instance.empty) in + let const_type = Typeops.type_of_constant_in env ucst in + cont env (mkConstU ucst) const_type stk + end + | VarKey id -> + let (_,_,ty) = lookup_named id env in + cont env (mkVar id) ty stk + | RelKey i -> + let n = (nb_rel env - i) in + let (_,_,ty) = lookup_rel n env in + cont env (mkRel n) (lift n ty) stk -and nf_stk env c t stk = +and nf_stk ?from:(from=0) env c t stk = match stk with | [] -> c | Zapp vargs :: stk -> - let t, args = nf_args env vargs t in - nf_stk env (mkApp(c,args)) t stk + if nargs vargs >= from then + let t, args = nf_args ~from:from env vargs t in + nf_stk env (mkApp(c,args)) t stk + else + let rest = from - nargs vargs in + nf_stk ~from:rest env c t stk | Zfix (f,vargs) :: stk -> + assert (from = 0) ; let fa, typ = nf_fix_app env f vargs in let _,_,codom = decompose_prod env typ in nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk | Zswitch sw :: stk -> + assert (from = 0) ; 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 @@ -215,6 +262,7 @@ and nf_stk env c t stk = let ci = case_info sw in nf_stk env (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> + assert (from = 0) ; let p' = Projection.make p true in let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in nf_stk env (mkProj(p',c)) ty stk @@ -240,14 +288,14 @@ and nf_predicate env ind mip params v pT = true, mkLambda(name,dom,body) | _, _ -> false, nf_val env v crazy_type -and nf_args env vargs t = +and nf_args env vargs ?from:(f=0) t = let t = ref t in - let len = nargs vargs in + let len = nargs vargs - f in let args = Array.init len (fun i -> let _,dom,codom = decompose_prod env !t in - let c = nf_val env (arg vargs i) dom in + let c = nf_val env (arg vargs (f+i)) dom in t := subst1 c codom; c) in !t,args |