wip

happy new year [pack update. also idris 0.7.0]
2024-02-10 10:14:22 +01:00 · 2024-02-10 10:14:22 +01:00 · 2024-02-10 10:14:22 +01:00 · 2024-02-10 10:14:22 +01:00 · 2024-02-10 10:14:22 +01:00 · 2024-02-10 10:14:22 +01:00
39 changed files with 1329 additions and 584 deletions
--- a/exe/CompileMonad.idr
+++ b/exe/CompileMonad.idr
@ -0,0 +1,157 @@
+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 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
+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
+handleLog : IORef LevelStack -> OpenFile -> LogL x a -> IOErr Error a
+handleLog lvls f l = case f of
+  OConsole ch => handleLogIO (const $ pure ()) lvls (consoleHandle ch) l
+  OFile _ h   => handleLogIO (const $ pure ()) lvls h l
+  ONone       => handleLogDiscard l
+
+private
+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
+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
+rethrowFileC : String -> Either FileError a -> Eff Compile a
+rethrowFileC f = rethrow . mapFst (WriteError f)
+
+
+export
+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
+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
+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
+withEarlyStop : Eff CompileStop () -> Eff Compile ()
+withEarlyStop = ignore . runFailAt STOP
+
+export
+stopHere : Has (FailL STOP) fs => Eff fs ()
+stopHere = failAt STOP
+
+
+export
+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
+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
+liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
+liftScheme act = do
+  runEff [|MkPair act (getAt MAIN)|]
+    [handleStateIORef !(newIORef empty),
+     handleStateIORef !(newIORef [])]
--- a/exe/Error.idr
+++ b/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
--- a/exe/Main.idr
+++ b/exe/Main.idr
@ -1,75 +1,28 @@
 module Main

 import Quox.Syntax as Q
-import Quox.Parser
 import Quox.Definition as Q
-import Quox.Pretty
 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 CompileMonad

-import Data.IORef
-import Data.SortedSet
-import Text.Show.PrettyVal
-import Text.Show.Pretty
 import System
 import System.File
+import Data.IORef
 import Control.Eff

+%default total
+
 %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 -> Eff Pretty a -> a
-runPretty opts act =
-  runPrettyWith Outer opts.flavor (hlFor opts.hlType opts.outFile) 2 act
-
-private
-putErrLn : HasIO io => String -> io ()
-putErrLn = ignore . fPutStrLn stderr
-
-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
@ -77,158 +30,89 @@ data Error =


 private
-loadError : Loc -> FilePath -> FileError -> Error
-loadError loc file err = FromParserError $ LoadError loc file err
+Step : Type -> Type -> Type
+Step a b = OpenFile -> a -> Eff Compile b

 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
-data CompileTag = OPTS | STATE
-
-private
-Compile : List (Type -> Type)
-Compile =
-  [Except Error,
-   ReaderL STATE State, ReaderL OPTS Options,
-   LoadFile, IO]
-
-private
-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
-FlexDoc : Type
-FlexDoc = {opts : LayoutOpts} -> Doc opts
-
-
-private
-outputStr : Lazy String -> Eff Compile ()
-outputStr str =
-  case !(asksAt OPTS outFile) of
-    NoOut   => pure ()
-    Console => putStr str
-    File f  => do
-      res <- withFile f WriteTruncate pure $ \h => fPutStr h str
-      rethrow $ mapFst (WriteError f) res
-
-private
-outputDocs : (opts : Options) ->
-             ({opts : LayoutOpts} -> List (Doc opts)) -> Eff Compile ()
-outputDocs opts doc =
-  outputStr $ concat $ map (render (Opts opts.width)) doc
-
-private
-outputDocStopIf : Phase ->
-                  ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
-                  Eff CompileStop ()
-outputDocStopIf p docs = do
+step : {default CErr console : ConsoleChannel} ->
+       Phase -> OutFile -> Step a b -> a -> Eff CompileStop b
+step phase file act x = do
  opts <- askAt OPTS
-  when (opts.until == Just p) $ Prelude.do
-    lift $ outputDocs !(askAt OPTS) (runPretty opts docs)
-    stopHere
-
-private
-liftFromParser : Eff FromParserIO a -> Eff CompileStop 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 CompileStop a
-liftErase defs act =
-  runEff act
-    [handleExcept $ \err => throw $ EraseError err,
-     handleStateIORef !(asksAt STATE suf)]
-
-private
-liftScheme : Eff Scheme a -> Eff CompileStop (a, List Id)
-liftScheme act = do
-  runEff [|MkPair act (getAt MAIN)|]
-    [handleStateIORef !(newIORef empty),
-     handleStateIORef !(newIORef [])]
+  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
-oneMain : Has (Except Error) fs => List Id -> Eff fs Id
-oneMain []    = throw NoMain
-oneMain [x]   = pure x
-oneMain mains = throw $ MultipleMains mains
-
-
-private
-processFile : String -> Eff Compile ()
-processFile file = withEarlyStop $ do
+private covering
+parse : Step String PFile
+parse h file = 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
-  opts <- askAt OPTS
-  main <- oneMain mains
-  lift $ outputDocs opts $ intersperse empty $ runPretty opts $ do
-    res    <- traverse prettySexp scheme
+    | Nothing => pure []
+  outputStr h $ show ast
+  pure ast
+
+private covering
+check : Step PFile (List Q.NDefinition)
+check h decls =
+  map concat $ for decls $ \decl => do
+    defs <- liftFromParser $ fromPTopLevel decl
+    outputDocs h $ traverse (\(x, d) => prettyDef x d) defs
+    pure defs
+
+private covering
+erase : Step (List Q.NDefinition) (List U.NDefinition)
+erase h defList =
+  for defList $ \(x, def) => do
+    def <- liftErase defs $ eraseDef defs x def
+    outputDoc h $ U.prettyDef x def
+    pure (x, def)
+where defs = SortedMap.fromList defList
+
+private covering
+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 $ case msexp of
+      Just s  => prettySexp s
+      Nothing => pure $ hsep [";;", prettyName x, "erased"]
+    pure (msexp, mains)
+  pure $ bimap catMaybes concat $ unzip sexps'
+
+private covering
+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
    pure $ text Scheme.prelude :: res ++ [runner]

-export
+private covering
+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}
+
+
+export covering
 main : IO ()
 main = do
  (_, opts, files) <- options
  case !(runCompile opts !newState $ traverse_ processFile files) of
    Right () => pure ()
-    Left  e  => die (Opts opts.width) $
-                runPretty ({outFile := Console} opts) $
-                prettyError e
+    Left  e  => dieError opts e


 -----------------------------------
@ -244,6 +128,13 @@ text _ =
   #" /_/"#,
   ""]

+--   ["",
+--    #" __ _ _  _ _____ __"#,
+--    #"/ _` | || / _ \ \ /"#,
+--    #"\__, |\_,_\___/_\_\"#,
+--    #"   |_|"#,
+--    ""]
+
 private
 qtuwu : PrettyOpts -> List String
 qtuwu opts =
--- a/exe/Options.idr
+++ b/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
@ -13,35 +16,44 @@ import Derive.Prelude
 public export
 data OutFile = File String | Console | NoOut
 %name OutFile f
