Libraries.Data.WithData

The WithData module combines a record and an arbitrary payload. The intended use is to
attach metadata to the payload.

Reexports

Definitions

record WithData : List KeyVal -> Type -> Type

  A pair for a type and an attached record hosting metadata about that type
  
  Intended usage
  --------------
  Only ever put plain types in the metadata
  Do not add functors such as `List` or `PTerm`. The functor instance
  for `WithData` is only functorial on its payload and not the metadata.
  
  There is rarely any need to write down `WithData [ ... ] a` thanks to the
  `AddMetadata` type constructor.
  
  While possible, you are not meant to pattern match on values of this type
  to extract the main payload, you can use the `val` projection, and to access
  metadata fields you can use `get` and `getAt` functions that will automatically
  compute and extract the value out of the metadata record.
  
  Example usage
  -------------
  Given a value of type `value : WithData ["loc" :-: Location, "cached" :-: Bool] Term`
  we can access the `Term` by projecting our the underlying value:
  ```idris example
  termValue : Term
  termValue = value.val
  ```
  To access the metadata fields use `get` with the name of the field or `getAt` with
  the index of the field. For example "loc" is at index `0` therefore one can access
  it using `getAt 0`:
  ```idris example
  termLocation : Location
  termLocation = value `getAt` 0
  ```
  Similarly, we can obtain the "cached" field by giving its name directly
  ```idris example
  termCache : Bool
  termCache = value.get "cached"
  ```

Totality: total
Visibility: public export
Constructor: 

MkWithData : Record additional -> payload -> WithData additional payload

Projections:

.metadata : WithData additional payload -> Record additional

.val : WithData additional payload -> payload

Hints:

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

Functor (WithData md)

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

.metadata : WithData additional payload -> Record additional

Visibility: public export

metadata : WithData additional payload -> Record additional

Visibility: public export

.val : WithData additional payload -> payload

Visibility: public export

val : WithData additional payload -> payload

Visibility: public export

AddMetadata : KeyVal -> Type -> Type

  Add some metadata to a type given a label and a type for the metadata
  This function matches on the type and add it to the metadata record if it is alread a `WithData`
  
  example:
  ```idris example
  Term : Type
  
  RichTerm : Type
  RichTerm = AddMetadata ("loc" :-: Location) $ AddMetadata ("cached" :-: Bool) Term
  ```
  The example shows how to add the fields "loc" and "cached" to the type `Term` as metadata. Those
  fields can be accessed with `get` and `getAt` functions

Visibility: public export

getAt : (ix : Nat) -> {auto 0 _ : FindIndex ix fields = Just out} -> WithData fields a -> out

  Obtain the value of the metadata at the given index
  @ ix The index of the value we are extracting
  @ inRange A proof the index is in range of the metadata record

Visibility: export

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

  Obtain the value out of the payload record given its label, same as `(.get)`
  @ label The label of the value we are extracting
  @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.

Visibility: export

.get : WithData fields a -> (0 field : String) -> {auto 0 _ : NameInRange field fields = Just (n, out)} -> out

  Obtain the value out of the payload record given its label, same as `get`.
  @ label The label of the value we are extracting.
  @ inRange A proof that the label is in the record at the appropriate index with the appropriate type.

Visibility: export

updateAt : (ix : Nat) -> FindIndex ix fields = Just out => (out -> out) -> WithData fields a -> WithData fields a

  Update at the given index, updates cannot change the type of the field.
  @ ix The index at which we update the value.
  @ inRange A proof that the index is in range of the metadata record.
  @ f The update function.

Visibility: export

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

  Update the value with the given field name
  @ label 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 ls = Just out => out -> WithData ls a -> WithData ls a

  Override the value at the given index.
  @ n The index at which we replace our value.
  @ inRange A proof that index is in range.
  @ newVal The new value remplacing the existing one.

Visibility: export

set : (0 label : String) -> {auto 0 _ : NameInRange label ls = Just (n, out)} -> out -> WithData ls a -> WithData ls a

  Override the value matching 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 new value remplacing the existing one.

Visibility: export

Add : (0 lbl : String) -> ty -> a -> WithData [(lbl :-: ty)] a

  Add a labelled value to the metadata

Visibility: export

(:+) : ty -> WithData ls a -> WithData ((lbl :-: ty) :: ls) a

  Add value the payload, ignore the label since it's given by the type

Visibility: export
Fixity Declaration: infixr operator, level 9

drop : WithData (l :: ls) a -> WithData ls a

  Drop the head element of the metadata

Visibility: export

.drop : WithData (l :: ls) a -> WithData ls a

  Drop the head element of the metadata

Visibility: export

interface HasDefault : Type -> Type

  An interface for default values, used to fill in missing values in metadata records

Parameters: a
Methods:

defValue : a

Implementations:

HasDefault FC

HasDefault BindingModifier

HasDefault String

defValue : HasDefault a => a

Visibility: public export

MkDef : a -> All (HasDefault . type) fs => WithData fs a

  Construct a payload filled with default values for its metadata

Visibility: export

Mk : All type fs -> a -> WithData fs a

  Construct a value with metadata but ignore the labels

Visibility: export

AddDef : HasDefault ty => WithData fl a -> WithData ((lbl :-: ty) :: fl) a

  Add a default value to an existing metadata record

Visibility: export

distribData : WithData fs (List a) -> List (WithData fs a)

Visibility: export

distribDataMaybe : WithData fs (Maybe a) -> Maybe (WithData fs a)

Visibility: export

traverseDataMaybe : (a -> Maybe b) -> WithData fs a -> Maybe (WithData fs b)

Visibility: export