2812e2bea4232fc4563d19d775ab97c388a41c4b
[~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 (_∘_)
8 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
9 open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
10 open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
11 open import Relation.Binary using (Setoid)
12 open Injection using (to)
13
14 open import Generic using (≡-to-Π)
15 open import Structures using (Shaped ; module Shaped)
16 open import Instances using (VecShaped)
17
18 module ListList where
19   record Get : Set₁ where
20     field
21       get : {A : Set} → List A → List A
22       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
23
24 module VecVec where
25   record Get : Set₁ where
26     field
27       getlen : ℕ → ℕ
28       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
29       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
30
31 module PartialVecVec where
32   record Get : Set₁ where
33     field
34       I : Setoid ℓ₀ ℓ₀
35       gl₁ : I ↪ EqSetoid ℕ
36       gl₂ : I ⟶ EqSetoid ℕ
37
38     |I|   = Setoid.Carrier I
39     |gl₁| = _⟨$⟩_ (to gl₁)
40     |gl₂| = _⟨$⟩_ gl₂
41
42     field
43       get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i)
44       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
45
46 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
47 VecVec-to-PartialVecVec G = record
48   { I = EqSetoid ℕ
49   ; gl₁ = id↪
50   ; gl₂ = ≡-to-Π getlen
51   ; get = get
52   ; free-theorem = free-theorem
53   } where open VecVec.Get G
54
55 module PartialShapeVec where
56   record Get : Set₁ where
57     field
58       Shape : Set
59       Container : Set → Shape → Set
60       ShapeT : Shaped Shape Container
61
62       I : Setoid ℓ₀ ℓ₀
63       gl₁ : I ↪ EqSetoid Shape
64       gl₂ : I ⟶ EqSetoid ℕ
65
66     |I|   = Setoid.Carrier I
67     |gl₁| = _⟨$⟩_ (to gl₁)
68     |gl₂| = _⟨$⟩_ gl₂
69
70     open Shaped ShapeT using (fmap)
71
72     field
73       get : {A : Set} {i : |I|} → Container A (|gl₁| i) → Vec A (|gl₂| i)
74       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmap f ≗ mapV f ∘ get
75
76     open Shaped ShapeT public
77
78 PartialVecVec-to-PartialShapeVec : PartialVecVec.Get → PartialShapeVec.Get
79 PartialVecVec-to-PartialShapeVec G = record
80   { ShapeT       = VecShaped
81   ; I            = I
82   ; gl₁          = gl₁
83   ; gl₂          = gl₂
84   ; get          = get
85   ; free-theorem = free-theorem
86   } where open PartialVecVec.Get G
87
88 module PartialShapeShape where
89   record Get : Set₁ where
90     field
91       SourceShape : Set
92       SourceContainer : Set → SourceShape → Set
93       SourceShapeT : Shaped SourceShape SourceContainer
94
95       ViewShape : Set
96       ViewContainer : Set → ViewShape → Set
97       ViewShapeT : Shaped ViewShape ViewContainer
98
99       I : Setoid ℓ₀ ℓ₀
100       gl₁ : I ↪ EqSetoid SourceShape
101       gl₂ : I ⟶ EqSetoid ViewShape
102
103     |I|   = Setoid.Carrier I
104     |gl₁| = _⟨$⟩_ (to gl₁)
105     |gl₂| = _⟨$⟩_ gl₂
106
107     open Shaped SourceShapeT using () renaming (fmap to fmapS)
108     open Shaped ViewShapeT using () renaming (fmap to fmapV)
109
110     field
111       get : {A : Set} {i : |I|} → SourceContainer A (|gl₁| i) → ViewContainer A (|gl₂| i)
112       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get
113
114     open Shaped SourceShapeT public using () renaming (fmap to fmapS)
115     open Shaped ViewShapeT public using () renaming (fmap to fmapV)
116
117 PartialShapeVec-to-PartialShapeShape : PartialShapeVec.Get → PartialShapeShape.Get
118 PartialShapeVec-to-PartialShapeShape G = record
119   { SourceShapeT = ShapeT
120   ; ViewShapeT   = VecShaped
121   ; I            = I
122   ; gl₁          = gl₁
123   ; gl₂          = gl₂
124   ; get          = get
125   ; free-theorem = free-theorem
126   } where open PartialShapeVec.Get G