Merge PR #9959: [native compiler] Remove `Lconstruct` from lambda code.

Ack-by: maximedenes
Reviewed-by: ppedrot

3 files changed, 33 insertions, 50 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 94ed288d2d..d7ec2ecf72 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -51,7 +51,6 @@ let fresh_lname n =
 (** Global names **)
 type gname = 
   | Gind of string * inductive (* prefix, inductive name *)
-  | Gconstruct of string * constructor (* prefix, constructor name *)
   | Gconstant of string * Constant.t (* prefix, constant name *)
   | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *)
   | Gcase of Label.t option * int
@@ -67,8 +66,6 @@ let eq_gname gn1 gn2 =
   match gn1, gn2 with
   | Gind (s1, ind1), Gind (s2, ind2) ->
      String.equal s1 s2 && eq_ind ind1 ind2
-  | Gconstruct (s1, c1), Gconstruct (s2, c2) ->
-      String.equal s1 s2 && eq_constructor c1 c2
   | Gconstant (s1, c1), Gconstant (s2, c2) ->
       String.equal s1 s2 && Constant.equal c1 c2
   | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) ->
@@ -88,7 +85,7 @@ let eq_gname gn1 gn2 =
   | Ginternal s1, Ginternal s2 -> String.equal s1 s2
   | Grel i1, Grel i2 -> Int.equal i1 i2
   | Gnamed id1, Gnamed id2 -> Id.equal id1 id2
