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.idr194
1 files changed, 100 insertions, 94 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index bcc0cb4..36b1b9f 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -11,116 +11,122 @@ import Text.PrettyPrint.Prettyprinter
public export
data Syntax : Type where
- Var : WithBounds String -> Syntax
+ Var : String -> Syntax
-- Sorts
- Sort : Bounds -> Sort -> Syntax
+ Sort : Sort -> Syntax
-- Dependent Products
- Pi : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
- Lambda : Bounds -> WithBounds String -> Syntax -> Syntax
- App : Syntax -> Syntax -> Syntax
+ Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Lambda : WithBounds String -> WithBounds Syntax -> Syntax
+ App : WithBounds Syntax -> WithBounds Syntax -> Syntax
-- Dependent Sums
- Sigma : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
- Pair : Bounds -> Syntax -> Syntax -> Syntax
- Fst : Bounds -> Syntax -> Syntax
- Snd : Bounds -> Syntax -> Syntax
+ Sigma : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Pair : WithBounds Syntax -> WithBounds Syntax -> Syntax
+ Fst : WithBounds Syntax -> Syntax
+ Snd : WithBounds Syntax -> Syntax
-- True
- Top : Bounds -> Syntax
- Point : Bounds -> Syntax
+ Top : Syntax
+ Point : Syntax
-- False
- Bottom : Bounds -> Syntax
- Absurd : Bounds -> Syntax -> Syntax -> Syntax
+ Bottom : Syntax
+ Absurd : WithBounds Syntax -> WithBounds Syntax -> Syntax
-- Equality
- Equal : Bounds -> Syntax -> Syntax -> Syntax
- Refl : Bounds -> Syntax -> Syntax
- Transp : Bounds -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax
- Cast : Bounds -> Syntax -> Syntax -> Syntax -> Syntax
- CastId : Bounds -> 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
+ CastId : WithBounds Syntax -> Syntax
public export
record Definition where
constructor MkDefinition
- bounds : Bounds -- of the name
- name : String
- ty : Syntax
- tm : Syntax
+ name : WithBounds String
+ ty : WithBounds Syntax
+ tm : WithBounds Syntax
-- Pretty Print ----------------------------------------------------------------
+prettyPrec : Prec -> Syntax -> Doc ann
+prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
+
+prettyPrec d (Var var) = pretty var
+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
+prettyPrec d (Lambda var t) =
+ parenthesise (d > Open) $
+ group $
+ backslash <+> pretty var.val <++>
+ pretty "=>" <+> softline <+>
+ prettyPrecBounds Open t
+prettyPrec d (App t u) =
+ parenthesise (d >= App) $
+ group $
+ fillSep [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
+prettyPrec d (Pair t u) =
+ angles $
+ group $
+ neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral
+prettyPrec d (Fst t) =
+ parenthesise (d >= App) $
+ group $
+ fillSep [pretty "fst", prettyPrecBounds App t]
+prettyPrec d (Snd t) =
+ parenthesise (d >= App) $
+ group $
+ fillSep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d Top = pretty "()"
+prettyPrec d Point = pretty "tt"
+prettyPrec d Bottom = pretty "Void"
+prettyPrec d (Absurd a t) =
+ parenthesise (d >= App) $
+ group $
+ fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t]
+prettyPrec d (Equal t u) =
+ parenthesise (d >= Equal) $
+ group $
+ prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> 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) =
+ parenthesise (d >= App) $
+ group $
+ fillSep $
+ [ pretty "transp"
+ , prettyPrecBounds App t
+ , prettyPrecBounds App b
+ , prettyPrecBounds App u
+ , prettyPrecBounds App t'
+ , prettyPrecBounds App e
+ ]
+prettyPrec d (Cast b e t) =
+ parenthesise (d >= App) $
+ group $
+ fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t]
+prettyPrec d (CastId t) =
+ parenthesise (d >= App) $
+ group $
+ fillSep [pretty "castRefl", prettyPrecBounds App t]
+
+prettyPrecBounds d (MkBounded val _ _) = prettyPrec d val
+
export
Pretty Syntax where
- prettyPrec d (Var var) = pretty var.val
- prettyPrec d (Sort _ s) = prettyPrec d s
- prettyPrec d (Pi _ var a b) =
- parenthesise (d > Open) $
- group $
- parens (pretty var.val <++> colon <+> softline <+> prettyPrec Open a) <++>
- pretty "->" <+> softline <+>
- prettyPrec Open b
- prettyPrec d (Lambda _ var t) =
- parenthesise (d > Open) $
- group $
- backslash <+> pretty var.val <++>
- pretty "=>" <+> softline <+>
- prettyPrec Open t
- prettyPrec d (App t u) =
- parenthesise (d >= App) $
- group $
- fillSep [prettyPrec Open t, prettyPrec App u]
- prettyPrec d (Sigma _ var a b) =
- parenthesise (d >= App) $
- group $
- parens (pretty var.val <++> colon <+> softline <+> prettyPrec Open a) <++>
- pretty "**" <+> softline <+>
- prettyPrec Open b
- prettyPrec d (Pair _ t u) =
- angles $
- group $
- neutral <++> prettyPrec Open t <+> comma <+> softline <+> prettyPrec Open u <++> neutral
- prettyPrec d (Fst _ t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "fst", prettyPrec App t]
- prettyPrec d (Snd _ t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "snd", prettyPrec App t]
- prettyPrec d (Top _) = pretty "()"
- prettyPrec d (Point _) = pretty "tt"
- prettyPrec d (Bottom _) = pretty "Void"
- prettyPrec d (Absurd _ a t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
- prettyPrec d (Equal _ t u) =
- parenthesise (d >= Equal) $
- group $
- prettyPrec Equal t <++> pretty "~" <+> softline <+> prettyPrec Equal u
- prettyPrec d (Refl _ t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "refl", prettyPrec App t]
- prettyPrec d (Transp _ t b u t' e) =
- parenthesise (d >= App) $
- group $
- fillSep $
- [ pretty "transp"
- , prettyPrec App t
- , prettyPrec App b
- , prettyPrec App u
- , prettyPrec App t'
- , prettyPrec App e
- ]
- prettyPrec d (Cast _ b e t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "cast", prettyPrec App b, prettyPrec App e, prettyPrec App t]
- prettyPrec d (CastId _ t) =
- parenthesise (d >= App) $
- group $
- fillSep [pretty "castRefl", prettyPrec App t]
+ prettyPrec = Syntax.prettyPrec
export
Pretty Definition where
pretty def = group $
- pretty def.name <++> colon <+> softline <+> pretty def.ty <+> hardline <+>
- pretty def.name <++> equals <+> softline <+> pretty def.tm
+ pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
+ pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:18:27 +0000