Define raw syntax.

2 files changed, 42 insertions, 0 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 229fbe6..3320896 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -6,3 +6,4 @@ depends = contrib
 
 modules
   = Obs.Sort
+  , Obs.Syntax
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
new file mode 100644
index 0000000..9ec1d3d
--- /dev/null
+++ b/src/Obs/Syntax.idr
@@ -0,0 +1,41 @@
+||| Raw syntax for terms. This is before eliminating names.
+module Obs.Syntax
+
+import Obs.Sort
+import Text.Bounded
+import Text.PrettyPrint.Prettyprinter
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Syntax : Type where
+  Var  : Bounds -> String -> Syntax
+  -- Sorts
+  Sort : Bounds -> Sort -> Syntax
+
+public export
+record Definition where
+  constructor MkDefinition
+  bounds : Bounds -- of the name
+  name   : String
+  ty     : Syntax
+  tm     : Syntax
+
+-- Operations ------------------------------------------------------------------
+
+fullBounds : Syntax -> Bounds
+fullBounds (Var x str) = x
+fullBounds (Sort x s)  = x
+
+-- Pretty Print ----------------------------------------------------------------
+
+export
+Pretty Syntax where
+  prettyPrec d (Var x str) = pretty str
+  prettyPrec d (Sort x s)  = prettyPrec d s
+
+export
+Pretty Definition where
+  pretty def = group $
+    pretty def.name <++> colon <+> softline <+> pretty def.ty <+> hardline <+>
+    pretty def.name <++> equals <+> softline <+> pretty def.tm