0 | ||| Modular records based on `All`
  1 | module Libraries.Data.Record
  2 |
  3 | import public Data.List.Quantifiers
  4 | import Data.Maybe
  5 |
  6 | %hide Data.List.Quantifiers.Any.Any
  7 | %hide Data.List.Quantifiers.Any.any
  8 |
  9 | export infixr 9 :-:
 10 | export infix 9 :-
 11 | export infixr 9 :+
 12 |
 13 | ||| A type with a string-label for it. Used in `Record`
 14 | |||
 15 | ||| ```idris example
 16 | ||| IntLabel : KeyVal
 17 | ||| IntLabel = "int" :-: Int
 18 | ||| ```
 19 | public export
 20 | record KeyVal where
 21 |   constructor (:-:)
 22 |   label : String
 23 |   type : Type
 24 |
 25 | ||| The value-constructor for `KeyVal`, essentially a pair of a label
 26 | ||| and a value that match the specification given by `KeyVal`
 27 | |||
 28 | ||| ```idris example
 29 | ||| IntLabel : KeyVal
 30 | ||| IntLabel = "int" :-: Int
 31 | |||
 32 | ||| intValue : LabelledValue IntLabel
 33 | ||| intValue = "int" :- 3
 34 | ||| ```
 35 | public export
 36 | record LabelledValue (kv : KeyVal) where
 37 |   constructor (:-)
 38 |   ||| The label matching the `KeyVal` spec, erased for performance reasons
 39 |   0 label : String
 40 |   ||| A proof that the label given matches the label in the specification
 41 |   {auto 0 check : kv.label === label}
 42 |   ||| A runtime value of the type given by the specification
 43 |   value : kv.type
 44 |
 45 | ||| Records are a list of of labelled values, their fields are given by a list of KeyVal
 46 | ||| Each element in the list describes a key
 47 | |||
 48 | ||| ```idris example
 49 | ||| Spec : List KeyVal
 50 | ||| Spec = [ "username" :-: String, "amount" :-: Double ]
 51 | |||
 52 | ||| recordValue : Record Spec
 53 | ||| recordValue = [ "username" :- "Alice", "amount" :- 3.14 ]
 54 | ||| ```
 55 | public export
 56 | Record : (fields : List KeyVal) -> Type
 57 | Record = All LabelledValue
 58 |
 59 | ||| Build a record from it's element values ignoring the labels
 60 | |||
 61 | ||| ```idris example
 62 | ||| Spec : List KeyVal
 63 | ||| Spec = [ "username" :-: String, "amount" :-: Double ]
 64 | |||
 65 | ||| recordValue : Record Spec
 66 | ||| recordValue = fromElems [ "Alice", 3.14 ]
 67 | ||| ```
 68 | export
 69 | fromElems : {fs : _} -> All KeyVal.type fs -> Record fs
 70 | fromElems {fs = []} [] = []
 71 | fromElems {fs = (l :-: t :: xs)} (x :: zs) = (l :- x) :: fromElems zs
 72 |
 73 | ||| Obtain the tail of a list of predicates
 74 | export
 75 | tail : All p (x :: xs) -> All p xs
 76 | tail (_ :: xs) = xs
 77 |
 78 | ||| A procedue to find the type at the given index
 79 | public export 0
 80 | FindIndex : Nat -> List KeyVal -> Maybe Type
 81 | FindIndex Z (x :: xs) = Just x.type
 82 | FindIndex (S n) (x :: xs) = FindIndex n xs
 83 | FindIndex _ _ = Nothing
 84 |
 85 | ||| A procedure to find the index and type of a given label
 86 | public export 0
 87 | NameInRange : (key : String) -> List KeyVal -> Maybe (Nat, Type)
 88 | NameInRange key [] = Nothing
 89 | NameInRange key (x :: xs) = if (key == x.label)
 90 |                                then Just (Z, x.type)
 91 |                                else map (mapFst S) (NameInRange key xs)
 92 |
 93 | -- Convert a `NameInRange` proof to a `FindIndex` proof
 94 | 0
 95 | IndexInRange : {fields : List KeyVal} ->
 96 |                NameInRange key fields === Just (ix, ty) ->
 97 |                FindIndex ix fields === Just ty
 98 | IndexInRange {fields = []} prf = absurd prf
 99 | IndexInRange {fields = ((label :-: type) :: xs)} {ty} prf with (key == label)
