From 1ebeb5fd02ed86c2743e15c5b3ca2a489346db4d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 7 Mar 2025 17:21:52 +0000
Subject: Rewrite for flap v2.0.0.

Make `foldcase` syntactic sugar.
---
 src/Inky/Term/Pretty.idr | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'src/Inky/Term/Pretty.idr')

diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index fbedab3..041eb42 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -188,14 +188,6 @@ prettyTerm (Roll _ t) d =
   parenthesise (d < Prefix) $ align $ pretty "~" <+> prettyTerm t Prefix
 prettyTerm (Unroll _ e) d =
   parenthesise (d < Prefix) $ align $ pretty "!" <+> prettyTerm e Prefix
-prettyTerm (Fold _ e ("__tmp" ** Case _ (Var _ ((%%) "__tmp" {pos = Here})) (MkRow ts _))) d =
-  let parts = prettyCases ts <>> [] in
-  -- XXX: should check for usage of "__tmp" in ts
-  group $ align $ hang 2 $ parenthesise (d < Open) $
-    (group $ "foldcase" <++> prettyTerm e Open <++> "by") <+> line <+>
-    (braces $ flatAlt
-      (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
-      (concatWith (surround $ ";" <++> neutral) parts))
 prettyTerm (Fold _ e (x ** t)) d =
   group $ align $ hang 2 $ parenthesise (d < Open) $
     (group $ hang (-2) $ "fold" <++> prettyTerm e Open <++> "by") <+> line <+>
@@ -231,3 +223,10 @@ prettyTerm (Cons _ t u) d =
   group $ align $ hang 2 $ parenthesise (d < App) $
     concatWith (surround line) [pretty "cons", prettyTerm t Suffix, prettyTerm u Suffix]
 prettyTerm (Str _ str) d = enclose "\"" "\"" $ pretty str
+prettyTerm (FoldCase _ e (MkRow ts _)) d =
+  let parts = prettyCases ts <>> [] in
+  group $ align $ hang 2 $ parenthesise (d < Open) $
+    (group $ "foldcase" <++> prettyTerm e Open <++> "by") <+> line <+>
+    (braces $ flatAlt
+      (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+      (concatWith (surround $ ";" <++> neutral) parts))
-- 
cgit v1.2.3