|
|
- {-# LANGUAGE LambdaCase #-}
- module Main where
-
- import Control.Monad.IO.Class
- import Control.Monad.Catch
-
- import qualified Data.Map.Strict as Map
- import Data.List
-
- import Elab
-
- import Eval (eval, UnifyError (..))
-
- import Presyntax.Parser
- import Presyntax
-
- import Syntax
-
- import System.Console.Haskeline (runInputT, defaultSettings, getInputLine)
- import System.Exit
-
- import Systems (formulaOfFace, Face)
- import System.Environment
-
- showTypeError :: Maybe [String] -> Elab.TypeError -> String
- showTypeError lines (NotInScope l_c) = "Variable not in scope: " ++ l_c
-
- showTypeError lines (UnifyError (NotPiType vl)) = "Not a function type: " ++ show vl
- showTypeError lines (UnifyError (NotSigmaType vl)) = "Not a sigma type: " ++ show vl
- showTypeError lines (UnifyError (Mismatch a b)) =
- unlines [ "Types are not equal: "
- , " " ++ show (quote a)
- , " vs "
- , " " ++ show (quote b)
- ]
-
- showTypeError lines (WrongFaces _ faces) = unlines (map face faces) where
- face :: ([Value], Value, Elab.TypeError) -> String
- face (ixs, rhs, err) =
- "When checking face described by " ++ show ixs ++ ":\n" ++ showTypeError Nothing err
-
- showTypeError lines (InSpan start end err)
- | Just lines <- lines, fst start == fst end
- = makeRange (lines !! fst start) start end ++ '\n':showTypeError Nothing err
- | otherwise = showTypeError Nothing err
-
- showTypeError lines (IncompleteSystem formula extent) =
- unlines $
- [ "Incomplete system: "
- , "it is defined by " ++ show formula
- , "but the context mandates extent " ++ show extent ]
-
- showTypeError lines (IncompatibleFaces (fa, ta) (fb, tb) err) =
- unlines [ showTypeError lines err
- , "while checking that these overlapping faces are compatible:"
- , "* " ++ show fa ++ " -> " ++ show ta
- , "* " ++ show fb ++ " -> " ++ show tb
- ]
-
- showTypeError _ x = show x
-
- makeRange :: String -> (Int, Int) -> (Int, Int) -> String
- makeRange line (_, sc) (_, ec) = line ++ "\n" ++ replicate (sc + 1) ' ' ++ replicate (ec - sc) '~'
-
- main :: IO ()
- main = do
- t <- getArgs
- case t of
- [file] -> Main.check file
- _ -> repl
-
- check :: FilePath -> IO ()
- check file = do
- code <- readFile file
- let
- ste e = do
- putStrLn $ showTypeError (Just (lines code)) e
- exitFailure
- case parseString body code of
- Left e -> print e
- Right x -> do
- (tm, _) <- infer (Env mempty) x `catch` ste `catch` (ste . UnifyError)
- print (eval (Env mempty) tm)
-
- repl :: IO ()
- repl = runInputT defaultSettings (go (Env mempty)) where
- go env = getInputLine "> " >>= \case
- Just i | ":sq " `isPrefixOf` i -> do
- case parseString body (replicate 4 ' ' ++ drop 4 i) of
- Right exp ->
- (do
- (tm, ty) <- liftIO $ infer env exp
- liftIO $ drawExtent ty (eval env tm)
- `catch` \e -> liftIO $ putStrLn (showTypeError (Just [i]) e))
- `catch` \e -> liftIO $ print (e :: SomeException)
- Left e -> liftIO (print e)
- go env
- Just i ->
- case parseString statement i of
- Left e -> liftIO (print e) *> go env
- Right (Assume vs) ->
- let
- loop env ((v, t):vs) = do
- tm <- liftIO $ Elab.check env t VTypeω
- let ty = eval env tm
- loop env{ names = Map.insert v (ty, VVar v) (names env) } vs
- loop env [] = go env
- in (loop env vs
- `catch` \e -> (liftIO $ putStrLn (showTypeError (Just [i]) e)) *> go env)
- `catch` \e -> (liftIO $ print (e :: SomeException)) *> go env
- Right (Eval v) -> do
- liftIO $
- (do
- (tm, ty) <- infer env v
- let v_nf = eval env tm
- putStrLn $ show v_nf ++ " : " ++ show ty
- `catch` \e -> putStrLn (showTypeError (Just [i]) e))
- `catch` \e -> print (e :: SomeException)
- go env
- Right (Declare n t e) -> do
- (do
- t <- liftIO $ Elab.check env t VTypeω
- let t' = eval env t
- b <- liftIO $ Elab.check env e t'
- let b' = eval env b
- go env{ names = Map.insert n (t', b') (names env) })
- `catch` \e -> (liftIO $ putStrLn (showTypeError (Just [i]) e)) *> go env
- `catch` \e -> (liftIO $ print (e :: SomeException)) *> go env
- Nothing -> pure ()
-
- drawExtent :: Value -> Value -> IO ()
- drawExtent ty vl = nicely $ getDirections ty vl where
- getDirections :: Value -> Value -> [([(String, Bool)], Value, Value)]
- getDirections (VPi _ VI r) (VLam s VI k) =
- let trues = getDirections (r VI1) (k VI1)
- falses = getDirections (r VI0) (k VI0)
- in map (\(p, t, v) -> ((s, True):p, t, v)) trues
- ++ map (\(p, t, v) -> ((s, False):p, t, v)) falses
- getDirections ty t = [([], ty, t)]
-
- nicely :: [([(String, Bool)], Value, Value)] -> IO ()
- nicely [] = pure ()
- nicely ((bs, ty, el):fcs) = do
- putStr . unwords $ theFace bs
- putStrLn $ " => " ++ show el ++ " : " ++ show ty
- nicely fcs
-
- theFace = map (\(i, b) ->
- if b
- then "(" ++ i ++ "1)"
- else "(" ++ i ++ "0)")
|