-  | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _
+  | (Gind _| Gconstant _ | Gproj _ | Gcase _ | Gpred _
     | Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ ->
       false
 
@@ -100,19 +97,17 @@ open Hashset.Combine
 let gname_hash gn = match gn with
 | Gind (s, ind) ->
    combinesmall 1 (combine (String.hash s) (ind_hash ind))
-| Gconstruct (s, c) ->
-   combinesmall 2 (combine (String.hash s) (constructor_hash c))
 | Gconstant (s, c) ->
-   combinesmall 3 (combine (String.hash s) (Constant.hash c))
-| Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gnorm (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gnormtbl (l, i) -> combinesmall 8 (combine (Option.hash Label.hash l) (Int.hash i))
-| Ginternal s -> combinesmall 9 (String.hash s)
-| Grel i -> combinesmall 10 (Int.hash i)
-| Gnamed id -> combinesmall 11 (Id.hash id)
-| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i))
+   combinesmall 2 (combine (String.hash s) (Constant.hash c))
+| Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gfixtype (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnorm (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnormtbl (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
+| Ginternal s -> combinesmall 8 (String.hash s)
+| Grel i -> combinesmall 9 (Int.hash i)
+| Gnamed id -> combinesmall 10 (Id.hash id)
+| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (ind_hash p) i))
 
 let case_ctr = ref (-1)
 
@@ -1280,9 +1275,6 @@ let ml_of_instance instance u =
   | Lmakeblock (prefix,(cn,_u),_,args) ->
      let args = Array.map (ml_of_lam env l) args in
      MLconstruct(prefix,cn,args)
-  | Lconstruct (prefix, (cn,u)) ->
-     let uargs = ml_of_instance env.env_univ u in
-      mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs
   | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
@@ -1533,8 +1525,6 @@ let string_of_gname g =
   match g with
   | Gind (prefix, (mind, i)) ->
       Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i
-  | Gconstruct (prefix, ((mind, i), j)) ->
-      Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
   | Gconstant (prefix, c) ->
       Format.sprintf "%sconst_%s" prefix (string_of_con c)
   | Gproj (prefix, (mind, n), i) ->
@@ -1932,16 +1922,6 @@ let compile_mind mb mind stack =
       Glet(name, MLapp (MLprimitive Mk_ind, args))
     in
     let nparams = mb.mind_nparams in
-    let params = 
-      Array.init nparams (fun i -> {lname = param_name; luid = i}) in
-    let add_construct j acc (_,arity) = 
-      let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in 
-      let c = ind, (j+1) in
-	  Glet(Gconstruct ("", c),
-	     mkMLlam (Array.append params args)
-	       (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
-    in
-    let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
     let add_proj proj_arg acc _pb =
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
@@ -1972,7 +1952,7 @@ let compile_mind mb mind stack =
       let _, _, _, pbs = info.(i) in
       Array.fold_left_i add_proj [] pbs
     in
-    projs @ constructors @ gtype :: accu :: stack
+    projs @ gtype :: accu :: stack
   in
   Array.fold_left_i f stack mb.mind_packets
 
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index ec3a7b893d..d88be94b39 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -42,8 +42,6 @@ type lambda =
   | Lmakeblock    of prefix * pconstructor * int * lambda array
                   (* prefix, constructor Name.t, constructor tag, arguments *)
         (* A fully applied constructor *)
-  | Lconstruct    of prefix * pconstructor (* prefix, constructor Name.t *)
-        (* A partially applied constructor *)
   | Luint         of Uint63.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t
@@ -121,7 +119,7 @@ let get_const_prefix env c =
 let map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _
-  | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam
+  | Llazy | Lforce | Lmeta _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -222,7 +220,7 @@ let lam_subst_args subst args =
 let can_subst lam = 
   match lam with
   | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Llam _
-  | Lconstruct _ | Lmeta _ | Levar _ -> true
+  | Lmeta _ | Levar _ -> true
   | _ -> false
 
 let can_merge_if bt bf =
@@ -337,9 +335,20 @@ let make_args start _end =
   Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
     
 (* Translation of constructors *)	
+let expand_constructor prefix cstr tag nparams arity =
+  let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
+  let ids = Array.make (nparams + arity) anon in
+  let args = make_args arity 1 in
+  Llam(ids, Lmakeblock (prefix, cstr, tag, args))
 
-let makeblock env cn u tag args =
-  if Array.for_all is_value args && Array.length args > 0 then
+(* [nparams] is the number of parameters still expected *)
+let makeblock env cn u tag nparams arity args =
+  let nargs = Array.length args in
+  if nparams > 0 || nargs < arity then
+    let prefix = get_mind_prefix env (fst (fst cn)) in
+    mkLapp (expand_constructor prefix (cn,u) tag nparams arity) args
+  else
+  if Array.for_all is_value args && nargs > 0 then
     let args = Array.map get_value args in
     Lval (Nativevalues.mk_block tag args)
   else
@@ -573,16 +582,12 @@ and lambda_of_app cache env sigma f args =
           mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args)
       end
   | Construct (c,u) ->
-      let tag, nparams, arity = Cache.get_construct_info cache env c in
-      let expected = nparams + arity in
-      let nargs = Array.length args in
-      let prefix = get_mind_prefix env (fst (fst c)) in
-      if Int.equal nargs expected then 
-          let args = lambda_of_args cache env sigma nparams args in
-          makeblock env c u tag args
-      else
-        let args = lambda_of_args cache env sigma 0 args in
-            mkLapp (Lconstruct (prefix, (c,u))) args
+    let tag, nparams, arity = Cache.get_construct_info cache env c in
+    let nargs = Array.length args in
+    if nparams < nargs then (* got all parameters *)
+      let args = lambda_of_args cache env sigma nparams args in
+      makeblock env c u tag 0 arity args
+    else makeblock env c u tag (nparams - nargs) arity empty_args
   | _ -> 
       let f = lambda_of_constr cache env sigma f in
       let args = lambda_of_args cache env sigma 0 args in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index b0de257a27..687789e82b 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -36,8 +36,6 @@ type lambda =
   | Lmakeblock    of prefix * pconstructor * int * lambda array
                   (* prefix, constructor Name.t, constructor tag, arguments *)
         (* A fully applied constructor *)
-  | Lconstruct    of prefix * pconstructor (* prefix, constructor Name.t *)
-        (* A partially applied constructor *)
   | Luint         of Uint63.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t