Define environment extensions.

2 files changed, 37 insertions, 0 deletions

diff --git a/obs.ipkg b/obs.ipkg
index be12a16..987d511 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -9,6 +9,7 @@ options = "--total"
 modules
   = Core.Declarative
   , Core.Environment
+  , Core.Environment.Extension
   , Core.Reduction
   , Core.Term
   , Core.Term.NormalForm
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)