pretty printing fixes

exe/CompileMonad.idr

@@ -14,6 +14,7 @@ import Error
 
 import System.File
 import Data.IORef
+import Data.Maybe
 import Control.Eff
 
 %default total
@@ -57,12 +58,18 @@ Compile =
    ReaderL STATE State, ReaderL OPTS Options, Log,
    LoadFile, IO]
 
+
 export %inline
 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
+handleLog ref f l = case f of
+  OConsole ch => handleLogIO (const $ pure ()) ref (consoleHandle ch) l
+  OFile _ h   => handleLogIO (const $ pure ()) ref h l
+  ONone       => do
+    lvls   <- readIORef ref
+    lenRef <- newIORef (length lvls)
+    res    <- handleLogDiscardIO lenRef l
+    writeIORef ref $ fixupDiscardedLog !(readIORef lenRef) lvls
+    pure res
 
 private %inline
 withLogFile : Options ->

exe/Main.idr

@@ -34,9 +34,8 @@ Step : Type -> Type -> Type
 Step a b = OpenFile -> a -> Eff Compile b
 
 private
-step : {default CErr console : ConsoleChannel} ->
-       Phase -> OutFile -> Step a b -> a -> Eff CompileStop b
-step phase file act x = do
+step : ConsoleChannel -> Phase -> OutFile -> Step a b -> a -> Eff CompileStop b
+step console phase file act x = do
   opts <- askAt OPTS
   res  <- withOutFile console file fromError $ \h => lift $ act h x
   when (opts.until == Just phase) stopHere
@@ -99,11 +98,11 @@ processFile : String -> Eff Compile ()
 processFile file = withEarlyStop $ pipeline !(askAt OPTS) file where
   pipeline : Options -> String -> Eff CompileStop ()
   pipeline opts =
-    step Parse  opts.dump.parse  Main.parse  >=>
-    step Check  opts.dump.check  Main.check  >=>
-    step Erase  opts.dump.erase  Main.erase  >=>
-    step Scheme opts.dump.scheme Main.scheme >=>
-    step End    opts.outFile     Main.output {console = COut}
+    step CErr Parse  opts.dump.parse  Main.parse  >=>
+    step CErr Check  opts.dump.check  Main.check  >=>
+    step CErr Erase  opts.dump.erase  Main.erase  >=>
+    step CErr Scheme opts.dump.scheme Main.scheme >=>
+    step COut End    opts.outFile     Main.output
 
 
 export covering

lib/Quox/EffExtra.idr

@@ -36,6 +36,15 @@ gets : Has (State s) fs => (s -> a) -> Eff fs a
 gets = getsAt ()
 
 
+export %inline
+stateAt : (0 lbl : tag) -> Has (StateL lbl s) fs => (s -> (a, s)) -> Eff fs a
+stateAt lbl f = do (res, x) <- getsAt lbl f; putAt lbl x $> res
+
+export %inline
+state : Has (State s) fs => (s -> (a, s)) -> Eff fs a
+state = stateAt ()
+
+
 export
 handleStateIORef : HasIO m => IORef st -> StateL lbl st a -> m a
 handleStateIORef r Get     = readIORef r
@@ -47,7 +56,6 @@ handleStateSTRef r Get     = liftST $ readSTRef r
 handleStateSTRef r (Put s) = liftST $ writeSTRef r s
 
 
-
 public export
 data Length : List a -> Type where
   Z : Length []
@@ -98,8 +106,8 @@ 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)
+handleWriterSTRef : HasST m => STRef s (SnocList w) -> WriterL lbl w a -> m s a
+handleWriterSTRef ref (Tell w) = liftST $ modifySTRef ref (:< w)
 
 
 public export

lib/Quox/Log.idr

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

lib/Quox/Name.idr

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

lib/Quox/Parser/FromParser.idr

@@ -49,10 +49,9 @@ record PureParserResult a where
   logLevels : LevelStack
 
 export
-fromParserPure : {default [<] ns : Mods} ->
-                 NameSuf -> Definitions -> LevelStack ->
+fromParserPure : Mods -> NameSuf -> Definitions -> LevelStack ->
                  Eff FromParserPure a -> Either Error (PureParserResult a)
-fromParserPure suf defs lvls act = runSTErr $ do
+fromParserPure ns suf defs lvls act = runSTErr $ do
   suf  <- newSTRef' suf
   defs <- newSTRef' defs
   log  <- newSTRef' [<]
@@ -76,7 +75,7 @@ parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
            (xs : Context' PatVar n)
   private
   fromBaseName : PBaseName -> m a
-  fromBaseName x = maybe (f $ MakePName [<] x) b $
+  fromBaseName x = maybe (f $ MkPName [<] x) b $
                    Context.find (\y => y.name == Just x) xs
 
   private
@@ -376,7 +375,7 @@ export covering
 expectFail : Loc -> Eff FromParserPure a -> Eff FromParserPure Error
 expectFail loc act = do
   gen <- getAt GEN; defs <- getAt DEFS; ns <- getAt NS; lvl <- curLevels
-  case fromParserPure {ns} gen defs (singleton lvl) act of
+  case fromParserPure ns gen defs (singleton lvl) act of
     Left  err => pure err
     Right _   => throw $ ExpectedFail loc
 
@@ -399,6 +398,10 @@ fromPDecl (PDef def) =
 fromPDecl (PNs  ns)  =
   maybeFail ns.fail ns.loc $
   localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
+fromPDecl (PPrag prag) =
+  case prag of
+    PLogPush p _ => Log.push p $> []
+    PLogPop    _ => Log.pop    $> []
 
 mutual
   export covering

lib/Quox/Parser/Lexer.idr

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

lib/Quox/Parser/Parser.idr

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

lib/Quox/Parser/Syntax.idr

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

lib/Quox/PrettyValExtra.idr

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

lib/Quox/Syntax/Term/Pretty.idr

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

lib/Quox/Typing/Context.idr

@@ -391,5 +391,5 @@ 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
+  sepSingle . exceptLast (<+> comma) . toList <$>
+    prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx

lib/Quox/Untyped/Scheme.idr

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

tests/Tests/Equal.idr

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

tests/Tests/FromPTerm.idr

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

tests/Tests/Lexer.idr

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

tests/Tests/Parser.idr

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

tests/Tests/PrettyTerm.idr

@@ -37,8 +37,8 @@ tests = "pretty printing terms" :- [
   "free vars" :- [
     testPrettyE1 [<] [<] (^F "x" 0) "x",
     testPrettyE  [<] [<] (^F "x" 1) "x¹" "x^1",
-    testPrettyE1 [<] [<] (^F (MakeName [< "A", "B", "C"] "x") 0) "A.B.C.x",
-    testPrettyE  [<] [<] (^F (MakeName [< "A", "B", "C"] "x") 2)
+    testPrettyE1 [<] [<] (^F (MkName [< "A", "B", "C"] "x") 0) "A.B.C.x",
+    testPrettyE  [<] [<] (^F (MkName [< "A", "B", "C"] "x") 2)
       "A.B.C.x²"
       "A.B.C.x^2"
   ],

tests/Tests/Reduce.idr

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

tests/Tests/Typechecker.idr

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

tests/TypingImpls.idr

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