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.

1 files changed, 38 insertions, 15 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)