Add extended environment, support for typechecking and evaluating decls

This is a checkpoint; it builds but doesn't yet work correctly!

cryptol/REPL/Command.hs

@@ -38,7 +38,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
-    (parseExprWith,ParseError(),Config(..),defaultConfig,parseModName)
+    (parseDeclsWith,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
@@ -126,6 +126,7 @@ instance Ord CommandDescr where
 
 data CommandBody
   = ExprArg     (String   -> REPL ())
+  | DeclsArg    (String   -> REPL ())
   | ExprTypeArg (String   -> REPL ())
   | FilenameArg (FilePath -> REPL ())
   | OptionArg   (String   -> REPL ())
@@ -175,6 +176,8 @@ commandList  =
     "set the current working directory"
   , CommandDescr ":module" (FilenameArg moduleCmd)
     "load a module"
+  , CommandDescr ":let" (DeclsArg letCmd)
+    "bind Cryptol expressions to names"
 
   , CommandDescr ":check" (ExprArg qcCmd)
     "use random testing to check that the argument always returns true"
@@ -228,6 +231,9 @@ evalCmd str = do
   ppOpts <- getPPValOpts
   io $ rethrowEvalError $ print $ pp $ E.WithBase ppOpts val
 
+letCmd :: String -> REPL ()
+letCmd = replEvalDecls
+
 qcCmd :: String -> REPL ()
 qcCmd "" =
   do xs <- getPropertyNames
@@ -551,6 +557,9 @@ 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
+
 interactiveConfig :: Config
 interactiveConfig = defaultConfig { cfgSource = "<interactive>" }
 
@@ -577,7 +586,14 @@ moduleCmdResult (res,ws0) = do
     Left err      -> raise (ModuleSystemError err)
 
 replCheckExpr :: P.Expr -> REPL (T.Expr,T.Schema)
-replCheckExpr e = liftModuleCmd $ M.checkExpr e
+replCheckExpr e = do
+  eenv <- getExtEnv
+  liftModuleCmd $ M.checkExprWith eenv e
+
+replCheckDecls :: [P.Decl] -> REPL [T.DeclGroup]
+replCheckDecls ds = do
+  eenv <- getExtEnv
+  liftModuleCmd $ M.checkDeclsWith eenv ds
 
 replSpecExpr :: T.Expr -> REPL T.Expr
 replSpecExpr e = liftModuleCmd $ S.specialize e
@@ -597,13 +613,21 @@ replEvalExpr str =
                let su = T.listSubst [ (T.tpVar a, t) | (a,t) <- tys ]
                return (def1, T.apSubst su (T.sType sig))
 
-     val <- liftModuleCmd (M.evalExpr def1)
+     eenv <- getExtEnv
+     val <- liftModuleCmd (M.evalExprWith eenv def1)
      whenDebug (io (putStrLn (dump def1)))
      return (val,ty)
   where
   warnDefault ns (x,t) =
         print $ text "Assuming" <+> ppWithNames ns x <+> text "=" <+> pp t
 
+replEvalDecls :: String -> REPL ()
+replEvalDecls str = do
+  decls <- replParseDecls str
+  -- TODO: extend name environment for all the names declared in decls
+  dgs <- replCheckDecls decls
+  undefined
+
 replEdit :: String -> REPL Bool
 replEdit file = do
   mb <- io (lookupEnv "EDITOR")
@@ -666,6 +690,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,7 @@ module REPL.Monad (
 
     -- ** Environment
   , getModuleEnv, setModuleEnv
+  , getExtEnv, setExtEnv
   , getTSyns, getNewtypes, getVars
   , whenDebug
   , getExprNames
@@ -61,6 +62,7 @@ import Control.Monad (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
@@ -80,6 +82,8 @@ data RW = RW
   , eContinue   :: Bool
   , eIsBatch    :: Bool
   , eModuleEnv  :: M.ModuleEnv
+  , eExtEnv     :: M.ExtendedEnv
+  -- ^ The dynamic environment for new bindings, eg @:let@
   , eUserEnv    :: UserEnv
   }
 
@@ -92,6 +96,7 @@ defaultRW isBatch = do
     , eContinue   = True
     , eIsBatch    = isBatch
     , eModuleEnv  = env
+    , eExtEnv     = mempty
     , eUserEnv    = mkUserEnv userOptions
     }
 
@@ -285,6 +290,11 @@ getModuleEnv  = eModuleEnv `fmap` getRW
 setModuleEnv :: M.ModuleEnv -> REPL ()
 setModuleEnv me = modifyRW_ (\rw -> rw { eModuleEnv = me })
 
+getExtEnv :: REPL M.ExtendedEnv
+getExtEnv  = eExtEnv `fmap` getRW
+
+setExtEnv :: M.ExtendedEnv -> REPL ()
+setExtEnv eenv = modifyRW_ (\rw -> rw { eExtEnv = eenv })
 
 -- User Environment Interaction ------------------------------------------------
 

src/Cryptol/Eval.hs

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

src/Cryptol/ModuleSystem.hs

@@ -9,13 +9,16 @@
 module Cryptol.ModuleSystem (
     -- * Module System
     ModuleEnv(..), initialModuleEnv
+  , ExtendedEnv(..)
   , ModuleError(..), ModuleWarning(..)
   , ModuleCmd, ModuleRes
   , findModule
   , loadModuleByPath
   , loadModule
-  , checkExpr
-  , evalExpr
+  , checkExprWith
+  , evalExprWith
+  , checkDeclsWith
+  , evalDeclsWith
   , focusedEnv
 
     -- * Interfaces
@@ -59,11 +62,24 @@ loadModule m env = runModuleM env $ do
   setFocusedModule (T.mName m')
   return m'
 
+-- Extended Environments -------------------------------------------------------
+
+-- These functions are particularly useful for interactive modes, as
+-- they allow for expressions to be evaluated in an environment that
+-- can extend dynamically outside of the context of a module.
+
 -- | Check the type of an expression.
-checkExpr :: P.Expr -> ModuleCmd (T.Expr,T.Schema)
-checkExpr e env = runModuleM env (interactive (Base.checkExpr e))
+checkExprWith :: ExtendedEnv -> P.Expr -> ModuleCmd (T.Expr,T.Schema)
+checkExprWith eenv e env = runModuleM env (interactive (Base.checkExprWith eenv e))
 
 -- | Evaluate an expression.
-evalExpr :: T.Expr -> ModuleCmd E.Value
-evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
+evalExprWith :: ExtendedEnv -> T.Expr -> ModuleCmd E.Value
+evalExprWith eenv e env = runModuleM env (interactive (Base.evalExprWith eenv e))
 
+-- | Typecheck declarations.
+checkDeclsWith :: ExtendedEnv -> [P.Decl] -> ModuleCmd [T.DeclGroup]
+checkDeclsWith eenv ds env = runModuleM env (interactive (Base.checkDeclsWith eenv ds))
+
+-- | Evaluate declarations and add them to the extended environment.
+evalDeclsWith :: ExtendedEnv -> [T.DeclGroup] -> ModuleCmd ExtendedEnv
+evalDeclsWith eenv dgs env = runModuleM env (interactive (Base.evalDeclsWith eenv dgs))

src/Cryptol/ModuleSystem/Base.hs

@@ -8,6 +8,7 @@
 
 module Cryptol.ModuleSystem.Base where
 
+import Cryptol.ModuleSystem.Env (ExtendedEnv(..))
 import Cryptol.ModuleSystem.Interface
 import Cryptol.ModuleSystem.Monad
 import qualified Cryptol.Eval                 as E
@@ -31,6 +32,7 @@ import Data.Foldable (foldMap)
 import Data.Function (on)
 import Data.List (nubBy)
 import Data.Maybe (mapMaybe,fromMaybe)
+import Data.Monoid ((<>), mconcat)
 import System.Directory (doesFileExist)
 import System.FilePath (addExtension,joinPath,(</>))
 import qualified Data.Map as Map
@@ -67,7 +69,6 @@ renameExpr e = do
   env <- getFocusedEnv
   rename (R.namingEnv env) e
 
-
 -- NoPat -----------------------------------------------------------------------
 
 -- | Run the noPat pass.
@@ -223,6 +224,35 @@ checkExpr e = do
   re  <- renameExpr npe
   typecheck T.tcExpr re =<< getQualifiedEnv
 
+-- | Typecheck a single expression in an extended environment.
+checkExprWith :: ExtendedEnv -> P.Expr -> ModuleM (T.Expr,T.Schema)
+checkExprWith eenv e = do
+  npe <- noPat e
+  re  <- renameExpr npe
+  env <- getQualifiedEnv
+  let env' = env <> eeIfaceDecls eenv
+  typecheck T.tcExpr re env'
+
+eeIfaceDecls :: ExtendedEnv -> IfaceDecls
+eeIfaceDecls EEnv { eeDecls = dgs } =
+  mconcat [ IfaceDecls
+            { ifTySyns   = Map.empty
+            , ifNewtypes = Map.empty
+            , ifDecls    = Map.singleton (ifDeclName ifd) [ifd]
+            }
+          | decl <- concatMap T.groupDecls dgs
+          , let ifd = mkIfaceDecl decl
+          ]
+
+-- | Typecheck a group of declarations in an extended environment.
+checkDeclsWith :: ExtendedEnv -> [P.Decl] -> ModuleM [T.DeclGroup]
+checkDeclsWith eenv ds = do
+  npds <- noPat ds
+  rds <- rename (eeNames eenv) npds
+  env <- getQualifiedEnv
+  let env' = env <> eeIfaceDecls eenv
+  typecheck T.tcDecls rds env'
+
 -- | Typecheck a module.
 checkModule :: P.Module -> ModuleM T.Module
 checkModule m = do
@@ -304,3 +334,17 @@ evalExpr :: T.Expr -> ModuleM E.Value
 evalExpr e = do
   env <- getEvalEnv
   return (E.evalExpr env e)
+
+evalExprWith :: ExtendedEnv -> T.Expr -> ModuleM E.Value
+evalExprWith eenv e = do
+  env <- getEvalEnv
+  return (E.evalExpr (env <> eeEnv eenv) e)
+
+-- | Evaluate typechecked declarations in an extended environment. The
+-- result of this is a new environment whose 'EvalEnv' is extended
+-- with the new declarations and their values.
+evalDeclsWith :: ExtendedEnv -> [T.DeclGroup] -> ModuleM ExtendedEnv
+evalDeclsWith eenv dgs = do
+  env <- getEvalEnv
+  let env' = env <> eeEnv eenv
+  return $ eenv { eeDecls = eeDecls eenv ++ dgs, eeEnv = E.evalDecls dgs env' }

src/Cryptol/ModuleSystem/Env.hs

@@ -14,6 +14,7 @@ import Paths_cryptol (getDataDir)
 
 import Cryptol.Eval (EvalEnv)
 import Cryptol.ModuleSystem.Interface
+import qualified Cryptol.ModuleSystem.NamingEnv as R
 import Cryptol.Parser.AST
 import qualified Cryptol.TypeCheck as T
 import qualified Cryptol.TypeCheck.AST as T
@@ -21,7 +22,7 @@ import qualified Cryptol.TypeCheck.AST as T
 import Control.Monad (guard)
 import Data.Foldable (fold)
 import Data.Function (on)
-import Data.Monoid (Monoid(..))
+import Data.Monoid ((<>), Monoid(..))
 import System.Environment.Executable(splitExecutablePath)
 import System.FilePath ((</>), normalise, joinPath, splitPath)
 import qualified Data.List as List
@@ -126,3 +127,28 @@ addLoadedModule tm lm
     , lmInterface = genIface tm
     , lmModule    = tm
     }
+
+-- Extended Environments -------------------------------------------------------
+
+-- | Extra information we need to carry around to dynamically extend
+-- an environment outside the context of a single module. Particularly
+-- useful when dealing with interactive declarations as in @:let@ or
+-- @it@.
+
+data ExtendedEnv = EEnv
+  { eeNames :: R.NamingEnv
+  , eeDecls :: [T.DeclGroup]
+  , eeEnv   :: EvalEnv
+  }
+
+instance Monoid ExtendedEnv where
+  mempty = EEnv
+    { eeNames = mempty
+    , eeDecls = mempty
+    , eeEnv   = mempty
+    }
+  mappend ee1 ee2 = EEnv
+    { eeNames = eeNames ee1 <> eeNames ee2
+    , eeDecls = eeDecls ee1 <> eeDecls ee2
+    , eeEnv   = eeEnv   ee1 <> eeEnv   ee2
+    }

src/Cryptol/ModuleSystem/Interface.hs

@@ -12,7 +12,7 @@ module Cryptol.ModuleSystem.Interface (
   , IfaceDecls(..)
   , IfaceTySyn, ifTySynName
   , IfaceNewtype
-  , IfaceDecl(..)
+  , IfaceDecl(..), mkIfaceDecl
 
   , shadowing
   , interpImport

src/Cryptol/Parser.y

@@ -5,6 +5,7 @@ module Cryptol.Parser
   , parseProgram, parseProgramWith
   , parseExpr, parseExprWith
   , parseDecl, parseDeclWith
+  , parseDecls, parseDeclsWith
   , parseModName
   , ParseError(..), ppError
   , Layout(..)
@@ -140,6 +141,7 @@ import Paths_cryptol
 %name programLayout program_layout
 %name expr    expr
 %name decl    decl
+%name decls   decls
 %name modName modName
 %tokentype { Located Token }
 %monad { ParseM }
@@ -722,5 +724,11 @@ parseDeclWith cfg = parse cfg { cfgModuleScope = False } decl
 parseDecl :: String -> Either ParseError Decl
 parseDecl = parseDeclWith defaultConfig
 
+parseDeclsWith :: Config -> String -> Either ParseError [Decl]
+parseDeclsWith cfg = parse cfg { cfgModuleScope = False } decls
+
+parseDecls :: String -> Either ParseError [Decl]
+parseDecls = parseDeclsWith defaultConfig
+
 -- vim: ft=haskell
 }

src/Cryptol/Parser/NoPat.hs

@@ -10,6 +10,7 @@
 -- patterns.  It also eliminates pattern bindings by de-sugaring them
 -- into `Bind`.  Furthermore, here we associate signatures and pragmas
 -- with the names to which they belong.
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE RecordWildCards #-}
 module Cryptol.Parser.NoPat (RemovePatterns(..),Error(..)) where
 
@@ -39,6 +40,8 @@ instance RemovePatterns Expr where
 instance RemovePatterns Module where
   removePatterns m = runNoPatM (noPatModule m)
 
+instance RemovePatterns [Decl] where
+  removePatterns ds = runNoPatM (noPatDs ds)
 
 simpleBind :: Located QName -> Expr -> Bind
 simpleBind x e = Bind { bName = x, bParams = [], bDef = e

src/Cryptol/TypeCheck.hs

@@ -9,6 +9,7 @@
 module Cryptol.TypeCheck
   ( tcModule
   , tcExpr
+  , tcDecls
   , InferInput(..)
   , InferOutput(..)
   , NameSeeds
@@ -22,6 +23,7 @@ module Cryptol.TypeCheck
 import qualified Cryptol.Parser.AST as P
 import           Cryptol.Parser.Position(Range)
 import           Cryptol.TypeCheck.AST
+import           Cryptol.TypeCheck.Depends (FromDecl)
 import           Cryptol.TypeCheck.Monad
                    ( runInferM
                    , InferInput(..)
@@ -31,7 +33,7 @@ import           Cryptol.TypeCheck.Monad
                    , lookupVar
                    )
 import           Cryptol.Prims.Types(typeOf)
-import           Cryptol.TypeCheck.Infer (inferModule, inferBinds)
+import           Cryptol.TypeCheck.Infer (inferModule, inferBinds, inferDs)
 import           Cryptol.TypeCheck.InferTypes(Error(..),Warning(..),VarType(..))
 import           Cryptol.TypeCheck.Solve(simplifyAllConstraints)
 import           Cryptol.Utils.PP
@@ -81,6 +83,11 @@ tcExpr e0 inp = runInferM inp
                           : map show res
                           )
 
+tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])
+tcDecls ds inp = runInferM inp $ inferDs ds $ \dgs -> do
+                   simplifyAllConstraints
+                   return dgs
+
 ppWarning :: (Range,Warning) -> Doc
 ppWarning (r,w) = text "[warning] at" <+> pp r <> colon $$ nest 2 (pp w)