diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Obs/Syntax.idr | 41 |
2 files changed, 42 insertions, 0 deletions
@@ -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 |