-%runElab derive "OutFile" [Eq, Ord, Show]
+%runElab derive "OutFile" [Eq, Show]

 public export
-data Phase = Parse | Check | Erase | Scheme
+data Phase = Parse | Check | Erase | Scheme | End
 %name Phase p
-%runElab derive "Phase" [Eq, Ord, Show]
+%runElab derive "Phase" [Eq, Show]

-||| a list of all `Phase`s
+||| a list of all intermediate `Phase`s (excluding `End`)
 public export %inline
 allPhases : List Phase
 allPhases = %runElab do
-  -- as a script so it stays up to date
  cs <- getCons $ fst !(lookupName "Phase")
-  traverse (check . var) cs
+  traverse (check . var) $ fromMaybe [] $ init' cs

-||| "guess" is Term for a terminal and NoHL for a file
+||| `Guess` is `Term` for a terminal and `NoHL` for a file
 public export
 data HLType = Guess | NoHL | Term | Html
-%runElab derive "HLType" [Eq, Ord, Show]
+%runElab derive "HLType" [Eq, Show]
+
+public export
+record Dump where
+  constructor MkDump
+  parse, check, erase, scheme : OutFile
+%name Dump dump
+%runElab derive "Dump" [Show]

 public export
 record Options where
  constructor MkOpts
-  hlType  : HLType
-  outFile : OutFile
-  until   : Maybe Phase
-  flavor  : Pretty.Flavor
-  width   : Nat
-  include : List String
+  include   : List String
+  dump      : Dump
+  outFile   : OutFile
+  until     : Maybe Phase
+  hlType    : HLType
+  flavor    : Pretty.Flavor
+  width     : Nat
+  logLevels : LogLevels
+  logFile   : OutFile
 %name Options opts
 %runElab derive "Options" [Show]

@ -54,12 +66,15 @@ defaultWidth = do
 export
 defaultOpts : IO Options
 defaultOpts = pure $ MkOpts {
-  hlType  = Guess,
-  outFile = Console,
-  until   = Nothing,
-  flavor  = Unicode,
-  width   = !defaultWidth,
-  include = ["."]
+  include   = ["."],
+  dump      = MkDump NoOut NoOut NoOut NoOut,
+  outFile   = Console,
+  until     = Nothing,
+  hlType    = Guess,
+  flavor    = Unicode,
+  width     = !defaultWidth,
+  logLevels = defaultLogLevels,
+  logFile   = Console
 }

 private
@ -70,19 +85,31 @@ data OptAction = ShowHelp HelpType | Err String | Ok (Options -> Options)
 %name OptAction act

 private
-toOutFile : String -> OptAction
-toOutFile ""  = Ok {outFile := NoOut}
-toOutFile "-" = Ok {outFile := Console}
-toOutFile f   = Ok {outFile := File f}
+toOutFile : String -> OutFile
+toOutFile ""  = NoOut
+toOutFile "-" = Console
+toOutFile f   = File f

 private
 toPhase : String -> OptAction
 toPhase str =
  let lstr = toLower str in
  case find (\p => toLower (show p) == lstr) allPhases of
-    Just p  => Ok {until := Just p}
+    Just p  => Ok $ setPhase p
    Nothing => Err "unknown phase name \{show str}\nphases: \{phaseNames}"
-where phaseNames = joinBy ", " $ map (toLower . show) allPhases
+where
+  phaseNames = joinBy ", " $ map (toLower . show) allPhases
+
+  defConsole : OutFile -> OutFile
+  defConsole NoOut = Console
+  defConsole f     = f
+
+  setPhase : Phase -> Options -> Options
+  setPhase Parse  = {until := Just Parse,  dump.parse  $= defConsole}
+  setPhase Check  = {until := Just Check,  dump.check  $= defConsole}
+  setPhase Erase  = {until := Just Erase,  dump.erase  $= defConsole}
+  setPhase Scheme = {until := Just Scheme, dump.scheme $= defConsole}
+  setPhase End    = id

 private
 toWidth : String -> OptAction
@ -96,17 +123,69 @@ toHLType str = case toLower str of
  "none" => Ok {hlType := NoHL}
  "term" => Ok {hlType := Term}
  "html" => Ok {hlType := Html}
-  _      => Err "unknown highlighting type \{str}\ntypes: term, html, none"
+  _      => 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
+private
+dirListFlag : String -> List String -> List String
+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)
 commonOptDescrs' = [
-  MkOpt ['i'] ["include"] (ReqArg (\i => Ok {include $= (i ::)}) "<dir>")
-    "add a directory to look for source files",
-  MkOpt ['o'] ["output"] (ReqArg toOutFile "<file>")
+  MkOpt ['i'] ["include"]
+    (ReqArg (\is => Ok {include $= dirListFlag is}) "<dir>:<dir>...")
+    "add directories to look for source files",
+  MkOpt ['o'] ["output"] (ReqArg (\s => Ok {outFile := toOutFile s}) "<file>")
    "output file (\"-\" for stdout, \"\" for no output)",
  MkOpt ['P'] ["phase"] (ReqArg toPhase "<phase>")
-    "phase to stop at (by default go as far as exists)"
+    "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
@ -119,7 +198,20 @@ extraOptDescrs = [
  MkOpt [] ["width"] (ReqArg toWidth "<width>")
    "max output width (defaults to terminal width)",
  MkOpt [] ["color", "colour"] (ReqArg toHLType "<type>")
-    "select highlighting type"
+    "select highlighting type",
+
+  MkOpt [] ["dump-parse"]
+    (ReqArg (\s => Ok {dump.parse := toOutFile s}) "<file>")
+    "dump AST",
+  MkOpt [] ["dump-check"]
+    (ReqArg (\s => Ok {dump.check := toOutFile s}) "<file>")
+    "dump typechecker output",
+  MkOpt [] ["dump-erase"]
+    (ReqArg (\s => Ok {dump.erase := toOutFile s}) "<file>")
+    "dump erasure output",
+  MkOpt [] ["dump-scheme"]
+    (ReqArg (\s => Ok {dump.scheme := toOutFile s}) "<file>")
+    "dump scheme output (without prelude)"
 ]

 private
@ -152,10 +244,6 @@ applyAction opts (ShowHelp All)    = usage allOptDescrs
 applyAction opts (Err err)         = die err
 applyAction opts (Ok f)            = pure $ f opts

-private
-finalise : Options -> Options
-finalise = {include $= reverse}
-
 export
 options : IO (String, Options, List String)
 options = do
@ -167,4 +255,4 @@ options = do
  unless (null res.unrecognized) $
    die "unrecognised options: \{joinBy ", " res.unrecognized}"
  opts <- foldlM applyAction !defaultOpts res.options
