move pretty stuff for DimEq

lib/Quox/Syntax/DimEq.idr

@@ -4,6 +4,8 @@ import public Quox.Syntax.Var
 import public Quox.Syntax.Dim
 import public Quox.Syntax.Subst
 import public Quox.Context
+import Quox.Pretty
+import Quox.Name
 
 import Data.Maybe
 import Data.Nat
@@ -216,6 +218,49 @@ setSelf (B i)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
   _ | IsGT gt | GT = absurd gt
 
 
+private
+prettyDVars : Pretty.HasEnv m => m (SnocList (Doc HL))
+prettyDVars = map (pretty0 False . DV) <$> asks dnames
+
+private
+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
+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) (weakD p)
+      eqs <- local {dnames $= tail} $ go eqs
+      pure $ eqs :< eq
+
+export
+PrettyHL (DimEq d) where
+  prettyM ZeroIsOne = parensIfM Outer $
+    align $ fillSep $ punctuate comma $ toList $
+    !prettyDVars :< !(prettyCst Zero One)
+  prettyM (C eqs)   = prettyM eqs
+
+export
+prettyDimEq : NContext d -> DimEq d -> Doc HL
+prettyDimEq ds = pretty0With False (toSnocList' ds) [<]
+
+
 public export
 wf' : DimEq' d -> Bool
 wf' [<]                 = True

lib/Quox/Typing/Context.idr

@@ -151,6 +151,10 @@ namespace EqContext
 
 
 parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
+  private
+  pipeD : Doc HL
+  pipeD = hl Syntax "|"
+
   export covering
   prettyTContext : QContext q n -> NContext n -> TContext q d n -> Doc HL
   prettyTContext qs ns ctx = separate comma $ toList $ go qs ns ctx where
@@ -160,41 +164,14 @@ parameters {auto _ : (Eq q, PrettyHL q, IsQty q)} (unicode : Bool)
       let bind = MkWithQty q $ MkBinder x t in
       go qs xs ctx :< runPretty unicode (pretty0M bind)
 
-  private
-  prettyDVars : NContext d -> Doc HL
-  prettyDVars ds = hseparate comma $ map (pretty0 unicode . DV) $ toList' ds
-
-  export
-  prettyDimEq1 : (PrettyHL a, PrettyHL b) => NContext d -> a -> b -> Doc HL
-  prettyDimEq1 ds p q = runPretty unicode $
-    local {dnames := toSnocList' ds} $ do
-      p <- pretty0M p; q <- pretty0M q
-      pure $ hsep [p, hl Syntax "=", q]
-
-  export
-  prettyDimEqCons : NContext d -> DimEq' d -> Doc HL
-  prettyDimEqCons ds eqs = hseparate comma $ toList $ go ds eqs
-  where
-    go : NContext e -> Context (Maybe . Dim) e -> SnocList (Doc HL)
-    go [<]       [<]              = [<]
-    go (ds :< _) (eqs :< Nothing) = go ds eqs
-    go (ds :< x) (eqs :< Just d)  = go ds eqs :< prettyDimEq1 ds (DV x) d
-
-  export
-  prettyDimEq : NContext d -> DimEq d -> Doc HL
-  prettyDimEq ds ZeroIsOne =
-    prettyDVars ds <+> comma <++> prettyDimEq1 [<] Zero One
-  prettyDimEq ds (C eqs) =
-    prettyDVars ds <+> comma <%%> prettyDimEqCons ds eqs
-
   export covering
   prettyTyContext : TyContext q d n -> Doc HL
   prettyTyContext (MkTyContext dctx dnames tctx tnames qtys) =
-    sep [prettyDimEq dnames dctx <++> hl Syntax "|",
+    sep [prettyDimEq dnames dctx <++> pipeD,
          prettyTContext qtys tnames tctx]
 
   export covering
   prettyEqContext : EqContext q n -> Doc HL
   prettyEqContext (MkEqContext dassign dnames tctx tnames qtys) =
-    sep [prettyDimEqCons dnames (fromGround' dassign) <++> hl Syntax "|",
+    sep [prettyDimEq dnames (fromGround dassign) <++> pipeD,
          prettyTContext qtys tnames tctx]