Merge branch 'feature/repl-bindings'

cryptol/REPL/Command.hs

@@ -33,12 +33,13 @@ import REPL.Trie
 
 import qualified Cryptol.ModuleSystem as M
 import qualified Cryptol.ModuleSystem.Base as M (preludeName)
+import qualified Cryptol.ModuleSystem.NamingEnv as M
 
 import qualified Cryptol.Eval.Value as E
 import qualified Cryptol.Testing.Random  as TestR
 import qualified Cryptol.Testing.Exhaust as TestX
 import Cryptol.Parser
-    (parseExprWith,ParseError(),Config(..),defaultConfig,parseModName)
+    (parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig,parseModName)
 import Cryptol.Parser.Position (emptyRange,getLoc)
 import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.TypeCheck.Subst as T
@@ -57,6 +58,7 @@ import Data.Char (isSpace,isPunctuation,isSymbol)
 import Data.Function (on)
 import Data.List (intercalate,isPrefixOf)
 import Data.Maybe (fromMaybe,mapMaybe)
+import Data.Monoid (mempty)
 import System.Exit (ExitCode(ExitSuccess))
 import System.Process (shell,createProcess,waitForProcess)
 import qualified System.Process as Process(runCommand)
@@ -126,6 +128,7 @@ instance Ord CommandDescr where
 
 data CommandBody
   = ExprArg     (String   -> REPL ())
+  | DeclsArg    (String   -> REPL ())
   | ExprTypeArg (String   -> REPL ())
   | FilenameArg (FilePath -> REPL ())
   | OptionArg   (String   -> REPL ())
@@ -224,9 +227,14 @@ getPPValOpts =
 
 evalCmd :: String -> REPL ()
 evalCmd str = do
-  (val,_ty) <- replEvalExpr str
-  ppOpts <- getPPValOpts
-  io $ rethrowEvalError $ print $ pp $ E.WithBase ppOpts val
+  ri <- replParseInput str
+  case ri of
+    P.ExprInput expr -> do
+      (val,_ty) <- replEvalExpr expr
+      ppOpts <- getPPValOpts
+      io $ rethrowEvalError $ print $ pp $ E.WithBase ppOpts val
+    P.LetInput decl -> do
+      replEvalDecl decl
 
 qcCmd :: String -> REPL ()
 qcCmd "" =
@@ -238,7 +246,8 @@ qcCmd "" =
                   qcCmd x
 
 qcCmd str =
-  do (val,ty) <- replEvalExpr str
+  do expr <- replParseExpr str
+     (val,ty) <- replEvalExpr expr
      EnvNum testNum  <- getUser "tests"
      case TestX.testableType ty of
        Just (sz,vss) | sz <= toInteger testNum ->
@@ -317,34 +326,70 @@ proveCmd :: String -> REPL ()
 proveCmd str = do
   parseExpr <- replParseExpr str
   (expr, schema) <- replCheckExpr parseExpr
+  denv <- getDynEnv
   -- spexpr <- replSpecExpr expr
   EnvString proverName <- getUser "prover"
   EnvBool iteSolver <- getUser "iteSolver"
   EnvBool verbose <- getUser "debug"
-  result <- liftModuleCmd $ Cryptol.Symbolic.prove (proverName, iteSolver, verbose) (expr, schema)
+  result <- liftModuleCmd $ Cryptol.Symbolic.prove (proverName, iteSolver, verbose)
+                                                   (M.deDecls denv)
+                                                   (expr, schema)
   ppOpts <- getPPValOpts
   case result of
     Left msg        -> io $ putStrLn msg
