1
------------------------------------------------------------------------
2
-- The Agda standard library
4
-- Record types with manifest fields and "with", based on Randy
5
-- Pollack's "Dependently Typed Records in Type Theory"
6
------------------------------------------------------------------------
8
-- For an example of how this module can be used, see README.Record.
10
-- The module is parametrised by the type of labels, which should come
11
-- with decidable equality.
13
open import Relation.Binary
14
open import Relation.Binary.PropositionalEquality
16
module Record (Label : Set) (_≟_ : Decidable (_≡_ {A = Label})) where
19
open import Data.Empty
21
open import Data.Product hiding (proj₁; proj₂)
23
open import Function hiding (type-signature)
25
open import Relation.Nullary
26
open import Relation.Nullary.Decidable
28
------------------------------------------------------------------------
29
-- A Σ-type with a manifest field
31
-- A variant of Σ where the value of the second field is "manifest"
32
-- (given by the first).
36
record Manifest-Σ {a b} (A : Set a) {B : A → Set b}
37
(f : (x : A) → B x) : Set a where
44
------------------------------------------------------------------------
45
-- Signatures and records
51
data Signature s : Set (suc s) where
53
_,_∶_ : (Sig : Signature s)
55
(A : Record Sig → Set s) →
57
_,_≔_ : (Sig : Signature s)
59
{A : Record Sig → Set s}
60
(a : (r : Record Sig) → A r) →
63
-- Record is a record type to ensure that the signature can be
64
-- inferred from a value of type Record Sig.
66
record Record {s} (Sig : Signature s) : Set s where
68
field fun : Record-fun Sig
70
Record-fun : ∀ {s} → Signature s → Set s
72
Record-fun (Sig , ℓ ∶ A) = Σ (Record Sig) A
73
Record-fun (Sig , ℓ ≔ a) = Manifest-Σ (Record Sig) a
75
------------------------------------------------------------------------
76
-- Variants of Signature and Record
78
-- It may be easier to define values of type Record′ (Sig⇒Sig′ Sig)
79
-- than of type Record Sig.
83
data Signature′ s : Set (suc s) where
85
_,_∶_ : (Sig : Signature′ s)
87
(A : Record′ Sig → Set s) →
89
_,_≔_ : (Sig : Signature′ s)
91
{A : Record′ Sig → Set s}
92
(a : (r : Record′ Sig) → A r) →
95
Record′ : ∀ {s} → Signature′ s → Set s
97
Record′ (Sig , ℓ ∶ A) = Σ (Record′ Sig) A
98
Record′ (Sig , ℓ ≔ a) = Manifest-Σ (Record′ Sig) a
100
-- We can convert between the two kinds of signatures/records.
104
Sig′⇒Sig : ∀ {s} → Signature′ s → Signature s
106
Sig′⇒Sig (Sig , ℓ ∶ A) = Sig′⇒Sig Sig , ℓ ∶ (A ∘ Rec⇒Rec′ _)
107
Sig′⇒Sig (Sig , ℓ ≔ a) = Sig′⇒Sig Sig , ℓ ≔ (a ∘ Rec⇒Rec′ _)
109
Rec⇒Rec′ : ∀ {s} (Sig : Signature′ s) →
110
Record (Sig′⇒Sig Sig) → Record′ Sig
111
Rec⇒Rec′ ∅ (rec r) = r
112
Rec⇒Rec′ (Sig , ℓ ∶ A) (rec r) = (Rec⇒Rec′ _ (Σ.proj₁ r) , Σ.proj₂ r)
113
Rec⇒Rec′ (Sig , ℓ ≔ a) (rec r) = (Rec⇒Rec′ _ (Manifest-Σ.proj₁ r) ,)
117
Sig⇒Sig′ : ∀ {s} → Signature s → Signature′ s
119
Sig⇒Sig′ (Sig , ℓ ∶ A) = Sig⇒Sig′ Sig , ℓ ∶ (A ∘ Rec′⇒Rec _)
120
Sig⇒Sig′ (Sig , ℓ ≔ a) = Sig⇒Sig′ Sig , ℓ ≔ (a ∘ Rec′⇒Rec _)
122
Rec′⇒Rec : ∀ {s} (Sig : Signature s) →
123
Record′ (Sig⇒Sig′ Sig) → Record Sig
125
Rec′⇒Rec (Sig , ℓ ∶ A) r = rec (Rec′⇒Rec _ (Σ.proj₁ r) , Σ.proj₂ r)
126
Rec′⇒Rec (Sig , ℓ ≔ a) r = rec (Rec′⇒Rec _ (Manifest-Σ.proj₁ r) ,)
128
------------------------------------------------------------------------
131
-- A signature's labels, starting with the last one.
133
labels : ∀ {s} → Signature s → List Label
135
labels (Sig , ℓ ∶ A) = ℓ ∷ labels Sig
136
labels (Sig , ℓ ≔ a) = ℓ ∷ labels Sig
138
-- Inhabited if the label is part of the signature.
142
_∈_ : ∀ {s} → Label → Signature s → Set
144
foldr (λ ℓ′ → if ⌊ ℓ ≟ ℓ′ ⌋ then (λ _ → ⊤) else id) ⊥ (labels Sig)
146
------------------------------------------------------------------------
149
-- Signature restriction and projection. (Restriction means removal of
150
-- a given field and all subsequent fields.)
152
Restrict : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig →
155
Restrict (Sig , ℓ′ ∶ A) ℓ ℓ∈ with ℓ ≟ ℓ′
157
... | no _ = Restrict Sig ℓ ℓ∈
158
Restrict (Sig , ℓ′ ≔ a) ℓ ℓ∈ with ℓ ≟ ℓ′
160
... | no _ = Restrict Sig ℓ ℓ∈
162
Restricted : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig → Set s
163
Restricted Sig ℓ ℓ∈ = Record (Restrict Sig ℓ ℓ∈)
165
Proj : ∀ {s} (Sig : Signature s) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
166
Restricted Sig ℓ ℓ∈ → Set s
168
Proj (Sig , ℓ′ ∶ A) ℓ with ℓ ≟ ℓ′
170
... | no _ = Proj Sig ℓ
171
Proj (_,_≔_ Sig ℓ′ {A = A} a) ℓ with ℓ ≟ ℓ′
173
... | no _ = Proj Sig ℓ
175
-- Record restriction and projection.
179
_∣_ : ∀ {s} {Sig : Signature s} → Record Sig →
180
(ℓ : Label) {ℓ∈ : ℓ ∈ Sig} → Restricted Sig ℓ ℓ∈
182
_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ with ℓ ≟ ℓ′
183
... | yes _ = Σ.proj₁ r
184
... | no _ = Σ.proj₁ r ∣ ℓ
185
_∣_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ with ℓ ≟ ℓ′
186
... | yes _ = Manifest-Σ.proj₁ r
187
... | no _ = Manifest-Σ.proj₁ r ∣ ℓ
191
_·_ : ∀ {s} {Sig : Signature s} (r : Record Sig)
192
(ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
193
Proj Sig ℓ {ℓ∈} (r ∣ ℓ)
195
_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ with ℓ ≟ ℓ′
196
... | yes _ = Σ.proj₂ r
197
... | no _ = Σ.proj₁ r · ℓ
198
_·_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ with ℓ ≟ ℓ′
199
... | yes _ = Manifest-Σ.proj₂ r
200
... | no _ = Manifest-Σ.proj₁ r · ℓ
202
------------------------------------------------------------------------
205
-- Sig With ℓ ≔ a is the signature Sig, but with the ℓ field set to a.
211
_With_≔_ : ∀ {s} (Sig : Signature s) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
212
((r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ r) → Signature s
214
Sig , ℓ′ ∶ A With ℓ ≔ a with ℓ ≟ ℓ′
215
... | yes _ = Sig , ℓ′ ≔ a
216
... | no _ = Sig With ℓ ≔ a , ℓ′ ∶ A ∘ drop-With
217
Sig , ℓ′ ≔ a′ With ℓ ≔ a with ℓ ≟ ℓ′
218
... | yes _ = Sig , ℓ′ ≔ a
219
... | no _ = Sig With ℓ ≔ a , ℓ′ ≔ a′ ∘ drop-With
221
drop-With : ∀ {s} {Sig : Signature s} {ℓ : Label} {ℓ∈ : ℓ ∈ Sig}
222
{a : (r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ r} →
223
Record (Sig With ℓ ≔ a) → Record Sig
224
drop-With {Sig = ∅} {ℓ∈ = ()} r
225
drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} (rec r) with ℓ ≟ ℓ′
226
... | yes _ = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r)
227
... | no _ = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r)
228
drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} (rec r) with ℓ ≟ ℓ′
229
... | yes _ = rec (Manifest-Σ.proj₁ r ,)
230
... | no _ = rec (drop-With (Manifest-Σ.proj₁ r) ,)
added
removed
src/Record.agda
