Can typecheck universe-polymorphic id

1 files changed, 25 insertions, 1 deletions

diff --git a/app/Main.hs b/app/Main.hs
index 65ae4a0..f8b586a 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,4 +1,28 @@
 module Main where
 
+import qualified Data.Map.Strict as Map
+import System.Exit (die)
+
+import AST
+import Parser
+import TypeCheck
+
+
 main :: IO ()
-main = putStrLn "Hello, Haskell!"
+main = do
+  source <- getContents
+
+  uprog <- case parseProgram "<stdin>" source of
+    Left err -> die (show err)
+    Right term -> return term
+
+  let env0 = Map.fromList
+        [("Level", Nothing :| TLevelUniv)
+        ,("lzero", Nothing :| TLevel)
+        ,("lsuc", Nothing :| TPi "x" TLevel TLevel)]
+
+  env <- case checkProgram env0 uprog of
+    Left err -> die err
+    Right env -> return env
+
+  print env