Define abstract syntax.

2 files changed, 54 insertions, 0 deletions

diff --git a/obs.ipkg b/obs.ipkg
index d637613..e9d4117 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -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