add logging to core

exe/CompileMonad.idr

@@ -37,7 +37,7 @@ record State where
   suf  : IORef NameSuf
 %name CompileMonad.State state
 
-export
+export %inline
 newState : HasIO io => io State
 newState = pure $ MkState {
   seen = !(newIORef empty),
@@ -57,14 +57,14 @@ Compile =
    ReaderL STATE State, ReaderL OPTS Options, Log,
    LoadFile, IO]
 
-export
+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
 
-private
+private %inline
 withLogFile : Options ->
               (IORef LevelStack -> OpenFile -> IO (Either Error a)) ->
               IO (Either Error a)
@@ -75,7 +75,7 @@ where
   fromError : String -> FileError -> IO (Either Error a)
   fromError file err = pure $ Left $ WriteError file err
 
-export covering
+export covering %inline
 runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
 runCompile opts state act = do
   withLogFile opts $ \lvls, logFile =>
@@ -87,19 +87,19 @@ runCompile opts state act = do
        handleLoadFileIOE loadError ParseError state.seen opts.include,
        liftIO]
 
-private
+private %inline
 rethrowFileC : String -> Either FileError a -> Eff Compile a
 rethrowFileC f = rethrow . mapFst (WriteError f)
 
 
-export
+export %inline
 outputStr : OpenFile -> Lazy String -> Eff Compile ()
 outputStr ONone           _   = pure ()
 outputStr (OConsole COut) str = putStr str
 outputStr (OConsole CErr) str = fPutStr stderr str >>= rethrowFileC "<stderr>"
 outputStr (OFile f h)     str = fPutStr h str >>= rethrowFileC f
 
-export
+export %inline
 outputDocs : OpenFile ->
              ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
              Eff Compile ()
@@ -108,7 +108,7 @@ outputDocs file docs = do
   for_ (runPretty opts (toOutFile file) docs) $ \x =>
     outputStr file $ render (Opts opts.width) x
 
-export
+export %inline
 outputDoc : OpenFile ->
             ({opts : LayoutOpts} -> Eff Pretty (Doc opts)) -> Eff Compile ()
 outputDoc file doc = outputDocs file $ singleton <$> doc
@@ -121,16 +121,16 @@ public export
 CompileStop : List (Type -> Type)
 CompileStop = FailL STOP :: Compile
 
-export
+export %inline
 withEarlyStop : Eff CompileStop () -> Eff Compile ()
 withEarlyStop = ignore . runFailAt STOP
 
-export
+export %inline
 stopHere : Has (FailL STOP) fs => Eff fs ()
 stopHere = failAt STOP
 
 
-export
+export %inline
 liftFromParser : Eff FromParserIO a -> Eff Compile a
 liftFromParser act =
   runEff act $ with Union.(::)
@@ -141,7 +141,7 @@ liftFromParser act =
      \g => send g,
      \g => send g]
 
-export
+export %inline
 liftErase : Q.Definitions -> Eff Erase a -> Eff Compile a
 liftErase defs act =
   runEff act
@@ -149,7 +149,7 @@ liftErase defs act =
      handleStateIORef !(asksAt STATE suf),
      \g => send g]
 
-export
+export %inline
 liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
 liftScheme act = do
   runEff [|MkPair act (getAt MAIN)|]

lib/Control/Monad/ST/Extra.idr

@@ -65,14 +65,18 @@ stLeft e = STE $ pure $ Left e
 
 
 parameters {auto _ : HasST m}
+  export %inline
+  newSTRef' : a -> m s (STRef s a)
+  newSTRef' x = liftST $ newSTRef x
+
   export %inline
   readSTRef' : STRef s a -> m s a
-  readSTRef' r = liftST $ ST.readSTRef r
+  readSTRef' r = liftST $ readSTRef r
 
   export %inline
   writeSTRef' : STRef s a -> a -> m s ()
-  writeSTRef' r x = liftST $ ST.writeSTRef r x
+  writeSTRef' r x = liftST $ writeSTRef r x
 
   export %inline
   modifySTRef' : STRef s a -> (a -> a) -> m s ()
