From 211de419bbc9b4f1586b9ebc7dd12c0e8dff3a1c Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Thu, 27 Jun 2019 15:25:26 +0100
Subject: [PATCH] Fix environments for nested names

This was a slight difference from Blodwen that wasn't accounted for -
there might be lets in the nested environment, so when building the
expanded application type, make sure we go under them
---
 src/TTImp/Elab/App.idr            |   2 +
 tests/Main.idr                    |   2 +-
 tests/idris2/basic009/LetCase.idr |  24 +++++++
 tests/idris2/basic009/Stuff.idr   | 102 ++++++++++++++++++++++++++++++
 tests/idris2/basic009/expected    |  15 +++++
 tests/idris2/basic009/input       |   3 +
 tests/idris2/basic009/run         |   3 +
 7 files changed, 150 insertions(+), 1 deletion(-)
 create mode 100644 tests/idris2/basic009/LetCase.idr
 create mode 100644 tests/idris2/basic009/Stuff.idr
 create mode 100644 tests/idris2/basic009/expected
 create mode 100644 tests/idris2/basic009/input
 create mode 100755 tests/idris2/basic009/run

diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr
index 06d519b..be504db 100644
--- a/src/TTImp/Elab/App.idr
+++ b/src/TTImp/Elab/App.idr
@@ -103,6 +103,8 @@ getVarType rigc nest env fc x
       useVars [] sc = sc
       useVars (a :: as) (Bind bfc n (Pi c _ ty) sc) 
            = Bind bfc n (Let c a ty) (useVars (map weaken as) sc)
+      useVars as (Bind bfc n (Let c v ty) sc) 
+           = Bind bfc n (Let c v ty) (useVars (map weaken as) sc)
       useVars _ sc = sc -- Can't happen?
 
 isHole : NF vars -> Bool
diff --git a/tests/Main.idr b/tests/Main.idr
index 24cc1b1..b0b2ffa 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -24,7 +24,7 @@ ttimpTests
 idrisTests : List String
 idrisTests
     = ["basic001", "basic002", "basic003", "basic004", "basic005",
-       "basic006", "basic007",
+       "basic006", "basic007", "basic008", "basic009",
        "coverage001", "coverage002",
        "error001", "error002", "error003", "error004", "error005",
        "error006",
diff --git a/tests/idris2/basic009/LetCase.idr b/tests/idris2/basic009/LetCase.idr
new file mode 100644
index 0000000..64cee16
--- /dev/null
+++ b/tests/idris2/basic009/LetCase.idr
@@ -0,0 +1,24 @@
+import Stuff
+
+data IsSuc : Nat -> Type where
+     Yes : IsSuc (S x)
+
+pred : (x : Nat) -> IsSuc x -> Nat
+pred (S x) Yes = x
+
+test1 : Nat -> Nat
+test1 x = let y = S (S x) in
+              case x of
+                   res => pred y ?foo
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+test2 : Nat -> Nat -> Nat
+test2 x@(S Z) y
+    = case y of
+           res =>
+               let fn : Vect (S Z) Nat -> Nat
+                   fn ys = ?bar
+               in pred x Yes
diff --git a/tests/idris2/basic009/Stuff.idr b/tests/idris2/basic009/Stuff.idr
new file mode 100644
index 0000000..d16af9f
--- /dev/null
+++ b/tests/idris2/basic009/Stuff.idr
@@ -0,0 +1,102 @@
+-- a mini prelude
+
+module Stuff
+
+public export
+data Bool = True | False
+
+public export
+not : Bool -> Bool
+not True = False
+not False = True
+
+public export
+data Maybe a = Nothing | Just a
+
+infixl 4 &&
+
+public export
+(&&) : Bool -> Lazy Bool -> Bool
+(&&) True x = x
+(&&) False x = False
+
+public export
+intToBool : Int -> Bool
+intToBool 0 = False
+intToBool x = True
+
+public export
+ifThenElse : Bool -> Lazy a -> Lazy a -> a
+ifThenElse True t e = t
+ifThenElse False t e = e
+
+public export
+data Nat = Z | S Nat
+
+public export
+fromInteger : Integer -> Nat
+fromInteger x = ifThenElse (intToBool (prim__eq_Integer x 0)) 
+                      Z (S (fromInteger (prim__sub_Integer x 1)))
+
+public export
+plus : Nat -> Nat -> Nat
+plus Z y = y
+plus (S k) y = S (plus k y)
+
+infixr 5 ::
+
+public export
+data List a = Nil | (::) a (List a)
+
+public export
+data Equal : a -> b -> Type where
+     Refl : {0 x : a} -> Equal x x
+
+public export
+data Unit = MkUnit
+
+public export
+data Pair : Type -> Type -> Type where
+     MkPair : {0 a, b : Type} -> (1 x : a) -> (1 y : b) -> Pair a b
+
+public export
+fst : {0 a, b : Type} -> (a, b) -> a
+fst (x, y) = x
+
+public export
+snd : {0 a, b : Type} -> (a, b) -> b
+snd (x, y) = y
+
+%pair Pair fst snd
+
+namespace DPair
+    public export
+    data DPair : (a : Type) -> (a -> Type) -> Type where
+         MkDPair : (x : a) -> p x -> DPair a p
+
+    fst : DPair a p -> a
+    fst (MkDPair x y) = x
+
+    snd : (x : DPair a p) -> p (fst x)
+    snd (MkDPair x y) = y
+
+public export
+data Unrestricted : Type -> Type where
+     Un : (x : a) -> Unrestricted a
+
+public export
+the : (a : Type) -> a -> a
+the _ x = x
+
+public export
+id : a -> a
+id x = x
+
+public export
+data Void : Type where
+
+public export
+data Dec : Type -> Type where
+     Yes : a -> Dec a
+     No : (a -> Void) -> Dec a
+
diff --git a/tests/idris2/basic009/expected b/tests/idris2/basic009/expected
new file mode 100644
index 0000000..63b1b3e
--- /dev/null
+++ b/tests/idris2/basic009/expected
@@ -0,0 +1,15 @@
+1/2: Building Stuff (Stuff.idr)
+2/2: Building LetCase (LetCase.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main>    y : Nat
+   res : Nat
+   x : Nat
+-------------------------------------
+foo : IsSuc (S (S x))
+Main>    x : Nat
+   res : Nat
+   y : Nat
+   ys : Vect (S Z) Nat
+-------------------------------------
+bar : Nat
+Main> Bye for now!
diff --git a/tests/idris2/basic009/input b/tests/idris2/basic009/input
new file mode 100644
index 0000000..7daf818
--- /dev/null
+++ b/tests/idris2/basic009/input
@@ -0,0 +1,3 @@
+:t foo
+:t bar
+:q
diff --git a/tests/idris2/basic009/run b/tests/idris2/basic009/run
new file mode 100755
index 0000000..cf0b5a0
--- /dev/null
+++ b/tests/idris2/basic009/run
@@ -0,0 +1,3 @@
+$1 --no-prelude LetCase.idr < input
+
+rm -rf build