-    Right Nothing   -> io $ putStrLn "Q.E.D."
-    Right (Just vs) -> io $ print $ hsep (doc : docs) <+> text "= False"
-                         where doc = ppPrec 3 parseExpr -- function application has precedence 3
-                               docs = map (pp . E.WithBase ppOpts) vs
+    Right Nothing   -> do
+      io $ putStrLn "Q.E.D."
+      -- set `it` variable to `True`
+      bindItVariable T.eTrue T.tBit
+    Right (Just tevs) -> do
+      let vs = map (\(_,_,v) -> v) tevs
+          tes = map (\(t,e,_) -> (t,e)) tevs
+          doc = ppPrec 3 parseExpr -- function application has precedence 3
+          docs = map (pp . E.WithBase ppOpts) vs
+      io $ print $ hsep (doc : docs) <+> text "= False"
+      -- bind the counterexamples to `it`
+      case tes of
+        [] -> return ()
+        -- if there's only one argument, just bind it
+        [(t, e)] -> bindItVariable e t
+        -- if there are more than one, tuple them up
+        _ -> bindItVariable texp tty
+               where tty = T.tTuple (map fst tes)
+                     texp = T.ETuple (map snd tes)
 
 satCmd :: String -> REPL ()
 satCmd str = do
   parseExpr <- replParseExpr str
   (expr, schema) <- replCheckExpr parseExpr
+  denv <- getDynEnv
   EnvString proverName <- getUser "prover"
   EnvBool iteSolver <- getUser "iteSolver"
   EnvBool verbose <- getUser "debug"
-  result <- liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose) (expr, schema)
+  result <- liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose)
+                                                 (M.deDecls denv)
+                                                 (expr, schema)
   ppOpts <- getPPValOpts
   case result of
     Left msg        -> io $ putStrLn msg
-    Right Nothing   -> io $ putStrLn "Unsatisfiable."
-    Right (Just vs) -> io $ print $ hsep (doc : docs) <+> text "= True"
-                         where doc = ppPrec 3 parseExpr -- function application has precedence 3
-                               docs = map (pp . E.WithBase ppOpts) vs
+    Right Nothing   -> do
+      io $ putStrLn "Unsatisfiable."
+      -- set `it` variable to `False`
+      bindItVariable T.eFalse T.tBit
+    Right (Just tevs) -> do
+      let vs = map (\(_,_,v) -> v) tevs
+          tes = map (\(t,e,_) -> (t,e)) tevs
+          doc = ppPrec 3 parseExpr -- function application has precedence 3
+          docs = map (pp . E.WithBase ppOpts) vs
+      io $ print $ hsep (doc : docs) <+> text "= True"
+      -- bind the satisfying assignment to `it`
+      case tes of
+        [] -> return ()
+        -- if there's only one argument, just bind it
+        [(t, e)] -> bindItVariable e t
+        -- if there are more than one, tuple them up
+        _ -> bindItVariable texp tty
+               where tty = T.tTuple (map fst tes)
+                     texp = T.ETuple (map snd tes)
 
 specializeCmd :: String -> REPL ()
 specializeCmd str = do
@@ -425,6 +470,7 @@ loadCmd path
         { lName = Just (T.mName m)
         , lPath = path
         }
+      setDynEnv mempty
 
 quitCmd :: REPL ()
 quitCmd  = stop
@@ -460,7 +506,7 @@ browseNewtypes pfx = do
 
 browseVars :: String -> REPL ()
 browseVars pfx = do
-  vars  <- getVars
+  vars <- getVars
   let allNames = vars
           {- This shows the built-ins as well:
              Map.union vars
@@ -561,6 +607,9 @@ replParse parse str = case parse str of
   Right a -> return a
   Left e  -> raise (ParseError e)
 
+replParseInput :: String -> REPL P.ReplInput
+replParseInput = replParse $ parseReplWith interactiveConfig
+
 replParseExpr :: String -> REPL P.Expr
 replParseExpr = replParse $ parseExprWith interactiveConfig
 
@@ -592,13 +641,27 @@ moduleCmdResult (res,ws0) = do
 replCheckExpr :: P.Expr -> REPL (T.Expr,T.Schema)
 replCheckExpr e = liftModuleCmd $ M.checkExpr e
 
+replCheckDecls :: [P.Decl] -> REPL [T.DeclGroup]
+replCheckDecls ds = do
+  npds <- liftModuleCmd $ M.noPat ds
+  denv <- getDynEnv
+  let dnames = M.namingEnv npds
+  ne' <- M.travNamingEnv uniqify dnames
+  let denv' = denv { M.deNames = ne' `M.shadowing` M.deNames denv }
+      undo exn = do
+        -- if typechecking fails, we want to revert changes to the
+        -- dynamic environment and reraise
+        setDynEnv denv
+        raise exn
+  setDynEnv denv'
+  catch (liftModuleCmd $ M.checkDecls npds) undo
+
 replSpecExpr :: T.Expr -> REPL T.Expr
 replSpecExpr e = liftModuleCmd $ S.specialize e
 
