summaryrefslogtreecommitdiff
path: root/src/Obs/Syntax.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs/Syntax.idr')
-rw-r--r--src/Obs/Syntax.idr153
1 files changed, 63 insertions, 90 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index d21569a..7bf4b61 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -2,6 +2,7 @@
module Obs.Syntax
import Obs.Sort
+
import Text.Bounded
import Text.PrettyPrint.Prettyprinter
@@ -11,41 +12,34 @@ import Text.PrettyPrint.Prettyprinter
public export
data Syntax : Type where
- Var : String -> Syntax
+ Var : String -> Syntax
-- Sorts
- Sort : Sort -> Syntax
+ Sort : Sort -> Syntax
-- Dependent Products
- Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
Lambda : WithBounds String -> WithBounds Syntax -> Syntax
- App : WithBounds Syntax -> WithBounds Syntax -> Syntax
+ App : WithBounds Syntax -> WithBounds Syntax -> Syntax
-- Dependent Sums
- Sigma : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
- Pair : WithBounds Syntax -> WithBounds Syntax -> Syntax
- Fst : WithBounds Syntax -> Syntax
- Snd : WithBounds Syntax -> Syntax
- -- Disjoint Coproducts
- Sum : WithBounds Syntax -> WithBounds Syntax -> Syntax
- Left : WithBounds Syntax -> Syntax
- Right : WithBounds Syntax -> Syntax
- Case : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
- -- Containers
- Container : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
- MkContainer : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
- Tag : WithBounds Syntax -> Syntax
- Position : WithBounds Syntax -> Syntax
- Next : WithBounds Syntax -> Syntax
- Sem : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Sigma : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Pair : WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Fst : WithBounds Syntax -> Syntax
+ Snd : WithBounds Syntax -> Syntax
+ -- Booleans
+ Bool : Syntax
+ True : Syntax
+ False : Syntax
+ If : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-- True
- Top : Syntax
- Point : Syntax
+ Top : Syntax
+ Point : Syntax
-- False
Bottom : Syntax
- Absurd : WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Absurd : WithBounds Syntax -> Syntax
-- Equality
- Equal : WithBounds Syntax -> WithBounds Syntax -> Syntax
- Refl : WithBounds Syntax -> Syntax
+ Equal : WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Refl : WithBounds Syntax -> Syntax
Transp : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
- Cast : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Cast : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
CastId : WithBounds Syntax -> Syntax
public export
@@ -65,115 +59,94 @@ prettyPrec d (Sort s) = prettyPrec d s
prettyPrec d (Pi var a b) =
parenthesise (d > Open) $
group $
- parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
- pretty "->" <+> softline <+>
- prettyPrecBounds Open b
+ parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
+ pretty "->" <+> line <+>
+ align (prettyPrecBounds Open b)
prettyPrec d (Lambda var t) =
parenthesise (d > Open) $
group $
backslash <+> pretty var.val <++>
- pretty "=>" <+> softline <+>
- prettyPrecBounds Open t
+ pretty "=>" <+> line <+>
+ align (prettyPrecBounds Open t)
prettyPrec d (App t u) =
parenthesise (d >= App) $
group $
- fillSep [prettyPrecBounds Open t, prettyPrecBounds App u]
+ vsep [prettyPrecBounds Open t, prettyPrecBounds App u]
prettyPrec d (Sigma var a b) =
parenthesise (d >= App) $
group $
- parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
- pretty "**" <+> softline <+>
- prettyPrecBounds Open b
+ parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
+ pretty "**" <+> line <+>
+ align (prettyPrecBounds Open b)
prettyPrec d (Pair t u) =
angles $
group $
- neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral
+ neutral <++> prettyPrecBounds Open t <+> comma <+> line <+> prettyPrecBounds Open u <++> neutral
prettyPrec d (Fst t) =
parenthesise (d >= App) $
group $
- fillSep [pretty "fst", prettyPrecBounds App t]
+ vsep [pretty "fst", prettyPrecBounds App t]
prettyPrec d (Snd t) =
parenthesise (d >= App) $
group $
- fillSep [pretty "snd", prettyPrecBounds App t]
-prettyPrec d (Sum a b) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "Either", prettyPrecBounds App a, prettyPrecBounds App b]
-prettyPrec d (Left t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "Left", prettyPrecBounds App t]
-prettyPrec d (Right t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "Right", prettyPrecBounds App t]
-prettyPrec d (Case t s b f g) =
+ vsep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d Bool = pretty "Bool"
+prettyPrec d True = pretty "True"
+prettyPrec d False = pretty "False"
+prettyPrec d (If var a t f g) =
parenthesise (d >= App) $
group $
- fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g]
-prettyPrec d (Container a s s') =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s']
-prettyPrec d (MkContainer t p f) =
- parenthesise (d >= User 0) $
- group $
- fillSep
- [ prettyPrecBounds (User 0) t <++> pretty "<|"
- , prettyPrecBounds (User 0) p <++> pretty "/"
- , prettyPrecBounds (User 0) f
- ]
-prettyPrec d (Tag t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "tag", prettyPrecBounds App t]
-prettyPrec d (Position t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "position", prettyPrecBounds App t]
-prettyPrec d (Next t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "next", prettyPrecBounds App t]
-prettyPrec d (Sem s a t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t]
+ vsep $
+ [ pretty "if"
+ , parens $
+ group $
+ backslash <+> pretty var.val <++>
+ pretty "=>" <+> line <+>
+ align (prettyPrecBounds Open a)
+ , prettyPrecBounds App t
+ , prettyPrecBounds App f
+ , prettyPrecBounds App g
+ ]
prettyPrec d Top = pretty "()"
prettyPrec d Point = pretty "tt"
prettyPrec d Bottom = pretty "Void"
-prettyPrec d (Absurd a t) =
+prettyPrec d (Absurd t) =
parenthesise (d >= App) $
group $
- fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t]
+ vsep [pretty "absurd", prettyPrecBounds App t]
prettyPrec d (Equal t u) =
parenthesise (d >= Equal) $
group $
- prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> prettyPrecBounds Equal u
+ prettyPrecBounds Equal t <++> pretty "~" <+> line <+> prettyPrecBounds Equal u
prettyPrec d (Refl t) =
parenthesise (d >= App) $
group $
- fillSep [pretty "refl", prettyPrecBounds App t]
-prettyPrec d (Transp t b u t' e) =
+ vsep [pretty "refl", prettyPrecBounds App t]
+prettyPrec d (Transp a t u t' e) =
parenthesise (d >= App) $
group $
- fillSep $
+ vsep $
[ pretty "transp"
+ , prettyPrecBounds App a
, prettyPrecBounds App t
- , prettyPrecBounds App b
, prettyPrecBounds App u
, prettyPrecBounds App t'
, prettyPrecBounds App e
]
-prettyPrec d (Cast b e t) =
+prettyPrec d (Cast a b e t) =
parenthesise (d >= App) $
group $
- fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t]
+ vsep $
+ [ pretty "cast"
+ , prettyPrecBounds App a
+ , prettyPrecBounds App b
+ , prettyPrecBounds App e
+ , prettyPrecBounds App t
+ ]
prettyPrec d (CastId t) =
parenthesise (d >= App) $
group $
- fillSep [pretty "castRefl", prettyPrecBounds App t]
+ vsep [pretty "castRefl", prettyPrecBounds App t]
prettyPrecBounds d (MkBounded val _ _) = prettyPrec d val
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:01:11 +0000