From 0ac9eb1ab46e5b2796aeb80ff547f0635715d312 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Mon, 16 Jan 2023 11:13:39 +0000
Subject: [PATCH] Fix de Brujin indexing of lambda arguments (#1727)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A lambda:

```
\ { v0 := b0 ; v1 := b1 ; ... ; vn := bn }
```

should be translated to:

```
λ? (λ? ... (λ? (match ?$0, ?$1, ... , ?$n with ...)))
```

i.e the de Brujin index of the values in the match always start from 0.

Fixes: https://github.com/anoma/juvix/issues/1695
---
 .../Compiler/Core/Translation/FromInternal.hs      | 12 +++---------
 test/Internal/Eval/Positive.hs                     |  7 ++++++-
 tests/Internal/positive/HigherOrderLambda.juvix    | 14 ++++++++++++++
 tests/Internal/positive/out/HigherOrderLambda.out  |  1 +
 4 files changed, 24 insertions(+), 10 deletions(-)
 create mode 100644 tests/Internal/positive/HigherOrderLambda.juvix
 create mode 100644 tests/Internal/positive/out/HigherOrderLambda.out

diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index f33b5a8d2..291311f61 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -298,19 +298,13 @@ goLambda l = do
     local
       (over indexTableVarsNum (+ nPatterns))
       (mapM goLambdaClause (l ^. Internal.lambdaClauses))
-  values' <- values
-  let match = mkMatch' (fromList values') (toList ms)
-  return $ foldr (\_ n -> mkLambda' n) match values'
+  let values = take nPatterns (mkVar' <$> [0 ..])
+      match = mkMatch' (fromList values) (toList ms)
+  return $ foldr (\_ n -> mkLambda' n) match values
   where
     nPatterns :: Int
     nPatterns = length (l ^. Internal.lambdaClauses . _head1 . Internal.lambdaPatterns)
 
-    values :: Sem r [Node]
-    values = do
-      varsNum <- asks (^. indexTableVarsNum)
-      let vs = take nPatterns [varsNum ..]
-      return (mkVar' <$> vs)
-
 goAxiomInductive ::
   forall r.
   Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r =>
diff --git a/test/Internal/Eval/Positive.hs b/test/Internal/Eval/Positive.hs
index 7767da0c8..bc0db921b 100644
--- a/test/Internal/Eval/Positive.hs
+++ b/test/Internal/Eval/Positive.hs
@@ -163,5 +163,10 @@ tests =
       "Builtin Inductive type"
       $(mkRelDir ".")
       $(mkRelFile "BuiltinInductive.juvix")
-      $(mkRelFile "out/BuiltinInductive.out")
+      $(mkRelFile "out/BuiltinInductive.out"),
+    PosTest
+      "Higher Order Lambda"
+      $(mkRelDir ".")
+      $(mkRelFile "HigherOrderLambda.juvix")
+      $(mkRelFile "out/HigherOrderLambda.out")
   ]
diff --git a/tests/Internal/positive/HigherOrderLambda.juvix b/tests/Internal/positive/HigherOrderLambda.juvix
new file mode 100644
index 000000000..c2eb3d300
--- /dev/null
+++ b/tests/Internal/positive/HigherOrderLambda.juvix
@@ -0,0 +1,14 @@
+module HigherOrderLambda;
+
+open import Stdlib.Prelude;
+
+map' : {A : Type} → {B : Type} → (A → B) → List A → List B;
+map' f := \{ nil := nil; (h :: t) := f h :: map' f t};
+
+lst : List Nat;
+lst := zero :: one :: nil;
+
+main : IO;
+main := printNatLn (foldr (+) zero (map' ((+) one) lst));
+
+end;
diff --git a/tests/Internal/positive/out/HigherOrderLambda.out b/tests/Internal/positive/out/HigherOrderLambda.out
new file mode 100644
index 000000000..7574e3e74
--- /dev/null
+++ b/tests/Internal/positive/out/HigherOrderLambda.out
@@ -0,0 +1 @@
+suc (suc (suc zero))