implement a bff on a shaped source type
[~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