From d36e804012a87ef1556bdb81be1fbf5c32c482a2 Mon Sep 17 00:00:00 2001
From: Nikita Vilunov <nikita@vilunov.me>
Date: Sat, 6 Jun 2020 21:58:50 +0300
Subject: [PATCH 1/2] ":let" command for REPL

---
 src/Idris/Parser.idr | 17 +++++++++++++++++
 src/Idris/REPL.idr   | 16 ++++++++++++++++
 src/Idris/Syntax.idr |  1 +
 3 files changed, 34 insertions(+)

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index d8b69e006c..febb222eaf 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1707,6 +1707,9 @@ data CmdArg : Type where
      ||| The command takes an expression.
      ExprArg : CmdArg
 
+     ||| The command takes a list of declarations
+     DeclsArg : CmdArg
+
      ||| The command takes a number.
      NumberArg : CmdArg
 
@@ -1721,6 +1724,7 @@ Show CmdArg where
   show NoArg = ""
   show NameArg = "<name>"
   show ExprArg = "<expr>"
+  show DeclsArg = "<decls>"
   show NumberArg = "<number>"
   show OptionArg = "<option>"
   show FileArg = "<filename>"
@@ -1785,6 +1789,18 @@ exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
       tm <- expr pdef "(interactive)" init
       pure (command tm)
 
+declsArgCmd : ParseCmd -> (List PDecl -> REPLCmd) -> String -> CommandDefinition
+declsArgCmd parseCmd command doc = (names, DeclsArg, doc, parse)
+  where
+    names : List String
+    names = extractNames parseCmd
+    parse : Rule REPLCmd
+    parse = do
+      symbol ":"
+      runParseCmd parseCmd
+      tm <- topDecl "(interactive)" init
+      pure (command tm)
+
 optArgCmd : ParseCmd -> (REPLOpt -> REPLCmd) -> Bool -> String -> CommandDefinition
 optArgCmd parseCmd command set doc = (names, OptionArg, doc, parse)
   where
@@ -1845,6 +1861,7 @@ parserCommandsForHelp =
   , noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars "Show remaining proof obligations (metavariables or holes)"
   , noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
   , noArgCmd (ParseREPLCmd ["?", "h", "help"]) Help "Display this help text"
+  , declsArgCmd (ParseKeywordCmd "let") NewDefn "Define a new value"
   ]
 
 export
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index 96b29ebe4d..8d41c30dbe 100644
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@@ -424,6 +424,7 @@ data REPLResult : Type where
   OptionsSet : List REPLOpt -> REPLResult
   LogLevelSet : Nat -> REPLResult
   VersionIs : Version -> REPLResult
+  DefDeclared : REPLResult
   Exited : REPLResult
   Edited : EditResult -> REPLResult
 
@@ -443,6 +444,20 @@ execExp ctm
          pure $ Executed ctm
 
 
+execDecls : {auto c : Ref Ctxt Defs} ->
+            {auto u : Ref UST UState} ->
+            {auto s : Ref Syn SyntaxInfo} ->
+            {auto m : Ref MD Metadata} ->
+            List PDecl -> Core REPLResult
+execDecls decls = do
+  traverse_ execDecl decls
+  pure DefDeclared
+  where
+    execDecl : PDecl -> Core ()
+    execDecl decl = do
+      i <- desugarDecl [] decl
+      traverse_ (processDecl [] (MkNested []) []) i
+
 export
 compileExp : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
@@ -492,6 +507,7 @@ process : {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto o : Ref ROpts REPLOpts} ->
           REPLCmd -> Core REPLResult
+process (NewDefn decls) = execDecls decls
 process (Eval itm)
     = do opts <- get ROpts
          case evalMode opts of
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index e6201e9115..90a6cce031 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -304,6 +304,7 @@ data EditCmd : Type where
 
 public export
 data REPLCmd : Type where
+     NewDefn : List PDecl -> REPLCmd 
      Eval : PTerm -> REPLCmd
      Check : PTerm -> REPLCmd
      PrintDef : Name -> REPLCmd

From 018c17b69a0aa1e678627a5c31b7f17641f5fa4a Mon Sep 17 00:00:00 2001
From: Nikita Vilunov <nikita@vilunov.me>
Date: Sun, 7 Jun 2020 16:40:45 +0300
Subject: [PATCH 2/2] Add :let test

---
 tests/Main.idr                       | 2 +-
 tests/idris2/interpreter002/expected | 3 +++
 tests/idris2/interpreter002/input    | 3 +++
 tests/idris2/interpreter002/run      | 3 +++
 4 files changed, 10 insertions(+), 1 deletion(-)
 create mode 100644 tests/idris2/interpreter002/expected
 create mode 100644 tests/idris2/interpreter002/input
 create mode 100755 tests/idris2/interpreter002/run

diff --git a/tests/Main.idr b/tests/Main.idr
index 8e61c4af4a..43a38b45ce 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -64,7 +64,7 @@ idrisTests
        "interface009", "interface010", "interface011", "interface012",
        "interface013", "interface014", "interface015",
        -- Miscellaneous REPL
-       "interpreter001",
+       "interpreter001", "interpreter002",
        -- Implicit laziness, lazy evaluation
        "lazy001",
        -- QTT and linearity related
diff --git a/tests/idris2/interpreter002/expected b/tests/idris2/interpreter002/expected
new file mode 100644
index 0000000000..5407b91b13
--- /dev/null
+++ b/tests/idris2/interpreter002/expected
@@ -0,0 +1,3 @@
+Main> Main> Main> "Privet, mir!"
+Main> 
+Bye for now!
diff --git a/tests/idris2/interpreter002/input b/tests/idris2/interpreter002/input
new file mode 100644
index 0000000000..e84ecac922
--- /dev/null
+++ b/tests/idris2/interpreter002/input
@@ -0,0 +1,3 @@
+:let i : String
+:let i = "Privet, mir!"
+i
diff --git a/tests/idris2/interpreter002/run b/tests/idris2/interpreter002/run
new file mode 100755
index 0000000000..b153002c60
--- /dev/null
+++ b/tests/idris2/interpreter002/run
@@ -0,0 +1,3 @@
+$1 --no-banner --no-prelude < input
+
+rm -rf build