Idris2Doc : Language.Reflection.TTImp

Language.Reflection.TTImp

Reexports
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
  Totality: total
  Visibility: public export
  Constructors:
  
IVar : FC -> Name -> TTImp
  
IPi : FC -> Count -> PiInfo TTImp -> Maybe Name -> TTImp -> TTImp -> TTImp
  
ILam : FC -> Count -> PiInfo TTImp -> Maybe Name -> TTImp -> TTImp -> TTImp
  
ILet : FC -> FC -> Count -> Name -> TTImp -> TTImp -> TTImp -> TTImp
  
ICase : FC -> List FnOpt -> TTImp -> TTImp -> List Clause -> TTImp
  
ILocal : FC -> List Decl -> TTImp -> TTImp
  
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
  
IApp : FC -> TTImp -> TTImp -> TTImp
  
INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp
  
IAutoApp : FC -> TTImp -> TTImp -> TTImp
  
IWithApp : FC -> TTImp -> TTImp -> TTImp
  
ISearch : FC -> Nat -> TTImp
  
IAlternative : FC -> AltType -> List TTImp -> TTImp
  
IRewrite : FC -> TTImp -> TTImp -> TTImp
  
IBindHere : FC -> BindMode -> TTImp -> TTImp
  
IBindVar : FC -> String -> TTImp
  
IAs : FC -> FC -> UseSide -> Name -> TTImp -> TTImp
  
IMustUnify : FC -> DotReason -> TTImp -> TTImp
  
IDelayed : FC -> LazyReason -> TTImp -> TTImp
  
IDelay : FC -> TTImp -> TTImp
  
IForce : FC -> TTImp -> TTImp
  
IQuote : FC -> TTImp -> TTImp
  
IQuoteName : FC -> Name -> TTImp
  
IQuoteDecl : FC -> List Decl -> TTImp
  
IUnquote : FC -> TTImp -> TTImp
  
IPrimVal : FC -> Constant -> TTImp
  
IType : FC -> TTImp
  
IHole : FC -> String -> TTImp
  
Implicit : FC -> Bool -> TTImp
  
IWithUnambigNames : FC -> List (FC, Name) -> TTImp -> TTImp

  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 Decl
  
Eq TTImp
  
Show TTImp
data IFieldUpdate : Type
  Totality: total
  Visibility: public export
  Constructors:
  
ISetField : List String -> TTImp -> IFieldUpdate
  
ISetFieldApp : List String -> TTImp -> IFieldUpdate

  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
  
GlobalHint : Bool -> FnOpt
  
ExternFn : FnOpt
  
ForeignFn : List TTImp -> FnOpt
  
ForeignExport : List TTImp -> FnOpt
  
Invertible : FnOpt
  
Totality : TotalReq -> FnOpt
  
Macro : FnOpt
  
SpecArgs : List Name -> FnOpt

  Hint: 
Eq TTImp => Eq FnOpt
data ITy : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTy : FC -> FC -> Name -> TTImp -> ITy

  Hints:
  
Eq TTImp => Eq ITy
  
Show ITy
data DataOpt : Type
  Totality: total
  Visibility: public export
  Constructors:
  
SearchBy : List Name -> DataOpt
  
NoHints : DataOpt
  
UniqueSearch : DataOpt
  
External : DataOpt
  
NoNewtype : DataOpt

  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
  Totality: total
  Visibility: public export
  Constructors:
  
PatClause : FC -> TTImp -> TTImp -> Clause
  
WithClause : FC -> TTImp -> Count -> TTImp -> Maybe Name -> List WithFlag -> List Clause -> Clause
  
ImpossibleClause : FC -> TTImp -> Clause

  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 Decl : Type
  Totality: total
  Visibility: public export
  Constructors:
  
IClaim : FC -> Count -> Visibility -> List FnOpt -> ITy -> Decl
  
IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl
  
IDef : FC -> Name -> List Clause -> Decl
  
IParameters : FC -> List (Name, (Count, (PiInfo TTImp, TTImp))) -> List Decl -> Decl
  
IRecord : FC -> Maybe String -> WithDefault Visibility Private -> Maybe TotalReq -> Record -> Decl
  
INamespace : FC -> Namespace -> List Decl -> Decl
  
ITransform : FC -> Name -> TTImp -> TTImp -> Decl
  
IRunElabDecl : FC -> TTImp -> Decl
  
ILog : Maybe (List String, Nat) -> Decl
  
IBuiltin : FC -> BuiltinType -> Name -> Decl

  Hints:
  
Eq TTImp => Eq Decl
  
Show Decl
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

  Hint: 
Functor 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 => (m TTImp -> m TTImp) -> TTImp -> m TTImp
  Totality: total
  Visibility: public export
mapMPiInfo : Applicative m => (m TTImp -> m TTImp) -> PiInfo TTImp -> m (PiInfo TTImp)
  Totality: total
  Visibility: public export
mapMClause : Applicative m => (m TTImp -> m TTImp) -> Clause -> m Clause
  Totality: total
  Visibility: public export
mapMITy : Applicative m => (m TTImp -> m TTImp) -> ITy -> m ITy
  Totality: total
  Visibility: public export
mapMFnOpt : Applicative m => (m TTImp -> m TTImp) -> FnOpt -> m FnOpt
  Totality: total
  Visibility: public export
mapMData : Applicative m => (m TTImp -> m TTImp) -> Data -> m Data
  Totality: total
  Visibility: public export
mapMIField : Applicative m => (m TTImp -> m TTImp) -> IField -> m IField
  Totality: total
  Visibility: public export
mapMRecord : Applicative m => (m TTImp -> m TTImp) -> Record -> m Record
  Totality: total
  Visibility: public export
mapMDecl : Applicative m => (m TTImp -> m TTImp) -> Decl -> m Decl
  Totality: total
  Visibility: public export
mapMIFieldUpdate : Applicative m => (m TTImp -> m TTImp) -> IFieldUpdate -> m IFieldUpdate
  Totality: total
  Visibility: public export
mapMAltType : Applicative m => (m TTImp -> m TTImp) -> AltType -> m AltType
  Totality: total
  Visibility: public export
mapMTTImp : Monad m => (TTImp -> m TTImp) -> TTImp -> m TTImp
  Totality: total
  Visibility: public export