module Main where
import Control.Monad.Reader
import qualified Control.Exception as E
import Data.List
import Data.Time
import System.Directory
import System.FilePath
import System.Environment
import System.Console.GetOpt
import System.Console.Haskeline
import System.Console.Haskeline.History
import Text.Printf
import Exp.Lex
import Exp.Par
import Exp.Print
import Exp.Abs hiding (NoArg)
import Exp.Layout
import Exp.ErrM| CubicalTT syntax
import CTT| Resolver for symbol resolution.
import Resolver| Type checker
import qualified TypeChecker as TC| Evaluator
import qualified Eval as E
type Interpreter a = InputT IO a| Flags
data Flag = Debug | Batch | Help | Version | Time
deriving (Eq,Show)
options :: [OptDescr Flag]
options = [ Option "d" ["debug"] (NoArg Debug) "run in debugging mode"
, Option "b" ["batch"] (NoArg Batch) "run in batch mode"
, Option "" ["help"] (NoArg Help) "print help"
, Option "-t" ["time"] (NoArg Time) "measure time spent computing"
, Option "" ["version"] (NoArg Version) "print version number" ]| Version number, welcome message, usage and prompt strings
version, welcome, usage, prompt :: String
version = "1.0"
welcome = "cubical, version: " ++ version ++ " (:h for help)\n"
usage = "Usage: cubical [options] <file.ctt>\nOptions:"
prompt = "> "| Entrypoint. handle command line arguments. If passed a file, load the file and then enter REPL loop. If not, directly enter REPL loop.
main :: IO ()
main = do
args <- getArgs
case getOpt Permute options args of
(flags,files,[])
| Help `elem` flags -> putStrLn $ usageInfo usage options
| Version `elem` flags -> putStrLn version
| otherwise -> case files of
[] -> do
putStrLn welcome
runInputT (settings []) (loop flags [] [] TC.verboseEnv)
[f] -> do
putStrLn welcome
putStrLn $ "Loading " ++ show f
initLoop flags f emptyHistory
_ -> putStrLn $ "Input error: zero or one file expected\n\n" ++
usageInfo usage options
(_,_,errs) -> putStrLn $ "Input error: " ++ concat errs ++ "\n" ++
usageInfo usage options| The main loop
loop :: [Flag] -> FilePath -> [(CTT.Ident,SymKind)] -> TC.TEnv -> Interpreter ()
loop flags f names tenv = do
input <- getInputLine prompt
case input of
Nothing -> outputStrLn help >> loop flags f names tenv
Just ":q" -> return ()
Just ":r" -> getHistory >>= lift . initLoop flags f
Just (':':'l':' ':str)
| ' ' `elem` str -> do outputStrLn "Only one file allowed after :l"
loop flags f names tenv
| otherwise -> getHistory >>= lift . initLoop flags str
Just (':':'c':'d':' ':str) -> do lift (setCurrentDirectory str)
loop flags f names tenv
Just ":h" -> outputStrLn help >> loop flags f names tenv
Just str' ->
let (msg,str,mod) = case str' of
(':':'n':' ':str) ->
("NORMEVAL: ",str,E.normal [])
str -> ("EVAL: ",str,id)
in case pExp (lexer str) of
Bad err -> outputStrLn ("Parse error: " ++ err) >> loop flags f names tenv| Resolve the expression
Ok exp ->
case runResolver $ local (insertIdents names) $ resolveExp exp of
Left err -> do outputStrLn ("Resolver failed: " ++ err)
loop flags f names tenv
Right body -> do| KEY STEP: type check the expression
x <- liftIO $ TC.runInfer tenv body
case x of
Left err -> do outputStrLn ("Could not type-check: " ++ err)
loop flags f names tenv
Right _ -> do
start <- liftIO getCurrentTime| KEY STEP: evaluate the expression.
let e = mod $ E.eval (TC.env tenv) body| Let’s not crash if the evaluation raises an error:
liftIO $ catch (putStrLn (msg ++ shrink (show e)))(writeFile “examples/nunivalence3.ctt” (show e))
(\e -> putStrLn ("Exception: " ++
show (e :: SomeException)))
stop <- liftIO getCurrentTime| Compute time and print nicely if -t is used.
let time = diffUTCTime stop start
secs = read (takeWhile (/='.') (init (show time)))
rest = read ('0':dropWhile (/='.') (init (show time)))
mins = secs `quot` 60
sec = printf "%.3f" (fromInteger (secs `rem` 60) + rest :: Float)
when (Time `elem` flags) $
outputStrLn $ "Time: " ++ show mins ++ "m" ++ sec ++ "s"Only print in seconds:
when (Time elem flags) $ outputStrLn $ “Time: “ ++ show time
loop flags f names tenv| load file
initLoop :: [Flag] -> FilePath -> History -> IO ()
initLoop flags f hist = doParse and type check files | imports defined below. Load modules. Module defined in ???
(_,_,mods) <- E.catch (imports True ([],[],[]) f)
(\e -> do putStrLn $ unlines $
("Exception: " :
(takeWhile (/= "CallStack (from HasCallStack):")
(lines $ show (e :: SomeException))))
return ([],[],[]))| Translate to TT. resolveModules from from Resolver.hs.
let res = runResolver $ resolveModules mods
case res of
Left err -> do
putStrLn $ "Resolver failed: " ++ err
runInputT (settings []) (putHistory hist >> loop flags f [] TC.verboseEnv)
Right (adefs,names) -> doAfter resolivng the file check if some definitions were shadowed:
let ns = map fst names
uns = nub ns
dups = ns \\ uns
unless (dups == []) $
putStrLn $ "Warning: the following definitions were shadowed [" ++
intercalate ", " dups ++ "]"
(merr,tenv) <- TC.runDeclss TC.verboseEnv adefs
case merr of
Just err -> putStrLn $ "Type checking failed: " ++ shrink err
Nothing -> unless (mods == []) $ putStrLn "File loaded."
if Batch `elem` flags
then return ()
else -- Compute names for auto completion
runInputT (settings [n | (n,_) <- names])
(putHistory hist >> loop flags f names tenv)| TODO: where is this coming from?!
lexer :: String -> [Token]
lexer = resolveLayout True . myLexer
showTree :: (Show a, Print a) => a -> IO ()
showTree tree = do
putStrLn $ "\n[Abstract Syntax]\n\n" ++ show tree
putStrLn $ "\n[Linearized tree]\n\n" ++ printTree treeUsed for auto completion
searchFunc :: [String] -> String -> [Completion]
searchFunc ns str = map simpleCompletion $ filter (str `isPrefixOf`) ns
settings :: [String] -> Settings IO
settings ns = Settings
{ historyFile = Nothing
, complete = completeWord Nothing " \t" $ return . searchFunc ns
, autoAddHistory = True }
shrink :: String -> String
shrink s = s -- if length s > 1000 then take 1000 s ++ "..." else s| import modules (not ok,loaded,already loaded defs) -> to load -> (new not ok, new loaded, new defs) the bool determines if it should be verbose or not
imports :: Bool -> ([String],[String],[Module]) -> String ->
IO ([String],[String],[Module])
imports v st@(notok,loaded,mods) f
| f `elem` notok = error ("Looping imports in " ++ f)
| f `elem` loaded = return st
| otherwise = do
b <- doesFileExist f
when (not b) $ error (f ++ " does not exist")
let prefix = dropFileName f
s <- readFile f
let ts = lexer s| parse a module and store it. | check that module name is same as filename.
case pModule ts of
Bad s -> error ("Parse failed in " ++ show f ++ "\n" ++ show s)
Ok mod@(Module (AIdent (_,name)) imp decls) -> do
let imp_ctt = [prefix ++ i ++ ".ctt" | Import (AIdent (_,i)) <- imp]
when (name /= dropExtension (takeFileName f)) $
error ("Module name mismatch in " ++ show f ++ " with wrong name " ++ "\"" ++ name ++ "\"")
(notok1,loaded1,mods1) <-
foldM (imports v) (f:notok,loaded,mods) imp_ctt
when v $ putStrLn $ "Parsed " ++ show f ++ " successfully!"
return (notok,f:loaded1,mods1 ++ [mod])
help :: String
help = "\nAvailable commands:\n" ++
" <statement> infer type and evaluate statement\n" ++
" :n <statement> normalize statement\n" ++
" :q quit\n" ++
" :l <filename> loads filename (and resets environment before)\n" ++
" :cd <path> change directory to path\n" ++
" :r reload\n" ++
" :h display this message\n"