summaryrefslogtreecommitdiff
path: root/src/Obs/Term.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs/Term.idr')
-rw-r--r--src/Obs/Term.idr168
1 files changed, 77 insertions, 91 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 10f2129..422af87 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,41 +12,48 @@ import Text.PrettyPrint.Prettyprinter
public export
data Term : Nat -> Type where
- Var : String -> Fin n -> Term n
+ Var : String -> Fin n -> Term n
-- Sorts
- Sort : Sort -> Term n
+ Sort : Sort -> Term n
-- Dependent Product
- Pi : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
+ Pi : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n
- App : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+ App : WithBounds (Term n) -> WithBounds (Term n) -> Term n
-- Dependent Sums
- Sigma : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
- Pair : WithBounds (Term n) -> WithBounds (Term n) -> Term n
- Fst : WithBounds (Term n) -> Term n
- Snd : WithBounds (Term n) -> Term n
- -- Disjoint Coproducts
- Sum : WithBounds (Term n) -> WithBounds (Term n) -> Term n
- Left : WithBounds (Term n) -> Term n
- Right : WithBounds (Term n) -> Term n
- Case : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
- -- Containers
- Container : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
- MkContainer : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
- Tag : WithBounds (Term n) -> Term n
- Position : WithBounds (Term n) -> Term n
- Next : WithBounds (Term n) -> Term n
- Sem : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+ Sigma : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
+ Pair : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+ Fst : WithBounds (Term n) -> Term n
+ Snd : WithBounds (Term n) -> Term n
+ -- Booleans
+ Bool : Term n
+ True : Term n
+ False : Term n
+ If : WithBounds String ->
+ WithBounds (Term (S n)) ->
+ WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ Term n
-- True
- Top : Term n
- Point : Term n
+ Top : Term n
+ Point : Term n
-- False
Bottom : Term n
- Absurd : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+ Absurd : WithBounds (Term n) -> Term n
-- Equality
- Equal : WithBounds (Term n) -> WithBounds (Term n) -> Term n
- Refl : WithBounds (Term n) -> Term n
- Transp : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
- Cast : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+ Equal : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+ Refl : WithBounds (Term n) -> Term n
+ Transp : WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ Term n
+ Cast : WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ WithBounds (Term n) ->
+ Term n
CastId : WithBounds (Term n) -> Term n
public export
@@ -71,115 +78,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) =
+ 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 "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) =
- 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 > Open) $
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 v _ _) = prettyPrec d v
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:15:45 +0000