0 | module Records
  1 | import Data.String
  2 | import Data.Maybe
  3 | import Data.List
  4 | import Data.List.Elem
  5 | import Data.Vect
  6 | import Data.Morphisms
  7 | import Decidable.Equality
  8 | import Data.IOArray.Prims
  9 | import Prelude
 10 |
 11 | infixr 10 :->
 12 | infixr 10 :->:
 13 | infixr 10 !!
 14 |
 15 | ||| Specification for a record, consisting of a list of key value pairs, where the value is the specification for that field.
 16 | public export
 17 | RecordSpec : Type -> Type
 18 | RecordSpec k = List (String, k)
 19 |
 20 | ||| A field (label value pair) in the record, with the given label and
 21 | ||| type.  The label is erased at the value level, but included to
 22 | ||| make it easy to see which field is used in the code.
 23 | public export
 24 | data RecordField : String -> Type -> Type where
 25 |   (:->) : (0 s:String) -> t -> RecordField s t
 26 |
 27 | ||| A field definition for a given label.
 28 | public export
 29 | data Field : String -> Type -> Type where
 30 |   (:->:) : (s:String) -> t -> Field s t
 31 |
 32 | ||| Get the specification for a single field.
 33 | public export
 34 | FieldSpec : Field s t -> t
 35 | FieldSpec (s :->: t) = t
 36 |
 37 | ||| The actual type of a field in the record.
 38 | public export
 39 | FieldToType : Type -> Type
 40 | FieldToType k = {s:String} -> Field s k -> Type
 41 |
 42 | ||| A strongly specified record.  The type contains the specification,
 43 | ||| and a function mapping that specification for each field to a
 44 | ||| concrete type.
 45 | public export
 46 | data Record : RecordSpec k -> FieldToType k -> Type where
 47 |     Nil : {0 f:FieldToType k} -> Record Nil f
 48 |     (::) :  {0 lbl:String}
 49 |          -> {0 f: FieldToType k}
 50 |          -> {0 t: k}
 51 |          -> RecordField lbl (f (lbl :->: t))
 52 |          -> Record xs f
 53 |          -> Record ((lbl, t) :: xs) f
 54 |
 55 | ||| Simple record with types as specification
 56 | public export
 57 | SimpleRecord : RecordSpec Type -> Type
 58 | SimpleRecord s = Record s FieldSpec
 59 |
 60 | ||| Constraint that holds for all values in a list.
 61 | public export
 62 | AllConstraints : (a -> Type) -> List a -> Type
 63 | AllConstraints f [] = ()
 64 | AllConstraints f (c::cs) = (f c, AllConstraints f cs)
 65 |
 66 | ||| proof that the spec has some label with the given spec
 67 | public export
 68 | data HasField : (s:String) -> (t:k) -> RecordSpec k -> Type where
 69 |   [search s]
 70 |   FirstField : HasField s t ((s, t) :: _)
 71 |   NextField : (0 prf : (t == s) === False) => HasField s v xs -> HasField s v ((t, w) :: xs)
 72 | %builtin Natural HasField
 73 |
 74 | implementation Uninhabited (HasField s t []) where
 75 |   uninhabited FirstField impossible
 76 |   uninhabited NextField impossible
 77 |
 78 | public export
 79 | HasField' : RecordSpec k -> (String, k) -> Type
 80 | HasField' r (s, t) = HasField s t r
 81 |
 82 | ||| Proof that a spec is a subset of another spec.
 83 | public export
 84 | HasFields : (l:RecordSpec k) -> RecordSpec k -> Type
 85 | HasFields l r = AllConstraints (HasField' r)  l
 86 |
 87 | ||| A label of a spec.  Contains a hidden (auto) proof that the label
 88 | ||| is actually in the RecordSpec, and a hidden reference to the field Spec.
 89 | public export
 90 | data LabelOf : RecordSpec k -> Type where
 91 |   MkLabel : {0 spec : RecordSpec k} ->
 92 |             (lbl : String) -> 
 93 |             {t : k} ->
 94 |             HasField lbl t spec =>
 95 |             LabelOf spec
 96 |
 97 | ||| Extract the string of the label
 98 | export
 99 | labelString : LabelOf spec -> String
100 | labelString (MkLabel lbl) = lbl
101 |
102 | ||| Extract the spec from the label
103 | export
104 | labelSpec : {0 spec : RecordSpec k} -> LabelOf spec -> k
105 | labelSpec (MkLabel {t} _) = t
106 |
107 | public export
108 | data IsNothing : Maybe a -> Type where
109 |   ItIsNothing : IsNothing Nothing
110 |
111 | ||| proof that an optional field with the given spec exists.  The spec
112 | ||| must be either present with the right type, or be absent.  This is
113 | ||| written in terms of HasField, so it is isomorphic to Maybe
114 | ||| Natural, which has an efficient runtime representation.
115 | public export
116 | data HasOptionalField : (s:String) -> (t:k) -> RecordSpec k -> Type where
117 |   NoSuchField : IsNothing (lookup s specs) => HasOptionalField s t specs
118 |   FieldExists : HasField s t specs => HasOptionalField  s t specs
119 |
120 | public export
121 | HasOptionalField' : RecordSpec k -> (String, k) -> Type
122 | HasOptionalField' r (s, t) = HasOptionalField s t r
123 |
124 | public export
125 | HasOptionalFields : (l:RecordSpec k) -> RecordSpec k -> Type
126 | HasOptionalFields l r = AllConstraints (HasOptionalField' r)  l
127 |
128 | export
129 | remField : RecordSpec k -> (String, k) -> RecordSpec k
130 | remField [] _ = []
131 | remField ((s, k) :: specs) (t, l) = 
132 |   if (s == t) then specs else (s, k) :: remField specs (t, l)
133 |
134 | export
135 | remFields :  (l:RecordSpec k)
136 |           -> RecordSpec k 
137 |           -> RecordSpec k
138 | remFields spec [] = spec
139 | remFields spec (x :: xs) = remFields (remField spec x) xs
140 |
141 | public export
142 | data NubFields : RecordSpec k -> RecordSpec k -> RecordSpec k ->Type where
143 |   MkNubFields : {spec:RecordSpec k} -> {fields: RecordSpec k} -> NubFields spec fields (remFields spec fields)
144 |
145 | ||| Proof that a record contains some mandatory fields, some optional
146 | ||| fields, and some remaining fields.
147 | public export
148 | data WithRecordFields :  RecordSpec k
149 |                       -> RecordSpec k 
150 |                       -> RecordSpec k
151 |                       -> RecordSpec k 
152 |                       -> Type where
153 |   MkWithRecordFields :  {spec:RecordSpec k} 
154 |                      -> {mandatory: RecordSpec k}
155 |                      -> {optional: RecordSpec k}
156 |                      -> {other: RecordSpec k}
157 |                      -> HasFields spec mandatory
158 |                      => NubFields spec (optional ++ mandatory) other
159 |                      => WithRecordFields spec mandatory optional other
160 |
161 | ||| Create an integer index of the field from the HasField proof.
162 | export
163 | hasFieldToIndex : HasField s t r -> Integer
164 | hasFieldToIndex FirstField = 0
165 | hasFieldToIndex (NextField prevField) = 1 + hasFieldToIndex prevField
166 | %builtin NaturalToInteger natToInteger
167 |
168 | ||| Get a field value by label
169 | public export
170 | get : (0 lbl:String) ->
171 |       {0 f: FieldToType k} ->
172 |       HasField lbl t r => 
173 |       Record r f -> 
174 |       (f (lbl :->: t))
175 | get s @{FirstField} ((s :-> x) :: y) = x
176 | get s @{(NextField later)} (_ :: xs) = get s @{later} xs
177 |
178 | ||| Get a field specification from the RecordSpec by label
179 | public export
180 | SpecGet : (0 lbl:String) ->
181 |           (r : RecordSpec k) ->
182 |           {t:k} ->
183 |           HasField lbl t r => 
184 |           k
185 | SpecGet lbl ((lbl, t) :: _) @{FirstField} = t
186 | SpecGet lbl ((t, w) :: xs) @{(NextField x)} = SpecGet lbl xs
187 |
188 | ||| Operator version of get with arguments flipped.
189 | export 
190 | (!!) : {0 f: FieldToType k} ->
191 |        Record r f ->
192 |        (0 lbl:String) ->
193 |        HasField lbl t r => 
194 |        (f (lbl :->: t))
195 | r !! s = get s r
196 |
197 | ||| Get an optional field from a spec, as Maybe value
198 | public export
199 | getMaybe : {0 f:FieldToType k} -> (0 s:String) -> HasOptionalField s t r => Record r f -> Maybe (f (s :->: t))
200 | getMaybe _ @{NoSuchField} _ = Nothing
201 | getMaybe s @{FieldExists} rl = Just $ get s rl
202 |
203 | ||| Get an optional field, return the given default if it is not found.
204 | public export
205 | getOpt : {0 f:FieldToType k} -> (0 s:String) -> HasOptionalField s t r => Lazy (f (s :->: t)) -> Record r f -> f (s :->: t)
206 | getOpt s def r = fromMaybe def $ getMaybe s r
207 |
208 | ||| Set a field in a record.
209 | export
210 | set : {0 f: FieldToType k} ->
211 |       {0 t : k} -> 
212 |       {0 lbl : String} ->
213 |       RecordField lbl (f (lbl :->: t)) ->
214 |       HasField lbl t r => 
215 |       Record r f -> 
216 |       Record r f
217 | set (lbl :-> x) @{FirstField} (lbl :-> _ :: r) = (lbl :-> x) :: r
218 | set x @{(NextField nf)} (y :: z) = y :: set x z
219 |
220 | ||| Map a function over all fields of a record.
221 | public export
222 | mapRecord : {specs : RecordSpec k} -> 
223 |             {0 f:FieldToType k} -> 
224 |             {0 g:FieldToType k} -> 
225 |             ({lbl:String} -> {spec : k} -> f (lbl :->: spec) -> g (lbl :->: spec)) -> 
226 |             Record specs f -> 
227 |             Record specs g
228 | mapRecord h [] = []
229 | mapRecord h ((lbl :-> y) :: z) = (lbl :-> h y) :: mapRecord h z
230 |
231 | ||| Run all the effects for each field.
232 | public export
233 | sequenceRecord : Applicative m =>
234 |                  {spec : RecordSpec k} -> 
235 |                  {0 f:FieldToType k} -> 
236 |                  Record spec (m . f) ->
237 |                  m (Record spec f)
238 | sequenceRecord [] = pure []
239 | sequenceRecord ((lbl :-> x) :: y) =
240 |   (\x', xs' => lbl :-> x' :: xs') <$> x <*> sequenceRecord y
241 |
242 | ||| Apply an effectful function over all fields of the record.
243 | public export 
244 | traverseRecord : Applicative m =>
245 |                  {specs : RecordSpec k} -> 
246 |                  {0 f:FieldToType k} -> 
247 |                  {0 g:FieldToType k} -> 
248 |                  ({lbl : String} -> 
249 |                   {spec : k} -> 
250 |                   f (lbl :->: spec) ->
251 |                   m (g (lbl :->: spec))) ->
252 |                  Record specs f ->
253 |                  m (Record specs g)
254 | traverseRecord f [] = pure []
255 | traverseRecord f ((lbl :-> x) :: y) = 
256 |   (\x', xs' => lbl :-> x' :: xs') <$> f x <*> traverseRecord f y
257 |
258 | ||| convenient specialization of sequenceRecord, to bind applicative
259 | ||| values.  Useful as replacement of applicative do in haskell.
260 | public export
261 | aseq : Applicative m =>
262 |        {spec : RecordSpec Type} -> 
263 |        Record spec (m . FieldSpec) -> 
264 |        m (SimpleRecord spec)
265 | aseq = sequenceRecord
266 |
267 | ||| Create a record by applying a function over each field in the RecordSpec.
268 | public export
269 | mapRecordSpec : {0 f : FieldToType k} -> 
270 |                 (spec:RecordSpec k) ->
271 |                 ((label:String) -> (spec:k) -> f (label :->: spec)) -> 
272 |                 Record spec f
273 | mapRecordSpec [] v = []
274 | mapRecordSpec ((s, x) :: xs) v = (s :-> v s x) :: mapRecordSpec xs v
275 |
276 | ||| Create a record by applying an effectful function over each field in the RecordSpec.
277 | public export
278 | traverseRecordSpec : Applicative m =>
279 |                      {0 f : FieldToType k} -> 
280 |                      (spec:RecordSpec k) ->
281 |                      ((label:String) -> (spec:k) -> m (f (label :->: spec))) -> 
282 |                      m (Record spec f)
283 | traverseRecordSpec [] _ = pure []
284 | traverseRecordSpec ((s, x) :: xs) f = 
285 |   (\x, xs => (s :-> x) :: xs) <$> f s x <*>  traverseRecordSpec xs f
286 |
287 | ||| Zip two records for each field in the record.
288 | public export
289 | zipWithRecord :  {spec : RecordSpec k} -> 
290 |                  {0 f : FieldToType k} ->
291 |                  {0 g : FieldToType k} ->
292 |                  {0 h : FieldToType k} ->
293 |                  ({s:String} -> {a : k} -> f (s :->: a) -> g (s :->: a) -> h (s :->: a)) ->
294 |                  Record spec f -> 
295 |                  Record spec g -> 
296 |                  Record spec h
297 | zipWithRecord f [] [] = []
298 | zipWithRecord f (s :-> x :: z) (s :-> y :: w) = 
299 |   s :-> f x y :: zipWithRecord f z w
300 |
301 | namespace Hkd
302 |   ||| Higher kinded heterogenous list
303 |   public export
304 |   data HkdList : (k -> Type) -> List k -> Type where
305 |     Nil : HkdList f []
306 |     (::) : {0 f:k -> Type} -> f a -> HkdList f b -> HkdList f (a :: b)
307 |
308 | ||| map a Hkd List
309 | export
310 | mapHkd : {0 g : k -> Type} -> (forall a . f a -> g a) -> HkdList f s -> HkdList g s
311 | mapHkd f [] = []
312 | mapHkd f (x :: y) = f x :: mapHkd f y
313 |
314 | splitRow : {0 fs : List (FieldToType k)} ->
315 |            {0 as : RecordSpec k} ->
316 |            HkdList (Record ((s, a) :: as)) fs -> 
317 |            ( HkdList ($ s :->: a) fs
318 |            , HkdList (Record as) fs)
319 | splitRow [] = ([], [])
320 | splitRow (((s :-> x) :: r) :: y) = 
321 |   let (ls, rs) = splitRow y 
322 |   in (x :: ls, r :: rs)
323 |
324 | ||| Zip a (heterogenous) list of records, by zipping each row over a
325 | ||| function.  The function takes a list of all the values in that row
326 | ||| for each of the records.
327 | export
328 | zipWithManyRecord : {0 fs : List (FieldToType k)} ->
329 |                     {g : FieldToType k} -> 
330 |                     {spec : RecordSpec k} ->
331 |                     ({s : String} -> {a : k} -> Hkd.HkdList ($ s :->: a) fs -> g (s :->: a)) ->
332 |                     Hkd.HkdList (Record spec) fs -> 
333 |                     Record spec g
334 | zipWithManyRecord f l with (spec)
335 |   _ | Nil = []
336 |   _ | ((s1, a1)::ss) =
337 |       let (l1, ls) = splitRow l
338 |       in s1 :-> f l1 :: zipWithManyRecord f ls
339 |
340 | ||| Maps each field to a value and combine them.
341 | export      
342 | foldMapRecord : Monoid m =>
343 |                 {spec : RecordSpec k} ->
344 |                 {f : FieldToType k} ->
345 |                 ({s:String} -> {a : k} -> f (s :->: a) -> m) -> 
346 |                 Record spec f -> 
347 |                 m
348 | foldMapRecord f [] = neutral
349 | foldMapRecord f ((s :-> x) :: y) = f x <+> foldMapRecord f y
350 |
351 | ||| Successively combine the fields using the provided function,
352 | ||| starting with the element that is in the final position i.e. the
353 | ||| right-most position.
354 | export
355 | foldrRecord : {f : FieldToType k} -> 
356 |               {spec : RecordSpec k} ->
357 |                ({s : String} -> {a : k} -> f (s :->: a) -> acc -> acc) -> 
358 |                acc -> 
359 |                Record spec f -> 
360 |                acc
361 | foldrRecord f acc [] = acc
362 | foldrRecord f acc ((s :-> x) :: y) =  f x $ foldrRecord f acc y
363 |
364 | ||| Successively combine the fields using the provided function,
365 | ||| starting with the element that is in the first position i.e. the
366 | ||| left-most position.
367 | export
368 | foldlRecord : {f : FieldToType k} -> 
369 |               {spec : RecordSpec k} -> 
370 |               ({s : String} -> {a : k} -> acc -> f (s :->: a) -> acc) -> 
371 |               acc -> 
372 |               Record spec f -> 
373 |               acc
374 | foldlRecord f acc [] = acc
375 | foldlRecord f acc ((s :-> x) :: y) = foldlRecord f (f acc x) y
376 |
377 | ||| create a record with all the labels of the spec.
378 | export
379 | recordLabels : {spec : RecordSpec k} -> Record spec (const String)
380 | recordLabels {spec = []} = []
381 | recordLabels {spec = ((lbl, x) :: xs)} = (lbl :-> lbl) :: recordLabels {spec = xs}
382 |
383 | ||| Type of the interface implementation for a given field.
384 | public export
385 | EntryDict : ((String, k) -> Type) -> FieldToType k
386 | EntryDict c (s :->: t) = c (s, t)
387 |
388 | ||| Create a record with the interface implementations for each field of the spec.
389 | export
390 | recordDicts : (0 c : (String, k) -> Type) -> 
391 |               (spec : RecordSpec k) -> 
392 |               (cs : AllConstraints c spec) => 
393 |               Record spec (EntryDict c)
394 | recordDicts c [] = []
395 | recordDicts c ((s, t) :: xs) {cs=(c1,_)} = s :-> c1 :: recordDicts c xs
396 |
397 | ||| Create a record with the specs for each field from the record spec.
398 | export
399 | recordSpecs : (l : RecordSpec k) -> Record l (const k)
400 | recordSpecs [] = []
401 | recordSpecs ((s, spec) :: xs) = s :-> spec :: recordSpecs xs
402 |
403 | ||| Concatenate two records
404 | export
405 | concatRecords : {spec1 : RecordSpec k} ->
406 |                 {spec2 : RecordSpec k} -> 
407 |                 {f : FieldToType k} ->
408 |                 Record spec1 f -> 
409 |                 Record spec2 f -> 
410 |                 Record (spec1 ++ spec2) f
411 | concatRecords [] y = y
412 | concatRecords (x :: z) y = x :: concatRecords z y
413 |
414 | ||| A subset of a RecordSpec, given a list of labels.
415 | public export
416 | RecordSubset : {spec : RecordSpec k} -> 
417 |                List (LabelOf spec) ->
418 |                RecordSpec k
419 | RecordSubset [] = []
420 | RecordSubset {spec} ((MkLabel {t} lbl) :: xs) =
421 |   (lbl, t) :: RecordSubset xs
422 |
423 | ||| Create a subset of a record, given a list of labels.
424 | export
425 | recordSubset : {spec : RecordSpec k} -> 
426 |                {f : FieldToType k} ->
427 |                (labels : List (LabelOf spec)) ->
428 |                Record spec f ->
429 |                Record (RecordSubset labels) f
430 | recordSubset [] r = []
431 | recordSubset ((MkLabel lbl) :: xs) r = 
432 |   (lbl :-> get lbl r) :: recordSubset xs r
433 |