diff options
Diffstat (limited to 'src/Obs/Term.idr')
| -rw-r--r-- | src/Obs/Term.idr | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr index 5126d99..8829038 100644 --- a/src/Obs/Term.idr +++ b/src/Obs/Term.idr @@ -12,6 +12,8 @@ import Text.Bounded -- Definition ------------------------------------------------------------------ +infix 5 ::< + data Term : Nat -> Type public export @@ -74,6 +76,12 @@ data Term : Nat -> Type where CastId : (value : WithBounds (Term n)) -> Term n public export +record Parameter (n : Nat) where + constructor MkParameter + name : WithBounds String + ty : WithBounds (Term n) + +public export record Definition (n : Nat) where constructor MkDefinition name : WithBounds String @@ -84,6 +92,7 @@ public export data Block : Nat -> Type where Nil : Block 0 (:<) : Block n -> Definition n -> Block (S n) + (::<) : Block n -> Parameter n -> Block (S n) -- Pretty Print ---------------------------------------------------------------- @@ -168,6 +177,11 @@ Pretty (Term n) where prettyPrec = Term.prettyPrec export +Pretty (Parameter n) where + pretty param = group $ + pretty "parameter" <++> pretty param.name.val <++> colon <+> softline <+> pretty param.ty.val + +export Pretty (Definition n) where pretty def = group $ pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+> @@ -177,4 +191,6 @@ export Pretty (Block n) where pretty [] = neutral pretty ([] :< def) = pretty def + pretty ([] ::< param) = pretty param pretty (blk :< def) = pretty blk <+> hardline <+> hardline <+> pretty def + pretty (blk ::< param) = pretty blk <+> hardline <+> hardline <+> pretty param |