implement a bff on a shaped source type

Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.

5 files changed, 150 insertions, 17 deletions

diff --git a/BFF.agda b/BFF.agda
index 2ce24db..b78e2af 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -15,11 +15,13 @@ open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid)
 
 open import FinMap
 open import Generic using (sequenceV ; ≡-to-Π)
+open import Structures using (Shaped ; module Shaped)
+open import Instances using (VecShaped)
 import CheckInsert
-open import GetTypes using (VecVec-to-PartialVecVec)
+open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeVec)
 
-module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
-  open GetTypes.PartialVecVec public using (Get)
+module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
+  open GetTypes.PartialShapeVec public using (Get ; module Get)
   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
   open CheckInsert A
 
@@ -27,27 +29,48 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   assoc []V       []V       = just empty
   assoc (i ∷V is) (b ∷V bs) = (assoc is bs) >>= (checkInsert i b)
 
+  enumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → (s : S) → C (Fin (Shaped.arity ShapeT s)) s
+  enumerate ShapeT s = fill s (allFin (arity s))
+    where open Shaped ShapeT
+
+  denumerate : {S : Set} {C : Set → S → Set} → (ShapeT : Shaped S C) → {α : Set} {s : S} → (c : C α s) → Fin (Shaped.arity ShapeT s) → α
+  denumerate ShapeT c = flip lookupV (Shaped.content ShapeT c)
+
+  bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.Container G Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Get.Container G (Maybe Carrier) (Get.|gl₁| G j))
+  bff G {i} j s v = let s′ = enumerate ShapeT (|gl₁| i)
+                        t′ = get s′
+                        g  = fromFunc (denumerate ShapeT s)
+                        g′ = delete-many t′ g
+                        t  = enumerate ShapeT (|gl₁| j)
+                        h  = assoc (get t) v
+                        h′ = (flip union (reshape g′ (arity (|gl₁| j)))) <$> h
+                    in ((λ f → fmap f t) ∘ flip lookupM) <$> h′
+    where open Get G
+
+  sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.Container G Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Get.Container G Carrier (Get.|gl₁| G j))
+  sbff G j s v = bff G j s v >>= Get.sequence G
+
+module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
+  open GetTypes.PartialVecVec public using (Get)
+  open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
+  open CheckInsert A
+
+  open PartialShapeBFF A public using (assoc)
+
   enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n
-  enumerate {n} _ = allFin n
+  enumerate {n} _ = PartialShapeBFF.enumerate A VecShaped n
 
   enumeratel : (n : ℕ) → Vec (Fin n) n
-  enumeratel = allFin
+  enumeratel = PartialShapeBFF.enumerate A VecShaped
 
   denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
-  denumerate = flip lookupV
+  denumerate = PartialShapeBFF.denumerate A VecShaped
 
   bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j))
-  bff G i s v = let s′ = enumerate s
-                    t′ = Get.get G s′
-                    g  = fromFunc (denumerate s)
-                    g′ = delete-many t′ g
-                    t  = enumeratel (Get.|gl₁| G i)
-                    h  = assoc (Get.get G t) v
-                    h′ = (flip union (reshape g′ (Get.|gl₁| G i))) <$> h
-                in (flip mapV t ∘ flip lookupM) <$> h′
+  bff G j s v = PartialShapeBFF.bff A (PartialVecVec-to-PartialShapeVec G) j s v
 
   sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j))
-  sbff G j s v = bff G j s v >>= sequenceV
+  sbff  G j s v = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeVec G) j s v
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.VecVec public using (Get)
diff --git a/Everything.agda b/Everything.agda
index 7383dd5..5ca5550 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -3,6 +3,7 @@ module Everything where
 
 import Generic
 import Structures
+import Instances
 import FinMap
 import CheckInsert
 import GetTypes
diff --git a/GetTypes.agda b/GetTypes.agda
index eb72cea..0db3f31 100644
--- a/GetTypes.agda
+++ b/GetTypes.agda
@@ -12,6 +12,8 @@ open import Relation.Binary using (Setoid)
 open Injection using (to)
 
 open import Generic using (≡-to-Π)
+open import Structures using (Shaped ; module Shaped)
+open import Instances using (VecShaped)
 
 module ListList where
   record Get : Set₁ where
@@ -49,3 +51,36 @@ VecVec-to-PartialVecVec G = record
   ; get = get
   ; free-theorem = free-theorem
   } where open VecVec.Get G
