Define Term substitution.

2 files changed, 88 insertions, 0 deletions

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