033257afeef33dd7baa5bac9c39ce1473fd79fdf
[~helmut/bidiragda.git] / GetTypes.agda
1 module GetTypes where
2
3 open import Level using () renaming (zero to ℓ₀)
4 open import Data.Nat using (ℕ)
5 open import Data.List using (List ; map)
6 open import Data.Vec using (Vec) renaming (map to mapV)
7 open import Function using (_∘_ ; id)
8 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
9 open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
10 open import Relation.Binary using (Setoid)
11
12 open import Generic using (≡-to-Π)
13 open import Structures using (Shaped ; module Shaped)
14 open import Instances using (VecShaped)
15
16 module ListList where
17   record Get : Set₁ where
18     field
19       get : {A : Set} → List A → List A
20       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
21
22 module VecVec where
23   record Get : Set₁ where
24     field
25       getlen : ℕ → ℕ
26       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
27       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
28
29 module PartialVecVec where
30   record Get : Set₁ where
31     field
32       I : Setoid ℓ₀ ℓ₀
33       gl₁ : I ⟶ EqSetoid ℕ
34       gl₂ : I ⟶ EqSetoid ℕ
35
36     |I|   = Setoid.Carrier I
37     |gl₁| = _⟨$⟩_ gl₁
38     |gl₂| = _⟨$⟩_ gl₂
39
40     field
41       get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i)
42       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
43
44 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
45 VecVec-to-PartialVecVec G = record
46   { I = EqSetoid ℕ
47   ; gl₁ = ≡-to-Π id
48   ; gl₂ = ≡-to-Π getlen
49   ; get = get
50   ; free-theorem = free-theorem
51   } where open VecVec.Get G
52
53 module PartialShapeShape where
54   record Get : Set₁ where
55     field
56       SourceShape : Set
57       SourceContainer : Set → SourceShape → Set
58       SourceShapeT : Shaped SourceShape SourceContainer
59
60       ViewShape : Set
61       ViewContainer : Set → ViewShape → Set
62       ViewShapeT : Shaped ViewShape ViewContainer
63
64       I : Setoid ℓ₀ ℓ₀
65       gl₁ : I ⟶ EqSetoid SourceShape
66       gl₂ : I ⟶ EqSetoid ViewShape
67
68     |I|   = Setoid.Carrier I
69     |gl₁| = _⟨$⟩_ gl₁
70     |gl₂| = _⟨$⟩_ gl₂
71
72     open Shaped SourceShapeT using () renaming (fmap to fmapS)
73     open Shaped ViewShapeT using () renaming (fmap to fmapV)
74
75     field
76       get : {A : Set} {i : |I|} → SourceContainer A (|gl₁| i) → ViewContainer A (|gl₂| i)
77       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get
78
79     open Shaped SourceShapeT public using () renaming (fmap to fmapS)
80     open Shaped ViewShapeT public using () renaming (fmap to fmapV)
81
82 PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
83 PartialVecVec-to-PartialShapeShape G = record
84   { SourceShapeT = VecShaped
85   ; ViewShapeT   = VecShaped
86   ; I            = I
87   ; gl₁          = gl₁
88   ; gl₂          = gl₂
89   ; get          = get
90   ; free-theorem = free-theorem
91   } where open PartialVecVec.Get G