exe/CompileMonad.idr

@@ -0,0 +1,164 @@
+module CompileMonad
+
+import Quox.Syntax as Q
+import Quox.Definition as Q
+import Quox.Untyped.Syntax as U
+import Quox.Parser
+import Quox.Untyped.Erase
+import Quox.Untyped.Scheme
+import Quox.Pretty
+import Quox.Log
+import Options
+import Output
+import Error
+
+import System.File
+import Data.IORef
+import Data.Maybe
+import Control.Eff
+
+%default total
+
+%hide Doc.(>>=)
+%hide Core.(>>=)
+
+%hide FromParser.Error
+%hide Erase.Error
+%hide Lexer.Error
+%hide Parser.Error
+
+
+
+public export
+record State where
+  constructor MkState
+  seen : IORef SeenSet
+  defs : IORef Q.Definitions
+  ns   : IORef Mods
+  suf  : IORef NameSuf
+%name CompileMonad.State state
+
+export %inline
+newState : HasIO io => io State
+newState = pure $ MkState {
+  seen = !(newIORef empty),
+  defs = !(newIORef empty),
+  ns   = !(newIORef [<]),
+  suf  = !(newIORef 0)
+}
+
+
+public export
+data CompileTag = OPTS | STATE
+
+public export
+Compile : List (Type -> Type)
+Compile =
+  [Except Error,
+   ReaderL STATE State, ReaderL OPTS Options, Log,
+   LoadFile, IO]
+
+
+export %inline
+handleLog : IORef LevelStack -> OpenFile -> LogL x a -> IOErr Error a
+handleLog ref f l = case f of
+  OConsole ch => handleLogIO (const $ pure ()) ref (consoleHandle ch) l
+  OFile _ h   => handleLogIO (const $ pure ()) ref h l
+  ONone       => do
+    lvls   <- readIORef ref
+    lenRef <- newIORef (length lvls)
+    res    <- handleLogDiscardIO lenRef l
+    writeIORef ref $ fixupDiscardedLog !(readIORef lenRef) lvls
+    pure res
+
+private %inline
+withLogFile : Options ->
+              (IORef LevelStack -> OpenFile -> IO (Either Error a)) ->
+              IO (Either Error a)
+withLogFile opts act = do
+  lvlStack <- newIORef $ singleton opts.logLevels
+  withOutFile CErr opts.logFile fromError $ act lvlStack
+where
+  fromError : String -> FileError -> IO (Either Error a)
+  fromError file err = pure $ Left $ WriteError file err
+
+export covering %inline
+runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
+runCompile opts state act = do
+  withLogFile opts $ \lvls, logFile =>
+    fromIOErr $ runEff act $ with Union.(::)
+      [handleExcept (\e => ioLeft e),
+       handleReaderConst state,
+       handleReaderConst opts,
+       handleLog lvls logFile,
+       handleLoadFileIOE loadError ParseError state.seen opts.include,
+       liftIO]
+
+private %inline
+rethrowFileC : String -> Either FileError a -> Eff Compile a
+rethrowFileC f = rethrow . mapFst (WriteError f)
+
+
+export %inline
+outputStr : OpenFile -> Lazy String -> Eff Compile ()
+outputStr ONone           _   = pure ()
+outputStr (OConsole COut) str = putStr str
+outputStr (OConsole CErr) str = fPutStr stderr str >>= rethrowFileC "<stderr>"
+outputStr (OFile f h)     str = fPutStr h str >>= rethrowFileC f
+
+export %inline
+outputDocs : OpenFile ->
+             ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
+             Eff Compile ()
+outputDocs file docs = do
+  opts <- askAt OPTS
+  for_ (runPretty opts (toOutFile file) docs) $ \x =>
+    outputStr file $ render (Opts opts.width) x
+
+export %inline
+outputDoc : OpenFile ->
+            ({opts : LayoutOpts} -> Eff Pretty (Doc opts)) -> Eff Compile ()
+outputDoc file doc = outputDocs file $ singleton <$> doc
+
+
+public export
+data StopTag = STOP
+
+public export
+CompileStop : List (Type -> Type)
+CompileStop = FailL STOP :: Compile
+
+export %inline
+withEarlyStop : Eff CompileStop () -> Eff Compile ()
+withEarlyStop = ignore . runFailAt STOP
+
+export %inline
+stopHere : Has (FailL STOP) fs => Eff fs ()
+stopHere = failAt STOP
+
+
+export %inline
+liftFromParser : Eff FromParserIO a -> Eff Compile a
+liftFromParser act =
+  runEff act $ with Union.(::)
+    [handleExcept $ \err => throw $ FromParserError err,
+     handleStateIORef !(asksAt STATE defs),
+     handleStateIORef !(asksAt STATE ns),
+     handleStateIORef !(asksAt STATE suf),
+     \g => send g,
+     \g => send g]
+
+export %inline
+liftErase : Q.Definitions -> Eff Erase a -> Eff Compile a
+liftErase defs act =
+  runEff act
+    [handleExcept $ \err => throw $ EraseError err,
+     handleStateIORef !(asksAt STATE suf),
+     \g => send g]
+
+export %inline
+liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
+liftScheme act = do
+  runEff [|MkPair act (getAt MAIN)|]
+    [handleStateIORef !(newIORef empty),
+     handleStateIORef !(newIORef [])]

exe/Error.idr

@@ -0,0 +1,49 @@
+module Error
+
+import Quox.Pretty
+import Quox.Parser
+import Quox.Untyped.Erase
+import Quox.Untyped.Scheme
+import Options
+import Output
+
+import System.File
+
+
+public export
+data Error =
+  ParseError String Parser.Error
+| FromParserError FromParser.Error
+| EraseError Erase.Error
+| WriteError FilePath FileError
+| NoMain
+| MultipleMains (List Scheme.Id)
+
+%hide FromParser.Error
+%hide Erase.Error
+%hide Lexer.Error
+%hide Parser.Error
+
+
+export
+loadError : Loc -> FilePath -> FileError -> Error
+loadError loc file err = FromParserError $ LoadError loc file err
+
+export
+prettyError : {opts : LayoutOpts} -> Error -> Eff Pretty (Doc opts)
+prettyError (ParseError file e) = prettyParseError file e
+prettyError (FromParserError e) = FromParser.prettyError True e
+prettyError (EraseError      e) = Erase.prettyError True e
+prettyError NoMain              = pure "no #[main] function given"
+prettyError (MultipleMains xs)  =
+  pure $ sep ["multiple #[main] functions given:",
+              separateLoose "," !(traverse prettyId xs)]
+prettyError (WriteError file e) = pure $
+  hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
+
+export
+dieError : Options -> Error -> IO a
+dieError opts e =
+  die (Opts opts.width) $
+  runPretty ({outFile := Console} opts) Console $
+  prettyError e

exe/Main.idr

@@ -7,7 +7,11 @@ import Quox.Parser
 import Quox.Untyped.Erase
 import Quox.Untyped.Scheme
 import Quox.Pretty
+import Quox.Log
 import Options
+import Output
+import Error
+import CompileMonad
 
 import System
 import System.File
@@ -19,227 +23,26 @@ import Control.Eff
 %hide Doc.(>>=)
 %hide Core.(>>=)
 
-
-private
-die : HasIO io => (opts : LayoutOpts) -> Doc opts -> io a
-die opts err = do
-  ignore $ fPutStr stderr $ render opts err
-  exitFailure
-
-private
-hlFor : HLType -> OutFile -> HL -> Highlight
-hlFor Guess Console = highlightSGR
-hlFor Guess _       = noHighlight
-hlFor NoHL  _       = noHighlight
-hlFor Term  _       = highlightSGR
-hlFor Html  _       = highlightHtml
-
-private
-runPretty : Options -> OutFile -> Eff Pretty a -> a
-runPretty opts file act =
-  runPrettyWith Outer opts.flavor (hlFor opts.hlType file) 2 act
-
-private
-record State where
-  constructor MkState
-  seen : IORef SeenSet
-  defs : IORef Q.Definitions
-  ns   : IORef Mods
-  suf  : IORef NameSuf
-%name Main.State state
-
-private
-newState : HasIO io => io State
-newState = pure $ MkState {
-  seen = !(newIORef empty),
-  defs = !(newIORef empty),
-  ns   = !(newIORef [<]),
-  suf  = !(newIORef 0)
-}
-
-private
-data Error =
-  ParseError String Parser.Error
-| FromParserError FromParser.Error
-| EraseError Erase.Error
-| WriteError FilePath FileError
-| NoMain
-| MultipleMains (List Id)
 %hide FromParser.Error
 %hide Erase.Error
 %hide Lexer.Error
 %hide Parser.Error
 
 
-private
-loadError : Loc -> FilePath -> FileError -> Error
-loadError loc file err = FromParserError $ LoadError loc file err
-
-private
-prettyError : {opts : LayoutOpts} -> Error -> Eff Pretty (Doc opts)
-prettyError (ParseError file e) = prettyParseError file e
-prettyError (FromParserError e) = FromParser.prettyError True e
-prettyError (EraseError      e) = Erase.prettyError True e
-prettyError NoMain              = pure "no #[main] function given"
-prettyError (MultipleMains xs)  =
-  pure $ sep ["multiple #[main] functions given:",
-              separateLoose "," !(traverse prettyId xs)]
-prettyError (WriteError file e) = pure $
-  hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
-
-private
-dieError : Options -> Error -> IO a
-dieError opts e =
-  die (Opts opts.width) $
-  runPretty ({outFile := Console} opts) Console $
-  prettyError e
-
-private
-data CompileTag = OPTS | STATE
-
-private
-Compile : List (Type -> Type)
-Compile =
-  [Except Error,
-   ReaderL STATE State, ReaderL OPTS Options,
-   LoadFile, IO]
-
-private covering
-runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
-runCompile opts state act =
-  fromIOErr $ runEff act $ with Union.(::)
-    [handleExcept (\e => ioLeft e),
-     handleReaderConst state,
-     handleReaderConst opts,
-     handleLoadFileIOE loadError ParseError state.seen opts.include,
-     liftIO]
-
-
-private
-data StopTag = STOP
-
-private
-CompileStop : List (Type -> Type)
-CompileStop = FailL STOP :: Compile
-
-private
-withEarlyStop : Has (FailL STOP) fs => Eff fs () -> Eff (fs - FailL STOP) ()
-withEarlyStop = ignore . runFailAt STOP
-
-private
-stopHere : Has (FailL STOP) fs => Eff fs ()
-stopHere = failAt STOP
-
-
-private
-data ConsoleChannel = COut | CErr
-
-private
-data OpenFile = OConsole ConsoleChannel | OFile String File | ONone
-
-private
-rethrowFile : String -> Either FileError a -> Eff Compile a
-rethrowFile f = rethrow . mapFst (WriteError f)
-
-private
-toOutFile : OpenFile -> OutFile
-toOutFile (OConsole _) = Console
-toOutFile (OFile f _)  = File f
-toOutFile ONone        = NoOut
-
-private
-withFileC : String -> (OpenFile -> Eff Compile a) -> Eff Compile a
-withFileC f act =
-  withFile f WriteTruncate pure (Prelude.map Right . act . OFile f) >>=
-  rethrowFile f
-
-private
-withOutFile : ConsoleChannel -> OutFile ->
-              (OpenFile -> Eff Compile a) -> Eff Compile a
-withOutFile _  (File f) act = withFileC f act
-withOutFile ch Console  act = act $ OConsole ch
-withOutFile _  NoOut    act = act ONone
-
-private
-outputStr : OpenFile -> Lazy String -> Eff Compile ()
-outputStr ONone           _   = pure ()
-outputStr (OConsole COut) str = putStr str
-outputStr (OConsole CErr) str = fPutStr stderr str >>= rethrowFile "<stderr>"
-outputStr (OFile f h)     str = fPutStr h str >>= rethrowFile f
-
-private
-outputDocs : OpenFile ->
-             ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
-             Eff Compile ()
-outputDocs file docs = do
-  opts <- askAt OPTS
-  for_ (runPretty opts (toOutFile file) docs) $ \x =>
-    outputStr file $ render (Opts opts.width) x
-
-private
-outputDoc : OpenFile ->
-            ({opts : LayoutOpts} -> Eff Pretty (Doc opts)) -> Eff Compile ()
-outputDoc file doc = outputDocs file $ singleton <$> doc
-
-private
-liftFromParser : Eff FromParserIO a -> Eff Compile a
-liftFromParser act =
-  runEff act $ with Union.(::)
-    [handleExcept $ \err => throw $ FromParserError err,
-     handleStateIORef !(asksAt STATE defs),
-     handleStateIORef !(asksAt STATE ns),
-     handleStateIORef !(asksAt STATE suf),
-     \g => send g]
-
-private
-liftErase : Q.Definitions -> Eff Erase a -> Eff Compile a
-liftErase defs act =
-  runEff act
-    [handleExcept $ \err => throw $ EraseError err,
-     handleStateIORef !(asksAt STATE suf)]
-
-private
-liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
-liftScheme act = do
-  runEff [|MkPair act (getAt MAIN)|]
-    [handleStateIORef !(newIORef empty),
-     handleStateIORef !(newIORef [])]
-
-
 private
 Step : Type -> Type -> Type
-Step i o = OpenFile -> i -> Eff Compile o
-
--- private
--- processFile : String -> Eff Compile ()
--- processFile file = withEarlyStop $ do
---   Just ast <- loadFile noLoc file
---     | Nothing => pure ()
---   -- putErrLn "checking \{file}"
---   when (!(asksAt OPTS until) == Just Parse) $ do
---     lift $ outputStr $ show ast
---     stopHere
---   defList <- liftFromParser $ concat <$> traverse fromPTopLevel ast
---   outputDocStopIf Check $
---     traverse (uncurry Q.prettyDef) defList
---   let defs = SortedMap.fromList defList
---   erased <- liftErase defs $
---     traverse (\(x, d) => (x,) <$> eraseDef defs x d) defList
---   outputDocStopIf Erase $
---     traverse (uncurry U.prettyDef) erased
---   (scheme, mains) <- liftScheme $ map catMaybes $
---     traverse (uncurry defToScheme) erased
---   outputDocStopIf Scheme $
---     intersperse empty <$> traverse prettySexp scheme
+Step a b = OpenFile -> a -> Eff Compile b
 
 private