-  modifySTRef' r f = liftST $ ST.modifySTRef r f
+  modifySTRef' r f = liftST $ modifySTRef r f

lib/Quox/Equal.idr

@@ -86,11 +86,11 @@ 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]
+  sayMany "equal" ty.loc
+    [logLevel :> "isEmpty",
+     95       :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     95       :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     logLevel :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
   res <- isEmptyNoLog defs ctx sg ty
   say "equal" logLevel ty.loc $ hsep ["isEmpty ⇝", pshow res]
   pure res
@@ -135,11 +135,11 @@ 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]
+  sayMany "equal" ty.loc
+    [logLevel :> "isSubSing",
+     95       :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     95       :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     logLevel :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
   res <- isSubSingNoLog defs ctx sg ty
   say "equal" logLevel ty.loc $ hsep ["isSubsing ⇝", pshow res]
   pure res
@@ -182,10 +182,10 @@ ensureTyConNoLog loc ctx ty = do
     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]
+  sayMany "equal" ty.loc
+    [60 :> "ensureTyCon",
+     95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     60 :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty]]
   ensureTyConNoLog loc ctx ty
 
 
@@ -807,14 +807,14 @@ namespace Term
       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]
+    sayMany "equal" s.loc
+      [30 :> "Term.compare0",
+       30 :> hsep ["mode =", pshow !mode],
+       95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+       95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+       31 :> hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty],
+       30 :> hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s],
+       30 :> hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]]
     compare0NoLog defs ctx sg ty s t
 
 namespace Elim
@@ -827,15 +827,16 @@ namespace Elim
     maybe (pure ty) throw err
 
   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]
+    sayMany "equal" e.loc
+      [30 :> "Elim.compare0",
+       30 :> hsep ["mode =", pshow !mode],
+       95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+       95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+       30 :> hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e],
+       30 :> hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f]]
     ty <- compare0NoLog defs ctx sg e f
     say "equal" 31 e.loc $
-      hsep ["ty ⇝", runPretty $ prettyTerm [<] ctx.tnames ty]
+      hsep ["Elim.compare0 ⇝", runPretty $ prettyTerm [<] ctx.tnames ty]
     pure ty
 
 export covering %inline
@@ -850,11 +851,12 @@ compareTypeNoLog defs ctx s t = do
   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]
+  sayMany "equal" s.loc
+    [30 :> "compareType",
+     30 :> hsep ["mode =", pshow !mode],
+     95 :> hsep ["ctx =", runPretty $ prettyEqContext ctx],
+     30 :> hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s],
+     30 :> hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t]]
   compareTypeNoLog defs ctx s t
 
 

lib/Quox/Log.idr

@@ -117,12 +117,21 @@ mergePush (SetDefault def) = {defLevel := def}
 mergePush (SetCats    map) = {levels   $= (map ++)}
 
 
+public export
+record LogMsg where
+  constructor (:>)
+  level : Nat
+  {auto 0 levelOk : IsLogLevel level}
+  message : Lazy LogDoc
+infix 0 :>
+%name Log.LogMsg msg
+
 public export
 data LogL : (lbl : tag) -> Type -> Type where
-  Say  : (cat : LogCategory) -> (lvl : LogLevel) ->
-         (loc : Loc) -> (msg : Lazy LogDoc) -> LogL lbl ()
-  Push : (push : PushArg) -> LogL lbl ()
-  Pop  : LogL lbl ()
+  SayMany   : (cat : LogCategory) -> (loc : Loc) ->
+              (msgs : List LogMsg) -> LogL lbl ()
+  Push      : (push : PushArg) -> LogL lbl ()
+  Pop       : LogL lbl ()
   CurLevels : LogL lbl LogLevels
 
 public export
@@ -130,12 +139,17 @@ Log : Type -> Type
 Log = LogL ()
 
 parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs}