100 |   IndexInRange {fields = ((label :-: type) :: xs)} {ty} prf | False with (NameInRange key xs) proof p
101 |     IndexInRange {fields = ((label :-: type) :: xs)} {ty} prf | False | Nothing = absurd prf
102 |     IndexInRange {fields = ((label :-: type) :: xs)} {ty} Refl | False | (Just (x, ty))
103 |       = IndexInRange {fields = xs, key} p
104 |   IndexInRange {fields = ((label :-: type) :: xs)} {ty = type} Refl | True = Refl
105 |
106 | ||| Add a label and a value to a record
107 | export
108 | add : (0 str : String) -> (_ : ty) -> Record fields -> Record (str :-: ty :: fields)
109 | add str val xs = (str :- val) :: xs
110 |
111 | absurd0 : (0 _ : t) -> Uninhabited t => a
112 | absurd0 x = void (uninhabited x)
113 |
114 | ||| Obtain the value from a record at given index
115 | ||| @ n The index at which we extract the value.
116 | ||| @ out The type of the value at the index.
117 | ||| @ inRange A proof that the field is in the record at the appropriate index with the appropriate type.
118 | export
119 | index : Record fields -> (n : Nat) -> (0 inRange : FindIndex n fields === Just out) => out
120 | index ((label :- val) :: y) 0 {inRange = Refl} = val
121 | index (x :: y) (S k) = index y k
122 | index [] 0 = absurd0 inRange
123 | index [] (S k) = absurd0 inRange
124 |
125 | ||| Obtain the value from a record given its label.
126 | ||| @ field The field for which we extract the value.
127 | ||| @ n The index corresponding to the field given.
128 | ||| @ out The type of the value at the given field.
129 | ||| @ inRange A proof that the field is in the record at the appropriate index with the appropriate type.
130 | export
131 | get : (0 label : String) -> Record fields ->
132 |       {n : Nat} ->
133 |       (0 inRange : NameInRange label fields === Just (n, out)) => out
134 | get field rec = index rec n {inRange = IndexInRange inRange}
135 |
136 | ||| Obtain the value from a record given its label and type.
137 | ||| @ field The field for which we extract the value.
138 | ||| @ out The type of the value at the given field.
139 | ||| @ n The index corresponding to the field given.
140 | ||| @ inRange A proof that the field is in the record at the appropriate index with the appropriate type.
141 | export
142 | get' : (0 label : String) -> (0 out : Type) -> Record fields ->
143 |        {n : Nat} ->
144 |        (0 inRange : NameInRange label fields === Just (n, out)) =>
145 |        out
146 | get' label type rec = get {n} label {out = type} rec {inRange = inRange}
147 |
148 | ||| Remove a value from the list, used in the type of `removeAt`
149 | public export
150 | ListRemoveAt :
151 |     (fields : List KeyVal) -> (n : Nat) ->
152 |     (inRange : IsJust (FindIndex n fields)) => List KeyVal
153 | ListRemoveAt [] 0 = absurd inRange
154 | ListRemoveAt (x :: xs) 0 = xs
155 | ListRemoveAt [] (S k) = absurd inRange
156 | ListRemoveAt (x :: xs) (S k) = x :: ListRemoveAt xs k
157 |
158 | ||| Remove the value at the given index.
159 | ||| @ n The index we are removing.
160 | ||| @ inRange A proof that the index is in range of the record spec.
161 | export
162 | removeAt :
163 |     (n : Nat) ->
164 |     (inRange : IsJust (FindIndex n fields)) =>
165 |     Record fields -> Record (ListRemoveAt fields n)
166 | removeAt 0 [] = absurd inRange
167 | removeAt 0 (x :: z) = z
168 | removeAt (S k) [] = absurd inRange
169 | removeAt (S k) (x :: xs) = x :: removeAt k xs
170 |
171 | ||| Update the value at the given index.
172 | ||| @ n The index we are removing.
173 | ||| @ inRange A proof that the index is in range of the record spec.
174 | ||| @ f The update function.
175 | export
176 | updateAt :
177 |     (n : Nat) ->
178 |     (0 inRange : (FindIndex n fields) === Just out) =>
179 |     (f : out -> out) ->
180 |     Record fields -> Record fields
181 | updateAt 0 f [] = absurd0 inRange
182 | updateAt 0 f ((label :- val) :: y) {inRange = Refl} = label :- f val :: y
183 | updateAt (S k) f [] = absurd0 inRange
184 | updateAt (S k) f (x :: y) = x :: updateAt k f y
185 |
186 | ||| Update the value with the given label.
187 | ||| @ field The label of the value we are updating.
188 | ||| @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.
189 | ||| @ f The update function.
190 | export
191 | update :
192 |     (0 label : String) -> {n : Nat} ->
193 |     (0 inRange : NameInRange label fields === Just (n, out)) =>
194 |     (f : out -> out) ->
195 |     Record fields -> Record fields
196 | update field f rec = updateAt n {fields, out, inRange = IndexInRange inRange} f rec
197 |
198 | ||| Override the value found at the given index.
199 | ||| @ n The index we are removing.
200 | ||| @ inRange A proof that the index is in range of the record spec.
201 | ||| @ newVal The value that will replace the existing one.
202 | export
203 | setAt : (n : Nat) -> (inRange : FindIndex n fields === Just out) => (newVal : out) ->
204 |         Record fields -> Record fields
205 | setAt n newVal x = updateAt n (const newVal) x
206 |
207 |
208 | ||| Override the value found at the given label.
209 | ||| @ label The label of the value we are overriding.
210 | ||| @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.
211 | ||| @ newVal The value that will replace the existing one.
212 | export
213 | set :
214 |     (0 label : String) -> {n : Nat} ->
215 |     (0 inRange : NameInRange label fields === Just (n, out)) =>
216 |     (newVal : out) ->
217 |     Record fields -> Record fields
218 | set field newVal rec = update field (const newVal) rec
219 |
220 |
221 |