-  pure (app, finalise opts, res.nonOptions)
+  pure (app, opts, res.nonOptions)
--- a/exe/Output.idr
+++ b/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
--- a/lib/Control/Monad/ST/Extra.idr
+++ b/lib/Control/Monad/ST/Extra.idr
@ -62,3 +62,17 @@ 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
+  readSTRef' : STRef s a -> m s a
+  readSTRef' r = liftST $ ST.readSTRef r
+
+  export %inline
+  writeSTRef' : STRef s a -> a -> m s ()
+  writeSTRef' r x = liftST $ ST.writeSTRef r x
+
+  export %inline
+  modifySTRef' : STRef s a -> (a -> a) -> m s ()
+  modifySTRef' r f = liftST $ ST.modifySTRef r f
--- a/lib/Quox/Definition.idr
+++ b/lib/Quox/Definition.idr
@ -89,12 +89,16 @@ isZero g = g.qty == GZero


 public export
-data DefEnvTag = DEFS
+NDefinition : Type
+NDefinition = (Name, Definition)

 public export
 Definitions : Type
 Definitions = SortedMap Name Definition

+public export
+data DefEnvTag = DEFS
+
 public export
 DefsReader : Type -> Type
 DefsReader = ReaderL DEFS Definitions
--- a/lib/Quox/EffExtra.idr
+++ b/lib/Quox/EffExtra.idr
@ -97,6 +97,10 @@ export
 handleReaderConst : Applicative m => r -> ReaderL lbl r a -> m a
 handleReaderConst x Ask = pure x

+export
+handleWriterST : HasST m => STRef s (SnocList w) -> WriterL lbl w a -> m s a
+handleWriterST ref (Tell w) = liftST $ modifySTRef ref (:< w)
+

 public export
 record IOErr e a where
--- a/lib/Quox/Equal.idr
+++ b/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
+  say "equal" logLevel ty.loc "isEmpty"
+  say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
+  say "equal" 95 ty.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
+  say "equal" logLevel ty.loc $
+    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
+  say "equal" logLevel ty.loc "isSubSing"
+  say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
+  say "equal" 95 ty.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
+  say "equal" logLevel ty.loc $
+    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 =>
-              (loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
-              Eff fs (So (isTyConE t))
-ensureTyCon loc ctx t = case nchoose $ isTyConE t of
-  Left  y => pure y
-  Right n => throw $ NotType loc (toTyContext ctx) (t // shift0 ctx.dimLen)
+ensureTyCon, ensureTyConNoLog :
+  (Has Log fs, Has ErrorEff fs) =>
+  (loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
+  Eff fs (So (isTyConE t))
+ensureTyConNoLog loc ctx ty = do
+  case nchoose $ isTyConE ty of
+    Left  y => pure y
+    Right n => throw $ NotType loc (toTyContext ctx) (ty // shift0 ctx.dimLen)
+
+ensureTyCon loc ctx ty = do
+  say "equal" 60 ty.loc "ensureTyCon"
+  say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
+  say "equal" 60 ty.loc $
+    hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
+  ensureTyConNoLog loc ctx ty


 namespace Term
@ -751,7 +795,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
@ -759,20 +807,70 @@ namespace Term
      tty <- ensureTyCon ty.loc ctx ty'
      compare0' defs ctx sg ty' s' t'

+  compare0 defs ctx sg ty s t = do
+    say "equal" 30 s.loc "Term.compare0"
+    say "equal" 30 s.loc $ hsep ["mode =", pshow !mode]
+    say "equal" 95 s.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
+    say "equal" 95 s.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
+    say "equal" 31 s.loc $
+      hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]
+    say "equal" 30 s.loc $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s]
+    say "equal" 30 s.loc $ 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
+    say "equal" 30 e.loc "Elim.compare0"
+    say "equal" 30 e.loc $ hsep ["mode =", pshow !mode]
+    say "equal" 95 e.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
+    say "equal" 95 e.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
+    say "equal" 30 e.loc $ hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e]
+    say "equal" 30 e.loc $ hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f]
+    ty <- compare0NoLog defs ctx sg e f
+    say "equal" 31 e.loc $
+      hsep ["ty ⇝", 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
+  say "equal" 30 s.loc "compareType"
+  say "equal" 30 s.loc $ hsep ["mode =", pshow !mode]
+  say "equal" 95 s.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx]
+  say "equal" 30 s.loc $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s]
+  say "equal" 30 s.loc $ 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)
@ -781,9 +879,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

@ -793,31 +893,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
--- a/lib/Quox/FreeVars.idr
+++ b/lib/Quox/FreeVars.idr
@ -229,27 +229,27 @@ HasFreeVars (Elim d) where


 private
-expandDShift : {d1 : Nat} -> Shift d1 d2 -> Context' (Dim d2) d1
-expandDShift by = tabulateLT d1 (\i => BV i noLoc // by)
+expandDShift : {d1 : Nat} -> Shift d1 d2 -> Loc -> Context' (Dim d2) d1
+expandDShift by loc = tabulateLT d1 (\i => BV i loc // by)

 private
-expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Context' (Dim d2) d1
-expandDSubst (Shift by) = expandDShift by
-expandDSubst (t ::: th) = expandDSubst th :< t
+expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Loc -> Context' (Dim d2) d1
+expandDSubst (Shift by) loc = expandDShift by loc
+expandDSubst (t ::: th) loc = expandDSubst th loc :< t


 private
-fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars tm =>
+fdvSubst' : {d1, d2, n : Nat} -> (Located2 tm, HasFreeDVars tm) =>
            tm d1 n -> DSubst d1 d2 -> FreeVars d2
 fdvSubst' t th =
-  fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th)
+  fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th t.loc)
 where
  maybeOnly : {d : Nat} -> Bool -> Dim d -> FreeVars d
  maybeOnly True (B i _) = only i
  maybeOnly _    _       = none

 private
-fdvSubst : {d, n : Nat} -> HasFreeDVars tm =>
+fdvSubst : {d, n : Nat} -> (Located2 tm, HasFreeDVars tm) =>
           WithSubst (\d => tm d n) Dim d -> FreeVars d
 fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th

--- a/lib/Quox/Loc.idr
+++ b/lib/Quox/Loc.idr
@ -118,6 +118,11 @@ export %inline
 or : Loc -> Loc -> Loc
 or (L l1) (L l2) = L $ l1 `or_` l2

+export %inline
+extendOr : Loc -> Loc -> Loc
+extendOr l1 l2 = (l1 `extendL` l2) `or` l2
+
+

 public export
 interface Located a where (.loc) : a -> Loc
@ -126,9 +131,22 @@ public export
 0 Located1 : (a -> Type) -> Type
 Located1 f = forall x. Located (f x)

+public export
+0 Located2 : (a -> b -> Type) -> Type
+Located2 f = forall x, y. Located (f x y)
+
 public export
 interface Located a => Relocatable a where setLoc : Loc -> a -> a

 public export
 0 Relocatable1 : (a -> Type) -> Type
 Relocatable1 f = forall x. Relocatable (f x)
