diff options
Diffstat (limited to 'BFF.agda')
| -rw-r--r-- | BFF.agda | 27 |
1 files changed, 21 insertions, 6 deletions
@@ -11,15 +11,19 @@ open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List ; [] ; _∷_ ; map ; length) open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) open import Function using (id ; _∘_ ; flip) -open import Relation.Binary using (DecSetoid ; module DecSetoid) +open import Function.Equality using (_⟶_ ; _⟨$⟩_) +open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪) +open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) +open import Relation.Binary.PropositionalEquality using (cong) renaming (setoid to EqSetoid) +open Injection using (to) open import FinMap -open import Generic using (mapMV) +open import Generic using (mapMV ; ≡-to-Π) import CheckInsert -import GetTypes +open import GetTypes using (VecVec-to-PartialVecVec) -module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where - open GetTypes.VecVec public using (Get) +module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where + open GetTypes.PartialVecVec public using (Get) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) open CheckInsert A @@ -33,7 +37,8 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV - bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)) + + bff : (G : Get) → ({i : Setoid.Carrier (Get.I G)} → Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i) → Vec Carrier ((Get.gl₂ G) ⟨$⟩ i) → Maybe (Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i))) bff G s v = let s′ = enumerate s t′ = Get.get G s′ g = fromFunc (denumerate s) @@ -41,3 +46,13 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where h = assoc t′ v h′ = (flip union g′) <$> h in h′ >>= flip mapMV s′ ∘ flip lookupV + +module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where + open GetTypes.VecVec public using (Get) + open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) + open CheckInsert A + + open PartialVecBFF A public using (assoc ; enumerate ; denumerate) + + bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)) + bff G = PartialVecBFF.bff A (VecVec-to-PartialVecVec G) |