From 14279fa92481304e594e092e702f6925e7142ac5 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 2 Apr 2023 11:52:53 +0100
Subject: Move Environment module.

---
 src/Core/Declarative.idr      |  2 +-
 src/Core/Environment.idr      | 88 +++++++++++++++++++++++++++++++++++++++++++
 src/Core/Reduction.idr        |  2 +-
 src/Core/Term/Environment.idr | 88 -------------------------------------------
 4 files changed, 90 insertions(+), 90 deletions(-)
 create mode 100644 src/Core/Environment.idr
 delete mode 100644 src/Core/Term/Environment.idr

(limited to 'src')

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index ae31870..ae7e3aa 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -1,9 +1,9 @@
 module Core.Declarative
 
 import Core.Context
+import Core.Environment
 import Core.Name
 import Core.Term
-import Core.Term.Environment
 import Core.Term.Substitution
 import Core.Thinning
 import Core.Var
diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr
new file mode 100644
index 0000000..ff484f4
--- /dev/null
+++ b/src/Core/Environment.idr
@@ -0,0 +1,88 @@
+module Core.Environment
+
+import Core.Context
+import Core.Term
+import Core.Thinning
+import Core.Var
+
+import Syntax.PreorderReasoning
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Env : Context -> Type where
+  Lin : Env [<]
+  Add : Env sx -> sy `Thins` sx -> Term sy -> Env (sx :< n)
+
+%name Env env
+
+-- Constructors ----------------------------------------------------------------
+
+public export
+(:<) : Env sx -> Term sx -> Env (sx :< n)
+env :< t = Add env (id _) t
+
+-- Operations ------------------------------------------------------------------
+
+record IndexResult (sx : Context) where
+  constructor MkRes
+  {0 sy : Context}
+  val : Term sy
+  thin : sy `Thins` sx
+
+shift : IndexResult sx -> IndexResult (sx :< n)
+shift (MkRes val thin) = MkRes val (drop thin n)
+
+expand : IndexResult sx -> Term sx
+expand (MkRes val thin) = wkn val thin
+
+doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx
+doIndex (Add env thin t) Here = shift $ MkRes t thin
+doIndex (Add env thin t) (There i) = shift $ doIndex env $ view i
+
+export
+index : Env sx -> Var sx -> Term sx
+index env i = expand $ doIndex env $ view i
+
+-- Equality --------------------------------------------------------------------
+
+namespace Eq
+  public export
+  data EnvEq : Env sx -> Env sx -> Type where
+    Lin : EnvEq [<] [<]
+    (:<) :
+      EnvEq env1 env2 ->
+      Term.wkn t thin1 = wkn u thin2 ->
+      EnvEq (Add env1 thin1 t) (Add env2 thin2 u)
+
+  %name EnvEq prf
+
+expandShift : (val : IndexResult sx) -> expand (shift val) = wkn (expand val) (drop (id sx) n)
+expandShift (MkRes val thin) = sym $ Calc $
+  |~ wkn (wkn val thin) (drop (id sx) n)
+  ~~ wkn val (drop (id sx) n . thin)     ...(wknHomo val thin $ drop (id sx) n)
+  ~~ wkn val (drop (id sx . thin) n)     ...(cong (wkn val) $ compLeftDrop (id sx) thin n)
+  ~~ wkn val (drop thin n)               ...(cong (\thin => wkn val (drop thin n)) $ compLeftIdentity thin)
+
+doIndexEqIsEq :
+  -- {env1, env2 : _} ->
+  EnvEq env1 env2 ->
+  {0 i : Var sx} ->
+  (view : View i) ->
+  expand (doIndex env1 view) = expand (doIndex env2 view)
+doIndexEqIsEq {sx = sx :< n} ((:<) {t, u, thin1, thin2} prf eq) Here = Calc $
+  |~ wkn t (drop thin1 n)
+  ~~ wkn (wkn t thin1) (drop (id sx) n) ...(expandShift (MkRes t thin1))
+  ~~ wkn (wkn u thin2) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ eq)
+  ~~ wkn u (drop thin2 n)               ...(sym $ expandShift (MkRes u thin2))
+doIndexEqIsEq {sx = sx :< n} ((:<) {env1, env2} prf eq) (There i) = Calc $
+  |~ expand (shift $ doIndex env1 $ view i)
+  ~~ wkn (expand $ doIndex env1 $ view i) (drop (id sx) n) ...(expandShift $ doIndex env1 $ view i)
+  ~~ wkn (expand $ doIndex env2 $ view i) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ doIndexEqIsEq prf (view i))
+  ~~ expand (shift $ doIndex env2 $ view i)                ...(sym $ expandShift $ doIndex env2 $ view i)
+
+export
+indexEqIsEq : EnvEq env1 env2 -> (i : Var sx) -> index env1 i = index env2 i
+indexEqIsEq prf i = doIndexEqIsEq prf $ view i
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
index b50b8c2..0c89abe 100644
--- a/src/Core/Reduction.idr
+++ b/src/Core/Reduction.idr
@@ -2,8 +2,8 @@ module Core.Reduction
 
 import Core.Context
 import Core.Declarative
