From ae603f2423e967c55dfd31b0dec26d19584aa322 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Sat, 23 Dec 2023 23:12:03 +0100
Subject: Can typecheck universe-polymorphic id

---
 app/Main.hs | 26 +++++++++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

(limited to 'app')

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
-- 
cgit v1.2.3-70-g09d2