-step : {default CErr console : ConsoleChannel} ->
-       Phase -> OutFile -> Step i o -> i -> Eff CompileStop o
-step phase file act x = do
+step : ConsoleChannel -> Phase -> OutFile -> Step a b -> a -> Eff CompileStop b
+step console phase file act x = do
   opts <- askAt OPTS
-  res <- lift $ withOutFile console file $ \h => act h x
+  res  <- withOutFile console file fromError $ \h => lift $ act h x
   when (opts.until == Just phase) stopHere
   pure res
+where
+  fromError : String -> FileError -> Eff CompileStop c
+  fromError file err = throw $ WriteError file err
 
 
 private covering
@@ -268,25 +71,23 @@ erase h defList =
 where defs = SortedMap.fromList defList
 
 private covering
-scheme : Step (List U.NDefinition) (List Sexp, Id)
+scheme : Step (List U.NDefinition) (List Sexp, List Id)
 scheme h defs = do
   sexps' <- for defs $ \(x, d) => do
     (msexp, mains) <- liftScheme $ defToScheme x d
-    outputDoc h $ maybe (sayErased x) prettySexp msexp
+    outputDoc h $ case msexp of
+      Just s  => prettySexp s
+      Nothing => pure $ hsep [";;", prettyName x, "erased"]
     pure (msexp, mains)
-  bitraverse (pure . catMaybes) (oneMain . concat) $ unzip sexps'
-where
-  sayErased : {opts : LayoutOpts} -> Name -> Eff Pretty (Doc opts)
-  sayErased x = pure $ hsep [";;", prettyName x, "erased"]
-
-  oneMain : List Id -> Eff Compile Id
-  oneMain [m] = pure m
-  oneMain []  = throw NoMain
-  oneMain ms  = throw $ MultipleMains ms
+  pure $ bimap catMaybes concat $ unzip sexps'
 
 private covering
-output : Step (List Sexp, Id) ()
-output h (sexps, main) =
+output : Step (List Sexp, List Id) ()
+output h (sexps, mains) = do
+  main <- case mains of
+    [m] => pure m
+    []  => throw NoMain
+    _   => throw $ MultipleMains mains
   lift $ outputDocs h $ do
     res    <- traverse prettySexp sexps
     runner <- makeRunMain main
@@ -297,11 +98,11 @@ processFile : String -> Eff Compile ()
 processFile file = withEarlyStop $ pipeline !(askAt OPTS) file where
   pipeline : Options -> String -> Eff CompileStop ()
   pipeline opts =
-    step Parse  opts.dump.parse  Main.parse  >=>
-    step Check  opts.dump.check  Main.check  >=>
-    step Erase  opts.dump.erase  Main.erase  >=>
-    step Scheme opts.dump.scheme Main.scheme >=>
-    step End    opts.outFile     Main.output {console = COut}
+    step CErr Parse  opts.dump.parse  Main.parse  >=>
+    step CErr Check  opts.dump.check  Main.check  >=>
+    step CErr Erase  opts.dump.erase  Main.erase  >=>
+    step CErr Scheme opts.dump.scheme Main.scheme >=>
+    step COut End    opts.outFile     Main.output
 
 
 export covering

exe/Options.idr

@@ -1,6 +1,9 @@
 module Options
 
 import Quox.Pretty
+import Quox.Log
+import Data.DPair
+import Data.SortedMap
 import System
 import System.Console.GetOpt
 import System.File
@@ -42,13 +45,15 @@ record Dump where
 public export
 record Options where
   constructor MkOpts
-  hlType  : HLType
+  include   : List String
   dump      : Dump
   outFile   : OutFile
   until     : Maybe Phase
+  hlType    : HLType
   flavor    : Pretty.Flavor
   width     : Nat
-  include : List String
+  logLevels : LogLevels
+  logFile   : OutFile
 %name Options opts
 %runElab derive "Options" [Show]
 
@@ -61,13 +66,15 @@ defaultWidth = do
 export
 defaultOpts : IO Options
 defaultOpts = pure $ MkOpts {
-  hlType  = Guess,
+  include   = ["."],
   dump      = MkDump NoOut NoOut NoOut NoOut,
   outFile   = Console,
   until     = Nothing,
+  hlType    = Guess,
   flavor    = Unicode,
   width     = !defaultWidth,
-  include = ["."]
+  logLevels = defaultLogLevels,
+  logFile   = Console
 }
 
 private
@@ -118,11 +125,52 @@ toHLType str = case toLower str of
   "html" => Ok {hlType := Html}
   _      => Err "unknown highlighting type \{show str}\ntypes: term, html, none"
 
-||| like ghc, -i '' clears the search path; -i a:b:c adds a,b,c to the end
+||| like ghc, `-i ""` clears the search path;
+||| `-i a:b:c` adds `a`, `b`, `c` to the end
 private
 dirListFlag : String -> List String -> List String
-dirListFlag arg val =
-  if null arg then [] else val ++ toList (split (== ':') arg)
+dirListFlag ""   val = []
+dirListFlag dirs val = val ++ toList (split (== ':') dirs)
+
+private
+splitLogFlag : String -> Either String (List (Maybe LogCategory, LogLevel))
+splitLogFlag = traverse flag1 . toList . split (== ':') where
+  parseLogCategory : String -> Either String LogCategory
+  parseLogCategory cat = do
+    let Just cat = toLogCategory cat
+      | _ => let catList = joinBy ", " logCategories in
+             Left "unknown log category. categories are:\n\{catList}"
+    pure cat
+
+  parseLogLevel : String -> Either String LogLevel
+  parseLogLevel lvl = do
+    let Just lvl = parsePositive lvl
+      | _ => Left "log level \{lvl} not a number"
+    let Just lvl = toLogLevel lvl
+      | _ => Left "log level \{show lvl} out of range 0–\{show maxLogLevel}"
+    pure lvl
+
+  flag1 : String -> Either String (Maybe LogCategory, LogLevel)
+  flag1 str = do
+    let (first, second) = break (== '=') str
+    case strM second of
+      StrCons '=' lvl => do
+        cat <- parseLogCategory first
+        lvl <- parseLogLevel lvl
+        pure (Just cat, lvl)
+      StrNil => (Nothing,) <$> parseLogLevel first
+      _      => Left "invalid log flag \{str}"
+
+private
+setLogFlag : LogLevels -> (Maybe LogCategory, LogLevel) -> LogLevels
+setLogFlag lvls (Nothing,   lvl) = {defLevel := lvl} lvls
+setLogFlag lvls (Just name, lvl) = {levels $= ((name, lvl) ::)} lvls
+
+private
+logFlag : String -> OptAction
+logFlag str = case splitLogFlag str of
+  Left  err   => Err err
+  Right flags => Ok $ \o => {logLevels := foldl setLogFlag o.logLevels flags} o
 
 private
 commonOptDescrs' : List (OptDescr OptAction)
@@ -133,7 +181,11 @@ commonOptDescrs' = [
   MkOpt ['o'] ["output"] (ReqArg (\s => Ok {outFile := toOutFile s}) "<file>")
     "output file (\"-\" for stdout, \"\" for no output)",
   MkOpt ['P'] ["phase"] (ReqArg toPhase "<phase>")
-    "stop after the given phase"
+    "stop after the given phase",
+  MkOpt ['l'] ["log"] (ReqArg logFlag "[<cat>=]<n>:...")
+    "set log level",
+  MkOpt ['L'] ["log-file"] (ReqArg (\s => Ok {logFile := toOutFile s}) "<file>")
+    "set log output file"
 ]
 
 private
@@ -148,13 +200,17 @@ extraOptDescrs = [
   MkOpt [] ["color", "colour"] (ReqArg toHLType "<type>")
     "select highlighting type",
 
-  MkOpt [] ["dparse"] (ReqArg (\s => Ok {dump.parse := toOutFile s}) "<file>")
+  MkOpt [] ["dump-parse"]
+    (ReqArg (\s => Ok {dump.parse := toOutFile s}) "<file>")
     "dump AST",
-  MkOpt [] ["dcheck"] (ReqArg (\s => Ok {dump.check := toOutFile s}) "<file>")
+  MkOpt [] ["dump-check"]
+    (ReqArg (\s => Ok {dump.check := toOutFile s}) "<file>")
     "dump typechecker output",
-  MkOpt [] ["derase"] (ReqArg (\s => Ok {dump.erase := toOutFile s}) "<file>")
+  MkOpt [] ["dump-erase"]
+    (ReqArg (\s => Ok {dump.erase := toOutFile s}) "<file>")
     "dump erasure output",
-  MkOpt [] ["dscheme"] (ReqArg (\s => Ok {dump.scheme := toOutFile s}) "<file>")
+  MkOpt [] ["dump-scheme"]
+    (ReqArg (\s => Ok {dump.scheme := toOutFile s}) "<file>")
     "dump scheme output (without prelude)"
 ]
 

exe/Output.idr

@@ -0,0 +1,59 @@
+module Output
+
+import Quox.Pretty
+import Options
+
+import System.File
+import System
+
+public export
+data ConsoleChannel = COut | CErr
+
+export
+consoleHandle : ConsoleChannel -> File
+consoleHandle COut = stdout
+consoleHandle CErr = stderr
+
+public export
+data OpenFile = OConsole ConsoleChannel | OFile String File | ONone
+
+export
+toOutFile : OpenFile -> OutFile
+toOutFile (OConsole _) = Console
+toOutFile (OFile f _)  = File f
+toOutFile ONone        = NoOut
+
+export
+withFile : HasIO m => String -> (String -> FileError -> m a) ->
+           (OpenFile -> m a) -> m a
+withFile f catch act = Prelude.do
+  res <- withFile f WriteTruncate pure (Prelude.map Right . act . OFile f)
+  either (catch f) pure res
+
+export
+withOutFile : HasIO m => ConsoleChannel -> OutFile ->
+              (String -> FileError -> m a) -> (OpenFile -> m a) -> m a
+withOutFile _  (File f) catch act = withFile f catch act
+withOutFile ch Console  catch act = act $ OConsole ch
+withOutFile _  NoOut    catch act = act ONone
+
+
+
+private
+hlFor : HLType -> OutFile -> HL -> Highlight
+hlFor Guess Console = highlightSGR
+hlFor Guess _       = noHighlight
+hlFor NoHL  _       = noHighlight
+hlFor Term  _       = highlightSGR
+hlFor Html  _       = highlightHtml
+
+export
+runPretty : Options -> OutFile -> Eff Pretty a -> a
+runPretty opts file act =
+  runPrettyWith Outer opts.flavor (hlFor opts.hlType file) 2 act
+
+export
+die : HasIO io => (opts : LayoutOpts) -> Doc opts -> io a
+die opts err = do
+  ignore $ fPutStr stderr $ render opts err
+  exitFailure

lib/Control/Monad/ST/Extra.idr

@@ -62,3 +62,21 @@ export %inline HasST (STErr e) where liftST = STE . map Right
 export
 stLeft : e -> STErr e s a
 stLeft e = STE $ pure $ Left e
+
+
+parameters {auto _ : HasST m}
+  export %inline
+  newSTRef' : a -> m s (STRef s a)
+  newSTRef' x = liftST $ newSTRef x
+
+  export %inline
+  readSTRef' : STRef s a -> m s a
+  readSTRef' r = liftST $ readSTRef r
+
+  export %inline
+  writeSTRef' : STRef s a -> a -> m s ()
+  writeSTRef' r x = liftST $ writeSTRef r x
+
+  export %inline
+  modifySTRef' : STRef s a -> (a -> a) -> m s ()
+  modifySTRef' r f = liftST $ modifySTRef r f

lib/Quox/EffExtra.idr

@@ -36,6 +36,15 @@ gets : Has (State s) fs => (s -> a) -> Eff fs a
 gets = getsAt ()
 
 
+export %inline
+stateAt : (0 lbl : tag) -> Has (StateL lbl s) fs => (s -> (a, s)) -> Eff fs a
+stateAt lbl f = do (res, x) <- getsAt lbl f; putAt lbl x $> res
+
+export %inline
+state : Has (State s) fs => (s -> (a, s)) -> Eff fs a
+state = stateAt ()
+
+
 export
 handleStateIORef : HasIO m => IORef st -> StateL lbl st a -> m a
 handleStateIORef r Get     = readIORef r
@@ -47,7 +56,6 @@ handleStateSTRef r Get     = liftST $ readSTRef r
 handleStateSTRef r (Put s) = liftST $ writeSTRef r s
 
 
-
 public export
 data Length : List a -> Type where
   Z : Length []
@@ -97,6 +105,10 @@ export
 handleReaderConst : Applicative m => r -> ReaderL lbl r a -> m a
 handleReaderConst x Ask = pure x
 
+export
+handleWriterSTRef : HasST m => STRef s (SnocList w) -> WriterL lbl w a -> m s a
+handleWriterSTRef ref (Tell w) = liftST $ modifySTRef ref (:< w)
+
 
 public export
 record IOErr e a where

lib/Quox/Equal.idr

@@ -2,9 +2,12 @@ module Quox.Equal
 
 import Quox.BoolExtra
 import public Quox.Typing
-import Data.Maybe
-import Quox.EffExtra
 import Quox.FreeVars
+import Quox.Pretty
+import Quox.EffExtra
+
+import Data.List1
+import Data.Maybe
 
 %default total
 
@@ -15,11 +18,11 @@ EqModeState = State EqMode
 
 public export
 Equal : List (Type -> Type)
-Equal = [ErrorEff, DefsReader, NameGen]
+Equal = [ErrorEff, DefsReader, NameGen, Log]
 
 public export
 EqualInner : List (Type -> Type)
-EqualInner = [ErrorEff, NameGen, EqModeState]
+EqualInner = [ErrorEff, NameGen, EqModeState, Log]
 
 
 export %inline
@@ -74,9 +77,25 @@ sameTyCon (E       {}) _            = False
 ||| * `[π.A]` is empty if `A` is.
 ||| * that's it.
 public export covering
