From 08fb686bf6f334e4368dd5439c37004238f925ae Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 20 Sep 2023 21:58:04 +0200
Subject: [PATCH] move Scoped to separate module

---
 lib/Quox/Scoped.idr           | 40 +++++++++++++++++++++++++++++++++++
 lib/Quox/Syntax/Term/Base.idr | 32 +---------------------------
 lib/quox-lib.ipkg             |  1 +
 3 files changed, 42 insertions(+), 31 deletions(-)
 create mode 100644 lib/Quox/Scoped.idr

diff --git a/lib/Quox/Scoped.idr b/lib/Quox/Scoped.idr
new file mode 100644
index 0000000..be43cfe
--- /dev/null
+++ b/lib/Quox/Scoped.idr
@@ -0,0 +1,40 @@
+module Quox.Scoped
+
+import public Quox.Var
+import public Quox.Context
+
+import Derive.Prelude
+
+%language ElabReflection
+%default total
+
+
+public export
+data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where
+  Y : (body : f (s + n)) -> ScopedBody s f n
+  N : (body : f n)       -> ScopedBody s f n
+%name ScopedBody body
+
+export %inline %hint
+EqScopedBody : (forall n. Eq (f n)) => Eq (ScopedBody s f n)
+EqScopedBody = deriveEq
+
+export %inline %hint
+ShowScopedBody : (forall n. Show (f n)) => Show (ScopedBody s f n)
+ShowScopedBody = deriveShow
+
+||| a scoped term with names
+public export
+record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
+  constructor S
+  names : BContext s
+  body  : ScopedBody s f n
+%name Scoped body
+
+export %inline
+(forall n. Eq (f n)) => Eq (Scoped s f n) where
+  s == t = s.body == t.body
+
+export %inline %hint
+ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
+ShowScoped = deriveShow
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 66794ef..43c97b3 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -1,6 +1,7 @@
 module Quox.Syntax.Term.Base
 
 import public Quox.Var
+import public Quox.Scoped
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst
 import public Quox.Syntax.Qty
@@ -46,37 +47,6 @@ TagVal : Type
 TagVal = String
 
 
-public export
-data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where
-  Y : (body : f (s + n)) -> ScopedBody s f n
-  N : (body : f n)       -> ScopedBody s f n
-%name ScopedBody body
-
-export %inline %hint
-EqScopedBody : (forall n. Eq (f n)) => Eq (ScopedBody s f n)
-EqScopedBody = deriveEq
-
-export %inline %hint
-ShowScopedBody : (forall n. Show (f n)) => Show (ScopedBody s f n)
-ShowScopedBody = deriveShow
-
-||| a scoped term with names
-public export
-record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
-  constructor S
-  names : BContext s
-  body  : ScopedBody s f n
-%name Scoped body
-
-export %inline
-(forall n. Eq (f n)) => Eq (Scoped s f n) where
-  s == t = s.body == t.body
-
-export %inline %hint
-ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
-ShowScoped = deriveShow
-
-
 infixl 8 :#
 infixl 9 :@, :%
 mutual
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 4572f4c..7e0af1b 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -18,6 +18,7 @@ modules =
   Quox.No,
   Quox.Loc,
   Quox.Var,
+  Quox.Scoped,
   Quox.OPE,
   Quox.Pretty,
   Quox.Syntax,