drop PartialShapeVec
[~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 PartialShapeShape where
56   record Get : Set₁ where
57     field
58       SourceShape : Set
59       SourceContainer : Set → SourceShape → Set
60       SourceShapeT : Shaped SourceShape SourceContainer
61
62       ViewShape : Set
63       ViewContainer : Set → ViewShape → Set
64       ViewShapeT : Shaped ViewShape ViewContainer
65
66       I : Setoid ℓ₀ ℓ₀
67       gl₁ : I ↪ EqSetoid SourceShape
68       gl₂ : I ⟶ EqSetoid ViewShape
69
70     |I|   = Setoid.Carrier I
71     |gl₁| = _⟨$⟩_ (to gl₁)
72     |gl₂| = _⟨$⟩_ gl₂
73
74     open Shaped SourceShapeT using () renaming (fmap to fmapS)
75     open Shaped ViewShapeT using () renaming (fmap to fmapV)
76
77     field
78       get : {A : Set} {i : |I|} → SourceContainer A (|gl₁| i) → ViewContainer A (|gl₂| i)
79       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get
80
81     open Shaped SourceShapeT public using () renaming (fmap to fmapS)
82     open Shaped ViewShapeT public using () renaming (fmap to fmapV)
83
84 PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
85 PartialVecVec-to-PartialShapeShape G = record
86   { SourceShapeT = VecShaped
87   ; ViewShapeT   = VecShaped
88   ; I            = I
89   ; gl₁          = gl₁
90   ; gl₂          = gl₂
91   ; get          = get
92   ; free-theorem = free-theorem
93   } where open PartialVecVec.Get G