Introduce better logging.

Led to immediate bug fixes for Pi types.

1 files changed, 6 insertions, 20 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 0915152..90616d4 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -3,6 +3,7 @@ module Obs.Abstract
 import Data.Fin
 import Data.String
 
+import Obs.Logging
 import Obs.Syntax
 import Obs.Term
 
@@ -11,31 +12,17 @@ import Text.Bounded
 
 %default total
 
-public export
 Context : Nat -> Type
 Context n = List (String, Fin n)
 
 bind : Context n -> String -> Context (S n)
 bind ctx str = (str, 0) :: map (mapSnd FS) ctx
 
-Error : Type -> Type
-Error = Either (Bounds, String)
-
-report : Bounds -> String -> Error a
-report = curry Left
-
 export
-printErr : Error a -> IO a
-printErr (Left (b, str)) = do
-  () <- putStrLn "error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
-  exitFailure
-printErr (Right x) = pure x
-
-export
-abstractSyntax : Context n -> Syntax -> Error (Term n)
+abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
 abstractSyntax ctx (Var var) = do
   let Just i = lookup var.val ctx
-    | Nothing => report var.bounds "unbound variable: \{var.val}"
+    | Nothing => inScope "unbound variable" $ fatal var
   pure (Var var i)
 abstractSyntax ctx (Sort bounds s) = pure (Sort bounds s)
 abstractSyntax ctx (Pi bounds var a b) = do
@@ -57,8 +44,7 @@ abstractSyntax ctx (Absurd bounds a t) = do
   t <- abstractSyntax ctx t
   pure (Absurd bounds a t)
 
-export
-abstractDefinition : Context n -> Definition -> Error (Definition n)
+abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
   { name = def.name
   , bounds = def.bounds
@@ -67,12 +53,12 @@ abstractDefinition ctx def = pure $ MkDefinition
   }
 
 export
-abstractBlock : (defs : List Definition) -> Error (Block (length defs))
+abstractBlock : (defs : List Definition) -> Logging ann (Block (length defs))
 abstractBlock defs =
   let asContext : Block n -> Context n
       asContext []            = []
       asContext (defs :< def) = bind (asContext defs) def.name
-  in let helper : Block n -> (defs : List Definition) -> Error (Block (length defs + n))
+  in let helper : Block n -> (defs : List Definition) -> Logging ann (Block (length defs + n))
          helper blk []            = pure blk
          helper blk (def :: defs) = do
            def <- abstractDefinition (asContext blk) def