Introduce better logging.

Led to immediate bug fixes for Pi types.

1 files changed, 48 insertions, 9 deletions

diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr
index 5e0903e..fc7140a 100644
--- a/src/Obs/Main.idr
+++ b/src/Obs/Main.idr
@@ -1,6 +1,9 @@
 module Obs.Main
 
+import Data.DPair
+
 import Obs.Abstract
+import Obs.Logging
 import Obs.NormalForm
 import Obs.Parser
 import Obs.Syntax
@@ -8,23 +11,59 @@ import Obs.Term
 import Obs.Typing
 
 import System
+import System.File
 
-import Text.PrettyPrint.Prettyprinter
 import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 %default total
 
-usage : IO ()
-usage = do
-  () <- putStrLn "usage: obs <file>"
+record Options where
+  constructor MkOptions
+  file : String
+  lvl  : Level
+
+usage : String -> IO a
+usage prog = do
+  () <- putStrLn "usage: \{prog} <file>"
   exitFailure
 
+parseLevel : String -> Maybe Level
+parseLevel "0" = Just Error
+parseLevel "1" = Just Warn
+parseLevel "2" = Just Debug
+parseLevel "3" = Just Info
+parseLevel "4" = Just Trace
+parseLevel "error" = Just Error
+parseLevel "warn"  = Just Warn
+parseLevel "debug" = Just Debug
+parseLevel "info"  = Just Info
+parseLevel "trace" = Just Trace
+parseLevel _ = Nothing
+
+parseOptions : List1 String -> IO Options
+parseOptions (prog ::: [file, "-v", lvl]) = do
+  let Just lvl = parseLevel lvl
+    | Nothing => usage prog
+  pure $ MkOptions file lvl
+parseOptions (prog ::: [file, "-v"]) = pure $ MkOptions file Debug
+parseOptions (prog ::: [file]) = pure $ MkOptions file Error
+parseOptions (prog ::: _) = usage prog
+
+partial
+main' : (input: String) -> Logging AnsiStyle (Exists NormalForm.Context)
+main' input = do
+  defs <- parse input
+  blk  <- abstractBlock defs
+  ctx  <- checkBlock blk
+  pure (Evidence _ ctx)
+
 partial
 main : IO ()
 main = do
-  [_, file] <- getArgs
-    | _ => usage
-  defs <- parseFile file
-  blk <- Abstract.printErr $ abstractBlock defs
-  ctx <- Typing.printErr $ checkBlock blk
+  (prog :: args) <- getArgs
+    | _ => usage "obs"
+  opts <- parseOptions (prog ::: args)
+  Right input <- readFile opts.file
+    | Left err => do putStrLn "failed to open file: \{show err}"; exitFailure
+  ctx <- logToTerminal opts.lvl $ main' input
   putStrLn "Everything type checks."