From d8ed3c5d8bb02c626b3d263ed9d6a4bcb5836ae0 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 9 Jun 2015 16:33:31 +0200 Subject: drop barred members from GetTypes These became duplicates of their non-barred counterparts. --- BFF.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'BFF.agda') diff --git a/BFF.agda b/BFF.agda index 26d1d5e..e9b459a 100644 --- a/BFF.agda +++ b/BFF.agda @@ -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 -- cgit v1.2.3