diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 73 |
1 files changed, 37 insertions, 36 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c53305e2..82c732c5 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -79,7 +79,7 @@ let construct_of_constr const env tag typ = (* spiwack : here be a branch for specific decompilation handled by retroknowledge *) try if const then - ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag), + ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (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) @@ -103,7 +103,7 @@ let construct_of_constr_block = construct_of_constr false let type_of_ind env (ind, u) = type_of_inductive env (Inductive.lookup_mind_specif env ind, u) -let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p = +let build_branches_type env sigma (mind,_ as _ind) mib mip u params 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 *) @@ -120,20 +120,17 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p = let codom = let ndecl = List.length decl in let papp = mkApp(lift ndecl p,crealargs) in - 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 params = Array.map (lift ndecl) params in - let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in - mkApp(papp,[|dep_cstr|]) - else papp + let cstr = ith_constructor_of_inductive ind (i+1) in + let relargs = Array.init carity (fun i -> mkRel (carity-i)) in + let params = Array.map (lift ndecl) params in + let dep_cstr = mkApp(mkApp(mkConstructU (cstr,u),params),relargs) in + mkApp(papp,[|dep_cstr|]) in decl, decl_with_letin, codom in Array.mapi build_one_branch mip.mind_nf_lc -let build_case_type dep p realargs c = - if dep then mkApp(mkApp(p, realargs), [|c|]) - else mkApp(p, realargs) +let build_case_type p realargs c = + mkApp(mkApp(p, realargs), [|c|]) (* La fonction de normalisation *) @@ -164,9 +161,9 @@ and nf_whd env sigma whd typ = | Vconstr_block b -> let tag = btag b in let (tag,ofs) = - if tag = Cbytecodes.last_variant_tag then + if tag = Obj.last_non_constant_constructor_tag then match whd_val (bfield b 0) with - | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1) + | Vconstr_const tag -> (tag+Obj.last_non_constant_constructor_tag, 1) | _ -> assert false else (tag, 0) in let capp,ctyp = construct_of_constr_block env tag typ in @@ -205,7 +202,7 @@ and nf_univ_args ~nb_univs mk env sigma stk = and nf_evar env sigma evk stk = let evi = try Evd.find sigma evk with Not_found -> assert false in let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in - let concl = Evd.evar_concl evi in + let concl = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in if List.is_empty hyps then nf_stk env sigma (mkEvar (evk, [||])) concl stk else match stk with @@ -214,11 +211,7 @@ and nf_evar env sigma evk stk = really an invariant? *) (** Let-bound arguments are present in the evar arguments but not in the type, so we turn the let into a product. *) - let drop_body = function - | NamedDecl.LocalAssum _ as d -> d - | NamedDecl.LocalDef (na, _, t) -> NamedDecl.LocalAssum (na, t) - in - let hyps = List.map drop_body hyps in + let hyps = Context.Named.drop_bodies hyps in let fold accu d = Term.mkNamedProd_or_LetIn d accu in let t = List.fold_left fold concl hyps in let t, args = nf_args env sigma args t in @@ -273,10 +266,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in - let pT = whd_all env pT in - let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in + let p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) - let btypes = build_branches_type env sigma ind mib mip u params dep p in + let btypes = build_branches_type env sigma ind mib mip u params p in (* calcul des branches *) let bsw = branch_of_switch (nb_rel env) sw in let mkbranch i (n,v) = @@ -285,8 +277,8 @@ and nf_stk ?from:(from=0) env sigma c t stk = Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin in let branchs = Array.mapi mkbranch bsw in - let tcase = build_case_type dep p realargs c in - let ci = sw.sw_annot.Cbytecodes.ci in + let tcase = build_case_type p realargs c in + let ci = sw.sw_annot.Vmvalues.ci in nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; @@ -295,15 +287,24 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkProj(p',c)) ty stk and nf_predicate env sigma ind mip params v pT = - match whd_val v, kind pT with - | Vfun f, Prod _ -> + match kind (whd_allnolet env pT) with + | LetIn (name,b,t,pT) -> + let body = + nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in + mkLetIn (name,b,t,body) + | Prod (name,dom,codom) -> begin + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in - let name,dom,codom = decompose_prod env pT in - let dep,body = + let body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in - dep, mkLambda(name,dom,body) - | Vfun f, _ -> + mkLambda(name,dom,body) + | _ -> assert false + end + | _ -> + match whd_val v with + | Vfun f -> let k = nb_rel env in let vb = reduce_fun k f in let name = Name (Id.of_string "c") in @@ -312,8 +313,8 @@ and nf_predicate env sigma ind mip params v pT = 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 (LocalAssum (name,dom)) env) sigma vb in - true, mkLambda(name,dom,body) - | _, _ -> false, nf_val env sigma v crazy_type + mkLambda(name,dom,body) + | _ -> assert false and nf_args env sigma vargs ?from:(f=0) t = let t = ref t in @@ -388,9 +389,9 @@ let cbv_vm env sigma c t = if Termops.occur_meta sigma c then CErrors.user_err Pp.(str "vm_compute does not support metas."); (** This evar-normalizes terms beforehand *) - let c = EConstr.to_constr sigma c in - let t = EConstr.to_constr sigma t in - let v = Vconv.val_of_constr env c in + let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in + let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in + let v = Csymtable.val_of_constr env c in EConstr.of_constr (nf_val env sigma v t) let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = |