From 75ef078b4bfdf3fa719b455b72b34af8519db3f8 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Feb 2023 11:25:11 +0100
Subject: [PATCH] don't print substitutions by default

---
 exe/Main.idr                    |  3 +-
 lib/Quox/Syntax/Term/Pretty.idr | 60 ++++++++++++++++++++++-----------
 2 files changed, 42 insertions(+), 21 deletions(-)

diff --git a/exe/Main.idr b/exe/Main.idr
index f2c0b7a..628c038 100644
--- a/exe/Main.idr
+++ b/exe/Main.idr
@@ -63,5 +63,6 @@ tm =
 main : IO Unit
 main = do
   putStrLn $ banner defPrettyOpts
+  prettyTermDef @{TermSubst True} tm
+  prettyTermDef @{TermSubst True} $ fst $ pushSubsts tm
   prettyTermDef tm
-  prettyTermDef $ pushSubsts tm
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index be3ac34..9defc43 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -94,18 +94,20 @@ prettyTag : TagVal -> Doc HL
 prettyTag t = hl Tag $ "`" <+> fromString t
 
 
-mutual
+parameters (showSubsts : Bool)
+ mutual
   export covering
-  PrettyHL q => PrettyHL (Term q d n) where
+  [TermSubst] PrettyHL q => PrettyHL (Term q d n) using TermSubst ElimSubst
+  where
     prettyM (TYPE l) =
       parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
     prettyM (Pi qty s (S [x] t)) =
-      prettyBindType [qty] x s !arrowD t
+      prettyBindType [qty] x s !arrowD t.term
     prettyM (Lam (S x t)) =
       let GotLams {names, body, _} = getLams' x t.term Refl in
       prettyLams T (toList names) body
     prettyM (Sig s (S [x] t)) =
-      prettyBindType {q} [] x s !timesD t
+      prettyBindType {q} [] x s !timesD t.term
     prettyM (Pair s t) =
       let GotPairs {init, last, _} = getPairs' [< s] t in
       prettyTuple $ toList $ init :< last
@@ -131,14 +133,21 @@ mutual
       prettyLams D (toList names) body
     prettyM (E e) = bracks <$> prettyM e
     prettyM (CloT s th) =
-      parensIfM SApp . hang 2 =<<
-        [|withPrec SApp (prettyM s) </> prettyTSubst th|]
+      if showSubsts then
+        parensIfM SApp . hang 2 =<<
+          [|withPrec SApp (prettyM s) </> prettyTSubst th|]
+      else
+        prettyM $ pushSubstsWith' id th s
     prettyM (DCloT s th) =
-      parensIfM SApp . hang 2 =<<
-        [|withPrec SApp (prettyM s) </> prettyDSubst th|]
+      if showSubsts then
+        parensIfM SApp . hang 2 =<<
+          [|withPrec SApp (prettyM s) </> prettyDSubst th|]
+      else
+        prettyM $ pushSubstsWith' th id s
 
   export covering
-  PrettyHL q => PrettyHL (Elim q d n) where
+  [ElimSubst] PrettyHL q => PrettyHL (Elim q d n) using TermSubst ElimSubst
+  where
     prettyM (F x) =
       hl' Free <$> prettyM x
     prettyM (B i) =
@@ -149,9 +158,9 @@ mutual
     prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do
       pat <- (parens . separate commaD . map (hl TVar)) <$>
              traverse prettyM [x, y]
-      prettyCase pi p r ret [([x, y], pat, body)]
+      prettyCase pi p r ret.term [([x, y], pat, body.term)]
     prettyM (CaseEnum pi t (S [r] ret) arms) =
-      prettyCase pi t r ret
+      prettyCase pi t r ret.term
         [([], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
     prettyM (e :% d) =
       let GotDArgs {fun, args, _} = getDArgs' e [d] in
@@ -161,17 +170,28 @@ mutual
         !(withPrec AnnL $ prettyM s) <++> !annD
           <//> !(withPrec Ann $ prettyM a)
     prettyM (CloE e th)  =
-      parensIfM SApp . hang 2 =<<
-        [|withPrec SApp (prettyM e) </> prettyTSubst th|]
+      if showSubsts then
+        parensIfM SApp . hang 2 =<<
+          [|withPrec SApp (prettyM e) </> prettyTSubst th|]
+      else
+        prettyM $ pushSubstsWith' id th e
     prettyM (DCloE e th) =
-      parensIfM SApp . hang 2 =<<
-        [|withPrec SApp (prettyM e) </> prettyDSubst th|]
-
-  export covering
-  {s : Nat} -> PrettyHL q => PrettyHL (ScopedBody s (Term q d) n) where
-    prettyM body = prettyM body.term
+      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 => PrettyHL q =>
                  TSubst q d from to -> m (Doc HL)
-  prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
+  prettyTSubst s =
+    prettySubstM (prettyM @{ElimSubst}) (!ask).tnames TVar "[" "]" s
+
+export covering %inline
+PrettyHL q => PrettyHL (Term q d n) where
+  prettyM = prettyM @{TermSubst False}
+
+export covering %inline
+PrettyHL q => PrettyHL (Elim q d n) where
+  prettyM = prettyM @{ElimSubst False}