From 44778825c288721d7b340d16bf74c65ce4502640 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 22 Aug 2022 10:17:08 +0200
Subject: [PATCH] add Definitions module

---
 lib/Quox/Context.idr    |  4 ++--
 lib/Quox/Definition.idr | 52 +++++++++++++++++++++++++++++++++++++++++
 lib/Quox/Equal.idr      |  1 +
 lib/Quox/Typing.idr     | 13 +----------
 lib/quox-lib.ipkg       |  1 +
 5 files changed, 57 insertions(+), 14 deletions(-)
 create mode 100644 lib/Quox/Definition.idr

diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 5bfe956..c87a634 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -15,7 +15,7 @@ import Control.Monad.Identity
 infixl 5 :<
 ||| a sequence of bindings under an existing context. each successive element
 ||| has one more bound variable, which correspond to all previous elements
-||| as well as the global context.
+||| as well as the surrounding context.
 public export
 data Telescope : (tm : Nat -> Type) -> (from, to : Nat) -> Type where
   Lin  : Telescope tm from from
@@ -26,7 +26,7 @@ public export
 Telescope' : (a : Type) -> (from, to : Nat) -> Type
 Telescope' a = Telescope (\_ => a)
 
-||| a global context is actually just a telescope over no existing bindings
+||| a top level context is actually just a telescope over no existing bindings
 public export
 Context : (tm : Nat -> Type) -> (len : Nat) -> Type
 Context tm len = Telescope tm 0 len
diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr
new file mode 100644
index 0000000..5cd3cdb
--- /dev/null
+++ b/lib/Quox/Definition.idr
@@ -0,0 +1,52 @@
+module Quox.Definition
+
+import public Quox.Syntax
+import public Data.SortedMap
+import public Control.Monad.State
+
+
+public export
+record AnyTerm where
+  constructor T
+  def : forall d, n. Term d n
+
+public export
+record Definition where
+  constructor MkDef'
+  qty         : Qty
+  0 qtyGlobal : IsGlobal qty
+  type        : AnyTerm
+  term        : Maybe AnyTerm
+
+public export %inline
+MkDef : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
+           (type, term : forall d, n. Term d n) -> Definition
+MkDef {qty, type, term} =
+  MkDef' {qty, qtyGlobal = %search, type = T type, term = Just (T term)}
+
+public export %inline
+MkAbstract : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
+             (type : forall d, n. Term d n) -> Definition
+MkAbstract {qty, type} =
+  MkDef' {qty, qtyGlobal = %search, type = T type, term = Nothing}
+
+
+public export %inline
+(.type0) : Definition -> Term 0 0
+g.type0 = g.type.def
+
+public export %inline
+(.term0) : Definition -> Maybe (Term 0 0)
+g.term0 = map (\t => t.def) g.term
+
+public export %inline
+(.qtyP) : Definition -> Subset Qty IsGlobal
+g.qtyP = Element g.qty g.qtyGlobal
+
+public export %inline
+isZero : Definition -> Bool
+isZero g = g.qty == Zero
+
+public export
+Definitions : Type
+Definitions = SortedMap Name Definition
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 52212ca..9be5846 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -1,6 +1,7 @@
 module Quox.Equal
 
 import public Quox.Syntax
+import public Quox.Definition
 import Control.Monad.Either
 import Generics.Derive
 
diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr
index f3cfa25..dd7b5b3 100644
--- a/lib/Quox/Typing.idr
+++ b/lib/Quox/Typing.idr
@@ -3,6 +3,7 @@ module Quox.Typing
 import public Quox.Syntax
 import public Quox.Context
 import public Quox.Equal
+import public Quox.Definition
 
 import Data.Nat
 import public Data.SortedMap
@@ -31,18 +32,6 @@ QOutput : Nat -> Type
 QOutput = QContext
 
 
-public export
-record Global where
-  constructor MkGlobal
-  qty         : Qty
-  0 qtyGlobal : IsGlobal qty
-  type, term  : forall d, n. Term d n
-
-public export
-Globals : Type
-Globals = SortedMap Name Global
-
-
 public export
 record TyContext (d, n : Nat) where
   constructor MkTyContext
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index d98ce18..f37371f 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -26,6 +26,7 @@ modules =
   Quox.Syntax.Term.Subst,
   Quox.Syntax.Universe,
   Quox.Syntax.Var,
+  Quox.Definition,
   Quox.Token,
   Quox.Lexer,
   Quox.Parser,