From 9452d3aee15b8943684828320324b3da37efb397 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 18 Dec 2022 21:09:33 +0000
Subject: Introduce better logging.

Led to immediate bug fixes for Pi types.
---
 src/Obs/Main.idr | 57 +++++++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 48 insertions(+), 9 deletions(-)

(limited to 'src/Obs/Main.idr')

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