executable that typechecks files!!

exe/Main.idr

@@ -1,17 +1,35 @@
 module Main
 
-import public Quox.Name
-import public Quox.Syntax
-import public Quox.Equal
-import public Quox.Pretty
-import public Quox.Typechecker
-import public Quox.Syntax.Qty.Three
+import Quox.Syntax
+import Quox.Parser
+import Quox.Definition
+import Quox.Pretty
 
-import Data.Nat
-import Data.Vect
-import Data.List
-import Control.ANSI
+import System
+import Data.IORef
+import Data.SortedSet
+import Control.Eff
+import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
+export
+die : Doc HL -> IO a
+die err = do putDoc $ termHL <$> err; exitFailure
+
+export
+main : IO ()
+main = do
+  seen <- newIORef SortedSet.empty
+  defs <- newIORef SortedMap.empty
+  for_ (drop 1 !getArgs) $ \file => do
+    putStrLn "checking \{file}"
+    Right res <- fromParserIO ["."] seen defs $ loadProcessFile file
+      | Left err => die $ prettyError True True err
+    for_ res $ \(name, def) => do
+      putDoc $ map termHL $
+        sep [hl Free $ pretty0 True name, colonD,
+             prettyTerm True [<] [<] def.type]
+
+-----------------------------------
 
 private
 text : PrettyOpts -> List String
@@ -52,17 +70,3 @@ join1 opts l r =
 export
 banner : PrettyOpts -> String
 banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
-
-export
-tm : Term Three 1 2
-tm =
-  (Pi_ One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
-    `DCloT` (K One ::: id))
-    `CloT`  (F "y" ::: TYPE 1 :# TYPE 2 ::: id)
-
-main : IO Unit
-main = do
-  putStrLn $ banner defPrettyOpts
-  prettyIODef @{TermSubst True} tm
-  prettyIODef @{TermSubst True} $ fst $ pushSubsts tm
-  prettyIODef tm