edwinb · rgrover · Apr 28, 2020 · Apr 28, 2020
diff --git a/dist/Makefile b/dist/Makefile
@@ -6,7 +6,7 @@ all: idris2
 
 idris2: idris2.c
 	$(MAKE) -C rts
-	$(CC) $(OPT) idris2.c -o idris2 -I rts -L rts -lidris_rts $(GMP_LIB_DIR) -lgmp -lm
+	$(CC) $(OPT) idris2.c -o idris2 -I rts -L rts -lidris_rts $(GMP_LIB_DIR) -lgmp -lm -lreadline
 
 clean:
 	${MAKE} -C rts clean

diff --git a/idris2.ipkg b/idris2.ipkg
@@ -84,6 +84,7 @@ modules =
     Text.Parser.Core,
     Text.Quantity,
     Text.Token,
+    Text.Readline,
 
     TTImp.BindImplicits,
     TTImp.Elab,

diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
@@ -45,6 +45,8 @@ import TTImp.ProcessDecls
 import Control.Catchable
 import Data.NameMap
 
+import Text.Readline
+
 import System
 
 %default covering
@@ -792,16 +794,14 @@ mutual
   repl
       = do ns <- getNS
            opts <- get ROpts
-           coreLift (putStr (prompt (evalMode opts) ++ showSep "." (reverse ns) ++ "> "))
-           inp <- coreLift getLine
-           end <- coreLift $ fEOF stdin
-           if end
-             then do
-               -- start a new line in REPL mode (not relevant in IDE mode)
-               coreLift $ putStrLn ""
-               iputStrLn "Bye for now!"
-              else do res <- interpret inp
-                      handleResult res
+           Just inp <- coreLift $ readline $ prompt (evalMode opts) ++ showSep "." (reverse ns) ++ "> "
+             | Nothing => do
+                -- start a new line in REPL mode (not relevant in IDE mode)
+                coreLift $ putStrLn ""
+                iputStrLn "Bye for now!"
+           coreLift $ addHistory inp
+           res <- interpret inp
+           handleResult res
 
     where
       prompt : REPLEval -> String

