From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 kernel/clambda.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel/clambda.ml')

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index f1b6f3dffc..d2f59c432b 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -113,7 +113,7 @@ let rec pp_lam lam =
        str")")
   | Lproj(i,kn,arg) ->
     hov 1
-      (str "(proj#" ++ int i ++ spc() ++ pr_con kn ++ str "(" ++ pp_lam arg
+      (str "(proj#" ++ int i ++ spc() ++ Projection.Repr.print kn ++ str "(" ++ pp_lam arg
        ++ str ")")
   | Luint _ ->
     str "(uint)"
@@ -708,10 +708,9 @@ let rec lambda_of_constr env c =
     Lcofix(init, (names, ltypes, lbodies))
 
   | Proj (p,c) ->
-    let pb = lookup_projection p env.global_env in
-    let n = pb.proj_arg in
+    let n = Projection.arg p in
     let lc = lambda_of_constr env c in
-    Lproj (n,Projection.constant p,lc)
+    Lproj (n,Projection.repr p,lc)
 
 and lambda_of_app env f args =
   match Constr.kind f with
-- 
cgit v1.2.3


From 076bb351257dfd3c605c010d95484f224bef5e56 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 10 Jul 2018 15:25:11 +0200
Subject: VM: don't duplicate projection narg information in lproj/kproj

---
 kernel/clambda.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'kernel/clambda.ml')

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
-- 
cgit v1.2.3