open import FinMap
open import Generic using (mapMV)
import CheckInsert
-import FreeTheorems
+import GetTypes
module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
- open FreeTheorems.VecVec public using (Get)
+ open GetTypes.VecVec public using (Get)
open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
open CheckInsert A
open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
import Relation.Binary.EqReasoning as EqR
-import FreeTheorems
-open FreeTheorems.VecVec using (Get ; module Get)
+import GetTypes
+open GetTypes.VecVec using (Get ; module Get)
open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid)
open import FinMap
import CheckInsert
import Generic
import FinMap
import CheckInsert
+import GetTypes
import FreeTheorems
import BFF
import Bidir
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≗_)
+import GetTypes
+
module ListList where
get-type : Set₁
get-type = {A : Set} → List A → List A
- record Get : Set₁ where
- field
- get : {A : Set} → List A → List A
- free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+ open GetTypes.ListList public
postulate
free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
get-type : (ℕ → ℕ) → Set₁
get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
- record Get : Set₁ where
- field
- getlen : ℕ → ℕ
- get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
- free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+ open GetTypes.VecVec public
postulate
free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
--- /dev/null
+module GetTypes where
+
+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 (_≗_)
+
+module ListList where
+ record Get : Set₁ where
+ field
+ get : {A : Set} → List A → List A
+ free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+
+module VecVec where
+ record Get : Set₁ where
+ field
+ getlen : ℕ → ℕ
+ get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+ free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
import BFF
open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
-import FreeTheorems
-open FreeTheorems.VecVec using (Get ; module Get)
+import GetTypes
+open GetTypes.VecVec using (Get ; module Get)
open BFF.VecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)
lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup f (map Maybe.just v) ≡ Maybe.just (lookup f v)