define bff on a partial getlen
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 28 Jan 2014 14:15:12 +0000 (15:15 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 28 Jan 2014 14:15:12 +0000 (15:15 +0100)
The representation chosen is to give both an injection gl₁ and a
function gl₂ (formerly getlen), such that by choosing a non-identity for
gl₁ partiality of getlen can be expressed. An alternative would have
been to allow getlen to return a Maybe ℕ and have get return
  maybe (Vec A) ⊤ (getlen n)
thus sending all inputs for which getlen yields nothing to tt. It seems
that while there is no way to obtain a such a getlen predicate from an
arbitrary index Setoid I, it should be possible to manufacture a Setoid
from a predicate. Thanks to Stefan Mehner for the insightful discussion.

BFF.agda
FreeTheorems.agda

index 61eeefd..0247bde 100644 (file)
--- a/BFF.agda
+++ b/BFF.agda
@@ -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
index f37cada..aacb95a 100644 (file)
@@ -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