added inthe interpretation functions

Author: jamesmckinna

README/Data/Fin/Relation/Ternary/PunchOut.agda

@@ -8,7 +8,7 @@
 -- precisely mirrored in the constructors of the view type
 --
 -- Using this view, we can exhibit the corresponding properties of
--- the function `punchIn` defined in `Data.Fin.Properties`
+-- the function `punchOut` defined in `Data.Fin.Properties`
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}

src/Data/Fin/Relation/Ternary/Pinch.agda

@@ -29,6 +29,9 @@ private
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
+-- Each constructor corresponds to a particular call-pattern in the original
+-- function definition; recursive calls are represented by inductive premises
+
 data View : ∀ {n} (i : Fin n) (j : Fin (suc n)) (k : Fin n) → Set where
 
   any-zero : ∀ {n} (i : Fin (suc n))             → View i zero zero
@@ -37,14 +40,24 @@ data View : ∀ {n} (i : Fin n) (j : Fin (suc n)) (k : Fin n) → Set where
 
 -- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
 
+-- The recursion/pattern analysis of the original definition of `pinch`
+-- (which is responsible for showing termination in the first place)
+-- is then exactly replicated in the definition of the covering function `view`;
+-- thus that definitional pattern analysis is encapsulated once and for all
+
 view : ∀ {n} i j → View {n} i j (pinch i j)
 view {suc _} i zero    = any-zero i
 view   zero    (suc j) = zero-suc j
 view   (suc i) (suc j) = suc-suc (view i j)
 
+-- Interpretation of the view: the original function itself
+
+⟦_⟧ : ∀ {i j} {k} .(v : View {n} i j k) → Fin n
+⟦_⟧ {n = n} {i} {j} {k} _ = pinch i j
+
 -- The View is complete
 
-view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → pinch i j ≡ k
+view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → ⟦ v ⟧ ≡ k
 view-complete (any-zero i) = refl
 view-complete (zero-suc j) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)

src/Data/Fin/Relation/Ternary/PunchIn.agda

@@ -27,6 +27,9 @@ private
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
+-- Each constructor corresponds to a particular call-pattern in the original
+-- function definition; recursive calls are represented by inductive premises
+
 data View : ∀ {n} (i : Fin (suc n)) (j : Fin n) (k : Fin (suc n)) → Set where
 
   zero-suc : ∀ {n} (j : Fin n)                   → View zero j (suc j)
@@ -43,14 +46,24 @@ view-codomain (suc-suc v) = (view-codomain v) ∘ suc-injective
 
 -- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
 
+-- The recursion/pattern analysis of the original definition of `punchIn`
+-- (which is responsible for showing termination in the first place)
+-- is then exactly replicated in the definition of the covering function `view`;
+-- thus that definitional pattern analysis is encapsulated once and for all
+
 view : ∀ i j → View {n} i j (punchIn i j)
 view zero         j  = zero-suc j
 view (suc i) zero    = suc-zero i
 view (suc i) (suc j) = suc-suc (view i j)
 
+-- Interpretation of the view: the original function itself
+
+⟦_⟧ : ∀ {i} {j} {k} .(v : View {n} i j k) → Fin (suc n)
+⟦_⟧ {n = n} {i} {j} {k} _ = punchIn i j
+
 -- The View is complete
 
-view-complete : ∀ {i j} {k} (v : View {n} i j k) → punchIn i j ≡ k
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → ⟦ v ⟧ ≡ k
 view-complete (zero-suc j) = refl
 view-complete (suc-zero i) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)

src/Data/Fin/Relation/Ternary/PunchOut.agda

@@ -28,6 +28,9 @@ private
 ------------------------------------------------------------------------
 -- The View, considered as a ternary relation
 
+-- Each constructor corresponds to a particular call-pattern in the original
+-- function definition; recursive calls are represented by inductive premises
+
 data View : ∀ {n} (i j : Fin (suc n)) (k : Fin n) → Set where
 
   zero-suc : ∀ {n} (j : Fin n)                   → View zero (suc j) j
@@ -44,15 +47,25 @@ view-domain (suc-suc v) = (view-domain v) ∘ suc-injective
 
 -- The View is sound, ie covers all telescopes satisfying that precondition
 
+-- The recursion/pattern analysis of the original definition of `punchOut`
+-- (which is responsible for showing termination in the first place)
+-- is then exactly replicated in the definition of the covering function `view`;
+-- thus that definitional pattern analysis is encapsulated once and for all
+
 view : ∀ {n} {i j} (d : Domain i j) → View {n} i j (punchOut d)
 view             {i = zero}  {j = zero}  d with () ← d refl
 view             {i = zero}  {j = suc j} d = zero-suc j
 view {n = suc _} {i = suc i} {j = zero}  d = suc-zero i
 view {n = suc _} {i = suc i} {j = suc j} d = suc-suc (view (d ∘ (cong suc)))
 
+-- Interpretation of the view: the original function itself
+
+⟦_⟧ : ∀ {i j} {k} (v : View {n} i j k) → Fin n
+⟦ v ⟧ = punchOut (view-domain v)
+
 -- The View is complete
 
-view-complete : ∀ {i j} {k} (v : View {n} i j k) → punchOut (view-domain v) ≡ k
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → ⟦ v ⟧ ≡ k
 view-complete (zero-suc j) = refl
 view-complete (suc-zero i) = refl
 view-complete (suc-suc v)  = cong suc (view-complete v)