diff options
| -rw-r--r-- | obs.ipkg | 2 | ||||
| -rw-r--r-- | src/Core/Term/Substitution.idr | 54 | ||||
| -rw-r--r-- | src/Core/Term/Thinned.idr | 34 | ||||
| -rw-r--r-- | src/Core/Thinning.idr | 15 |
4 files changed, 105 insertions, 0 deletions
@@ -8,4 +8,6 @@ options = "--total" modules = Core.Term + , Core.Term.Substitution + , Core.Term.Thinned , Core.Thinning diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr new file mode 100644 index 0000000..6846d80 --- /dev/null +++ b/src/Core/Term/Substitution.idr @@ -0,0 +1,54 @@ +module Core.Term.Substitution + +import Core.Term +import Core.Term.Thinned +import Core.Thinning + +infix 4 =~= + +-- Definition ------------------------------------------------------------------ + +public export +data Subst : Nat -> Nat -> Type where + Wkn : m `Thins` n -> Subst m n + (:<) : Subst m n -> Thinned n -> Subst (S m) n + +namespace Eq + public export + data (=~=) : Subst m n -> Subst m n -> Type where + Refl : sub =~= sub + (:<) : sub1 =~= sub2 -> t =~= u -> sub1 :< t =~= sub2 :< u + +%name Subst sub +%name Eq.(=~=) prf + +-- Indexing -------------------------------------------------------------------- + +public export +index : Subst m n -> Fin m -> Thinned n +index (Wkn thin) i = Var i `Over` thin +index (sub :< t) FZ = t +index (sub :< t) (FS i) = index sub i + +-- Weakening ------------------------------------------------------------------- + +public export +wkn : Subst k m -> m `Thins` n -> Subst k n +wkn (Wkn thin') thin = Wkn (thin . thin') +wkn (sub :< t) thin = wkn sub thin :< wkn t thin + +-- Constructors ---------------------------------------------------------------- + +public export +lift : Subst m n -> Subst (S m) (S n) +lift sub = wkn sub (drop $ id n) :< (Var 0 `Over` id (S n)) + +-- Substitution ---------------------------------------------------------------- + +public export +subst : Term m -> Subst m n -> Term n +subst (Var i) sub = expand $ index sub i +subst Set sub = Set +subst (Pi t u) sub = Pi (subst t sub) (subst u $ lift sub) +subst (Abs t) sub = Abs (subst t $ lift sub) +subst (App t u) sub = App (subst t sub) (subst u sub) diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr new file mode 100644 index 0000000..0bc6dcf --- /dev/null +++ b/src/Core/Term/Thinned.idr @@ -0,0 +1,34 @@ +module Core.Term.Thinned + +import Core.Term +import Core.Thinning + +%prefix_record_projections off + +infix 4 =~= + +-- Definition ------------------------------------------------------------------ + +public export +record Thinned (n : Nat) where + constructor Over + {0 m : Nat} + term : Term m + thin : m `Thins` n + +%name Thinned t, u, v + +%inline +public export +expand : Thinned n -> Term n +expand (term `Over` thin) = wkn term thin + +public export +(=~=) : Thinned n -> Thinned n -> Type +t =~= u = expand t = expand u + +-- Weakening ------------------------------------------------------------------- + +public export +wkn : Thinned m -> m `Thins` n -> Thinned n +wkn t thin = { thin $= (thin .) } t diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index dc4efcb..a2500e9 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -68,3 +68,18 @@ export wkn : Fin m -> m `Thins` n -> Fin n wkn i IsId = i wkn i (IsThinner thin) = wkn' i thin + +-- Composition ----------------------------------------------------------------- + +comp : Thinner m n -> Thinner k m -> Thinner k n +comp IsBase thin2 = IsDrop thin2 +comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2) +comp (IsKeep thin1) IsBase = IsDrop thin1 +comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2) +comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2) + +export +(.) : m `Thins` n -> k `Thins` m -> k `Thins` n +IsId . thin2 = thin2 +IsThinner thin1 . IsId = IsThinner thin1 +IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2) |