summaryrefslogtreecommitdiff
path: root/pretyping/nativenorm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/nativenorm.ml')
-rw-r--r--pretyping/nativenorm.ml109
1 files changed, 56 insertions, 53 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 1ed4d21b..4e95ecfe 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -21,8 +21,6 @@ open Nativecode
open Nativevalues
open Context.Rel.Declaration
-module NamedDecl = Context.Named.Declaration
-
(** This module implements normalization by evaluation to OCaml code *)
exception Find_at of int
@@ -125,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
try
if const then
let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
- retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp
+ Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp
else
raise Not_found
with Not_found ->
@@ -134,19 +132,19 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
(mkApp(mkConstructU((ind,i),u), params), ctyp)
-let construct_of_constr const env tag typ =
+let construct_of_constr const env sigma tag typ =
let t, l = app_type env typ in
- match kind t with
+ match EConstr.kind_upto sigma t with
| Ind (ind,u) ->
construct_of_constr_notnative const env tag ind u l
| _ -> assert false
-let construct_of_constr_const env tag typ =
- fst (construct_of_constr true env tag typ)
+let construct_of_constr_const env sigma tag typ =
+ fst (construct_of_constr true env sigma tag typ)
let construct_of_constr_block = construct_of_constr false
-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 *)
@@ -163,20 +161,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 (fst 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,snd ind),params),relargs) in
- mkApp(papp,[|dep_cstr|])
- else papp
+ let cstr = ith_constructor_of_inductive (fst 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,snd ind),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|])
(* normalisation of values *)
@@ -190,6 +185,14 @@ let branch_of_switch lvl ans bs =
bs ci in
Array.init (Array.length tbl) branch
+let get_proj env (ind, proj_arg) =
+ let mib = Environ.lookup_mind (fst ind) env in
+ match Declareops.inductive_make_projection ind mib ~proj_arg with
+ | None ->
+ CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
+ | Some p ->
+ Projection.make p true
+
let rec nf_val env sigma v typ =
match kind_of_value v with
| Vaccu accu -> nf_accu env sigma accu
@@ -204,9 +207,9 @@ let rec nf_val env sigma v typ =
let env = push_rel (LocalAssum (name,dom)) env in
let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
mkLambda(name,dom,body)
- | Vconst n -> construct_of_constr_const env n typ
+ | Vconst n -> construct_of_constr_const env sigma n typ
| Vblock b ->
- let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
+ let capp,ctyp = construct_of_constr_block env sigma (block_tag b) typ in
let args = nf_bargs env sigma b ctyp in
mkApp(capp,args)
@@ -281,9 +284,10 @@ and nf_atom env sigma atom =
let codom = nf_type env sigma (codom vn) in
mkProd(n,dom,codom)
| Ameta (mv,_) -> mkMeta mv
- | Aproj(p,c) ->
+ | Aproj (p, c) ->
let c = nf_accu env sigma c in
- mkProj(Projection.make p true,c)
+ let p = get_proj env p in
+ mkProj(p, c)
| _ -> fst (nf_atom_type env sigma atom)
and nf_atom_type env sigma atom =
@@ -305,13 +309,13 @@ and nf_atom_type env sigma atom =
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
let params,realargs = Array.chop nparams allargs in
+ let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
- hnf_prod_applist env
+ hnf_prod_applist_assum env nparamdecls
(Inductiveops.type_of_inductive env ind) (Array.to_list params) in
- let pT = whd_all env pT in
- let dep, p = nf_predicate env sigma ind mip params p pT in
+ let p = nf_predicate env sigma ind mip params p pT in
(* Calcul du type des branches *)
- let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in
+ let btypes = build_branches_type env sigma (fst ind) mib mip u params p in
(* calcul des branches *)
let bsw = branch_of_switch (nb_rel env) ans bs in
let mkbranch i v =
@@ -320,7 +324,7 @@ and nf_atom_type env sigma atom =
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 a in
+ let tcase = build_case_type p realargs a in
let ci = ans.asw_ci in
mkCase(ci, p, a, branchs), tcase
| Afix(tt,ft,rp,s) ->
@@ -350,7 +354,7 @@ and nf_atom_type env sigma atom =
let env = push_rel (LocalAssum (n,dom)) env in
let codom,s2 = nf_type_sort env sigma (codom vn) in
mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2
- | Aevar(evk, _, args) ->
+ | Aevar(evk,args) ->
nf_evar env sigma evk args
| Ameta(mv,ty) ->
let ty = nf_type env sigma ty in
@@ -358,25 +362,30 @@ and nf_atom_type env sigma atom =
| Aproj(p,c) ->
let c,tc = nf_accu_type env sigma c in
let cj = make_judge c tc in
- let uj = Typeops.judge_of_projection env (Projection.make p true) cj in
+ let p = get_proj env p in
+ let uj = Typeops.judge_of_projection env p cj in
uj.uj_val, uj.uj_type
and nf_predicate env sigma ind mip params v pT =
- match kind_of_value 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 kind_of_value v with
+ | Vfun f ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
- let name,dom,codom =
- try decompose_prod env pT with
- DestKO ->
- CErrors.anomaly
- (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
- 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)
+ | _ -> nf_type env sigma v
+ end
+ | _ ->
+ match kind_of_value v with
+ | Vfun f ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
let name = Name (Id.of_string "c") in
@@ -385,13 +394,13 @@ 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_type (push_rel (LocalAssum (name,dom)) env) sigma vb in
- true, mkLambda(name,dom,body)
- | _, _ -> false, nf_type env sigma v
+ mkLambda(name,dom,body)
+ | _ -> nf_type env sigma v
and nf_evar env sigma evk args =
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 ty = Evd.evar_concl evi in
+ let ty = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
if List.is_empty hyps then begin
assert (Int.equal (Array.length args) 0);
mkEvar (evk, [||]), ty
@@ -399,11 +408,7 @@ and nf_evar env sigma evk args =
else
(** 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 ty hyps in
let ty, args = nf_args env sigma args t in
@@ -412,9 +417,8 @@ and nf_evar env sigma evk args =
mkEvar (evk, Array.rev_of_list args), ty
let evars_of_evar_map sigma =
- { Nativelambda.evars_val = Evd.existential_opt_value sigma;
- Nativelambda.evars_typ = Evd.existential_type sigma;
- Nativelambda.evars_metas = Evd.meta_type sigma }
+ { Nativelambda.evars_val = Evd.existential_opt_value0 sigma;
+ Nativelambda.evars_metas = Evd.meta_type0 sigma }
(* fork perf process, return profiler's process id *)
let start_profiler_linux profile_fn =
@@ -468,13 +472,12 @@ let native_norm env sigma c ty =
if not Coq_config.native_compiler then
user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
else
- let penv = Environ.pre_env env in
(*
Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
*)
let ml_filename, prefix = Nativelib.get_ml_filename () in
- let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in
+ let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in
let profile = get_profiling_enabled () in
match Nativelib.compile ml_filename code ~profile:profile with
| true, fn ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 15:18:35 +0000