+  public export %inline
+  sayManyAt : (cat : String) -> (0 catOk : IsLogCategory cat) =>
+              Loc -> List LogMsg -> Eff fs ()
+  sayManyAt cat loc msgs {catOk} =
+    send $ SayMany {lbl} (Element cat catOk) loc msgs
+
   public export %inline
   sayAt : (cat : String) -> (0 catOk : IsLogCategory cat) =>
           (lvl : Nat)    -> (0 lvlOk : IsLogLevel lvl) =>
           Loc -> Lazy LogDoc -> Eff fs ()
-  sayAt cat lvl loc msg {catOk, lvlOk} =
-    send $ Say {lbl} (Element cat catOk) (Element lvl lvlOk) loc msg
+  sayAt cat lvl loc msg = sayManyAt cat loc [lvl :> msg]
 
   public export %inline
   pushAt : PushArg -> Eff fs ()
@@ -150,6 +164,11 @@ parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs}
   curLevelsAt = send $ CurLevels {lbl}
 
 parameters {auto _ : Has Log fs}
+  public export %inline
+  sayMany : (cat : String) -> (0 catOk : IsLogCategory cat) =>
+            Loc -> List LogMsg -> Eff fs ()
+  sayMany = sayManyAt ()
+
   public export %inline
   say : (cat : String) -> (0 _ : IsLogCategory cat) =>
         (lvl : Nat)    -> (0 _ : IsLogLevel lvl) =>
@@ -169,51 +188,53 @@ parameters {auto _ : Has Log fs}
   curLevels = curLevelsAt ()
 
 
-export
+export %inline
 doPush : PushArg -> LevelStack -> LevelStack
 doPush push list = mergePush push (head list) `cons` list
 
-export
+export %inline
 doPop : List1 a -> List1 a
-doPop list = fromMaybe list $ fromList list.tail
+doPop (_ ::: x :: xs) = x ::: xs
+doPop (x ::: [])      = x ::: []
 
-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 %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
+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
-  Say cat lvl loc msg => doSay !(readIORef lvls) printMsg cat lvl loc msg
-  CurLevels           => head <$> readIORef lvls
+  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
 where printMsg : LogDoc -> m ()
       printMsg msg = fPutStr h (render _ msg) >>= either th pure
 
-export
+export %inline
 handleLogST : (HasST m, Monad (m s)) =>
-              STRef s (SnocList LogDoc) ->
-              STRef s LevelStack ->
+              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
+  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)
 
-export
+export %inline
 handleLogDiscard : Applicative m => LogL tag a -> m a
 handleLogDiscard = \case
-  Say  {}   => pure ()
-  Push {}   => pure ()
-  Pop       => pure ()
-  CurLevels => pure defaultLogLevels
+  SayMany {} => pure ()
+  Push    {} => pure ()
+  Pop        => pure ()
+  CurLevels  => pure defaultLogLevels

lib/Quox/Parser/FromParser.idr

@@ -53,22 +53,22 @@ fromParserPure : {default [<] ns : Mods} ->
                  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
+  suf  <- newSTRef' suf
+  defs <- newSTRef' defs
+  log  <- newSTRef' [<]
+  lvls <- newSTRef' lvls
   res  <- runEff act $ with Union.(::)
