X-Git-Url: https://git.linta.de/?p=~helmut%2Fbidiragda.git;a=blobdiff_plain;f=BFFPlug.agda;h=a31d1bbb2c0d23eac1c0ebd61ac8ccbe81c011e5;hp=5c219a5c151034488d36d7b3afd072bb37c016ea;hb=dbad09a8a5843e91f862657c3011ec7f63ea819b;hpb=94f6fbed8b04e95446c38d6ea89dcc9c3a64304b;ds=sidebyside diff --git a/BFFPlug.agda b/BFFPlug.agda index 5c219a5..a31d1bb 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -11,7 +11,6 @@ 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.LeftInverse using (_RightInverseOf_) import Category.Monad open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_) @@ -37,20 +36,20 @@ bffplug G sput {i} s v | just j | yes refl with bff G j s v ... | nothing = nothing ... | just s′ = just (j , s′) -_SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set +_SimpleRightInvOf_ : {A B : Set} → (A → B) → (B → A) → Set f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g -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 (Maybe 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) +bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec (Maybe 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' ; tail' ; take') reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m) - reverse-put s v = bffinv reverse' (≡-to-Π id) (λ _ → refl) s v >>= sequenceV + reverse-put s v = bffinv reverse' id (λ _ → refl) s v >>= sequenceV drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m)) - drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl) + drop-put k = bffinv (drop' k) id (λ _ → refl) double : ℕ → ℕ double zero = zero @@ -62,10 +61,10 @@ 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 (Maybe Carrier) (double m)) - sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len + sieve-put = bffinv sieve' double sieve-inv-len tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m)) - tail-put = bffinv tail' (≡-to-Π id) (λ _ → refl) + tail-put = bffinv tail' id (λ _ → refl) take-put : (k : ℕ) → {n : ℕ} → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n)) take-put k = bffsameshape (take' k)