Generics.SOP

Reexports

Definitions

interface Generic : Type -> List (List Type) -> Type

  Interface for converting a data type from and to
  its generic representation as a sum of products.
  
  Additional Idris coolness: This comes with proofs
  that `from . to = id` and `to . from = id` and
  thus, that `t` and `SOP code` are indeed isomorphic.

Parameters: t, code
Constructor: 

MkGeneric

Methods:

from : t -> SOP I code

  Converts the data type to its generic representation.

to : SOP I code -> t

  Converts the generic representation back to the original
  value.

fromToId : (v : t) -> to (from v) = v

  Proof that `to . from = id`.

toFromId : (v : SOP I code) -> from (to v) = v

  Proof that `from . to = id`.

Implementations:

Generic () [[]]

Generic (a, b) [[a, b]]

Generic (LPair a b) [[a, b]]

Generic Void []

Generic (Stream a) [[a, Inf (Stream a)]]

from : Generic t code => t -> SOP I code

  Converts the data type to its generic representation.

Totality: total
Visibility: public export

to : Generic t code => SOP I code -> t

  Converts the generic representation back to the original
  value.

Totality: total
Visibility: public export

fromToId : {auto __con : Generic t code} -> (v : t) -> to (from v) = v

  Proof that `to . from = id`.

Totality: total
Visibility: public export

toFromId : {auto __con : Generic t code} -> (v : SOP I code) -> from (to v) = v

  Proof that `from . to = id`.

Totality: total
Visibility: public export

fromInjective : {auto {conArg:13479} : Generic t code} -> (0 x : t) -> (0 y : t) -> from x = from y -> x = y

Totality: total
Visibility: export

0 Code : (t : Type) -> Generic t code => List (List Type)

Totality: total
Visibility: public export

genExtract : (0 ts : List Type) -> t -> Generic t code => Elem ts code => Maybe (NP I ts)

  Tries to extract the arguments of a single constructor
  from a value's generic representation.

Totality: total
Visibility: public export

genExtract1 : (0 t' : Type) -> t -> Generic t code => Elem [t'] code => Maybe t'

  Tries to extract the value of a single one argument
  constructor from a value's generic representation.

Totality: total
Visibility: public export

valuesNP : Generic t code => EnumType code => NP_ (List Type) (K t) code

  Returns all value from a generic enum type
  (all nullary constructors) wrapped in homogeneous n-ary product.

Totality: total
Visibility: public export

values : Generic t code => EnumType code => List t

  Returns all value from a generic enum type
  (all nullary constructors) wrapped in a list.

Totality: total
Visibility: public export

valuesForNP : (0 t : Type) -> Generic t code => EnumType code => NP_ (List Type) (K t) code

  Like `valuesNP` but takes the erased value type as an
  explicit argument to help with type inference.

Totality: total
Visibility: public export

valuesFor : (0 t : Type) -> Generic t code => EnumType code => List t

  Like `values` but takes the erased value type as an
  explicit argument to help with type inference.

Totality: total
Visibility: public export

genEq : Generic t code => POP Eq code => t -> t -> Bool

  Default `(==)` implementation for data types with a `Generic`
  instance.

Totality: total
Visibility: public export

genCompare : Generic t code => POP Ord code => t -> t -> Ordering

  Default `compare` implementation for data types with a `Generic`
  instance.

Totality: total
Visibility: public export

genDecEq : Generic t code => POP DecEq code => (x : t) -> (y : t) -> Dec (x = y)

  Default `decEq` implementation for data types with a `Generic`
  instance.

Totality: total
Visibility: public export

genAppend : Generic t [ts] => POP Semigroup [ts] => t -> t -> t

  Default `(<+>)` implementation for data types with a `Generic`
  instance.

Totality: total
Visibility: public export

genNeutral : Generic t [ts] => POP Monoid [ts] => t

  Default `neutral` implementation for data types with a `Generic`
  instance.

Totality: total
Visibility: public export