open import Structures using (Shaped ; module Shaped)
open import Instances using (VecShaped)
import CheckInsert
-open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeVec ; PartialShapeVec-to-PartialShapeShape)
+open import GetTypes using (VecVec-to-PartialVecVec ; PartialVecVec-to-PartialShapeShape)
module PartialShapeBFF (A : DecSetoid ℓ₀ ℓ₀) where
open GetTypes.PartialShapeShape public using (Get ; module Get)
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 j s v = PartialShapeBFF.bff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v
+ 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 j s v = PartialShapeBFF.sbff A (PartialShapeVec-to-PartialShapeShape (PartialVecVec-to-PartialShapeVec G)) j s v
+ sbff G j s v = PartialShapeBFF.sbff A (PartialVecVec-to-PartialShapeShape G) j s v
module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
open GetTypes.VecVec public using (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
-
module PartialShapeShape where
record Get : Set₁ where
field
open Shaped SourceShapeT public using () renaming (fmap to fmapS)
open Shaped ViewShapeT public using () renaming (fmap to fmapV)
-PartialShapeVec-to-PartialShapeShape : PartialShapeVec.Get → PartialShapeShape.Get
-PartialShapeVec-to-PartialShapeShape G = record
- { SourceShapeT = ShapeT
+PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
+PartialVecVec-to-PartialShapeShape G = record
+ { SourceShapeT = VecShaped
; ViewShapeT = VecShaped
; I = I
; gl₁ = gl₁
; gl₂ = gl₂
; get = get
; free-theorem = free-theorem
- } where open PartialShapeVec.Get G
+ } where open PartialVecVec.Get G