+
+public export
+0 Relocatable2 : (a -> b -> Type) -> Type
+Relocatable2 f = forall x, y. Relocatable (f x y)
+
+
+export
+locs : Located a => Foldable t => t a -> Loc
+locs = foldl (\loc, y => loc `extendOr` y.loc) noLoc
--- a/lib/Quox/Log.idr
+++ b/lib/Quox/Log.idr
@ -0,0 +1,219 @@
+module Quox.Log
+
+import Quox.Loc
+import Quox.Pretty
+
+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
+maxLogLevel : Nat
+maxLogLevel = 100
+
+public export
+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
+
+
+public export
+LogLevel : Type
+LogLevel = Subset Nat IsLogLevel
+
+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
+
+
+public export
+LevelMap : Type
+LevelMap = List (LogCategory, LogLevel)
+-- i tried SortedMap first, but it is too much overhead for LevelMaps
+
+public export
+record LogLevels where
+  constructor MkLogLevels
+  defLevel : LogLevel
+  levels   : LevelMap
+%name LogLevels lvls
+%runElab derive "LogLevels" [Eq, Show]
+
+public export
+LevelStack : Type
+LevelStack = List1 LogLevels
+
+export %inline
+defaultLogLevels : LogLevels
+defaultLogLevels = MkLogLevels (Element 0 Oh) []
+
+export %inline
+initStack : LevelStack
+initStack = singleton defaultLogLevels
+
+||| right biased for the default and for overlapping elements
+public export %inline
+mergeLevels : LogLevels -> LogLevels -> LogLevels
+mergeLevels (MkLogLevels _ map1) (MkLogLevels def map2) =
+  MkLogLevels def $ map1 ++ map2
+
+export %inline
+getLevel : LogCategory -> LogLevels -> LogLevel
+getLevel cat lvls = fromMaybe lvls.defLevel $ lookup cat lvls.levels
+
+
+public export
+LogDoc : Type
+LogDoc = Doc (Opts {lineLength = 80})
+
+
+public export
+data PushArg = SetDefault LogLevel | SetCats LevelMap
+%name PushArg push
+
+export %inline
+mergePush : PushArg -> LogLevels -> LogLevels
+mergePush (SetDefault def) = {defLevel := def}
+mergePush (SetCats    map) = {levels   $= (map ++)}
+
+
+public export
+data LogL : (lbl : tag) -> Type -> Type where
+  Say  : (cat : LogCategory) -> (lvl : LogLevel) ->
+         (loc : Loc) -> (msg : Lazy LogDoc) -> LogL lbl ()
+  Push : (push : PushArg) -> LogL lbl ()
+  Pop  : LogL lbl ()
+  CurLevels : LogL lbl LogLevels
+
+public export
+Log : Type -> Type
+Log = LogL ()
+
+parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs}
+  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 {catOk, lvlOk} =
+    send $ Say {lbl} (Element cat catOk) (Element lvl lvlOk) loc msg
+
+  public export %inline
+  pushAt : PushArg -> Eff fs ()
+  pushAt lvls = send $ Push {lbl} lvls
+
+  public export %inline
+  popAt : Eff fs ()
+  popAt = send $ Pop {lbl}
+
+  public export %inline
+  curLevelsAt : Eff fs LogLevels
+  curLevelsAt = send $ CurLevels {lbl}
+
+parameters {auto _ : Has Log fs}
+  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 : PushArg -> Eff fs ()
+  push = pushAt ()
+
+  public export %inline
+  pop : Eff fs ()
+  pop = popAt ()
+
+  public export %inline
+  curLevels : Eff fs LogLevels
+  curLevels = curLevelsAt ()
+
+
+export
+doPush : PushArg -> LevelStack -> LevelStack
+doPush push list = mergePush push (head list) `cons` list
+
+export
+doPop : List1 a -> List1 a
+doPop list = fromMaybe list $ fromList list.tail
+
+export
+doSay : Applicative m =>
+        LevelStack -> (LogDoc -> m ()) ->
+        LogCategory -> LogLevel -> Loc -> Lazy LogDoc -> m ()
+doSay (map ::: _) act cat lvl loc msg =
+  when (lvl <= getLevel cat map) $ do
+    let loc = runPretty $ prettyLoc loc
+    act $ hcat [loc, text cat.fst, "@", pshow lvl.fst, ":"] <++> msg
+
+export
+handleLogIO : HasIO m => (FileError -> m ()) ->
+              IORef LevelStack -> File -> LogL tag a -> m a
+handleLogIO th lvls h = \case
+  Push push           => modifyIORef lvls $ doPush push
+  Pop                 => modifyIORef lvls doPop
+  Say cat lvl loc msg => doSay !(readIORef lvls) printMsg cat lvl loc msg
+  CurLevels           => head <$> readIORef lvls
+where printMsg : LogDoc -> m ()
+      printMsg msg = fPutStr h (render _ msg) >>= either th pure
+
+export
+handleLogST : (HasST m, Monad (m s)) =>
+              STRef s (SnocList LogDoc) ->
+              STRef s LevelStack ->
+              LogL tag a -> m s a
+handleLogST docs lvls = \case
+  Push push           => modifySTRef' lvls $ doPush push
+  Pop                 => modifySTRef' lvls doPop
+  Say cat lvl loc msg => doSay !(readSTRef' lvls) printMsg cat lvl loc msg
+  CurLevels           => head <$> readSTRef' lvls
+where printMsg : LogDoc -> m s ()
+      printMsg msg = modifySTRef' docs (:< msg)
+
+export
+handleLogDiscard : Applicative m => LogL tag a -> m a
+handleLogDiscard = \case
+  Say  {}   => pure ()
+  Push {}   => pure ()
+  Pop       => pure ()
+  CurLevels => pure defaultLogLevels
--- a/lib/Quox/NatExtra.idr
+++ b/lib/Quox/NatExtra.idr
@ -82,7 +82,7 @@ namespace Int

  export %inline
  fromHex : String -> Maybe Int
-  fromHex = fromHex' 0
+  fromHex str = do guard $ str /= ""; fromHex' 0 str

 namespace Nat
  export
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@ -27,51 +27,49 @@ import Data.IORef
 %default total


-public export
-NDefinition : Type
-NDefinition = (Name, Definition)
-
-
 public export
 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
+                 NameSuf -> Definitions -> LevelStack ->
+                 Eff FromParserPure a -> Either Error (PureParserResult a)
+fromParserPure suf defs lvls act = runSTErr $ do
  suf  <- liftST $ newSTRef suf
  defs <- liftST $ newSTRef defs
+  log  <- liftST $ newSTRef [<]
+  lvls <- liftST $ newSTRef lvls
  res  <- runEff act $ with Union.(::)
    [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 suf,
+     handleLogST log lvls]
+  pure $ MkPureParserResult {
+    val       = res,
+    suf       = !(liftST $ readSTRef suf),
+    defs      = !(liftST $ readSTRef defs),
+    log       = !(liftST $ readSTRef log),
+    logLevels = !(liftST $ readSTRef lvls)
+  }


 parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
@ -307,7 +305,7 @@ mutual
                    Eff FromParserPure (DScopeTermN s d n)
  fromPTermDScope ds ns xs t =
    if all isUnused xs then
-      SN <$> fromPTermWith ds ns t
+      SN {f = \d => Term d n} <$> fromPTermWith ds ns t
    else
      DST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith (ds ++ xs) ns t

@ -333,6 +331,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
@ -375,8 +374,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

--- a/lib/Quox/Scoped.idr
+++ b/lib/Quox/Scoped.idr
@ -38,3 +38,22 @@ export %inline
 export %inline %hint
 ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
 ShowScoped = deriveShow
+
+
+||| scope which ignores all its binders
+public export %inline
+SN : Located1 f => {s : Nat} -> f n -> Scoped s f n
+SN body = S (replicate s $ BN Unused body.loc) $ N body
+
+||| scope which uses its binders
+public export %inline
+SY : BContext s -> f (s + n) -> Scoped s f n
+SY ns = S ns . Y
+
+public export %inline
+name : Scoped 1 f n -> BindName
+name (S [< x] _) = x
+
+public export %inline
+(.name) : Scoped 1 f n -> BindName
+s.name = name s
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/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
@ -71,13 +76,13 @@ toMaybe (Just x) = Just x


 export
-fromGround' : Context' DimConst d -> DimEq' d
-fromGround' [<]        = [<]
-fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc)
+fromGround' : BContext d -> Context' DimConst d -> DimEq' d
+fromGround' [<]       [<]        = [<]
+fromGround' (xs :< x) (ctx :< e) = fromGround' xs ctx :< Just (K e x.loc)

 export
