Language.Reflection.TTImp(source)

Reexports

Definitions

data BindMode : Type

Totality: total
Visibility: public export
Constructors:

PI : Count -> BindMode

PATTERN : BindMode

COVERAGE : BindMode

NONE : BindMode

Hint: 

Eq BindMode

data UseSide : Type

Totality: total
Visibility: public export
Constructors:

UseLeft : UseSide

UseRight : UseSide

Hint: 

Eq UseSide

data DotReason : Type

Totality: total
Visibility: public export
Constructors:

NonLinearVar : DotReason

VarApplied : DotReason

NotConstructor : DotReason

ErasedArg : DotReason

UserDotted : DotReason

UnknownDot : DotReason

UnderAppliedCon : DotReason

Hint: 

Eq DotReason

data TTImp : Type

  The elaborator representation of an Idris term
  All of these take a file context `FC` as their first argument

Totality: total
Visibility: public export
Constructors:

IVar : FC -> Name -> TTImp

  A variable reference, by name

IPi : FC -> Count -> PiInfo TTImp -> Maybe Name -> TTImp -> TTImp -> TTImp

  A function type, of the form `(mult binder : argTy) -> retTy`, with implicitness determined by `info`

ILam : FC -> Count -> PiInfo TTImp -> Maybe Name -> TTImp -> TTImp -> TTImp

  A lambda abstraction, of the form`\(mult binder : argTy) => retTy`, with implicitness determined by `info`

ILet : FC -> FC -> Count -> Name -> TTImp -> TTImp -> TTImp -> TTImp

  A let binding, of the form `let mult var : nTy = nVal in scope`

ICase : FC -> List FnOpt -> TTImp -> TTImp -> List Clause -> TTImp

  A case expression `case val : ty of clauses`

ILocal : FC -> List Decl -> TTImp -> TTImp

  A list of full declarations local to a term

IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp

  An update to a record value, `{ updates } val`

IApp : FC -> TTImp -> TTImp -> TTImp

  A function application, `f x`

INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp

  A named function application (for named parameters), e.g, `f {arg=x}`

IAutoApp : FC -> TTImp -> TTImp -> TTImp

  An explicitly inserted auto implicit, `f @{x}`

IWithApp : FC -> TTImp -> TTImp -> TTImp

  A `with` application `f | e`

ISearch : FC -> Nat -> TTImp

  `%search`

IAlternative : FC -> AltType -> List TTImp -> TTImp

  A list of potential desugarings of an ambiguous expression
  The success conditions of typechecking is determined by AltType

IRewrite : FC -> TTImp -> TTImp -> TTImp

  A rewrite expression, `rewrite eq in exp`

IBindHere : FC -> BindMode -> TTImp -> TTImp

  Any implicit bindings in the scope should be bound here, using
  the given binder

IBindVar : FC -> Name -> TTImp

  A name which should be implicitly bound

IAs : FC -> FC -> UseSide -> Name -> TTImp -> TTImp

  An 'as' pattern, valid on the LHS of a clause only, `group@pat`

IMustUnify : FC -> DotReason -> TTImp -> TTImp

  A 'dot' pattern, i.e. one which must be equal to the given value
  by unification, `.(e)`

IDelayed : FC -> LazyReason -> TTImp -> TTImp

  The delay type, `Delay t`

IDelay : FC -> TTImp -> TTImp

  The constructor of `Delay`, `delay t`

IForce : FC -> TTImp -> TTImp

  `force`

IQuote : FC -> TTImp -> TTImp

  Quasi-quotation of expression (`( ... ))

IQuoteName : FC -> Name -> TTImp

  Quasi-quotation of a name (`{ ... })

