From b882d95eb08fea2341bcfa6b41aa06e060cde1ec Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 17 Dec 2022 15:15:29 +0000
Subject: Define abstract syntax.

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

(limited to 'src')

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