-isEmpty : Definitions -> EqContext n -> SQty -> Term 0 n ->
-          Eff EqualInner Bool
-isEmpty defs ctx sg ty0 = do
+isEmpty :
+  {default 30 logLevel : Nat} -> (0 _ : So (isLogLevel logLevel)) =>
+  Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
+
+private covering
+isEmptyNoLog :
+  Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
+
+isEmpty defs ctx sg ty = do
+  sayMany "equal" ty.loc
+    [logLevel :> "isEmpty",
+     95       :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     95       :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     logLevel :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
+  res <- isEmptyNoLog defs ctx sg ty
+  say "equal" logLevel ty.loc $ hsep ["isEmpty ⇝", pshow res]
+  pure res
+
+isEmptyNoLog defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
   let Left  y = choose $ isTyConE ty0
     | Right n => pure False
@@ -85,16 +104,17 @@ isEmpty defs ctx sg ty0 = do
     IOState {} => pure False
     Pi {arg, res, _} => pure False
     Sig {fst, snd, _} =>
-      isEmpty defs ctx sg fst `orM`
-      isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term
+      isEmpty defs ctx sg fst {logLevel = 90} `orM`
+      isEmpty defs (extendTy0 snd.name fst ctx) sg snd.term {logLevel = 90}
     Enum {cases, _} =>
       pure $ null cases
     Eq {} => pure False
     NAT {} => pure False
     STRING {} => pure False
-    BOX {ty, _} => isEmpty defs ctx sg ty
+    BOX {ty, _} => isEmpty defs ctx sg ty {logLevel = 90}
     E _ => pure False
 
+
 ||| true if a type is known to be a subsingleton purely by its form.
 ||| a subsingleton is a type with only zero or one possible values.
 ||| equality/subtyping accepts immediately on values of subsingleton types.
@@ -106,27 +126,42 @@ isEmpty defs ctx sg ty0 = do
 ||| * an enum type is a subsingleton if it has zero or one tags.
 ||| * a box type is a subsingleton if its content is
 public export covering
-isSubSing : Definitions -> EqContext n -> SQty -> Term 0 n ->
-            Eff EqualInner Bool
-isSubSing defs ctx sg ty0 = do
+isSubSing :
+  {default 30 logLevel : Nat} -> (0 _ : So (isLogLevel logLevel)) =>
+  Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
+
+private covering
+isSubSingNoLog :
+  Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool
+
+isSubSing defs ctx sg ty = do
+  sayMany "equal" ty.loc
+    [logLevel :> "isSubSing",
+     95       :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     95       :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     logLevel :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
+  res <- isSubSingNoLog defs ctx sg ty
+  say "equal" logLevel ty.loc $ hsep ["isSubsing ⇝", pshow res]
+  pure res
+
+isSubSingNoLog defs ctx sg ty0 = do
   Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
-  let Left  y = choose $ isTyConE ty0
-    | Right n => pure False
+  let Left y = choose $ isTyConE ty0 | _ => pure False
   case ty0 of
     TYPE {} => pure False
     IOState {} => pure False
     Pi {arg, res, _} =>
-      isEmpty defs ctx sg arg `orM`
-      isSubSing defs (extendTy0 res.name arg ctx) sg res.term
+      isEmpty defs ctx sg arg {logLevel = 90} `orM`
+      isSubSing defs (extendTy0 res.name arg ctx) sg res.term {logLevel = 90}
     Sig {fst, snd, _} =>
-      isSubSing defs ctx sg fst `andM`
-      isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term
+      isSubSing defs ctx sg fst {logLevel = 90} `andM`
+      isSubSing defs (extendTy0 snd.name fst ctx) sg snd.term {logLevel = 90}
     Enum {cases, _} =>
       pure $ length (SortedSet.toList cases) <= 1
     Eq {} => pure True
     NAT {} => pure False
     STRING {} => pure False
-    BOX {ty, _} => isSubSing defs ctx sg ty
+    BOX {ty, _} => isSubSing defs ctx sg ty {logLevel = 90}
     E _ => pure False
 
 
@@ -137,12 +172,21 @@ bigger l r = gets $ \case Super => l; _ => r
 
 
 export
-ensureTyCon : Has ErrorEff fs =>
+ensureTyCon, ensureTyConNoLog :
+  (Has Log fs, Has ErrorEff fs) =>
   (loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
   Eff fs (So (isTyConE t))
-ensureTyCon loc ctx t = case nchoose $ isTyConE t of
+ensureTyConNoLog loc ctx ty = do
+  case nchoose $ isTyConE ty of
     Left  y => pure y
-  Right n => throw $ NotType loc (toTyContext ctx) (t // shift0 ctx.dimLen)
+    Right n => throw $ NotType loc (toTyContext ctx) (ty // shift0 ctx.dimLen)
+
+ensureTyCon loc ctx ty = do
+  sayMany "equal" ty.loc
+    [60 :> "ensureTyCon",
+     95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     60 :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
+  ensureTyConNoLog loc ctx ty
 
 
 namespace Term
@@ -750,7 +794,11 @@ namespace Elim
 
 
 namespace Term
-  compare0 defs ctx sg ty s t =
+  export covering %inline
+  compare0NoLog :
+    Definitions -> EqContext n -> SQty -> (ty, s, t : Term 0 n) ->
+    Eff EqualInner ()
+  compare0NoLog defs ctx sg ty s t =
     wrapErr (WhileComparingT ctx !mode sg ty s t) $ do
       Element ty' _ <- whnf defs ctx SZero ty.loc ty
       Element s'  _ <- whnf defs ctx sg s.loc  s
@@ -758,20 +806,72 @@ namespace Term
       tty <- ensureTyCon ty.loc ctx ty'
       compare0' defs ctx sg ty' s' t'
 
+  compare0 defs ctx sg ty s t = do
+    sayMany "equal" s.loc
+      [30 :> "Term.compare0",
+       30 :> hsep ["mode =", pshow !mode],
+       95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+       95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+       31 :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty],
+       30 :> hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s],
+       30 :> hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]]
+    compare0NoLog defs ctx sg ty s t
+
 namespace Elim
-  compare0 defs ctx sg e f = do
+  export covering %inline
+  compare0NoLog :
+    Definitions -> EqContext n -> SQty -> (e, f : Elim 0 n) ->
+    Eff EqualInner (Term 0 n)
+  compare0NoLog defs ctx sg e f = do
     (ty, err) <- runStateAt InnerErr Nothing $ compare0Inner defs ctx sg e f
     maybe (pure ty) throw err
 
-compareType defs ctx s t = do
+  compare0 defs ctx sg e f = do
+    sayMany "equal" e.loc
+      [30 :> "Elim.compare0",
+       30 :> hsep ["mode =", pshow !mode],
+       95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+       95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+       30 :> hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e],
+       30 :> hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f]]
+    ty <- compare0NoLog defs ctx sg e f
+    say "equal" 31 e.loc $
+      hsep ["Elim.compare0 ⇝", runPretty $ prettyTerm [<] ctx.tnames ty]
+    pure ty
+
+export covering %inline
+compareTypeNoLog :
+  Definitions -> EqContext n -> (s, t : Term 0 n) -> Eff EqualInner ()
+compareTypeNoLog defs ctx s t = do
   Element s' _ <- whnf defs ctx SZero s.loc s
   Element t' _ <- whnf defs ctx SZero t.loc t
   ts <- ensureTyCon s.loc ctx s'
   tt <- ensureTyCon t.loc ctx t'
-  st <- either pure (const $ clashTy s.loc ctx s' t') $
-        nchoose $ sameTyCon s' t'
+  let Left _ = choose $ sameTyCon s' t' | _ => clashTy s.loc ctx s' t'
   compareType' defs ctx s' t'
 
+compareType defs ctx s t = do
+  sayMany "equal" s.loc
+    [30 :> "compareType",
+     30 :> hsep ["mode =", pshow !mode],
+     95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     30 :> hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s],
+     30 :> hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]]
+  compareTypeNoLog defs ctx s t
+
+
+private
+getVars : TyContext d _ -> FreeVars d -> List BindName
+getVars ctx (FV fvs) = case ctx.dctx of
+  ZeroIsOne => []
+  C eqs     => toList $ getVars' ctx.dnames eqs fvs
+where
+  getVars' : BContext d' -> DimEq' d' -> FreeVars' d' -> SnocList BindName
+  getVars' (names :< name) (eqs :< eq) (fvs :< fv) =
+    let rest = getVars' names eqs fvs in
+    case eq of Nothing => rest :< name
+               Just _  => rest
+  getVars' [<] [<] [<] = [<]
 
 parameters (loc : Loc) (ctx : TyContext d n)
   parameters (mode : EqMode)
@@ -780,9 +880,11 @@ parameters (loc : Loc) (ctx : TyContext d n)
     fromInner = lift . map fst . runState mode
 
     private
