Generics.Meta

Metadata about a data type's constructor and field names.

Since for the time being, record syntax is still under discussion,
records are not yet treated any differently from other
product types. This might well change in the future, once
the issues about record syntax are resolved.

Also, it seems not yet to be possible to get access to an
operator's fixity through elaborator reflection. We try to make
this information available as soon as possible.

Definitions

data ArgName : Type

  Name and integer index of constructor arguments

Totality: total
Visibility: public export
Constructors:

NamedArg : Nat -> String -> ArgName

  Name and index of a named argument

UnnamedArg : Nat -> ArgName

  Index of an unnamed argument

getName : ArgName -> Maybe String

  Tries to extract an argument's name.

Totality: total
Visibility: public export

record ConInfo_ : (k : Type) -> List k -> Type

  Namespace, name and arguments of a single data constructor
  
  The arguments are wrapped in an n-ary product
  parameterized by the constant functor, to make them
  accessible to the SOP combinators.

Totality: total
Visibility: public export
Constructor: 

MkConInfo : List String -> String -> NP_ k (K ArgName) ks -> ConInfo_ k ks

Projections:

.args : ConInfo_ k ks -> NP_ k (K ArgName) ks

  Constructor arguments

.conNS : ConInfo_ k ks -> List String

  Namespace of the constructor

.conName : ConInfo_ k ks -> String

  Name of the constructor

.conNS : ConInfo_ k ks -> List String

  Namespace of the constructor

Totality: total
Visibility: public export

conNS : ConInfo_ k ks -> List String

  Namespace of the constructor

Totality: total
Visibility: public export

.conName : ConInfo_ k ks -> String

  Name of the constructor

Totality: total
Visibility: public export

conName : ConInfo_ k ks -> String

  Name of the constructor

Totality: total
Visibility: public export

.args : ConInfo_ k ks -> NP_ k (K ArgName) ks

  Constructor arguments

Totality: total
Visibility: public export

args : ConInfo_ k ks -> NP_ k (K ArgName) ks

  Constructor arguments

Totality: total
Visibility: public export

ConInfo : List k -> Type

  Alias for `ConInfo_` with the `k` parameter being implicit.

Totality: total
Visibility: public export

argNames : ConInfo ks -> Maybe (NP (K String) ks)

  Tries to extract the set of argument names from
  a constructor.

Totality: total
Visibility: public export

isOperator : String -> Bool

  Returns `True` if a constructor's `conName` consists
  only of non-alphanumeric characters.

Totality: total
Visibility: public export

wrapOperator : String -> String

  Wraps a function name in parentheses if it is an operator

Totality: total
Visibility: public export

record TypeInfo' : (k : Type) -> List (List k) -> Type

  Namespace, name and constructors of a data type.
  
  The constructors are wrapped in an n-ary product
  parameterized by `ConInfo`, to make them
  accessible to the SOP combinators.

Totality: total
Visibility: public export
Constructor: 

MkTypeInfo : List String -> String -> NP_ (List k) (ConInfo_ k) kss -> TypeInfo' k kss

Projections:

.constructors : TypeInfo' k kss -> NP_ (List k) (ConInfo_ k) kss

  n-ary product of the data type's constructors

.typeNS : TypeInfo' k kss -> List String

  Namespace of the data type

.typeName : TypeInfo' k kss -> String

  Name of the data type

.typeNS : TypeInfo' k kss -> List String

  Namespace of the data type

Totality: total
Visibility: public export

typeNS : TypeInfo' k kss -> List String

  Namespace of the data type

Totality: total
Visibility: public export

.typeName : TypeInfo' k kss -> String

  Name of the data type

Totality: total
Visibility: public export

typeName : TypeInfo' k kss -> String

  Name of the data type

Totality: total
Visibility: public export

.constructors : TypeInfo' k kss -> NP_ (List k) (ConInfo_ k) kss

  n-ary product of the data type's constructors

Totality: total
Visibility: public export

constructors : TypeInfo' k kss -> NP_ (List k) (ConInfo_ k) kss

  n-ary product of the data type's constructors

Totality: total
Visibility: public export

TypeInfo : List (List k) -> Type

  Alias for `TypeInfo'` with the `k` parameter being implicit.

Totality: total
Visibility: public export

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

  Interface to make a data type's metadata available at runtime.
  
  In order to get access to the meta data, it is often more convenient
  to use function `metaFor`.

Parameters: t, code
Constraints: Generic t code
Constructor: 

MkMeta

Methods:

meta : TypeInfo' Type code

Implementations:

Meta Nat [[], [Nat]]

Meta (Maybe ty) [[], [ty]]

Meta (Either a b) [[a], [b]]

Meta (List {arg:666}) [[], [{arg:666}, List {arg:666}]]

Meta (List1 a) [[a, List a]]

Meta (Dec {arg:3987}) [[{arg:3987}], [Not {arg:3987}]]

Meta Ordering [[], [], []]

Meta Bool [[], []]

Meta Prec [[], [], [], [], [Nat], [], []]

Meta Mode [[], [], [], [], [], []]

Meta FileError [[Int], [], [], [], [], []]

Meta File [[FilePtr]]

Meta FileMode [[], [], []]

Meta Permissions [[List FileMode, List FileMode, List FileMode]]

Meta ClockType [[], [], [], [], [], [], []]

meta : Meta t code => TypeInfo' Type code

Totality: total
Visibility: public export

metaFor : (0 t : Type) -> Meta t code => TypeInfo code

  Return's the `TypeInfo` of a data type. This is
  an alias for `meta {t = t}`.

Totality: total
Visibility: public export

genShowPrec : Meta t code => POP Show code => Prec -> t -> String

  Generic show function.
  
  This is still quite basic. It uses prefix notation for operators
  and data types with List constructors (`Nil` and `(::)`)
  are not yet displayed using list syntax ("[a,b,c]").
  
  However, constructors with only named arguments are displayed
  in record syntax style.

Totality: total
Visibility: public export