-fromGround : Context' DimConst d -> DimEq d
-fromGround = C . fromGround'
+fromGround : BContext d -> Context' DimConst d -> DimEq d
+fromGround = C .: fromGround'


 public export %inline
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@ -96,18 +96,18 @@ map f (t ::: th) = f t ::: map f th


 public export %inline
-push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
-push th = fromVar VZ ::: (th . shift 1)
+push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to)
+push loc th = fromVarLoc VZ loc ::: (th . shift 1)

 -- [fixme] a better way to do this?
 public export
-pushN : CanSubstSelf f => (s : Nat) ->
+pushN : CanSubstSelf f => (s : Nat) -> Loc ->
        Subst f from to -> Subst f (s + from) (s + to)
-pushN 0     th = th
-pushN (S s) th =
+pushN 0     _   th = th
+pushN (S s) loc th =
  rewrite plusSuccRightSucc s from in
  rewrite plusSuccRightSucc s to in
-  pushN s $ fromVar VZ ::: (th . shift 1)
+  pushN s loc $ fromVarLoc VZ loc ::: (th . shift 1)

 public export
 drop1 : Subst f (S from) to -> Subst f from to
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@ -236,117 +236,6 @@ mutual
  ShowElim : Show (Elim d n)
  ShowElim = assert_total {a = Show (Elim d n)} deriveShow

-||| scope which ignores all its binders
-public export %inline
-SN : {s : Nat} -> f n -> Scoped s f n
-SN = S (replicate s $ BN Unused noLoc) . N
-
-||| scope which uses its binders
-public export %inline
-SY : BContext s -> f (s + n) -> Scoped s f n
-SY ns = S ns . Y
-
-public export %inline
-name : Scoped 1 f n -> BindName
-name (S [< x] _) = x
-
-public export %inline
-(.name) : Scoped 1 f n -> BindName
-s.name = name s
-
-||| more convenient Pi
-public export %inline
-PiY : (qty : Qty) -> (x : BindName) ->
-      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
-PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
-
-||| more convenient Lam
-public export %inline
-LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
-LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
-
-public export %inline
-LamN : (body : Term d n) -> (loc : Loc) -> Term d n
-LamN {body, loc} = Lam {body = SN body, loc}
-
-||| non dependent function type
-public export %inline
-Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
-Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
-
-||| more convenient Sig
-public export %inline
-SigY : (x : BindName) -> (fst : Term d n) ->
-       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
-SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
-
-||| non dependent pair type
-public export %inline
-And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
-And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
-
-||| more convenient Eq
-public export %inline
-EqY : (i : BindName) -> (ty : Term (S d) n) ->
-      (l, r : Term d n) -> (loc : Loc) -> Term d n
-EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
-
-||| more convenient DLam
-public export %inline
-DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
-DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
-
-public export %inline
-DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
-DLamN {body, loc} = DLam {body = SN body, loc}
-
-||| non dependent equality type
-public export %inline
-Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
-Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
-
-||| same as `F` but as a term
-public export %inline
-FT : Name -> Universe -> Loc -> Term d n
-FT x u loc = E $ F x u loc
-
-||| same as `B` but as a term
-public export %inline
-BT : Var n -> (loc : Loc) -> Term d n
-BT i loc = E $ B i loc
-
-||| abbreviation for a bound variable like `BV 4` instead of
-||| `B (VS (VS (VS (VS VZ))))`
-public export %inline
-BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
-BV i loc = B (V i) loc
-
-||| same as `BV` but as a term
-public export %inline
-BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
-BVT i loc = E $ BV i loc
-
-public export %inline
-Zero : Loc -> Term d n
-Zero = Nat 0
-
-public export %inline
-enum : List TagVal -> Loc -> Term d n
-enum ts loc = Enum (SortedSet.fromList ts) loc
-
-public export %inline
-typeCase : Elim d n -> Term d n ->
-           List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
-typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
-
-public export %inline
-typeCase1Y : Elim d n -> Term d n ->
-             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
-             (loc : Loc) ->
-             {default (NAT loc) def : Term d n} ->
-             Elim d n
-typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
-

 export
 Located (Elim d n) where
@ -463,3 +352,97 @@ Relocatable1 f => Relocatable (ScopedBody s f n) where
 export
 Relocatable1 f => Relocatable (Scoped s f n) where
  setLoc loc (S names body) = S (setLoc loc <$> names) (setLoc loc body)
+
+
+||| more convenient Pi
+public export %inline
+PiY : (qty : Qty) -> (x : BindName) ->
+      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
+PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
+
+||| more convenient Lam
+public export %inline
+LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
+LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
+
+public export %inline
+LamN : (body : Term d n) -> (loc : Loc) -> Term d n
+LamN {body, loc} = Lam {body = SN body, loc}
+
+||| non dependent function type
+public export %inline
+Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
+Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
+
+||| more convenient Sig
+public export %inline
+SigY : (x : BindName) -> (fst : Term d n) ->
+       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
+SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
+
+||| non dependent pair type
+public export %inline
+And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
+And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
+
+||| more convenient Eq
+public export %inline
+EqY : (i : BindName) -> (ty : Term (S d) n) ->
+      (l, r : Term d n) -> (loc : Loc) -> Term d n
+EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
+
+||| more convenient DLam
+public export %inline
+DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
+DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
+
+public export %inline
+DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
+DLamN {body, loc} = DLam {body = SN body, loc}
+
+||| non dependent equality type
+public export %inline
+Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
+Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
+
+||| same as `F` but as a term
+public export %inline
+FT : Name -> Universe -> Loc -> Term d n
+FT x u loc = E $ F x u loc
+
+||| same as `B` but as a term
+public export %inline
+BT : Var n -> (loc : Loc) -> Term d n
+BT i loc = E $ B i loc
+
+||| abbreviation for a bound variable like `BV 4` instead of
+||| `B (VS (VS (VS (VS VZ))))`
+public export %inline
+BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
+BV i loc = B (V i) loc
+
+||| same as `BV` but as a term
+public export %inline
+BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
+BVT i loc = E $ BV i loc
+
+public export %inline
+Zero : Loc -> Term d n
+Zero = Nat 0
+
+public export %inline
+enum : List TagVal -> Loc -> Term d n
+enum ts loc = Enum (SortedSet.fromList ts) loc
+
+public export %inline
+typeCase : Elim d n -> Term d n ->
+           List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
+typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
+
+public export %inline
+typeCase1Y : Elim d n -> Term d n ->
+             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
+             (loc : Loc) ->
+             {default (NAT loc) def : Term d n} ->
+             Elim d n
+typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@ -608,7 +608,7 @@ prettyElim dnames tnames (Coe ty p q val _) =

 prettyElim dnames tnames e@(Comp ty p q val r zero one _) =
  parensIfM App =<< do
