diff options
| -rw-r--r-- | BFFPlug.agda | 15 | ||||
| -rw-r--r-- | Examples.agda | 19 | ||||
| -rw-r--r-- | FreeTheorems.agda | 12 | ||||
| -rw-r--r-- | GetTypes.agda | 35 |
4 files changed, 37 insertions, 44 deletions
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) diff --git a/Examples.agda b/Examples.agda index ca65835..f30faa5 100644 --- a/Examples.agda +++ b/Examples.agda @@ -6,9 +6,8 @@ import Algebra.Structures open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_) open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop) open import Function using (id) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) renaming (setoid to EqSetoid) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) -open import Generic using (≡-to-Π) open import Structures using (Shaped) import GetTypes import FreeTheorems @@ -17,10 +16,10 @@ open GetTypes.PartialVecVec using (Get) open FreeTheorems.PartialVecVec using (assume-get) reverse' : Get -reverse' = assume-get (≡-to-Π id) (≡-to-Π id) reverse +reverse' = assume-get id id reverse double' : Get -double' = assume-get (≡-to-Π id) (≡-to-Π g) f +double' = assume-get id g f where g : ℕ → ℕ g zero = zero g (suc n) = suc (suc (g n)) @@ -29,19 +28,19 @@ double' = assume-get (≡-to-Π id) (≡-to-Π g) f f (x ∷ v) = x ∷ x ∷ f v double'' : Get -double'' = assume-get (≡-to-Π id) (≡-to-Π _) (λ v → v ++ v) +double'' = assume-get id _ (λ v → v ++ v) tail' : Get -tail' = assume-get (≡-to-Π suc) (≡-to-Π id) tail +tail' = assume-get suc id tail take' : ℕ → Get -take' n = assume-get (≡-to-Π (_+_ n)) (≡-to-Π _) (take n) +take' n = assume-get (_+_ n) _ (take n) drop' : ℕ → Get -drop' n = assume-get (≡-to-Π (_+_ n)) (≡-to-Π _) (drop n) +drop' n = assume-get (_+_ n) _ (drop n) sieve' : Get -sieve' = assume-get (≡-to-Π id) (≡-to-Π _) f +sieve' = assume-get id _ f where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉ f [] = [] f (x ∷ []) = x ∷ [] @@ -58,7 +57,7 @@ intersperse s (x ∷ []) = x ∷ [] intersperse s (x ∷ y ∷ v) = x ∷ s ∷ intersperse s (y ∷ v) intersperse' : Get -intersperse' = assume-get (≡-to-Π suc) (≡-to-Π intersperse-len) f +intersperse' = assume-get suc intersperse-len f where f : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A (intersperse-len n) f (s ∷ v) = intersperse s v diff --git a/FreeTheorems.agda b/FreeTheorems.agda index 08bbe88..25759e0 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -5,9 +5,7 @@ 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 Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid) -open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≗_) import GetTypes @@ -36,13 +34,13 @@ module VecVec where assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get } 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 (gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i) + get-type : {I : Set} → (I → ℕ) → (I → ℕ) → Set₁ + get-type {I} gl₁ gl₂ = {A : Set} {i : I} → Vec A (gl₁ i) → Vec A (gl₂ i) open GetTypes.PartialVecVec public postulate - 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 + free-theorem : {I : Set} → (gl₁ : I → ℕ) → (gl₂ : I → ℕ) (get : get-type gl₁ gl₂) → {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get - assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ⟶ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) (get : get-type gl₁ gl₂) → Get + assume-get : {I : Set} → (gl₁ : I → ℕ) → (gl₂ : I → ℕ) (get : get-type gl₁ gl₂) → Get assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get } diff --git a/GetTypes.agda b/GetTypes.agda index 033257a..286b9aa 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -5,11 +5,8 @@ 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 (_∘_ ; id) -open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid) -open import Relation.Binary using (Setoid) +open import Relation.Binary.PropositionalEquality using (_≗_) -open import Generic using (≡-to-Π) open import Structures using (Shaped ; module Shaped) open import Instances using (VecShaped) @@ -29,13 +26,13 @@ module VecVec where module PartialVecVec where record Get : Set₁ where field - I : Setoid ℓ₀ ℓ₀ - gl₁ : I ⟶ EqSetoid ℕ - gl₂ : I ⟶ EqSetoid ℕ + I : Set + gl₁ : I → ℕ + gl₂ : I → ℕ - |I| = Setoid.Carrier I - |gl₁| = _⟨$⟩_ gl₁ - |gl₂| = _⟨$⟩_ gl₂ + |I| = I + |gl₁| = gl₁ + |gl₂| = gl₂ field get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i) @@ -43,9 +40,9 @@ module PartialVecVec where VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get VecVec-to-PartialVecVec G = record - { I = EqSetoid ℕ - ; gl₁ = ≡-to-Π id - ; gl₂ = ≡-to-Π getlen + { I = ℕ + ; gl₁ = id + ; gl₂ = getlen ; get = get ; free-theorem = free-theorem } where open VecVec.Get G @@ -61,13 +58,13 @@ module PartialShapeShape where ViewContainer : Set → ViewShape → Set ViewShapeT : Shaped ViewShape ViewContainer - I : Setoid ℓ₀ ℓ₀ - gl₁ : I ⟶ EqSetoid SourceShape - gl₂ : I ⟶ EqSetoid ViewShape + I : Set + gl₁ : I → SourceShape + gl₂ : I → ViewShape - |I| = Setoid.Carrier I - |gl₁| = _⟨$⟩_ gl₁ - |gl₂| = _⟨$⟩_ gl₂ + |I| = I + |gl₁| = gl₁ + |gl₂| = gl₂ open Shaped SourceShapeT using () renaming (fmap to fmapS) open Shaped ViewShapeT using () renaming (fmap to fmapV) |