diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 7d86fad9..e281f22d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -15,6 +15,7 @@ open Environ open Inductive open Reduction open Vm +open Context.Rel.Declaration (*******************************************) (* Calcul de la forme normal d'un terme *) @@ -23,7 +24,7 @@ open Vm let crazy_type = mkSet let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + let (name,dom,codom as res) = destProd (whd_all env t) in match name with | Anonymous -> (Name (Id.of_string "x"), dom, codom) | Name _ -> res @@ -46,12 +47,10 @@ let invert_tag cst tag reloc_tbl = (* Argggg, ces constructeurs de ... qui commencent a 1*) let find_rectype_a env c = - let (t, l) = - let t = whd_betadeltaiota env c in - try destApp t with DestKO -> (t,[||]) in + let (t, l) = decompose_appvect (whd_all env c) in match kind_of_term t with | Ind ind -> (ind, l) - | _ -> raise Not_found + | _ -> assert false (* Instantiate inductives and parameters in constructor type *) @@ -59,11 +58,11 @@ let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in - let ndecls = Context.rel_context_length mib.mind_params_ctxt in + let ndecls = Context.Rel.length mib.mind_params_ctxt in if Int.equal ndecls 0 then ctyp else let _,ctyp = decompose_prod_n_assum ndecls ctyp in - substl (List.rev (Termops.adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) + substl (List.rev (adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) ctyp @@ -140,7 +139,7 @@ and nf_whd env whd typ = let dom = nf_vtype env (dom p) in let name = Name (Id.of_string "x") in let vc = body_of_vfun (nb_rel env) (codom p) in - let codom = nf_vtype (push_rel (name,None,dom) env) vc in + let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) vc in mkProd(name,dom,codom) | Vfun f -> nf_fun env f typ | Vfix(f,None) -> nf_fix env f @@ -208,11 +207,12 @@ and constr_type_of_idkey env (idkey : Vars.id_key) stk = in nf_univ_args ~nb_univs mk env stk | VarKey id -> - let (_,_,ty) = lookup_named id env in + let open Context.Named.Declaration in + let ty = get_type (lookup_named id env) in nf_stk env (mkVar id) ty stk | RelKey i -> let n = (nb_rel env - i) in - let (_,_,ty) = lookup_rel n env in + let ty = get_type (lookup_rel n env) in nf_stk env (mkRel n) (lift n ty) stk and nf_stk ?from:(from=0) env c t stk = @@ -238,7 +238,7 @@ and nf_stk ?from:(from=0) env c t stk = let params,realargs = Util.Array.chop nparams allargs in let pT = hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in - let pT = whd_betadeltaiota env pT in + let pT = whd_all env pT in let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) let btypes = build_branches_type env ind mib mip u params dep p in @@ -266,7 +266,7 @@ and nf_predicate env ind mip params v pT = let vb = body_of_vfun k f in let name,dom,codom = decompose_prod env pT in let dep,body = - nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in + nf_predicate (push_rel (LocalAssum (name,dom)) env) ind mip params vb codom in dep, mkLambda(name,dom,body) | Vfun f, _ -> let k = nb_rel env in @@ -276,7 +276,7 @@ and nf_predicate env ind mip params v pT = let rargs = Array.init n (fun i -> mkRel (n-i)) in let params = if Int.equal n 0 then params else Array.map (lift n) params in let dom = mkApp(mkIndU ind,Array.append params rargs) in - let body = nf_vtype (push_rel (name,None,dom) env) vb in + let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) vb in true, mkLambda(name,dom,body) | _, _ -> false, nf_val env v crazy_type @@ -309,10 +309,10 @@ and nf_fun env f typ = try decompose_prod env typ with DestKO -> (* 27/2/13: Turned this into an anomaly *) - Errors.anomaly + CErrors.anomaly (Pp.strbrk "Returned a functional value in a type not recognized as a product type.") in - let body = nf_val (push_rel (name,None,dom) env) vb codom in + let body = nf_val (push_rel (LocalAssum (name,dom)) env) vb codom in mkLambda(name,dom,body) and nf_fix env f = |