restricted grammar of :let commands

For now, you can only enter one binding at a time at the REPL, and can
only enter expression bindings rather than type signatures or type
synonyms. It wouldn't be too hard to add type synonyms, but the value
is questionable.

cryptol/REPL/Command.hs

@@ -39,7 +39,7 @@ import qualified Cryptol.Eval.Value as E
 import qualified Cryptol.Testing.Random  as TestR
 import qualified Cryptol.Testing.Exhaust as TestX
 import Cryptol.Parser
-    (parseDeclsWith,parseExprWith,ParseError(),Config(..),defaultConfig,parseModName)
+    (parseLetDeclWith,parseExprWith,ParseError(),Config(..),defaultConfig,parseModName)
 import Cryptol.Parser.Position (emptyRange,getLoc)
 import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.TypeCheck.Subst as T
@@ -562,8 +562,8 @@ replParse parse str = case parse str of
 replParseExpr :: String -> REPL P.Expr
 replParseExpr = replParse $ parseExprWith interactiveConfig
 
-replParseDecls :: String -> REPL [P.Decl]
-replParseDecls = replParse $ parseDeclsWith interactiveConfig
+replParseDecl :: String -> REPL P.Decl
+replParseDecl = replParse $ parseLetDeclWith interactiveConfig
 
 interactiveConfig :: Config
 interactiveConfig = defaultConfig { cfgSource = "<interactive>" }
@@ -659,8 +659,8 @@ bindItVariable expr ty = do
 
 replEvalDecls :: String -> REPL ()
 replEvalDecls str = do
-  decls <- replParseDecls str
-  dgs <- replCheckDecls decls
+  decl <- replParseDecl str
+  dgs <- replCheckDecls [decl]
   liftModuleCmd (M.evalDecls dgs)
 
 replEdit :: String -> REPL Bool

cryptol/REPL/Monad.hs

@@ -51,7 +51,6 @@ import Cryptol.Prims.Types(typeOf)
 import Cryptol.Prims.Syntax(ECon(..),ppPrefix)
 import Cryptol.Eval (EvalError)
 import qualified Cryptol.ModuleSystem as M
-import qualified Cryptol.ModuleSystem.Base as M
 import qualified Cryptol.ModuleSystem.Env as M
 import qualified Cryptol.ModuleSystem.NamingEnv as M
 import Cryptol.Parser (ParseError,ppError)

src/Cryptol/Parser.y

@@ -6,6 +6,7 @@ module Cryptol.Parser
   , parseExpr, parseExprWith
   , parseDecl, parseDeclWith
   , parseDecls, parseDeclsWith
+  , parseLetDecl, parseLetDeclWith
   , parseModName
   , ParseError(..), ppError
   , Layout(..)
@@ -142,6 +143,7 @@ import Paths_cryptol
 %name expr    expr
 %name decl    decl
 %name decls   decls
+%name letDecl let_decl
 %name modName modName
 %tokentype { Located Token }
 %monad { ParseM }
@@ -272,6 +274,17 @@ decl                    :: { Decl }
   | 'type' name tysyn_params '=' type
                            {% at ($1,$5) `fmap` mkTySyn $2 (reverse $3) $5  }
 
+let_decl                :: { Decl }
+  : apat '=' expr          { at ($1,$3) $ DPatBind $1 $3                    }
+  | name apats '=' expr    { at ($1,$4) $
+                             DBind $ Bind { bName      = fmap mkUnqual $1
+                                          , bParams    = reverse $2
+                                          , bDef       = $4
+                                          , bSignature = Nothing
+                                          , bPragmas   = []
+                                          , bMono      = False
+                                          } }
+
 newtype                 :: { Newtype }
   : 'newtype' qname '=' newtype_body
                            { Newtype { nName = $2, nParams = [], nBody = $4 } }
@@ -298,8 +311,6 @@ vdecls                  :: { [Decl] }
   : decl                   { [$1] }
   | vdecls 'v;' decl       { $3 : $1 }
 
-
-
 --------------------------------------------------------------------------------
 -- if a then b else c : [10]
 
@@ -730,5 +741,11 @@ parseDeclsWith cfg = parse cfg { cfgModuleScope = False } decls
 parseDecls :: String -> Either ParseError [Decl]
 parseDecls = parseDeclsWith defaultConfig
 
+parseLetDeclWith :: Config -> String -> Either ParseError Decl
+parseLetDeclWith cfg = parse cfg { cfgModuleScope = False } letDecl
+
+parseLetDecl :: String -> Either ParseError Decl
+parseLetDecl = parseLetDeclWith defaultConfig
+
 -- vim: ft=haskell
 }