diff options
| -rw-r--r-- | Examples.agda | 27 | ||||
| -rw-r--r-- | FreeTheorems.agda | 10 | ||||
| -rw-r--r-- | GetTypes.agda | 14 |
3 files changed, 19 insertions, 32 deletions
diff --git a/Examples.agda b/Examples.agda index bda3ae1..ca65835 100644 --- a/Examples.agda +++ b/Examples.agda @@ -1,14 +1,11 @@ module Examples where -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉ ; pred) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉) open import Data.Nat.Properties using (cancel-+-left) import Algebra.Structures -open Algebra.Structures.IsCommutativeSemiring Data.Nat.Properties.isCommutativeSemiring using (+-isCommutativeMonoid) -open Algebra.Structures.IsCommutativeMonoid +-isCommutativeMonoid using () renaming (comm to +-comm) 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 Function.Injection using () renaming (Injection to _↪_ ; id to id↪) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) renaming (setoid to EqSetoid) open import Generic using (≡-to-Π) @@ -20,10 +17,10 @@ open GetTypes.PartialVecVec using (Get) open FreeTheorems.PartialVecVec using (assume-get) reverse' : Get -reverse' = assume-get id↪ (≡-to-Π id) reverse +reverse' = assume-get (≡-to-Π id) (≡-to-Π id) reverse double' : Get -double' = assume-get id↪ (≡-to-Π g) f +double' = assume-get (≡-to-Π id) (≡-to-Π g) f where g : ℕ → ℕ g zero = zero g (suc n) = suc (suc (g n)) @@ -32,25 +29,19 @@ double' = assume-get id↪ (≡-to-Π g) f f (x ∷ v) = x ∷ x ∷ f v double'' : Get -double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v) - -suc-injection : EqSetoid ℕ ↪ EqSetoid ℕ -suc-injection = record { to = ≡-to-Π suc; injective = cong pred } +double'' = assume-get (≡-to-Π id) (≡-to-Π _) (λ v → v ++ v) tail' : Get -tail' = assume-get suc-injection (≡-to-Π id) tail - -n+-injection : ℕ → EqSetoid ℕ ↪ EqSetoid ℕ -n+-injection n = record { to = ≡-to-Π (_+_ n); injective = cancel-+-left n } +tail' = assume-get (≡-to-Π suc) (≡-to-Π id) tail take' : ℕ → Get -take' n = assume-get (n+-injection n) (≡-to-Π _) (take n) +take' n = assume-get (≡-to-Π (_+_ n)) (≡-to-Π _) (take n) drop' : ℕ → Get -drop' n = assume-get (n+-injection n) (≡-to-Π _) (drop n) +drop' n = assume-get (≡-to-Π (_+_ n)) (≡-to-Π _) (drop n) sieve' : Get -sieve' = assume-get id↪ (≡-to-Π _) f +sieve' = assume-get (≡-to-Π id) (≡-to-Π _) f where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉ f [] = [] f (x ∷ []) = x ∷ [] @@ -67,7 +58,7 @@ intersperse s (x ∷ []) = x ∷ [] intersperse s (x ∷ y ∷ v) = x ∷ s ∷ intersperse s (y ∷ v) intersperse' : Get -intersperse' = assume-get suc-injection (≡-to-Π intersperse-len) f +intersperse' = assume-get (≡-to-Π suc) (≡-to-Π 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 d4eb174..08bbe88 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -6,10 +6,8 @@ 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 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) import GetTypes @@ -38,13 +36,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 (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i) + 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) 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 : 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 - assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → Get + assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ⟶ EqSetoid ℕ) → (gl₂ : I ⟶ EqSetoid ℕ) (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 f23d154..033257a 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -4,12 +4,10 @@ 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 Function using (_∘_ ; id) open import Function.Equality using (_⟶_ ; _⟨$⟩_) -open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪) open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid) open import Relation.Binary using (Setoid) -open Injection using (to) open import Generic using (≡-to-Π) open import Structures using (Shaped ; module Shaped) @@ -32,11 +30,11 @@ module PartialVecVec where record Get : Set₁ where field I : Setoid ℓ₀ ℓ₀ - gl₁ : I ↪ EqSetoid ℕ + gl₁ : I ⟶ EqSetoid ℕ gl₂ : I ⟶ EqSetoid ℕ |I| = Setoid.Carrier I - |gl₁| = _⟨$⟩_ (to gl₁) + |gl₁| = _⟨$⟩_ gl₁ |gl₂| = _⟨$⟩_ gl₂ field @@ -46,7 +44,7 @@ module PartialVecVec where VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get VecVec-to-PartialVecVec G = record { I = EqSetoid ℕ - ; gl₁ = id↪ + ; gl₁ = ≡-to-Π id ; gl₂ = ≡-to-Π getlen ; get = get ; free-theorem = free-theorem @@ -64,11 +62,11 @@ module PartialShapeShape where ViewShapeT : Shaped ViewShape ViewContainer I : Setoid ℓ₀ ℓ₀ - gl₁ : I ↪ EqSetoid SourceShape + gl₁ : I ⟶ EqSetoid SourceShape gl₂ : I ⟶ EqSetoid ViewShape |I| = Setoid.Carrier I - |gl₁| = _⟨$⟩_ (to gl₁) + |gl₁| = _⟨$⟩_ gl₁ |gl₂| = _⟨$⟩_ gl₂ open Shaped SourceShapeT using () renaming (fmap to fmapS) |