mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 13:01:31 +03:00
102 lines
3.1 KiB
Haskell
102 lines
3.1 KiB
Haskell
-- |
|
|
-- Module : $Header$
|
|
-- Copyright : (c) 2013-2014 Galois, Inc.
|
|
-- License : BSD3
|
|
-- Maintainer : cryptol@galois.com
|
|
-- Stability : provisional
|
|
-- Portability : portable
|
|
|
|
module Main where
|
|
|
|
import Notebook
|
|
|
|
import REPL.Command
|
|
import REPL.Monad (lName, lPath)
|
|
import qualified REPL.Monad as REPL
|
|
|
|
import qualified Cryptol.ModuleSystem as M
|
|
import Cryptol.Parser (defaultConfig, parseModule, Config(..))
|
|
import qualified Cryptol.Parser.AST as P
|
|
import qualified Cryptol.TypeCheck.AST as T
|
|
import Cryptol.Utils.PP (pp)
|
|
|
|
import Control.Applicative ((<$>))
|
|
import Control.Monad (forever, forM_)
|
|
import System.IO (hFlush, stdout)
|
|
|
|
main :: IO ()
|
|
main = runNB $ do
|
|
liftREPL loadPrelude `catch` \x -> io $ print $ pp x
|
|
io $ putStr "<READY>" >> hFlush stdout
|
|
let loop = do
|
|
line <- io getLine
|
|
runExns $ case line of
|
|
"<BEGINMOD>" ->
|
|
handleModFrag =<< parseModFrag =<< readUntil (== "<ENDMOD>")
|
|
"<BEGINAUTO>" ->
|
|
handleAuto =<< readUntil (== "<ENDAUTO>")
|
|
_ ->
|
|
handleCmd line
|
|
io $ putStr "<DONE>" >> hFlush stdout
|
|
forever loop
|
|
|
|
-- Input Handling --------------------------------------------------------------
|
|
|
|
-- | Determine whether the input is a module fragment or a series of
|
|
-- interactive commands, and behave accordingly.
|
|
handleAuto :: String -> NB ()
|
|
handleAuto str = do
|
|
let cfg = defaultConfig { cfgSource = "<notebook>" }
|
|
cmdParses cmd =
|
|
case parseCommand findNbCommand cmd of
|
|
Just (Unknown _) -> False
|
|
Just (Ambiguous _ _) -> False
|
|
_ -> True
|
|
case parseModule cfg str of
|
|
Right m -> handleModFrag m
|
|
Left modExn -> do
|
|
let cmds = lines str
|
|
if and (map cmdParses cmds)
|
|
then forM_ cmds handleCmd
|
|
else raise (AutoParseError modExn)
|
|
|
|
parseModFrag :: String -> NB P.Module
|
|
parseModFrag str = liftREPL $ replParse (parseModule cfg) str
|
|
where cfg = defaultConfig { cfgSource = "<notebook>" }
|
|
|
|
-- | Read a module fragment and incorporate it into the current context.
|
|
handleModFrag :: P.Module -> NB ()
|
|
handleModFrag m = do
|
|
let m' = removeIncludes $ removeImports m
|
|
old <- getTopDecls
|
|
let new = modNamedDecls m'
|
|
merged = updateNamedDecls old new
|
|
doLoad = try $ liftREPL $ liftModuleCmd (M.loadModule (moduleFromDecls nbName merged))
|
|
|
|
em'' <- doLoad
|
|
-- only update the top decls if the module successfully loaded
|
|
case em'' of
|
|
Left exn -> raise exn
|
|
Right m'' -> do
|
|
setTopDecls merged
|
|
liftREPL $ REPL.setLoadedMod REPL.LoadedModule
|
|
{ lName = Just (T.mName m'')
|
|
, lPath = "<notebook>"
|
|
}
|
|
|
|
readUntil :: (String -> Bool) -> NB String
|
|
readUntil shouldStop = unlines . reverse <$> go []
|
|
where go xs = do
|
|
line <- io getLine
|
|
if shouldStop line
|
|
then return xs
|
|
else go (line : xs)
|
|
|
|
-- | Treat a line as an interactive command.
|
|
handleCmd :: String -> NB ()
|
|
handleCmd line =
|
|
case parseCommand findNbCommand line of
|
|
Nothing -> return ()
|
|
Just cmd -> do
|
|
liftREPL $ runCommand cmd
|