VM: don't duplicate projection narg information in lproj/kproj

6 files changed, 13 insertions, 16 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 8030060339..9a1224aab2 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -128,8 +128,7 @@ type instruction =
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
-  | Kproj of int * Projection.Repr.t  (* index of the projected argument,
-                                           name of projection *)
+  | Kproj of Projection.Repr.t
   | Kensurestackcapacity of int
 (* spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (* jump to label *)
@@ -311,7 +310,7 @@ let rec pp_instr i =
 
   | Kbranch lbl -> str "branch " ++ pp_lbl lbl
 
-  | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Projection.Repr.print p
+  | Kproj p -> str "proj " ++ Projection.Repr.print p
 
   | Kensurestackcapacity size -> str "growstack " ++ int size
 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 9c289e87d9..f17a1e657e 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -88,8 +88,7 @@ type instruction =
   | Ksetfield of int                    (** accu[n] = sp[0] ; sp = pop sp *)
   | Kstop
   | Ksequence of bytecodes * bytecodes
-  | Kproj of int * Projection.Repr.t  (** index of the projected argument,
-                                            name of projection *)
+  | Kproj of Projection.Repr.t
   | Kensurestackcapacity of int
 
 (** spiwack: instructions concerning integers *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 6677db2fd9..4613cd3214 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -492,8 +492,8 @@ let rec compile_lam env cenv lam sz cont =
 
   | Lval v -> compile_structured_constant cenv v sz cont
 
-  | Lproj (n,kn,arg) ->
-     compile_lam env cenv arg sz (Kproj (n,kn) :: cont)
+  | Lproj (p,arg) ->
+     compile_lam env cenv arg sz (Kproj p :: cont)
 
   | Lvar id -> pos_named id cenv :: cont
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 7643fdb55f..ca24f9b689 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -284,7 +284,7 @@ let emit_instr env = function
       if n <= 1 then out env (opSETFIELD0+n)
       else (out env opSETFIELD;out_int env n)
   | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
-  | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_proj_name env p
+  | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
   | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
   (* spiwack *)
   | Kbranch lbl -> out env opBRANCH; out_label env lbl
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index 3afef339fb..171ca38830 100644
--- a/kernel/cinstr.mli
+++ b/kernel/cinstr.mli
@@ -36,7 +36,7 @@ and lambda =
   | Lval          of structured_constant
   | Lsort         of Sorts.t
   | Lind          of pinductive
-  | Lproj         of int * Projection.Repr.t * lambda
+  | Lproj         of Projection.Repr.t * lambda
   | Luint         of uint
 
 (* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index d2f59c432b..7c00e40fb0 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -111,9 +111,9 @@ let rec pp_lam lam =
       (str "(PRIM " ++ pr_con kn ++  spc() ++
        prlist_with_sep spc pp_lam  (Array.to_list args) ++
        str")")
-  | Lproj(i,kn,arg) ->
+  | Lproj(p,arg) ->
     hov 1
-      (str "(proj#" ++ int i ++ spc() ++ Projection.Repr.print kn ++ str "(" ++ pp_lam arg
+      (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg
        ++ str ")")
   | Luint _ ->
     str "(uint)"
@@ -205,9 +205,9 @@ let rec map_lam_with_binders g f n lam =
   | Lprim(kn,ar,op,args) ->
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Lprim(kn,ar,op,args')
-  | Lproj(i,kn,arg) ->
+  | Lproj(p,arg) ->
     let arg' = f n arg in
-    if arg == arg' then lam else Lproj(i,kn,arg')
+    if arg == arg' then lam else Lproj(p,arg')
   | Luint u ->
     let u' = map_uint g f n u in
     if u == u' then lam else Luint u'
@@ -376,7 +376,7 @@ let rec occurrence k kind lam =
     let kind = occurrence_args k kind ltypes in
     let _ = occurrence_args (k+Array.length ids) false lbodies in
     kind
-  | Lproj(_,_,arg) ->
+  | Lproj(_,arg) ->
     occurrence k kind arg
   | Luint u -> occurrence_uint k kind u
 
@@ -708,9 +708,8 @@ let rec lambda_of_constr env c =
     Lcofix(init, (names, ltypes, lbodies))
 
   | Proj (p,c) ->
-    let n = Projection.arg p in
     let lc = lambda_of_constr env c in
-    Lproj (n,Projection.repr p,lc)
+    Lproj (Projection.repr p,lc)
 
 and lambda_of_app env f args =
   match Constr.kind f with