0 | ||| The WithData module combines a record and an arbitrary payload. The intended use is to
1 | ||| attach metadata to the payload.
9 | %hide Data.List.Quantifiers.Any.Any
10 | %hide Data.List.Quantifiers.Any.any
12 | ||| A pair for a type and an attached record hosting metadata about that type
13 | |||
14 | ||| Intended usage
15 | ||| --------------
16 | ||| Only ever put plain types in the metadata
17 | ||| Do not add functors such as `List` or `PTerm`. The functor instance
18 | ||| for `WithData` is only functorial on its payload and not the metadata.
19 | |||
20 | ||| There is rarely any need to write down `WithData [ ... ] a` thanks to the
21 | ||| `AddMetadata` type constructor.
22 | |||
23 | ||| While possible, you are not meant to pattern match on values of this type
24 | ||| to extract the main payload, you can use the `val` projection, and to access
25 | ||| metadata fields you can use `get` and `getAt` functions that will automatically
26 | ||| compute and extract the value out of the metadata record.
27 | |||
28 | ||| Example usage
29 | ||| -------------
30 | ||| Given a value of type `value : WithData ["loc" :-: Location, "cached" :-: Bool] Term`
31 | ||| we can access the `Term` by projecting our the underlying value:
32 | ||| ```idris example
33 | ||| termValue : Term
34 | ||| termValue = value.val
35 | ||| ```
36 | ||| To access the metadata fields use `get` with the name of the field or `getAt` with
37 | ||| the index of the field. For example "loc" is at index `0` therefore one can access
38 | ||| it using `getAt 0`:
39 | ||| ```idris example
40 | ||| termLocation : Location
41 | ||| termLocation = value `getAt` 0
42 | ||| ```
43 | ||| Similarly, we can obtain the "cached" field by giving its name directly
44 | ||| ```idris example
45 | ||| termCache : Bool
46 | ||| termCache = value.get "cached"
47 | ||| ```
54 | ||| Add some metadata to a type given a label and a type for the metadata
55 | ||| This function matches on the type and add it to the metadata record if it is alread a `WithData`
56 | |||
57 | ||| example:
58 | ||| ```idris example
59 | ||| Term : Type
60 | |||
61 | ||| RichTerm : Type
62 | ||| RichTerm = AddMetadata ("loc" :-: Location) $ AddMetadata ("cached" :-: Bool) Term
63 | ||| ```
64 | ||| The example shows how to add the fields "loc" and "cached" to the type `Term` as metadata. Those
65 | ||| fields can be accessed with `get` and `getAt` functions
71 | ||| Obtain the value of the metadata at the given index
72 | ||| @ ix The index of the value we are extracting
73 | ||| @ inRange A proof the index is in range of the metadata record
74 | export
80 | ||| Obtain the value out of the payload record given its label, same as `(.get)`
81 | ||| @ label The label of the value we are extracting
82 | ||| @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.
83 | export
86 | -- ^ The field we are accessing
88 | -- ^ The index of the field, this can usually be infered
90 | -- ^ A proof that the field is in the record, its position matches the index `n` and the type at that location is `out`
92 | -- ^ The data from which we are extracting the field
93 | out
96 | ||| Obtain the value out of the payload record given its label, same as `get`.
97 | ||| @ label The label of the value we are extracting.
98 | ||| @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.
99 | export
102 | -- ^ The data from which we are extracting the field
104 | -- ^ The field we are accessing
106 | -- ^ The index of the field, this can usually be infered
108 | -- ^ A proof that the field is in the record, its position matches the index `n` and the type at that location is `out`
109 | out
112 | ||| Update at the given index, updates cannot change the type of the field.
113 | ||| @ ix The index at which we update the value.
114 | ||| @ inRange A proof that the index is in range of the metadata record.
115 | ||| @ f The update function.
116 | export
119 | -- ^ The index selected for updating
121 | -- ^ The proof that the index is in range
123 | -- ^ The update function.
127 | ||| Update the value with the given field name
128 | ||| @ label The label of the value we are updating
129 | ||| @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.
130 | ||| @ f The update function.
131 | export
134 | -- ^ The field we want to update
136 | -- ^ The index of the field, this can usually be infered
138 | -- ^ A proof that the field is in the record, its position matches the index `n` and the type at that location is `out`
140 | -- ^ The update function for the field
142 | -- ^ The data for which we are updating the field
146 | ||| Override the value at the given index.
147 | ||| @ n The index at which we replace our value.
148 | ||| @ inRange A proof that index is in range.
149 | ||| @ newVal The new value remplacing the existing one.
150 | export
153 | -- ^ The index at which we override our value
155 | -- ^ A proof that the index is in range
157 | -- ^ The new value that is going to replace the old one
159 | -- ^ The data for which we are overriding a value
163 | ||| Override the value matching the given label
164 | ||| @ label The label of the value we are overriding.
165 | ||| @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.
166 | ||| @ newVal The new value remplacing the existing one.
167 | export
176 | ||| Add a labelled value to the metadata
177 | export
181 | ||| Add value the payload, ignore the label since it's given by the type
182 | export
188 | ||| Drop the head element of the metadata
189 | export
193 | ||| Drop the head element of the metadata
194 | export
198 | ||| WithData is functiorial in its payload
199 | export
203 | ------------------------------------------------------------------------------------------------
204 | -- Default fields for records
205 | ------------------------------------------------------------------------------------------------
207 | ||| An interface for default values, used to fill in missing values in metadata records
216 | ||| Construct a payload filled with default values for its metadata
217 | export
221 | ||| Construct a value with metadata but ignore the labels
222 | export
226 | ||| Add a default value to an existing metadata record
227 | export
232 | ------------------------------------------------------------------------------------------------
233 | -- WithData distributes with List and Maybe
234 | ------------------------------------------------------------------------------------------------
236 | export
240 | export
245 | export
249 | ------------------------------------------------------------------------------------------------
250 | -- Interface implementations
251 | ------------------------------------------------------------------------------------------------
253 | export
258 | export