-    ty   <- prettyTypeLine dnames tnames $ assert_smaller e $ SN ty
+    ty   <- assert_total $ prettyTypeLine dnames tnames $ SN ty
    pq   <- sep <$> sequence [prettyDArg dnames p, prettyDArg dnames q]
    val  <- prettyTArg dnames tnames val
    r    <- prettyDArg dnames r
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@ -56,12 +56,12 @@ namespace DSubst.DScopeTermN
  (//) : {s : Nat} ->
         DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
         DScopeTermN s d2 n
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th
  S ns (N body) // th = S ns $ N $ body // th


 export %inline FromVar (Elim d) where fromVarLoc = B
-export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
+export %inline FromVar (Term d) where fromVarLoc = E .: fromVarLoc


 ||| does the minimal reasonable work:
@ -104,7 +104,7 @@ namespace ScopeTermN
  (//) : {s : Nat} ->
         ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
         ScopeTermN s d n2
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th
  S ns (N body) // th = S ns $ N $ body // th

 namespace DScopeTermN
@ -189,11 +189,11 @@ dsub1 t p = dsubN t [< p]


 public export %inline
-(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+(.zero) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n
 body.zero = dsub1 body $ K Zero loc

 public export %inline
-(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+(.one) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n
 body.one = dsub1 body $ K One loc


--- a/lib/Quox/Typechecker.idr
+++ b/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,23 @@ 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
+    say "check" 10 subj.loc $ text fun
+    say "check" 95 subj.loc $ hsep ["ctx =",  runPretty $ prettyTyContext ctx]
+    say "check" 95 subj.loc $ hsep ["sg =",   runPretty $ prettyQty sg.qty]
+    say "check" 10 subj.loc $ hsep ["subj =", runPretty $ prettyTermTC ctx subj]
+    let Just ty = ty | Nothing => pure ()
+    say "check" 10 subj.loc $ hsep ["ty =", runPretty $ prettyTermTC ctx ty]
+
 mutual
  ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
  |||
@ -53,7 +71,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 = do
+    checkLogs "check" ctx sg subj (Just ty)
+    ifConsistentElse ctx.dctx
+      (checkC ctx sg subj ty)
+      (say "check" 20 subj.loc "check: 0=1")

  ||| "Ψ | Γ ⊢₀ s ⇐ A"
  |||
@ -84,7 +106,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
+    checkLogs "checkType" ctx SZero subj univ
+    ignore $ ifConsistentElse ctx.dctx
+      (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 +134,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
+    checkLogs "infer" ctx sg (E subj) Nothing
+    ifConsistentElse ctx.dctx
+      (inferC ctx sg subj)
+      (say "check" 20 subj.loc "infer: 0=1")

  ||| `infer`, assuming the dimension context is consistent
  export covering %inline
@ -304,7 +335,7 @@ mutual
    infres <- inferC ctx SZero e
    -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
    case u of
-      Just u  => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
+      Just u  => lift $ subtype e.loc ctx infres.type (TYPE u e.loc)
      Nothing => ignore $ expectTYPE !(askAt DEFS) ctx SZero e.loc infres.type
    -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀

--- a/lib/Quox/Typing.idr
+++ b/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
@ -46,16 +47,15 @@ lookupFree x loc defs = maybe (throw $ NotInScope loc x) pure $ lookup x defs
 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
+  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
  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 noLoc) $ 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,103 +65,121 @@ 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) ->
+    expect : String -> ExpectErrorConstructor ->
             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 what err pat rhs = Prelude.do
+      match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
+      pure $ \term => do
+        say "check" 30 term.loc $ hsep ["expecting:", text what]
+        res <- whnf term
+        maybe (throw $ err loc ctx.names term) pure $ match $ fst res

    export covering %inline
    expectTYPE : Term d n -> Eff fs Universe
-    expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
+    expectTYPE = expect "universe" ExpectedTYPE `(TYPE {l, _}) `(l)

    export covering %inline
    expectPi : Term d n -> Eff fs (Qty, Term d n, ScopeTerm d n)
-    expectPi = expect ExpectedPi `(Pi {qty, arg, res, _}) `((qty, arg, res))
+    expectPi = expect "function type" ExpectedPi
+      `(Pi {qty, arg, res, _}) `((qty, arg, res))

    export covering %inline
    expectSig : Term d n -> Eff fs (Term d n, ScopeTerm d n)
-    expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
+    expectSig = expect "pair type" ExpectedSig
+      `(Sig {fst, snd, _}) `((fst, snd))

    export covering %inline
    expectEnum : Term d n -> Eff fs (SortedSet TagVal)
-    expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
+    expectEnum = expect "enum type" ExpectedEnum
+      `(Enum {cases, _}) `(cases)

    export covering %inline
    expectEq : Term d n -> Eff fs (DScopeTerm d n, Term d n, Term d n)
-    expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
+    expectEq = expect "equality type" ExpectedEq
+      `(Eq {ty, l, r, _}) `((ty, l, r))

    export covering %inline
    expectNAT : Term d n -> Eff fs ()
-    expectNAT = expect ExpectedNAT `(NAT {}) `(())
+    expectNAT = expect "Nat" ExpectedNAT `(NAT {}) `(())

    export covering %inline
    expectSTRING : Term d n -> Eff fs ()
-    expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
+    expectSTRING = expect "String" ExpectedSTRING `(STRING {}) `(())

    export covering %inline
    expectBOX : Term d n -> Eff fs (Qty, Term d n)
-    expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
+    expectBOX = expect "box type" ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))


  namespace EqContext
   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) ->
+    expect : String -> ExpectErrorConstructor ->
             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 what err pat rhs = do
+      match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
+      pure $ \term => do
+        say "equal" 30 term.loc $ hsep ["expecting:", text what]
+        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
-    expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
+    expectTYPE = expect "universe" ExpectedTYPE `(TYPE {l, _}) `(l)

    export covering %inline
    expectPi : Term 0 n -> Eff fs (Qty, Term 0 n, ScopeTerm 0 n)
-    expectPi = expect ExpectedPi `(Pi {qty, arg, res, _}) `((qty, arg, res))
+    expectPi = expect "function type" ExpectedPi
+      `(Pi {qty, arg, res, _}) `((qty, arg, res))

    export covering %inline
    expectSig : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
