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.idr215
1 files changed, 99 insertions, 116 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 578bf83..446fdcb 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,147 +12,130 @@ import Text.PrettyPrint.Prettyprinter
public export
data Term : Nat -> Type where
- Var : WithBounds String -> Fin n -> Term n
+ Var : String -> Fin n -> Term n
-- Sorts
- Sort : Bounds -> Sort -> Term n
+ Sort : Sort -> Term n
-- Dependent Product
- Pi : Bounds -> String -> Term n -> Term (S n) -> Term n
- Lambda : Bounds -> String -> Term (S n) -> Term n
- App : Term n -> Term 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
-- Dependent Sums
- Sigma : Bounds -> String -> Term n -> Term (S n) -> Term n
- Pair : Bounds -> Term n -> Term n -> Term n
- Fst : Bounds -> Term n -> Term n
- Snd : Bounds -> 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
-- True
- Top : Bounds -> Term n
- Point : Bounds -> Term n
+ Top : Term n
+ Point : Term n
-- False
- Bottom : Bounds -> Term n
- Absurd : Bounds -> Term n -> Term n -> Term n
+ Bottom : Term n
+ Absurd : WithBounds (Term n) -> WithBounds (Term n) -> Term n
-- Equality
- Equal : Bounds -> Term n -> Term n -> Term n
- Refl : Bounds -> Term n -> Term n
- Transp : Bounds -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
- Cast : Bounds -> Term n -> Term n -> Term n -> Term n
- CastId : Bounds -> 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) -> Term n
+ CastId : WithBounds (Term n) -> Term n
public export
record Definition (n : Nat) where
constructor MkDefinition
- bounds : Bounds -- of the name
- name : String
- ty : Term n
- tm : Term n
+ name : WithBounds String
+ ty : WithBounds (Term n)
+ tm : WithBounds (Term n)
public export
data Block : Nat -> Type where
Nil : Block 0
(:<) : Block n -> Definition n -> Block (S n)
--- Operations ------------------------------------------------------------------
+-- Pretty Print ----------------------------------------------------------------
-export
-fullBounds : Term n -> WithBounds (Term n)
-fullBounds tm@(Var var i) = map (\_ => tm) var
-fullBounds tm@(Sort x s) = MkBounded tm False x
-fullBounds tm@(Pi x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
-fullBounds tm@(Lambda x var t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(App t u) = map (\_ => tm) (mergeBounds (fullBounds t) (fullBounds u))
-fullBounds tm@(Sigma x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
-fullBounds tm@(Pair x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
-fullBounds tm@(Fst x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Snd x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Top x) = MkBounded tm False x
-fullBounds tm@(Point x) = MkBounded tm False x
-fullBounds tm@(Bottom x) = MkBounded tm False x
-fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
-fullBounds tm@(Equal x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
-fullBounds tm@(Refl x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Transp x t b u t' e) = mergeBounds (mergeBounds (mergeBounds (fullBounds t) (fullBounds b)) (mergeBounds (fullBounds u) (fullBounds t'))) (mergeBounds (fullBounds e) (MkBounded tm False x))
-fullBounds tm@(Cast x b e t) = mergeBounds (mergeBounds (fullBounds b) (fullBounds e)) (mergeBounds (fullBounds t) (MkBounded tm False x))
-fullBounds tm@(CastId x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+prettyPrec : Prec -> Term n -> Doc ann
+prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann
--- Pretty Print ----------------------------------------------------------------
+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 > Open) $
+ 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 v _ _) = prettyPrec d v
export
Pretty (Term n) 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 <++> colon <+> softline <+> prettyPrec Open a) <++>
- pretty "->" <+> softline <+>
- prettyPrec Open b
- prettyPrec d (Lambda _ var t) =
- parenthesise (d > Open) $
- group $
- backslash <+> pretty var <++>
- 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 <++> 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 > Open) $
- 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 = Term.prettyPrec
export
Pretty (Definition n) 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
export
Pretty (Block n) where
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:40:40 +0000