diff options
| -rw-r--r-- | BFFPlug.agda | 38 | ||||
| -rw-r--r-- | Examples.agda | 19 |
2 files changed, 29 insertions, 28 deletions
diff --git a/BFFPlug.agda b/BFFPlug.agda index 1d5570c..f463a09 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -12,46 +12,44 @@ open import Relation.Binary using (module DecSetoid) open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq) open import Relation.Nullary using (yes ; no) open import Function using (flip ; id ; _∘_) -open import Function.Equality using (_⟶_) +open import Function.Equality using (_⟶_ ; _⟨$⟩_) open import Function.LeftInverse using (_RightInverseOf_) +open import Generic using (≡-to-Π) import BFF import GetTypes import Examples open DecSetoid A using (Carrier) -open GetTypes.VecVec public using (Get) -open BFF.VecBFF A public +open GetTypes.PartialVecVec public using (Get) +open BFF.PartialVecBFF A public -bffsameshape : (G : Get) → {n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n) -bffsameshape G {n} = bff G n +bffsameshape : (G : Get) → {i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i)) +bffsameshape G {i} = bff G i -bffplug : (G : Get) → (ℕ → ℕ → Maybe ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (∃ λ l → Vec Carrier l) -bffplug G sput {n} {m} s v with sput n m +bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec Carrier (Get.|gl₁| G j)) +bffplug G sput {i} {m} s v with sput i m ... | nothing = nothing -... | just l with Get.getlen G l ≟ m -... | no getlenl≢m = nothing -bffplug G sput {n} s v | just l | yes refl with bff G l s v +... | just j with Get.|gl₂| G j ≟ m +... | no gl₂j≢m = nothing +bffplug G sput {i} s v | just j | yes refl with bff G j s v ... | nothing = nothing -... | just s′ = just (l , s′) - -as-Π : {A B : Set} → (f : A → B) → PropEq A ⟶ PropEq B -as-Π f = record { _⟨$⟩_ = f; cong = cong f } +... | just s′ = just (j , s′) _SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set -f SimpleRightInvOf g = as-Π f RightInverseOf as-Π g +f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g -bffinv : (G : Get) → (nelteg : ℕ → ℕ) → nelteg SimpleRightInvOf Get.getlen G → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (nelteg m)) -bffinv G nelteg inv {n} {m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v) +bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec Carrier (Get.|gl₁| G (nelteg ⟨$⟩ m))) +bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (sym (inv m)) v) module InvExamples where open Examples using (reverse' ; drop' ; sieve') reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m) - reverse-put = bffinv reverse' id (λ _ → refl) + reverse-put = bffinv reverse' (≡-to-Π id) (λ _ → refl) drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (m + k)) - drop-put k = bffinv (drop' k) (flip _+_ k) (flip m+n∸n≡m k) + drop-put k = bffinv (drop' k) (≡-to-Π (flip _+_ k)) (flip m+n∸n≡m k) double : ℕ → ℕ double zero = zero @@ -63,4 +61,4 @@ module InvExamples where sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x) sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m)) - sieve-put = bffinv sieve' double sieve-inv-len + sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len diff --git a/Examples.agda b/Examples.agda index 5971460..25bdbaa 100644 --- a/Examples.agda +++ b/Examples.agda @@ -2,18 +2,21 @@ module Examples where open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉) open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_) +open import Function using (id) +open import Function.Injection using () renaming (id to id↪) +open import Generic using (≡-to-Π) import GetTypes import FreeTheorems -open GetTypes.VecVec using (Get) -open FreeTheorems.VecVec using (assume-get) +open GetTypes.PartialVecVec using (Get) +open FreeTheorems.PartialVecVec using (assume-get) reverse' : Get -reverse' = assume-get reverse +reverse' = assume-get id↪ (≡-to-Π id) reverse double' : Get -double' = assume-get f +double' = assume-get id↪ (≡-to-Π g) f where g : ℕ → ℕ g zero = zero g (suc n) = suc (suc (g n)) @@ -22,24 +25,24 @@ double' = assume-get f f (x ∷ v) = x ∷ x ∷ f v double'' : Get -double'' = assume-get (λ v → v ++ v) +double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v) take' : ℕ → Get -take' n = assume-get (f n) +take' n = assume-get id↪ (≡-to-Π _) (f n) where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n) f n [] = [] f zero (x ∷ xs) = [] f (suc n) (x ∷ xs) = x ∷ f n xs drop' : ℕ → Get -drop' n = assume-get (f n) +drop' n = assume-get id↪ (≡-to-Π _) (f n) where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n) f zero xs = xs f (suc n) [] = [] f (suc n) (x ∷ xs) = f n xs sieve' : Get -sieve' = assume-get f +sieve' = assume-get id↪ (≡-to-Π _) f where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉ f [] = [] f (x ∷ []) = x ∷ [] |