diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Obs/Term.idr | 53 |
2 files changed, 54 insertions, 0 deletions
@@ -12,3 +12,4 @@ modules , Obs.Parser , Obs.Sort , Obs.Syntax + , Obs.Term diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr new file mode 100644 index 0000000..cb9701de --- /dev/null +++ b/src/Obs/Term.idr @@ -0,0 +1,53 @@ +||| Abstract syntax for terms. +module Obs.Term + +import Data.Fin +import Obs.Sort +import Text.Bounded +import Text.PrettyPrint.Prettyprinter + +-- Definition ------------------------------------------------------------------ + +public export +data Term : Nat -> Type where + Var : Bounds -> Fin n -> Term n + -- Sorts + Sort : Bounds -> Sort -> Term n + +public export +record Definition (n : Nat) where + constructor MkDefinition + bounds : Bounds -- of the name + name : String + ty : Term n + tm : Term n + +public export +data Block : Nat -> Type where + Nil : Block 0 + (:<) : Block n -> Definition n -> Block (S n) + +-- Operations ------------------------------------------------------------------ + +fullBounds : Term n -> Bounds +fullBounds (Var x i) = x +fullBounds (Sort x s) = x + +-- Pretty Print ---------------------------------------------------------------- + +export +Pretty (Term n) where + prettyPrec d (Var x i) = pretty "$\{show i}" + prettyPrec d (Sort x s) = prettyPrec d s + +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 + +export +Pretty (Block n) where + pretty [] = neutral + pretty ([] :< def) = pretty def + pretty (blk :< def) = pretty blk <+> hardline <+> hardline <+> pretty def |