Merge pull request #248 from vilunov/repl-let

":let" command for REPL

src/Idris/Parser.idr

@@ -1711,6 +1711,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
 
@@ -1725,6 +1728,7 @@ Show CmdArg where
   show NoArg = ""
   show NameArg = "<name>"
   show ExprArg = "<expr>"
+  show DeclsArg = "<decls>"
   show NumberArg = "<number>"
   show OptionArg = "<option>"
   show FileArg = "<filename>"
@@ -1789,6 +1793,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
@@ -1849,6 +1865,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

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

src/Idris/Syntax.idr

@@ -305,6 +305,7 @@ data EditCmd : Type where
 
 public export
 data REPLCmd : Type where
+     NewDefn : List PDecl -> REPLCmd 
      Eval : PTerm -> REPLCmd
      Check : PTerm -> REPLCmd
      PrintDef : Name -> REPLCmd

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

tests/idris2/interpreter002/expected

@@ -0,0 +1,3 @@
+Main> Main> Main> "Privet, mir!"
+Main> 
+Bye for now!

tests/idris2/interpreter002/input

@@ -0,0 +1,3 @@
+:let i : String
+:let i = "Privet, mir!"
+i

tests/idris2/interpreter002/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-prelude < input
+
+rm -rf build