Language.Reflection.Compat

This module contains copies of the pre-overhaul definitions of the `elab-util` library and/or code derived from these copies
(the overhaul is this one: https://github.com/stefan-hoeck/idris2-elab-util/pull/56).
This is done due to be able to migrate to the newer `elab-util` slowly, using both old and new definitions.

This copying is done with the permission of Stefan Höck, the author and copyright holder of the `elab-util` library.

Reexports

Definitions

record Con : Type

  Constructor of a data type

Totality: total
Visibility: public export
Constructor: 

MkCon : Name -> List Arg -> TTImp -> Con

Projections:

.args : Con -> List Arg

.name : Con -> Name

.type : Con -> TTImp

Hint: 

LogPosition Con

.name : Con -> Name

Totality: total
Visibility: public export

name : Con -> Name

Totality: total
Visibility: public export

.args : Con -> List Arg

Totality: total
Visibility: public export

args : Con -> List Arg

Totality: total
Visibility: public export

.type : Con -> TTImp

Totality: total
Visibility: public export

type : Con -> TTImp

Totality: total
Visibility: public export

getCon : Elaboration m => Name -> m Con

  Tries to lookup a constructor by name.

Totality: total
Visibility: export

record TypeInfo : Type

  Information about a data type
  
  @name : Name of the data type
          Note: There is no guarantee that the name will be fully
          qualified
  @args : Type arguments of the data type
  @cons : List of data constructors

Totality: total
Visibility: public export
Constructor: 

MkTypeInfo : Name -> List Arg -> List Con -> TypeInfo

Projections:

.argNames : (ti : TypeInfo) -> {auto 0 _ : AllTyArgsNamed ti} -> List Name

.args : TypeInfo -> List Arg

.cons : TypeInfo -> List Con

.decl : TypeInfo -> Decl

  Generate a declaration from TypeInfo

.name : TypeInfo -> Name

Hint: 

LogPosition TypeInfo

.name : TypeInfo -> Name

Totality: total
Visibility: public export

name : TypeInfo -> Name

Totality: total
Visibility: public export

.args : TypeInfo -> List Arg

Totality: total
Visibility: public export

args : TypeInfo -> List Arg

Totality: total
Visibility: public export

.cons : TypeInfo -> List Con

Totality: total
Visibility: public export

cons : TypeInfo -> List Con

Totality: total
Visibility: public export

getInfo' : Elaboration m => Name -> m TypeInfo

  Tries to get information about the data type specified
  by name. The name need not be fully qualified, but
  needs to be unambiguous.

Totality: total
Visibility: export

getInfo : Name -> Elab TypeInfo

  macro version of `getInfo'`

Totality: total
Visibility: export

data ConArgsNamed : Con -> Type

Totality: total
Visibility: public export
Constructor: 

TheyAreNamed : All IsNamedArg ars -> ConArgsNamed (MkCon nm ars ty)

areConArgsNamed : (con : Con) -> Dec (ConArgsNamed con)

Totality: total
Visibility: public export

0 conArgsNamed : {auto 0 _ : ConArgsNamed c} -> All IsNamedArg (c .args)

Totality: total
Visibility: public export

data AllTyArgsNamed : TypeInfo -> Type

Totality: total
Visibility: public export
Constructor: 

TheyAllAreNamed : All IsNamedArg ars -> All ConArgsNamed cns -> AllTyArgsNamed (MkTypeInfo nm ars cns)

areAllTyArgsNamed : (ty : TypeInfo) -> Dec (AllTyArgsNamed ty)

Totality: total
Visibility: public export

0 .tyArgsNamed : (0 _ : AllTyArgsNamed t) -> All IsNamedArg (t .args)

Totality: total
Visibility: public export

0 .tyConArgsNamed : (0 _ : AllTyArgsNamed t) -> All ConArgsNamed (t .cons)

Totality: total
Visibility: public export

.tyName : TypeInfo -> Name

Totality: total
Visibility: public export

.tyArgs : TypeInfo -> List Arg

Totality: total
Visibility: public export

.tyCons : TypeInfo -> List Con

Totality: total
Visibility: public export

.conArgs : Con -> List Arg

Totality: total
Visibility: public export