Cube.hs

-- Simple interface to lambda cube type checker.
import System.Environment(getArgs)
import Data.Char(isSpace)
import Data.List(sortBy)
import Data.Function(on)
import REPL
import CubeExpr

main :: IO ()
main = do
    args <- getArgs
    case args of
	["-?"] -> usage
	["-help"] -> usage
	["--help"] -> usage
        [] -> interactive
	_  -> batch args

usage :: IO ()
usage = putStr "\
\Usage: cube           -- start in interactive mode\n\
\       cube files     -- concatenate files, type check, evaluate\n\
\       cube - files   -- insert let&in, concatenate files, type check, evaluate\n\
\"

batch :: [FilePath] -> IO ()
batch ("-":names) = mapM readFile names >>= batch' . addIn . ("let " :)
  where addIn ss = init ss ++ [" in "] ++ [last ss]
batch names = mapM readFile names >>= batch'

batch' :: [String] -> IO ()
batch' files = do
    let expr = unRight "Parse error: " $ unreads $ concat files
        typ = unRight "Type error: " $ typeCheck expr
    putStrLn $ "Type:\n" ++ show typ
    putStrLn $ "Value:\n" ++ show (nf expr)

unRight :: String -> Either String a -> a
unRight msg (Left msg') = error $ msg ++ msg'
unRight _ (Right a) = a

unreads :: (Show a, Read a) => String -> Either String a
unreads s =
    let xss = reads s
    in  case filter (null . snd) xss of
        (x, _) : _ -> Right x  -- pick first when ambiguous.
        _ -> 
	    -- Find the shortest suffix and report error there.
	    let rest = head $ sortBy (compare `on` length) $ map snd xss ++ [s]
	        ls = length (filter (=='\n') s)
		lrest = length (filter (=='\n') rest)
	    in  Left $ "line " ++ show (ls - lrest) ++ ": " ++ rest

data State = State { defs :: String, skipLam :: Bool } deriving (Show)

interactive :: IO ()
interactive = repl $ REPL { repl_init = cinit, repl_eval = ceval, repl_exit = cexit }
  where cinit = do
          putStrLn "Welcome to the Cube."
	  putStrLn "Use :help to get help."
	  return ("Cube> ", State "" False)
	cexit _ = putStrLn "Bye."
	ceval s line = do
	    let rest = dropWhile isSpace $ dropWhile (not . isSpace) line
	        load = readFile rest >>= addFile s
		quit = return (True, s)
		help = do putStrLn helpMsg; return (False, s)
	    case words line of
	      [] -> return (False, s)
	      ":h" : _ -> help
	      ":help" : _ -> help
	      ":q" : _ -> quit
	      ":quit" : _ -> quit
	      ":let" : _ -> addFile s (rest ++ ";\n")
	      ":l" : _ -> load
	      ":load" : _ -> load
	      ":defs" : _ -> do putStrLn (defs s); return (False, s)
	      ":skip" : _ -> return (False, s { skipLam = not (skipLam s) })
	      _ -> do evalPrint s line 
	              return (False, s)

        evalPrint s se = do
	    mt <- readAndCheck s se
	    case mt of
	         Nothing -> return ()
		 Just (e, t) -> do
		     let v = nf e
		         (v', t') = if skipLam s then skipLambda v t else (v, t)
		     putStrLn $ show v' ++ "\n  ::\n" ++ show t'
	    return (False, s)

        addFile s n = do
	     let s' = s { defs = defs s ++ n }
	     mt <- readAndCheck s' "\\ (a::*) -> a"
	     case mt of
	         Nothing -> return (False, s)
		 Just _ ->  return (False, s')

	readAndCheck s e =
	     case unreads $ "let " ++ defs s ++ " in " ++ e of
	     Left msg -> do putStrLn $ "Syntax error: " ++ msg; return Nothing
	     Right expr ->
	         case typeCheck expr of
		 Left msg -> do putStrLn $ "Type error: " ++ msg; return Nothing
		 Right typ -> return $ Just (expr, typ)

helpMsg :: String
helpMsg = "\
\Commands:\n\
\  :defs        show loaded definitions\n\
\  :let def     add definition\n\
\  :load name   load file with definitions\n\
\  :help        show this message\n\
\  :quit        quit\n\
\  :skip        toggle skipping initial lambdas\n\
\  expr         evaluate expression\n\
\"