From 8281e2ea3e531196b8e26ea021ff417670b68bb8 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 17 Dec 2022 12:41:22 +0000
Subject: Define raw syntax.

---
 src/Obs/Syntax.idr | 41 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 src/Obs/Syntax.idr

(limited to 'src')

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
-- 
cgit v1.2.3