diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Core/Environment/Extension.idr | 36 |
2 files changed, 37 insertions, 0 deletions
@@ -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) |