examples/bool.quox

@@ -17,7 +17,7 @@ def0 If : 1.Bool → 0.★₀ → 0.★₀ → ★₀ =
 def0 T : ω.Bool → ★₀ = λ b ⇒ If b True False;
 
 def true-not-false : Not ('true ≡ 'false : Bool) =
-  λ eq ⇒ coe [i ⇒ T (eq @i)] 'true;
+  λ eq ⇒ coe [i ⇒ T (eq @i)] @0 @1 'true;
 
 
 -- [todo] infix

examples/misc.quox

@@ -28,9 +28,9 @@ def funext :
   λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖;
 
 def sym : 0.(A : ★₀) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
-  λ A x y eq ⇒ δ 𝑖 ⇒ comp [A] (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 };
+  λ A x y eq ⇒ δ 𝑖 ⇒ comp [A] @0 @1 (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 };
 
 def trans : 0.(A : ★₀) → 0.(x y z : A) →
             ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
   λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒
-    comp [A] (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 };
+    comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @0 };

examples/nat.quox

@@ -51,7 +51,7 @@ def zero-not-succ : 0.(m : ℕ) → Not (zero ≡ succ m : ℕ) =
   λ m eq ⇒ coe [𝑖 ⇒ IsSucc (eq @𝑖)] @1 @0 'true;
 
 def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) =
-  λ m eq ⇒ coe [𝑖 ⇒ IsSucc (eq @𝑖)] 'true;
+  λ m eq ⇒ coe [𝑖 ⇒ IsSucc (eq @𝑖)] @0 @1 'true;
 
 
 def0 not-succ-self : 0.(m : ℕ) → Not (m ≡ succ m : ℕ) =

exe/Main.idr

@@ -9,26 +9,11 @@ import System
 import Data.IORef
 import Data.SortedSet
 import Control.Eff
+import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
-private
-Opts : LayoutOpts
-Opts = Opts 80
-
-private
-putDoc : Doc Opts -> IO ()
-putDoc = putStr . render Opts
-
-private
-die : Doc Opts -> IO a
-die err = do putDoc err; exitFailure
-
-private
-prettySig : {opts : _} -> Name -> Definition -> Eff Pretty (Doc opts)
-prettySig name def = do
-  qty  <- prettyQty def.qty.fst
-  name <- prettyFree name
-  type <- prettyTerm [<] [<] def.type
-  hangDSingle (hsep [hcat [qty, !dotD, name], !colonD]) type
+export
+die : Doc HL -> IO a
+die err = do putDoc $ termHL <$> err; exitFailure
 
 export
 main : IO ()
@@ -39,11 +24,15 @@ main = do
   for_ (drop 1 !getArgs) $ \file => do
     putStrLn "checking \{file}"
     Right res <- fromParserIO ["."] seen suf defs $ loadProcessFile noLoc file
-      | Left err => die $ runPrettyColor $ prettyError True err
-    for_ res $ \(name, def) => putDoc $ runPrettyColor $ prettySig name def
+      | Left err => die $ prettyError True True err
+    for_ res $ \(name, def) => do
+      putDoc $ map termHL $ nest 2 $
+        sep [hsep [hcat [pretty0 True def.qty.fst, dotD,
+                         hl Free (pretty0 True name)],
+                   colonD],
+             prettyTerm True [<] [<] def.type]
 
 -----------------------------------
-{-
 
 private
 text : PrettyOpts -> List String
@@ -84,4 +73,3 @@ join1 opts l r =
 export
 banner : PrettyOpts -> String
 banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
--}

lib/Quox/Context.idr

@@ -319,27 +319,9 @@ export %inline
   showPrec d = showPrec d . toSnocList
     where Show (Exists tm) where showPrec d t = showPrec d t.snd
 