-replEvalExpr :: String -> REPL (E.Value, T.Type)
-replEvalExpr str =
-  do expr      <- replParseExpr str
-     (def,sig) <- replCheckExpr expr
+replEvalExpr :: P.Expr -> REPL (E.Value, T.Type)
+replEvalExpr expr =
+  do (def,sig) <- replCheckExpr expr
 
      let range = fromMaybe emptyRange (getLoc expr)
      (def1,ty) <-
@@ -612,11 +675,41 @@ replEvalExpr str =
 
      val <- liftModuleCmd (M.evalExpr def1)
      whenDebug (io (putStrLn (dump def1)))
+     -- add "it" to the namespace
+     bindItVariable def1 ty
      return (val,ty)
   where
   warnDefault ns (x,t) =
         print $ text "Assuming" <+> ppWithNames ns x <+> text "=" <+> pp t
 
+-- | Creates a fresh binding of "it" to the expression given, and adds
+-- it to the current dynamic environment
+bindItVariable :: T.Expr -> T.Type -> REPL ()
+bindItVariable expr ty = do
+  let it = T.QName Nothing (P.Name "it")
+  freshIt <- uniqify it
+  let dg = T.NonRecursive decl
+      schema = T.Forall { T.sVars  = []
+                        , T.sProps = []
+                        , T.sType  = ty
+                        }
+      decl = T.Decl { T.dName       = freshIt
+                    , T.dSignature  = schema
+                    , T.dDefinition = expr
+                    , T.dPragmas    = []
+                    }
+  liftModuleCmd (M.evalDecls [dg])
+  denv <- getDynEnv
+  let en = M.EFromBind (P.Located emptyRange freshIt)
+      nenv' = M.singletonE it en `M.shadowing` M.deNames denv
+  setDynEnv $ denv { M.deNames = nenv' }
+
+replEvalDecl :: P.Decl -> REPL ()
+replEvalDecl decl = do
+  dgs <- replCheckDecls [decl]
+  whenDebug (mapM_ (\dg -> (io (putStrLn (dump dg)))) dgs)
+  liftModuleCmd (M.evalDecls dgs)
+
 replEdit :: String -> REPL Bool
 replEdit file = do
   mb <- io (lookupEnv "EDITOR")
@@ -679,6 +772,7 @@ parseCommand findCmd line = do
   case findCmd cmd of
     [c] -> case cBody c of
       ExprArg     body -> Just (Command (body args'))
+      DeclsArg    body -> Just (Command (body args'))
       ExprTypeArg body -> Just (Command (body args'))
       FilenameArg body -> Just (Command (body =<< expandHome args'))
       OptionArg   body -> Just (Command (body args'))

cryptol/REPL/Haskeline.hs

@@ -136,6 +136,7 @@ cmdComp prefix c = Completion
 cmdArgument :: CommandBody -> CompletionFunc REPL
 cmdArgument ct cursor@(l,_) = case ct of
   ExprArg     _ -> completeExpr cursor
+  DeclsArg    _ -> (completeExpr +++ completeType) cursor
   ExprTypeArg _ -> (completeExpr +++ completeType) cursor
   FilenameArg _ -> completeFilename cursor
   ShellArg _    -> completeFilename cursor

cryptol/REPL/Monad.hs

@@ -23,6 +23,8 @@ module REPL.Monad (
 
     -- ** Environment
   , getModuleEnv, setModuleEnv
+  , getDynEnv, setDynEnv
+  , uniqify
   , getTSyns, getNewtypes, getVars
   , whenDebug
   , getExprNames
@@ -49,6 +51,8 @@ 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.Env as M
+import qualified Cryptol.ModuleSystem.NamingEnv as M
 import Cryptol.Parser (ParseError,ppError)
 import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
 import Cryptol.Parser.NoPat (Error)
@@ -58,10 +62,12 @@ import Cryptol.Utils.Panic (panic)
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Symbolic (proverNames)
 
-import Control.Monad (unless,when)
+import Control.Applicative (Applicative(..))
+import Control.Monad (ap,unless,when)
 import Data.IORef
     (IORef,newIORef,readIORef,modifyIORef)
 import Data.List (isPrefixOf)
+import Data.Monoid (Monoid(..))
 import Data.Typeable (Typeable)
 import System.Console.ANSI (setTitle)
 import qualified Control.Exception as X
@@ -81,6 +87,7 @@ data RW = RW
   , eContinue   :: Bool
   , eIsBatch    :: Bool
   , eModuleEnv  :: M.ModuleEnv
+  , eNameSupply :: Int
   , eUserEnv    :: UserEnv
   }
 
@@ -93,6 +100,7 @@ defaultRW isBatch = do
     , eContinue   = True
     , eIsBatch    = isBatch
     , eModuleEnv  = env
+    , eNameSupply = 0
     , eUserEnv    = mkUserEnv userOptions
     }
 
@@ -122,6 +130,12 @@ instance Functor REPL where
   {-# INLINE fmap #-}
   fmap f m = REPL (\ ref -> fmap f (unREPL m ref))
 
+instance Applicative REPL where
+  {-# INLINE pure #-}
+  pure = return
+  {-# INLINE (<*>) #-}
+  (<*>) = ap
+
 instance Monad REPL where
   {-# INLINE return #-}
   return x = REPL (\_ -> return x)
@@ -244,8 +258,27 @@ keepOne src as = case as of
 getVars :: REPL (Map.Map P.QName M.IfaceDecl)
 getVars  = do
   me <- getModuleEnv
+  denv <- getDynEnv
+  -- the subtle part here is removing the #Uniq prefix from
+  -- interactively-bound variables, and also excluding any that are
+  -- shadowed and thus can no longer be referenced
   let decls = M.focusedEnv me
-  return (keepOne "getVars" `fmap` M.ifDecls decls)
+      edecls = M.ifDecls (M.deIfaceDecls denv)
+      -- is this QName something the user might actually type?
+      isShadowed (qn@(P.QName (Just (P.ModName ['#':_])) name), _) =
+          case Map.lookup localName neExprs of
+            Nothing -> False
+            Just uniqueNames -> isNamed uniqueNames
+        where localName = P.QName Nothing name
+              isNamed us = any (== qn) (map M.qname us)
+              neExprs = M.neExprs (M.deNames denv)
+      isShadowed _ = False
+      unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
+      edecls' = Map.fromList
+              . map unqual
+              . filter isShadowed
+              $ Map.toList edecls
+  return (keepOne "getVars" `fmap` (M.ifDecls decls `mappend` edecls'))
 
 getTSyns :: REPL (Map.Map P.QName T.TySyn)
 getTSyns  = do
@@ -286,6 +319,25 @@ getModuleEnv  = eModuleEnv `fmap` getRW
 setModuleEnv :: M.ModuleEnv -> REPL ()
 setModuleEnv me = modifyRW_ (\rw -> rw { eModuleEnv = me })
 
+getDynEnv :: REPL M.DynamicEnv
+getDynEnv  = (M.meDynEnv . eModuleEnv) `fmap` getRW
+
+setDynEnv :: M.DynamicEnv -> REPL ()
+setDynEnv denv = do
+  me <- getModuleEnv
+  setModuleEnv (me { M.meDynEnv = denv })
+
+-- | Given an existing qualified name, prefix it with a
+-- relatively-unique string. We make it unique by prefixing with a
+-- character @#@ that is not lexically valid in a module name.
+uniqify :: P.QName -> REPL P.QName
+uniqify (P.QName Nothing name) = do
+  i <- eNameSupply `fmap` getRW
+  modifyRW_ (\rw -> rw { eNameSupply = i+1 })
+  let modname' = P.ModName [ '#' : ("Uniq_" ++ show i) ]
+  return (P.QName (Just modname') name)
+uniqify qn =
+  panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn]
 
 -- User Environment Interaction ------------------------------------------------
 

src/Cryptol/Eval.hs

@@ -14,6 +14,7 @@ module Cryptol.Eval (
   , EvalEnv()
   , emptyEnv
   , evalExpr
+  , evalDecls
   , EvalError(..)
   , WithBase(..)
   ) where