IQuoteDecl : FC -> List Decl -> TTImp

  Quasi-quotation of a list of declarations (`[ ... ])

IUnquote : FC -> TTImp -> TTImp

  Unquote of an expression (~e)

IPrimVal : FC -> Constant -> TTImp

  A primitive value, such as an integer or string constant.
  Also any primitive *type*, apart from `Type` itself

IType : FC -> TTImp

  The type `Type`

IHole : FC -> String -> TTImp

  A named hole

Implicit : FC -> Bool -> TTImp

  An implicit value, solved by unification, but which will also be
  bound (either as a pattern variable or a type variable) if unsolved
  at the end of elaborator.
  Note that `Implicit False` is `?`, while `Implicit True` is `_`

IWithUnambigNames : FC -> List (FC, Name) -> TTImp -> TTImp

  An explicit disambiguation directive `with names exp`

Hints:

Eq TTImp => Eq Clause

Eq TTImp => Eq IFieldUpdate

Eq TTImp => Eq AltType

Eq TTImp => Eq FnOpt

Eq TTImp => Eq ITy

Eq TTImp => Eq Data

Eq TTImp => Eq IField

Eq TTImp => Eq Record

Eq TTImp => Eq IClaimData

Eq TTImp => Eq Decl

Eq TTImp

Show TTImp

data IFieldUpdate : Type

  A record field update

Totality: total
Visibility: public export
Constructors:

ISetField : List String -> TTImp -> IFieldUpdate

  `path := val`

ISetFieldApp : List String -> TTImp -> IFieldUpdate

  `path $= val`

Hints:

Eq TTImp => Eq IFieldUpdate

Show IFieldUpdate

data AltType : Type

Totality: total
Visibility: public export
Constructors:

FirstSuccess : AltType

Unique : AltType

UniqueDefault : TTImp -> AltType

Hint: 

Eq TTImp => Eq AltType

data FnOpt : Type

Totality: total
Visibility: public export
Constructors:

Inline : FnOpt

NoInline : FnOpt

Deprecate : FnOpt

TCInline : FnOpt

Hint : Bool -> FnOpt

  Flag means the hint is a direct hint, not a function which might
  find the result (e.g. chasing parent interface dictionaries)

GlobalHint : Bool -> FnOpt

  A hint that is searched if direct hints search failed.
  `%globalhint` if the argument is `True`, `%defaulthint` if `False`.

ExternFn : FnOpt

ForeignFn : List TTImp -> FnOpt

  Defined externally, takes a list of calling conventions

ForeignExport : List TTImp -> FnOpt

  Mark for export to a foreign language, takes a list of calling conventions

Invertible : FnOpt

  assume safe to cancel arguments in unification

Totality : TotalReq -> FnOpt

Macro : FnOpt

  `%macro`

SpecArgs : List Name -> FnOpt

Hint: 

Eq TTImp => Eq FnOpt

data ITy : Type

  A name with an associated type

Totality: total
Visibility: public export
Constructor: 

MkTy : FC -> WithFC Name -> TTImp -> ITy

Hints:

Eq TTImp => Eq ITy

Show ITy

data DataOpt : Type

Totality: total
Visibility: public export
Constructors:

SearchBy : List1 Name -> DataOpt

  Determining arguments

NoHints : DataOpt

  Don't generate search hints for constructors

UniqueSearch : DataOpt

  Auto implicit search must check result is unique

External : DataOpt

  Implemented externally

NoNewtype : DataOpt

  Don't apply newtype optimization

Hint: 

Eq DataOpt

data Data : Type

Totality: total
Visibility: public export
Constructors:

MkData : FC -> Name -> Maybe TTImp -> List DataOpt -> List ITy -> Data

MkLater : FC -> Name -> TTImp -> Data

Hints:

Eq TTImp => Eq Data

Show Data

data IField : Type

Totality: total
Visibility: public export
Constructor: 

MkIField : FC -> Count -> PiInfo TTImp -> Name -> TTImp -> IField

Hints:

Eq TTImp => Eq IField

Show IField

data Record : Type

Totality: total
Visibility: public export
Constructor: 

MkRecord : FC -> Name -> List (Name, (Count, (PiInfo TTImp, TTImp))) -> List DataOpt -> Name -> List IField -> Record

Hints:

Eq TTImp => Eq Record

Show Record

data WithFlag : Type

Totality: total
Visibility: public export
Constructor: 

Syntactic : WithFlag

Hint: 

Eq WithFlag

data Clause : Type

  A clause in a function definition

Totality: total
Visibility: public export
Constructors:

PatClause : FC -> TTImp -> TTImp -> Clause

  A simple pattern

WithClause : FC -> TTImp -> Count -> TTImp -> Maybe (Count, Name) -> List WithFlag -> List Clause -> Clause

  A pattern with views

ImpossibleClause : FC -> TTImp -> Clause

  An impossible pattern

Hint: 

Eq TTImp => Eq Clause

data WithDefault : (a : Type) -> a -> Type

Totality: total
Visibility: public export
Constructors:

DefaultedValue : WithDefault a def

SpecifiedValue : a -> WithDefault a def

Hints:

Eq a => Eq (WithDefault a def)

Ord a => Ord (WithDefault a def)

Show a => Show (WithDefault a def)

specified : a -> WithDefault a def

Totality: total
Visibility: export

defaulted : WithDefault a def

Totality: total
Visibility: export

collapseDefault : WithDefault a def -> a

Totality: total
Visibility: export

onWithDefault : Lazy b -> (a -> b) -> WithDefault a def -> b

Totality: total
Visibility: export

data IClaimData : Type

Totality: total
Visibility: public export
Constructor: 

MkIClaimData : Count -> Visibility -> List FnOpt -> ITy -> IClaimData

Hints:

Eq TTImp => Eq IClaimData

Show IClaimData

data Decl : Type

  A top-level declaration

Totality: total
Visibility: public export
Constructors:

IClaim : WithFC IClaimData -> Decl

  A type ascription, `a : b`.
  Called a claim because of Curry Howard, the statement `x : p` is equivalent to `x` is a proof of `p`.

IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl

  A data type declaration

IDef : FC -> Name -> List Clause -> Decl

  A function body definition

IParameters : FC -> List (Name, (Count, (PiInfo TTImp, TTImp))) -> List Decl -> Decl

  A parameters block, e.g. `parameters {0 m : _} {auto _ : Monad m} (level : Nat)

IRecord : FC -> Maybe String -> WithDefault Visibility Private -> Maybe TotalReq -> Record -> Decl

  A record declaration
  @ ns Nested namespace

INamespace : FC -> Namespace -> List Decl -> Decl

  A namespace declaration, `namespace ns where decls`

ITransform : FC -> Name -> TTImp -> TTImp -> Decl

  A transformation rule declaration

IRunElabDecl : FC -> TTImp -> Decl

  A top-level elaborator script run, `%runElab`

ILog : Maybe (List String, Nat) -> Decl

  A directive for enabling compile-time logging, `%logging "<topic>" <level>`

IBuiltin : FC -> BuiltinType -> Name -> Decl

  A builtin declaration, `%builtin type name`

Hints:

Eq TTImp => Eq Decl

Show Decl

fromTTImp : TTImp -> TTImp

Totality: total
Visibility: public export

fromDecls : List Decl -> List Decl

Totality: total
Visibility: public export

getFC : TTImp -> FC

Totality: total
Visibility: public export

mapTopmostFC : (FC -> FC) -> TTImp -> TTImp

Totality: total
Visibility: public export

data Mode : Type

Totality: total
Visibility: public export
Constructors:

InDecl : Mode

InCase : Mode

showClause : Mode -> Clause -> String

Totality: total
Visibility: public export

data Argument : Type -> Type

Totality: total
Visibility: public export
Constructors:

Arg : FC -> a -> Argument a

NamedArg : FC -> Name -> a -> Argument a

AutoArg : FC -> a -> Argument a

Hints:

Foldable Argument

Functor Argument

Traversable Argument

isExplicit : Argument a -> Maybe (FC, a)

Totality: total
Visibility: public export

fromPiInfo : FC -> PiInfo t -> Maybe Name -> a -> Maybe (Argument a)

Totality: total
Visibility: public export

iApp : TTImp -> Argument TTImp -> TTImp

Totality: total
Visibility: public export

unArg : Argument a -> a

Totality: total
Visibility: public export

apply : TTImp -> List (Argument TTImp) -> TTImp

  We often apply multiple arguments, this makes things simpler

Totality: total
Visibility: public export

data IsAppView : (FC, Name) -> SnocList (Argument TTImp) -> TTImp -> Type

Totality: total
Visibility: public export
Constructors:

AVVar : IsAppView (fc, t) [<] (IVar fc t)

AVApp : IsAppView x ts f -> IsAppView x (ts :< Arg fc t) (IApp fc f t)

AVNamedApp : IsAppView x ts f -> IsAppView x (ts :< NamedArg fc n t) (INamedApp fc f n t)

AVAutoApp : IsAppView x ts f -> IsAppView x (ts :< AutoArg fc t) (IAutoApp fc f a)

record AppView : TTImp -> Type

Totality: total
Visibility: public export
Constructor: 

MkAppView : (head : (FC, Name)) -> (args : SnocList (Argument TTImp)) -> (0 _ : IsAppView head args t) -> AppView t

Projections:

.args : AppView t -> SnocList (Argument TTImp)

.head : AppView t -> (FC, Name)

0 .isAppView : ({rec:0} : AppView t) -> IsAppView (head {rec:0}) (args {rec:0}) t

.head : AppView t -> (FC, Name)

Totality: total
Visibility: public export

head : AppView t -> (FC, Name)

Totality: total
Visibility: public export

.args : AppView t -> SnocList (Argument TTImp)

Totality: total
Visibility: public export

args : AppView t -> SnocList (Argument TTImp)

Totality: total
Visibility: public export

0 .isAppView : ({rec:0} : AppView t) -> IsAppView (head {rec:0}) (args {rec:0}) t

Totality: total
Visibility: public export

0 isAppView : ({rec:0} : AppView t) -> IsAppView (head {rec:0}) (args {rec:0}) t

Totality: total
Visibility: public export

appView : (t : TTImp) -> Maybe (AppView t)

Totality: total
Visibility: public export

mapTTImp : (TTImp -> TTImp) -> TTImp -> TTImp

Totality: total
Visibility: public export

mapPiInfo : (TTImp -> TTImp) -> PiInfo TTImp -> PiInfo TTImp

Totality: total
Visibility: public export

mapClause : (TTImp -> TTImp) -> Clause -> Clause

Totality: total
Visibility: public export

mapITy : (TTImp -> TTImp) -> ITy -> ITy

Totality: total
Visibility: public export

mapFnOpt : (TTImp -> TTImp) -> FnOpt -> FnOpt

Totality: total
Visibility: public export

mapData : (TTImp -> TTImp) -> Data -> Data

Totality: total
Visibility: public export

mapIField : (TTImp -> TTImp) -> IField -> IField

Totality: total
Visibility: public export

mapRecord : (TTImp -> TTImp) -> Record -> Record

Totality: total
Visibility: public export

mapDecl : (TTImp -> TTImp) -> Decl -> Decl

Totality: total
Visibility: public export

mapIFieldUpdate : (TTImp -> TTImp) -> IFieldUpdate -> IFieldUpdate

Totality: total
Visibility: public export

mapAltType : (TTImp -> TTImp) -> AltType -> AltType

Totality: total
Visibility: public export

mapATTImp' : Applicative m => (TTImp -> m TTImp -> m TTImp) -> TTImp -> m TTImp

Totality: total
Visibility: public export

mapMPiInfo : Applicative m => (TTImp -> m TTImp -> m TTImp) -> PiInfo TTImp -> m (PiInfo TTImp)

Totality: total
Visibility: public export

mapMClause : Applicative m => (TTImp -> m TTImp -> m TTImp) -> Clause -> m Clause

Totality: total
Visibility: public export

mapMITy : Applicative m => (TTImp -> m TTImp -> m TTImp) -> ITy -> m ITy

Totality: total
Visibility: public export

mapMFnOpt : Applicative m => (TTImp -> m TTImp -> m TTImp) -> FnOpt -> m FnOpt

Totality: total
Visibility: public export

mapMData : Applicative m => (TTImp -> m TTImp -> m TTImp) -> Data -> m Data

Totality: total
Visibility: public export

mapMIField : Applicative m => (TTImp -> m TTImp -> m TTImp) -> IField -> m IField

Totality: total
Visibility: public export

mapMRecord : Applicative m => (TTImp -> m TTImp -> m TTImp) -> Record -> m Record

Totality: total
Visibility: public export

mapMDecl : Applicative m => (TTImp -> m TTImp -> m TTImp) -> Decl -> m Decl

Totality: total
Visibility: public export

mapMIFieldUpdate : Applicative m => (TTImp -> m TTImp -> m TTImp) -> IFieldUpdate -> m IFieldUpdate

Totality: total
Visibility: public export

mapMAltType : Applicative m => (TTImp -> m TTImp -> m TTImp) -> AltType -> m AltType

Totality: total
Visibility: public export

mapATTImp : Monad m => (m TTImp -> m TTImp) -> TTImp -> m TTImp

Totality: total
Visibility: public export

mapMTTImp' : Monad m => (TTImp -> TTImp -> m TTImp) -> TTImp -> m TTImp

Totality: total
Visibility: public export

mapMTTImp : Monad m => (TTImp -> m TTImp) -> TTImp -> m TTImp

Totality: total
Visibility: public export