-    eachFace : Applicative f => FreeVars d ->
-               (EqContext n -> DSubst d 0 -> f ()) -> f ()
-    eachFace fvs act =
+    eachCorner : Has Log fs => Loc -> FreeVars d ->
+                 (EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs ()
+    eachCorner loc fvs act = do
+      say "equal" 50 loc $
+        hsep $ "eachCorner: split on" :: map prettyBind' (getVars ctx fvs)
       for_ (splits loc ctx.dctx fvs) $ \th =>
         act (makeEqContext ctx th) th
 
@@ -792,31 +894,36 @@ parameters (loc : Loc) (ctx : TyContext d n)
       Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner ()
 
     private
-    runCompare : FreeVars d -> CompareAction d n -> Eff Equal ()
-    runCompare fvs act = fromInner $ eachFace fvs $ act !(askAt DEFS)
+    runCompare : Loc -> FreeVars d -> CompareAction d n -> Eff Equal ()
+    runCompare loc fvs act = fromInner $ eachCorner loc fvs $ act !(askAt DEFS)
 
     private
-    fdvAll : HasFreeDVars t => List (t d n) -> FreeVars d
-    fdvAll = let Val d = ctx.dimLen in foldMap (fdvWith [|d|] ctx.termLen)
+    foldMap1 : Semigroup b => (a -> b) -> List1 a -> b
+    foldMap1 f = foldl1By (\x, y => x <+> f y) f
+
+    private
+    fdvAll : HasFreeDVars t => (xs : List (t d n)) -> (0 _ : NonEmpty xs) =>
+             FreeVars d
+    fdvAll (x :: xs) = foldMap1 (fdvWith ctx.dimLen ctx.termLen) (x ::: xs)
 
     namespace Term
       export covering
       compare : SQty -> (ty, s, t : Term d n) -> Eff Equal ()
-      compare sg ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th =>
-        compare0 defs ectx sg (ty // th) (s // th) (t // th)
+      compare sg ty s t = runCompare s.loc (fdvAll [ty, s, t]) $
+        \defs, ectx, th => compare0 defs ectx sg (ty // th) (s // th) (t // th)
 
       export covering
       compareType : (s, t : Term d n) -> Eff Equal ()
-      compareType s t = runCompare (fdvAll [s, t]) $ \defs, ectx, th =>
-        compareType defs ectx (s // th) (t // th)
+      compareType s t = runCompare s.loc (fdvAll [s, t]) $
+        \defs, ectx, th => compareType defs ectx (s // th) (t // th)
 
     namespace Elim
       ||| you don't have to pass the type in but the arguments must still be
       ||| of the same type!!
       export covering
       compare : SQty -> (e, f : Elim d n) -> Eff Equal ()
-      compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th =>
-        ignore $ compare0 defs ectx sg (e // th) (f // th)
+      compare sg e f = runCompare e.loc (fdvAll [e, f]) $
+        \defs, ectx, th => ignore $ compare0 defs ectx sg (e // th) (f // th)
 
   namespace Term
     export covering %inline

lib/Quox/Log.idr

@@ -0,0 +1,317 @@
+module Quox.Log
+
+import Quox.Loc
+import Quox.Pretty
+import Quox.PrettyValExtra
+
+import Data.So
+import Data.DPair
+import Data.Maybe
+import Data.List1
+import Control.Eff
+import Control.Monad.ST.Extra
+import Data.IORef
+import System.File
+import Derive.Prelude
+
+%default total
+%language ElabReflection
+
+
+public export %inline
+maxLogLevel : Nat
+maxLogLevel = 100
+
+public export %inline
+logCategories : List String
+logCategories = ["whnf", "equal", "check"]
+
+public export %inline
+isLogLevel : Nat -> Bool
+isLogLevel l = l <= maxLogLevel
+
+public export
+IsLogLevel : Nat -> Type
+IsLogLevel l = So $ isLogLevel l
+
+public export %inline
+isLogCategory : String -> Bool
+isLogCategory cat = cat `elem` logCategories
+
+public export
+IsLogCategory : String -> Type
+IsLogCategory cat = So $ isLogCategory cat
+
+-- Q: why are you using `So` instead of `LT` and `Elem`
+-- A: ① proof search gives up before finding a proof of e.g. ``99 `LT` 100``
+--      (i.e. `LTESucc⁹⁹ LTEZero`)
+--    ② the proofs aren't looked at in any way, i just wanted to make sure the
+--      list of categories was consistent everywhere
+
+
+||| a verbosity level from 0–100. higher is noisier. each log entry has a
+||| verbosity level above which it will be printed, chosen, uh, based on vibes.
+public export
+LogLevel : Type
+LogLevel = Subset Nat IsLogLevel
+
+||| a logging category, like "check" (type checking), "whnf", or whatever.
+public export
+LogCategory : Type
+LogCategory = Subset String IsLogCategory
+
+
+public export %inline
+toLogLevel : Nat -> Maybe LogLevel
+toLogLevel l =
+  case choose $ isLogLevel l of
+    Left  y => Just $ Element l y
+    Right _ => Nothing
+
+public export %inline
+toLogCategory : String -> Maybe LogCategory
+toLogCategory c =
+  case choose $ isLogCategory c of
+    Left  y => Just $ Element c y
+    Right _ => Nothing
+
+
+||| verbosity levels for each category, if they differ from the default
+public export
+LevelMap : Type
+LevelMap = List (LogCategory, LogLevel)
+
+-- Q: why `List` instead of `SortedMap`
+-- A: oof ouch my constant factors (maybe this one was more obvious)
+
+
+public export
+record LogLevels where
+  constructor MkLogLevels
+  defLevel : LogLevel
+  levels   : LevelMap
+%name LogLevels lvls
+%runElab derive "LogLevels" [Eq, Show, PrettyVal]
+
+public export
+LevelStack : Type
+LevelStack = List LogLevels
+
+public export %inline
+defaultLevel : LogLevel
+defaultLevel = Element 0 Oh
+
+export %inline
+defaultLogLevels : LogLevels
+defaultLogLevels = MkLogLevels defaultLevel []
+
+export %inline
+initStack : LevelStack
+initStack = []
+
+export %inline
+getLevel1 : LogCategory -> LogLevels -> LogLevel
+getLevel1 cat (MkLogLevels def lvls) = fromMaybe def $ lookup cat lvls
+
+export %inline
+getLevel : LogCategory -> LevelStack -> LogLevel
+getLevel cat (lvls :: _) = getLevel1 cat lvls
+getLevel cat []          = defaultLevel
+
+export %inline
+getCurLevels : LevelStack -> LogLevels
+getCurLevels (lvls :: _) = lvls
+getCurLevels []          = defaultLogLevels
+
+
+public export
+LogDoc : Type
+LogDoc = Doc (Opts {lineLength = 80})
+
+
+private %inline
+replace : Eq a => a -> b -> List (a, b) -> List (a, b)
+replace k v kvs = (k, v) :: filter (\y => fst y /= k) kvs
+
+private %inline
+mergeLeft : Eq a => List (a, b) -> List (a, b) -> List (a, b)
+mergeLeft l r = foldl (\lst, (k, v) => replace k v lst) r l
+
+
+public export
+data PushArg =
+    SetDefault LogLevel
+  | SetCat     LogCategory LogLevel
+  | SetAll     LogLevel
+%runElab derive "PushArg" [Eq, Ord, Show, PrettyVal]
+%name PushArg push
+
+export %inline
+applyPush : LogLevels -> PushArg -> LogLevels
+applyPush lvls (SetDefault def)     = {defLevel := def} lvls
+applyPush lvls (SetCat     cat lvl) = {levels   $= replace cat lvl} lvls
+applyPush lvls (SetAll     lvl)     = MkLogLevels lvl []
+
+export %inline
+fromPush : PushArg -> LogLevels
+fromPush = applyPush defaultLogLevels
+
+
+public export
+record LogMsg where
+  constructor (:>)
+  level : Nat
+  {auto 0 levelOk : IsLogLevel level}
+  message : Lazy LogDoc
+infix 0 :>
+%name Log.LogMsg msg
+
+public export
+data LogL : (lbl : tag) -> Type -> Type where
+  ||| print some log messages
+  SayMany : (cat : LogCategory) -> (loc : Loc) ->
+            (msgs : List LogMsg) -> LogL lbl ()
+  ||| set some verbosity levels
+  Push : (push : List PushArg) -> LogL lbl ()
+  ||| restore the previous verbosity levels.
+  ||| returns False if the stack was already empty
+  Pop : LogL lbl Bool
+  ||| returns the current verbosity levels
+  CurLevels : LogL lbl LogLevels
+
+public export
+Log : Type -> Type
+Log = LogL ()
+
+parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs}
+  public export %inline
+  sayManyAt : (cat : String) -> (0 catOk : IsLogCategory cat) =>
+              Loc -> List LogMsg -> Eff fs ()
+  sayManyAt cat loc msgs {catOk} =
+    send $ SayMany {lbl} (Element cat catOk) loc msgs
+
+  public export %inline
+  sayAt : (cat : String) -> (0 catOk : IsLogCategory cat) =>
+          (lvl : Nat)    -> (0 lvlOk : IsLogLevel lvl) =>
+          Loc -> Lazy LogDoc -> Eff fs ()
+  sayAt cat lvl loc msg = sayManyAt cat loc [lvl :> msg]
+
+  public export %inline
+  pushAt : List PushArg -> Eff fs ()
+  pushAt lvls = send $ Push {lbl} lvls
+
+  public export %inline
+  push1At : PushArg -> Eff fs ()
+  push1At lvl = pushAt [lvl]
+
+  public export %inline
+  popAt : Eff fs Bool
+  popAt = send $ Pop {lbl}
+
+  public export %inline
+  curLevelsAt : Eff fs LogLevels
+  curLevelsAt = send $ CurLevels {lbl}
+
+parameters {auto _ : Has Log fs}
+  public export %inline
+  sayMany : (cat : String) -> (0 catOk : IsLogCategory cat) =>
+            Loc -> List LogMsg -> Eff fs ()
+  sayMany = sayManyAt ()
+
+  public export %inline
+  say : (cat : String) -> (0 _ : IsLogCategory cat) =>
+        (lvl : Nat)    -> (0 _ : IsLogLevel lvl) =>
+        Loc -> Lazy LogDoc -> Eff fs ()
+  say = sayAt ()
+
+  public export %inline
+  push : List PushArg -> Eff fs ()
+  push = pushAt ()
+
+  public export %inline
+  push1 : PushArg -> Eff fs ()
+  push1 = push1At ()
+
+  public export %inline
+  pop : Eff fs Bool
+  pop = popAt ()
+
+  public export %inline
+  curLevels : Eff fs LogLevels
+  curLevels = curLevelsAt ()
+
+
+||| handles a `Log` effect with an existing `State` and `Writer`
+export %inline
+handleLogSW : (0 s : ts) -> (0 w : tw) ->
+              Has (StateL s LevelStack) fs => Has (WriterL w LogDoc) fs =>
+              LogL tag a -> Eff fs a
+handleLogSW s w = \case
+  Push push => modifyAt s $ \lst =>
+    foldl applyPush (fromMaybe defaultLogLevels (head' lst)) push :: lst
+  Pop => stateAt s $ maybe (False, []) (True,) . tail'
+  SayMany cat loc msgs => do
+    catLvl <- getsAt s $ fst . getLevel cat
+    let loc = runPretty $ prettyLoc loc
+    for_ msgs $ \(lvl :> msg) => when (lvl <= catLvl) $ tellAt w $
+      hcat [loc, text cat.fst, "@", pshow lvl, ":"] <++> msg
+  CurLevels =>
+    getsAt s getCurLevels
+
+export %inline
+handleLogSW_ : LogL tag a -> Eff [State LevelStack, Writer LogDoc] a
+handleLogSW_ = handleLogSW () ()
+
+export %inline
+handleLogIO : HasIO m => MonadRec m =>
+              (FileError -> m ()) -> IORef LevelStack -> File ->
+              LogL tag a -> m a
+handleLogIO th lvls h act =
+  runEff (handleLogSW_ act) [handleStateIORef lvls, handleWriter {m} printMsg]
+where printMsg : LogDoc -> m ()
+      printMsg msg = fPutStr h (render _ msg) >>= either th pure
+
+export %inline
+handleLogST : HasST m => MonadRec (m s) =>
+              STRef s (SnocList LogDoc) -> STRef s LevelStack ->
+              LogL tag a -> m s a
+handleLogST docs lvls act =
+  runEff (handleLogSW_ act) [handleStateSTRef lvls, handleWriterSTRef docs]
+
+export %inline
+handleLogDiscard : (0 s : ts) -> Has (StateL s Nat) fs =>
+                   LogL tag a -> Eff fs a
+handleLogDiscard s = \case
+  Push _     => modifyAt s S
+  Pop        => stateAt s $ \k => (k > 0, pred k)
+  SayMany {} => pure ()
+  CurLevels  => pure defaultLogLevels
+
+export %inline
+handleLogDiscard_ : LogL tag a -> Eff [State Nat] a
+handleLogDiscard_ = handleLogDiscard ()
+
+export %inline
+handleLogDiscardST : HasST m => MonadRec (m s) => STRef s Nat ->
+                     LogL tag a -> m s a
+handleLogDiscardST ref act =
+  runEff (handleLogDiscard_ act) [handleStateSTRef ref]
+
+export %inline
+handleLogDiscardIO : HasIO m => MonadRec m => IORef Nat ->
+                     LogL tag a -> m a
+handleLogDiscardIO ref act =
+  runEff (handleLogDiscard_ act) [handleStateIORef ref]
+
+
+||| approximate the push/pop effects in a discarded log by trimming a stack or
+||| repeating its most recent element
+export %inline
+fixupDiscardedLog : Nat -> LevelStack -> LevelStack
+fixupDiscardedLog want lvls =
+  let len = length lvls in
+  case compare len want of
+    EQ => lvls
+    GT => drop (len `minus` want) lvls
+    LT => let new = fromMaybe defaultLogLevels $ head' lvls in
+          replicate (want `minus` len) new ++ lvls

lib/Quox/Name.idr

@@ -43,14 +43,14 @@ Mods = SnocList String
 
 public export
 record Name where
-  constructor MakeName
+  constructor MkName
   mods : Mods
   base : BaseName
 %runElab derive "Name" [Eq, Ord]
 
 public export %inline
 unq : BaseName -> Name
-unq = MakeName [<]
+unq = MkName [<]
 
 ||| add some namespaces to the beginning of a name
 public export %inline
@@ -64,31 +64,31 @@ PBaseName = String
 
 public export
 record PName where
-  constructor MakePName
+  constructor MkPName
   mods : Mods
   base : PBaseName
 %runElab derive "PName" [Eq, Ord, PrettyVal]
 
 export %inline
 fromPName : PName -> Name
-fromPName p = MakeName p.mods $ UN p.base
+fromPName p = MkName p.mods $ UN p.base
 
 export %inline
 toPName : Name -> PName
-toPName p = MakePName p.mods $ baseStr p.base
+toPName p = MkPName p.mods $ baseStr p.base
 
 export %inline
 fromPBaseName : PBaseName -> Name
-fromPBaseName = MakeName [<] . UN
+fromPBaseName = MkName [<] . UN
 
 export
 Show PName where
-  show (MakePName mods base) =
+  show (MkPName mods base) =
     show $ concat $ intersperse "." $ toList $ mods :< base
 
 export Show Name where show = show . toPName
 
-export FromString PName where fromString = MakePName [<]
+export FromString PName where fromString = MkPName [<]
 
 export FromString Name where fromString = fromPBaseName
 
@@ -116,7 +116,7 @@ export
 fromListP : List1 String -> PName
 fromListP (x ::: xs) = go [<] x xs where
   go : SnocList String -> String -> List String -> PName
-  go mods x []        = MakePName mods x
+  go mods x []        = MkPName mods x
   go mods x (y :: ys) = go (mods :< x) y ys
 
 export %inline

lib/Quox/Parser/FromParser.idr

@@ -32,48 +32,50 @@ data StateTag = NS | SEEN
 
 public export
 FromParserPure : List (Type -> Type)
-FromParserPure = [Except Error, DefsState, StateL NS Mods, NameGen]
+FromParserPure = [Except Error, DefsState, StateL NS Mods, NameGen, Log]
 
 public export
 FromParserIO : List (Type -> Type)
 FromParserIO = FromParserPure ++ [LoadFile]
 
 
+public export
+record PureParserResult a where
+  constructor MkPureParserResult
+  val       : a
+  suf       : NameSuf
+  defs      : Definitions
+  log       : SnocList LogDoc
+  logLevels : LevelStack
+
 export
-fromParserPure : {default [<] ns : Mods} ->
-                 NameSuf -> Definitions ->
-                 Eff FromParserPure a ->
-                 Either Error (a, NameSuf, Definitions)
-fromParserPure suf defs act = runSTErr $ do
-  suf  <- liftST $ newSTRef suf
-  defs <- liftST $ newSTRef defs
+fromParserPure : Mods -> NameSuf -> Definitions -> LevelStack ->
+                 Eff FromParserPure a -> Either Error (PureParserResult a)
+fromParserPure ns suf defs lvls act = runSTErr $ do
+  suf  <- newSTRef' suf
+  defs <- newSTRef' defs
+  log  <- newSTRef' [<]
+  lvls <- newSTRef' lvls
   res  <- runEff act $ with Union.(::)
-    [handleExcept (\e => stLeft e),
+    [handleExcept $ \e => stLeft e,
      handleStateSTRef defs,
-     handleStateSTRef !(liftST $ newSTRef ns),
-     handleStateSTRef suf]
-  pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
-
-
-export covering
-fromParserIO : (MonadRec io, HasIO io) =>
-               IncludePath -> IORef SeenSet ->
-               IORef NameSuf -> IORef Definitions ->
-               Eff FromParserIO a -> io (Either Error a)
-fromParserIO inc seen suf defs act =
-  liftIO $ fromIOErr $ runEff act $ with Union.(::)
-    [handleExcept (\e => ioLeft e),
-     handleStateIORef defs,
-     handleStateIORef !(newIORef [<]),
-     handleStateIORef suf,
-     handleLoadFileIOE LoadError WrapParseError seen inc]
+     handleStateSTRef !(newSTRef' ns),
+     handleStateSTRef suf,
+     handleLogST log lvls]
+  pure $ MkPureParserResult {
+    val       = res,
+    suf       = !(readSTRef' suf),
+    defs      = !(readSTRef' defs),
+    log       = !(readSTRef' log),
+    logLevels = !(readSTRef' lvls)
+  }
 
 
 parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
            (xs : Context' PatVar n)
   private
   fromBaseName : PBaseName -> m a
-  fromBaseName x = maybe (f $ MakePName [<] x) b $
+  fromBaseName x = maybe (f $ MkPName [<] x) b $
                    Context.find (\y => y.name == Just x) xs
 
   private
@@ -328,6 +330,7 @@ liftTC : Eff TC a -> Eff FromParserPure a
 liftTC tc = runEff tc $ with Union.(::)
   [handleExcept $ \e => throw $ WrapTypeError e,
    handleReaderConst !(getAt DEFS),
+   \g => send g,
    \g => send g]
 
 private
@@ -370,8 +373,9 @@ data HasFail = NoFail | AnyFail | FailWith String
 
 export covering
 expectFail : Loc -> Eff FromParserPure a -> Eff FromParserPure Error
-expectFail loc act =
-  case fromParserPure !(getAt GEN) !(getAt DEFS) {ns = !(getAt NS)} act of
+expectFail loc act = do
+  gen <- getAt GEN; defs <- getAt DEFS; ns <- getAt NS; lvl <- curLevels
+  case fromParserPure ns gen defs (singleton lvl) act of
     Left  err => pure err
     Right _   => throw $ ExpectedFail loc
 
@@ -394,6 +398,10 @@ fromPDecl (PDef def) =
 fromPDecl (PNs  ns)  =
   maybeFail ns.fail ns.loc $
   localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
+fromPDecl (PPrag prag) =
+  case prag of
+    PLogPush p _ => Log.push p $> []
+    PLogPop    _ => Log.pop    $> []
 
 mutual
   export covering

lib/Quox/Parser/Lexer.idr

@@ -247,7 +247,7 @@ public export
 reserved : List Reserved
 reserved =
   [Punc1 "(", Punc1 ")", Punc1 "[", Punc1 "]", Punc1 "{", Punc1 "}",
-   Punc1 ",", Punc1 ";", Punc1 "#[",
+   Punc1 ",", Punc1 ";", Punc1 "#[", Punc1 "#![",
    Sym1 "@",
    Sym1 ":",
    Sym "⇒" `Or` Sym "=>",

lib/Quox/Parser/Parser.idr

@@ -124,7 +124,7 @@ qname = terminalMatch "name" `(Name n) `(n)
 ||| unqualified name
 export
 baseName : Grammar True PBaseName
-baseName = terminalMatch "unqualified name" `(Name (MakePName [<] b)) `(b)
+baseName = terminalMatch "unqualified name" `(Name (MkPName [<] b)) `(b)
 
 ||| dimension constant (0 or 1)
 export
@@ -152,7 +152,7 @@ qty fname = withLoc fname [|PQ qtyVal|]
 export
 exactName : String -> Grammar True ()
 exactName name = terminal "expected '\{name}'" $ \case
-  Name (MakePName [<] x) => guard $ x == name
+  Name (MkPName [<] x) => guard $ x == name
   _                    => Nothing
 
 
@@ -626,14 +626,19 @@ term fname = lamTerm fname
 
 
 export
-attr : FileName -> Grammar True PAttr
-attr fname = withLoc fname $ do
-  resC "#["
+attr' : FileName -> (o : String) -> (0 _ : IsReserved o) =>
+        Grammar True PAttr
+attr' fname o = withLoc fname $ do
+  resC o
   name <- baseName
   args <- many $ termArg fname
   mustWork $ resC "]"
   pure $ PA name args
 
+export %inline
+attr : FileName -> Grammar True PAttr
+attr fname = attr' fname "#["
+
 export
 findDups : List PAttr -> List String
 findDups attrs =
@@ -658,44 +663,48 @@ attrList fname = do
   noDups res $> res
 
 public export
-data AttrMatch a = Matched a | NoMatch String | Malformed String String
+data AttrMatch a =
+    Matched a
+  | NoMatch String (List String)
+  | Malformed String String
 
 export
 Functor AttrMatch where
   map f (Matched x)     = Matched $ f x
-  map f (NoMatch s)     = NoMatch s
+  map f (NoMatch s w)   = NoMatch s w
   map f (Malformed a e) = Malformed a e
 
 export
 (<|>) : AttrMatch a -> AttrMatch a -> AttrMatch a
 Matched x     <|> _ = Matched x
-NoMatch _     <|> y = y
+NoMatch {}    <|> y = y
 Malformed a e <|> _ = Malformed a e
 
 export
-isFail : PAttr -> AttrMatch PFail
-isFail (PA "fail" []        _) = Matched PFailAny
-isFail (PA "fail" [Str s _] _) = Matched $ PFailMatch s
-isFail (PA "fail" _ _) = Malformed "fail" "be absent or a string literal"
-isFail a = NoMatch a.name
+isFail : PAttr -> List String -> AttrMatch PFail
+isFail (PA "fail" []        _) _ = Matched PFailAny
+isFail (PA "fail" [Str s _] _) _ = Matched $ PFailMatch s
+isFail (PA "fail" _ _) _ = Malformed "fail" "be absent or a string literal"
+isFail a w = NoMatch a.name w
 
 export
-isMain : PAttr -> AttrMatch ()
-isMain (PA "main" [] _) = Matched ()
-isMain (PA "main" _  _) = Malformed "main" "have no arguments"
-isMain a = NoMatch a.name
+isMain : PAttr -> List String -> AttrMatch ()
+isMain (PA "main" [] _) _ = Matched ()
+isMain (PA "main" _  _) _ = Malformed "main" "have no arguments"
+isMain a w = NoMatch a.name w
 
 export
-isScheme : PAttr -> AttrMatch String
-isScheme (PA "compile-scheme" [Str s _] _) = Matched s
-isScheme (PA "compile-scheme" _ _) =
+isScheme : PAttr -> List String -> AttrMatch String
+isScheme (PA "compile-scheme" [Str s _] _) _ = Matched s
+isScheme (PA "compile-scheme" _ _) _ =
   Malformed "compile-scheme" "be a string literal"
-isScheme a = NoMatch a.name
+isScheme a w = NoMatch a.name w
 
 export
 matchAttr : String -> AttrMatch a -> Either String a
 matchAttr _ (Matched x) = Right x
-matchAttr d (NoMatch a) = Left "unrecognised \{d} attribute \{a}"
+matchAttr d (NoMatch a w) = Left $ unlines
+  ["unrecognised \{d} attribute \{a}", "expected one of: \{show w}"]
 matchAttr _ (Malformed a s) = Left $ unlines
   ["invalid \{a} attribute", "(should \{s})"]
 
@@ -710,10 +719,12 @@ where
   data PDefAttr = DefFail PFail | DefMain | DefScheme String
 
   isDefAttr : PAttr -> Either String PDefAttr
-  isDefAttr attr = matchAttr "definition" $
-        DefFail   <$> isFail attr
-    <|> DefMain   <$  isMain attr
-    <|> DefScheme <$> isScheme attr
+  isDefAttr attr =
+    let defAttrs = ["fail", "main", "compile-scheme"] in
+    matchAttr "definition" $
+        DefFail   <$> isFail attr defAttrs
+    <|> DefMain   <$  isMain attr defAttrs
+    <|> DefScheme <$> isScheme attr defAttrs
 
   addAttr : PDefinition -> PAttr -> Either String PDefinition
   addAttr def attr =
@@ -730,7 +741,7 @@ mkPNamespace attrs name decls = do
   res <- foldlM addAttr start attrs
   pure $ \l => {loc_ := l} (the PNamespace res)
 where
-  isNsAttr = matchAttr "namespace" . isFail
+  isNsAttr a = matchAttr "namespace" $ isFail a ["fail"]
 
   addAttr : PNamespace -> PAttr -> Either String PNamespace
   addAttr ns attr = pure $ {fail := !(isNsAttr attr)} ns
@@ -785,6 +796,48 @@ export
 nsname : Grammar True Mods
 nsname = do ns <- qname; pure $ ns.mods :< ns.base
 
+export
+pragma : FileName -> Grammar True PPragma
+pragma fname = do
+  a <- attr' fname "#!["
+  either fatalError pure $ case a.name of
+    "log" => logArgs a.args a.loc
+    _     => Left $
+      #"unrecognised pragma "\#{a.name}"\n"# ++
+      #"known pragmas: ["log"]"#
+where
+  levelOOB : Nat -> Either String a
+  levelOOB n = Left $
+    "log level \{show n} out of bounds\n" ++
+    "expected number in range 0–\{show maxLogLevel} inclusive"
+
+  toLevel : Nat -> Either String LogLevel
+  toLevel lvl = maybe (levelOOB lvl) Right $ toLogLevel lvl
+
+  unknownCat : String -> Either String a
+  unknownCat cat = Left $
+    "unknown log category \{show cat}\n" ++
+    "known categories: \{show $ ["all", "default"] ++ logCategories}"
+
+  toCat : String -> Either String LogCategory
+  toCat cat = maybe (unknownCat cat) Right $ toLogCategory cat
+
+  fromPair : PTerm -> Either String (String, Nat)
+  fromPair (Pair (V (MkPName [<] x) Nothing _) (Nat n _) _) = Right (x, n)
+  fromPair _ = Left "invalid argument to log pragma"
+
+  logCatArg : (String, Nat) -> Either String Log.PushArg
+  logCatArg ("default", lvl) = [|SetDefault $ toLevel lvl|]
+  logCatArg ("all",     lvl) = [|SetAll $ toLevel lvl|]
+  logCatArg (cat,       lvl) = [|SetCat (toCat cat) (toLevel lvl)|]
+
+  logArgs : List PTerm -> Loc -> Either String PPragma
+  logArgs [] _ = Left "missing arguments to log pragma"
+  logArgs [V "pop" Nothing _] loc = Right $ PLogPop loc
+  logArgs other loc = do
+    args <- traverse (logCatArg <=< fromPair) other
+    pure $ PLogPush args loc
+
 
 export
 decl : FileName -> Grammar True PDecl
@@ -806,7 +859,9 @@ declBody fname attrs =
   [|PDef $ definition fname attrs|] <|> [|PNs $ namespace_ fname attrs|]
 
 -- decl : FileName -> Grammar True PDecl
-decl fname = attrList fname >>= declBody fname
+decl fname =
+      (attrList fname >>= declBody fname)
+  <|> PPrag <$> pragma fname
 
 export
 load : FileName -> Grammar True PTopLevel

lib/Quox/Parser/Syntax.idr

@@ -4,6 +4,7 @@ import public Quox.Loc
 import public Quox.Syntax
 import public Quox.Definition
 import Quox.PrettyValExtra
+import public Quox.Log
 
 import Derive.Prelude
 %hide TT.Name
@@ -17,7 +18,7 @@ data PatVar = Unused Loc | PV PBaseName Loc
 %name PatVar v
 %runElab derive "PatVar" [Eq, Ord, Show, PrettyVal]
 
-export
+export %inline
 Located PatVar where
   (Unused loc).loc = loc
   (PV _   loc).loc = loc
@@ -41,7 +42,7 @@ record PQty where
 %name PQty qty
 %runElab derive "PQty" [Eq, Ord, Show, PrettyVal]
 
-export Located PQty where q.loc = q.loc_
+export %inline Located PQty where q.loc = q.loc_
 
 namespace PDim
   public export
@@ -49,7 +50,7 @@ namespace PDim
   %name PDim p, q
   %runElab derive "PDim" [Eq, Ord, Show, PrettyVal]
 
-export
+export %inline
 Located PDim where
   (K _ loc).loc = loc
   (V _ loc).loc = loc
@@ -118,7 +119,7 @@ namespace PTerm
 
 %runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show, PrettyVal]
 
-export
+export %inline
 Located PTerm where
   (TYPE    _             loc).loc = loc
   (IOState               loc).loc = loc
@@ -148,7 +149,7 @@ Located PTerm where
   (Comp    _ _ _ _ _ _ _ loc).loc = loc
   (Let     _ _           loc).loc = loc
 
-export
+export %inline
 Located PCaseBody where
   (CasePair _ _ loc).loc = loc
   (CaseEnum _   loc).loc = loc
@@ -182,7 +183,19 @@ record PDefinition where
 %name PDefinition def
 %runElab derive "PDefinition" [Eq, Ord, Show, PrettyVal]
 
-export Located PDefinition where def.loc = def.loc_
+export %inline Located PDefinition where def.loc = def.loc_
+
+public export
+data PPragma =
+    PLogPush (List Log.PushArg) Loc
+  | PLogPop  Loc
+%name PPragma prag
+%runElab derive "PPragma" [Eq, Ord, Show, PrettyVal]
+
+export %inline
+Located PPragma where
+  (PLogPush _ loc).loc = loc
+  (PLogPop    loc).loc = loc
 
 mutual
   public export
@@ -198,22 +211,24 @@ mutual
   data PDecl =
       PDef  PDefinition
     | PNs   PNamespace
+    | PPrag PPragma
   %name PDecl decl
 %runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show, PrettyVal]
 
-export Located PNamespace where ns.loc = ns.loc_
+export %inline Located PNamespace where ns.loc = ns.loc_
 
-export
+export %inline
 Located PDecl where
   (PDef  d).loc    = d.loc
   (PNs   ns).loc   = ns.loc
+  (PPrag prag).loc = prag.loc
 
 public export
 data PTopLevel = PD PDecl | PLoad String Loc
 %name PTopLevel t
 %runElab derive "PTopLevel" [Eq, Ord, Show, PrettyVal]
 
-export
+export %inline
 Located PTopLevel where
   (PD    decl).loc  = decl.loc
   (PLoad _ loc).loc = loc
@@ -228,7 +243,7 @@ record PAttr where
 %name PAttr attr
 %runElab derive "PAttr" [Eq, Ord, Show, PrettyVal]
 
-export Located PAttr where attr.loc = attr.loc_
+export %inline Located PAttr where attr.loc = attr.loc_
 
 
 public export

lib/Quox/PrettyValExtra.idr

@@ -1,5 +1,6 @@
 module Quox.PrettyValExtra
 
+import Data.DPair
 import Derive.Prelude
 import public Text.Show.Value
 import public Text.Show.PrettyVal
@@ -8,3 +9,12 @@ import public Text.Show.PrettyVal.Derive
 %language ElabReflection
 
 %runElab derive "SnocList" [PrettyVal]
+
+
+export %inline
+PrettyVal a => PrettyVal (Subset a p) where
+  prettyVal (Element x _) = Con "Element" [prettyVal x, Con "_" []]
+
+export %inline
+(forall x. PrettyVal (p x)) => PrettyVal (Exists p) where
+  prettyVal (Evidence _ p) = Con "Evidence" [Con "_" [], prettyVal p]

lib/Quox/Syntax/DimEq.idr

@@ -59,10 +59,15 @@ Traversable (IfConsistent eqs) where
   traverse f Nothing  = pure Nothing
   traverse f (Just x) = Just <$> f x
 
+public export
+ifConsistentElse : Applicative f => (eqs : DimEq d) ->
+                   f a -> f () -> f (IfConsistent eqs a)
+ifConsistentElse ZeroIsOne yes no = Nothing <$  no
+ifConsistentElse (C _)     yes no = Just    <$> yes
+
 public export
 ifConsistent : Applicative f => (eqs : DimEq d) -> f a -> f (IfConsistent eqs a)
-ifConsistent ZeroIsOne act = pure Nothing
-ifConsistent (C _)     act = Just <$> act
+ifConsistent eqs act = ifConsistentElse eqs act (pure ())
 
 public export
 toMaybe : IfConsistent eqs a -> Maybe a

lib/Quox/Syntax/Term/Pretty.idr

@@ -229,7 +229,6 @@ prettyDTApps dnames tnames f xs = do
 private
 record CaseArm opts d n where
   constructor MkCaseArm
-  {0 dinner, ninner : Nat}
   pat    : Doc opts
   dbinds : BTelescope d dinner -- 🍴
   tbinds : BTelescope n ninner
@@ -297,7 +296,7 @@ prettyCase_ : {opts : _} ->
               Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
               Eff Pretty (Doc opts)
 prettyCase_ dnames tnames intro head ret body = do
-  head   <- assert_total prettyElim dnames tnames head
+  head   <- withPrec Outer $ assert_total prettyElim dnames tnames head
   ret    <- prettyCaseRet dnames tnames ret
   bodys  <- prettyCaseBody dnames tnames body
   return <- returnD; of_ <- ofD
@@ -325,11 +324,6 @@ private
 LetExpr : Nat -> Nat -> Nat -> Type
 LetExpr d n n' = (Telescope (LetBinder d) n n', Term d n')
 
-private
-PrettyLetResult : LayoutOpts -> Nat -> Type
-PrettyLetResult opts d =
-  Exists $ \n => (BContext n, Term d n, SnocList (Doc opts))
-
 -- [todo] factor out this and the untyped version somehow
 export
 splitLet : Telescope (LetBinder d) n n' -> Term d n' -> Exists (LetExpr d n)
@@ -364,9 +358,10 @@ prettyLets dnames xs lets = snd <$> go lets where
     Nothing => do
       e <- withPrec Outer $ assert_total prettyElim dnames tnames e
       eq <- cstD; d <- askAt INDENT
+      inn <- inD
       pure $ ifMultiline
-        (hsep [hdr, eq, e])
-        (vsep [hdr, indent d $ hsep [eq, e]])
+        (hsep [hdr, eq, e, inn])
+        (vsep [hdr, indent d $ hsep [eq, e, inn]])
 
   go : forall b. Telescope (LetBinder d) a b ->
        Eff Pretty (BContext b, SnocList (Doc opts))
@@ -437,13 +432,10 @@ prettyDisp u = map Just $ hl Universe =<<
   ifUnicode (text $ superscript $ show u) (text $ "^" ++ show u)
 
 
-prettyTerm dnames tnames (TYPE l _) =
-  case !(askAt FLAVOR) of
-    Unicode => do
-      star  <- hl Syntax "★"
-      level <- hl Universe $ text $ superscript $ show l
-      pure $ hcat [star, level]
-    Ascii   => [|hl Syntax "Type" <++> hl Universe (text $ show l)|]
+prettyTerm dnames tnames (TYPE l _) = do
+  type  <- hl Syntax . text =<< ifUnicode "★" "Type"
+  level <- prettyDisp l
+  pure $ maybe type (type <+>) level
 
 prettyTerm dnames tnames (IOState _) =
   ioStateD

lib/Quox/Typechecker.idr

@@ -3,6 +3,7 @@ module Quox.Typechecker
 import public Quox.Typing
 import public Quox.Equal
 import Quox.Displace
+import Quox.Pretty
 
 import Data.List
 import Data.SnocVect
@@ -14,7 +15,7 @@ import Quox.EffExtra
 
 public export
 0 TC : List (Type -> Type)
-TC = [ErrorEff, DefsReader, NameGen]
+TC = [ErrorEff, DefsReader, NameGen, Log]
 
 
 parameters (loc : Loc)
@@ -41,6 +42,24 @@ lubs ctx []        = zeroFor ctx
 lubs ctx (x :: xs) = lubs1 $ x ::: xs
 
 
+private
+prettyTermTC : {opts : LayoutOpts} ->
+               TyContext d n -> Term d n -> Eff Pretty (Doc opts)
+prettyTermTC ctx s = prettyTerm ctx.dnames ctx.tnames s
+
+
+private
+checkLogs : String -> TyContext d n -> SQty ->
+            Term d n -> Maybe (Term d n) -> Eff TC ()
+checkLogs fun ctx sg subj ty = do
+  let tyDoc = delay $ maybe (text "none") (runPretty . prettyTermTC ctx) ty
+  sayMany "check" subj.loc
+    [10 :> text fun,
+     95 :> hsep ["ctx =",  runPretty $ prettyTyContext ctx],
+     95 :> hsep ["sg =",   runPretty $ prettyQty sg.qty],
+     10 :> hsep ["subj =", runPretty $ prettyTermTC ctx subj],
+     10 :> hsep ["ty =",   tyDoc]]
+
 mutual
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
   |||
@@ -53,7 +72,11 @@ mutual
   export covering %inline
   check : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
           Eff TC (CheckResult ctx.dctx n)
-  check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty
+  check ctx sg subj ty =
+    ifConsistentElse ctx.dctx
+      (do checkLogs "check" ctx sg subj (Just ty)
+          checkC ctx sg subj ty)
+      (say "check" 20 subj.loc "check: 0=1")
 
   ||| "Ψ | Γ ⊢₀ s ⇐ A"
   |||
@@ -84,7 +107,12 @@ mutual
   ||| universe doesn't matter, only that a term is _a_ type, so it is optional.
   export covering %inline
   checkType : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
-  checkType ctx subj l = ignore $ ifConsistent ctx.dctx $ checkTypeC ctx subj l
+  checkType ctx subj l = do
+    let univ = TYPE <$> l <*> pure noLoc
+    ignore $ ifConsistentElse ctx.dctx
+      (do checkLogs "checkType" ctx SZero subj univ
+          checkTypeC ctx subj l)
+      (say "check" 20 subj.loc "checkType: 0=1")
 
   export covering %inline
   checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
@@ -107,7 +135,11 @@ mutual
   export covering %inline
   infer : (ctx : TyContext d n) -> SQty -> Elim d n ->
           Eff TC (InferResult ctx.dctx d n)
-  infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj
+  infer ctx sg subj = do
+    ifConsistentElse ctx.dctx
+      (do checkLogs "infer" ctx sg (E subj) Nothing
+          inferC ctx sg subj)
+      (say "check" 20 subj.loc "infer: 0=1")
 
   ||| `infer`, assuming the dimension context is consistent
   export covering %inline

lib/Quox/Typing.idr

@@ -7,6 +7,7 @@ import public Quox.Typing.Error as Typing
 import public Quox.Syntax
 import public Quox.Definition
 import public Quox.Whnf
+import public Quox.Pretty
 
 import Language.Reflection
 import Control.Eff
@@ -47,15 +48,14 @@ public export
 substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n)
 substCasePairRet [< x, y] dty retty =
   let tm  = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc
-      arg = Ann tm (dty // fromNat 2) tm.loc
-  in
+      arg = Ann tm (dty // fromNat 2) tm.loc in
   retty.term // (arg ::: shift 2)
 
 public export
 substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
 substCaseSuccRet [< p, ih] retty =
-  let arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT p.loc) $ p.loc `extendL` ih.loc
-  in
+  let loc = p.loc `extendL` ih.loc
+      arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT p.loc) loc in
   retty.term // (arg ::: shift 2)
 
 public export
@@ -65,23 +65,31 @@ substCaseBoxRet x dty retty =
   retty.term // (arg ::: shift 1)
 
 
-parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
+private
+0 ExpectErrorConstructor : Type
+ExpectErrorConstructor =
+  forall d, n. Loc -> NameContexts d n -> Term d n -> Error
+
+parameters (defs : Definitions)
+           {auto _ : (Has ErrorEff fs, Has NameGen fs, Has Log fs)}
   namespace TyContext
    parameters (ctx : TyContext d n) (sg : SQty) (loc : Loc)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-           tm d n -> Eff fs (NonRedex tm d n defs ? sg)
+           tm d n -> Eff fs (NonRedex tm d n defs (toWhnfContext ctx) sg)
     whnf tm = do
       let Val n = ctx.termLen; Val d = ctx.dimLen
       res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
       rethrow res
 
     private covering %macro
-    expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> Error) ->
-             TTImp -> TTImp -> Elab (Term d n -> Eff fs a)
-    expect k l r = do
-      f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
-      pure $ \t => maybe (throw $ k loc ctx.names t) pure . f . fst =<< whnf t
+    expect : ExpectErrorConstructor -> TTImp -> TTImp ->
+             Elab (Term d n -> Eff fs a)
+    expect err pat rhs = Prelude.do
+      match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
+      pure $ \term => do
+        res <- whnf term
+        maybe (throw $ err loc ctx.names term) pure $ match $ fst res
 
     export covering %inline
     expectTYPE : Term d n -> Eff fs Universe
@@ -120,19 +128,20 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
    parameters (ctx : EqContext n) (sg : SQty) (loc : Loc)
     export covering
     whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
-           tm 0 n -> Eff fs (NonRedex tm 0 n defs ? sg)
+           tm 0 n -> Eff fs (NonRedex tm 0 n defs (toWhnfContext ctx) sg)
     whnf tm = do
       res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
       rethrow res
 
     private covering %macro
-    expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> Error) ->
-             TTImp -> TTImp -> Elab (Term 0 n -> Eff fs a)
-    expect k l r = do
-      f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
-      pure $ \t =>
-        let err = throw $ k loc ctx.names (t // shift0 ctx.dimLen) in
-        maybe err pure . f . fst =<< whnf t
+    expect : ExpectErrorConstructor -> TTImp -> TTImp ->
+             Elab (Term 0 n -> Eff fs a)
+    expect err pat rhs = do
+      match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
+      pure $ \term => do
+        res <- whnf term
+        let t0 = delay $ term // shift0 ctx.dimLen
+        maybe (throw $ err loc ctx.names t0) pure $ match $ fst res
 
     export covering %inline
     expectTYPE : Term 0 n -> Eff fs Universe

lib/Quox/Typing/Context.idr

@@ -339,9 +339,10 @@ namespace WhnfContext
 private
 prettyTContextElt : {opts : _} ->
                     BContext d -> BContext n ->
-                    Qty -> BindName -> LocalVar d n -> Eff Pretty (Doc opts)
+                    Doc opts -> BindName -> LocalVar d n ->
+                    Eff Pretty (Doc opts)
 prettyTContextElt dnames tnames q x s = do
-  q  <- prettyQty q;   dot <- dotD
+  dot <- dotD
   x  <- prettyTBind x; colon <- colonD
   ty <- withPrec Outer $ prettyTerm dnames tnames s.type; eq <- cstD
   tm <- traverse (withPrec Outer . prettyTerm dnames tnames) s.term
@@ -356,7 +357,7 @@ prettyTContextElt dnames tnames q x s = do
 
 private
 prettyTContext' : {opts : _} ->
-                  BContext d -> QContext n -> BContext n ->
+                  BContext d -> Context' (Doc opts) n -> BContext n ->
                   TContext d n -> Eff Pretty (SnocList (Doc opts))
 prettyTContext' _ [<] [<] [<] = pure [<]
 prettyTContext' dnames (qtys :< q) (tnames :< x) (tys :< t) =
@@ -369,6 +370,7 @@ prettyTContext : {opts : _} ->
                  TContext d n -> Eff Pretty (Doc opts)
 prettyTContext dnames qtys tnames tys = do
   comma <- commaD
+  qtys <- traverse prettyQty qtys
   sepSingle . exceptLast (<+> comma) . toList <$>
     prettyTContext' dnames qtys tnames tys
 
@@ -384,3 +386,10 @@ prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
 export
 prettyEqContext : {opts : _} -> EqContext n -> Eff Pretty (Doc opts)
 prettyEqContext ctx = prettyTyContext $ toTyContext ctx
+
+export
+prettyWhnfContext : {opts : _} -> WhnfContext d n -> Eff Pretty (Doc opts)
+prettyWhnfContext ctx =
+  let Val n = ctx.termLen in
+  sepSingle . exceptLast (<+> comma) . toList <$>
+    prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx

lib/Quox/Untyped/Erase.idr

@@ -88,7 +88,7 @@ parameters {opts : LayoutOpts} (showContext : Bool)
 
 public export
 Erase : List (Type -> Type)
-Erase = [Except Error, NameGen]
+Erase = [Except Error, NameGen, Log]
 
 export
 liftWhnf : Eff Whnf a -> Eff Erase a

lib/Quox/Untyped/Scheme.idr

@@ -113,13 +113,13 @@ makeIdBase mods str = joinBy "." $ toList $ mods :< str
 
 export
 makeId : Name -> Id
-makeId (MakeName mods (UN str))   = I (makeIdBase mods str) 0
-makeId (MakeName mods (MN str k)) = I (makeIdBase mods str) 0
-makeId (MakeName mods Unused)     = I (makeIdBase mods "_") 0
+makeId (MkName mods (UN str))   = I (makeIdBase mods str) 0
+makeId (MkName mods (MN str k)) = I (makeIdBase mods str) 0
+makeId (MkName mods Unused)     = I (makeIdBase mods "_") 0
 
 export
 makeIdB : BindName -> Id
-makeIdB (BN name _) = makeId $ MakeName [<] name
+makeIdB (BN name _) = makeId $ MkName [<] name
 
 private
 bump : Id -> Id

lib/Quox/Whnf/ComputeElimType.idr

@@ -2,6 +2,7 @@ module Quox.Whnf.ComputeElimType
 
 import Quox.Whnf.Interface
 import Quox.Displace
+import Quox.Pretty
 
 %default total
 
@@ -18,7 +19,6 @@ computeElimType :
   (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
   Eff Whnf (Term d n)
 
-
 ||| computes a type and then reduces it to whnf
 export covering
 computeWhnfElimType0 :
@@ -28,7 +28,16 @@ computeWhnfElimType0 :
   (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
   Eff Whnf (Term d n)
 
-computeElimType defs ctx sg e =
+
+private covering
+computeElimTypeNoLog, computeWhnfElimType0NoLog :
+  CanWhnf Term Interface.isRedexT =>
+  CanWhnf Elim Interface.isRedexE =>
+  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
+  (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
+  Eff Whnf (Term d n)
+
+computeElimTypeNoLog defs ctx sg e =
   case e of
     F x u loc => do
       let Just def = lookup x defs
@@ -39,7 +48,7 @@ computeElimType defs ctx sg e =
       pure (ctx.tctx !! i).type
 
     App f s loc =>
-      case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of
         Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
         ty               => throw $ ExpectedPi loc ctx.names ty
 
@@ -47,12 +56,12 @@ computeElimType defs ctx sg e =
       pure $ sub1 ret pair
 
     Fst pair loc =>
-      case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0NoLog defs ctx sg pair {ne = noOr1 ne}) of
         Sig {fst, _} => pure fst
         ty           => throw $ ExpectedSig loc ctx.names ty
 
     Snd pair loc =>
-      case !(computeWhnfElimType0 defs ctx sg pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0NoLog defs ctx sg pair {ne = noOr1 ne}) of
         Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
         ty           => throw $ ExpectedSig loc ctx.names ty
 
@@ -66,7 +75,7 @@ computeElimType defs ctx sg e =
       pure $ sub1 ret box
 
     DApp {fun = f, arg = p, loc} =>
-      case !(computeWhnfElimType0 defs ctx sg f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of
         Eq {ty, _} => pure $ dsub1 ty p
         t          => throw $ ExpectedEq loc ctx.names t
 
@@ -82,5 +91,20 @@ computeElimType defs ctx sg e =
     TypeCase {ret, _} =>
       pure ret
 
+computeElimType defs ctx sg e {ne} = do
+  let Val n = ctx.termLen
+  sayMany "whnf" e.loc
+    [90 :> "computeElimType",
+     95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx],
+     90 :> hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]]
+  res <- computeElimTypeNoLog defs ctx sg e {ne}
+  say "whnf" 91 e.loc $
+    hsep ["computeElimType ⇝",
+          runPretty $ prettyTerm ctx.dnames ctx.tnames res]
+  pure res
+
 computeWhnfElimType0 defs ctx sg e =
   computeElimType defs ctx sg e >>= whnf0 defs ctx SZero
+
+computeWhnfElimType0NoLog defs ctx sg e {ne} =
+  computeElimTypeNoLog defs ctx sg e {ne} >>= whnf0 defs ctx SZero

lib/Quox/Whnf/Interface.idr

@@ -1,6 +1,7 @@
 module Quox.Whnf.Interface
 
 import public Quox.No
+import public Quox.Log
 import public Quox.Syntax
 import public Quox.Definition
 import public Quox.Typing.Context
@@ -13,7 +14,7 @@ import public Control.Eff
 
 public export
 Whnf : List (Type -> Type)
-Whnf = [Except Error, NameGen]
+Whnf = [Except Error, NameGen, Log]
 
 
 public export
@@ -24,7 +25,8 @@ RedexTest tm =
 public export
 interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
-  whnf : (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
+  whnf, whnfNoLog :
+    (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
     tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
   -- having isRedex be part of the class header, and needing to be explicitly
   -- quantified on every use since idris can't infer its type, is a little ugly.
@@ -32,9 +34,11 @@ where
   -- cases idris can't tell that `isRedex` and `isRedexT` are the same thing
 
 public export %inline
-whnf0 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
+whnf0, whnfNoLog0 :
+  {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
   Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
 whnf0      defs ctx q t = fst <$> whnf defs ctx q t
+whnfNoLog0 defs ctx q t = fst <$> whnfNoLog defs ctx q t
 
 public export
 0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>

lib/Quox/Whnf/Main.idr

@@ -4,6 +4,7 @@ import Quox.Whnf.Interface
 import Quox.Whnf.ComputeElimType
 import Quox.Whnf.TypeCase
 import Quox.Whnf.Coercion
+import Quox.Pretty
 import Quox.Displace
 import Data.SnocVect
 
@@ -14,19 +15,43 @@ export covering CanWhnf Term Interface.isRedexT
 export covering CanWhnf Elim Interface.isRedexE
 
 
+-- the String is what to call the "s" argument in logs (maybe "s", or "e")
+private %inline
+whnfDefault :
+  {0 isRedex : RedexTest tm} ->
+  (CanWhnf tm isRedex, Located2 tm) =>
+  String ->
+  (forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) ->
+  (defs : Definitions) ->
+  (ctx : WhnfContext d n) ->
+  (sg : SQty) ->
+  (s : tm d n) ->
+  Eff Whnf (Subset (tm d n) (No . isRedex defs ctx sg))
+whnfDefault name ppr defs ctx sg s = do
+  sayMany "whnf" s.loc
+    [10 :> "whnf",
+     95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx],
+     95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     10 :> hsep [text name, "=", runPretty $ ppr ctx s]]
+  res <- whnfNoLog defs ctx sg s
+  say "whnf" 11 s.loc $ hsep ["whnf ⇝", runPretty $ ppr ctx res.fst]
+  pure res
+
 covering
 CanWhnf Elim Interface.isRedexE where
-  whnf defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
+  whnf = whnfDefault "e" $ \ctx, e => prettyElim ctx.dnames ctx.tnames e
+
+  whnfNoLog defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
     _ | Just y  = whnf defs ctx sg $ setLoc loc $ injElim ctx y
     _ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
 
-  whnf defs ctx sg (B i loc) with (ctx.tctx !! i) proof eq1
+  whnfNoLog defs ctx sg (B i loc) with (ctx.tctx !! i) proof eq1
     _ | l with (l.term) proof eq2
       _ | Just y  = whnf defs ctx sg $ Ann y l.type loc
       _ | Nothing = pure $ Element (B i loc) $ rewrite eq1 in rewrite eq2 in Ah
 
   -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
-  whnf defs ctx sg (App f s appLoc) = do
+  whnfNoLog defs ctx sg (App f s appLoc) = do
     Element f fnf <- whnf defs ctx sg f
     case nchoose $ isLamHead f of
       Left _ => case f of
@@ -41,7 +66,7 @@ CanWhnf Elim Interface.isRedexE where
   --
   -- 0 · case e return p ⇒ C of { (a, b) ⇒ u } ⇝
   -- u[fst e/a, snd e/b] ∷ C[e/p]
-  whnf defs ctx sg (CasePair pi pair ret body caseLoc) = do
+  whnfNoLog defs ctx sg (CasePair pi pair ret body caseLoc) = do
     Element pair pairnf <- whnf defs ctx sg pair
     case nchoose $ isPairHead pair of
       Left _ => case pair of
@@ -64,7 +89,7 @@ CanWhnf Elim Interface.isRedexE where
                            (pairnf `orNo` np `orNo` notYesNo n0)
 
   -- fst ((s, t) ∷ (x : A) × B) ⇝ s ∷ A
-  whnf defs ctx sg (Fst pair fstLoc) = do
+  whnfNoLog defs ctx sg (Fst pair fstLoc) = do
     Element pair pairnf <- whnf defs ctx sg pair
     case nchoose $ isPairHead pair of
       Left _ => case pair of
@@ -76,7 +101,7 @@ CanWhnf Elim Interface.isRedexE where
         pure $ Element (Fst pair fstLoc) (pairnf `orNo` np)
 
   -- snd ((s, t) ∷ (x : A) × B) ⇝ t ∷ B[(s ∷ A)/x]
-  whnf defs ctx sg (Snd pair sndLoc) = do
+  whnfNoLog defs ctx sg (Snd pair sndLoc) = do
     Element pair pairnf <- whnf defs ctx sg pair
     case nchoose $ isPairHead pair of
       Left _ => case pair of
@@ -89,7 +114,7 @@ CanWhnf Elim Interface.isRedexE where
 
   -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
   -- u ∷ C['a∷{a,…}/p]
-  whnf defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
+  whnfNoLog defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
     Element tag tagnf <- whnf defs ctx sg tag
     case nchoose $ isTagHead tag of
       Left _ => case tag of
@@ -110,7 +135,7 @@ CanWhnf Elim Interface.isRedexE where
   --
   -- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
   --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
-  whnf defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
+  whnfNoLog defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
     Element nat natnf <- whnf defs ctx sg nat
     case nchoose $ isNatHead nat of
       Left _ =>
@@ -137,7 +162,7 @@ CanWhnf Elim Interface.isRedexE where
 
   -- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
   --   u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
-  whnf defs ctx sg (CaseBox pi box ret body caseLoc) = do
+  whnfNoLog defs ctx sg (CaseBox pi box ret body caseLoc) = do
     Element box boxnf <- whnf defs ctx sg box
     case nchoose $ isBoxHead box of
       Left _ => case box of
@@ -153,7 +178,7 @@ CanWhnf Elim Interface.isRedexE where
   -- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗›
   --
   -- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
-  whnf defs ctx sg (DApp f p appLoc) = do
+  whnfNoLog defs ctx sg (DApp f p appLoc) = do
     Element f fnf <- whnf defs ctx sg f
     case nchoose $ isDLamHead f of
       Left _ => case f of
@@ -173,7 +198,7 @@ CanWhnf Elim Interface.isRedexE where
         B {} => pure $ Element (DApp f p appLoc) (fnf `orNo` ndlh `orNo` Ah)
 
   -- e ∷ A ⇝ e
-  whnf defs ctx sg (Ann s a annLoc) = do
+  whnfNoLog defs ctx sg (Ann s a annLoc) = do
     Element s snf <- whnf defs ctx sg s
     case nchoose $ isE s of
       Left  _  => let E e = s in pure $ Element e $ noOr2 snf
@@ -181,7 +206,7 @@ CanWhnf Elim Interface.isRedexE where
         Element a anf <- whnf defs ctx SZero a
         pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
 
-  whnf defs ctx sg (Coe sty p q val coeLoc) =
+  whnfNoLog defs ctx sg (Coe sty p q val coeLoc) =
     --   𝑖 ∉ fv(A)
     -- -------------------------------
     --   coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
@@ -201,7 +226,7 @@ CanWhnf Elim Interface.isRedexE where
       (_, Right ty) =>
         whnf defs ctx sg $ Ann val ty coeLoc
 
-  whnf defs ctx sg (Comp ty p q val r zero one compLoc) =
+  whnfNoLog defs ctx sg (Comp ty p q val r zero one compLoc) =
     case p `decEqv` q of
       -- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
       Yes y   => whnf defs ctx sg $ Ann val ty compLoc
@@ -213,7 +238,7 @@ CanWhnf Elim Interface.isRedexE where
         B {}     => pure $ Element (Comp ty p q val r zero one compLoc)
                                    (notYesNo npq `orNo` Ah)
 
-  whnf defs ctx sg (TypeCase ty ret arms def tcLoc) =
+  whnfNoLog defs ctx sg (TypeCase ty ret arms def tcLoc) =
     case sg `decEq` SZero of
       Yes Refl => do
         Element ty  tynf  <- whnf defs ctx SZero ty
@@ -226,48 +251,50 @@ CanWhnf Elim Interface.isRedexE where
       No _ =>
         throw $ ClashQ tcLoc sg.qty Zero
 
-  whnf defs ctx sg (CloE (Sub el th)) =
-    whnf defs ctx sg $ pushSubstsWith' id th el
-  whnf defs ctx sg (DCloE (Sub el th)) =
-    whnf defs ctx sg $ pushSubstsWith' th id el
+  whnfNoLog defs ctx sg (CloE (Sub el th)) =
+    whnfNoLog defs ctx sg $ pushSubstsWith' id th el
+  whnfNoLog defs ctx sg (DCloE (Sub el th)) =
+    whnfNoLog defs ctx sg $ pushSubstsWith' th id el
 
 covering
 CanWhnf Term Interface.isRedexT where
-  whnf _ _ _ t@(TYPE    {}) = pure $ nred t
-  whnf _ _ _ t@(IOState {}) = pure $ nred t
-  whnf _ _ _ t@(Pi      {}) = pure $ nred t
-  whnf _ _ _ t@(Lam     {}) = pure $ nred t
-  whnf _ _ _ t@(Sig     {}) = pure $ nred t
-  whnf _ _ _ t@(Pair    {}) = pure $ nred t
-  whnf _ _ _ t@(Enum    {}) = pure $ nred t
-  whnf _ _ _ t@(Tag     {}) = pure $ nred t
-  whnf _ _ _ t@(Eq      {}) = pure $ nred t
-  whnf _ _ _ t@(DLam    {}) = pure $ nred t
-  whnf _ _ _ t@(NAT     {}) = pure $ nred t
-  whnf _ _ _ t@(Nat     {}) = pure $ nred t
-  whnf _ _ _ t@(STRING  {}) = pure $ nred t
-  whnf _ _ _ t@(Str     {}) = pure $ nred t
-  whnf _ _ _ t@(BOX     {}) = pure $ nred t
-  whnf _ _ _ t@(Box     {}) = pure $ nred t
+  whnf = whnfDefault "e" $ \ctx, s => prettyTerm ctx.dnames ctx.tnames s
 
-  whnf _ _ _ (Succ p loc) =
+  whnfNoLog _ _ _ t@(TYPE    {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(IOState {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Pi      {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Lam     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Sig     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Pair    {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Enum    {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Tag     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Eq      {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(DLam    {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(NAT     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Nat     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(STRING  {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Str     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(BOX     {}) = pure $ nred t
+  whnfNoLog _ _ _ t@(Box     {}) = pure $ nred t
+
+  whnfNoLog _ _ _ (Succ p loc) =
     case nchoose $ isNatConst p of
       Left _ => case p of
         Nat p _               => pure $ nred $ Nat (S p) loc
         E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
       Right nc => pure $ nred $ Succ p loc
 
-  whnf defs ctx sg (Let _ rhs body _) =
+  whnfNoLog defs ctx sg (Let _ rhs body _) =
     whnf defs ctx sg $ sub1 body rhs
 
   -- s ∷ A ⇝ s   (in term context)
-  whnf defs ctx sg (E e) = do
+  whnfNoLog defs ctx sg (E e) = do
     Element e enf <- whnf defs ctx sg e
     case nchoose $ isAnn e of
       Left  _  => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf
       Right na => pure $ Element (E e) $ na `orNo` enf
 
-  whnf defs ctx sg (CloT (Sub tm th)) =
-    whnf defs ctx sg $ pushSubstsWith' id th tm
-  whnf defs ctx sg (DCloT (Sub tm th)) =
-    whnf defs ctx sg $ pushSubstsWith' th id tm
+  whnfNoLog defs ctx sg (CloT (Sub tm th)) =
+    whnfNoLog defs ctx sg $ pushSubstsWith' id th tm
+  whnfNoLog defs ctx sg (DCloT (Sub tm th)) =
+    whnfNoLog defs ctx sg $ pushSubstsWith' th id tm

lib/quox-lib.ipkg

@@ -19,6 +19,7 @@ modules =
   Quox.PrettyValExtra,
   Quox.Decidable,
   Quox.No,
+  Quox.Log,
   Quox.Loc,
   Quox.Var,
   Quox.Scoped,

tests/Tests/DimEq.idr

@@ -97,7 +97,7 @@ tests = "dimension constraints" :- [
     testPrettyD iijj ZeroIsOne "𝑖, 𝑗, 0 = 1",
     testPrettyD [<] new "" {label = "[empty output from empty context]"},
     testPrettyD ii new "𝑖",
-    testPrettyD iijj (fromGround [< "𝑖", "𝑗"] [< Zero, One])
+    testPrettyD iijj (fromGround iijj [< Zero, One])
       "𝑖, 𝑗, 𝑖 = 0, 𝑗 = 1",
     testPrettyD iijj (C [< Just (^K Zero), Nothing])
       "𝑖, 𝑗, 𝑖 = 0",

tests/Tests/Equal.idr

@@ -27,7 +27,7 @@ parameters (label : String) (act : Eff Equal ())
   testEq = test label $ runEqual globals act
 
   testNeq : Test
-  testNeq = testThrows label (const True) $ runTC globals act $> "()"
+  testNeq = testThrows label (const True) $ runTC globals act $> "ok"
 
 
 parameters (ctx : TyContext d n)

tests/Tests/FromPTerm.idr

@@ -68,7 +68,7 @@ parameters {c : Bool} {auto _ : Show b}
 
 runFromParser : {default empty defs : Definitions} ->
                 Eff FromParserPure a -> Either FromParser.Error a
-runFromParser = map fst . fromParserPure 0 defs
+runFromParser = map val . fromParserPure [<] 0 defs initStack
 
 export
 tests : Test

tests/Tests/Lexer.idr

@@ -71,7 +71,7 @@ tests = "lexer" :- [
     lexes "δελτα" [Name "δελτα"],
     lexes "★★" [Name "★★"],
     lexes "Types" [Name "Types"],
-    lexes "a.b.c.d.e" [Name $ MakePName [< "a","b","c","d"] "e"],
+    lexes "a.b.c.d.e" [Name $ MkPName [< "a","b","c","d"] "e"],
     lexes "normalïse" [Name "normalïse"],
       -- ↑ replace i + combining ¨ with precomposed ï
     lexes "map#" [Name "map#"],
@@ -90,16 +90,16 @@ tests = "lexer" :- [
     lexes "***" [Name "***"],
     lexes "+**" [Name "+**"],
     lexes "+#" [Name "+#"],
-    lexes "+.+.+" [Name $ MakePName [< "+", "+"] "+"],
-    lexes "a.+" [Name $ MakePName [< "a"] "+"],
-    lexes "+.a" [Name $ MakePName [< "+"] "a"],
+    lexes "+.+.+" [Name $ MkPName [< "+", "+"] "+"],
+    lexes "a.+" [Name $ MkPName [< "a"] "+"],
+    lexes "+.a" [Name $ MkPName [< "+"] "a"],
 
     lexes "+a" [Name "+", Name "a"],
 
     lexes "x." [Name "x", Reserved "."],
     lexes "&." [Name "&", Reserved "."],
     lexes ".x" [Reserved ".", Name "x"],
-    lexes "a.b.c." [Name $ MakePName [< "a", "b"] "c", Reserved "."],
+    lexes "a.b.c." [Name $ MkPName [< "a", "b"] "c", Reserved "."],
 
     lexes "case" [Reserved "case"],
     lexes "caseω" [Reserved "caseω"],

tests/Tests/Parser.idr

@@ -63,9 +63,9 @@ tests = "parser" :- [
 
   "names" :- [
     parsesAs (const qname) "x"
-      (MakePName [<] "x"),
+      (MkPName [<] "x"),
     parsesAs (const qname) "Data.List.length"
-      (MakePName [< "Data", "List"] "length"),
+      (MkPName [< "Data", "List"] "length"),
     parseFails (const qname) "_"
   ],
 
@@ -124,7 +124,7 @@ tests = "parser" :- [
     parseMatch term "f"
       `(V "f" {}),
     parseMatch term "f.x.y"
-      `(V (MakePName [< "f", "x"] "y") {}),
+      `(V (MkPName [< "f", "x"] "y") {}),
     parseMatch term "f x"
       `(App (V "f" {}) (V "x" {}) _),
     parseMatch term "f x y"
@@ -526,12 +526,56 @@ tests = "parser" :- [
               PSucceed False Nothing _]
             PSucceed _),
          PD (PDef $ MkPDef (PQ Any _) "y"
-          (PConcrete Nothing (V (MakePName [< "a"] "x") Nothing _))
+          (PConcrete Nothing (V (MkPName [< "a"] "x") Nothing _))
           PSucceed False Nothing _)]),
     parseMatch input #" load "a.quox"; def b = a.b "#
       `([PLoad "a.quox" _,
          PD (PDef $ MkPDef (PQ Any _) "b"
-          (PConcrete Nothing (V (MakePName [< "a"] "b") Nothing _))
-          PSucceed False Nothing _)])
+          (PConcrete Nothing (V (MkPName [< "a"] "b") Nothing _))
+          PSucceed False Nothing _)]),
+    parseMatch input #" #[main] postulate hi : String "#
+      `([PD (PDef $ MkPDef (PQ Any _) "hi"
+          (PPostulate (STRING _))
+          PSucceed True Nothing _)]),
+    parseMatch input #" #[compile-scheme "hi"] postulate hi : String "#
+      `([PD (PDef $ MkPDef (PQ Any _) "hi"
+          (PPostulate (STRING _))
+          PSucceed False (Just "hi") _)]),
+    parseMatch input #" #[main] #[compile-scheme "hi"] postulate hi : String "#
+      `([PD (PDef $ MkPDef (PQ Any _) "hi"
+          (PPostulate (STRING _))
+          PSucceed True (Just "hi") _)]),
+    parseMatch input #" #[fail] def hi = "hi!!!! uwu" "#
+      `([PD (PDef $ MkPDef (PQ Any _) "hi"
+          (PConcrete Nothing (Str "hi!!!! uwu" _))
+          PFailAny False Nothing _)]),
+    parseMatch input #" #[fail "type"] def hi = "hi!!!! uwu" "#
+      `([PD (PDef $ MkPDef (PQ Any _) "hi"
+          (PConcrete Nothing (Str "hi!!!! uwu" _))
+          (PFailMatch "type") False Nothing _)]),
+    parseMatch input #" #[fail] namespace ns { } "#
+      `([PD (PNs $ MkPNamespace [< "ns"] [] PFailAny _)]),
+    parseFails input #" #[fail 69] namespace ns { } "#,
+    parseFails input "#[main]",
+    parseFails input "#[main] namespace a { } ",
+    parseFails input #" #[not-an-attr] postulate hi : String "#,
+    parseFails input #" #[log pop] postulate hi : String "#,
+    parseMatch input #" #![log pop] "#
+      `([PD (PPrag (PLogPop _))]),
+    parseMatch input #" #![log (all, 5)] "#
+      `([PD (PPrag (PLogPush [SetAll (Element 5 _)] _))]),
+    parseMatch input #" #![log (default, 69)] "#
+      `([PD (PPrag (PLogPush [SetDefault (Element 69 _)] _))]),
+    parseMatch input #" #![log (whnf, 100)] "#
+      `([PD (PPrag (PLogPush [SetCat (Element "whnf" _) (Element 100 _)] _))]),
+    parseMatch input #" #![log (all, 5) (default, 69) (whnf, 100)] "#
+      `([PD (PPrag (PLogPush
+          [SetAll (Element 5 _), SetDefault (Element 69 _),
+           SetCat (Element "whnf" _) (Element 100 _)] _))]),
+    parseFails input #" #![log] "#,
+    parseFails input #" #![log (non-category, 5)] "#,
+    parseFails input #" #![log (whnf, 50000000)] "#,
+    parseFails input #" #![log [0.★⁵]] "#,
+    parseFails input #" #![main] "#
   ]
 ]

tests/Tests/PrettyTerm.idr

@@ -37,8 +37,8 @@ tests = "pretty printing terms" :- [
   "free vars" :- [
     testPrettyE1 [<] [<] (^F "x" 0) "x",
     testPrettyE  [<] [<] (^F "x" 1) "x¹" "x^1",
-    testPrettyE1 [<] [<] (^F (MakeName [< "A", "B", "C"] "x") 0) "A.B.C.x",
-    testPrettyE  [<] [<] (^F (MakeName [< "A", "B", "C"] "x") 2)
+    testPrettyE1 [<] [<] (^F (MkName [< "A", "B", "C"] "x") 0) "A.B.C.x",
+    testPrettyE  [<] [<] (^F (MkName [< "A", "B", "C"] "x") 2)
       "A.B.C.x²"
       "A.B.C.x^2"
   ],
@@ -105,8 +105,8 @@ tests = "pretty printing terms" :- [
   ],
 
   "type universes" :- [
-    testPrettyT [<] [<] (^TYPE 0) "★⁰" "Type 0",
-    testPrettyT [<] [<] (^TYPE 100) "★¹⁰⁰" "Type 100"
+    testPrettyT [<] [<] (^TYPE 0) "★" "Type",
+    testPrettyT [<] [<] (^TYPE 100) "★¹⁰⁰" "Type^100"
   ],
 
   "function types" :- [
@@ -120,8 +120,8 @@ tests = "pretty printing terms" :- [
       "1.(x : A) -> B x",
     testPrettyT [<] [<]
       (^PiY Zero "A" (^TYPE 0) (^Arr Any (^BVT 0) (^BVT 0)))
-      "0.(A : ★⁰) → ω.A → A"
-      "0.(A : Type 0) -> #.A -> A",
+      "0.(A : ★) → ω.A → A"
+      "0.(A : Type) -> #.A -> A",
     testPrettyT [<] [<]
       (^Arr Any (^Arr Any (^FT "A" 0) (^FT "A" 0)) (^FT "A" 0))
       "ω.(ω.A → A) → A"
@@ -133,8 +133,8 @@ tests = "pretty printing terms" :- [
     testPrettyT [<] [<]
       (^PiY Zero "P" (^Arr Zero (^FT "A" 0) (^TYPE 0))
         (E $ ^App (^BV 0) (^FT "a" 0)))
-      "0.(P : 0.A → ★⁰) → P a"
-      "0.(P : 0.A -> Type 0) -> P a"
+      "0.(P : 0.A → ★) → P a"
+      "0.(P : 0.A -> Type) -> P a"
   ],
 
   "pair types" :- [
@@ -193,8 +193,8 @@ tests = "pretty printing terms" :- [
   "case" :- [
     testPrettyE [<] [<]
       (^CasePair One (^F "a" 0) (SN $ ^TYPE 1) (SN $ ^TYPE 0))
-      "case1 a return ★¹ of { (_, _) ⇒ ★⁰ }"
-      "case1 a return Type 1 of { (_, _) => Type 0 }",
+      "case1 a return ★¹ of { (_, _) ⇒ ★ }"
+      "case1 a return Type^1 of { (_, _) => Type }",
     testPrettyT [<] [<]
       (^LamY "u" (E $
         ^CaseEnum One (^F "u" 0)
@@ -209,10 +209,10 @@ tests = "pretty printing terms" :- [
 
   "type-case" :- [
     testPrettyE [<] [<]
-      {label = "type-case ℕ ∷ ★⁰ return ★⁰ of { ⋯ }"}
+      {label = "type-case ℕ ∷ ★ return ★ of { ⋯ }"}
       (^TypeCase (^Ann (^NAT) (^TYPE 0)) (^TYPE 0) empty (^NAT))
-      "type-case ℕ ∷ ★⁰ return ★⁰ of { _ ⇒ ℕ }"
-      "type-case Nat :: Type 0 return Type 0 of { _ => Nat }"
+      "type-case ℕ ∷ ★ return ★ of { _ ⇒ ℕ }"
+      "type-case Nat :: Type return Type of { _ => Nat }"
   ],
 
   skipWith "(todo: print user-written redundant annotations)" $
@@ -236,6 +236,6 @@ tests = "pretty printing terms" :- [
     testPrettyE [<] [<]
       (^Ann (^Arr One (^FT "A" 0) (^FT "A" 0)) (^TYPE 7))
       "(1.A → A) ∷ ★⁷"
-      "(1.A -> A) :: Type 7"
+      "(1.A -> A) :: Type^7"
   ]
 ]

tests/Tests/Reduce.idr

@@ -14,8 +14,10 @@ import Control.Eff
 
 runWhnf : Eff Whnf a -> Either Error a
 runWhnf act = runSTErr $ do
-  runEff act [handleExcept (\e => stLeft e),
-              handleStateSTRef !(liftST $ newSTRef 0)]
+  runEff act $ with Union.(::)
+    [handleExcept (\e => stLeft e),
+     handleStateSTRef !(newSTRef' 0),
+     handleLogDiscardST !(newSTRef' 0)]
 
 parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
            {auto _ : (Eq (tm d n), Show (tm d n))}

tests/Tests/Typechecker.idr

@@ -114,11 +114,11 @@ parameters (label : String) (act : Lazy (Eff Test ()))
            {default defGlobals globals : Definitions}
   testTC : Test
   testTC = test label {e = Error', a = ()} $
-    extract $ runExcept $ runReaderAt DEFS globals act
+    runEff act [handleExcept (\e => Left e), handleReaderConst globals]
 
   testTCFail : Test
   testTCFail = testThrows label (const True) $
-    (extract $ runExcept $ runReaderAt DEFS globals act) $> "()"
+    runEff act [handleExcept (\e => Left e), handleReaderConst globals] $> "ok"
 
 
 inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> Eff Test ()

tests/TypingImpls.idr

@@ -22,10 +22,11 @@ ToInfo Error where
 export
 runEqual : Definitions -> Eff Equal a -> Either Error a
 runEqual defs act = runSTErr $ do
-  runEff act
+  runEff act $ with Union.(::)
     [handleExcept (\e => stLeft e),
      handleReaderConst defs,
-     handleStateSTRef !(liftST $ newSTRef 0)]
+     handleStateSTRef !(newSTRef' 0),
+     handleLogDiscardST !(newSTRef' 0)]
 
 export
 runTC : Definitions -> Eff TC a -> Either Error a