amelia
/
CCHM


{-# 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)")