diff options
| -rw-r--r-- | BFF.agda | 22 | ||||
| -rw-r--r-- | FreeTheorems.agda | 27 |
2 files changed, 46 insertions, 3 deletions
@@ -11,7 +11,11 @@ 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 _↪_) +open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) +open import Relation.Binary.PropositionalEquality using () renaming (setoid to EqSetoid) +open Injection using (to) open import FinMap open import Generic using (mapMV) @@ -41,3 +45,19 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where h = assoc t′ v h′ = (flip union g′) <$> h in h′ >>= flip mapMV s′ ∘ flip lookupV + +module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where + open FreeTheorems.PartialVecVec public using (get-type) + open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) + open CheckInsert A + + open VecBFF A public using (assoc ; enumerate ; denumerate) + + bff : {I : Setoid ℓ₀ ℓ₀} {gl₁ : I ↪ (EqSetoid ℕ)} {gl₂ : I ⟶ EqSetoid ℕ} → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i))) + bff get s v = let s′ = enumerate s + t′ = get s′ + g = fromFunc (denumerate s) + g′ = delete-many t′ g + h = assoc t′ v + h′ = (flip union g′) <$> h + in h′ >>= flip mapMV s′ ∘ flip lookupV diff --git a/FreeTheorems.agda b/FreeTheorems.agda index f37cada..aacb95a 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -1,10 +1,15 @@ module FreeTheorems where +open import Level using () renaming (zero to ℓ₀) open import Data.Nat using (ℕ) open import Data.List using (List ; map) open import Data.Vec using (Vec) renaming (map to mapV) open import Function using (_∘_) -open import Relation.Binary.PropositionalEquality using (_≗_) +open import Function.Equality using (_⟶_ ; _⟨$⟩_) +open import Function.Injection using (module Injection) renaming (Injection to _↪_) +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid) +open import Relation.Binary using (Setoid) +open Injection using (to) module ListList where get-type : Set₁ @@ -17,5 +22,23 @@ module VecVec where get-type : (ℕ → ℕ) → Set₁ get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) + free-theorem-type : Set₁ + free-theorem-type = {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get + + postulate + free-theorem : free-theorem-type + +module PartialVecVec where + get-type : {I : Setoid ℓ₀ ℓ₀} → (I ↪ (EqSetoid ℕ)) → (I ⟶ (EqSetoid ℕ)) → Set₁ + get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i) + postulate - free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get + free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get + + open VecVec using () renaming (free-theorem-type to VecVec-free-theorem-type) + + ≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B + ≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f } + + VecVec-free-theorem : VecVec-free-theorem-type + VecVec-free-theorem {getlen} get = free-theorem Function.Injection.id (≡-to-Π getlen) get |