Define environment extensions.

1 files changed, 36 insertions, 0 deletions

diff --git a/src/Core/Environment/Extension.idr b/src/Core/Environment/Extension.idr
new file mode 100644
index 0000000..9914697
--- /dev/null
+++ b/src/Core/Environment/Extension.idr
@@ -0,0 +1,36 @@
+module Core.Environment.Extension
+
+import Core.Environment
+import Core.Term.Thinned
+import Core.Thinning
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Extends : m `Thins` n -> Env n -> Env m -> Type where
+  Id : Extends (id n) env env
+  Drop : Extends thin env1 env2 -> Extends (drop thin) (env1 :< a) env2
+  Keep : Extends thin env1 env2 -> Extends (keep thin) (env1 :< wkn a thin) (env2 :< a)
+
+%name Extends ext
+
+-- Composition -----------------------------------------------------------------
+
+public export
+(.) : Extends thin2 env3 env2 -> Extends thin1 env2 env1 -> Extends (thin2 . thin1) env3 env1
+Id . ext1 =
+  rewrite compLeftId thin1 in
+  ext1
+Drop {thin = thin2} ext2 . ext1 =
+  rewrite compLeftDrop thin2 thin1 in
+  Drop (ext2 . ext1)
+Keep {thin = thin2} ext2 . Id =
+  rewrite compRightId (keep thin2) in
+  Keep ext2
+Keep {thin = thin2} ext2 . Drop {thin = thin1} ext1 =
+  rewrite compRightDrop thin2 thin1 in
+  Drop (ext2 . ext1)
+Keep {thin = thin2} ext2 . Keep {thin = thin1, a} ext1 =
+  rewrite compKeep thin2 thin1 in
+  rewrite wknHomo a thin1 thin2 in
+  Keep (ext2 . ext1)