diff options
Diffstat (limited to 'BFF.agda')
| -rw-r--r-- | BFF.agda | 14 |
1 files changed, 7 insertions, 7 deletions
@@ -36,18 +36,18 @@ module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where 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.SourceContainer G Carrier (Get.|gl₁| G i) → Get.ViewContainer G Carrier (Get.|gl₂| G j) → Maybe (Get.SourceContainer G (Maybe Carrier) (Get.|gl₁| G j)) - bff G {i} j s v = let s′ = enumerate SourceShapeT (|gl₁| i) + bff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Get.SourceContainer G Carrier (Get.gl₁ G i) → Get.ViewContainer G Carrier (Get.gl₂ G j) → Maybe (Get.SourceContainer G (Maybe Carrier) (Get.gl₁ G j)) + bff G {i} j s v = let s′ = enumerate SourceShapeT (gl₁ i) t′ = get s′ g = fromFunc (denumerate SourceShapeT s) g′ = delete-many (Shaped.content ViewShapeT t′) g - t = enumerate SourceShapeT (|gl₁| j) + t = enumerate SourceShapeT (gl₁ j) h = assoc (Shaped.content ViewShapeT (get t)) (Shaped.content ViewShapeT v) - h′ = (flip union (reshape g′ (Shaped.arity SourceShapeT (|gl₁| j)))) <$> h + h′ = (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j)))) <$> h in ((λ f → fmapS f t) ∘ flip lookupM) <$> h′ where open Get G - sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Get.SourceContainer G Carrier (Get.|gl₁| G i) → Get.ViewContainer G Carrier (Get.|gl₂| G j) → Maybe (Get.SourceContainer G Carrier (Get.|gl₁| G j)) + sbff : (G : Get) → {i : Get.I G} → (j : Get.I G) → Get.SourceContainer G Carrier (Get.gl₁ G i) → Get.ViewContainer G Carrier (Get.gl₂ G j) → Maybe (Get.SourceContainer G Carrier (Get.gl₁ G j)) sbff G j s v = bff G j s v >>= Shaped.sequence (Get.SourceShapeT G) module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where @@ -66,10 +66,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier 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 : 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 j s v = PartialShapeBFF.bff A (PartialVecVec-to-PartialShapeShape 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 : 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 = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeShape G) j s v module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where |