+import Core.Environment
 import Core.Term
-import Core.Term.Environment
 import Core.Term.NormalForm
 import Core.Term.Substitution
 
diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr
deleted file mode 100644
index d292a96..0000000
--- a/src/Core/Term/Environment.idr
+++ /dev/null
@@ -1,88 +0,0 @@
-module Core.Term.Environment
-
-import Core.Context
-import Core.Term
-import Core.Thinning
-import Core.Var
-
-import Syntax.PreorderReasoning
-
-%prefix_record_projections off
-
--- Definition ------------------------------------------------------------------
-
-public export
-data Env : Context -> Type where
-  Lin : Env [<]
-  Add : Env sx -> sy `Thins` sx -> Term sy -> Env (sx :< n)
-
-%name Env env
-
--- Constructors ----------------------------------------------------------------
-
-public export
-(:<) : Env sx -> Term sx -> Env (sx :< n)
-env :< t = Add env (id _) t
-
--- Operations ------------------------------------------------------------------
-
-record IndexResult (sx : Context) where
-  constructor MkRes
-  {0 sy : Context}
-  val : Term sy
-  thin : sy `Thins` sx
-
-shift : IndexResult sx -> IndexResult (sx :< n)
-shift (MkRes val thin) = MkRes val (drop thin n)
-
-expand : IndexResult sx -> Term sx
-expand (MkRes val thin) = wkn val thin
-
-doIndex : Env sx -> {0 i : Var sx} -> View i -> IndexResult sx
-doIndex (Add env thin t) Here = shift $ MkRes t thin
-doIndex (Add env thin t) (There i) = shift $ doIndex env $ view i
-
-export
-index : Env sx -> Var sx -> Term sx
-index env i = expand $ doIndex env $ view i
-
--- Equality --------------------------------------------------------------------
-
-namespace Eq
-  public export
-  data EnvEq : Env sx -> Env sx -> Type where
-    Lin : EnvEq [<] [<]
-    (:<) :
-      EnvEq env1 env2 ->
-      Term.wkn t thin1 = wkn u thin2 ->
-      EnvEq (Add env1 thin1 t) (Add env2 thin2 u)
-
-  %name EnvEq prf
-
-expandShift : (val : IndexResult sx) -> expand (shift val) = wkn (expand val) (drop (id sx) n)
-expandShift (MkRes val thin) = sym $ Calc $
-  |~ wkn (wkn val thin) (drop (id sx) n)
-  ~~ wkn val (drop (id sx) n . thin)     ...(wknHomo val thin $ drop (id sx) n)
-  ~~ wkn val (drop (id sx . thin) n)     ...(cong (wkn val) $ compLeftDrop (id sx) thin n)
-  ~~ wkn val (drop thin n)               ...(cong (\thin => wkn val (drop thin n)) $ compLeftIdentity thin)
-
-doIndexEqIsEq :
-  -- {env1, env2 : _} ->
-  EnvEq env1 env2 ->
-  {0 i : Var sx} ->
-  (view : View i) ->
-  expand (doIndex env1 view) = expand (doIndex env2 view)
-doIndexEqIsEq {sx = sx :< n} ((:<) {t, u, thin1, thin2} prf eq) Here = Calc $
-  |~ wkn t (drop thin1 n)
-  ~~ wkn (wkn t thin1) (drop (id sx) n) ...(expandShift (MkRes t thin1))
-  ~~ wkn (wkn u thin2) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ eq)
-  ~~ wkn u (drop thin2 n)               ...(sym $ expandShift (MkRes u thin2))
-doIndexEqIsEq {sx = sx :< n} ((:<) {env1, env2} prf eq) (There i) = Calc $
-  |~ expand (shift $ doIndex env1 $ view i)
-  ~~ wkn (expand $ doIndex env1 $ view i) (drop (id sx) n) ...(expandShift $ doIndex env1 $ view i)
-  ~~ wkn (expand $ doIndex env2 $ view i) (drop (id sx) n) ...(cong (\t => wkn t (drop (id sx) n)) $ doIndexEqIsEq prf (view i))
-  ~~ expand (shift $ doIndex env2 $ view i)                ...(sym $ expandShift $ doIndex env2 $ view i)
-
-export
-indexEqIsEq : EnvEq env1 env2 -> (i : Var sx) -> index env1 i = index env2 i
-indexEqIsEq prf i = doIndexEqIsEq prf $ view i
-- 
cgit v1.2.3