diff --git a/src/Text/Readline.idr b/src/Text/Readline.idr
@@ -0,0 +1,20 @@
+module Text.Readline
+
+%include C "readline/readline.h"
+%include C "readline/history.h"
+
+prim_readline : String -> IO String
+prim_readline = foreign FFI_C "readline" (String -> IO String)
+
+export
+readline : String -> IO (Maybe String)
+readline prompt = do
+  s <- prim_readline prompt
+  isNull <- nullStr s
+  if isNull
+     then pure Nothing
+     else pure $ Just s
+
+export
+addHistory : String -> IO ()
+addHistory = foreign FFI_C "add_history" (String -> IO ())
diff --git a/tests/chez/chez001/expected b/tests/chez/chez001/expected
@@ -1,3 +1,5 @@
-[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
 1/1: Building Total (Total.idr)
-Main> Main> Bye for now!
+Main> :exec main
+[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez002/expected b/tests/chez/chez002/expected
@@ -1,3 +1,5 @@
-[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]
 1/1: Building Pythag (Pythag.idr)
-Main> Main> Bye for now!
+Main> :exec printLn (pythag 200)
+[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez003/expected b/tests/chez/chez003/expected
@@ -1,6 +1,8 @@
+1/1: Building IORef (IORef.idr)
+Main> :exec main
 94
 94
 188
 188
-1/1: Building IORef (IORef.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez004/expected b/tests/chez/chez004/expected
@@ -1,3 +1,5 @@
+1/1: Building Buffer (Buffer.idr)
+Main> :exec main
 100
 94
 94.42
@@ -6,5 +8,5 @@
 [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
 Buffer read fail
-1/1: Building Buffer (Buffer.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez005/expected b/tests/chez/chez005/expected
@@ -1,3 +1,5 @@
-(3 ** [2, 4, 6])
 1/1: Building Filter (Filter.idr)
-Main> Main> Bye for now!
+Main> :exec printLn (filter even [S Z,2,3,4,5,6])
+(3 ** [2, 4, 6])
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez006/expected b/tests/chez/chez006/expected
@@ -1,3 +1,5 @@
+1/1: Building TypeCase (TypeCase.idr)
+Main> :exec main
 "Nat"
 "List of Nat"
 "List of Something else"
@@ -9,11 +11,13 @@
 "List of Int"
 43
 42
-1/1: Building TypeCase (TypeCase.idr)
-Main> Main> Main.strangeId is total
-Main> Main.strangeId':
+Main> :total strangeId
+Main.strangeId is total
+Main> :missing strangeId'
+Main.strangeId':
 strangeId' _
-Main> Bye for now!
+Main> :q
+Bye for now!
 1/1: Building TypeCase2 (TypeCase2.idr)
 TypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1:
 Can't match on Nat (Erased argument)

diff --git a/tests/chez/chez007/expected b/tests/chez/chez007/expected
@@ -1,5 +1,7 @@
+1/1: Building TypeCase (TypeCase.idr)
+Main> :exec main
 "Function from Nat to Nat"
 "Function from Nat to Vector of 0 Int"
 "Function on Type"
-1/1: Building TypeCase (TypeCase.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez008/expected b/tests/chez/chez008/expected
@@ -1,5 +1,7 @@
+1/1: Building Nat (Nat.idr)
+Main> :exec main
 1
 1
 1
-1/1: Building Nat (Nat.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez009/expected b/tests/chez/chez009/expected
@@ -1,4 +1,6 @@
+1/1: Building uni (uni.idr)
+Main> :exec main
 42
 ällo
-1/1: Building uni (uni.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez010/expected b/tests/chez/chez010/expected
@@ -1,3 +1,5 @@
+1/1: Building CB (CB.idr)
+Main> :exec main
 9
 Callback coming
 In callback
@@ -7,5 +9,5 @@ In callback with (1, 2)
 3
 9
 'k'
-1/1: Building CB (CB.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez011/expected b/tests/chez/chez011/expected
@@ -1,8 +1,15 @@
+1/1: Building bangs (bangs.idr)
+Main> addm1 (Just 3) (Just 4)
+Just 7
+Main> addm2 (Just 3) (Just 4)
+Just 7
+Main> :exec printThing1
 5
+Main> :exec printThing2
 "12"
+Main> :exec printBool True
 True
+Main> :exec printBool False
 False
-1/1: Building bangs (bangs.idr)
-Main> Just 7
-Main> Just 7
-Main> Main> Main> Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez012/expected b/tests/chez/chez012/expected
@@ -1,4 +1,6 @@
+1/1: Building array (array.idr)
+Main> :exec main
 [Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]
 [Just 1, Just 2, Just 3, Just 4, Just 5]
-1/1: Building array (array.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez013/expected b/tests/chez/chez013/expected
@@ -1,5 +1,7 @@
+1/1: Building Struct (Struct.idr)
+Main> :exec main
 (40, 30)
 "Here": (40, 30)
 Made it!
-1/1: Building Struct (Struct.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez014/expected b/tests/chez/chez014/expected
@@ -1,4 +1,6 @@
+1/1: Building Echo (Echo.idr)
+Main> :exec main
 Received: hello world!
 Received: echo: hello world!
-1/1: Building Echo (Echo.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez015/expected b/tests/chez/chez015/expected
@@ -1,4 +1,6 @@
+1/1: Building Numbers (Numbers.idr)
+Main> :exec main
 [3518437212327232157160858338944, 1537557061787000452679295093927559, 3518437212327232157160858338070, 8051343735302590748651849744, 379]
 [8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]
-1/1: Building Numbers (Numbers.idr)
-Main> Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/chez/chez016/expected b/tests/chez/chez016/expected
@@ -1,3 +1,5 @@
-Running Chez program located in folder with spaces
 1/1: Building Main (Main.idr)
-Main> Main> Bye for now!
+Main> :exec main
+Running Chez program located in folder with spaces
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic001/expected b/tests/idris2/basic001/expected
@@ -1,8 +1,12 @@
 1/1: Building Vect (Vect.idr)
-Main> Main> Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
-Main> (interactive):1:28--1:51:When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat
+Main> :set showtypes
+Main> zipWith plus (Cons Z (Cons (S Z) Nil)) (Cons (S Z) (Cons (S Z) Nil))
+Cons (S Z) (Cons (S (S Z)) []) : Vect (S (S Z)) Nat
+Main> zipWith plus (Cons Z Nil) (Cons (S Z) (Cons Z Nil))
+(interactive):1:28--1:51:When unifying Vect (S (S Z)) Nat and Vect (S Z) Nat
 Mismatch between:
 	S Z
 and
 	Z
-Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic002/expected b/tests/idris2/basic002/expected
@@ -1,6 +1,11 @@
 1/1: Building Do (Do.idr)
-Main> Just (S (S (S Z)))
-Main> Just Z
-Main> Just (S (S (S Z)))
-Main> Just Z
-Main> Bye for now!
+Main> mPatBind (Just (S Z)) (Just (S (S Z)))
+Just (S (S (S Z)))
+Main> mPatBind (Just (S Z)) Nothing
+Just Z
+Main> mLetBind (Just (S Z)) (Just (S (S Z)))
+Just (S (S (S Z)))
+Main> mLetBind (Just (S Z)) Nothing
+Just Z
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic003/expected b/tests/idris2/basic003/expected
@@ -1,8 +1,10 @@
 1/1: Building Ambig1 (Ambig1.idr)
-Main> Bye for now!
+Main> :q
+Bye for now!
 1/1: Building Ambig2 (Ambig2.idr)
 Ambig2.idr:22:21--22:28:While processing right hand side of keepUnique at Ambig2.idr:22:1--24:1:
 Ambiguous elaboration. Possible correct results:
 	Main.Set.toList ?arg
 	Main.Vect.toList ?arg
-Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic004/expected b/tests/idris2/basic004/expected
@@ -1,6 +1,10 @@
 1/2: Building Stuff (Stuff.idr)
 2/2: Building Wheres (Wheres.idr)
-Wheres> [3, 2, 1]
-Wheres> 8
-Wheres> 84
-Wheres> Bye for now!
+Wheres> reverse (1 :: 2 :: 3 :: Nil)
+[3, 2, 1]
+Wheres> foo 4
+8
+Wheres> foo 21
+84
+Wheres> :q
+Bye for now!
diff --git a/tests/idris2/basic005/expected b/tests/idris2/basic005/expected
@@ -2,4 +2,5 @@
 NoInfer.idr:1:7--1:9:Unsolved holes:
 Main.{_:1} introduced at NoInfer.idr:1:7--1:9
 
-Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic006/expected b/tests/idris2/basic006/expected
@@ -1,5 +1,8 @@
 1/2: Building Stuff (Stuff.idr)
 2/2: Building PMLet (PMLet.idr)
-Main> 99
-Main> 64
-Main> Bye for now!
+Main> testLet 0
+99
+Main> testLet 8
+64
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic007/expected b/tests/idris2/basic007/expected
@@ -1,8 +1,14 @@
 1/2: Building Stuff (Stuff.idr)
 2/2: Building DoLocal (DoLocal.idr)
-Main> Just 1
-Main> Just 0
-Main> Just 94
-Main> Nothing
-Main> Nothing
-Main> Bye for now!
+Main> mthings (Just (Just 20)) (Just Nothing)
+Just 1
+Main> mthings (Just Nothing) (Just (Just 54))
+Just 0
+Main> mthings (Just (Just 20)) (Just (Just 54))
+Just 94
+Main> mthings (Just (Just 20)) Nothing
+Nothing
+Main> mthings Nothing (Just (Just 54))
+Nothing
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic008/expected b/tests/idris2/basic008/expected
@@ -1,5 +1,9 @@
 1/1: Building If (If.idr)
-Main> "Zero"
-Main> "Odd"
-Main> "Even"
-Main> Bye for now!
+Main> testZ Z
+"Zero"
+Main> testZ (S (S (S Z)))
+"Odd"
+Main> testZ (S (S (S (S Z))))
+"Even"
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic009/expected b/tests/idris2/basic009/expected
@@ -1,8 +1,10 @@
 1/2: Building Stuff (Stuff.idr)
 2/2: Building LetCase (LetCase.idr)
-Main>    y : Nat
+Main> :t foo
+   y : Nat
    res : Nat
    x : Nat
 -------------------------------------
 foo : IsSuc y
-Main> Bye for now!
+Main> :q
+Bye for now!
diff --git a/tests/idris2/basic010/expected b/tests/idris2/basic010/expected
@@ -1,4 +1,8 @@
 1/1: Building Comp (Comp.idr)
-Main> Main> Main.comp : {0 a : Type} -> {0 c : Type} -> {0 b : Type} -> (b -> c) -> (a -> b) -> a -> c
-Main> Main.comp2 : {0 c : Type} -> {0 b : Type} -> (b -> c) -> {a : Type} -> (a -> b) -> a -> c
-Main> Bye for now!
+Main> :set showimplicits
+Main> :t comp
+Main.comp : {0 a : Type} -> {0 c : Type} -> {0 b : Type} -> (b -> c) -> (a -> b) -> a -> c
+Main> :t comp2
+Main.comp2 : {0 c : Type} -> {0 b : Type} -> (b -> c) -> {a : Type} -> (a -> b) -> a -> c
+Main> :q
+Bye for now!