-    expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
+    expectSig = expect "pair type" ExpectedSig
+      `(Sig {fst, snd, _}) `((fst, snd))

    export covering %inline
    expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
-    expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
+    expectEnum = expect "enum type" ExpectedEnum `(Enum {cases, _}) `(cases)

    export covering %inline
    expectEq : Term 0 n -> Eff fs (DScopeTerm 0 n, Term 0 n, Term 0 n)
-    expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
+    expectEq = expect "equality type" ExpectedEq
+      `(Eq {ty, l, r, _}) `((ty, l, r))

    export covering %inline
    expectNAT : Term 0 n -> Eff fs ()
-    expectNAT = expect ExpectedNAT `(NAT {}) `(())
+    expectNAT = expect "Nat" ExpectedNAT `(NAT {}) `(())

    export covering %inline
    expectSTRING : Term 0 n -> Eff fs ()
-    expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
+    expectSTRING = expect "String" ExpectedSTRING `(STRING {}) `(())

    export covering %inline
    expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n)
-    expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
+    expectBOX = expect "box type" ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
--- a/lib/Quox/Typing/Context.idr
+++ b/lib/Quox/Typing/Context.idr
@ -272,7 +272,7 @@ namespace EqContext
  toTyContext : (e : EqContext n) -> TyContext e.dimLen n
  toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
    MkTyContext {
-      dctx = fromGround dassign,
+      dctx = fromGround dnames dassign,
      tctx = map (subD $ shift0 dimLen) tctx,
      dnames, tnames, qtys
    }
@ -312,9 +312,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
@ -329,7 +330,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) =
@ -342,6 +343,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

@ -357,3 +359,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
+  separateTight !commaD <$>
+  prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx
--- a/lib/Quox/Untyped/Erase.idr
+++ b/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
--- a/lib/Quox/Untyped/Scheme.idr
+++ b/lib/Quox/Untyped/Scheme.idr
@ -70,7 +70,7 @@ public export
 data Id = I String Nat
 %runElab derive "Id" [Eq, Ord]

-private
+export
 prettyId' : {opts : LayoutOpts} -> Id -> Doc opts
 prettyId' (I str 0) = text $ escId str
 prettyId' (I str k) = text $ escId "\{str}:\{show k}"
--- a/lib/Quox/Untyped/Syntax.idr
+++ b/lib/Quox/Untyped/Syntax.idr
@ -93,6 +93,10 @@ public export
 0 Definitions : Type
 Definitions = SortedMap Name Definition

+public export
+0 NDefinition : Type
+NDefinition = (Name, Definition)
+

 export covering
 prettyTerm : {opts : LayoutOpts} -> BContext n ->
@ -262,7 +266,7 @@ CanSubstSelf Term where
    B i loc =>
      getLoc th i loc
    Lam x body loc =>
