Idris2Doc : Language.Reflection.TTImp

Language.Reflection.TTImp

(source)
Reexports
import public Data.List1
import public Language.Reflection.TT
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