104 lines
2.8 KiB
Idris
104 lines
2.8 KiB
Idris
module Main
|
|
|
|
import Core.Check
|
|
import Core.Term
|
|
import Core.Value
|
|
import Core.Normalize
|
|
import Core.Misc
|
|
import Parser.Parse
|
|
|
|
import Control.Monad.Either
|
|
import Data.Vect
|
|
import Data.String
|
|
import Data.IORef
|
|
import Data.IOArray
|
|
import System
|
|
import System.File
|
|
|
|
smartPrint : {a : Type} -> Show a => a -> IO ()
|
|
smartPrint {a = String} = putStrLn
|
|
smartPrint {a = _} = printLn
|
|
|
|
isTrue : String -> Bool -> IO ()
|
|
isTrue _ True = pure ()
|
|
isTrue str False = putStrLn str >> exitFailure
|
|
|
|
unwrapCC : {a : Type} -> Show a => IO b -> Either a b -> IO b
|
|
unwrapCC {a = a} iob = \case
|
|
Left e => do
|
|
smartPrint e
|
|
iob
|
|
Right s => pure s
|
|
|
|
unwrap : {a : Type} -> Show a => Either a b -> IO b
|
|
unwrap = unwrapCC exitFailure
|
|
|
|
createNST : IO (Ref NST Nat)
|
|
createNST = do
|
|
nstIoRef <- newIORef 0
|
|
pure (MkRefP NST nstIoRef)
|
|
|
|
createDTX : (label : Type) -> Int -> IO (RefA label Value)
|
|
createDTX label n = do
|
|
arr <- newArray n
|
|
pure (MkRefP label arr)
|
|
|
|
typeCheck : {auto deftrs : RefA DTR Value}
|
|
-> {auto deftys : RefA DTY Value}
|
|
-> {auto frst : Ref NST Nat}
|
|
-> Int -> List (Term 0, Term 0) -> IO ()
|
|
typeCheck i [] = pure ()
|
|
typeCheck i ((ty, tr) :: defs) = do
|
|
vty <- unwrap =<< resolve (eval [] ty)
|
|
vtr <- unwrap =<< resolve (eval [] tr)
|
|
isTrue "putArr DTY" =<< putArr DTY i vty
|
|
isTrue "putArr DTR" =<< putArr DTR i vtr
|
|
typeCheck (i+1) defs
|
|
|
|
replRead : IO String
|
|
replRead = do
|
|
line <- getLine
|
|
if null (trim line)
|
|
then replRead
|
|
else case line of
|
|
":exit" => exitSuccess
|
|
_ => pure line
|
|
|
|
repl : {auto deftrs : RefA DTR Value}
|
|
-> {auto deftys : RefA DTY Value}
|
|
-> {auto frst : Ref NST Nat}
|
|
-> List String -> IO a
|
|
repl strs = do
|
|
line <- replRead
|
|
term <- unwrapCC (repl strs) (parseEnv strs line)
|
|
type <- unwrapCC (repl strs) =<< resolve (whnf =<< infer [] [] term)
|
|
val <- unwrapCC (repl strs) =<< resolve (whnf =<< eval [] term)
|
|
putStr "inferred type: "
|
|
printLn type
|
|
putStr "weak head normal form: "
|
|
printLn val
|
|
repl strs
|
|
|
|
main : IO ()
|
|
main = getArgs >>= \case
|
|
(_ :: x :: xs) => do
|
|
putStrLn (x ++ ": ")
|
|
putStr "Parsing: "
|
|
(strs, res) <- readFile x >>= unwrap >>= unwrap . toplevel
|
|
putStrLn " OK!"
|
|
let rlen = cast (length res)
|
|
nst <- createNST
|
|
dtr <- createDTX DTR rlen
|
|
dty <- createDTX DTY rlen
|
|
putStr "Typechecking: "
|
|
typeCheck 0 res
|
|
putStrLn "OK!"
|
|
case xs of
|
|
("repl" :: _) => repl strs
|
|
_ => exitSuccess
|
|
_ => do
|
|
nst <- createNST
|
|
dtr <- createDTX DTR 0
|
|
dty <- createDTX DTY 0
|
|
repl []
|