diff options
Diffstat (limited to 'src/Obs/Term.idr')
| -rw-r--r-- | src/Obs/Term.idr | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr index 2cc2f93..62a22bc 100644 --- a/src/Obs/Term.idr +++ b/src/Obs/Term.idr @@ -12,12 +12,15 @@ import Text.PrettyPrint.Prettyprinter public export data Term : Nat -> Type where - Var : Bounds -> Fin n -> Term n + Var : Bounds -> Fin n -> Term n -- Sorts - Sort : Bounds -> Sort -> Term n + Sort : Bounds -> Sort -> Term n -- True - Top : Bounds -> Term n - Point : Bounds -> Term n + Top : Bounds -> Term n + Point : Bounds -> Term n + -- False + Bottom : Bounds -> Term n + Absurd : Bounds -> Term n -> Term n -> Term n public export record Definition (n : Nat) where @@ -35,20 +38,27 @@ data Block : Nat -> Type where -- Operations ------------------------------------------------------------------ export -fullBounds : Term n -> Bounds -fullBounds (Var x i) = x -fullBounds (Sort x s) = x -fullBounds (Top x) = x -fullBounds (Point x) = x +fullBounds : Term n -> WithBounds (Term n) +fullBounds tm@(Var x i) = MkBounded tm False x +fullBounds tm@(Sort x s) = 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) -- Pretty Print ---------------------------------------------------------------- export Pretty (Term n) where - prettyPrec d (Var x i) = pretty "$\{show i}" + prettyPrec d (Var x i) = pretty "$\{show i}" prettyPrec d (Sort x s) = prettyPrec d s - prettyPrec d (Top x) = pretty "()" - prettyPrec d (Point x) = pretty "_" + prettyPrec d (Top x) = pretty "()" + prettyPrec d (Point x) = pretty "_" + prettyPrec d (Bottom x) = pretty "Void" + prettyPrec d (Absurd x a t) = + parenthesise (d > Open) $ + group $ + fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t] export Pretty (Definition n) where |