|
{-# LANGUAGE LambdaCase #-}
|
|
module Main where
|
|
|
|
import Presyntax.Parser
|
|
|
|
import System.Environment (getArgs)
|
|
import Elaboration
|
|
import Elaboration.Monad
|
|
import Control.Monad.Reader
|
|
import Syntax
|
|
import Evaluate (elabMetas, zonk, evaluate, quote)
|
|
import Syntax.Pretty
|
|
import Data.Foldable
|
|
import Control.Concurrent
|
|
import qualified Data.IntMap.Strict as Map
|
|
import Value (Meta(Solved, Unsolved))
|
|
|
|
main :: IO ()
|
|
main = do
|
|
[path] <- getArgs
|
|
text <- readFile path
|
|
x <-
|
|
case parseString body text of
|
|
Left e -> error (show e)
|
|
Right x -> pure x
|
|
|
|
swapMVar elabMetas mempty
|
|
swapMVar elabNext 0
|
|
|
|
t <- runElab ((,) <$> infer x <*> ask) emptyElabState
|
|
case t of
|
|
Left e -> traverse_ (putStrLn . showProgError text) e
|
|
Right ((x, t), e) -> do
|
|
metas <- readMVar elabMetas
|
|
for_ (Map.toList metas) $ \case
|
|
(n, Unsolved names v) ->
|
|
putStrLn $ '?':show n ++ " : " ++ showWithPrec names 0 (quote (Lvl (length names)) (zonk v)) "" ++ " = ? "
|
|
(n, Solved v) ->
|
|
putStrLn $ '?':show n ++ " = " ++ showTerm 0 (quote (Lvl 0) v) ""
|
|
|
|
putStrLn . flip id "" $ showTerm 0 x
|
|
putStrLn . flip id "" $ showString "Type: " . showTerm 0 (quote (Lvl 0) (zonk t))
|
|
let t = quote (Lvl 0) . zonk . evaluate (elabEnv e) $ x
|
|
putStrLn $ "Normal form: " ++ showTerm 0 t ""
|
|
|
|
showProgError :: String -> ProgError -> String
|
|
showProgError text (ProgError e sl sc el ec)
|
|
| sl == el, sl < length (lines text) =
|
|
let code = lines text
|
|
line = code !! sl
|
|
|
|
linum = show sl
|
|
|
|
caretLine = replicate (length linum) ' ' ++ " | " ++ replicate sc ' ' ++ "^" ++ replicate (ec - sc) '~'
|
|
paddedLine = replicate (length linum) ' ' ++ " | "
|
|
in unlines [ paddedLine
|
|
, linum ++ " | " ++ line
|
|
, caretLine
|
|
, showElabError e ""
|
|
]
|
|
| otherwise = showElabError e ""
|