-      Lam x (assert_total $ body // push th) loc
+      Lam x (assert_total $ body // push x.loc th) loc
    App fun arg loc =>
      App (fun // th) (arg // th) loc
    Pair fst snd loc =>
@ -282,19 +286,18 @@ CanSubstSelf Term where
    Succ nat loc =>
      Succ (nat // th) loc
    CaseNat nat zer suc loc =>
-      CaseNat (nat // th) (zer // th)
-              (assert_total substSuc suc th) loc
+      CaseNat (nat // th) (zer // th) (assert_total substSuc suc th) loc
    Str s loc =>
      Str s loc
    Let u x rhs body loc =>
-      Let u x (rhs // th) (assert_total $ body // push th) loc
+      Let u x (rhs // th) (assert_total $ body // push x.loc th) loc
    Erased loc =>
      Erased loc
  where
    substSuc : forall from, to.
               CaseNatSuc from -> USubst from to -> CaseNatSuc to
-    substSuc (NSRec    x ih t) th = NSRec    x ih $ t // pushN 2 th
-    substSuc (NSNonrec x    t) th = NSNonrec x    $ t // push    th
+    substSuc (NSRec    x ih t) th = NSRec    x ih $ t // pushN 2 x.loc th
+    substSuc (NSNonrec x    t) th = NSNonrec x    $ t // push    x.loc th

 public export
 subN : SnocVect s (Term n) -> Term (s + n) -> Term n
--- a/lib/Quox/Var.idr
+++ b/lib/Quox/Var.idr
@ -141,9 +141,9 @@ weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
 public export
 interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n

-public export %inline
-fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
-fromVar x = fromVarLoc x loc
+-- public export %inline
+-- fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
+-- fromVar x = fromVarLoc x loc

 public export FromVar Var where fromVarLoc x _ = x

--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@ -63,11 +63,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
    (tfst, tsnd) <- tycaseSig defs ctx1 ty
    let [< x, y] = body.names
-        a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
+        a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
        tsnd' = tsnd.term //
-          (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
-            (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
-        b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
+          (CoeT i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
+            (weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2)
+        b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
    whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
      (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc

@ -141,7 +141,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
    let ctx1 = extendDim i ctx
    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
    ta <- tycaseBOX defs ctx1 ty
-    let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
+    let xloc = body.name.loc
+    let a' = CoeT i (weakT 1 ta) p q (BVT 0 xloc) xloc
    whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
      (ST body.names $ body.term // (a' ::: shift 1)) loc

@ -218,19 +219,22 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
      STRING tyLoc =>
        whnf defs ctx sg $ Ann s (STRING tyLoc) loc

-      -- η expand
+      -- η expand.... kinda
      --
      -- (coe (𝑖 ⇒ [π. A]) @p @q s)
      --   ⇝
-      -- [case1 coe (𝑖 ⇒ [π. A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
-      --   ∷ [π. A]‹q/𝑖›
-      BOX qty inner tyLoc =>
+      -- [case1 s ∷ [π.A]‹p/𝑖› return A‹q/𝑖›
+      --  of {[x] ⇒ coe (𝑖 ⇒ A) @p @q x}] ∷ [π.A]‹q/𝑖›
+      --
+      -- a literal η expansion of `e ⇝ [case e of {[x] ⇒ x}]` causes a loop in
+      -- the equality checker because whnf of `case e ⋯` requires whnf of `e`
+      BOX qty inner tyLoc => do
        let inner = CaseBox {
              qty  = One,
-              box  = Coe (SY [< i] ty) p q s loc,
-              ret  = SN $ ty // one q,
-              body = SY [< !(mnb "x" loc)] $ BVT 0 loc,
+              box  = Ann s (ty // one p) s.loc,
+              ret  = SN $ inner // one q,
+              body = SY [< !(mnb "x" loc)] $ E $
+                     Coe (ST [< i] $ weakT 1 inner) p q (BVT 0 s.loc) s.loc,
              loc
            }
-        in
        whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc
--- a/lib/Quox/Whnf/ComputeElimType.idr
+++ b/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,19 @@ computeElimType defs ctx sg e =
    TypeCase {ret, _} =>
      pure ret

+computeElimType defs ctx sg e {ne} = do
+  let Val n = ctx.termLen
+  say "whnf" 90 e.loc "computeElimType"
+  say "whnf" 95 e.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
+  say "whnf" 90 e.loc $
+    hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]
+  res <- computeElimTypeNoLog defs ctx sg e {ne}
+  say "whnf" 91 e.loc $
+    hsep ["⇝", 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
--- a/lib/Quox/Whnf/Interface.idr
+++ b/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,17 +25,20 @@ RedexTest tm =
 public export
 interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
 where
-  whnf : (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
-         tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q))
+  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.
  -- but none of the alternatives i've thought of so far work. e.g. in some
  -- cases idris can't tell that `isRedex` and `isRedexT` are the same thing

 public export %inline
-whnf0 : {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
+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 =>
@ -83,7 +87,7 @@ isTagHead (Ann (Tag {}) (Enum {}) _) = True
 isTagHead (Coe {})                   = True
 isTagHead _                          = False

-||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ`
+||| an expression like `𝑘 ∷ ℕ` for a natural constant 𝑘, or `suc n ∷ ℕ`
 public export %inline
 isNatHead : Elim {} -> Bool
 isNatHead (Ann (Nat  {}) (NAT {}) _) = True
@ -160,11 +164,13 @@ isK (K {}) = True
 isK _      = False


-||| if `ty` is a type constructor, and `val` is a value of that type where a
-||| coercion can be reduced. which is the case if any of:
-||| - `ty` is an atomic type
-||| - `ty` has η
-||| - `val` is a constructor form
+||| true if `ty` is a type constructor, and `val` is a value of that type where
+||| a coercion can be reduced
+|||
+||| 1. `ty` is an atomic type
+||| 2. `ty` has an η law that is usable in this context
+|||    (e.g. η for pairs only exists when σ=0, not when σ=1)
+||| 3. `val` is a constructor form
 public export %inline
 canPushCoe : SQty -> (ty, val : Term {}) -> Bool
 canPushCoe sg (TYPE    {}) _         = True
--- a/lib/Quox/Whnf/Main.idr
+++ b/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,42 @@ 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
+  say "whnf" 10 s.loc "whnf"
+  say "whnf" 95 s.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
+  say "whnf" 95 s.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty]
+  say "whnf" 10 s.loc $ 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 +65,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 +88,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 +100,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 +113,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 +134,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 +161,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 +177,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 +197,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 +205,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 +225,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 +237,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 +250,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 $ Element (Succ p loc) nc
+      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
--- a/lib/Quox/Whnf/TypeCase.idr
+++ b/lib/Quox/Whnf/TypeCase.idr
@ -120,9 +120,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
    -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
    Pi {arg, res, loc = piLoc, _} =>
-      let arg' = Ann arg (TYPE u noLoc) arg.loc
+      let arg' = Ann arg (TYPE u arg.loc) arg.loc
          res' = Ann (Lam res res.loc)
-                     (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc
+                     (Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc
      in
      whnf defs ctx SZero $
        Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
@ -130,9 +130,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
    -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
    Sig {fst, snd, loc = sigLoc, _} =>
-      let fst' = Ann fst (TYPE u noLoc) fst.loc
+      let fst' = Ann fst (TYPE u fst.loc) fst.loc
          snd' = Ann (Lam snd snd.loc)
-                     (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc
+                     (Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc
      in
      whnf defs ctx SZero $
        Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
@ -150,8 +150,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
      let a0 = a.zero; a1 = a.one in
      whnf defs ctx SZero $ Ann
        (subN (tycaseRhsDef def KEq arms)
-           [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc,
-              Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc,
+           [< Ann a0 (TYPE u a.loc) a.loc, Ann a1 (TYPE u a.loc) a.loc,
+              Ann (DLam a a.loc) (Eq0 (TYPE u a.loc) a0 a1 a.loc) a.loc,
              Ann l a0 l.loc, Ann r a1 r.loc])
        ret loc

@ -166,5 +166,5 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
    -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
    BOX {ty = a, loc = boxLoc, _} =>
      whnf defs ctx SZero $ Ann
-        (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc))
+        (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u a.loc) a.loc))
        ret loc
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@ -19,6 +19,7 @@ modules =
  Quox.PrettyValExtra,
  Quox.Decidable,
  Quox.No,
+  Quox.Log,
  Quox.Loc,
  Quox.Var,
  Quox.Scoped,
--- a/pack.toml
+++ b/pack.toml
@ -1,4 +1,4 @@
-collection = "nightly-231020"
+collection = "nightly-240101"

 [custom.all.tap]
 type = "git"
--- a/quox.bib
+++ b/quox.bib
@ -329,6 +329,13 @@
  doi          = {10.1109/LICS.2000.855774},
 }

+@misc{ornaments,
+  author = {Conor {McBride}},
+  title  = {Ornamental Algebras, Algebraic Ornaments},
+  year   = {2011},
+  url    = {https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/LitOrn.pdf},
+}
+

 % Misc implementation

--- a/tests/Tests/DimEq.idr
+++ b/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",
--- a/tests/Tests/FromPTerm.idr
+++ b/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
--- a/tests/Tests/Reduce.idr
+++ b/tests/Tests/Reduce.idr
@ -15,7 +15,8 @@ import Control.Eff
 runWhnf : Eff Whnf a -> Either Error a
 runWhnf act = runSTErr $ do
  runEff act [handleExcept (\e => stLeft e),
-              handleStateSTRef !(liftST $ newSTRef 0)]
+              handleStateSTRef !(liftST $ newSTRef 0),
+              handleLogDiscard]

 parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
           {auto _ : (Eq (tm d n), Show (tm d n))}
--- a/tests/TypingImpls.idr
+++ b/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 !(liftST $ newSTRef 0),
+     handleLogDiscard]

 export
 runTC : Definitions -> Eff TC a -> Either Error a
Author	SHA1	Message	Date
rhiannon morris	8b8bec250a	wip	2024-02-10 10:14:22 +01:00
rhiannon morris	103700d882	wip	2024-02-10 10:14:22 +01:00
rhiannon morris	642ac25a71	happy new year [pack update. also idris 0.7.0]	2024-02-10 10:14:22 +01:00
rhiannon morris	05a688d49e	reject "" in NatExtra.fromHex	2024-02-10 10:14:22 +01:00
rhiannon morris	1c8c50f3e2	remove some unneeded Ord impls	2024-02-10 10:14:22 +01:00
rhiannon morris	f337625801	remove most noLocs	2024-02-10 10:14:22 +01:00
rhiannon morris	1f01cec322	refactor Main a whole lot	2024-02-10 10:14:22 +01:00
rhiannon morris	103f019dbd	move NDefinition to Quox.Definition and add an untyped one	2024-02-10 10:14:22 +01:00
rhiannon morris	2cafb35bc1	fix some comments	2024-02-10 10:14:22 +01:00
rhiannon morris	47069a9316	fill a stray hole	2024-02-10 10:14:22 +01:00
rhiannon morris	fb14b756c7	add algebraic ornaments to bib	2024-02-10 10:14:22 +01:00
rhiannon morris	81783dbae0	fix typechecker loop when coercing boxes closes #38	2024-02-10 10:07:06 +01:00