Add type checking.HEADmaster

Currently, there is Set in Set. Next step is to add universe levels.

1 files changed, 25 insertions, 12 deletions

diff --git a/src/Main.idr b/src/Main.idr
index 2f05ccf..6f3fafe 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -2,6 +2,7 @@ module Main
 
 import CC.Name
 import CC.Term
+import CC.Term.Elaborate
 import CC.Term.Eval
 import CC.Term.Parse
 import CC.Term.Pretty
@@ -56,24 +57,36 @@ parseStdin = do
 
 helpMsg : String
 helpMsg = unlines [
-  "usage: cc-eval [--help|nf]",
+  "usage: cc-check [--help|nf|type]",
   "  --help : display this message",
-  "  nf     : read expression from stdin, print its normal form"
+  "  nf     : read & typecheck expression from stdin, print its normal form and type",
+  "  type   : read & typecheck expression from stdin, print its type"
   ]
 
+
+
 mainWith : IO (List String) -> IO RawTerm -> IO ()
 mainWith getOpt getTerm = do
-  [_, "nf"] <- getOpt
-    | [_, "--help"] => putStrLn helpMsg
-    | _ => putErrLn helpMsg >> exitFailure
-  rawTerm <- getTerm
-  let Right term = runNameError $ translate [<] rawTerm
-    | Left errs => for_ errs putErr >> exitFailure
-  let nf : Term [<] = normalise [<] term
-  putDoc (pretty nf)
+  opts <- getOpt
+  case opts of
+    [_, "--help"] => putStrLn helpMsg
+    [_, "nf"] => do
+      rawTerm <- getTerm
+      let Right (t, ty) = runElabError $ inferTerm rawTerm
+        | Left errs => for_ errs putErr >> exitFailure
+      let nf : Term [<] = normalise [<] t
+      let ty = quote ty
+      putDoc (group $ pretty nf <++> colon <+> line <+> pretty ty)
+    [_, "type"] => do
+      rawTerm <- getTerm
+      let Right (t, ty) = runElabError $ inferTerm rawTerm
+        | Left errs => for_ errs putErr >> exitFailure
+      putDoc (group $ pretty $ quote ty)
+    _ => putErrLn helpMsg >> exitFailure
   where
-  putErr : Name -> IO ()
-  putErr n = putBoundErrLn (bounds n) "undefined name: \{n}"
+  putErr : Either Name (String, Maybe Bounds) -> IO ()
+  putErr (Left n) = putBoundErrLn (bounds n) "undefined name: \{n}"
+  putErr (Right (s, bounds)) = putBoundErrLn bounds s
 
 partial
 main : IO ()