Language.Reflection.Compat

(source)

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

import public Data.Alternative
import public Data.List.Quantifiers
import public Data.List1
import public Data.String
import public Data.Vect
import public Deriving.Show
import public Language.Reflection
import public Language.Reflection.Syntax
import public Language.Reflection.Syntax.Ops

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

Hints:

LogPosition Con
Show 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

countShow : Show Count

Totality: total
Visibility: export

piInfoShow : Show a => Show (PiInfo a)

Totality: total
Visibility: export

argShow : Show Arg

Totality: total
Visibility: export

conShow : Show Con

Totality: total
Visibility: 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

Hints:

LogPosition TypeInfo
Show 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

tiShow : Show TypeInfo

Totality: total
Visibility: 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