Imported Upstream version 8.9.0upstream/8.9.0upstream

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 ->