Language.Reflection.Expr

Reexports

import public Control.Applicative.Const
import public Data.Bits
import public Data.Cozippable
import public Data.Fin.Set
import public Data.Fin.ToFin
import public Data.List.Ex
import public Data.List.Quantifiers
import public Data.SortedSet
import public Data.These
import public Data.Vect.Dependent
import public Language.Reflection
import public Language.Reflection.Syntax
import public Syntax.IHateParens.List

Definitions

data IsNamedArg : Arg -> Type

Totality: total
Visibility: public export
Constructor:

ItIsNamed : IsNamedArg (MkArg cnt pii (Just n) ty)

isNamedArg : (arg : Arg) -> Dec (IsNamedArg arg)

Totality: total
Visibility: public export

stname : Maybe Name -> Name

Totality: total
Visibility: public export

argName : (a : Arg) -> {auto 0 _ : IsNamedArg a} -> Name

Totality: total
Visibility: public export

argName' : Arg -> Name

Totality: total
Visibility: public export

cleanupNamedHoles : TTImp -> TTImp

Totality: total
Visibility: export

cleanupArg : Arg -> Arg

  Run `cleanupNamedHoles` over all `Arg`'s `TTImp`s

Totality: total
Visibility: public export

argNames : (l : List Arg) -> {auto 0 _ : All IsNamedArg l} -> List Name

Totality: total
Visibility: export

normaliseAs' : Elaboration m => (0 expected : Type) -> (TTImp -> TTImp) -> {0 resulting : expected -> Type} -> (0 _ : ((x : expected) -> resulting x)) -> TTImp -> m TTImp

Totality: total
Visibility: export

normaliseAs : Elaboration m => (0 _ : Type) -> TTImp -> m TTImp

Totality: total
Visibility: public export

normalise : Elaboration m => TTImp -> m TTImp

Totality: total
Visibility: public export

normaliseAsType : Elaboration m => TTImp -> m TTImp

Totality: total
Visibility: public export

data AnyApp : Type

Totality: total
Visibility: public export
Constructors:

PosApp : TTImp -> AnyApp
NamedApp : Name -> TTImp -> AnyApp
AutoApp : TTImp -> AnyApp
WithApp : TTImp -> AnyApp

appArg : Arg -> TTImp -> AnyApp

Totality: total
Visibility: public export

getExpr : AnyApp -> TTImp

Totality: total
Visibility: public export

mapExpr : (TTImp -> TTImp) -> AnyApp -> AnyApp

Totality: total
Visibility: public export

unAppAny : TTImp -> (TTImp, List AnyApp)

Totality: total
Visibility: public export

reAppAny1 : TTImp -> AnyApp -> TTImp

Totality: total
Visibility: public export

reAppAny : Foldable f => TTImp -> f AnyApp -> TTImp

Totality: total
Visibility: public export

record AllApps : Type

  All argument values applied in an expression
  
  Used for convenience when traversing given arguments and their types

Totality: total
Visibility: public export
Constructor:

MkAllApps : List TTImp -> List TTImp -> SortedMap Name TTImp -> AllApps

Projections:

.autoArgs : AllApps -> List TTImp
.explicitArgs : AllApps -> List TTImp
.namedArgs : AllApps -> SortedMap Name TTImp

.explicitArgs : AllApps -> List TTImp

Totality: total
Visibility: public export

explicitArgs : AllApps -> List TTImp

Totality: total
Visibility: public export

.autoArgs : AllApps -> List TTImp

Totality: total
Visibility: public export

autoArgs : AllApps -> List TTImp

Totality: total
Visibility: public export

.namedArgs : AllApps -> SortedMap Name TTImp

Totality: total
Visibility: public export

namedArgs : AllApps -> SortedMap Name TTImp

Totality: total
Visibility: public export

addApp : AnyApp -> AllApps -> AllApps

  Insert an `AnyApp` into `AllApps`

Totality: total
Visibility: public export

mkAllApps : List AnyApp -> AllApps

  Make an `AllApps` out of a list of `AnyApp`
  
  Used in conjunction with `unAppAny`

Totality: total
Visibility: public export

popNamed : Maybe Name -> AllApps -> Maybe (TTImp, AllApps)

  Pop a value from `AllApps` by argument name
  
  The argument/value is returned from `AllApps`

Totality: total
Visibility: public export

popArgVal : Arg -> AllApps -> Maybe (TTImp, AllApps)

  Pop an argument value from `AllApps`, returning Nothing if no value is given
  
  The argument/value is returned from `AllApps`

Totality: total
Visibility: public export

popArgVals : List Arg -> AllApps -> List (Maybe TTImp)

  Extract given values of arguments from `AllApps`

Totality: total
Visibility: public export

liftList : Foldable f => f TTImp -> TTImp

  Lifts the given foldable of elements to an expression of a list-like data type

Totality: total
Visibility: public export

liftList' : Foldable f => f TTImp -> TTImp

  Lifts the given foldable of elements to an expression of `Prelude.List`

Totality: total
Visibility: public export

applySyn : TTImp -> TTImp -> TTImp

Totality: total
Visibility: public export

unDPair : TTImp -> (List Arg, TTImp)

Totality: total
Visibility: public export

unDPairUnAlt : TTImp -> Maybe (List Arg, TTImp)

Totality: total
Visibility: public export

buildDPair : TTImp -> List (Name, TTImp) -> TTImp

Totality: total
Visibility: public export

unNS : Name -> (List String, Name)

  Returns unnamespaced name and list of all namespaces stored in direct order
  
  Say, for `Data.Vect.Vect` it would return (["Data", "Vect"], `{Vect}).

Totality: total
Visibility: export

allNameSuffixes : Name -> List Name

  Returns all names that are suffixes of a given name (including the original name itself).
  
  For example, for the name `Data.Vect.Vect` suffixes set would include
  `Data.Vect.Vect`, `Vect.Vect` and `Vect`.

Totality: total
Visibility: export

isNamespaced : Name -> Bool

Totality: total
Visibility: export

isImplicit : PiInfo c -> Bool

Totality: total
Visibility: public export

isSameTypeAs : Name -> Name -> Elab Bool

Totality: total
Visibility: public export

nameConformsTo : Name -> Name -> Bool

Totality: total
Visibility: export

allVarNames' : TTImp -> SortedSet Name

Totality: total
Visibility: export

allVarNames : TTImp -> List Name

Totality: total
Visibility: export

isVar : TTImp -> Bool

Totality: total
Visibility: public export

0 ArgDeps : Nat -> Type

Totality: total
Visibility: public export

argDeps : (args : List Arg) -> ArgDeps (args .length)

Totality: total
Visibility: export

dependees : (args : List Arg) -> FinSet (args .length)

Totality: total
Visibility: export