-
-parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
-           (nameHL : HL)
-           (pterm : forall n. BContext n -> tm n -> Eff Pretty (Doc opts))
-  private
-  prettyOne : BindName -> BContext to -> tm to -> Eff Pretty (Doc opts)
-  prettyOne x xs tm = hsep <$> sequence
-    [hl nameHL $ prettyBind' x, hl Delim $ text ":", pterm xs tm]
-
-  private
-  prettyEach : BContext to -> Telescope tm from to ->
-               Eff Pretty (Telescope' (Doc opts) from to)
-  prettyEach _         [<]       = pure [<]
-  prettyEach (xs :< x) (ts :< t) = [|prettyEach xs ts :< prettyOne x xs t|]
-
-  export
-  prettyTel : BContext to -> Telescope tm from to -> Eff Pretty (Doc opts)
-  prettyTel names tel = do
-    docs <- prettyEach names tel
-    comma <- hl Delim $ text ","
-    pure $ separateTight comma $ toList' docs
+export %inline
+(forall n. PrettyHL (tm n)) => PrettyHL (Telescope tm from to) where
+  prettyM tel = separate (hl Delim ";") <$> traverse prettyM (toList tel)
 
 
 namespace BContext

lib/Quox/Parser/FromParser.idr

@@ -6,7 +6,6 @@ import Quox.Parser.Parser
 import Quox.Typechecker
 
 import Data.List
-import Data.Maybe
 import Data.SnocVect
 import Quox.EffExtra
 

lib/Quox/Parser/FromParser/Error.idr

@@ -29,73 +29,56 @@ data Error =
   | WrapParseError String ParseError
 
 
-export
-prettyLexError : {opts : _} -> String -> LexError -> Eff Pretty (Doc opts)
-prettyLexError file (Err reason line col char) = do
-  let loc = makeLoc file (MkBounds line col line col)
-  reason <- case reason of
-    EndInput    => pure "unexpected end of input"
-    NoRuleApply => pure $ text "unrecognised character: \{show char}"
-    ComposeNotClosing (sl, sc) (el, ec) => pure $
-      hsep ["unterminated token at", !(prettyBounds (MkBounds sl sc el ec))]
-  pure $ vappend !(prettyLoc loc) reason
-
-export
-prettyParseError1 : {opts : _} -> String -> ParsingError _ ->
-                    Eff Pretty (Doc opts)
-prettyParseError1 file (Error msg Nothing) =
-  pure $ text msg
-prettyParseError1 file (Error msg (Just bounds)) =
-  pure $ vappend !(prettyLoc $ makeLoc file bounds) (text msg)
-
-export
-prettyParseError : {opts : _} -> String -> ParseError ->
-                   Eff Pretty (Doc opts)
-prettyParseError file (LexError err) =
-  pure $ vsep ["lexical error:", !(prettyLexError file err)]
-prettyParseError file (ParseError errs) =
-  map (vsep . ("parse error:" ::)) $
-    traverse (map ("-" <++>) . prettyParseError1 file) (toList errs)
-
-
-parameters (showContext : Bool)
+parameters (unicode, showContext : Bool)
   export
-  prettyError : {opts : _} -> Error -> Eff Pretty (Doc opts)
+  prettyParseError1 : String -> ParsingError _ -> Doc HL
+  prettyParseError1 file (Error msg Nothing) =
+    pretty msg
+  prettyParseError1 file (Error msg (Just bounds)) =
+    hsep [prettyLoc $ makeLoc file bounds, pretty msg]
+
+  export
+  prettyParseError : String -> ParseError -> Doc HL
+  prettyParseError file (LexError   err) =
+    vsep ["lexical error:", nest 2 $ pretty $ show err]
+  prettyParseError file (ParseError errs) =
+    vsep $ "parse error:" ::
+           map (("-" <++>) . prettyParseError1 file) (toList errs)
+
+  export
+  prettyError : Error -> Doc HL
   prettyError (AnnotationNeeded loc ctx tm) =
-    [|vappend (prettyLoc loc)
-        (hangD "type annotation needed on"
-               !(prettyTerm ctx.dnames ctx.tnames tm))|]
+    sep [prettyLoc loc <++> "the term",
+         prettyTerm unicode ctx.dnames ctx.tnames tm,
+         "needs a type annotation"]
     -- [todo] print the original PTerm instead
 
   prettyError (DuplicatesInEnum loc tags) =
-    [|vappend (prettyLoc loc)
-        (hangD "duplicate tags in enum type" !(prettyEnum tags))|]
+    sep [prettyLoc loc <++> "duplicate tags in enum type",
+         braces $ fillSep $ map pretty tags]
 
   prettyError (DimNotInScope loc i) =
-    [|vappend (prettyLoc loc)
-        (pure $ hsep ["dimension", !(hl DVar $ text i), "not in scope"])|]
+    sep [prettyLoc loc <++> "dimension",
+         pretty0 unicode $ DV $ fromString i, "not in scope"]
 
   prettyError (TermNotInScope loc x) =
-    [|vappend (prettyLoc loc)
-        (pure $ hsep ["term variable", !(prettyFree x), "not in scope"])|]
+    sep [prettyLoc loc <++> "term variable",
+         hl Free $ pretty0 unicode x, "not in scope"]
 
-  prettyError (QtyNotGlobal loc pi) = pure $
-    vappend !(prettyLoc loc)
-      (sep ["quantity" <++> !(prettyQty pi),
-            "can't be used on a top level declaration"])
+  prettyError (QtyNotGlobal loc pi) =
+    sep [prettyLoc loc <++> "quantity", pretty0 unicode pi,
+         "can't be used on a top level declaration"]
 
-  prettyError (DimNameInTerm loc i) = pure $
-    vappend !(prettyLoc loc)
-      (sep ["dimension" <++> !(hl DVar $ text i),
-            "used in a term context"])
+  prettyError (DimNameInTerm loc i) =
+    sep [prettyLoc loc <++> "dimension variable",
+         pretty0 unicode $ DV $ fromString i, "used in a term context"]
 
   prettyError (WrapTypeError err) =
-    Typing.prettyError showContext $ trimContext 2 err
+    Typing.prettyError unicode showContext $ trimContext 2 err
 
-  prettyError (LoadError loc str err) = pure $
-    vsep [!(prettyLoc loc),
-          "couldn't load file" <++> text str,
-          text $ show err]
+  prettyError (LoadError loc str err) =
+    vsep [hsep [prettyLoc loc, "couldn't load file", pretty str],
+          fromString $ show err]
 
   prettyError (WrapParseError file err) =
     prettyParseError file err

lib/Quox/Parser/Parser.idr

@@ -287,22 +287,12 @@ termArg fname = withLoc fname $
   <|> [|V qname|]
   <|> const <$> tupleTerm fname
 
-||| optionally, two dimension arguments. if absent default to `@0 @1`
-private
-optDirection : FileName -> Grammar False (PDim, PDim)
-optDirection fname = withLoc fname $ do
-  dims <- optional [|(,) (dimArg fname) (dimArg fname)|]
-  pure $ \loc => fromMaybe (K Zero loc, K One loc) dims
-
 export
 coeTerm : FileName -> Grammar True PTerm
 coeTerm fname = withLoc fname $ do
   resC "coe"
-  mustWork $ do
-    line   <- typeLine fname
-    (p, q) <- optDirection fname
-    val    <- termArg fname
-    pure $ Coe line p q val
+  mustWork [|Coe (typeLine fname) (dimArg fname) (dimArg fname)
+                 (termArg fname)|]
 
 public export
 CompBranch : Type
@@ -311,7 +301,8 @@ CompBranch = (DimConst, PatVar, PTerm)
 export
 compBranch : FileName -> Grammar True CompBranch
 compBranch fname =
-  [|(,,) dimConst (patVar fname) (needRes "⇒" *> assert_total term fname)|]
+  [|(,,) dimConst (patVar fname)
+         (needRes "⇒" *> assert_total term fname)|]
 
 private
 checkCompTermBody : (PatVar, PTerm) -> PDim -> PDim -> PTerm -> PDim ->
@@ -330,7 +321,7 @@ compTerm fname = withLoc fname $ do
   resC "comp"
   mustWork $ do
     a <- typeLine fname
-    (p, q) <- optDirection fname
+    p <- dimArg  fname; q <- dimArg fname
     s <- termArg fname; r <- dimArg fname
     bodyStart <- bounds $ needRes "{"
     s0 <- compBranch fname; needRes ";"

lib/Quox/Pretty.idr

@@ -3,14 +3,15 @@ module Quox.Pretty
 import Quox.Loc
 import Quox.Name
 
-import public Text.PrettyPrint.Bernardy
-import public Text.PrettyPrint.Bernardy.Core.Decorate
-import public Quox.EffExtra
+import public Text.PrettyPrint.Prettyprinter.Doc
+import Text.PrettyPrint.Prettyprinter.Render.String
+import Text.PrettyPrint.Prettyprinter.Render.Terminal
 import public Data.String
-import Control.ANSI.SGR
-
 import Data.DPair
 import Data.SnocList
+
+import public Control.Monad.Identity
+import public Control.Monad.Reader
 import Derive.Prelude
 
 %default total
@@ -20,17 +21,13 @@ import Derive.Prelude
 
 
 public export
-data PPrec
-= Outer
-| Times   -- "_ × _"
-| InTimes -- arguments of ×
-| AnnL    -- left of "∷"
-| Eq      -- "_ ≡ _ : _"
-| InEq    -- arguments of ≡
-  -- ...
-| App  -- term/dimension application
-| Arg  -- argument to nonfix function
-%runElab derive "PPrec" [Eq, Ord, Show]
+record PrettyOpts where
+  constructor MakePrettyOpts
+  unicode, color : Bool
+
+public export
+defPrettyOpts : PrettyOpts
+defPrettyOpts = MakePrettyOpts {unicode = True, color = True}
 
 
 public export
@@ -43,253 +40,254 @@ data HL
 | Tag
 %runElab derive "HL" [Eq, Ord, Show]
 
-
 public export
-data Flavor = Unicode | Ascii
-%runElab derive "Flavor" [Eq, Ord, Show]
-
-export %inline
-noHighlight : HL -> Highlight
-noHighlight _ = MkHighlight "" ""
-
-
-public export
-data EffTag = PREC | FLAVOR | HIGHLIGHT | INDENT
-
-public export
-Pretty : List (Type -> Type)
-Pretty = [StateL PREC PPrec, ReaderL FLAVOR Flavor,
-          ReaderL HIGHLIGHT (HL -> Highlight), ReaderL INDENT Nat]
-
-export %inline
-runPrettyWith : PPrec -> Flavor -> (HL -> Highlight) -> Nat ->
-                Eff Pretty a -> a
-runPrettyWith prec flavor highlight indent act =
-  extract $
-  evalStateAt PREC prec $
-  runReaderAt FLAVOR flavor $
-  runReaderAt HIGHLIGHT highlight $
-  runReaderAt INDENT indent act
+data PPrec
+= Outer
+| AnnR    -- right of "∷"
+| AnnL    -- left  of "∷"
+| Eq      -- "_ ≡ _ : _"
+| InEq    -- arguments of ≡
+| Times   -- "_ × _"
+| InTimes -- arguments of ×
+  -- ...
+| App  -- term/dimension application
+| SApp -- substitution application
+| Arg  -- argument to nonfix function
+%runElab derive "PPrec" [Eq, Ord, Show]
 
 
 export %inline
-toSGR : HL -> List SGR
-toSGR Delim   = []
-toSGR TVar    = [SetForeground BrightYellow]
-toSGR TVarErr = [SetForeground BrightYellow, SetStyle SingleUnderline]
-toSGR Dim     = [SetForeground BrightGreen]
-toSGR DVar    = [SetForeground BrightGreen]
-toSGR DVarErr = [SetForeground BrightGreen, SetStyle SingleUnderline]
-toSGR Qty     = [SetForeground BrightMagenta]
-toSGR Free    = [SetForeground BrightBlue]
-toSGR Syntax  = [SetForeground BrightCyan]
-toSGR Tag     = [SetForeground BrightRed]
+hl : HL -> Doc HL -> Doc HL
+hl = annotate
 
 export %inline
-highlightSGR : HL -> Highlight
-highlightSGR h = MkHighlight (escapeSGR $ toSGR h) (escapeSGR [Reset])
+hl' : HL -> Doc HL -> Doc HL
+hl' h = hl h . unAnnotate
+
+export %inline
+hlF : Functor f => HL -> f (Doc HL) -> f (Doc HL)
+hlF = map . hl
+
+export %inline
+hlF' : Functor f => HL -> f (Doc HL) -> f (Doc HL)
+hlF' = map . hl'
 
 
 export %inline
-runPretty : Eff Pretty a -> a
-runPretty = runPrettyWith Outer Unicode noHighlight 2
+delims : Doc HL -> Doc HL -> Doc HL -> Doc HL
+delims l r doc = hl Delim l <+> doc <+> hl Delim r
 
 export %inline
-runPrettyColor : Eff Pretty a -> a
-runPrettyColor = runPrettyWith Outer Unicode highlightSGR 2
-
+parens : Doc HL -> Doc HL
+parens = delims "(" ")"
 
 export %inline
-hl : {opts : _} -> HL -> Doc opts -> Eff Pretty (Doc opts)
-hl h doc = asksAt HIGHLIGHT $ \f => decorate (f h) doc
+bracks : Doc HL -> Doc HL
+bracks = delims "[" "]"
 
+||| includes spaces inside the braces
+export %inline
+braces : Doc HL -> Doc HL
+braces doc = hl Delim "{" <++> nest 2 doc <++> hl Delim "}"
 
 export %inline
-indentD : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
-indentD doc = pure $ indent !(askAt INDENT) doc
-
-export %inline
-hangD : {opts : _} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
-hangD d1 d2 = pure $ hangSep !(askAt INDENT) d1 d2
-
-export %inline
-hangDSingle : {opts : _} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
-hangDSingle d1 d2 =
-  pure $ ifMultiline (d1 <++> d2) (vappend d1 !(indentD d2))
-
-
-export
-tightDelims : {opts : _} -> (l, r : String) -> (inner : Doc opts) ->
-              Eff Pretty (Doc opts)
-tightDelims l r inner = do
-  l <- hl Delim $ text l
-  r <- hl Delim $ text r
-  pure $ hcat [l, inner, r]
-
-export
-looseDelims : {opts : _} -> (l, r : String) -> (inner : Doc opts) ->
-              Eff Pretty (Doc opts)
-looseDelims l r inner = do
-  l <- hl Delim $ text l
-  r <- hl Delim $ text r
-  let short = hsep [l, inner, r]
-      long  = vsep [l, !(indentD inner), r]
-  pure $ ifMultiline short long
-
-export %inline
-parens : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
-parens = tightDelims "(" ")"
-
-export %inline
-bracks : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
-bracks = tightDelims "[" "]"
-
-export %inline
-braces : {opts : _} -> Doc opts -> Eff Pretty (Doc opts)
-braces = looseDelims "{" "}"
-
-export %inline
-parensIf : {opts : _} -> Bool -> Doc opts -> Eff Pretty (Doc opts)
+parensIf : Bool -> Doc HL -> Doc HL
 parensIf True  = parens
-parensIf False = pure
+parensIf False = id
 
-
-||| uses hsep only if the whole list fits on one line
-export
-sepSingle : {opts : _} -> List (Doc opts) -> Doc opts
-sepSingle xs = ifMultiline (hsep xs) (vsep xs)
-
-export
-fillSep : {opts : _} -> List (Doc opts) -> Doc opts
-fillSep []        = empty
-fillSep (x :: xs) = foldl (\x, y => sep [x, y]) x xs
-
-export
-exceptLast : {opts : _} -> (Doc opts -> Doc opts) ->
-             List (Doc opts) -> List (Doc opts)
-exceptLast f []        = []
-exceptLast f [x]       = [x]
-exceptLast f (x :: xs) = f x :: exceptLast f xs
-
-parameters {opts : LayoutOpts} {auto _ : Foldable t}
-  export
-  separateLoose : Doc opts -> t (Doc opts) -> Doc opts
-  separateLoose d = sep . exceptLast (<++> d) . toList
-
-  export
-  separateTight : Doc opts -> t (Doc opts) -> Doc opts
-  separateTight d = sep . exceptLast (<+> d) . toList
-
-  export
-  fillSeparateTight : Doc opts -> t (Doc opts) -> Doc opts
-  fillSeparateTight d = fillSep . exceptLast (<+> d) . toList
+export %inline
+comma : Doc HL
+comma = hl Delim ","
 
 
 export %inline
-ifUnicode : (uni, asc : Lazy a) -> Eff Pretty a
-ifUnicode uni asc =
-  asksAt FLAVOR $ \case
-    Unicode => uni
-    Ascii   => asc
+asep : List (Doc a) -> Doc a
+asep = align . sep
+
+export
+separate' : Doc a -> List (Doc a) -> List (Doc a)
+separate' s []        = []
+separate' s [x]       = [x]
+separate' s (x :: xs) = x <+> s :: separate' s xs
 
 export %inline
-parensIfM : {opts : _} -> PPrec -> Doc opts -> Eff Pretty (Doc opts)
-parensIfM d doc = parensIf (!(getAt PREC) > d) doc
+separate : Doc a -> List (Doc a) -> Doc a
+separate s = sep . separate' s
 
 export %inline
-withPrec : PPrec -> Eff Pretty a -> Eff Pretty a
-withPrec = localAt_ PREC
-
-
-export
-prettyFree : {opts : _} -> Name -> Eff Pretty (Doc opts)
-prettyFree = hl Free . text . toDots
-
-export
-prettyBind' : BindName -> Doc opts
-prettyBind' = text . baseStr . name
-
-export
-prettyTBind : {opts : _} -> BindName -> Eff Pretty (Doc opts)
-prettyTBind = hl TVar . prettyBind'
-
-export
-prettyDBind : {opts : _} -> BindName -> Eff Pretty (Doc opts)
-prettyDBind = hl DVar . prettyBind'
-
-
+hseparate : Doc a -> List (Doc a) -> Doc a
+hseparate s = hsep . separate' s
 
 export %inline
-typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
-eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
-ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
-  {opts : _} -> Eff Pretty (Doc opts)
-typeD     = hl Syntax . text =<< ifUnicode "★" "Type"
-arrowD    = hl Delim  . text =<< ifUnicode "→" "->"
-darrowD   = hl Delim  . text =<< ifUnicode "⇒" "=>"
-timesD    = hl Delim  . text =<< ifUnicode "×" "**"
-lamD      = hl Syntax . text =<< ifUnicode "λ" "fun"
-eqndD     = hl Delim  . text =<< ifUnicode "≡" "=="
-dlamD     = hl Syntax . text =<< ifUnicode "δ" "dfun"
-annD      = hl Delim  . text =<< ifUnicode "∷" "::"
-natD      = hl Syntax . text =<< ifUnicode "ℕ" "Nat"
-eqD       = hl Syntax $ text "Eq"
-colonD    = hl Delim  $ text ":"
-commaD    = hl Delim  $ text ","
-semiD     = hl Delim  $ text ";"
-caseD     = hl Syntax $ text "case"
-typecaseD = hl Syntax $ text "type-case"
-ofD       = hl Syntax $ text "of"
-returnD   = hl Syntax $ text "return"
-dotD      = hl Delim  $ text "."
-zeroD     = hl Syntax $ text "zero"
-succD     = hl Syntax $ text "succ"
-coeD      = hl Syntax $ text "coe"
-compD     = hl Syntax $ text "comp"
-undD      = hl Syntax $ text "_"
-cstD      = hl Syntax $ text "="
-pipeD     = hl Syntax $ text "|"
+vseparate : Doc a -> List (Doc a) -> Doc a
+vseparate s = vsep . separate' s
+
+export %inline
+aseparate : Doc a -> List (Doc a) -> Doc a
+aseparate s = align . separate s
+
+
+public export
+record PrettyEnv where
+  constructor MakePrettyEnv
+  ||| names of bound dimension variables
+  dnames  : SnocList BaseName
+  ||| names of bound term variables
+  tnames  : SnocList BaseName
+  ||| use non-ascii characters for syntax
+  unicode : Bool
+  ||| surrounding precedence level
+  prec    : PPrec
+
+public export
+HasEnv : (Type -> Type) -> Type
+HasEnv = MonadReader PrettyEnv
+
+export %inline
+ifUnicode : HasEnv m => (uni, asc : Lazy a) -> m a
+ifUnicode uni asc = if (!ask).unicode then [|uni|] else [|asc|]
+
+export %inline
+parensIfM : HasEnv m => PPrec -> Doc HL -> m (Doc HL)
+parensIfM d doc = pure $ parensIf ((!ask).prec > d) doc
+
+export %inline
+withPrec : HasEnv m => PPrec -> m a -> m a
+withPrec d = local {prec := d}
+
+public export data BinderSort = T | D
+
+export %inline
+unders : HasEnv m => BinderSort -> SnocList BaseName -> m a -> m a
+unders T xs = local {prec := Outer, tnames $= (++ xs)}
+unders D xs = local {prec := Outer, dnames $= (++ xs)}
+
+export %inline
+under : HasEnv m => BinderSort -> BaseName -> m a -> m a
+under t x = unders t [< x]
+
+
+public export
+interface PrettyHL a where
+  prettyM : HasEnv m => a -> m (Doc HL)
+
+export %inline
+pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
+pretty0M = local {prec := Outer} . prettyM
+
+export %inline
+runPrettyWith : (unicode : Bool) -> (dnames, tnames : SnocList BaseName) ->
+                Reader PrettyEnv a -> a
+runPrettyWith unicode dnames tnames act =
+  let env = MakePrettyEnv {dnames, tnames, unicode, prec = Outer} in
+  runReader env act
+
+export %inline
+runPretty : (unicode : Bool) -> Reader PrettyEnv a -> a
+runPretty unicode = runPrettyWith unicode [<] [<]
+
+export %inline
+pretty0With : PrettyHL a => (unicode : Bool) ->
+             (dnames, tnames : SnocList BaseName) ->
+             a -> Doc HL
+pretty0With {unicode, dnames, tnames} =
+  runPrettyWith {unicode, dnames, tnames} . prettyM
+
+export %inline
+pretty0 : PrettyHL a => (unicode : Bool) -> a -> Doc HL
+pretty0 unicode = pretty0With unicode [<] [<]
+
+
+
+export PrettyHL BaseName where prettyM = pure . pretty . baseStr
+export PrettyHL Name     where prettyM = pure . pretty . toDots
+export PrettyHL BindName where prettyM = prettyM . name
 
 
 export
-prettyApp : {opts : _} -> Nat -> Doc opts -> List (Doc opts) -> Doc opts
-prettyApp ind f args =
-      hsep (f :: args)
-  <|> hsep [f, vsep args]
-  <|> vsep (f :: map (indent ind) args)
+nameSeq : HL -> List Name -> Doc HL
+nameSeq h = hl h . asep . map (pretty0 False)
 
-export
-prettyAppD : {opts : _} -> Doc opts -> List (Doc opts) -> Eff Pretty (Doc opts)
-prettyAppD f args = pure $ prettyApp !(askAt INDENT) f args
+export %inline
+prettyStr : PrettyHL a => (unicode : Bool) -> a -> String
+prettyStr unicode =
+  let layout = layoutSmart (MkLayoutOptions (AvailablePerLine 80 0.8)) in
+  renderString . layout . pretty0 unicode
 
 
 export
-escapeString : String -> String
-escapeString = concatMap esc1 . unpack where
-  esc1 : Char -> String
-  esc1 '"'  = #"\""#
-  esc1 '\\' = #"\\"#
-  esc1 '\n' = #"\n"#
-  esc1 c    = singleton c
+termHL : HL -> AnsiStyle
+termHL Delim   = neutral
+termHL TVar    = color BrightYellow
+termHL TVarErr = color BrightYellow  <+> underline
+termHL Dim     = color BrightGreen
+termHL DVar    = color BrightGreen
+termHL DVarErr = color BrightGreen   <+> underline
+termHL Qty     = color BrightMagenta
+termHL Free    = color BrightBlue
+termHL Syntax  = color BrightCyan
+termHL Tag     = color BrightRed
+
+export %inline
+prettyIO : PrettyOpts -> PrettyHL a => a -> IO Unit
+prettyIO opts x =
+  let reann = if opts.color then map termHL else unAnnotate in
+  Terminal.putDoc $ reann $ pretty0 opts.unicode x
+
+export %inline
+prettyIODef : PrettyHL a => a -> IO Unit
+prettyIODef = prettyIO defPrettyOpts
+
+
+infixr 6 <%%>, <%>
+export %inline
+(<%%>) : Doc a -> Doc a -> Doc a
+a <%%> b = sep [a, b]
+
+export %inline
+(<%>) : Doc a -> Doc a -> Doc a
+a <%> b = cat [a, b]
+
+
+
+||| wrapper for names that pretty-prints highlighted as a `TVar`.
+public export data TVarName = TV BaseName
+export %inline PrettyHL TVarName where prettyM (TV x) = hlF TVar $ prettyM x
+
+||| wrapper for names that pretty-prints highlighted as a `DVar`.
+public export data DVarName = DV BaseName
+export %inline PrettyHL DVarName where prettyM (DV x) = hlF DVar $ prettyM x
+
 
 export
-quoteTag : String -> String
-quoteTag tag =
-  if isName tag then tag else
-  "\"" ++ escapeString tag ++ "\""
+(forall a. PrettyHL (f a)) => PrettyHL (Exists f) where
+  prettyM x = prettyM x.snd
 
 export
-prettyBounds : {opts : _} -> Bounds -> Eff Pretty (Doc opts)
-prettyBounds (MkBounds l1 c1 l2 c2) =
-  hcat <$> sequence
-    [hl TVar $ text $ show l1, colonD,
-     hl DVar $ text $ show c1, hl Delim "-",
-     hl TVar $ text $ show l2, colonD,
-     hl DVar $ text $ show c2, colonD]
+PrettyHL a => PrettyHL (Subset a b) where
+  prettyM x = prettyM x.fst
+
+public export
+WithPretty : Type -> Type
+WithPretty a = (PrettyHL a, a)
+
+export %inline PrettyHL (WithPretty a) where prettyM x = prettyM $ snd x
+
+export %inline
+epretty : PrettyHL a => a -> Exists WithPretty
+epretty @{p} x = Evidence a (p, x)
+
+
+public export data Lit = L (Doc HL)
+export PrettyHL Lit where prettyM (L doc) = pure doc
+
 
 export
-prettyLoc : {opts : _} -> Loc -> Eff Pretty (Doc opts)
-prettyLoc (L NoLoc) =
-  hcat <$> sequence [hl TVarErr "no location", colonD]
-prettyLoc (L (YesLoc file b)) =
-  hcat <$> sequence [hl Free $ text file, colonD, prettyBounds b]
+prettyLoc : Loc -> Doc HL
+prettyLoc (L NoLoc) = hl TVarErr "no location" <+> hl Delim ":"
+prettyLoc (L (YesLoc file (MkBounds l1 c1 l2 c2))) =
+    hcat [hl Free $ pretty file, hl Delim ":",
+          hl TVar $ pretty l1,   hl Delim ":",
+          hl DVar $ pretty c1,   hl Delim "-",
+          hl TVar $ pretty l2,   hl Delim ":",
+          hl DVar $ pretty c2,   hl Delim ":"]

lib/Quox/Syntax/Dim.idr

@@ -44,15 +44,6 @@ data Dim : Nat -> Type where
 %name Dim.Dim p, q
 %runElab deriveIndexed "Dim" [Eq, Ord, Show]
 
-
-||| `endsOr l r x p` returns `ends l r ε` if `p` is a constant ε, and
-||| `x` otherwise.
-public export
-endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
-endsOr l r x (K e _) = ends l r e
-endsOr l r x (B _ _) = x
-
-
 export
 Located (Dim d) where
   (K _ loc).loc = loc
@@ -64,13 +55,32 @@ Relocatable (Dim d) where
   setLoc loc (B i _) = B i loc
 
 export
-prettyDimConst : {opts : _} -> DimConst -> Eff Pretty (Doc opts)
-prettyDimConst = hl Dim . text . ends "0" "1"
+PrettyHL DimConst where
+  prettyM = pure . hl Dim . ends "0" "1"
 
 export
-prettyDim : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts)
-prettyDim names (K e _) = prettyDimConst e
-prettyDim names (B i _) = prettyDBind $ names !!! i
+PrettyHL (Dim n) where
+  prettyM (K e _) = prettyM e
+  prettyM (B i _) = prettyVar DVar DVarErr (!ask).dnames i
+
+export
+prettyDim : (dnames : NContext d) -> Dim d -> Doc HL
+prettyDim dnames p =
+  let env = MakePrettyEnv {
+    dnames = toSnocList' dnames, tnames = [<],
+    unicode = True, prec = Outer
+  } in
+  runReader env $ prettyM p
+
+
+||| `endsOr l r x e` returns:
+||| - `l` if `p` is `K Zero`;
+||| - `r` if `p` is `K One`;
+||| - `x` otherwise.
+public export
+endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
+endsOr l r x (K e _) = ends l r e
+endsOr l r x (B _ _) = x
 
 
 public export %inline
@@ -83,6 +93,13 @@ DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim
 
 
+export %inline
+prettyDSubst : Pretty.HasEnv m => DSubst from to -> m (Doc HL)
+prettyDSubst th =
+  prettySubstM prettyM (!ask).dnames DVar
+    !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
+
+
 public export FromVar Dim where fromVarLoc = B
 
 

lib/Quox/Syntax/DimEq.idr

@@ -229,37 +229,46 @@ setSelf (B i _)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
 
 
 private
-prettyDVars : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts))
-prettyDVars = traverse prettyDBind . toSnocList'
+prettyDVars : Pretty.HasEnv m => m (SnocList (Doc HL))
+prettyDVars = map (pretty0 False . DV) <$> asks dnames
 
 private
-prettyCst : {opts : _} -> BContext d -> Dim d -> Dim d -> Eff Pretty (Doc opts)
-prettyCst dnames p q =
-  hsep <$> sequence [prettyDim dnames p, cstD, prettyDim dnames q]
-
-private
-prettyCsts : {opts : _} -> BContext d -> DimEq' d ->
-             Eff Pretty (SnocList (Doc opts))
-prettyCsts [<] [<] = pure [<]
-prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
-prettyCsts dnames (eqs :< Just q)  =
-  [|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 noLoc) (weakD 1 q)|]
+prettyCst : (PrettyHL a, PrettyHL b, Pretty.HasEnv m) => a -> b -> m (Doc HL)
+prettyCst p q = do
+  p <- pretty0M p
+  q <- pretty0M q
+  pure $ hsep [p, hl Syntax "=", q]
 
 export
-prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
-prettyDimEq' dnames eqs = do
-  vars <- prettyDVars dnames
-  eqs  <- prettyCsts dnames eqs
-  let prec = if length vars <= 1 && null eqs then Arg else Outer
-  parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
+PrettyHL (DimEq' d) where
+  prettyM eqs {m} = do
+    vars <- prettyDVars
+    eqs  <- go eqs
+    let prec = if length vars <= 1 && null eqs then Arg else Outer
+    parensIfM prec $ align $ fillSep $ punctuate comma $ toList $ vars ++ eqs
+  where
+    tail : SnocList a -> SnocList a
+    tail [<] = [<]
+    tail (xs :< _) = xs
+
+    go : DimEq' d' -> m (SnocList (Doc HL))
+    go [<]              = pure [<]
+    go (eqs :< Nothing) = local {dnames $= tail} $ go eqs
+    go (eqs :< Just p)  = do
+      eq  <- prettyCst (BV {d = 1} 0 noLoc) (weakD 1 p)
+      eqs <- local {dnames $= tail} $ go eqs
+      pure $ eqs :< eq
 
 export
-prettyDimEq : {opts : _} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
-prettyDimEq dnames ZeroIsOne = do
-  vars <- prettyDVars dnames
-  cst  <- prettyCst [<] (K Zero noLoc) (K One noLoc)
-  pure $ separateTight !commaD $ vars :< cst
-prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs
+PrettyHL (DimEq d) where
+  prettyM ZeroIsOne = parensIfM Outer $
+    align $ fillSep $ punctuate comma $ toList $
+    !prettyDVars :< !(prettyCst Zero One)
+  prettyM (C eqs)   = prettyM eqs
+
+export
+prettyDimEq : BContext d -> DimEq d -> Doc HL
+prettyDimEq ds = pretty0With False (toNames ds) [<]
 
 
 public export

lib/Quox/Syntax/Qty.idr

@@ -20,20 +20,35 @@ import Derive.Prelude
 ||| - ω (or #): don't care. an ω variable *can* also be used 0/1 time
 public export
 data Qty = Zero | One | Any
-%runElab derive "Qty" [Eq, Ord, Show]
 %name Qty.Qty pi, rh
 
+%runElab derive "Qty" [Eq, Ord, Show]
+
 
 export
-prettyQty : {opts : _} -> Qty -> Eff Pretty (Doc opts)
-prettyQty Zero = hl Qty $ text "0"
-prettyQty One  = hl Qty $ text "1"
-prettyQty Any  = hl Qty =<< ifUnicode (text "ω") (text "#")
+PrettyHL Qty where
+  prettyM pi = hl Qty <$>
+    case pi of
+      Zero => pure "0"
+      One  => pure "1"
+      Any  => ifUnicode "ω" "#"
 
 ||| prints in a form that can be a suffix of "case"
 public export
-prettySuffix : {opts : _} -> Qty -> Eff Pretty (Doc opts)
-prettySuffix = prettyQty
+prettySuffix : Pretty.HasEnv m => Qty -> m (Doc HL)
+prettySuffix = prettyM
+
+public export
+DecEq Qty where
+  decEq Zero Zero = Yes Refl
+  decEq Zero One  = No $ \case _ impossible
+  decEq Zero Any  = No $ \case _ impossible
+  decEq One  Zero = No $ \case _ impossible
+  decEq One  One  = Yes Refl
+  decEq One  Any  = No $ \case _ impossible
+  decEq Any  Zero = No $ \case _ impossible
+  decEq Any  One  = No $ \case _ impossible
+  decEq Any  Any  = Yes Refl
 
 
 ||| e.g. if in the expression `(s, t)`, the variable `x` is
@@ -68,11 +83,10 @@ compat pi rh  = pi == rh
 
 ||| "π ∨ ρ"
 |||
-||| returns a quantity τ with π ≤ τ and ρ ≤ τ.
-||| if π = ρ, then it's that, otherwise it's ω.
+||| returns some quantity τ where π ≤ τ and ρ ≤ τ, if one exists.
 public export
-lub : Qty -> Qty -> Qty
-lub p q = if p == q then p else Any
+lub : Qty -> Qty -> Maybe Qty
+lub p q = Just $ if p == q then p else Any
 
 
 ||| to maintain subject reduction, only 0 or 1 can occur

lib/Quox/Syntax/Shift.idr

@@ -1,6 +1,7 @@
 module Quox.Syntax.Shift
 
 import public Quox.Syntax.Var
+import Quox.Pretty
 
 import Data.Nat
 import Data.So
@@ -205,6 +206,24 @@ compViaNatCorrect by (SS bz) =
 %transform "Shift.(.)" Shift.(.) = compViaNat
 
 
+||| `prettyShift bnd unicode prec by` pretty-prints the shift `by`, with the
+||| following arguments:
+|||
+||| * `by : Shift from to`
+||| * `bnd : HL` is the highlight used for bound variables of this kind
+||| * `unicode : Bool` is whether to use unicode characters in the output
+||| * `prec : PPrec` is the surrounding precedence level
+export
+prettyShift : Pretty.HasEnv m => (bnd : HL) -> Shift from to -> m (Doc HL)
+prettyShift bnd by =
+  parensIfM Outer $ hsep $
+    [hl bnd   !(ifUnicode "𝑖"  "i"), hl Delim !(ifUnicode "≔" ":="),
+     hl bnd $ !(ifUnicode "𝑖+" "i+") <+> pretty by.nat]
+
+||| prints using the `TVar` highlight for variables
+export PrettyHL (Shift from to) where prettyM = prettyShift TVar
+
+
 infixl 8 //
 public export
 interface CanShift f where

lib/Quox/Syntax/Subst.idr

@@ -3,6 +3,7 @@ module Quox.Syntax.Subst
 import public Quox.Syntax.Shift
 import Quox.Syntax.Var
 import Quox.Name
+import Quox.Pretty
 
 import Data.Nat
 import Data.List
@@ -53,6 +54,11 @@ getLoc (Shift by) i      loc = fromVarLoc (shift by i) loc
 getLoc (t ::: th) VZ     _   = t
 getLoc (t ::: th) (VS i) loc = getLoc th i loc
 
+-- infixl 8 !!
+-- public export
+-- (!!) : FromVar term => Subst term from to -> Var from -> term to
+-- th !! i = getLoc th i noLoc
+
 
 public export
 CanSubstSelf Var where
@@ -124,6 +130,40 @@ one : f n -> Subst f (S n) n
 one x = fromSnocVect [< x]
 
 
+||| `prettySubst pr names bnd op cl th` pretty-prints the substitution `th`,
+||| with the following arguments:
+|||
+||| * `th : Subst f from to`
+||| * `pr : f to -> m (Doc HL)` prints a single element
+||| * `names : List Name` is a list of known bound var names
+||| * `bnd : HL` is the highlight to use for bound variables being subsituted
+||| * `op, cl : Doc HL` are the opening and closing brackets
+export
+prettySubstM : Pretty.HasEnv m =>
+               (pr : f to -> m (Doc HL)) ->
+               (names : SnocList BaseName) -> (bnd : HL) -> (op, cl : Doc HL) ->
+               Subst f from to -> m (Doc HL)
+prettySubstM pr names bnd op cl th =
+  encloseSep (hl Delim op) (hl Delim cl) (hl Delim "; ") <$>
+    withPrec Outer (go 0 th)
+ where
+  go1 : Nat -> f to -> m (Doc HL)
+  go1 i t = pure $ hang 2 $ sep
+    [hsep [!(prettyVar' bnd bnd names i),
+           hl Delim !(ifUnicode "≔" ":=")],
+     !(pr t)]
+
+  go : forall from. Nat -> Subst f from to -> m (List (Doc HL))
+  go _ (Shift SZ) = pure []
+  go _ (Shift by) = [|pure (prettyShift bnd by)|]
+  go i (t ::: th) = [|go1 i t :: go (S i) th|]
+
+||| prints with [square brackets] and the `TVar` highlight for variables
+export
+PrettyHL (f to) => PrettyHL (Subst f from to) where
+  prettyM th = prettySubstM prettyM (!ask).tnames TVar "[" "]" th
+
+
 ||| whether two substitutions with the same codomain have the same shape
 ||| (the same number of terms and the same shift at the end). if so, they
 ||| also have the same domain

lib/Quox/Syntax/Term.idr

@@ -1,6 +1,7 @@
 module Quox.Syntax.Term
 
 import public Quox.Syntax.Term.Base
+import public Quox.Syntax.Term.Split
 import public Quox.Syntax.Term.Subst
 import public Quox.Syntax.Term.Pretty
 import public Quox.Syntax.Term.Tighten

lib/Quox/Syntax/Term/Pretty.idr

@@ -1,539 +1,423 @@
 module Quox.Syntax.Term.Pretty
 
 import Quox.Syntax.Term.Base
+import Quox.Syntax.Term.Split
 import Quox.Syntax.Term.Subst
 import Quox.Context
 import Quox.Pretty
 
 import Data.Vect
-import Derive.Prelude
 
 %default total
-%language ElabReflection
+
+
+export %inline
+typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD :
+  Pretty.HasEnv m => m (Doc HL)
+typeD   = hlF Syntax $ ifUnicode "★" "Type"
+arrowD  = hlF Delim  $ ifUnicode "→" "->"
+darrowD = hlF Delim  $ ifUnicode "⇒" "=>"
+timesD  = hlF Delim  $ ifUnicode "×" "**"
+lamD    = hlF Syntax $ ifUnicode "λ" "fun"
+eqndD   = hlF Delim  $ ifUnicode "≡" "=="
+dlamD   = hlF Syntax $ ifUnicode "δ" "dfun"
+annD    = hlF Delim  $ ifUnicode "∷" "::"
+natD    = hlF Syntax $ ifUnicode "ℕ" "Nat"
+
+export %inline
+eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
+ofD, dotD, zeroD, succD, coeD, compD : Doc HL
+eqD       = hl Syntax "Eq"
+colonD    = hl Delim  ":"
+commaD    = hl Delim  ","
+semiD     = hl Delim  ";"
+caseD     = hl Syntax "case"
+typecaseD = hl Syntax "type-case"
+ofD       = hl Syntax "of"
+returnD   = hl Syntax "return"
+dotD      = hl Delim "."
+zeroD     = hl Syntax "zero"
+succD     = hl Syntax "succ"
+coeD      = hl Syntax "coe"
+compD     = hl Syntax "compD"
 
 
 export
-prettyUniverse : {opts : _} -> Universe -> Eff Pretty (Doc opts)
-prettyUniverse = hl Syntax . text . show
-
-
-export
-prettyTerm : {opts : _} -> BContext d -> BContext n -> Term d n ->
-             Eff Pretty (Doc opts)
-
-export
-prettyElim : {opts : _} -> BContext d -> BContext n -> Elim d n ->
-             Eff Pretty (Doc opts)
-
-private
-BTelescope : Nat -> Nat -> Type
-BTelescope = Telescope' BindName
-
-
-private
-subscript : String -> String
-subscript = pack . map sub . unpack where
+prettyUnivSuffix : Pretty.HasEnv m => Universe -> m (Doc HL)
+prettyUnivSuffix l =
+  ifUnicode (pretty $ pack $ map sub $ unpack $ show l) (pretty l)
+ where
   sub : Char -> Char
   sub c = case c of
     '0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄'
     '5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c
 
-
-private
-PiBind : Nat -> Nat -> Type
-PiBind d n = (Qty, BindName, Term d n)
-
-private
-pbname : PiBind d n -> BindName
-pbname (_, x, _) = x
-
-private
-record SplitPi d n where
-  constructor MkSplitPi
-  binds : Telescope (PiBind d) n inner
-  cod   : Term d inner
-
-private
-splitPi : Telescope (PiBind d) n inner -> Term d inner -> SplitPi d n
-splitPi binds (Pi qty arg res _) =
-  splitPi (binds :< (qty, res.name, arg)) $
-    assert_smaller res $ pushSubsts' res.term
-splitPi binds cod = MkSplitPi {binds, cod}
-
-private
-prettyPiBind1 : {opts : _} ->
-                Qty -> BindName -> BContext d -> BContext n -> Term d n ->
-                Eff Pretty (Doc opts)
-prettyPiBind1 pi (BN Unused _) dnames tnames s =
-  hcat <$> sequence
-    [prettyQty pi, dotD,
-     withPrec Arg $ assert_total prettyTerm dnames tnames s]
-prettyPiBind1 pi x dnames tnames s = hcat <$> sequence
-  [prettyQty pi, dotD,
-   hl Delim $ text "(",
-   hsep <$> sequence
-     [prettyTBind x, hl Delim $ text ":",
-      withPrec Outer $ assert_total prettyTerm dnames tnames s],
-   hl Delim $ text ")"]
-
-private
-prettyPiBinds : {opts : _} ->
-                BContext d -> BContext n ->
-                Telescope (PiBind d) n inner ->
-                Eff Pretty (SnocList (Doc opts))
-prettyPiBinds _ _ [<] = pure [<]
-prettyPiBinds dnames tnames (binds :< (q, x, t)) =
-  let tnames' = tnames . map pbname binds in
-  [|prettyPiBinds dnames tnames binds :<
-    prettyPiBind1 q x dnames tnames' t|]
+export
+prettyUniverse : Universe -> Doc HL
+prettyUniverse = hl Syntax . pretty
 
 
-private
-SigBind : Nat -> Nat -> Type
-SigBind d n = (BindName, Term d n)
+public export
+data WithQty a = MkWithQty Qty a
 
-private
-record SplitSig d n where
-  constructor MkSplitSig
-  binds : Telescope (SigBind d) n inner
-  last  : Term d inner
-
-private
-splitSig : Telescope (SigBind d) n inner -> Term d inner -> SplitSig d n
-splitSig binds (Sig fst snd _) =
-  splitSig (binds :< (snd.name, fst)) $
-    assert_smaller snd $ pushSubsts' snd.term
-splitSig binds last = MkSplitSig {binds, last}
-
-private
-prettySigBind1 : {opts : _} ->
-                 BindName -> BContext d -> BContext n -> Term d n ->
-                 Eff Pretty (Doc opts)
-prettySigBind1 (BN Unused _) dnames tnames s =
-  withPrec InTimes $ assert_total prettyTerm dnames tnames s
-prettySigBind1 x dnames tnames s = hcat <$> sequence
-  [hl Delim $ text "(",
-   hsep <$> sequence
-     [prettyTBind x, hl Delim $ text ":",
-      withPrec Outer $ assert_total prettyTerm dnames tnames s],
-   hl Delim $ text ")"]
-
-private
-prettySigBinds : {opts : _} ->
-                 BContext d -> BContext n ->
-                 Telescope (SigBind d) n inner ->
-                 Eff Pretty (SnocList (Doc opts))
-prettySigBinds _ _ [<] = pure [<]
-prettySigBinds dnames tnames (binds :< (x, t)) =
-  let tnames' = tnames . map fst binds in
-  [|prettySigBinds dnames tnames binds :<
-    prettySigBind1 x dnames tnames' t|]
+export
+PrettyHL a => PrettyHL (WithQty a) where
+  prettyM (MkWithQty q x) = do
+    q <- pretty0M q
+    x <- withPrec Arg $ prettyM x
+    pure $ hcat [q, dotD, x]
 
 
-private
-prettyTypeLine : {opts : _} ->
-                 BContext d -> BContext n ->
-                 DScopeTerm d n ->
-                 Eff Pretty (Doc opts)
-prettyTypeLine dnames tnames (S _ (N body)) =
-  bracks =<< withPrec Outer (prettyTerm dnames tnames body)
-prettyTypeLine dnames tnames (S [< i] (Y body)) =
-  bracks =<< do
-    i'  <- prettyDBind i
-    ty' <- withPrec Outer $ prettyTerm (dnames :< i) tnames body
-    pure $ sep [hsep [i', !darrowD], ty']
+public export
+data Binder a = MkBinder BaseName a
 
-
-private
-data NameSort = T | D
-%runElab derive "NameSort" [Eq]
-
-private
-NameChunks : Type
-NameChunks = SnocList (NameSort, SnocList BindName)
-
-private
-record SplitLams d n where
-  constructor MkSplitLams
-  dnames : BTelescope d dinner
-  tnames : BTelescope n ninner
-  chunks : NameChunks
-  body   : Term dinner ninner
-
-private
-splitLams : Term d n -> SplitLams d n
-splitLams s = go [<] [<] [<] (pushSubsts' s)
-where
-  push : NameSort -> BindName -> NameChunks -> NameChunks
-  push s y [<] = [< (s, [< y])]
-  push s y (xss :< (s', xs)) =
-    if s == s' then xss :< (s', xs :< y)
-    else xss :< (s', xs) :< (s, [< y])
-
-  go : BTelescope d dinner -> BTelescope n ninner ->
-       SnocList (NameSort, SnocList BindName) ->
-       Term dinner ninner -> SplitLams d n
-  go dnames tnames chunks (Lam b _) =
-    go dnames (tnames :< b.name) (push T b.name chunks) $
-       assert_smaller b $ pushSubsts' b.term
-  go dnames tnames chunks (DLam b _) =
-    go (dnames :< b.name) tnames (push D b.name chunks) $
-       assert_smaller b $ pushSubsts' b.term
-  go dnames tnames chunks s =
-    MkSplitLams dnames tnames chunks s
-
-
-private
-splitTuple : SnocList (Term d n) -> Term d n -> SnocList (Term d n)
-splitTuple ss p@(Pair t1 t2 _) =
-  splitTuple (ss :< t1) $ assert_smaller p $ pushSubsts' t2
-splitTuple ss t = ss :< t
-
-
-private
-prettyTArg : {opts : _} -> BContext d -> BContext n ->
-             Term d n -> Eff Pretty (Doc opts)
-prettyTArg dnames tnames s =
-  withPrec Arg $ assert_total prettyTerm dnames tnames s
-
-private
-prettyDArg : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts)
-prettyDArg dnames p =
-  map (text "@" <+>) $ withPrec Arg $ prettyDim dnames p
-
-private
-splitApps : Elim d n -> (Elim d n, List (Either (Dim d) (Term d n)))
-splitApps e = go [] (pushSubsts' e)
-where
-  go : List (Either (Dim d) (Term d n)) -> Elim d n ->
-       (Elim d n, List (Either (Dim d) (Term d n)))
-  go xs e@(App  f s _) =
-    go (Right s :: xs) $ assert_smaller e $ pushSubsts' f
-  go xs e@(DApp f p _) =
-    go (Left  p :: xs) $ assert_smaller e $ pushSubsts' f
-  go xs s = (s, xs)
-
-export FromString (Elim d n) where fromString s = F (fromString s) noLoc
-export FromString (Term d n) where fromString s = FT (fromString s) noLoc
-
-private
-prettyDTApps : {opts : _} ->
-               BContext d -> BContext n ->
-               Elim d n -> List (Either (Dim d) (Term d n)) ->
-               Eff Pretty (Doc opts)
-prettyDTApps dnames tnames f xs = do
-  f  <- withPrec Arg $ assert_total prettyElim dnames tnames f
-  xs <- for xs $ either (prettyDArg dnames) (prettyTArg dnames tnames)
-  parensIfM App =<< prettyAppD f xs
-
-
-private
-record CaseArm opts d n where
-  constructor MkCaseArm
-  pat    : Doc opts
-  dbinds : BTelescope d dinner -- 🍴
-  tbinds : BTelescope n ninner
-  body   : Term dinner ninner
-
-parameters {opts : LayoutOpts} (dnames : BContext d) (tnames : BContext n)
-  private
-  prettyCaseArm : CaseArm opts d n -> Eff Pretty (Doc opts)
-  prettyCaseArm (MkCaseArm pat dbinds tbinds body) = do
-    body <- withPrec Outer $ assert_total
-            prettyTerm (dnames . dbinds) (tnames . tbinds) body
-    header <- (pat <++>) <$> darrowD
-    pure $ hsep [header, body] <|> vsep [header, !(indentD body)]
-
-  private
-  prettyCaseBody : List (CaseArm opts d n) -> Eff Pretty (Doc opts)
-  prettyCaseBody xs =
-    braces . separateTight !semiD =<< traverse prettyCaseArm xs
-
-private
-prettyCompPat : {opts : _} -> DimConst -> BindName -> Eff Pretty (Doc opts)
-prettyCompPat e x = [|prettyDimConst e <++> prettyDBind x|]
-
-private
-layoutComp : {opts : _} ->
-             (typq : List (Doc opts)) -> (val, r : Doc opts) ->
-             (arms : List (Doc opts)) -> Eff Pretty (Doc opts)
-layoutComp typq val r arms = do
-  comp <- compD; lb <- hl Delim "{"; rb <- hl Delim "}"
-  ind  <- askAt INDENT
-  pure $ ifMultiline
-    (hsep $ concat {t = List} [[comp], typq, [val, r, lb], arms, [rb]]) $
-    (comp <++>
-      vsep [sep typq, val, r <++> lb, indent ind $ vsep arms, rb]) <|>
-    (vsep $ (comp ::) $ map (indent ind) $ concat {t = List}
-      [typq, [val, r <++> lb], map (indent ind) arms, [rb]])
+export
+PrettyHL a => PrettyHL (Binder a) where
+  prettyM (MkBinder x ty) = do
+    x  <- pretty0M $ TV x
+    ty <- align <$> pretty0M ty
+    pure $ parens $ sep [hsep [x, colonD], ty]
 
 
 export
-prettyTag : {opts : _} -> String -> Eff Pretty (Doc opts)
-prettyTag tag = hl Tag $ text $ "'" ++ quoteTag tag
+prettyBindType : PrettyHL a => PrettyHL b =>
+                 Pretty.HasEnv m =>
+                 Maybe Qty -> BindName -> a -> Doc HL -> b -> m (Doc HL)
+prettyBindType q (BN x _) s arr t = do
+  bind <- case q of
+    Nothing => pretty0M $ MkBinder x s
+    Just q  => pretty0M $ MkWithQty q $ MkBinder x s
+  t <- withPrec AnnR $ under T x $ prettyM t
+  parensIfM AnnR $ hang 2 $ bind <++> arr <%%> t
 
 export
-prettyEnum : {opts : _} -> List String -> Eff Pretty (Doc opts)
-prettyEnum cases =
-  tightDelims "{" "}" =<<
-  fillSeparateTight !commaD <$>
-  traverse (hl Tag . text . quoteTag) cases
+prettyArm : PrettyHL a => Pretty.HasEnv m =>
+            BinderSort -> SnocList BindName -> Doc HL -> a -> m (Doc HL)
+prettyArm sort xs pat body = do
+  let xs = map name xs
+  body <- withPrec Outer $ unders sort xs $ prettyM body
+  pure $ hang 2 $ sep [pat <++> !darrowD, body]
+
+export
+prettyLams : PrettyHL a => Pretty.HasEnv m =>
+             Maybe (Doc HL) -> BinderSort -> SnocList BindName -> a ->
+             m (Doc HL)
+prettyLams lam sort names body = do
+  let var = case sort of T => TVar; D => DVar
+  header <- sequence $ [hlF var $ prettyM x | x <- toList names]
+  let header = sep $ maybe header (:: header) lam
+  parensIfM Outer =<< prettyArm sort names header body
+
+
+public export
+data TypeLine a = MkTypeLine BindName a
+
+export
+PrettyHL a => PrettyHL (TypeLine a) where
+  prettyM (MkTypeLine i ty) =
+    if i.name == Unused then
+      bracks <$> pretty0M ty
+    else
+      map bracks $ withPrec Outer $ prettyLams Nothing D [< i] ty
+
+
+export
+prettyApps' : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
+              f -> List (Maybe (Doc HL), a) -> m (Doc HL)
+prettyApps' fun args = do
+  fun  <- withPrec App $ prettyM fun
+  args <- traverse prettyArg args
+  parensIfM App $ hang 2 $ sep $ fun :: args
+ where
+  prettyArg : (Maybe (Doc HL), a) -> m (Doc HL)
+  prettyArg (Nothing,  arg) = withPrec Arg (prettyM arg)
+  prettyArg (Just pfx, arg) = (hl Delim pfx <+>) <$> withPrec Arg (prettyM arg)
+
+export
+prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
+             Maybe (Doc HL) -> f -> List a -> m (Doc HL)
+prettyApps pfx f args = prettyApps' f (map (pfx,) args)
+
+export
+prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL)
+prettyTuple = map (parens . align . separate commaD) . traverse prettyM
+
+export
+prettyArms : PrettyHL a => Pretty.HasEnv m =>
+             BinderSort -> List (SnocList BindName, Doc HL, a) -> m (Doc HL)
+prettyArms s =
+  map (braces . aseparate semiD) .
+  traverse (\(xs, l, r) => prettyArm s xs l r)
+
+export
+prettyCase' : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
+              Doc HL -> a -> BindName -> b ->
+              List (SnocList BindName, Doc HL, c) ->
+              m (Doc HL)
+prettyCase' intro elim r ret arms = do
+  elim  <- pretty0M elim
+  ret   <- case r.name of
+    Unused => under T r.name $ pretty0M ret
+    _      => prettyLams Nothing T [< r] ret
+  arms  <- prettyArms T arms
+  pure $ asep [intro <++> elim, returnD <++> ret, ofD <++> arms]
+
+export
+prettyCase : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
+             Qty -> a -> BindName -> b ->
+             List (SnocList BindName, Doc HL, c) ->
+             m (Doc HL)
+prettyCase pi elim r ret arms = do
+  caseq <- (caseD <+>) <$> prettySuffix pi
+  prettyCase' caseq elim r ret arms
+
+export
+escapeString : String -> String
+escapeString = concatMap esc1 . unpack where
+  esc1 : Char -> String
+  esc1 '"'  = #"\""#
+  esc1 '\\' = #"\\"#
+  esc1 '\n' = #"\n"#
+  esc1 c    = singleton c
+
+export
+quoteTag : TagVal -> Doc HL
+quoteTag tag =
+  if isName tag then fromString tag else
+  hcat ["\"", fromString $ escapeString tag, "\""]
+
+export
+prettyTag : TagVal -> Doc HL
+prettyTag t = hl Tag $ "'" <+> quoteTag t
+
+export
+prettyTagBare : TagVal -> Doc HL
+prettyTagBare t = hl Tag $ quoteTag t
+
+export
+prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
+prettyBoxVal val = bracks <$> pretty0M val
+
+export
+prettyCompPat : Pretty.HasEnv m => DimConst -> BindName -> m (Doc HL)
+prettyCompPat e j = hsep <$> sequence [pretty0M e, pretty0M $ DV j.name]
+
+export
+toNatLit : Term d n -> Maybe Nat
+toNatLit (Zero _)   = Just 0
+toNatLit (Succ n _) = [|S $ toNatLit n|]
+toNatLit _          = Nothing
 
 private
-prettyCaseRet : {opts : _} ->
-                BContext d -> BContext n ->
-                ScopeTerm d n -> Eff Pretty (Doc opts)
-prettyCaseRet dnames tnames body = withPrec Outer $ case body of
-  S _     (N tm) => assert_total prettyTerm dnames tnames tm
-  S [< x] (Y tm) => do
-    header <- [|prettyTBind x <++> darrowD|]
-    body   <- assert_total prettyTerm dnames (tnames :< x) tm
-    pure $ hsep [header, body] <|> vsep [header, !(indentD body)]
-
-private
-prettyCase_ : {opts : _} ->
-              BContext d -> BContext n ->
-              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
-  ret  <- prettyCaseRet dnames tnames ret
-  body <- prettyCaseBody dnames tnames body
-  parensIfM Outer $ sep [intro <++> head, !returnD <++> ret, !ofD <++> body]
-
-private
-prettyCase : {opts : _} ->
-             BContext d -> BContext n ->
-             Qty -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
-             Eff Pretty (Doc opts)
-prettyCase dnames tnames qty head ret body =
-  prettyCase_ dnames tnames ![|caseD <+> prettyQty qty|] head ret body
+eterm : Term d n -> Exists (Term d)
+eterm = Evidence n
 
 
-private
-isDefaultDir : Dim d -> Dim d -> Bool
-isDefaultDir (K Zero _) (K One _) = True
-isDefaultDir _ _ = False
+parameters (showSubsts : Bool)
+ mutual
+  export covering
+  [TermSubst] PrettyHL (Term d n) using ElimSubst
+  where
+    prettyM (TYPE l _) =
+      pure $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
+
+    prettyM (Pi qty s (S _ (N t)) _) = do
+      dom <- pretty0M $ MkWithQty qty s
+      cod <- withPrec AnnR $ prettyM t
+      parensIfM AnnR $ asep [dom <++> !arrowD, cod]
+
+    prettyM (Pi qty s (S [< x] (Y t)) _) =
+      prettyBindType (Just qty) x s !arrowD t
+
+    prettyM (Lam (S x t) _) =
+      let GotLams {names, body, _} = getLams' x t.term Refl in
+      prettyLams (Just !lamD) T (toSnocList' names) body
+
+    prettyM (Sig s (S _ (N t)) _) = do
+      s <- withPrec InTimes $ prettyM s
+      t <- withPrec Times   $ prettyM t
+      parensIfM Times $ asep [s <++> !timesD, t]
+
+    prettyM (Sig s (S [< x] (Y t)) _) =
+      prettyBindType Nothing x s !timesD t
+
+    prettyM (Pair s t _) =
+      let GotPairs {init, last, _} = getPairs' [< s] t in
+      prettyTuple $ toList $ init :< last
+
+    prettyM (Enum tags _) =
+      pure $ delims "{" "}" . aseparate comma $ map prettyTagBare $
+        Prelude.toList tags
+
+    prettyM (Tag t _) =
+      pure $ prettyTag t
+
+    prettyM (Eq (S _ (N ty)) l r _) = do
+      l  <- withPrec InEq $ prettyM l
+      r  <- withPrec InEq $ prettyM r
+      ty <- withPrec InEq $ prettyM ty
+      parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty]
+
+    prettyM (Eq (S [< i] (Y ty)) l r _) = do
+      prettyApps Nothing (L eqD)
+        [epretty $ MkTypeLine i ty, epretty l, epretty r]
+
+    prettyM (DLam (S i t) _) =
+      let GotDLams {names, body, _} = getDLams' i t.term Refl in
+      prettyLams (Just !dlamD) D (toSnocList' names) body
+
+    prettyM (Nat _) = natD
+
+    prettyM (Zero _) = pure $ hl Syntax "0"
+
+    prettyM (Succ n _) =
+      case toNatLit n of
+        Just n  => pure $ hl Syntax $ pretty $ S n
+        Nothing => prettyApps Nothing (L succD) [n]
+
+    prettyM (BOX pi ty _) = do
+      pi <- pretty0M pi
+      ty <- pretty0M ty
+      pure $ bracks $ hcat [pi, dotD, align ty]
+
+    prettyM (Box val _) = prettyBoxVal val
+
+    prettyM (E e) = prettyM e
+
+    prettyM (CloT (Sub s th)) =
+      if showSubsts then
+        parensIfM SApp . hang 2 =<<
+          [|withPrec SApp (prettyM s) <%> prettyTSubst th|]
+      else
+        prettyM $ pushSubstsWith' id th s
+
+    prettyM (DCloT (Sub s th)) =
+      if showSubsts then
+        parensIfM SApp . hang 2 =<<
+          [|withPrec SApp (prettyM s) <%> prettyDSubst th|]
+      else
+        prettyM $ pushSubstsWith' th id s
+
+  export covering
+  [ElimSubst] PrettyHL (Elim d n) using TermSubst
+  where
+    prettyM (F x _) =
+      hl' Free <$> prettyM x
+
+    prettyM (B i _) =
+      prettyVar TVar TVarErr (!ask).tnames i
+
+    prettyM (App e s _) =
+      let GotArgs {fun, args, _} = getArgs' e [s] in
+      prettyApps Nothing fun args
+
+    prettyM (CasePair pi p (S [< r] ret) (S [< x, y] body) _) = do
+      pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y]
+      prettyCase pi p r ret.term [([< x, y], pat, body.term)]
+
+    prettyM (CaseEnum pi t (S [< r] ret) arms _) =
+      prettyCase pi t r ret.term
+        [([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
+
+    prettyM (CaseNat pi pi' nat (S [< r] ret) zer (S [< s, ih] suc) _) =
+      prettyCase pi nat r ret.term
+        [([<],       zeroD,    eterm zer),
+         ([< s, ih], !succPat, eterm suc.term)]
+    where
+      succPat : m (Doc HL)
+      succPat = case (ih, pi') of
+        (BN Unused _, Zero) => pure $ succD <++> !(pretty0M s)
+        _ => pure $ asep [succD <++> !(pretty0M s) <+> comma,
+                          !(pretty0M $ MkWithQty pi' ih)]
+
+    prettyM (CaseBox pi box (S [< r] ret) (S [< u] body) _) =
+      prettyCase pi box r ret.term
+        [([< u], !(prettyBoxVal $ TV u.name), body.term)]
+
+    prettyM (DApp e d _) =
+      let GotDArgs {fun, args, _} = getDArgs' e [d] in
+      prettyApps (Just "@") fun args
+
+    prettyM (Ann s a _) = do
+      s <- withPrec AnnL $ prettyM s
+      a <- withPrec AnnR $ prettyM a
+      parensIfM AnnR $ hang 2 $ s <++> !annD <%%> a
+
+    prettyM (Coe (S [< i] ty) p q val _) =
+      let ty = case ty of
+            Y ty => epretty $ MkTypeLine i ty
+            N ty => epretty ty
+      in
+      prettyApps' (L coeD)
+        [(Nothing,  ty),
+         (Just "@", epretty p),
+         (Just "@", epretty q),
+         (Nothing,  epretty val)]
+
+    prettyM (Comp ty p q val r (S [< z] zero) (S [< o] one) _) = do
+      apps <- prettyApps' (L compD)
+        [(Nothing,  epretty $ MkTypeLine (BN Unused noLoc) ty),
+         (Just "@", epretty p),
+         (Just "@", epretty q),
+         (Nothing,  epretty val),
+         (Just "@", epretty r)]
+      arms <- prettyArms D
+        [([< z], !(prettyCompPat Zero z), zero.term),
+         ([< o], !(prettyCompPat One  o), one.term)]
+      pure $ apps <++> arms
+
+    prettyM (TypeCase ty ret arms def _) = do
+      arms <- traverse fromArm (toList arms)
+      prettyCase' typecaseD ty (BN Unused noLoc) ret $
+        arms ++ [([<], hl Syntax "_", eterm def)]
+    where
+      v : BindName -> Doc HL
+      v = pretty0 True . TV . name
+
+      tyCasePat : (k : TyConKind) -> BContext (arity k) -> m (Doc HL)
+      tyCasePat KTYPE [<] = typeD
+      tyCasePat KPi   [< a, b] = pure $ parens $ hsep [v a, !arrowD, v b]
+      tyCasePat KSig  [< a, b] = pure $ parens $ hsep [v a, !arrowD, v b]
+      tyCasePat KEnum [<]   = pure $ hl Syntax "{}"
+      tyCasePat KNat  [<]   = natD
+      tyCasePat KBOX  [< a] = pure $ bracks $ v a
+      tyCasePat KEq   vars  =
+        prettyApps Nothing (L eqD) $ map (TV . name) $ toList' vars
+
+      fromArm : TypeCaseArm d n ->
+                m (SnocList BindName, Doc HL, Exists (Term d))
+      fromArm (k ** S ns t) =
+        pure (toSnocList' ns, !(tyCasePat k ns), eterm t.term)
+
+    prettyM (CloE (Sub e th)) =
+      if showSubsts then
+        parensIfM SApp . hang 2 =<<
+          [|withPrec SApp (prettyM e) <%> prettyTSubst th|]
+      else
+        prettyM $ pushSubstsWith' id th e
+
+    prettyM (DCloE (Sub e th)) =
+      if showSubsts then
+        parensIfM SApp . hang 2 =<<
+          [|withPrec SApp (prettyM e) <%> prettyDSubst th|]
+      else
+        prettyM $ pushSubstsWith' th id e
+
+  export covering
+  prettyTSubst : Pretty.HasEnv m => TSubst d from to -> m (Doc HL)
+  prettyTSubst s =
+    prettySubstM (prettyM @{ElimSubst}) (!ask).tnames TVar "[" "]" s
+
+export covering %inline
+PrettyHL (Term d n) where prettyM = prettyM @{TermSubst False}
+
+export covering %inline
+PrettyHL (Elim d n) where prettyM = prettyM @{ElimSubst False}
 
 
--- [fixme] use telescopes in Scoped
-private
-toTel : BContext s -> BTelescope n (s + n)
-toTel [<]        = [<]
-toTel (ctx :< x) = toTel ctx :< x
-
-private
-prettyTyCasePat : {opts : _} ->
-                  (k : TyConKind) -> BContext (arity k) ->
-                  Eff Pretty (Doc opts)
-prettyTyCasePat KTYPE [<] = typeD
-prettyTyCasePat KPi [< a, b] =
-  parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b]
-prettyTyCasePat KSig [< a, b] =
-  parens . hsep =<< sequence [prettyTBind a, timesD, prettyTBind b]
-prettyTyCasePat KEnum [<] = hl Syntax $ text "{}"
-prettyTyCasePat KEq [< a0, a1, a, l, r] =
-  hsep <$> sequence (eqD :: map prettyTBind [a0, a1, a, l, r])
-prettyTyCasePat KNat [<] = natD
-prettyTyCasePat KBOX [< a] = bracks =<< prettyTBind a
-
-
-prettyLambda : {opts : _} -> BContext d -> BContext n ->
-               Term d n -> Eff Pretty (Doc opts)
-prettyLambda dnames tnames s =
-  parensIfM Outer =<< do
-    let MkSplitLams {dnames = ds, tnames = ts, chunks, body} = splitLams s
-    hangDSingle !(header chunks)
-      !(assert_total prettyTerm (dnames . ds) (tnames . ts) body)
-where
-  introChar : NameSort -> Eff Pretty (Doc opts)
-  introChar T = lamD
-  introChar D = dlamD
-
-  prettyBind : NameSort -> BindName -> Eff Pretty (Doc opts)
-  prettyBind T = prettyTBind
-  prettyBind D = prettyDBind
-
-  header1 : NameSort -> List BindName -> Eff Pretty (Doc opts)
-  header1 s xs = hsep <$> sequence
-    [introChar s, sep <$> traverse (prettyBind s) xs, darrowD]
-
-  header : NameChunks -> Eff Pretty (Doc opts)
-  header cs = sep <$> traverse (\(s, xs) => header1 s (toList xs)) (toList cs)
-
-
-prettyTerm dnames tnames (TYPE l _) =
-  hl Syntax =<<
-    case !(askAt FLAVOR) of
-      Unicode => pure $ text $ "★" ++ subscript (show l)
-      Ascii   => prettyAppD (text "Type") [text $ show l]
-
-prettyTerm dnames tnames (Pi qty arg res _) =
-  parensIfM Outer =<< do
-    let MkSplitPi {binds, cod} = splitPi [< (qty, res.name, arg)] res.term
-    arr   <- arrowD
-    lines <- map (<++> arr) <$> prettyPiBinds dnames tnames binds
-    let tnames = tnames . map pbname binds
-    cod <- withPrec Outer $ prettyTerm dnames tnames (assert_smaller res cod)
-    pure $ sepSingle $ toList $ lines :< cod
-
-prettyTerm dnames tnames s@(Lam {}) =
-  prettyLambda dnames tnames s
-
-prettyTerm dnames tnames (Sig fst snd _) =
-  parensIfM Times =<< do
-    let MkSplitSig {binds, last} = splitSig [< (snd.name, fst)] snd.term
-    times <- timesD
-    lines <- map (<++> times) <$> prettySigBinds dnames tnames binds
-    let tnames = tnames . map Builtin.fst binds
-    last <- withPrec InTimes $
-            prettyTerm dnames tnames (assert_smaller snd last)
-    pure $ sepSingle $ toList $ lines :< last
-
-prettyTerm dnames tnames p@(Pair fst snd _) =
-  parens =<< do
-    let elems = splitTuple [< fst] snd
-    lines <- for elems $ \t =>
-      withPrec Outer $ prettyTerm dnames tnames $ assert_smaller p t
-    pure $ separateTight !commaD lines
-
-prettyTerm dnames tnames (Enum cases _) =
-  prettyEnum $ SortedSet.toList cases
-
-prettyTerm dnames tnames (Tag tag _) =
-  prettyTag tag
-
-prettyTerm dnames tnames (Eq (S _ (N ty)) l r _) = do
-  l  <- withPrec InEq $ prettyTerm dnames tnames l
-  r  <- withPrec InEq $ prettyTerm dnames tnames r
-  ty <- withPrec InEq $ prettyTerm dnames tnames ty
-  pure $ sep [l <++> !eqndD, r <++> !colonD, ty]
-
-prettyTerm dnames tnames (Eq ty l r _) = do
-  ty <- prettyTypeLine dnames tnames ty
-  l  <- withPrec Arg $ prettyTerm dnames tnames l
-  r  <- withPrec Arg $ prettyTerm dnames tnames r
-  prettyAppD !eqD [ty, l, r]
-
-prettyTerm dnames tnames s@(DLam {}) =
-  prettyLambda dnames tnames s
-
-prettyTerm dnames tnames (Nat _) = natD
-prettyTerm dnames tnames (Zero _) = hl Syntax "0"
-prettyTerm dnames tnames (Succ p _) = do
-  succD <- succD
-  let succ : Doc opts -> Eff Pretty (Doc opts)
-      succ t = prettyAppD succD [t]
-      toNat : Term d n -> Eff Pretty (Either (Doc opts) Nat)
-      toNat s with (pushSubsts' s)
-        _ | Zero _   = pure $ Right 0
-        _ | Succ d _ = bitraverse succ (pure . S) =<<
-                       toNat (assert_smaller s d)
-        _ | s'       = map Left . withPrec Arg $
-                       prettyTerm dnames tnames $ assert_smaller s s'
-  either succ (hl Syntax . text . show . S) =<< toNat p
-
-prettyTerm dnames tnames (BOX qty ty _) =
-  bracks . hcat =<<
-    sequence [prettyQty qty, dotD,
-              withPrec Outer $ prettyTerm dnames tnames ty]
-
-prettyTerm dnames tnames (Box val _) =
-  bracks =<< withPrec Outer (prettyTerm dnames tnames val)
-
-prettyTerm dnames tnames (E e) = prettyElim dnames tnames e
-
-prettyTerm dnames tnames t0@(CloT (Sub t ph)) =
-  prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' id ph t
-
-prettyTerm dnames tnames t0@(DCloT (Sub t ph)) =
-  prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' ph id t
-
-prettyElim dnames tnames (F x _) =
-  prettyFree x
-
-prettyElim dnames tnames (B i _) =
-  prettyTBind $ tnames !!! i
-
-prettyElim dnames tnames e@(App {}) =
-  let (f, xs) = splitApps e in
-  prettyDTApps dnames tnames f xs
-
-prettyElim dnames tnames (CasePair qty pair ret body _) = do
-  let [< x, y] = body.names
-  pat <- parens . hsep =<< sequence
-         [[|prettyTBind x <+> commaD|], prettyTBind y]
-  prettyCase dnames tnames qty pair ret
-    [MkCaseArm pat [<] [< x, y] body.term]
-
-prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
-  arms <- for (SortedMap.toList arms) $ \(tag, body) =>
-    pure $ MkCaseArm !(prettyTag tag) [<] [<] body
-  prettyCase dnames tnames qty tag ret arms
-
-prettyElim dnames tnames (CaseNat qty qtyIH nat ret zero succ _) = do
-  let zarm = MkCaseArm !zeroD [<] [<] zero
-      [< p, ih] = succ.names
-  spat0 <- [|succD <++> prettyTBind p|]
-  ihpat0 <- map hcat $ sequence [prettyQty qtyIH, dotD, prettyTBind ih]
-  spat <- if ih.name == Unused
-          then pure spat0
-          else pure $ hsep [spat0 <+> !commaD, ihpat0]
-  let sarm = MkCaseArm spat [<] [< p, ih] succ.term
-  prettyCase dnames tnames qty nat ret [zarm, sarm]
-
-prettyElim dnames tnames (CaseBox qty box ret body _) = do
-  pat <- bracks =<< prettyTBind body.name
-  let arm = MkCaseArm pat [<] [< body.name] body.term
-  prettyCase dnames tnames qty box ret [arm]
-
-prettyElim dnames tnames e@(DApp {}) =
-  let (f, xs) = splitApps e in
-  prettyDTApps dnames tnames f xs
-
-prettyElim dnames tnames (Ann tm ty _) =
-  parensIfM Outer =<<
-    hangDSingle !(withPrec AnnL  [|prettyTerm dnames tnames tm <++> annD|])
-                !(withPrec Outer (prettyTerm dnames tnames ty))
-
-prettyElim dnames tnames (Coe ty p q val _) =
-  parensIfM App =<<
-    if isDefaultDir p q then do
-      ty  <- prettyTypeLine dnames tnames ty
-      val <- prettyTArg dnames tnames val
-      prettyAppD !coeD [ty, val]
-    else do
-      ty  <- prettyTypeLine dnames tnames ty
-      p   <- prettyDArg dnames p
-      q   <- prettyDArg dnames q
-      val <- prettyTArg dnames tnames val
-      prettyAppD !coeD [ty, sep [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
-    pq   <- sep <$> sequence [prettyDArg dnames p, prettyDArg dnames q]
-    val  <- prettyTArg dnames tnames val
-    r    <- prettyDArg dnames r
-    sc   <- semiD
-    arm0 <- map (<+> sc) $ prettyCaseArm dnames tnames $
-      MkCaseArm !(prettyCompPat Zero zero.name) [< zero.name] [<] zero.term
-    arm1 <- prettyCaseArm dnames tnames $
-      MkCaseArm !(prettyCompPat One one.name) [< one.name] [<] one.term
-    ind  <- askAt INDENT
-    if isDefaultDir p q
-       then layoutComp [ty]     val r [arm0, arm1]
-       else layoutComp [ty, pq] val r [arm0, arm1]
-
-prettyElim dnames tnames (TypeCase ty ret arms def _) = do
-  arms <- for (toList arms) $ \(k ** body) => do
-    pat <- prettyTyCasePat k body.names
-    pure $ MkCaseArm pat [<] (toTel body.names) body.term
-  let darm = MkCaseArm !undD [<] [<] def
-  prettyCase_ dnames tnames !typecaseD ty (SN ret) $ arms ++ [darm]
-
-prettyElim dnames tnames e0@(CloE (Sub e ph)) =
-  prettyElim dnames tnames $ assert_smaller e0 $ pushSubstsWith' id ph e
-
-prettyElim dnames tnames e0@(DCloE (Sub e ph)) =
-  prettyElim dnames tnames $ assert_smaller e0 $ pushSubstsWith' ph id e
+export covering
+prettyTerm : (unicode : Bool) ->
+             (dnames : BContext d) -> (tnames : BContext n) ->
+             Term d n -> Doc HL
+prettyTerm unicode dnames tnames term =
+  pretty0With unicode (toNames dnames) (toNames tnames) term

lib/Quox/Syntax/Term/Split.idr

@@ -0,0 +1,251 @@
+module Quox.Syntax.Term.Split
+
+import Quox.Syntax.Term.Base
+import Quox.Syntax.Term.Subst
+import Quox.Syntax.Term.Tighten
+import Quox.Context
+
+import public Quox.No
+import public Data.Vect
+
+%default total
+
+
+public export %inline
+isLam : Term {} -> Bool
+isLam (Lam {}) = True
+isLam _        = False
+
+public export
+0 NotLam : Pred $ Term {}
+NotLam = No . isLam
+
+
+public export %inline
+isDLam : Term {} -> Bool
+isDLam (DLam {}) = True
+isDLam _         = False
+
+public export
+0 NotDLam : Pred $ Term {}
+NotDLam = No . isDLam
+
+
+public export %inline
+isPair : Term {} -> Bool
+isPair (Pair {}) = True
+isPair _         = False
+
+public export
+0 NotPair : Pred $ Term {}
+NotPair = No . isPair
+
+
+public export %inline
+isApp : Elim {} -> Bool
+isApp (App {}) = True
+isApp _        = False
+
+public export
+0 NotApp : Pred $ Elim {}
+NotApp = No . isApp
+
+
+public export %inline
+isDApp : Elim {} -> Bool
+isDApp (DApp {}) = True
+isDApp _         = False
+
+public export
+0 NotDApp : Pred $ Elim {}
+NotDApp = No . isDApp
+
+
+-- infixl 9 :@@
+-- ||| apply multiple arguments at once
+-- public export %inline
+-- (:@@) : Elim d n -> List (Term d n) -> Elim d n
+-- f :@@ ss = foldl app f ss where
+--   app : Elim d n -> Term d n -> Elim d n
+--   app f s = App f s (f.loc `extend'` s.loc.bounds)
+
+public export
+record GetArgs d n where
+  constructor GotArgs
+  fun      : Elim d n
+  args     : List (Term d n)
+  0 notApp : NotApp fun
+
+mutual
+  export %inline
+  getArgs' : Elim d n -> List (Term d n) -> GetArgs d n
+  getArgs' fun0 args =
+    let Element fun nc = pushSubsts fun0 in
+    getArgsNc (assert_smaller fun0 fun) args
+
+  private
+  getArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
+              List (Term d n) -> GetArgs d n
+  getArgsNc fun args = case nchoose $ isApp fun of
+    Left  y => let App f a _ = fun in getArgs' f (a :: args)
+    Right n => GotArgs {fun, args, notApp = n}
+
+||| splits an application into its head and arguments. if it's not an
+||| application then the list is just empty.
+||| looks through substitutions for applications.
+export %inline
+getArgs : Elim d n -> GetArgs d n
+getArgs e = getArgs' e []
+
+
+-- infixl 9 :%%
+-- ||| apply multiple dimension arguments at once
+-- public export %inline
+-- (:%%) : Elim d n -> List (Dim d) -> Elim d n
+-- f :%% ss = foldl dapp f ss where
+--   dapp : Elim d n -> Dim d -> Elim d n
+--   dapp f p = DApp f p (f.loc `extend'` p.loc.bounds)
+
+public export
+record GetDArgs d n where
+  constructor GotDArgs
+  fun       : Elim d n
+  args      : List (Dim d)
+  0 notDApp : NotDApp fun
+
+mutual
+  export %inline
+  getDArgs' : Elim d n -> List (Dim d) -> GetDArgs d n
+  getDArgs' fun0 args =
+    let Element fun nc = pushSubsts fun0 in
+    getDArgsNc (assert_smaller fun0 fun) args
+
+  private
+  getDArgsNc : (e : Elim d n) -> (0 nc : NotClo e) =>
+               List (Dim d) -> GetDArgs d n
+  getDArgsNc fun args = case nchoose $ isDApp fun of
+    Left  y => let DApp f d _ = fun in getDArgs' f (d :: args)
+    Right n => GotDArgs {fun, args, notDApp = n}
+
+||| splits a dimension application into its head and arguments. if it's not an
+||| d application then the list is just empty
+export %inline
+getDArgs : Elim d n -> GetDArgs d n
+getDArgs e = getDArgs' e []
+
+
+-- infixr 1 :\\
+-- public export
+-- absN : BContext m -> Term d (m + n) -> Term d n
+-- absN [<]       s = s
+-- absN (xs :< x) s = absN xs $ Lam (ST [< x] s) ?absloc
+
+-- public export %inline
+-- (:\\) : BContext m -> Term d (m + n) -> Term d n
+-- (:\\) = absN
+
+
+-- infixr 1 :\\%
+-- public export
+-- dabsN : BContext m -> Term (m + d) n -> Term d n
+-- dabsN [<]       s = s
+-- dabsN (xs :< x) s = dabsN xs $ DLam (DST [< x] s) ?dabsLoc
+
+-- public export %inline
+-- (:\\%) : BContext m -> Term (m + d) n -> Term d n
+-- (:\\%) = dabsN
+
+
+public export
+record GetLams d n where
+  constructor GotLams
+  {0 lams, rest : Nat}
+  names    : BContext lams
+  body     : Term d rest
+  0 eq     : lams + n = rest
+  0 notLam : NotLam body
+
+mutual
+  export %inline
+  getLams' : forall lams, rest.
+             BContext lams -> Term d rest -> (0 eq : lams + n = rest) ->
+             GetLams d n
+  getLams' xs s0 eq =
+    let Element s nc = pushSubsts s0 in
+    getLamsNc xs (assert_smaller s0 s) eq
+
+  private
+  getLamsNc : forall lams, rest.
+              BContext lams ->
+              (t : Term d rest) -> (0 nc : NotClo t) =>
+              (0 eq : lams + n = rest) ->
+              GetLams d n
+  getLamsNc xs s Refl = case nchoose $ isLam s of
+    Left  y => let Lam (S [< x] body) _ = s in
+               getLams' (xs :< x) (assert_smaller s body.term) Refl
+    Right n => GotLams xs s Refl n
+
+export %inline
+getLams : Term d n -> GetLams d n
+getLams s = getLams' [<] s Refl
+
+
+public export
+record GetDLams d n where
+  constructor GotDLams
+  {0 lams, rest : Nat}
+  names     : BContext lams
+  body      : Term rest n
+  0 eq      : lams + d = rest
+  0 notDLam : NotDLam body
+
+mutual
+  export %inline
+  getDLams' : forall lams, rest.
+              BContext lams -> Term rest n -> (0 eq : lams + d = rest) ->
+              GetDLams d n
+  getDLams' xs s0 eq =
+    let Element s nc = pushSubsts s0 in
+    getDLamsNc xs (assert_smaller s0 s) eq
+
+  private
+  getDLamsNc : forall lams, rest.
+               BContext lams ->
+               (t : Term rest n) -> (0 nc : NotClo t) =>
+               (0 eq : lams + d = rest) ->
+               GetDLams d n
+  getDLamsNc is s Refl = case nchoose $ isDLam s of
+    Left  y => let DLam (S [< i] body) _ = s in
+               getDLams' (is :< i) (assert_smaller s body.term) Refl
+    Right n => GotDLams is s Refl n
+
+export %inline
+getDLams : Term d n -> GetDLams d n
+getDLams s = getDLams' [<] s Refl
+
+
+public export
+record GetPairs d n where
+  constructor GotPairs
+  init : SnocList $ Term d n
+  last : Term d n
+  notPair : NotPair last
+
+mutual
+  export %inline
+  getPairs' : SnocList (Term d n) -> Term d n -> GetPairs d n
+  getPairs' ss t0 =
+    let Element t nc = pushSubsts t0 in getPairsNc ss (assert_smaller t0 t)
+
+  private
+  getPairsNc : SnocList (Term d n) ->
+               (t : Term d n) -> (0 nc : NotClo t) =>
+               GetPairs d n
+  getPairsNc ss t = case nchoose $ isPair t of
+    Left  y => let Pair s t _ = t in
+               getPairs' (ss :< s) t
+    Right n => GotPairs ss t n
+
+export
+getPairs : Term d n -> GetPairs d n
+getPairs = getPairs' [<]

lib/Quox/Syntax/Term/Subst.idr

@@ -234,10 +234,6 @@ parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
                     tm dfrom from -> tm dto to
   pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
 
-  export %inline
-  pushSubsts' : tm d n -> tm d n
-  pushSubsts' s = fst $ pushSubsts s
-
 mutual
   public export
   isCloT : CloTest Term

lib/Quox/Syntax/Var.idr

@@ -2,6 +2,7 @@ module Quox.Syntax.Var
 
 import public Quox.Loc
 import public Quox.Name
+import Quox.Pretty
 import Quox.OPE
 
 import Data.Nat
@@ -65,6 +66,32 @@ lookupS _     [<]       = Nothing
 lookupS Z     (sx :< x) = Just x
 lookupS (S i) (sx :< x) = lookupS i sx
 
+parameters {auto _ : Pretty.HasEnv m}
+  private
+  prettyIndex : Nat -> m (Doc a)
+  prettyIndex i =
+    ifUnicode (pretty $ pack $ map sup $ unpack $ show i) ("#" <+> pretty i)
+   where
+    sup : Char -> Char
+    sup c = case c of
+      '0' => '⁰'; '1' => '¹'; '2' => '²'; '3' => '³'; '4' => '⁴'
+      '5' => '⁵'; '6' => '⁶'; '7' => '⁷'; '8' => '⁸'; '9' => '⁹'; _ => c
+
+  ||| `prettyVar hlok hlerr names i` pretty prints the de Bruijn index `i`.
+  |||
+  ||| If it is within the bounds of `names`, then it uses the name at that index,
+  ||| highlighted as `hlok`. Otherwise it is just printed as a number highlighted
+  ||| as `hlerr`.
+  export
+  prettyVar' : HL -> HL -> SnocList BaseName -> Nat -> m (Doc HL)
+  prettyVar' hlok hlerr names i =
+    case lookupS i names of
+      Just x  => hlF' hlok $ prettyM x
+      Nothing => pure $ hl hlerr $ "#" <+> pretty i
+
+  export
+  prettyVar : HL -> HL -> SnocList BaseName -> Var n -> m (Doc HL)
+  prettyVar hlok hlerr names i = prettyVar' hlok hlerr names i.nat
 
 public export
 fromNatWith : (i : Nat) -> (0 p : i `LT` n) -> Var n

lib/Quox/Typechecker.idr

@@ -39,15 +39,15 @@ parameters (loc : Loc)
   popQ pi = popQs [< pi]
 
 export
-lubs1 : List1 (QOutput n) -> QOutput n
-lubs1 ([<] ::: _) = [<]
+lubs1 : List1 (QOutput n) -> Maybe (QOutput n)
+lubs1 ([<] ::: _) = Just [<]
 lubs1 ((qs :< p) ::: pqs) =
   let (qss, ps) = unzip $ map unsnoc pqs in
-  lubs1 (qs ::: qss) :< foldl lub p ps
+  [|lubs1 (qs ::: qss) :< foldlM lub p ps|]
 
 export
-lubs : TyContext d n -> List (QOutput n) -> QOutput n
-lubs ctx []        = zeroFor ctx
+lubs : TyContext d n -> List (QOutput n) -> Maybe (QOutput n)
+lubs ctx []        = Just $ zeroFor ctx
 lubs ctx (x :: xs) = lubs1 $ x ::: xs
 
 
@@ -397,9 +397,12 @@ mutual
     unless (ttags == armTags) $ throw $ BadCaseEnum loc ttags armTags
     armres <- for arms $ \(a, s) =>
       checkC ctx sg s $ sub1 ret $ Ann (Tag a s.loc) tres.type s.loc
+    let Just armout = lubs ctx armres
+          | _ => throw $ BadQtys loc "case arms" ctx $
+              zipWith (\qs, (t, rhs) => (qs, Tag t noLoc)) armres arms
     pure $ InfRes {
       type = sub1 ret t,
-      qout = pi * tres.qout + lubs ctx armres
+      qout = pi * tres.qout + armout
     }
 
   infer' ctx sg (CaseNat pi pi' n ret zer suc loc) = do
@@ -471,8 +474,12 @@ mutual
         val1  = val1.term
     qout1 <- check ctx1 sg val1 ty'
     lift $ equal loc (eqDim (B VZ p.loc) p' ctx1) ty' val1 val'
-    let qouts  = qout :: catMaybes [toMaybe qout0, toMaybe qout1]
-    pure $ InfRes {type = ty, qout = lubs ctx qouts}
+    let qout0' = toMaybe $ map (, val0 // one p) qout0
+        qout1' = toMaybe $ map (, val1 // one p) qout1
+        qouts  = (qout, val) :: catMaybes [qout0', qout1']
+    let Just qout = lubs ctx $ map fst qouts
+      | Nothing => throw $ BadQtys loc "composition" ctx qouts
+    pure $ InfRes {type = ty, qout}
 
   infer' ctx sg (TypeCase ty ret arms def loc) = do
     -- if σ = 0

lib/Quox/Typing/Context.idr

@@ -228,38 +228,41 @@ namespace WhnfContext
 
 
 private
-prettyTContextElt : {opts : _} ->
-                    BContext d -> BContext n ->
-                    Qty -> BindName -> Term d n -> Eff Pretty (Doc opts)
-prettyTContextElt dnames tnames q x s =
-  pure $ hsep [hcat [!(prettyQty q), !dotD, !(prettyTBind x)], !colonD,
-               !(withPrec Outer $ prettyTerm dnames tnames s)]
+data CtxBinder a = MkCtxBinder BindName a
 
-private
-prettyTContext' : {opts : _} ->
-                  BContext d -> QContext n -> BContext n ->
-                  TContext d n -> Eff Pretty (SnocList (Doc opts))
-prettyTContext' _ [<] [<] [<] = pure [<]
-prettyTContext' dnames (qtys :< q) (tnames :< x) (tys :< t) =
-  [|prettyTContext' dnames qtys tnames tys :<
-    prettyTContextElt dnames tnames q x t|]
+PrettyHL a => PrettyHL (CtxBinder a) where
+  prettyM (MkCtxBinder x t) = pure $
+    sep [hsep [!(pretty0M $ TV x.name), colonD], !(pretty0M t)]
 
-export
-prettyTContext : {opts : _} ->
-                 BContext d -> QContext n -> BContext n ->
-                 TContext d n -> Eff Pretty (Doc opts)
-prettyTContext dnames qtys tnames tys =
-  separateTight !commaD <$> prettyTContext' dnames qtys tnames tys
+parameters (unicode : Bool)
+  private
+  pipeD : Doc HL
+  pipeD = hl Syntax "|"
 
-export
-prettyTyContext : {opts : _} -> TyContext d n -> Eff Pretty (Doc opts)
-prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
-  case dctx of
-    C [<] => prettyTContext dnames qtys tnames tctx
-    _     => pure $
-      sep [!(prettyDimEq dnames dctx) <++> !pipeD,
-           !(prettyTContext dnames qtys tnames tctx)]
+  export covering
+  prettyTContext : BContext d ->
+                   QContext n -> BContext n ->
+                   TContext d n -> Doc HL
+  prettyTContext ds qs xs ctx = separate comma $ toList $ go qs xs ctx where
+    go : QContext m -> BContext m -> TContext d m -> SnocList (Doc HL)
+    go [<]       [<]       [<] = [<]
+    go (qs :< q) (xs :< x) (ctx :< t) =
+      let bind = MkWithQty q $ MkCtxBinder x t in
+      go qs xs ctx :<
+      runPrettyWith unicode (toNames ds) (toNames xs) (pretty0M bind)
 
-export
-prettyEqContext : {opts : _} -> EqContext n -> Eff Pretty (Doc opts)
-prettyEqContext ctx = prettyTyContext $ toTyContext ctx
+  export covering
+  prettyTyContext : TyContext d n -> Doc HL
+  prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
+    case dctx of
+      C [<] => prettyTContext dnames qtys tnames tctx
+      _     => sep [prettyDimEq dnames dctx <++> pipeD,
+                    prettyTContext dnames qtys tnames tctx]
+
+  export covering
+  prettyEqContext : EqContext n -> Doc HL
+  prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
+    case dassign of
+      [<] => prettyTContext [<] qtys tnames tctx
+      _   => sep [prettyDimEq dnames (fromGround dassign) <++> pipeD,
+                  prettyTContext [<] qtys tnames tctx]

lib/Quox/Typing/Error.idr

@@ -111,50 +111,43 @@ ErrorEff : Type -> Type
 ErrorEff = Except Error
 
 
-export
-Located Error where
-  (ExpectedTYPE    loc _ _).loc       = loc
-  (ExpectedPi      loc _ _).loc       = loc
-  (ExpectedSig     loc _ _).loc       = loc
-  (ExpectedEnum    loc _ _).loc       = loc
-  (ExpectedEq      loc _ _).loc       = loc
-  (ExpectedNat     loc _ _).loc       = loc
-  (ExpectedBOX     loc _ _).loc       = loc
-  (BadUniverse     loc _ _).loc       = loc
-  (TagNotIn        loc _ _).loc       = loc
-  (BadCaseEnum     loc _ _).loc       = loc
-  (BadQtys         loc _ _ _).loc     = loc
-  (ClashT          loc _ _ _ _ _).loc = loc
-  (ClashTy         loc _ _ _ _).loc   = loc
-  (ClashE          loc _ _ _ _).loc   = loc
-  (ClashU          loc _ _ _).loc     = loc
-  (ClashQ          loc _ _).loc       = loc
-  (NotInScope      loc _).loc         = loc
-  (NotType         loc _ _).loc       = loc
-  (WrongType       loc _ _ _).loc     = loc
-  (MissingEnumArm  loc _ _).loc       = loc
-  (WhileChecking   _ _ _ _ err).loc   = err.loc
-  (WhileCheckingTy _ _ _ err).loc     = err.loc
-  (WhileInferring  _ _ _ err).loc     = err.loc
-  (WhileComparingT _ _ _ _ _ err).loc = err.loc
-  (WhileComparingE _ _ _ _ err).loc   = err.loc
+||| whether the error is surrounded in some context
+||| (e.g. "while checking s : A, …")
+public export
+isErrorContext : Error -> Bool
+isErrorContext (WhileChecking   {}) = True
+isErrorContext (WhileCheckingTy {}) = True
+isErrorContext (WhileInferring  {}) = True
+isErrorContext (WhileComparingT {}) = True
+isErrorContext (WhileComparingE {}) = True
+isErrorContext _                    = False
 
+||| remove one layer of context
+export
+peelContext : (e : Error) -> (0 _ : So (isErrorContext e)) =>
+              (Error -> Error, Error)
+peelContext (WhileChecking ctx x s t err) =
+  (WhileChecking ctx x s t, err)
+peelContext (WhileCheckingTy ctx s k err) =
+  (WhileCheckingTy ctx s k, err)
+peelContext (WhileInferring ctx x e err) =
+  (WhileInferring ctx x e, err)
+peelContext (WhileComparingT ctx x s t r err) =
+  (WhileComparingT ctx x s t r, err)
+peelContext (WhileComparingE ctx x e f err) =
+  (WhileComparingE ctx x e f, err)
 
 ||| separates out all the error context layers
 ||| (e.g. "while checking s : A, …")
 export
 explodeContext : Error -> (List (Error -> Error), Error)
-explodeContext (WhileChecking ctx x s t err) =
-  mapFst (WhileChecking ctx x s t ::) $ explodeContext err
-explodeContext (WhileCheckingTy ctx s k err) =
-  mapFst (WhileCheckingTy ctx s k ::) $ explodeContext err
-explodeContext (WhileInferring ctx x e err) =
-  mapFst (WhileInferring ctx x e ::) $ explodeContext err
-explodeContext (WhileComparingT ctx x s t r err) =
-  mapFst (WhileComparingT ctx x s t r ::) $ explodeContext err
-explodeContext (WhileComparingE ctx x e f err) =
-  mapFst (WhileComparingE ctx x e f ::) $ explodeContext err
-explodeContext err = ([], err)
+explodeContext err =
+  case choose $ isErrorContext err of
+    Left y =>
+      let (f,  inner) = peelContext err
+          (fs, root)  = explodeContext $ assert_smaller err inner in
+      (f :: fs, root)
+    Right n => ([], err)
 
 ||| leaves the outermost context layer, and the innermost (up to) n, and removes
 ||| the rest if there are more than n+1 in total
@@ -189,211 +182,190 @@ parameters {auto _ : Has ErrorEff fs} (loc : Loc)
 
 
 private
-prettyMode : EqMode -> String
+prettyMode : EqMode -> Doc HL
 prettyMode Equal = "equal to"
 prettyMode Sub   = "a subtype of"
 prettyMode Super = "a supertype of"
 
 private
-prettyModeU : EqMode -> String
+prettyModeU : EqMode -> Doc HL
 prettyModeU Equal = "equal to"
 prettyModeU Sub   = "less than or equal to"
 prettyModeU Super = "greater than or equal to"
 
 private
-isTypeInUniverse : Maybe Universe -> String
+isTypeInUniverse : Maybe Universe -> Doc HL
 isTypeInUniverse Nothing  = "is a type"
-isTypeInUniverse (Just k) = "is a type in universe \{show k}"
+isTypeInUniverse (Just k) = "is a type in universe" <++> prettyUniverse k
 
+parameters (unicode : Bool)
+  private
+  termn : NameContexts d n -> Term d n -> Doc HL
+  termn ctx = hang 4 . prettyTerm unicode ctx.dnames ctx.tnames
 
-private
-filterSameQtys : BContext n -> List (QOutput n, z) ->
-                 Exists $ \n' => (BContext n', List (QOutput n', z))
-filterSameQtys [<]       qts = Evidence 0 ([<], qts)
-filterSameQtys (ns :< n) qts =
-  let (qs, qts) = unzip $ map (\(qs :< q, t) => (q, qs, t)) qts
-      Evidence l (ns, qts) = filterSameQtys ns qts
-  in
-  if allSame qs
-  then Evidence l (ns, qts)
-  else Evidence (S l) (ns :< n, zipWith (\(qs, t), q => (qs :< q, t)) qts qs)
-where
-  allSame : List Qty -> Bool
-  allSame []        = True
-  allSame (q :: qs) = all (== q) qs
+  private
+  dstermn : {s : Nat} -> NameContexts d n -> DScopeTermN s d n -> Doc HL
+  dstermn ctx (S i t) = termn (extendDimN i ctx) t.term
 
+  private
+  filterSameQtys : BContext n -> List (QOutput n, z) ->
+                   Exists $ \n' => (BContext n', List (QOutput n', z))
+  filterSameQtys [<]       qts = Evidence 0 ([<], qts)
+  filterSameQtys (ns :< n) qts =
+    let (qs, qts) = unzip $ map (\(qs :< q, t) => (q, qs, t)) qts
+        Evidence l (ns, qts) = filterSameQtys ns qts
+    in
+    if allSame qs
+    then Evidence l (ns, qts)
+    else Evidence (S l) (ns :< n, zipWith (\(qs, t), q => (qs :< q, t)) qts qs)
+  where
+    allSame : List Qty -> Bool
+    allSame []        = True
+    allSame (q :: qs) = all (== q) qs
 
-private
-printCaseQtys : {opts : _} -> TyContext d n ->
-                BContext n' -> List (QOutput n', Term d n) ->
-                Eff Pretty (List (Doc opts))
-printCaseQtys ctx ns qts =
-  let Evidence _ (ns, qts) = filterSameQtys ns qts in
-  traverse (line ns) qts
-where
-  line : BContext l -> (QOutput l, Term d n) -> Eff Pretty (Doc opts)
-  line ns (qs, t) = map (("-" <++>) . sep) $ sequence
-    [hangDSingle "the term"
-      !(prettyTerm ctx.dnames ctx.tnames t),
-     hangDSingle "uses variables" $
-      separateTight !commaD $ toSnocList' !(traverse prettyTBind ns),
-     hangDSingle "with quantities" $
-      separateTight !commaD $ toSnocList' !(traverse prettyQty qs)]
+  private
+  printCaseQtys : TyContext d n ->
+                  BContext n' -> List (QOutput n', Term d n) ->
+                  List (Doc HL)
+  printCaseQtys ctx ns qts =
+    let Evidence l (ns, qts) = filterSameQtys ns qts in
+    map (line ns) qts
+  where
+    commaList : PrettyHL a => Context' a l -> Doc HL
+    commaList = hseparate comma . map (pretty0 unicode) . toList'
 
-export
-prettyErrorNoLoc : {opts : _} -> (showContext : Bool) -> Error ->
-                   Eff Pretty (Doc opts)
-prettyErrorNoLoc showContext = \case
-  ExpectedTYPE _ ctx s =>
-    hangDSingle "expected a type universe, but got"
-      !(prettyTerm ctx.dnames ctx.tnames s)
+    line : BContext l -> (QOutput l, Term d n) -> Doc HL
+    line ns (qs, t) =
+      "-" <++> asep ["the term", termn ctx.names t,
+                     "uses variables", commaList $ (TV . name) <$> ns,
+                     "with quantities", commaList qs]
 
-  ExpectedPi _ ctx s =>
-    hangDSingle "expected a function type, but got"
-      !(prettyTerm ctx.dnames ctx.tnames s)
+  -- [todo] only show some contexts, probably
+  export
+  prettyError : (showContext : Bool) -> Error -> Doc HL
+  prettyError showContext = \case
+    ExpectedTYPE loc ctx s =>
+      sep [prettyLoc loc <++> "expected a type universe, but got", termn ctx s]
 
-  ExpectedSig _ ctx s =>
-    hangDSingle "expected a pair type, but got"
-      !(prettyTerm ctx.dnames ctx.tnames s)
+    ExpectedPi loc ctx s =>
+      sep [prettyLoc loc <++> "expected a function type, but got", termn ctx s]
 
-  ExpectedEnum _ ctx s =>
-    hangDSingle "expected an enumeration type, but got"
-      !(prettyTerm ctx.dnames ctx.tnames s)
+    ExpectedSig loc ctx s =>
+      sep [prettyLoc loc <++> "expected a pair type, but got", termn ctx s]
 
-  ExpectedEq _ ctx s =>
-    hangDSingle "expected an enumeration type, but got"
-      !(prettyTerm ctx.dnames ctx.tnames s)
+    ExpectedEnum loc ctx s =>
+      sep [prettyLoc loc <++> "expected an enumeration type, but got",
+           termn ctx s]
 
-  ExpectedNat _ ctx s =>
-    hangDSingle
-      ("expected the type" <++>
-        !(prettyTerm [<] [<] $ Nat noLoc) <+> ", but got")
-      !(prettyTerm ctx.dnames ctx.tnames s)
+    ExpectedEq loc ctx s =>
+      sep [prettyLoc loc <++> "expected an equality type, but got", termn ctx s]
 
-  ExpectedBOX _ ctx s =>
-    hangDSingle "expected a box type, but got"
-      !(prettyTerm ctx.dnames ctx.tnames s)
+    ExpectedNat loc ctx s {d, n} =>
+      sep [prettyLoc loc <++> "expected the type",
+           pretty0 unicode $ Nat noLoc {d, n}, "but got", termn ctx s]
 
-  BadUniverse _ k l => pure $
-    sep ["the universe level" <++> !(prettyUniverse k),
-         "is not strictly less than" <++> !(prettyUniverse l)]
+    ExpectedBOX loc ctx s =>
+      sep [prettyLoc loc <++> "expected a box type, but got", termn ctx s]
 
-  TagNotIn _ tag set =>
-    hangDSingle (hsep ["the tag", !(prettyTag tag), "is not contained in"])
-      !(prettyTerm [<] [<] $ Enum set noLoc)
+    BadUniverse loc k l =>
+      sep [prettyLoc loc <++> "the universe level", prettyUniverse k,
+           "is not strictly less than", prettyUniverse l]
 
-  BadCaseEnum _ head body => sep <$> sequence
-    [hangDSingle "case expression has head of type"
-       !(prettyTerm [<] [<] $ Enum head noLoc),
-     hangDSingle "but cases for"
-       !(prettyTerm [<] [<] $ Enum body noLoc)]
+    TagNotIn loc tag set =>
+      sep [hsep [prettyLoc loc, "tag", prettyTag tag, "is not contained in"],
+           termn empty (Enum set noLoc)]
 
-  BadQtys _ what ctx arms =>
-    hangDSingle (text "inconsistent variable usage in \{what}") $
-      sep !(printCaseQtys ctx ctx.tnames arms)
+    BadCaseEnum loc type arms =>
+      sep [prettyLoc loc <++> "case expression has head of type",
+           termn empty (Enum type noLoc),
+           "but cases for", termn empty (Enum arms noLoc)]
 
-  ClashT _ ctx mode ty s t =>
-    inEContext ctx . sep =<< sequence
-    [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
-     hangDSingle (text "is not \{prettyMode mode}")
-        !(prettyTerm [<] ctx.tnames t),
-     hangDSingle "at type" !(prettyTerm [<] ctx.tnames ty)]
+    BadQtys loc what ctx arms =>
+      hang 4 $ sep $
+        hsep [prettyLoc loc, "inconsistent variable usage in", fromString what]
+          :: printCaseQtys ctx ctx.tnames arms
 
-  ClashTy _ ctx mode a b =>
-    inEContext ctx . sep =<< sequence
-    [hangDSingle "the type" !(prettyTerm [<] ctx.tnames a),
-     hangDSingle (text "is not \{prettyMode mode}")
-        !(prettyTerm [<] ctx.tnames b)]
+    ClashT loc ctx mode ty s t =>
+      inEContext ctx $
+      sep [prettyLoc loc <++> "the term", termn ctx.names0 s,
+           hsep ["is not", prettyMode mode], termn ctx.names0 t,
+           "at type", termn ctx.names0 ty]
 
-  ClashE _ ctx mode e f =>
-    inEContext ctx . sep =<< sequence
-    [hangDSingle "the term" !(prettyElim [<] ctx.tnames e),
-     hangDSingle (text "is not \{prettyMode mode}")
-        !(prettyElim [<] ctx.tnames f)]
+    ClashTy loc ctx mode a b =>
+      inEContext ctx $
+      sep [prettyLoc loc <++> "the type", termn ctx.names0 a,
+           hsep ["is not", prettyMode mode], termn ctx.names0 b]
 
-  ClashU _ mode k l => pure $
-    sep ["the universe level" <++> !(prettyUniverse k),
-         text "is not \{prettyModeU mode}" <++> !(prettyUniverse l)]
+    ClashE loc ctx mode e f =>
+      inEContext ctx $
+      sep [prettyLoc loc <++> "the term", termn ctx.names0 $ E e,
+           hsep ["is not", prettyMode mode], termn ctx.names0 $ E f]
 
-  ClashQ _ pi rh => pure $
-    sep ["the quantity" <++> !(prettyQty pi),
-         "is not equal to" <++> !(prettyQty rh)]
+    ClashU loc mode k l =>
+      sep [prettyLoc loc <++> "the universe level", prettyUniverse k,
+           hsep ["is not", prettyMode mode], prettyUniverse l]
 
-  NotInScope _ x => pure $
-    hsep [!(prettyFree x), "is not in scope"]
+    ClashQ loc pi rh =>
+      sep [prettyLoc loc <++> "the quantity", pretty0 unicode pi,
+           "is not equal to", pretty0 unicode rh]
 
-  NotType _ ctx s =>
-    inTContext ctx . sep =<< sequence
-    [hangDSingle "the term" !(prettyTerm ctx.dnames ctx.tnames s),
-     pure "is not a type"]
+    NotInScope loc x =>
+      hsep [prettyLoc loc, hl' Free $ pretty0 unicode x, "is not in scope"]
 
-  WrongType _ ctx ty s =>
-    inEContext ctx . sep =<< sequence
-    [hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
-     hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)]
+    NotType loc ctx s =>
+      inTContext ctx $
+      sep [prettyLoc loc <++> "the term", termn ctx.names s, "is not a type"]
 
-  MissingEnumArm _ tag tags => pure $
-    sep [hsep ["the tag", !(prettyTag tag), "is not contained in"],
-         !(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)]
+    WrongType loc ctx ty s =>
+      inEContext ctx $
+      sep [prettyLoc loc <++> "the term", termn ctx.names0 s,
+           "cannot have type", termn ctx.names0 ty]
 
-  WhileChecking ctx pi s a err =>
-    [|vappendBlank
-        (inTContext ctx . sep =<< sequence
-          [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s),
-           hangDSingle "has type"       !(prettyTerm ctx.dnames ctx.tnames a),
-           hangDSingle "with quantity"  !(prettyQty pi)])
-        (prettyErrorNoLoc showContext err)|]
+    MissingEnumArm loc tag tags =>
+      sep [hsep [prettyLoc loc, "the tag", hl Tag $ pretty tag,
+                 "is not contained in"],
+           termn empty $ Enum (fromList tags) noLoc]
 
-  WhileCheckingTy ctx a k err =>
-    [|vappendBlank
-        (inTContext ctx . sep =<< sequence
-          [hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames a),
-           pure $ text $ isTypeInUniverse k])
-        (prettyErrorNoLoc showContext err)|]
+    WhileChecking ctx pi s a err =>
+      vsep [inTContext ctx $
+              sep ["while checking", termn ctx.names s,
+                   "has type", termn ctx.names a,
+                   hsep ["with quantity", pretty0 unicode pi]],
+            prettyError showContext err]
 
-  WhileInferring ctx pi e err =>
-    [|vappendBlank
-        (inTContext ctx . sep =<< sequence
-          [hangDSingle "while inferring the type of"
-              !(prettyElim ctx.dnames ctx.tnames e),
-           hangDSingle "with quantity"  !(prettyQty pi)])
-        (prettyErrorNoLoc showContext err)|]
+    WhileCheckingTy ctx a k err =>
+      vsep [inTContext ctx $
+              sep ["while checking", termn ctx.names a,
+                   isTypeInUniverse k],
+            prettyError showContext err]
 
-  WhileComparingT ctx mode a s t err =>
-    [|vappendBlank
-        (inEContext ctx . sep =<< sequence
-          [hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s),
-           hangDSingle (text "is \{prettyMode mode}")
-              !(prettyTerm [<] ctx.tnames t),
-           hangDSingle "at type" !(prettyTerm [<] ctx.tnames a)])
-        (prettyErrorNoLoc showContext err)|]
+    WhileInferring ctx pi e err =>
+      vsep [inTContext ctx $
+              sep ["while inferring the type of", termn ctx.names $ E e,
+                   hsep ["with quantity", pretty0 unicode pi]],
+            prettyError showContext err]
 
-  WhileComparingE ctx mode e f err =>
-    [|vappendBlank
-        (inEContext ctx . sep =<< sequence
-          [hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e),
-           hangDSingle (text "is \{prettyMode mode}")
-              !(prettyElim [<] ctx.tnames f)])
-        (prettyErrorNoLoc showContext err)|]
+    WhileComparingT ctx mode a s t err =>
+      vsep [inEContext ctx $
+              sep ["while checking that", termn ctx.names0 s,
+                   hsep ["is", prettyMode mode], termn ctx.names0 t,
+                   "at type", termn ctx.names0 a],
+            prettyError showContext err]
 
-where
-  vappendBlank : Doc opts -> Doc opts -> Doc opts
-  vappendBlank a b = flush a `vappend` b
+    WhileComparingE ctx mode e f err =>
+      vsep [inEContext ctx $
+              sep ["while checking that", termn ctx.names0 $ E e,
+                   hsep ["is", prettyMode mode], termn ctx.names0 $ E f],
+            prettyError showContext err]
+  where
+    inTContext : TyContext d n -> Doc HL -> Doc HL
+    inTContext ctx doc =
+      if showContext && not (null ctx) then
+        vsep [sep ["in context", prettyTyContext unicode ctx], doc]
+      else doc
 
-  inTContext : TyContext d n -> Doc opts -> Eff Pretty (Doc opts)
-  inTContext ctx doc =
-    if showContext && not (null ctx) then
-      pure $ vappend doc (sep ["in context", !(prettyTyContext ctx)])
-    else pure doc
-
-  inEContext : EqContext n -> Doc opts -> Eff Pretty (Doc opts)
-  inEContext ctx doc =
-    if showContext && not (null ctx) then
-      pure $ vappend doc (sep ["in context", !(prettyEqContext ctx)])
-    else pure doc
-
-export
-prettyError : {opts : _} -> (showContext : Bool) ->
-              Error -> Eff Pretty (Doc opts)
-prettyError showContext err = sep <$> sequence
-  [prettyLoc err.loc, indentD =<< prettyErrorNoLoc showContext err]
+    inEContext : EqContext n -> Doc HL -> Doc HL
+    inEContext ctx doc =
+      if showContext && not (null ctx) then
+        vsep [sep ["in context", prettyEqContext unicode ctx], doc]
+      else doc

lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr

@@ -1,45 +0,0 @@
--- this module has to be called this because a module A.B's private elements are
--- still visible to A.B.C, even if they're in different packages. which i don't
--- think is a good idea but i also don't want to fork prettier over it
-module Text.PrettyPrint.Bernardy.Core.Decorate
-
-import public Text.PrettyPrint.Bernardy.Core
-import Data.DPair
-
-
-public export
-record Highlight where
-  constructor MkHighlight
-  before, after : String
-
-export
-emptyHL : Highlight -> Bool
-emptyHL (MkHighlight before after) = before == "" && after == ""
-
-
--- taken from prettier-ansi
-private
-decorateImpl : Highlight ->
-               (ss : SnocList String) -> (0 _ : NonEmptySnoc ss) =>
-               Subset (SnocList String) NonEmptySnoc
-decorateImpl h [<x]      = Element [< h.before ++ x ++ h.after] %search
-decorateImpl h (sx :< x) = Element (go [] sx :< (x ++ h.after)) %search
-  where
-    go : List String -> SnocList String -> SnocList String
-    go strs [< x]     = [< h.before ++ x] <>< strs
-    go strs (sx :< x) = go (x :: strs) sx
-    go strs [<]       = [<] <>< strs
-
-||| Decorate a `Layout` with the given ANSI codes *without*
-||| changing its stats like width or height.
-export
-decorateLayout : Highlight -> Layout -> Layout
-decorateLayout h l@(MkLayout content stats) =
-  if emptyHL h then l else
-  layout (decorateImpl h content) stats
-
-||| Decorate a `Doc` with the given highlighting *without*
-||| changing its stats like width or height.
-export
-decorate : {opts : _} -> Highlight -> Doc opts -> Doc opts
-decorate h doc = doc >>= \l => pure (decorateLayout h l)

lib/quox-lib.ipkg

@@ -5,10 +5,9 @@ authors   = "rhiannon morris"
 sourceloc = "https://git.rhiannon.website/rhi/quox"
 license   = "acsl"
 
-depends = base, contrib, elab-util, sop, snocvect, eff, prettier
+depends = base, contrib, elab-util, sop, snocvect, eff
 
 modules =
-  Text.PrettyPrint.Bernardy.Core.Decorate,
   Quox.BoolExtra,
   Quox.CharExtra,
   Quox.NatExtra,
@@ -29,6 +28,7 @@ modules =
   Quox.Syntax.Term.Base,
   Quox.Syntax.Term.Tighten,
   Quox.Syntax.Term.Pretty,
+  Quox.Syntax.Term.Split,
   Quox.Syntax.Term.Subst,
   Quox.Syntax.Var,
   Quox.Definition,

pack.toml

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

syntax.ebnf

@@ -54,12 +54,10 @@ dep eq         = "Eq", type line, term arg, term arg.
 succ           = "succ", term arg.
 normal app     = term arg, {term arg | dim arg}.
 
-(* direction defaults to @0 @1 *)
-coe       = "coe", type line, [dim arg, dim arg], term arg.
+coe       = "coe", type line, dim arg, dim arg, term arg.
 type line = "[", [pat var, "⇒"], term, "]".
 
-comp        = "comp", type line, [dim arg, dim arg],
-              term arg, dim arg, comp body.
+comp        = "comp", type line, dim arg, dim arg, term arg, dim arg, comp body.
 comp body   = "{", comp branch, ";", comp branch, [";"], "}".
 comp branch = dim const, name, "⇒", term.
 

tests/PrettyExtra.idr

@@ -10,36 +10,22 @@ squash = pack . squash' . unpack . trim where
   squash' : List Char -> List Char
   squash' [] = []
   squash' (c :: cs) =
-    if isSpace c then ' ' :: squash' (dropWhile isSpace cs)
-    else c :: squash' cs
-
-public export
-Printer : Type -> Type
-Printer a = {opts : _} -> a -> Eff Pretty (Doc opts)
+    if isSpace c then
+      ' ' :: squash' (dropWhile isSpace cs)
+    else
+      c :: squash' cs
 
 export
-renderSquash : ({opts : _} -> Doc opts) -> String
-renderSquash doc = squash $ render (Opts 10000) doc
+renderSquash : Doc HL -> String
+renderSquash doc = squash $ renderShow (layoutCompact doc) ""
 
 export
-prettySquash : Printer a -> Flavor -> a -> String
-prettySquash pr f x =
-  renderSquash $ runPrettyWith Outer f noHighlight 0 (pr x)
-
-export
-testPretty : Printer a -> a -> (uni, asc : String) ->
+testPretty : PrettyHL a => (dnames, tnames : SnocList BaseName) ->
+             a -> (uni, asc : String) ->
              {default uni label : String} -> Test
-testPretty pr t uni asc {label} = test {e = Info} label $ do
+testPretty dnames tnames t uni asc {label} = test {e = Info} label $ do
   let uni  = squash uni; asc = squash asc
-      uni' = prettySquash pr Unicode t
-      asc' = prettySquash pr Ascii t
+      uni' = renderSquash $ pretty0With True  dnames tnames t
+      asc' = renderSquash $ pretty0With False dnames tnames t
   unless (uni == uni') $ Left [("exp", uni), ("got", uni')]
   unless (asc == asc') $ Left [("exp", asc), ("got", asc')]
-
-export
-runPrettyDef : Eff Pretty a -> a
-runPrettyDef = runPrettyWith Outer Unicode noHighlight 0
-
-export
-prettyStr : ({opts : _} -> Eff Pretty (Doc opts)) -> String
-prettyStr doc = render (Opts 60) $ runPrettyDef doc

tests/Tests/DimEq.idr

@@ -16,65 +16,62 @@ import Data.So
 -- [todo] 'set' never breaks existing equalities
 
 private
-prettyDimEq_ : {opts : _} -> {default Arg prec : PPrec} ->
-               BContext d -> DimEq d -> Eff Pretty (Doc opts)
-prettyDimEq_ [<] (C _) = pure "·"
-prettyDimEq_ ds eqs    = prettyDimEq ds eqs
+prettyDimEq' : {default Arg prec : PPrec} -> NContext d -> DimEq d -> Doc HL
+prettyDimEq' [<] (C _) = "·"
+prettyDimEq' ds eqs =
+  runPrettyWith False (toSnocList' ds) [<] $ withPrec prec $ prettyM eqs
 
 private
-testPrettyD : BContext d -> DimEq d -> (str : String) ->
+testPrettyD : NContext d -> DimEq d -> (str : String) ->
               {default str label : String} -> Test
 testPrettyD ds eqs str {label} =
-  testPretty (prettyDimEq ds) eqs str str {label}
+  testPretty (toSnocList' ds) [<] eqs str str {label}
 
 private
-testWf : BContext d -> DimEq d -> Test
+testWf : NContext d -> DimEq d -> Test
 testWf ds eqs =
-  test (prettySquash (prettyDimEq_ ds) Unicode eqs ++ "⊢ ✓") $
+  test (renderSquash $ sep [prettyDimEq' {prec = Outer} ds eqs, "⊢", "✓"]) $
     unless (wf eqs) $ Left ()
 
 private
-testNwf : BContext d -> DimEq d -> Test
+testNwf : NContext d -> DimEq d -> Test
 testNwf ds eqs =
-  test (prettySquash (prettyDimEq_ ds) Unicode eqs ++ "⊢ ✗") $
+  test (renderSquash $ sep [prettyDimEq' {prec = Outer} ds eqs, "⊬", "✓"]) $
     when (wf eqs) $ Left ()
 
 
 private
-testEqLabel : String -> (ds : BContext d) -> (exp, got : DimEq d) -> String
-testEqLabel op ds exp got =
-  renderSquash $ runPrettyDef $ do
-  pure $ sep [!(prettyDimEq_ ds exp), text op, !(prettyDimEq_ ds got)]
+testEqLabel : String -> (ds : NContext d) -> (exp, got : DimEq d) -> String
+testEqLabel op ds exp got = renderSquash $
+  sep [prettyDimEq' ds exp, fromString op, prettyDimEq' ds got]
 
 private
-testNeq : (ds : BContext d) -> (exp, got : DimEq d) ->
+testNeq : (ds : NContext d) -> (exp, got : DimEq d) ->
           {default (testEqLabel "≠" ds exp got) label : String} -> Test
 testNeq {label} ds exp got =
   test label $ unless (exp /= got) $ Left ()
 
 private
-testEq : (ds : BContext d) -> (exp, got : DimEq d) ->
+testEq : (ds : NContext d) -> (exp, got : DimEq d) ->
          {default (testEqLabel "=" ds exp got) label : String} -> Test
 testEq {label} ds exp got =
   test label $ unless (exp == got) $
-    Left [("exp", prettySquash (prettyDimEq_ ds) Unicode exp),
-          ("got", prettySquash (prettyDimEq_ ds) Unicode got)]
+    Left [("exp", renderSquash $ prettyDimEq' ds exp),
+          ("got", renderSquash $ prettyDimEq' ds got)]
 
 private
-testSetLabel : String -> BContext d -> DimEq d ->
+testSetLabel : String -> NContext d -> DimEq d ->
                DimEq d -> List (Dim d, Dim d) -> String
-testSetLabel op ds exp start sets = renderSquash $ runPrettyDef $ do
-  pure $ sep
-    [parens $ sep $ intersperse "/" $
-       !(prettyDimEq_ {prec = Outer} ds start) :: !(traverse prettySet sets),
-     text op, !(prettyDimEq_ ds exp)]
+testSetLabel op ds exp start sets = renderSquash $
+  sep [parens $ sep $ intersperse "/" $
+         prettyDimEq' {prec = Outer} ds start :: map prettySet sets,
+       fromString op, prettyDimEq' ds exp]
 where
-  prettySet : {opts : _} -> (Dim d, Dim d) -> Eff Pretty (Doc opts)
-  prettySet (p, q) = pure $
-    hsep [!(prettyDim ds p), "≔", !(prettyDim ds q)]
+  prettySet : (Dim d, Dim d) -> Doc HL
+  prettySet (p, q) = hsep [prettyDim ds p, "≔", prettyDim ds q]
 
 private
-testSet : (ds : BContext d) -> (exp, start : DimEq d) ->
+testSet : (ds : NContext d) -> (exp, start : DimEq d) ->
           (sets : List (Dim d, Dim d)) ->
           (0 _ : (So (wf start), So (wf exp))) =>
           Test
@@ -83,7 +80,7 @@ testSet ds exp start sets =
     foldl (\eqs, (p, q) => set p q eqs) start sets
 
 private
-ii, iijj, iijjkk, iijjkkll : BContext ?
+ii, iijj, iijjkk, iijjkkll : NContext ?
 ii = [< "𝑖"]
 iijj = [< "𝑖", "𝑗"]
 iijjkk = [< "𝑖", "𝑗", "𝑘"]

tests/Tests/FromPTerm.idr

@@ -7,7 +7,6 @@ import Tests.Parser as TParser
 import Quox.EffExtra
 import TAP
 import AstExtra
-import PrettyExtra
 
 import System.File
 import Derive.Prelude
@@ -30,7 +29,7 @@ ToInfo Failure where
   toInfo (ParseError err) = toInfo err
   toInfo (FromParser err) =
     [("type", "FromParserError"),
-     ("got", prettyStr $ prettyError True err)]
+     ("got", show $ prettyError True True err)]
   toInfo (WrongResult got) =
     [("type", "WrongResult"), ("got", got)]
   toInfo (ExpectedFail got) =

tests/Tests/Parser.idr

@@ -290,8 +290,6 @@ tests = "parser" :- [
       `(Coe (Unused _, V "A" _) (V "p" _) (V "q" _) (V "x" _) _),
     parseMatch term "coe [i ⇒ A] @p @q x"
       `(Coe (PV "i" _, V "A" _) (V "p" _) (V "q" _) (V "x" _) _),
-    parseMatch term "coe [A] x"
-      `(Coe (Unused _, V "A" _) (K Zero _) (K One _) (V "x" _) _),
     parseFails term "coe [A] @p @q",
     parseFails term "coe A @p @q x",
     parseFails term "coe [i ⇒ A] @p q x"
@@ -301,15 +299,9 @@ tests = "parser" :- [
     parseMatch term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
       `(Comp (Unused _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _)
           (PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _),
-    parseMatch term "comp [𝑖 ⇒ A] @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
-      `(Comp (PV "𝑖" _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _)
-          (PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _),
     parseMatch term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 0 𝑘 ⇒ s₁; }"
       `(Comp (Unused _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _)
           (PV "𝑘" _, V "s₁" _) (PV "𝑗" _, V "s₀" _) _),
-    parseMatch term "comp [A] s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
-      `(Comp (Unused _, V "A" _) (K Zero _) (K One _) (V "s" _) (V "r" _)
-          (PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _),
     parseFails term "comp [A] @p @q s @r { 1 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁; }",
     parseFails term "comp [A] @p @q s @r { 0 𝑗 ⇒ s₀ }",
     parseFails term "comp [A] @p @q s @r { }"

tests/Tests/PrettyTerm.idr

@@ -5,11 +5,11 @@ import Quox.Syntax
 import PrettyExtra
 
 
-parameters (ds : BContext d) (ns : BContext n)
+parameters (ds : NContext d) (ns : NContext n)
   testPrettyT : Term d n -> (uni, asc : String) ->
                 {default uni label : String} -> Test
   testPrettyT t uni asc {label} =
-    testPretty (prettyTerm ds ns) t uni asc {label}
+    testPretty (toSnocList' ds) (toSnocList' ns) t uni asc {label}
 
   testPrettyT1 : Term d n -> (str : String) ->
                  {default str label : String} -> Test
@@ -101,8 +101,8 @@ tests = "pretty printing terms" :- [
   ],
 
   "type universes" :- [
-    testPrettyT [<] [<] (^TYPE 0) "★₀" "Type 0",
-    testPrettyT [<] [<] (^TYPE 100) "★₁₀₀" "Type 100"
+    testPrettyT [<] [<] (^TYPE 0) "★₀" "Type0",
+    testPrettyT [<] [<] (^TYPE 100) "★₁₀₀" "Type100"
   ],
 
   "function types" :- [
@@ -117,7 +117,7 @@ tests = "pretty printing terms" :- [
     testPrettyT [<] [<]
       (^PiY Zero "A" (^TYPE 0) (^Arr Any (^BVT 0) (^BVT 0)))
       "0.(A : ★₀) → ω.A → A"
-      "0.(A : Type 0) -> #.A -> A",
+      "0.(A : Type0) -> #.A -> A",
     testPrettyT [<] [<]
       (^Arr Any (^Arr Any (^FT "A") (^FT "A")) (^FT "A"))
       "ω.(ω.A → A) → A"
@@ -130,7 +130,7 @@ tests = "pretty printing terms" :- [
       (^PiY Zero "P" (^Arr Zero (^FT "A") (^TYPE 0))
         (E $ ^App (^BV 0) (^FT "a")))
       "0.(P : 0.A → ★₀) → P a"
-      "0.(P : 0.A -> Type 0) -> P a"
+      "0.(P : 0.A -> Type0) -> P a"
   ],
 
   "pair types" :- [
@@ -190,7 +190,7 @@ tests = "pretty printing terms" :- [
     testPrettyE [<] [<]
       (^CasePair One (^F "a") (SN $ ^TYPE 1) (SN $ ^TYPE 0))
       "case1 a return ★₁ of { (_, _) ⇒ ★₀ }"
-      "case1 a return Type 1 of { (_, _) => Type 0 }",
+      "case1 a return Type1 of { (_, _) => Type0 }",
     testPrettyT [<] [<]
       (^LamY "u" (E $
         ^CaseEnum One (^F "u")
@@ -208,7 +208,7 @@ tests = "pretty printing terms" :- [
       {label = "type-case ℕ ∷ ★₀ return ★₀ of { ⋯ }"}
       (^TypeCase (^Ann (^Nat) (^TYPE 0)) (^TYPE 0) empty (^Nat))
       "type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ }"
-      "type-case Nat :: Type 0 return Type 0 of { _ => Nat }"
+      "type-case Nat :: Type0 return Type0 of { _ => Nat }"
   ],
 
   "annotations" :- [
@@ -231,6 +231,6 @@ tests = "pretty printing terms" :- [
     testPrettyE [<] [<]
       (^Ann (^Arr One (^FT "A") (^FT "A")) (^TYPE 7))
       "(1.A → A) ∷ ★₇"
-      "(1.A -> A) :: Type 7"
+      "(1.A -> A) :: Type7"
   ]
 ]

tests/Tests/Typechecker.idr

@@ -6,7 +6,6 @@ import public TypingImpls
 import TAP
 import Quox.EffExtra
 import AstExtra
-import PrettyExtra
 
 
 %hide Prelude.App
@@ -15,20 +14,20 @@ import PrettyExtra
 
 data Error'
   = TCError Typing.Error
-  | WrongInfer (BContext d) (BContext n) (Term d n) (Term d n)
+  | WrongInfer (Term d n) (Term d n)
   | WrongQOut (QOutput n) (QOutput n)
 
 export
 ToInfo Error' where
   toInfo (TCError e) = toInfo e
-  toInfo (WrongInfer dnames tnames good bad) =
+  toInfo (WrongInfer good bad) =
     [("type", "WrongInfer"),
-     ("wanted", prettyStr $ prettyTerm dnames tnames good),
-     ("got", prettyStr $ prettyTerm dnames tnames bad)]
+     ("wanted", prettyStr True good),
+     ("got", prettyStr True bad)]
   toInfo (WrongQOut good bad) =
     [("type", "WrongQOut"),
-     ("wanted", show good),
-     ("wanted", show bad)]
+     ("wanted", prettyStr True good),
+     ("wanted", prettyStr True bad)]
 
 0 M : Type -> Type
 M = Eff [Except Error', DefsReader]
@@ -117,7 +116,7 @@ parameters (label : String) (act : Lazy (M ()))
 
 inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> M ()
 inferredTypeEq ctx exp got =
-  wrapErr (const $ WrongInfer ctx.dnames ctx.tnames exp got) $ inj $ lift $
+  wrapErr (const $ WrongInfer exp got) $ inj $ lift $
     equalType noLoc ctx exp got
 
 qoutEq : (exp, got : QOutput n) -> M ()

tests/TypingImpls.idr

@@ -3,7 +3,6 @@ module TypingImpls
 import TAP
 import public Quox.Typing
 import public Quox.Pretty
-import PrettyExtra
 
 import Derive.Prelude
 %language ElabReflection
@@ -15,7 +14,4 @@ import Derive.Prelude
 %runElab derive "Error" [Show]
 
 export
-ToInfo Error where
-  toInfo err =
-    let str = render (Opts 60) $ runPrettyDef $ prettyError True err in
-    [("err", str)]
+ToInfo Error where toInfo err = [("err", show $ prettyError True True err)]