port to agda/2.6.0.1 and agda-stdlib/1.1
[~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       get : {A : Set} {i : I} → Vec A (gl₁ i) → Vec A (gl₂ i)
33       free-theorem : {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
34
35 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
36 VecVec-to-PartialVecVec G = record
37   { I = ℕ
38   ; gl₁ = id
39   ; gl₂ = getlen
40   ; get = get
41   ; free-theorem = free-theorem
42   } where open VecVec.Get G
43
44 module PartialShapeShape where
45   record Get : Set₁ where
46     field
47       SourceShape : Set
48       SourceContainer : Set → SourceShape → Set
49       SourceShapeT : Shaped SourceShape SourceContainer
50
51       ViewShape : Set
52       ViewContainer : Set → ViewShape → Set
53       ViewShapeT : Shaped ViewShape ViewContainer
54
55       I : Set
56       gl₁ : I → SourceShape
57       gl₂ : I → ViewShape
58
59     open Shaped SourceShapeT using () renaming (fmap to fmapS)
60     open Shaped ViewShapeT using () renaming (fmap to fmapV)
61
62     field
63       get : {A : Set} {i : I} → SourceContainer A (gl₁ i) → ViewContainer A (gl₂ i)
64       free-theorem : {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get
65
66     open Shaped SourceShapeT public using () renaming (fmap to fmapS)
67     open Shaped ViewShapeT public using () renaming (fmap to fmapV)
68
69 PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
70 PartialVecVec-to-PartialShapeShape G = record
71   { SourceShapeT = VecShaped
72   ; ViewShapeT   = VecShaped
73   ; I            = I
74   ; gl₁          = gl₁
75   ; gl₂          = gl₂
76   ; get          = get
77   ; free-theorem = free-theorem
78   } where open PartialVecVec.Get G