-    [handleExcept (\e => stLeft e),
+    [handleExcept $ \e => stLeft e,
      handleStateSTRef defs,
-     handleStateSTRef !(liftST $ newSTRef ns),
+     handleStateSTRef !(newSTRef' ns),
      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)
+    suf       = !(readSTRef' suf),
+    defs      = !(readSTRef' defs),
+    log       = !(readSTRef' log),
+    logLevels = !(readSTRef' lvls)
   }
 
 

lib/Quox/Typechecker.idr

@@ -52,12 +52,13 @@ 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]
+  let tyDoc = delay $ maybe (text "none") (runPretty . prettyTermTC ctx) ty
+  sayMany "check" subj.loc
+    [10 :> text fun,
+     95 :> hsep ["ctx =",  runPretty $ prettyTyContext ctx],
+     95 :> hsep ["sg =",   runPretty $ prettyQty sg.qty],
+     10 :> hsep ["subj =", runPretty $ prettyTermTC ctx subj],
+     10 :> hsep ["ty =",   tyDoc]]
 
 mutual
   ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
@@ -71,10 +72,10 @@ 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 = do
-    checkLogs "check" ctx sg subj (Just ty)
+  check ctx sg subj ty =
     ifConsistentElse ctx.dctx
-      (checkC ctx sg subj ty)
+      (do checkLogs "check" ctx sg subj (Just ty)
+          checkC ctx sg subj ty)
       (say "check" 20 subj.loc "check: 0=1")
 
   ||| "Ψ | Γ ⊢₀ s ⇐ A"
@@ -108,9 +109,9 @@ mutual
   checkType : TyContext d n -> Term d n -> Maybe Universe -> Eff TC ()
   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)
+      (do checkLogs "checkType" ctx SZero subj univ
+          checkTypeC ctx subj l)
       (say "check" 20 subj.loc "checkType: 0=1")
 
   export covering %inline
@@ -135,9 +136,9 @@ mutual
   infer : (ctx : TyContext d n) -> SQty -> Elim d n ->
           Eff TC (InferResult ctx.dctx d n)
   infer ctx sg subj = do
-    checkLogs "infer" ctx sg (E subj) Nothing
     ifConsistentElse ctx.dctx
-      (inferC ctx sg subj)
+      (do checkLogs "infer" ctx sg (E subj) Nothing
+          inferC ctx sg subj)
       (say "check" 20 subj.loc "infer: 0=1")
 
   ||| `infer`, assuming the dimension context is consistent

lib/Quox/Typing.idr

@@ -83,50 +83,45 @@ parameters (defs : Definitions)
       rethrow res
 
     private covering %macro
-    expect : String -> ExpectErrorConstructor ->
-             TTImp -> TTImp -> Elab (Term d n -> Eff fs a)
-    expect what err pat rhs = Prelude.do
+    expect : ExpectErrorConstructor -> TTImp -> TTImp ->
+             Elab (Term d n -> Eff fs a)
+    expect err pat rhs = Prelude.do
       match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
       pure $ \term => do
-        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 "universe" ExpectedTYPE `(TYPE {l, _}) `(l)
+    expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
 
     export covering %inline
     expectPi : Term d n -> Eff fs (Qty, Term d n, ScopeTerm d n)
-    expectPi = expect "function type" ExpectedPi
-      `(Pi {qty, arg, res, _}) `((qty, arg, res))
+    expectPi = expect 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 "pair type" ExpectedSig
-      `(Sig {fst, snd, _}) `((fst, snd))
+    expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
 
     export covering %inline
     expectEnum : Term d n -> Eff fs (SortedSet TagVal)
-    expectEnum = expect "enum type" ExpectedEnum
-      `(Enum {cases, _}) `(cases)
+    expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
 
     export covering %inline
     expectEq : Term d n -> Eff fs (DScopeTerm d n, Term d n, Term d n)
-    expectEq = expect "equality type" ExpectedEq
-      `(Eq {ty, l, r, _}) `((ty, l, r))
+    expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
 
     export covering %inline
     expectNAT : Term d n -> Eff fs ()
-    expectNAT = expect "Nat" ExpectedNAT `(NAT {}) `(())
+    expectNAT = expect ExpectedNAT `(NAT {}) `(())
 
     export covering %inline
     expectSTRING : Term d n -> Eff fs ()
-    expectSTRING = expect "String" ExpectedSTRING `(STRING {}) `(())
+    expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
 
     export covering %inline
     expectBOX : Term d n -> Eff fs (Qty, Term d n)
-    expectBOX = expect "box type" ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
+    expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
 
 
   namespace EqContext
@@ -139,47 +134,43 @@ parameters (defs : Definitions)
       rethrow res
 
     private covering %macro
-    expect : String -> ExpectErrorConstructor ->
-             TTImp -> TTImp -> Elab (Term 0 n -> Eff fs a)
-    expect what err pat rhs = do
+    expect : ExpectErrorConstructor -> TTImp -> TTImp ->
+             Elab (Term 0 n -> Eff fs a)
+    expect err pat rhs = do
       match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing)
       pure $ \term => do
-        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 "universe" ExpectedTYPE `(TYPE {l, _}) `(l)
+    expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
 
     export covering %inline
     expectPi : Term 0 n -> Eff fs (Qty, Term 0 n, ScopeTerm 0 n)
-    expectPi = expect "function type" ExpectedPi
-      `(Pi {qty, arg, res, _}) `((qty, arg, res))
+    expectPi = expect 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 "pair type" ExpectedSig
-      `(Sig {fst, snd, _}) `((fst, snd))
+    expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
 
     export covering %inline
     expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
-    expectEnum = expect "enum type" ExpectedEnum `(Enum {cases, _}) `(cases)
+    expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
 
     export covering %inline
     expectEq : Term 0 n -> Eff fs (DScopeTerm 0 n, Term 0 n, Term 0 n)
-    expectEq = expect "equality type" ExpectedEq
-      `(Eq {ty, l, r, _}) `((ty, l, r))
+    expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
 
     export covering %inline
     expectNAT : Term 0 n -> Eff fs ()
-    expectNAT = expect "Nat" ExpectedNAT `(NAT {}) `(())
+    expectNAT = expect ExpectedNAT `(NAT {}) `(())
 
     export covering %inline
     expectSTRING : Term 0 n -> Eff fs ()
-    expectSTRING = expect "String" ExpectedSTRING `(STRING {}) `(())
+    expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
 
     export covering %inline
     expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n)
-    expectBOX = expect "box type" ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
+    expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))

