drop the Function.Equality requirement from GetTypes
[~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 Relation.Binary.PropositionalEquality using (_≗_)
9
10 open import Structures using (Shaped ; module Shaped)
11 open import Instances using (VecShaped)
12
13 module ListList where
14   record Get : Set₁ where
15     field
16       get : {A : Set} → List A → List A
17       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
18
19 module VecVec where
20   record Get : Set₁ where
21     field
22       getlen : ℕ → ℕ
23       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
24       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
25
26 module PartialVecVec where
27   record Get : Set₁ where
28     field
29       I : Set
30       gl₁ : I → ℕ
31       gl₂ : I → ℕ
32
33     |I|   = I
34     |gl₁| = gl₁
35     |gl₂| = gl₂
36
37     field
38       get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i)
39       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
40
41 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
42 VecVec-to-PartialVecVec G = record
43   { I = ℕ
44   ; gl₁ = id
45   ; gl₂ = getlen
46   ; get = get
47   ; free-theorem = free-theorem
48   } where open VecVec.Get G
49
50 module PartialShapeShape where
51   record Get : Set₁ where
52     field
53       SourceShape : Set
54       SourceContainer : Set → SourceShape → Set
55       SourceShapeT : Shaped SourceShape SourceContainer
56
57       ViewShape : Set
58       ViewContainer : Set → ViewShape → Set
59       ViewShapeT : Shaped ViewShape ViewContainer
60
61       I : Set
62       gl₁ : I → SourceShape
63       gl₂ : I → ViewShape
64
65     |I|   = I
66     |gl₁| = gl₁
67     |gl₂| = gl₂
68
69     open Shaped SourceShapeT using () renaming (fmap to fmapS)
70     open Shaped ViewShapeT using () renaming (fmap to fmapV)
71
72     field
73       get : {A : Set} {i : |I|} → SourceContainer A (|gl₁| i) → ViewContainer A (|gl₂| i)
74       free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get
75
76     open Shaped SourceShapeT public using () renaming (fmap to fmapS)
77     open Shaped ViewShapeT public using () renaming (fmap to fmapV)
78
79 PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
80 PartialVecVec-to-PartialShapeShape G = record
81   { SourceShapeT = VecShaped
82   ; ViewShapeT   = VecShaped
83   ; I            = I
84   ; gl₁          = gl₁
85   ; gl₂          = gl₂
86   ; get          = get
87   ; free-theorem = free-theorem
88   } where open PartialVecVec.Get G