diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2025-03-07 17:21:52 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2025-03-13 13:21:06 +0000 |
| commit | 1ebeb5fd02ed86c2743e15c5b3ca2a489346db4d (patch) | |
| tree | f88834cd7b029343a1ad4a5969258e4022fdd00d /src/Inky/Term/Pretty.idr | |
| parent | f5b75edd91389f0a45045b707abfa36c746e8d54 (diff) | |
Make `foldcase` syntactic sugar.
Diffstat (limited to 'src/Inky/Term/Pretty.idr')
| -rw-r--r-- | src/Inky/Term/Pretty.idr | 15 |
1 files changed, 7 insertions, 8 deletions
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)) |