lib/Quox/Var.idr

@@ -141,9 +141,6 @@ 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 FromVar Var where fromVarLoc x _ = x
 

lib/Quox/Whnf/ComputeElimType.idr

@@ -93,13 +93,14 @@ computeElimTypeNoLog defs ctx sg e =
 
 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]
+  sayMany "whnf" e.loc
+    [90 :> "computeElimType",
+     95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx],
+     90 :> hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]]
   res <- computeElimTypeNoLog defs ctx sg e {ne}
   say "whnf" 91 e.loc $
-    hsep ["⇝", runPretty $ prettyTerm ctx.dnames ctx.tnames res]
+    hsep ["computeElimType ⇝",
+          runPretty $ prettyTerm ctx.dnames ctx.tnames res]
   pure res
 
 computeWhnfElimType0 defs ctx sg e =

lib/Quox/Whnf/Main.idr

@@ -28,10 +28,11 @@ whnfDefault :
   (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]
+  sayMany "whnf" s.loc
+    [10 :> "whnf",
+     95 :> hsep ["ctx =", runPretty $ prettyWhnfContext ctx],
+     95 :> hsep ["sg =", runPretty $ prettyQty sg.qty],
+     10 :> hsep [text name, "=", runPretty $ ppr ctx s]]
   res <- whnfNoLog defs ctx sg s
   say "whnf" 11 s.loc $ hsep ["whnf ⇝", runPretty $ ppr ctx res.fst]
   pure res

pack.toml

@@ -1,4 +1,4 @@
-collection = "nightly-240101"
+collection = "nightly-240326"
 
 [custom.all.tap]
 type = "git"

tests/Tests/PrettyTerm.idr

@@ -215,6 +215,7 @@ tests = "pretty printing terms" :- [
       "type-case Nat :: Type 0 return Type 0 of { _ => Nat }"
   ],
 
+  skipWith "(todo: print user-written redundant annotations)" $
   "annotations" :- [
     testPrettyE [<] [<]
       (^Ann (^FT "a" 0) (^FT "A" 0))