Libraries.Data.Record

Modular records based on `All`

Reexports

Definitions

record KeyVal : Type

  A type with a string-label for it. Used in `Record`
  
  ```idris example
  IntLabel : KeyVal
  IntLabel = "int" :-: Int
  ```

Totality: total
Visibility: public export
Constructor: 

(:-:) : String -> Type -> KeyVal

Projections:

.label : KeyVal -> String

.type : KeyVal -> Type

Hints:

All (Eq . type) fs => Eq (Record fs)

All (Eq . type) fs => Eq a => Eq (WithData fs a)

Functor (WithData md)

All (TTC . type) fs => TTC (Record fs)

All (TTC . type) fs => TTC a => TTC (WithData fs a)

.label : KeyVal -> String

Visibility: public export

label : KeyVal -> String

Visibility: public export

.type : KeyVal -> Type

Visibility: public export

type : KeyVal -> Type

Visibility: public export

record LabelledValue : KeyVal -> Type

  The value-constructor for `KeyVal`, essentially a pair of a label
  and a value that match the specification given by `KeyVal`
  
  ```idris example
  IntLabel : KeyVal
  IntLabel = "int" :-: Int
  
  intValue : LabelledValue IntLabel
  intValue = "int" :- 3
  ```

Totality: total
Visibility: public export
Constructor: 

(:-) : (0 label : String) -> {auto 0 _ : kv .label = label} -> kv .type -> LabelledValue kv

Projections:

0 .check : ({rec:0} : LabelledValue kv) -> kv .label = label {rec:0}

  A proof that the label given matches the label in the specification

0 .label : LabelledValue kv -> String

  The label matching the `KeyVal` spec, erased for performance reasons

.value : LabelledValue kv -> kv .type

  A runtime value of the type given by the specification

0 .label : LabelledValue kv -> String

  The label matching the `KeyVal` spec, erased for performance reasons

Visibility: public export

0 label : LabelledValue kv -> String

  The label matching the `KeyVal` spec, erased for performance reasons

Visibility: public export

0 .check : ({rec:0} : LabelledValue kv) -> kv .label = label {rec:0}

  A proof that the label given matches the label in the specification

Visibility: public export

0 check : ({rec:0} : LabelledValue kv) -> kv .label = label {rec:0}

  A proof that the label given matches the label in the specification

Visibility: public export

.value : LabelledValue kv -> kv .type

  A runtime value of the type given by the specification

Visibility: public export

value : LabelledValue kv -> kv .type

  A runtime value of the type given by the specification

Visibility: public export

Record : List KeyVal -> Type

  Records are a list of of labelled values, their fields are given by a list of KeyVal
  Each element in the list describes a key
  
  ```idris example
  Spec : List KeyVal
  Spec = [ "username" :-: String, "amount" :-: Double ]
  
  recordValue : Record Spec
  recordValue = [ "username" :- "Alice", "amount" :- 3.14 ]
  ```

Visibility: public export

fromElems : All type fs -> Record fs

  Build a record from it's element values ignoring the labels
  
  ```idris example
  Spec : List KeyVal
  Spec = [ "username" :-: String, "amount" :-: Double ]
  
  recordValue : Record Spec
  recordValue = fromElems [ "Alice", 3.14 ]
  ```

Visibility: export

tail : All p (x :: xs) -> All p xs

  Obtain the tail of a list of predicates

Visibility: export

0 FindIndex : Nat -> List KeyVal -> Maybe Type

  A procedue to find the type at the given index

Visibility: public export

0 NameInRange : String -> List KeyVal -> Maybe (Nat, Type)

  A procedure to find the index and type of a given label

Visibility: public export

add : (0 str : String) -> ty -> Record fields -> Record ((str :-: ty) :: fields)

  Add a label and a value to a record

Visibility: export

index : Record fields -> (n : Nat) -> {auto 0 _ : FindIndex n fields = Just out} -> out

  Obtain the value from a record at given index
  @ n The index at which we extract the value.
  @ out The type of the value at the index.
  @ inRange A proof that the field is in the record at the appropriate index with the appropriate type.

Visibility: export

get : (0 label : String) -> Record fields -> {auto 0 _ : NameInRange label fields = Just (n, out)} -> out

  Obtain the value from a record given its label.
  @ field The field for which we extract the value.
  @ n The index corresponding to the field given.
  @ out The type of the value at the given field.
  @ inRange A proof that the field is in the record at the appropriate index with the appropriate type.

Visibility: export

get' : (0 label : String) -> (0 out : Type) -> Record fields -> {auto 0 _ : NameInRange label fields = Just (n, out)} -> out

  Obtain the value from a record given its label and type.
  @ field The field for which we extract the value.
  @ out The type of the value at the given field.
  @ n The index corresponding to the field given.
  @ inRange A proof that the field is in the record at the appropriate index with the appropriate type.

Visibility: export

ListRemoveAt : (fields : List KeyVal) -> (n : Nat) -> IsJust (FindIndex n fields) => List KeyVal

  Remove a value from the list, used in the type of `removeAt`

Visibility: public export

removeAt : (n : Nat) -> {auto inRange : IsJust (FindIndex n fields)} -> Record fields -> Record (ListRemoveAt fields n)

  Remove the value at the given index.
  @ n The index we are removing.
  @ inRange A proof that the index is in range of the record spec.

Visibility: export

updateAt : (n : Nat) -> {auto 0 _ : FindIndex n fields = Just out} -> (out -> out) -> Record fields -> Record fields

  Update the value at the given index.
  @ n The index we are removing.
  @ inRange A proof that the index is in range of the record spec.
  @ f The update function.

Visibility: export

update : (0 label : String) -> {auto 0 _ : NameInRange label fields = Just (n, out)} -> (out -> out) -> Record fields -> Record fields

  Update the value with the given label.
  @ field The label of the value we are updating.
  @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.
  @ f The update function.

Visibility: export

setAt : (n : Nat) -> FindIndex n fields = Just out => out -> Record fields -> Record fields

  Override the value found at the given index.
  @ n The index we are removing.
  @ inRange A proof that the index is in range of the record spec.
  @ newVal The value that will replace the existing one.

Visibility: export

set : (0 label : String) -> {auto 0 _ : NameInRange label fields = Just (n, out)} -> out -> Record fields -> Record fields

  Override the value found at the given label.
  @ label The label of the value we are overriding.
  @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.
  @ newVal The value that will replace the existing one.

Visibility: export