+
+module PartialShapeVec where
+  record Get : Set₁ where
+    field
+      Shape : Set
+      Container : Set → Shape → Set
+      ShapeT : Shaped Shape Container
+
+      I : Setoid ℓ₀ ℓ₀
+      gl₁ : I ↪ EqSetoid Shape
+      gl₂ : I ⟶ EqSetoid ℕ
+
+    |I|   = Setoid.Carrier I
+    |gl₁| = _⟨$⟩_ (to gl₁)
+    |gl₂| = _⟨$⟩_ gl₂
+
+    open Shaped ShapeT using (fmap)
+
+    field
+      get : {A : Set} {i : |I|} → Container A (|gl₁| i) → Vec A (|gl₂| i)
+      free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmap f ≗ mapV f ∘ get
+
+    open Shaped ShapeT public
+
+PartialVecVec-to-PartialShapeVec : PartialVecVec.Get → PartialShapeVec.Get
+PartialVecVec-to-PartialShapeVec G = record
+  { ShapeT       = VecShaped
+  ; I            = I
+  ; gl₁          = gl₁
+  ; gl₂          = gl₂
+  ; get          = get
+  ; free-theorem = free-theorem
+  } where open PartialVecVec.Get G
diff --git a/Instances.agda b/Instances.agda
new file mode 100644
index 0000000..faff6f8
--- /dev/null
+++ b/Instances.agda
@@ -0,0 +1,18 @@
+module Instances where
+
+open import Data.Nat using (ℕ)
+open import Data.Vec using (Vec)
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+open import Structures using (Shaped)
+
+VecShaped : Shaped ℕ Vec
+VecShaped = record
+  { arity = id
+  ; content = id
+  ; fill = λ _ → id
+  ; isShaped = record
+    { content-fill = λ _ → refl
+    ; fill-content = λ _ _ → refl
+    } }
diff --git a/Structures.agda b/Structures.agda
index f1fd85b..10abd42 100644
--- a/Structures.agda
+++ b/Structures.agda
@@ -1,10 +1,17 @@
 module Structures where
 
 open import Category.Functor using (RawFunctor ; module RawFunctor)
-open import Function using (_∘_ ; id)
+open import Category.Monad using (module RawMonad)
+open import Data.Maybe using (Maybe) renaming (monad to MaybeMonad)
+open import Data.Nat using (ℕ)
+open import Data.Vec as V using (Vec)
+import Data.Vec.Properties as VP
+open import Function using (_∘_ ; flip ; id)
 open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
 open import Relation.Binary using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl ; module ≡-Reasoning)
+
+open import Generic using (sequenceV)
 
 record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α → F β) : Set₁ where
   field
@@ -29,3 +36,52 @@ record Functor (f : Set → Set) : Set₁ where
 
   open RawFunctor rawfunctor public
   open IsFunctor isFunctor public
+
+record IsShaped (S : Set)
+                (C : Set → S → Set)
+                (arity : S → ℕ)
+                (content : {α : Set} {s : S} → C α s → Vec α (arity s))
+                (fill : {α : Set} → (s : S) → Vec α (arity s) → C α s)
+                : Set₁ where
+  field
+    content-fill : {α : Set} {s : S} → (c : C α s) → fill s (content c) ≡ c
+    fill-content : {α : Set} → (s : S) → (v : Vec α (arity s)) → content (fill s v) ≡ v
+
+  fmap : {α β : Set} → (f : α → β) → {s : S} → C α s → C β s
+  fmap f {s} c = fill s (V.map f (content c))
+
+  isFunctor : (s : S) → IsFunctor (flip C s) (λ f → fmap f)
+  isFunctor s = record
+    { cong = λ g≗h c → P.cong (fill s) (VP.map-cong g≗h (content c))
+    ; identity = λ c → begin
+        fill s (V.map id (content c))
+          ≡⟨ P.cong (fill s) (VP.map-id (content c)) ⟩
+        fill s (content c)
+          ≡⟨ content-fill c ⟩
+        c ∎
+    ; composition = λ g h c → P.cong (fill s) (begin
+        V.map (g ∘ h) (content c)
+          ≡⟨ VP.map-∘ g h (content c) ⟩
+        V.map g (V.map h (content c))
+          ≡⟨ P.cong (V.map g) (P.sym (fill-content s (V.map h (content c)))) ⟩
+        V.map g (content (fill s (V.map h (content c)))) ∎)
+    } where open ≡-Reasoning
+
+  fmap-content : {α β : Set} → (f : α → β) → {s : S} → content {β} {s} ∘ fmap f ≗ V.map f ∘ content
+  fmap-content f c = fill-content _ (V.map f (content c))
+  fill-fmap : {α β : Set} → (f : α → β) → (s : S) → fmap f ∘ fill s ≗ fill s ∘ V.map f
+  fill-fmap f s v = P.cong (fill s ∘ V.map f) (fill-content s v)
+
+  sequence : {α : Set} {s : S} → C (Maybe α) s → Maybe (C α s)
+  sequence {s = s} c = fill s <$> sequenceV (content c)
+    where open RawMonad MaybeMonad
+
+record Shaped (S : Set) (C : Set → S → Set) : Set₁ where
+  field
+    arity : S → ℕ
+    content : {α : Set} {s : S} → C α s → Vec α (arity s)
+    fill : {α : Set} → (s : S) → Vec α (arity s) → C α s
+
+    isShaped : IsShaped S C arity content fill
+
+  open IsShaped isShaped public