-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Functional Programming Language with Dependent Types
--   
--   Idris is a general purpose language with full dependent types. It is
--   compiled, with eager evaluation. Dependent types allow types to be
--   predicated on values, meaning that some aspects of a program's
--   behaviour can be specified precisely in the type. The language is
--   closely related to Epigram and Agda. There is a tutorial at
--   <a>http://www.idris-lang.org/documentation</a>. Features include:
--   
--   <ul>
--   <li>Full, first class, dependent types with dependent pattern
--   matching</li>
--   <li>where clauses, with rule, case expressions, pattern matching let
--   and lambda bindings</li>
--   <li>Interfaces (similar to type classes), monad comprehensions</li>
--   <li>do notation, idiom brackets, syntactic conveniences for lists,
--   tuples, dependent pairs</li>
--   <li>Totality checking</li>
--   <li>Coinductive types</li>
--   <li>Indentation significant syntax, extensible syntax</li>
--   <li>Cumulative universes</li>
--   <li>Simple foreign function interface (to C)</li>
--   <li>Hugs style interactive environment</li>
--   </ul>
@package idris
@version 1.3.2


module IRTS.JavaScript.AST
data JsExpr
JsNull :: JsExpr
JsUndefined :: JsExpr
JsThis :: JsExpr
JsLambda :: [Text] -> JsStmt -> JsExpr
JsApp :: JsExpr -> [JsExpr] -> JsExpr
JsNew :: JsExpr -> [JsExpr] -> JsExpr
JsPart :: JsExpr -> Text -> JsExpr
JsMethod :: JsExpr -> Text -> [JsExpr] -> JsExpr
JsVar :: Text -> JsExpr
JsArrayProj :: JsExpr -> JsExpr -> JsExpr
JsObj :: [(Text, JsExpr)] -> JsExpr
JsProp :: JsExpr -> Text -> JsExpr
JsInt :: Int -> JsExpr
JsBool :: Bool -> JsExpr
JsInteger :: Integer -> JsExpr
JsDouble :: Double -> JsExpr
JsStr :: String -> JsExpr
JsArray :: [JsExpr] -> JsExpr
JsErrorExp :: JsExpr -> JsExpr
JsUniOp :: Text -> JsExpr -> JsExpr
JsBinOp :: Text -> JsExpr -> JsExpr -> JsExpr
JsForeign :: Text -> [JsExpr] -> JsExpr
JsB2I :: JsExpr -> JsExpr
JsForce :: JsExpr -> JsExpr
data JsStmt
JsEmpty :: JsStmt
JsComment :: Text -> JsStmt
JsExprStmt :: JsExpr -> JsStmt
JsFun :: Text -> [Text] -> JsStmt -> JsStmt
JsSeq :: JsStmt -> JsStmt -> JsStmt
JsReturn :: JsExpr -> JsStmt
JsDecVar :: Text -> JsExpr -> JsStmt
JsDecConst :: Text -> JsExpr -> JsStmt
JsDecLet :: Text -> JsExpr -> JsStmt
JsSet :: JsExpr -> JsExpr -> JsStmt
JsIf :: JsExpr -> JsStmt -> Maybe JsStmt -> JsStmt
JsSwitchCase :: JsExpr -> [(JsExpr, JsStmt)] -> Maybe JsStmt -> JsStmt
JsError :: JsExpr -> JsStmt
JsForever :: JsStmt -> JsStmt
JsContinue :: JsStmt
JsBreak :: JsStmt
jsAst2Text :: JsExpr -> Text
jsStmt2Text :: JsStmt -> Text
jsLazy :: JsExpr -> JsExpr
jsCurryLam :: [Text] -> JsExpr -> JsExpr
jsCurryApp :: JsExpr -> [JsExpr] -> JsExpr
jsAppN :: Text -> [JsExpr] -> JsExpr
jsExpr2Stmt :: JsExpr -> JsStmt
jsStmt2Expr :: JsStmt -> JsExpr
jsSetVar :: Text -> JsExpr -> JsStmt
instance Data.Data.Data IRTS.JavaScript.AST.JsStmt
instance GHC.Classes.Eq IRTS.JavaScript.AST.JsStmt
instance GHC.Show.Show IRTS.JavaScript.AST.JsStmt
instance Data.Data.Data IRTS.JavaScript.AST.JsExpr
instance GHC.Classes.Eq IRTS.JavaScript.AST.JsExpr
instance GHC.Show.Show IRTS.JavaScript.AST.JsExpr


module Idris.Colours
data IdrisColour
IdrisColour :: Maybe Color -> Bool -> Bool -> Bool -> Bool -> IdrisColour
[colour] :: IdrisColour -> Maybe Color
[vivid] :: IdrisColour -> Bool
[underline] :: IdrisColour -> Bool
[bold] :: IdrisColour -> Bool
[italic] :: IdrisColour -> Bool
data ColourTheme
ColourTheme :: IdrisColour -> IdrisColour -> IdrisColour -> IdrisColour -> IdrisColour -> IdrisColour -> IdrisColour -> IdrisColour -> ColourTheme
[keywordColour] :: ColourTheme -> IdrisColour
[boundVarColour] :: ColourTheme -> IdrisColour
[implicitColour] :: ColourTheme -> IdrisColour
[functionColour] :: ColourTheme -> IdrisColour
[typeColour] :: ColourTheme -> IdrisColour
[dataColour] :: ColourTheme -> IdrisColour
[promptColour] :: ColourTheme -> IdrisColour
[postulateColour] :: ColourTheme -> IdrisColour

-- | Idris's default console colour theme
defaultTheme :: ColourTheme
colouriseKwd :: ColourTheme -> String -> String
colouriseBound :: ColourTheme -> String -> String
colouriseImplicit :: ColourTheme -> String -> String
colourisePostulate :: ColourTheme -> String -> String
colouriseType :: ColourTheme -> String -> String
colouriseFun :: ColourTheme -> String -> String
colouriseData :: ColourTheme -> String -> String
colouriseKeyword :: ColourTheme -> String -> String
colourisePrompt :: ColourTheme -> String -> String

-- | Set the colour of a string using POSIX escape codes
colourise :: IdrisColour -> String -> String
data ColourType
KeywordColour :: ColourType
BoundVarColour :: ColourType
ImplicitColour :: ColourType
FunctionColour :: ColourType
TypeColour :: ColourType
DataColour :: ColourType
PromptColour :: ColourType
PostulateColour :: ColourType

-- | Start a colour on a handle, to support colour output on Windows
hStartColourise :: Handle -> IdrisColour -> IO ()

-- | End a colour region on a handle
hEndColourise :: Handle -> IdrisColour -> IO ()
instance GHC.Enum.Enum Idris.Colours.ColourType
instance GHC.Enum.Bounded Idris.Colours.ColourType
instance GHC.Show.Show Idris.Colours.ColourType
instance GHC.Classes.Eq Idris.Colours.ColourType
instance GHC.Generics.Generic Idris.Colours.ColourTheme
instance GHC.Show.Show Idris.Colours.ColourTheme
instance GHC.Classes.Eq Idris.Colours.ColourTheme
instance GHC.Show.Show Idris.Colours.IdrisColour
instance GHC.Classes.Eq Idris.Colours.IdrisColour


module Idris.Help
data CmdArg

-- | The command takes an expression
ExprArg :: CmdArg

-- | The command takes a name
NameArg :: CmdArg

-- | The command takes a file
FileArg :: CmdArg

-- | The command takes a shell command name
ShellCommandArg :: CmdArg

-- | The command takes a module name
ModuleArg :: CmdArg

-- | The command takes a list of package names
PkgArgs :: CmdArg

-- | The command takes a number
NumberArg :: CmdArg

-- | The command takes a namespace name
NamespaceArg :: CmdArg

-- | The command takes an option
OptionArg :: CmdArg

-- | The command takes a metavariable
MetaVarArg :: CmdArg

-- | The command is the colour-setting command
ColourArg :: CmdArg

-- | No completion (yet!?)
NoArg :: CmdArg

-- | do not use
SpecialHeaderArg :: CmdArg

-- | The width of the console
ConsoleWidthArg :: CmdArg

-- | An Idris declaration, as might be contained in a file
DeclArg :: CmdArg

-- | Zero or more of one kind of argument
ManyArgs :: CmdArg -> CmdArg

-- | Zero or one of one kind of argument
OptionalArg :: CmdArg -> CmdArg

-- | One kind of argument followed by another
SeqArgs :: CmdArg -> CmdArg -> CmdArg

-- | Use these for completion, but don't show them in :help
extraHelp :: [([String], CmdArg, String)]
instance GHC.Show.Show Idris.Help.CmdArg


module IRTS.System
getIdrisDataFileByName :: String -> IO FilePath
getCC :: IO String
getLibFlags :: IO [[Char]]
getIdrisDataDir :: IO String
getIdrisLibDir :: IO FilePath
getIdrisDocDir :: IO FilePath
getIdrisCRTSDir :: IO FilePath
getIdrisJSRTSDir :: IO FilePath
getIncFlags :: IO [[Char]]
getEnvFlags :: IO [String]
version :: Version


module Util.DynamicLinker
data ForeignFun
Fun :: String -> () -> ForeignFun
[fun_name] :: ForeignFun -> String
[fun_handle] :: ForeignFun -> ()
data DynamicLib
Lib :: String -> () -> DynamicLib
[lib_name] :: DynamicLib -> String
[lib_handle] :: DynamicLib -> ()
tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)
tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)
instance GHC.Classes.Eq Util.DynamicLinker.DynamicLib


-- | TT is the core language of Idris. The language has:
--   
--   <ul>
--   <li>Full dependent types</li>
--   <li>A hierarchy of universes, with cumulativity: Type : Type1, Type1 :
--   Type2, ...</li>
--   <li>Pattern matching letrec binding</li>
--   <li>(primitive types defined externally)</li>
--   </ul>
--   
--   Some technical stuff:
--   
--   <ul>
--   <li>Typechecker is kept as simple as possible - no unification, just a
--   checker for incomplete terms.</li>
--   <li>We have a simple collection of tactics which we use to elaborate
--   source programs with implicit syntax into fully explicit terms.</li>
--   </ul>
module Idris.Core.TT
data AppStatus n
Complete :: AppStatus n
MaybeHoles :: AppStatus n
Holes :: [n] -> AppStatus n
data ArithTy
ATInt :: IntTy -> ArithTy
ATFloat :: ArithTy

-- | All binding forms are represented in a uniform fashion. This type only
--   represents the types of bindings (and their values, if any); the
--   attached identifiers are part of the <a>Bind</a> constructor for the
--   <a>TT</a> type.
data Binder b

-- | A function binding
Lam :: RigCount -> !b -> Binder b
[binderCount] :: Binder b -> RigCount

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b

-- | A binding that occurs in a function type expression, e.g. <tt>(x:Int)
--   -&gt; ...</tt> The <a>binderImpl</a> flag says whether it was a scoped
--   implicit (i.e. forall bound) in the high level Idris, but otherwise
--   has no relevance in TT.
Pi :: RigCount -> Maybe ImplicitInfo -> !b -> !b -> Binder b
[binderCount] :: Binder b -> RigCount
[binderImpl] :: Binder b -> Maybe ImplicitInfo

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b
[binderKind] :: Binder b -> !b

-- | A binding that occurs in a <tt>let</tt> expression
Let :: RigCount -> !b -> b -> Binder b
[binderCount] :: Binder b -> RigCount

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b

-- | value for bound variable
[binderVal] :: Binder b -> b

-- | NLet is an intermediate product in the evaluator that's used for
--   temporarily naming locals during reduction. It won't occur outside the
--   evaluator.
NLet :: !b -> b -> Binder b

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b

-- | value for bound variable
[binderVal] :: Binder b -> b

-- | A hole in a term under construction in the elaborator. If this is not
--   filled during elaboration, it is an error.
Hole :: !b -> Binder b

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b

-- | A saved TT hole that will later be converted to a top-level Idris
--   metavariable applied to all elements of its local environment.
GHole :: Int -> [Name] -> !b -> Binder b
[envlen] :: Binder b -> Int
[localnames] :: Binder b -> [Name]

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b

-- | A provided value for a hole. It will later be substituted - the guess
--   is to keep it computationally inert while working on other things if
--   necessary.
Guess :: !b -> b -> Binder b

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b

-- | value for bound variable
[binderVal] :: Binder b -> b

-- | A pattern variable (these are bound around terms that make up
--   pattern-match clauses)
PVar :: RigCount -> !b -> Binder b
[binderCount] :: Binder b -> RigCount

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b

-- | The type of a pattern binding
PVTy :: !b -> Binder b

-- | type annotation for bound variable
[binderTy] :: Binder b -> !b
data Const
I :: Int -> Const
BI :: Integer -> Const
Fl :: Double -> Const
Ch :: Char -> Const
Str :: String -> Const
B8 :: Word8 -> Const
B16 :: Word16 -> Const
B32 :: Word32 -> Const
B64 :: Word64 -> Const
AType :: ArithTy -> Const
StrType :: Const
WorldType :: Const
TheWorld :: Const
VoidType :: Const
Forgot :: Const

-- | Contexts allow us to map names to things. A root name maps to a
--   collection of things in different namespaces with that name.
type Ctxt a = Map Name (Map Name a)
data ConstraintFC
ConstraintFC :: UConstraint -> FC -> ConstraintFC
[uconstraint] :: ConstraintFC -> UConstraint
[ufc] :: ConstraintFC -> FC

-- | Data declaration options
data DataOpt

-- | Set if the the data-type is coinductive
Codata :: DataOpt
DataErrRev :: DataOpt
type DataOpts = [DataOpt]
data Datatype n
Data :: n -> Int -> TT n -> Bool -> [(n, TT n)] -> Datatype n
[d_typename] :: Datatype n -> n
[d_typetag] :: Datatype n -> Int
[d_type] :: Datatype n -> TT n
[d_unique] :: Datatype n -> Bool
[d_cons] :: Datatype n -> [(n, TT n)]
type Env = EnvTT Name
type EnvTT n = [(n, RigCount, Binder (TT n))]
type Err = Err' Term

-- | Idris errors. Used as exceptions in the compiler, but reported to
--   users if they reach the top level.
data Err' t
Msg :: String -> Err' t
InternalMsg :: String -> Err' t
CantUnify :: Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> Err' t -> [(Name, t)] -> Int -> Err' t
InfiniteUnify :: Name -> t -> [(Name, t)] -> Err' t
CantConvert :: t -> t -> [(Name, t)] -> Err' t
CantSolveGoal :: t -> [(Name, t)] -> Err' t
UnifyScope :: Name -> Name -> t -> [(Name, t)] -> Err' t
CantInferType :: String -> Err' t
NonFunctionType :: t -> t -> Err' t
NotEquality :: t -> t -> Err' t
TooManyArguments :: Name -> Err' t
CantIntroduce :: t -> Err' t
NoSuchVariable :: Name -> Err' t
WithFnType :: t -> Err' t
NoTypeDecl :: Name -> Err' t
NotInjective :: t -> t -> t -> Err' t
CantResolve :: Bool -> t -> Err' t -> Err' t
InvalidTCArg :: Name -> t -> Err' t
CantResolveAlts :: [Name] -> Err' t
NoValidAlts :: [Name] -> Err' t
IncompleteTerm :: t -> Err' t

-- | Location, bad universe, old domain, new domain, suspects
UniverseError :: FC -> UExp -> (Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' t
UniqueError :: Universe -> Name -> Err' t
UniqueKindError :: Universe -> Name -> Err' t
ProgramLineComment :: Err' t
Inaccessible :: Name -> Err' t
UnknownImplicit :: Name -> Name -> Err' t
CantMatch :: t -> Err' t
NonCollapsiblePostulate :: Name -> Err' t
AlreadyDefined :: Name -> Err' t
ProofSearchFail :: Err' t -> Err' t
NoRewriting :: t -> t -> t -> Err' t
At :: FC -> Err' t -> Err' t
Elaborating :: String -> Name -> Maybe t -> Err' t -> Err' t
ElaboratingArg :: Name -> Name -> [(Name, Name)] -> Err' t -> Err' t
ProviderError :: String -> Err' t
LoadingFailed :: String -> Err' t -> Err' t
ReflectionError :: [[ErrorReportPart]] -> Err' t -> Err' t
ReflectionFailed :: String -> Err' t -> Err' t

-- | User-specified message, proof term, goals with context (first goal is
--   focused)
ElabScriptDebug :: [ErrorReportPart] -> t -> [(Name, t, [(Name, Binder t)])] -> Err' t
ElabScriptStuck :: t -> Err' t

-- | The error occurred during a top-level elaboration script
RunningElabScript :: Err' t -> Err' t
ElabScriptStaging :: Name -> Err' t
FancyMsg :: [ErrorReportPart] -> Err' t

-- | Used for error reflection
data ErrorReportPart
TextPart :: String -> ErrorReportPart
NamePart :: Name -> ErrorReportPart
TermPart :: Term -> ErrorReportPart
RawPart :: Raw -> ErrorReportPart
SubReport :: [ErrorReportPart] -> ErrorReportPart

-- | Source location. These are typically produced by <a>withExtent</a>
data FC
FC :: String -> (Int, Int) -> (Int, Int) -> FC

-- | Filename
[_fc_fname] :: FC -> String

-- | Line and column numbers for the start of the location span
[_fc_start] :: FC -> (Int, Int)

-- | Line and column numbers for the end of the location span
[_fc_end] :: FC -> (Int, Int)

-- | Locations for machine-generated terms
NoFC :: FC

-- | Locations with file only
FileFC :: String -> FC

-- | Filename
[_fc_fname] :: FC -> String

-- | FC with equality
newtype FC'
FC' :: FC -> FC'
[unwrapFC] :: FC' -> FC
data ImplicitInfo
Impl :: Bool -> Bool -> Bool -> ImplicitInfo
[tcimplementation] :: ImplicitInfo -> Bool
[toplevel_imp] :: ImplicitInfo -> Bool
[machine_gen] :: ImplicitInfo -> Bool
data IntTy
ITFixed :: NativeTy -> IntTy
ITNative :: IntTy
ITBig :: IntTy
ITChar :: IntTy

-- | Names are hierarchies of strings, describing scope (so no danger of
--   duplicate names, but need to be careful on lookup).
data Name

-- | User-provided name
UN :: !Text -> Name

-- | Root, namespaces
NS :: !Name -> [Text] -> Name

-- | Machine chosen names
MN :: !Int -> !Text -> Name

-- | Decorated function names
SN :: !SpecialName -> Name

-- | Reference to IBC file symbol table (used during serialisation)
SymRef :: Int -> Name

-- | Output annotation for pretty-printed name - decides colour
data NameOutput
TypeOutput :: NameOutput
FunOutput :: NameOutput
DataOutput :: NameOutput
MetavarOutput :: NameOutput
PostulateOutput :: NameOutput
data NameType
Bound :: NameType
Ref :: NameType

-- | Data constructor
DCon :: Int -> Int -> Bool -> NameType
[nt_tag] :: NameType -> Int
[nt_arity] :: NameType -> Int
[nt_unique] :: NameType -> Bool

-- | Type constructor
TCon :: Int -> Int -> NameType
[nt_tag] :: NameType -> Int
[nt_arity] :: NameType -> Int
data NativeTy
IT8 :: NativeTy
IT16 :: NativeTy
IT32 :: NativeTy
IT64 :: NativeTy

-- | Output annotations for pretty-printing
data OutputAnnotation

-- | ^ The name, classification, docs overview, and pretty-printed type
AnnName :: Name -> Maybe NameOutput -> Maybe String -> Maybe String -> OutputAnnotation

-- | ^ The name and whether it is implicit
AnnBoundName :: Name -> Bool -> OutputAnnotation
AnnConst :: Const -> OutputAnnotation

-- | type, doc overview
AnnData :: String -> String -> OutputAnnotation

-- | name, doc overview
AnnType :: String -> String -> OutputAnnotation
AnnKeyword :: OutputAnnotation
AnnFC :: FC -> OutputAnnotation
AnnTextFmt :: TextFormatting -> OutputAnnotation

-- | A link to this URL
AnnLink :: String -> OutputAnnotation

-- | pprint bound vars, original term
AnnTerm :: [(Name, Bool)] -> TT Name -> OutputAnnotation

-- | more general, isomorphic, or more specific
AnnSearchResult :: Ordering -> OutputAnnotation
AnnErr :: Err -> OutputAnnotation

-- | A namespace (e.g. on an import line or in a namespace declaration).
--   Stored starting at the root, with the hierarchy fully resolved. If a
--   file path is present, then the namespace represents a module imported
--   from that file.
AnnNamespace :: [Text] -> Maybe FilePath -> OutputAnnotation
AnnQuasiquote :: OutputAnnotation
AnnAntiquote :: OutputAnnotation

-- | type of syntax element: backslash or braces etc.
AnnSyntax :: String -> OutputAnnotation
data Provenance
ExpectedType :: Provenance
TooManyArgs :: Term -> Provenance
InferredVal :: Provenance
GivenVal :: Provenance
SourceTerm :: Term -> Provenance
data Raw
Var :: Name -> Raw
RBind :: Name -> Binder Raw -> Raw -> Raw
RApp :: Raw -> Raw -> Raw
RType :: Raw
RUType :: Universe -> Raw
RConstant :: Const -> Raw
data RigCount
Rig0 :: RigCount
Rig1 :: RigCount
RigW :: RigCount
data SpecialName
WhereN :: !Int -> !Name -> !Name -> SpecialName
WithN :: !Int -> !Name -> SpecialName
ImplementationN :: !Name -> [Text] -> SpecialName
ParentN :: !Name -> !Text -> SpecialName
MethodN :: !Name -> SpecialName
CaseN :: !FC' -> !Name -> SpecialName
ImplementationCtorN :: !Name -> SpecialName
MetaN :: !Name -> !Name -> SpecialName
data TC a
OK :: !a -> TC a
Error :: Err -> TC a
type Term = TT Name
class TermSize a
termsize :: TermSize a => Name -> a -> Int

-- | Text formatting output
data TextFormatting
BoldText :: TextFormatting
ItalicText :: TextFormatting
UnderlineText :: TextFormatting

-- | Terms in the core language. The type parameter is the type of
--   identifiers used for bindings and explicit named references; usually
--   we use <tt>TT <a>Name</a></tt>.
data TT n

-- | named references with type (P for <a>Parameter</a>, motivated by
--   McKinna and Pollack's Pure Type Systems Formalized)
P :: NameType -> n -> TT n -> TT n

-- | a resolved de Bruijn-indexed variable
V :: !Int -> TT n

-- | a binding
Bind :: n -> !Binder (TT n) -> TT n -> TT n

-- | function, function type, arg
App :: AppStatus n -> !TT n -> TT n -> TT n

-- | constant
Constant :: Const -> TT n

-- | argument projection; runtime only (-1) is a special case for 'subtract
--   one from BI'
Proj :: TT n -> !Int -> TT n

-- | an erased term
Erased :: TT n

-- | special case for totality checking
Impossible :: TT n

-- | For building case trees when coverage checkimg only. Marks a term as
--   being inferred by the machine, rather than given by the programmer
Inferred :: TT n -> TT n

-- | the type of types at some level
TType :: UExp -> TT n

-- | Uniqueness type universe (disjoint from TType)
UType :: Universe -> TT n
type Type = Term
data TypeInfo
TI :: [Name] -> Bool -> DataOpts -> [Int] -> [Name] -> Bool -> TypeInfo
[con_names] :: TypeInfo -> [Name]
[codata] :: TypeInfo -> Bool
[data_opts] :: TypeInfo -> DataOpts
[param_pos] :: TypeInfo -> [Int]
[mutual_types] :: TypeInfo -> [Name]
[linear_con] :: TypeInfo -> Bool

-- | Universe constraints
data UConstraint

-- | Strictly less than
ULT :: UExp -> UExp -> UConstraint

-- | Less than or equal to
ULE :: UExp -> UExp -> UConstraint
type UCs = (Int, [UConstraint])

-- | Universe expressions for universe checking
data UExp

-- | universe variable, with source file to disambiguate
UVar :: String -> Int -> UExp

-- | explicit universe level
UVal :: Int -> UExp
data Universe
NullType :: Universe
UniqueType :: Universe
AllTypes :: Universe
addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a
addBinder :: TT n -> TT n
addDef :: Name -> a -> Ctxt a -> Ctxt a
allTTNames :: Eq n => TT n -> [n]

-- | Return the arity of a (normalised) type
arity :: TT n -> Int

-- | Introduce a <a>Bind</a> into the given term for each element of the
--   given list of (name, binder) pairs.
bindAll :: [(n, Binder (TT n))] -> TT n -> TT n

-- | Pretty-printer helper for the binding site of a name
bindingOf :: Name -> Bool -> Doc OutputAnnotation

-- | Like <a>bindAll</a>, but the <a>Binder</a>s are <a>TT</a> terms
--   instead. The first argument is a function to map <tt>TT</tt> terms to
--   <tt>Binder</tt>s. This function might often be something like
--   <a>Lam</a>, which directly constructs a <tt>Binder</tt> from a
--   <tt>TT</tt> term.
bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
caseName :: Name -> Bool

-- | Get the docstring for a Const
constDocs :: Const -> String

-- | Determines whether the input constant represents a type
constIsType :: Const -> Bool
deleteDefExact :: Name -> Ctxt a -> Ctxt a
discard :: Monad m => m a -> m ()
emptyContext :: () => Map k a

-- | Empty source location
emptyFC :: FC

-- | Replace all non-free de Bruijn references in the given term with
--   references to the name of their binding.
explicitNames :: TT n -> TT n

-- | Give a notion of end location associated with an FC
fc_end :: FC -> (Int, Int)

-- | Give a notion of filename associated with an FC
fc_fname :: FC -> String

-- | Give a notion of start location associated with an FC
fc_start :: FC -> (Int, Int)

-- | Determine whether the first argument is completely contained in the
--   second
fcIn :: FC -> FC -> Bool

-- | Source location with file only
fileFC :: String -> FC

-- | Replace every non-free reference to the name of a binding in the given
--   term with a de Bruijn index.
finalise :: Eq n => TT n -> TT n
fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

-- | Cast a <a>TT</a> term to a <a>Raw</a> value, discarding universe
--   information and the types of named references and replacing all de
--   Bruijn indices with the corresponding name. It is an error if there
--   are free de Bruijn indices.
forget :: TT Name -> Raw
forgetEnv :: [Name] -> TT Name -> Raw

-- | Returns all names used free in the term
freeNames :: Eq n => TT n -> [n]

-- | Return a list of pairs of the names of the outermost <a>Pi</a>-bound
--   variables in the given term, together with their types.
getArgTys :: TT n -> [(n, TT n)]
getRetTy :: TT n -> TT n

-- | As getRetTy but substitutes names for de Bruijn indices
substRetTy :: TT n -> TT n
implicitable :: Name -> Bool

-- | Replace the outermost (index 0) de Bruijn variable with the given term
instantiate :: TT n -> TT n -> TT n
internalNS :: String
intTyName :: IntTy -> String

-- | A term is injective iff it is a data constructor, type constructor,
--   constant, the type Type, pi-binding, or an application of an injective
--   term.
isInjective :: TT n -> Bool
isTypeConst :: Const -> Bool
lookupCtxt :: Name -> Ctxt a -> [a]
lookupCtxtExact :: Name -> Ctxt a -> Maybe a

-- | Look up a name in the context, given an optional namespace. The name
--   (n) may itself have a (partial) namespace given.
--   
--   Rules for resolution:
--   
--   <ul>
--   <li>if an explicit namespace is given, return the names which match
--   it. If none match, return all names.</li>
--   <li>if the name has has explicit namespace given, return the names
--   which match it and ignore the given namespace.</li>
--   <li>otherwise, return all names.</li>
--   </ul>
lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]
mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b

-- | Returns a term representing the application of the first argument (a
--   function) to every element of the second argument.
mkApp :: TT n -> [TT n] -> TT n
nativeTyWidth :: NativeTy -> Int
nextName :: Name -> Name

-- | Returns true if V 0 and bound name n do not occur in the term
noOccurrence :: Eq n => n -> TT n -> Bool
nsroot :: Name -> Name

-- | Return number of occurrences of V 0 or bound name i the term
occurrences :: Eq n => n -> TT n -> Int
pEraseType :: TT n -> TT n
pmap :: () => (t -> b) -> (t, t) -> (b, b)

-- | Pretty-print a raw term.
pprintRaw :: [Name] -> Raw -> Doc OutputAnnotation

-- | Pretty-print a term
pprintTT :: [Name] -> TT Name -> Doc OutputAnnotation
pprintTTClause :: [(Name, Type)] -> Term -> Term -> Doc OutputAnnotation
prettyEnv :: Env -> Term -> Doc OutputAnnotation
psubst :: Eq n => n -> TT n -> TT n -> TT n

-- | Replace references to the given <a>Name</a>-like id with references to
--   de Bruijn index 0.
pToV :: Eq n => n -> TT n -> TT n

-- | Convert several names. First in the list comes out as V 0
pToVs :: Eq n => [n] -> TT n -> TT n

-- | Check whether a term has any hole bindings in it - impure if so
pureTerm :: TT Name -> Bool
raw_apply :: Raw -> [Raw] -> Raw
raw_unapply :: Raw -> (Raw, [Raw])
refsIn :: TT Name -> [Name]
safeForget :: TT Name -> Maybe Raw
safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
showCG :: Name -> String
showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
showEnvDbg :: (Show a, Eq a) => [(a, RigCount, Binder (TT a))] -> TT a -> [Char]
showSep :: String -> [String] -> String
sImplementationN :: Name -> [String] -> SpecialName
sMN :: Int -> String -> Name
sNS :: Name -> [String] -> Name
str :: Text -> String

-- | As <a>instantiate</a>, but in addition to replacing <tt><a>V</a>
--   0</tt>, replace references to the given <a>Name</a>-like id.
subst :: Eq n => n -> TT n -> TT n -> TT n

-- | As <a>subst</a>, but takes a list of (name, substitution) pairs
--   instead of a single name and substitution
substNames :: Eq n => [(n, TT n)] -> TT n -> TT n

-- | Replaces all terms equal (in the sense of <tt>(==)</tt>) to the old
--   term with the new term.
substTerm :: Eq n => TT n -> TT n -> TT n -> TT n

-- | As <a>instantiate</a>, but also decrement the indices of all de Bruijn
--   variables remaining in the term, so that there are no more references
--   to the variable that has been substituted.
substV :: TT n -> TT n -> TT n
sUN :: String -> Name

-- | Return True if the argument <a>Name</a> should be interpreted as the
--   name of a interface.
tcname :: Name -> Bool

-- | Hard-code a heuristic maximum term size, to prevent attempts to
--   serialize or force infinite or just gigantic terms
termSmallerThan :: Int -> Term -> Bool
tfail :: Err -> TC a
thead :: Text -> Char
tnull :: Text -> Bool
toAlist :: Ctxt a -> [(Name, a)]
traceWhen :: () => Bool -> String -> p -> p
txt :: String -> Text

-- | Deconstruct an application; returns the function and a list of
--   arguments
unApply :: TT n -> (TT n, [TT n])
uniqueBinders :: [Name] -> TT Name -> TT Name
uniqueName :: Name -> [Name] -> Name
uniqueNameFrom :: [Name] -> [Name] -> Name
uniqueNameSet :: Name -> Set Name -> Name
unList :: Term -> Maybe [Term]
updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

-- | Replace de Bruijn indices in the given term with explicit references
--   to the names of the bindings they refer to. It is an error if the
--   given term contains free de Bruijn indices.
vToP :: TT n -> TT n

-- | Weaken a term by adding i to each de Bruijn index (i.e. lift it over i
--   bindings)
weakenTm :: Int -> TT n -> TT n
rigPlus :: RigCount -> RigCount -> RigCount
rigMult :: RigCount -> RigCount -> RigCount
fstEnv :: () => (a, b, c) -> a
rigEnv :: () => (a, b, c) -> b
sndEnv :: () => (a, b, c) -> c
lookupBinder :: Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
envBinders :: () => [(a, b1, b2)] -> [(a, b2)]
envZero :: () => [(a, b, c)] -> [(a, RigCount, c)]
instance GHC.Classes.Ord Idris.Core.TT.OutputAnnotation
instance GHC.Generics.Generic Idris.Core.TT.OutputAnnotation
instance GHC.Classes.Eq Idris.Core.TT.OutputAnnotation
instance GHC.Show.Show Idris.Core.TT.OutputAnnotation
instance GHC.Base.Functor Idris.Core.TT.TC
instance GHC.Classes.Eq a => GHC.Classes.Eq (Idris.Core.TT.TC a)
instance GHC.Generics.Generic (Idris.Core.TT.Err' t)
instance Data.Data.Data t => Data.Data.Data (Idris.Core.TT.Err' t)
instance GHC.Base.Functor Idris.Core.TT.Err'
instance GHC.Classes.Ord t => GHC.Classes.Ord (Idris.Core.TT.Err' t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Idris.Core.TT.Err' t)
instance GHC.Generics.Generic Idris.Core.TT.ErrorReportPart
instance Data.Data.Data Idris.Core.TT.ErrorReportPart
instance GHC.Classes.Ord Idris.Core.TT.ErrorReportPart
instance GHC.Classes.Eq Idris.Core.TT.ErrorReportPart
instance GHC.Show.Show Idris.Core.TT.ErrorReportPart
instance GHC.Generics.Generic Idris.Core.TT.Provenance
instance Data.Data.Data Idris.Core.TT.Provenance
instance GHC.Classes.Ord Idris.Core.TT.Provenance
instance GHC.Classes.Eq Idris.Core.TT.Provenance
instance GHC.Show.Show Idris.Core.TT.Provenance
instance GHC.Generics.Generic Idris.Core.TT.TypeInfo
instance GHC.Show.Show Idris.Core.TT.TypeInfo
instance GHC.Generics.Generic Idris.Core.TT.DataOpt
instance GHC.Classes.Eq Idris.Core.TT.DataOpt
instance GHC.Show.Show Idris.Core.TT.DataOpt
instance GHC.Classes.Eq n => GHC.Classes.Eq (Idris.Core.TT.Datatype n)
instance GHC.Base.Functor Idris.Core.TT.Datatype
instance (GHC.Show.Show n, GHC.Classes.Eq n) => GHC.Show.Show (Idris.Core.TT.Datatype n)
instance GHC.Generics.Generic Idris.Core.TT.Raw
instance Data.Data.Data Idris.Core.TT.Raw
instance GHC.Classes.Ord Idris.Core.TT.Raw
instance GHC.Classes.Eq Idris.Core.TT.Raw
instance GHC.Show.Show Idris.Core.TT.Raw
instance GHC.Generics.Generic (Idris.Core.TT.TT n)
instance Data.Data.Data n => Data.Data.Data (Idris.Core.TT.TT n)
instance GHC.Base.Functor Idris.Core.TT.TT
instance GHC.Classes.Ord n => GHC.Classes.Ord (Idris.Core.TT.TT n)
instance GHC.Generics.Generic (Idris.Core.TT.Binder b)
instance Data.Data.Data b => Data.Data.Data (Idris.Core.TT.Binder b)
instance Data.Traversable.Traversable Idris.Core.TT.Binder
instance Data.Foldable.Foldable Idris.Core.TT.Binder
instance GHC.Base.Functor Idris.Core.TT.Binder
instance GHC.Classes.Ord b => GHC.Classes.Ord (Idris.Core.TT.Binder b)
instance GHC.Classes.Eq b => GHC.Classes.Eq (Idris.Core.TT.Binder b)
instance GHC.Show.Show b => GHC.Show.Show (Idris.Core.TT.Binder b)
instance GHC.Generics.Generic Idris.Core.TT.RigCount
instance Data.Data.Data Idris.Core.TT.RigCount
instance GHC.Classes.Ord Idris.Core.TT.RigCount
instance GHC.Classes.Eq Idris.Core.TT.RigCount
instance GHC.Show.Show Idris.Core.TT.RigCount
instance GHC.Show.Show n => GHC.Show.Show (Idris.Core.TT.AppStatus n)
instance GHC.Generics.Generic (Idris.Core.TT.AppStatus n)
instance Data.Data.Data n => Data.Data.Data (Idris.Core.TT.AppStatus n)
instance GHC.Base.Functor Idris.Core.TT.AppStatus
instance GHC.Classes.Ord n => GHC.Classes.Ord (Idris.Core.TT.AppStatus n)
instance GHC.Classes.Eq n => GHC.Classes.Eq (Idris.Core.TT.AppStatus n)
instance GHC.Generics.Generic Idris.Core.TT.NameType
instance Data.Data.Data Idris.Core.TT.NameType
instance GHC.Classes.Ord Idris.Core.TT.NameType
instance GHC.Show.Show Idris.Core.TT.NameType
instance GHC.Generics.Generic Idris.Core.TT.ConstraintFC
instance Data.Data.Data Idris.Core.TT.ConstraintFC
instance GHC.Show.Show Idris.Core.TT.ConstraintFC
instance GHC.Generics.Generic Idris.Core.TT.UConstraint
instance Data.Data.Data Idris.Core.TT.UConstraint
instance GHC.Classes.Ord Idris.Core.TT.UConstraint
instance GHC.Classes.Eq Idris.Core.TT.UConstraint
instance GHC.Generics.Generic Idris.Core.TT.UExp
instance Data.Data.Data Idris.Core.TT.UExp
instance GHC.Classes.Ord Idris.Core.TT.UExp
instance GHC.Classes.Eq Idris.Core.TT.UExp
instance GHC.Generics.Generic Idris.Core.TT.ImplicitInfo
instance Data.Data.Data Idris.Core.TT.ImplicitInfo
instance GHC.Classes.Ord Idris.Core.TT.ImplicitInfo
instance GHC.Classes.Eq Idris.Core.TT.ImplicitInfo
instance GHC.Show.Show Idris.Core.TT.ImplicitInfo
instance GHC.Generics.Generic Idris.Core.TT.Universe
instance Data.Data.Data Idris.Core.TT.Universe
instance GHC.Classes.Ord Idris.Core.TT.Universe
instance GHC.Classes.Eq Idris.Core.TT.Universe
instance GHC.Generics.Generic Idris.Core.TT.Const
instance Data.Data.Data Idris.Core.TT.Const
instance GHC.Classes.Ord Idris.Core.TT.Const
instance GHC.Generics.Generic Idris.Core.TT.ArithTy
instance Data.Data.Data Idris.Core.TT.ArithTy
instance GHC.Classes.Ord Idris.Core.TT.ArithTy
instance GHC.Classes.Eq Idris.Core.TT.ArithTy
instance GHC.Show.Show Idris.Core.TT.ArithTy
instance GHC.Generics.Generic Idris.Core.TT.IntTy
instance Data.Data.Data Idris.Core.TT.IntTy
instance GHC.Classes.Ord Idris.Core.TT.IntTy
instance GHC.Classes.Eq Idris.Core.TT.IntTy
instance GHC.Show.Show Idris.Core.TT.IntTy
instance GHC.Generics.Generic Idris.Core.TT.NativeTy
instance Data.Data.Data Idris.Core.TT.NativeTy
instance GHC.Enum.Enum Idris.Core.TT.NativeTy
instance GHC.Classes.Ord Idris.Core.TT.NativeTy
instance GHC.Classes.Eq Idris.Core.TT.NativeTy
instance GHC.Show.Show Idris.Core.TT.NativeTy
instance GHC.Generics.Generic Idris.Core.TT.Name
instance Data.Data.Data Idris.Core.TT.Name
instance GHC.Classes.Ord Idris.Core.TT.Name
instance GHC.Classes.Eq Idris.Core.TT.Name
instance GHC.Generics.Generic Idris.Core.TT.SpecialName
instance Data.Data.Data Idris.Core.TT.SpecialName
instance GHC.Classes.Ord Idris.Core.TT.SpecialName
instance GHC.Classes.Eq Idris.Core.TT.SpecialName
instance GHC.Generics.Generic Idris.Core.TT.TextFormatting
instance GHC.Classes.Ord Idris.Core.TT.TextFormatting
instance GHC.Classes.Eq Idris.Core.TT.TextFormatting
instance GHC.Show.Show Idris.Core.TT.TextFormatting
instance GHC.Generics.Generic Idris.Core.TT.NameOutput
instance GHC.Classes.Ord Idris.Core.TT.NameOutput
instance GHC.Classes.Eq Idris.Core.TT.NameOutput
instance GHC.Show.Show Idris.Core.TT.NameOutput
instance GHC.Classes.Ord Idris.Core.TT.FC'
instance GHC.Generics.Generic Idris.Core.TT.FC'
instance Data.Data.Data Idris.Core.TT.FC'
instance GHC.Classes.Ord Idris.Core.TT.FC
instance GHC.Generics.Generic Idris.Core.TT.FC
instance Data.Data.Data Idris.Core.TT.FC
instance GHC.Classes.Eq Idris.Core.TT.Option
instance Util.Pretty.Pretty Idris.Core.TT.Err Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Pretty a Idris.Core.TT.OutputAnnotation => Util.Pretty.Pretty (Idris.Core.TT.TC a) Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Pretty Idris.Core.TT.Name Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Pretty [Idris.Core.TT.Name] Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Pretty Idris.Core.TT.NativeTy Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Pretty Idris.Core.TT.ArithTy Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Pretty Idris.Core.TT.Const Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Pretty Idris.Core.TT.Raw Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Pretty Idris.Core.TT.NameType Idris.Core.TT.OutputAnnotation
instance GHC.Base.Monad Idris.Core.TT.TC
instance GHC.Base.MonadPlus Idris.Core.TT.TC
instance GHC.Base.Applicative Idris.Core.TT.TC
instance GHC.Base.Alternative Idris.Core.TT.TC
instance GHC.Show.Show a => GHC.Show.Show (Idris.Core.TT.TC a)
instance Util.Pretty.Sized Idris.Core.TT.Err
instance GHC.Show.Show Idris.Core.TT.Err
instance Util.Pretty.Sized Idris.Core.TT.ErrorReportPart
instance Util.Pretty.Sized Idris.Core.TT.Raw
instance Idris.Core.TT.TermSize (Idris.Core.TT.TT Idris.Core.TT.Name)
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.Core.TT.TT a)
instance Util.Pretty.Pretty a o => Util.Pretty.Pretty (Idris.Core.TT.TT a) o
instance GHC.Classes.Eq n => GHC.Classes.Eq (Idris.Core.TT.TT n)
instance (GHC.Classes.Eq n, GHC.Show.Show n) => GHC.Show.Show (Idris.Core.TT.TT n)
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.Core.TT.Binder a)
instance Idris.Core.TT.TermSize a => Idris.Core.TT.TermSize [a]
instance Util.Pretty.Sized Idris.Core.TT.NameType
instance GHC.Classes.Eq Idris.Core.TT.NameType
instance GHC.Classes.Eq Idris.Core.TT.ConstraintFC
instance GHC.Classes.Ord Idris.Core.TT.ConstraintFC
instance GHC.Show.Show Idris.Core.TT.UConstraint
instance Util.Pretty.Sized Idris.Core.TT.UExp
instance GHC.Show.Show Idris.Core.TT.UExp
instance GHC.Show.Show Idris.Core.TT.Universe
instance Util.Pretty.Sized Idris.Core.TT.Universe
instance GHC.Classes.Eq Idris.Core.TT.Const
instance Util.Pretty.Sized Idris.Core.TT.Const
instance GHC.Show.Show Idris.Core.TT.Const
instance Util.Pretty.Sized Idris.Core.TT.Name
instance GHC.Show.Show Idris.Core.TT.Name
instance GHC.Show.Show Idris.Core.TT.SpecialName
instance GHC.Classes.Eq Idris.Core.TT.FC'
instance GHC.Show.Show Idris.Core.TT.FC'
instance GHC.Base.Semigroup Idris.Core.TT.FC
instance GHC.Base.Monoid Idris.Core.TT.FC
instance GHC.Classes.Eq Idris.Core.TT.FC
instance Util.Pretty.Sized Idris.Core.TT.FC
instance GHC.Show.Show Idris.Core.TT.FC


module Idris.Unlit
unlit :: FilePath -> String -> TC String


module Idris.Docstrings

-- | Representation of Idris's inline documentation. The type paramter
--   represents the type of terms that are associated with code blocks.
data Docstring a
DocString :: Options -> Blocks a -> Docstring a

-- | Block-level elements.
data Block a
Para :: Inlines a -> Block a
Header :: Int -> Inlines a -> Block a
Blockquote :: Blocks a -> Block a
List :: Bool -> ListType -> [Blocks a] -> Block a
CodeBlock :: CodeAttr -> Text -> a -> Block a
HtmlBlock :: Text -> Block a
HRule :: Block a
data Inline a
Str :: Text -> Inline a
Space :: Inline a
SoftBreak :: Inline a
LineBreak :: Inline a
Emph :: Inlines a -> Inline a
Strong :: Inlines a -> Inline a
Code :: Text -> a -> Inline a
Link :: Inlines a -> Text -> Text -> Inline a
Image :: Inlines a -> Text -> Text -> Inline a
Entity :: Text -> Inline a
RawHtml :: Text -> Inline a

-- | Construct a docstring from a Text that contains Markdown-formatted
--   docs
parseDocstring :: Text -> Docstring ()

-- | Convert a docstring to be shown by the pretty-printer
renderDocstring :: (a -> String -> Doc OutputAnnotation) -> Docstring a -> Doc OutputAnnotation

-- | The empty docstring
emptyDocstring :: Docstring a

-- | Check whether a docstring is emtpy
nullDocstring :: Docstring a -> Bool

-- | Empty documentation for a definition
noDocs :: (Docstring a, [(Name, Docstring a)])

-- | Construct a docstring consisting of the first block-level element of
--   the argument docstring, for use in summaries.
overview :: Docstring a -> Docstring a

-- | Does a string occur in the docstring?
containsText :: Text -> Docstring a -> Bool
renderHtml :: Docstring DocTerm -> Html

-- | Annotate the code samples in a docstring
annotCode :: forall a b. (String -> b) -> Docstring a -> Docstring b

-- | The various kinds of code samples that can be embedded in docs
data DocTerm
Unchecked :: DocTerm
Checked :: Term -> DocTerm
Example :: Term -> DocTerm
Failing :: Err -> DocTerm

-- | Render a term in the documentation
renderDocTerm :: (Term -> Doc OutputAnnotation) -> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation

-- | Run some kind of processing step over code in a Docstring. The code
--   processor gets the language and annotations as parameters, along with
--   the source and the original annotation.
checkDocstring :: forall a b. (String -> [String] -> String -> a -> b) -> Docstring a -> Docstring b
instance GHC.Generics.Generic (Idris.Docstrings.Docstring a)
instance Data.Traversable.Traversable Idris.Docstrings.Docstring
instance Data.Foldable.Foldable Idris.Docstrings.Docstring
instance GHC.Base.Functor Idris.Docstrings.Docstring
instance GHC.Show.Show a => GHC.Show.Show (Idris.Docstrings.Docstring a)
instance GHC.Generics.Generic (Idris.Docstrings.Block a)
instance Data.Traversable.Traversable Idris.Docstrings.Block
instance Data.Foldable.Foldable Idris.Docstrings.Block
instance GHC.Base.Functor Idris.Docstrings.Block
instance GHC.Show.Show a => GHC.Show.Show (Idris.Docstrings.Block a)
instance GHC.Generics.Generic (Idris.Docstrings.Inline a)
instance Data.Traversable.Traversable Idris.Docstrings.Inline
instance Data.Foldable.Foldable Idris.Docstrings.Inline
instance GHC.Base.Functor Idris.Docstrings.Inline
instance GHC.Show.Show a => GHC.Show.Show (Idris.Docstrings.Inline a)
instance GHC.Generics.Generic Idris.Docstrings.DocTerm
instance GHC.Show.Show Idris.Docstrings.DocTerm


module Idris.Core.Constraints

-- | Check that a list of universe constraints can be satisfied.
ucheck :: Set ConstraintFC -> TC ()
instance GHC.Show.Show Idris.Core.Constraints.Domain
instance GHC.Classes.Ord Idris.Core.Constraints.Domain
instance GHC.Classes.Eq Idris.Core.Constraints.Domain
instance GHC.Show.Show Idris.Core.Constraints.Var
instance GHC.Classes.Ord Idris.Core.Constraints.Var
instance GHC.Classes.Eq Idris.Core.Constraints.Var


-- | Note: The case-tree elaborator only produces (Case n alts)-cases; in
--   other words, it never inspects anything else than variables.
--   
--   ProjCase is a special powerful case construct that allows inspection
--   of compound terms. Occurrences of ProjCase arise no earlier than in
--   the function <a>prune</a> as a means of optimisation of already built
--   case trees.
--   
--   While the intermediate representation (follows in the pipeline, named
--   LExp) allows casing on arbitrary terms, here we choose to maintain the
--   distinction in order to allow for better optimisation opportunities.
module Idris.Core.CaseTree
data CaseDef
CaseDef :: [Name] -> !SC -> [Term] -> CaseDef
type SC = SC' Term
data SC' t

-- | invariant: lowest tags first
Case :: CaseType -> Name -> [CaseAlt' t] -> SC' t

-- | special case for projections/thunk-forcing before inspection
ProjCase :: t -> [CaseAlt' t] -> SC' t
STerm :: !t -> SC' t

-- | error message
UnmatchedCase :: String -> SC' t

-- | already checked to be impossible
ImpossibleCase :: SC' t
type CaseAlt = CaseAlt' Term
data CaseAlt' t
ConCase :: Name -> Int -> [Name] -> !SC' t -> CaseAlt' t

-- | reflection function
FnCase :: Name -> [Name] -> !SC' t -> CaseAlt' t
ConstCase :: Const -> !SC' t -> CaseAlt' t
SucCase :: Name -> !SC' t -> CaseAlt' t
DefaultCase :: !SC' t -> CaseAlt' t
type ErasureInfo = Name -> [Int]
data Phase
CoverageCheck :: [Int] -> Phase
CompileTime :: Phase
RunTime :: Phase
type CaseTree = SC
data CaseType
Updatable :: CaseType
Shared :: CaseType
simpleCase :: Bool -> SC -> Bool -> Phase -> FC -> [Int] -> [(Type, Bool)] -> [([Name], Term, Term)] -> ErasureInfo -> TC CaseDef
small :: Name -> [Name] -> SC -> Bool
namesUsed :: SC -> [Name]

-- | Return all called functions, and which arguments are used in each
--   argument position for the call, in order to help reduce compilation
--   time, and trace all unused arguments
findCalls :: SC -> [Name] -> [(Name, [[Name]])]
findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]
findUsedArgs :: SC -> [Name] -> [Name]
substSC :: Name -> Name -> SC -> SC
substAlt :: Name -> Name -> CaseAlt -> CaseAlt
mkForce :: Name -> Name -> SC -> SC
instance GHC.Show.Show Idris.Core.CaseTree.Group
instance GHC.Classes.Eq Idris.Core.CaseTree.ConType
instance GHC.Show.Show Idris.Core.CaseTree.ConType
instance GHC.Show.Show Idris.Core.CaseTree.Partition
instance GHC.Show.Show Idris.Core.CaseTree.Pat
instance GHC.Classes.Eq Idris.Core.CaseTree.Phase
instance GHC.Show.Show Idris.Core.CaseTree.Phase
instance GHC.Show.Show Idris.Core.CaseTree.CaseDef
instance GHC.Generics.Generic (Idris.Core.CaseTree.SC' t)
instance GHC.Base.Functor Idris.Core.CaseTree.SC'
instance GHC.Classes.Ord t => GHC.Classes.Ord (Idris.Core.CaseTree.SC' t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Idris.Core.CaseTree.SC' t)
instance GHC.Generics.Generic (Idris.Core.CaseTree.CaseAlt' t)
instance GHC.Base.Functor Idris.Core.CaseTree.CaseAlt'
instance GHC.Classes.Ord t => GHC.Classes.Ord (Idris.Core.CaseTree.CaseAlt' t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Idris.Core.CaseTree.CaseAlt' t)
instance GHC.Show.Show t => GHC.Show.Show (Idris.Core.CaseTree.CaseAlt' t)
instance GHC.Generics.Generic Idris.Core.CaseTree.CaseType
instance GHC.Show.Show Idris.Core.CaseTree.CaseType
instance GHC.Classes.Ord Idris.Core.CaseTree.CaseType
instance GHC.Classes.Eq Idris.Core.CaseTree.CaseType
instance Idris.Core.TT.TermSize Idris.Core.CaseTree.CaseAlt
instance Idris.Core.TT.TermSize Idris.Core.CaseTree.SC
instance GHC.Show.Show t => GHC.Show.Show (Idris.Core.CaseTree.SC' t)


module Idris.Core.Evaluate
normalise :: Context -> Env -> TT Name -> TT Name
normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name

-- | Normalise fully type checked terms (so, assume all names/let bindings
--   resolved)
normaliseC :: Context -> Env -> TT Name -> TT Name

-- | Normalise everything, whether abstract, private or public
normaliseAll :: Context -> Env -> TT Name -> TT Name

-- | As normaliseAll, but with an explicit list of names *not* to reduce
normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name
toValue :: Context -> Env -> TT Name -> Value
quoteTerm :: Value -> TT Name

-- | Simplify for run-time (i.e. basic inlining)
rt_simplify :: Context -> Env -> TT Name -> TT Name

-- | Like normalise, but we only reduce functions that are marked as okay
--   to inline, and lets
simplify :: Context -> Env -> TT Name -> TT Name

-- | Like simplify, but we only reduce functions that are marked as okay to
--   inline, and don't reduce lets
inlineSmall :: Context -> Env -> TT Name -> TT Name
specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> (TT Name, [(Name, Int)])

-- | Unfold the given names in a term, the given number of times in a
--   stack. Preserves 'let'. This is primarily to support inlining of the
--   given names, and can also help with partial evaluation by allowing a
--   rescursive definition to be unfolded once only. Specifically used to
--   unfold definitions using interfaces before going to the totality
--   checker (otherwise mutually recursive definitions in implementations
--   will not work...)
unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
convEq' :: Context -> [Name] -> TT Name -> TT Name -> TC Bool

-- | A definition is either a simple function (just an expression with a
--   type), a constant, which could be a data or type constructor, an axiom
--   or as an yet undefined function, or an Operator. An Operator is a
--   function which explains how to reduce. A CaseOp is a function defined
--   by a simple case tree
data Def
Function :: !Type -> !Term -> Def
TyDecl :: NameType -> !Type -> Def
Operator :: Type -> Int -> ([Value] -> Maybe Value) -> Def
CaseOp :: CaseInfo -> !Type -> ![(Type, Bool)] -> ![Either Term (Term, Term)] -> ![([Name], Term, Term)] -> !CaseDefs -> Def
data CaseInfo
CaseInfo :: Bool -> Bool -> Bool -> CaseInfo
[case_inlinable] :: CaseInfo -> Bool
[case_alwaysinline] :: CaseInfo -> Bool
[tc_dictionary] :: CaseInfo -> Bool
data CaseDefs
CaseDefs :: !([Name], SC) -> !([Name], SC) -> CaseDefs
[cases_compiletime] :: CaseDefs -> !([Name], SC)
[cases_runtime] :: CaseDefs -> !([Name], SC)
data Accessibility
Hidden :: Accessibility
Public :: Accessibility
Frozen :: Accessibility
Private :: Accessibility
type Injectivity = Bool

-- | The result of totality checking
data Totality

-- | well-founded arguments
Total :: [Int] -> Totality

-- | productive
Productive :: Totality
Partial :: PReason -> Totality
Unchecked :: Totality
Generated :: Totality
type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)

-- | Reasons why a function may not be total
data PReason
Other :: [Name] -> PReason
Itself :: PReason
NotCovering :: PReason
NotPositive :: PReason
UseUndef :: Name -> PReason
ExternalIO :: PReason
BelieveMe :: PReason
Mutual :: [Name] -> PReason
NotProductive :: PReason
data MetaInformation

-- | No meta-information
EmptyMI :: MetaInformation

-- | Meta information for a data declaration with position of parameters
DataMI :: [Int] -> MetaInformation

-- | Contexts used for global definitions and for proof state. They contain
--   universe constraints and existing definitions. Also store maximum
--   RigCount of the name (can't bind a name at multiplicity 1 in a RigW,
--   for example)
data Context

-- | The initial empty context
initContext :: Context

-- | Get the definitions from a context
ctxtAlist :: Context -> [(Name, Def)]
next_tvar :: Context -> Int
addToCtxt :: Name -> Term -> Type -> Context -> Context
setAccess :: Name -> Accessibility -> Context -> Context
setInjective :: Name -> Injectivity -> Context -> Context
setTotal :: Name -> Totality -> Context -> Context
setRigCount :: Name -> RigCount -> Context -> Context
setMetaInformation :: Name -> MetaInformation -> Context -> Context
addCtxtDef :: Name -> Def -> Context -> Context
addTyDecl :: Name -> NameType -> Type -> Context -> Context
addDatatype :: Datatype Name -> Context -> Context
addCasedef :: Name -> ErasureInfo -> CaseInfo -> Bool -> SC -> Bool -> Bool -> [(Type, Bool)] -> [Int] -> [Either Term (Term, Term)] -> [([Name], Term, Term)] -> [([Name], Term, Term)] -> Type -> Context -> TC Context
simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context
lookupNames :: Name -> Context -> [Name]

-- | Get the list of pairs of fully-qualified names and their types that
--   match some name
lookupTyName :: Name -> Context -> [(Name, Type)]

-- | Get the pair of a fully-qualified name and its type, if there is a
--   unique one matching the name used as a key.
lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)

-- | Get the types that match some name
lookupTy :: Name -> Context -> [Type]

-- | Get the single type that matches some name precisely
lookupTyExact :: Name -> Context -> Maybe Type
lookupP :: Name -> Context -> [Term]
lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
lookupDef :: Name -> Context -> [Def]
lookupNameDef :: Name -> Context -> [(Name, Def)]
lookupDefExact :: Name -> Context -> Maybe Def
lookupDefAcc :: Name -> Bool -> Context -> [(Def, Accessibility)]
lookupDefAccExact :: Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupVal :: Name -> Context -> [Value]
mapDefCtxt :: (Def -> Def) -> Context -> Context
tcReducible :: Name -> Context -> Bool
lookupTotalAccessibility :: Name -> Context -> [(Totality, Accessibility)]
lookupTotal :: Name -> Context -> [Totality]
lookupTotalExact :: Name -> Context -> Maybe Totality
lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
lookupRigCount :: Name -> Context -> [Totality]
lookupRigCountExact :: Name -> Context -> Maybe RigCount
lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupMetaInformation :: Name -> Context -> [MetaInformation]
lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type)
isTCDict :: Name -> Context -> Bool

-- | Return true if the given type is a concrete type familyor primitive
--   False it it's a function to compute a type or a variable
isCanonical :: Type -> Context -> Bool

-- | Check whether a resolved name is certainly a data constructor
isDConName :: Name -> Context -> Bool

-- | Check whether any overloading of a name is a data constructor
canBeDConName :: Name -> Context -> Bool
isTConName :: Name -> Context -> Bool
isConName :: Name -> Context -> Bool
isFnName :: Name -> Context -> Bool
conGuarded :: Context -> Name -> Term -> Bool

-- | A HOAS representation of values
data Value
VP :: NameType -> Name -> Value -> Value
VV :: Int -> Value
VBind :: Bool -> Name -> Binder Value -> (Value -> Eval Value) -> Value
VBLet :: RigCount -> Int -> Name -> Value -> Value -> Value -> Value
VApp :: Value -> Value -> Value
VType :: UExp -> Value
VUType :: Universe -> Value
VErased :: Value
VImpossible :: Value
VConstant :: Const -> Value
VProj :: Value -> Int -> Value
VTmp :: Int -> Value
class Quote a
quote :: Quote a => Int -> a -> Eval (TT Name)
initEval :: EvalState

-- | Create a unique name given context and other existing names
uniqueNameCtxt :: Context -> Name -> [Name] -> Name
uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
definitions :: Context -> Ctxt TTDecl
visibleDefinitions :: Context -> Ctxt TTDecl
isUniverse :: Term -> Bool
linearCheck :: Context -> Type -> TC ()
linearCheckArg :: Context -> Type -> TC ()
instance GHC.Generics.Generic Idris.Core.Evaluate.Context
instance GHC.Show.Show Idris.Core.Evaluate.Context
instance GHC.Generics.Generic Idris.Core.Evaluate.MetaInformation
instance GHC.Show.Show Idris.Core.Evaluate.MetaInformation
instance GHC.Classes.Eq Idris.Core.Evaluate.MetaInformation
instance GHC.Generics.Generic Idris.Core.Evaluate.Totality
instance GHC.Classes.Eq Idris.Core.Evaluate.Totality
instance GHC.Generics.Generic Idris.Core.Evaluate.PReason
instance GHC.Classes.Eq Idris.Core.Evaluate.PReason
instance GHC.Show.Show Idris.Core.Evaluate.PReason
instance GHC.Generics.Generic Idris.Core.Evaluate.Accessibility
instance GHC.Classes.Ord Idris.Core.Evaluate.Accessibility
instance GHC.Classes.Eq Idris.Core.Evaluate.Accessibility
instance GHC.Generics.Generic Idris.Core.Evaluate.Def
instance GHC.Generics.Generic Idris.Core.Evaluate.CaseInfo
instance GHC.Generics.Generic Idris.Core.Evaluate.CaseDefs
instance GHC.Classes.Eq Idris.Core.Evaluate.EvalOpt
instance GHC.Show.Show Idris.Core.Evaluate.EvalOpt
instance GHC.Show.Show Idris.Core.Evaluate.EvalState
instance GHC.Show.Show Idris.Core.Evaluate.Totality
instance GHC.Show.Show Idris.Core.Evaluate.Accessibility
instance GHC.Show.Show Idris.Core.Evaluate.Def
instance GHC.Show.Show Idris.Core.Evaluate.Value
instance GHC.Classes.Eq Idris.Core.Evaluate.Value
instance Idris.Core.Evaluate.Quote Idris.Core.Evaluate.Value
instance GHC.Show.Show (a -> b)


module Idris.Core.WHNF

-- | Reduce a term to weak head normal form.
whnf :: Context -> Env -> Term -> Term

-- | Reduce a type so that all arguments are expanded
whnfArgs :: Context -> Env -> Term -> Term
data WEnv
instance GHC.Show.Show Idris.Core.WHNF.WEnv


-- | Unification is applied inside the theorem prover. We're looking for
--   holes which can be filled in, by matching one term's normal form
--   against another. Returns a list of hole names paired with the term
--   which solves them, and a list of things which need to be injective.
module Idris.Core.Unify
match_unify :: Context -> Env -> (TT Name, Maybe Provenance) -> (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] -> TC [(Name, TT Name)]
unify :: Context -> Env -> (TT Name, Maybe Provenance) -> (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [Name] -> [FailContext] -> TC ([(Name, TT Name)], Fails)
type Fails = [(TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)]
data FailContext
FailContext :: FC -> Name -> Name -> FailContext
[fail_sourceloc] :: FailContext -> FC
[fail_fn] :: FailContext -> Name
[fail_param] :: FailContext -> Name
data FailAt
Match :: FailAt
Unify :: FailAt
unrecoverable :: Fails -> Bool
instance GHC.Show.Show Idris.Core.Unify.UInfo
instance GHC.Show.Show Idris.Core.Unify.FailContext
instance GHC.Classes.Eq Idris.Core.Unify.FailContext
instance GHC.Classes.Eq Idris.Core.Unify.FailAt
instance GHC.Show.Show Idris.Core.Unify.FailAt


module Idris.Core.Typecheck
convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()
converts :: Context -> Env -> Term -> Term -> TC ()
isHole :: () => (a, b1, Binder b2) -> Bool
errEnv :: () => [(a, b1, Binder b2)] -> [(a, b2)]
isType :: Context -> Env -> Term -> TC ()
convType :: String -> Context -> Env -> Term -> StateT UCs TC ()
recheck :: String -> Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
recheck_borrowing :: Bool -> [Name] -> String -> Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
check :: Context -> Env -> Raw -> TC (Term, Type)
check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
data UniqueUse
Never :: UniqueUse
Once :: UniqueUse
LendOnly :: UniqueUse
Many :: UniqueUse
checkUnique :: [Name] -> Context -> Env -> Term -> TC ()
instance GHC.Classes.Eq Idris.Core.Typecheck.UniqueUse


module Idris.Core.ProofTerm
data ProofTerm
data Goal
GD :: Env -> Binder Term -> Goal
[premises] :: Goal -> Env
[goalType] :: Goal -> Binder Term
mkProofTerm :: Term -> ProofTerm
getProofTerm :: ProofTerm -> Term
resetProofTerm :: ProofTerm -> ProofTerm
updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

-- | Given a list of solved holes, fill out the solutions in a term
updateSolvedTerm :: [(Name, Term)] -> Term -> Term

-- | Given a list of solved holes, fill out the solutions in a term. Return
--   whether updates were performed, to facilitate sharing when there are
--   no updates.
updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
bound_in :: ProofTerm -> [Name]
bound_in_term :: Term -> [Name]

-- | Refocus the proof term zipper on a particular hole, if it exists. If
--   not, return the original proof term.
refocus :: Hole -> ProofTerm -> ProofTerm

-- | As <a>subst</a>, in TT, but takes advantage of knowing not to
--   substitute under Complete applications.
updsubst :: Eq n => n -> TT n -> TT n -> TT n
type Hole = Maybe Name
type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
goal :: Hole -> ProofTerm -> TC Goal
atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm -> StateT a TC (ProofTerm, Bool)
instance GHC.Show.Show Idris.Core.ProofTerm.ProofTerm
instance GHC.Show.Show Idris.Core.ProofTerm.TermPath
instance GHC.Show.Show Idris.Core.ProofTerm.BinderPath


module Idris.Core.DeepSeq

-- | Forcing the contents of a context, for diagnosing and working around
--   space leaks
forceDefCtxt :: Context -> Context
instance Control.DeepSeq.NFData Idris.Core.TT.Name
instance Control.DeepSeq.NFData Idris.Core.Evaluate.Context
instance Control.DeepSeq.NFData Idris.Core.TT.NameOutput
instance Control.DeepSeq.NFData Idris.Core.TT.TextFormatting
instance Control.DeepSeq.NFData Idris.Core.TT.OutputAnnotation
instance Control.DeepSeq.NFData Idris.Core.TT.SpecialName
instance Control.DeepSeq.NFData Idris.Core.TT.Universe
instance Control.DeepSeq.NFData Idris.Core.TT.Raw
instance Control.DeepSeq.NFData Idris.Core.TT.FC
instance Control.DeepSeq.NFData Idris.Core.TT.FC'
instance Control.DeepSeq.NFData Idris.Core.TT.Provenance
instance Control.DeepSeq.NFData Idris.Core.TT.UConstraint
instance Control.DeepSeq.NFData Idris.Core.TT.ConstraintFC
instance Control.DeepSeq.NFData Idris.Core.TT.Err
instance Control.DeepSeq.NFData Idris.Core.TT.ErrorReportPart
instance Control.DeepSeq.NFData Idris.Core.TT.ImplicitInfo
instance Control.DeepSeq.NFData Idris.Core.TT.RigCount
instance Control.DeepSeq.NFData b => Control.DeepSeq.NFData (Idris.Core.TT.Binder b)
instance Control.DeepSeq.NFData Idris.Core.TT.UExp
instance Control.DeepSeq.NFData Idris.Core.TT.NameType
instance Control.DeepSeq.NFData Idris.Core.TT.NativeTy
instance Control.DeepSeq.NFData Idris.Core.TT.IntTy
instance Control.DeepSeq.NFData Idris.Core.TT.ArithTy
instance Control.DeepSeq.NFData Idris.Core.TT.Const
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Idris.Core.TT.AppStatus a)
instance Control.DeepSeq.NFData n => Control.DeepSeq.NFData (Idris.Core.TT.TT n)
instance Control.DeepSeq.NFData Idris.Core.Evaluate.Accessibility
instance Control.DeepSeq.NFData Idris.Core.Evaluate.Totality
instance Control.DeepSeq.NFData Idris.Core.Evaluate.PReason
instance Control.DeepSeq.NFData Idris.Core.Evaluate.MetaInformation
instance Control.DeepSeq.NFData Idris.Core.Evaluate.Def
instance Control.DeepSeq.NFData Idris.Core.Evaluate.CaseInfo
instance Control.DeepSeq.NFData Idris.Core.Evaluate.CaseDefs
instance Control.DeepSeq.NFData Idris.Core.CaseTree.CaseType
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.Core.CaseTree.SC' t)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.Core.CaseTree.CaseAlt' t)


module Idris.Core.Binary
instance Data.Binary.Class.Binary Idris.Core.TT.ErrorReportPart
instance Data.Binary.Class.Binary Idris.Core.TT.Provenance
instance Data.Binary.Class.Binary Idris.Core.TT.UConstraint
instance Data.Binary.Class.Binary Idris.Core.TT.ConstraintFC
instance Data.Binary.Class.Binary a => Data.Binary.Class.Binary (Idris.Core.TT.Err' a)
instance Data.Binary.Class.Binary Idris.Core.TT.FC
instance Data.Binary.Class.Binary Idris.Core.TT.FC'
instance Data.Binary.Class.Binary Idris.Core.TT.Name
instance Data.Binary.Class.Binary Idris.Core.TT.SpecialName
instance Data.Binary.Class.Binary Idris.Core.TT.Const
instance Data.Binary.Class.Binary Idris.Core.TT.Raw
instance Data.Binary.Class.Binary Idris.Core.TT.RigCount
instance Data.Binary.Class.Binary Idris.Core.TT.ImplicitInfo
instance Data.Binary.Class.Binary b => Data.Binary.Class.Binary (Idris.Core.TT.Binder b)
instance Data.Binary.Class.Binary Idris.Core.TT.Universe
instance Data.Binary.Class.Binary Idris.Core.TT.NameType
instance Data.Binary.Class.Binary Idris.Core.TT.UExp
instance Data.Binary.Class.Binary (Idris.Core.TT.TT Idris.Core.TT.Name)


module Idris.IdeMode
parseMessage :: String -> Either Err (SExp, Integer)
convSExp :: SExpable a => String -> a -> Integer -> String
data WhatDocs
Overview :: WhatDocs
Full :: WhatDocs
data IdeModeCommand
REPLCompletions :: String -> IdeModeCommand
Interpret :: String -> IdeModeCommand
TypeOf :: String -> IdeModeCommand
CaseSplit :: Int -> String -> IdeModeCommand
AddClause :: Int -> String -> IdeModeCommand
AddProofClause :: Int -> String -> IdeModeCommand
AddMissing :: Int -> String -> IdeModeCommand
MakeWithBlock :: Int -> String -> IdeModeCommand
MakeCaseBlock :: Int -> String -> IdeModeCommand

-- | ^ Recursive?, line, name, hints, depth
ProofSearch :: Bool -> Int -> String -> [String] -> Maybe Int -> IdeModeCommand
MakeLemma :: Int -> String -> IdeModeCommand
LoadFile :: String -> Maybe Int -> IdeModeCommand
DocsFor :: String -> WhatDocs -> IdeModeCommand
Apropos :: String -> IdeModeCommand
GetOpts :: IdeModeCommand
SetOpt :: Opt -> Bool -> IdeModeCommand

-- | ^ the Int is the column count for pretty-printing
Metavariables :: Int -> IdeModeCommand
WhoCalls :: String -> IdeModeCommand
CallsWho :: String -> IdeModeCommand
BrowseNS :: String -> IdeModeCommand
TermNormalise :: [(Name, Bool)] -> Term -> IdeModeCommand
TermShowImplicits :: [(Name, Bool)] -> Term -> IdeModeCommand
TermNoImplicits :: [(Name, Bool)] -> Term -> IdeModeCommand
TermElab :: [(Name, Bool)] -> Term -> IdeModeCommand
PrintDef :: String -> IdeModeCommand
ErrString :: Err -> IdeModeCommand
ErrPPrint :: Err -> IdeModeCommand
GetIdrisVersion :: IdeModeCommand
sexpToCommand :: SExp -> Maybe IdeModeCommand
toSExp :: SExpable a => a -> SExp
data SExp
SexpList :: [SExp] -> SExp
StringAtom :: String -> SExp
BoolAtom :: Bool -> SExp
IntegerAtom :: Integer -> SExp
SymbolAtom :: String -> SExp
class SExpable a
data Opt
ShowImpl :: Opt
ErrContext :: Opt

-- | The version of the IDE mode command set. Increment this when you
--   change it so clients can adapt.
ideModeEpoch :: Int
getLen :: Handle -> IO (Either Err Int)
getNChar :: Handle -> Int -> String -> IO String
sExpToString :: SExp -> String
instance GHC.Show.Show Idris.IdeMode.Opt
instance GHC.Show.Show Idris.IdeMode.SExp
instance GHC.Classes.Eq Idris.IdeMode.SExp
instance Idris.IdeMode.SExpable Idris.IdeMode.SExp
instance Idris.IdeMode.SExpable GHC.Types.Bool
instance Idris.IdeMode.SExpable GHC.Base.String
instance Idris.IdeMode.SExpable GHC.Integer.Type.Integer
instance Idris.IdeMode.SExpable GHC.Types.Int
instance Idris.IdeMode.SExpable Idris.Core.TT.Name
instance Idris.IdeMode.SExpable a => Idris.IdeMode.SExpable (GHC.Maybe.Maybe a)
instance Idris.IdeMode.SExpable a => Idris.IdeMode.SExpable [a]
instance (Idris.IdeMode.SExpable a, Idris.IdeMode.SExpable b) => Idris.IdeMode.SExpable (a, b)
instance (Idris.IdeMode.SExpable a, Idris.IdeMode.SExpable b, Idris.IdeMode.SExpable c) => Idris.IdeMode.SExpable (a, b, c)
instance (Idris.IdeMode.SExpable a, Idris.IdeMode.SExpable b, Idris.IdeMode.SExpable c, Idris.IdeMode.SExpable d) => Idris.IdeMode.SExpable (a, b, c, d)
instance (Idris.IdeMode.SExpable a, Idris.IdeMode.SExpable b, Idris.IdeMode.SExpable c, Idris.IdeMode.SExpable d, Idris.IdeMode.SExpable e) => Idris.IdeMode.SExpable (a, b, c, d, e)
instance Idris.IdeMode.SExpable Idris.Core.TT.NameOutput
instance Idris.IdeMode.SExpable Idris.Core.TT.OutputAnnotation
instance Idris.IdeMode.SExpable Idris.Core.TT.FC


module IRTS.Lang
data Endianness
Native :: Endianness
BE :: Endianness
LE :: Endianness
data LVar
Loc :: Int -> LVar
Glob :: Name -> LVar
data LExp
LV :: Name -> LExp
LApp :: Bool -> LExp -> [LExp] -> LExp
LLazyApp :: Name -> [LExp] -> LExp
LLazyExp :: LExp -> LExp
LForce :: LExp -> LExp
LLet :: Name -> LExp -> LExp -> LExp
LLam :: [Name] -> LExp -> LExp
LProj :: LExp -> Int -> LExp
LCon :: Maybe Name -> Int -> Name -> [LExp] -> LExp
LCase :: CaseType -> LExp -> [LAlt] -> LExp
LConst :: Const -> LExp
LForeign :: FDesc -> FDesc -> [(FDesc, LExp)] -> LExp
LOp :: PrimFn -> [LExp] -> LExp
LNothing :: LExp
LError :: String -> LExp
data FDesc
FCon :: Name -> FDesc
FStr :: String -> FDesc
FUnknown :: FDesc
FIO :: FDesc -> FDesc
FApp :: Name -> [FDesc] -> FDesc
data Export
ExportData :: FDesc -> Export
ExportFun :: Name -> FDesc -> FDesc -> [FDesc] -> Export
data ExportIFace
Export :: Name -> String -> [Export] -> ExportIFace
data PrimFn
LPlus :: ArithTy -> PrimFn
LMinus :: ArithTy -> PrimFn
LTimes :: ArithTy -> PrimFn
LUDiv :: IntTy -> PrimFn
LSDiv :: ArithTy -> PrimFn
LURem :: IntTy -> PrimFn
LSRem :: ArithTy -> PrimFn
LAnd :: IntTy -> PrimFn
LOr :: IntTy -> PrimFn
LXOr :: IntTy -> PrimFn
LCompl :: IntTy -> PrimFn
LSHL :: IntTy -> PrimFn
LLSHR :: IntTy -> PrimFn
LASHR :: IntTy -> PrimFn
LEq :: ArithTy -> PrimFn
LLt :: IntTy -> PrimFn
LLe :: IntTy -> PrimFn
LGt :: IntTy -> PrimFn
LGe :: IntTy -> PrimFn
LSLt :: ArithTy -> PrimFn
LSLe :: ArithTy -> PrimFn
LSGt :: ArithTy -> PrimFn
LSGe :: ArithTy -> PrimFn
LSExt :: IntTy -> IntTy -> PrimFn
LZExt :: IntTy -> IntTy -> PrimFn
LTrunc :: IntTy -> IntTy -> PrimFn
LStrConcat :: PrimFn
LStrLt :: PrimFn
LStrEq :: PrimFn
LStrLen :: PrimFn
LIntFloat :: IntTy -> PrimFn
LFloatInt :: IntTy -> PrimFn
LIntStr :: IntTy -> PrimFn
LStrInt :: IntTy -> PrimFn
LFloatStr :: PrimFn
LStrFloat :: PrimFn
LChInt :: IntTy -> PrimFn
LIntCh :: IntTy -> PrimFn
LBitCast :: ArithTy -> ArithTy -> PrimFn
LFExp :: PrimFn
LFLog :: PrimFn
LFSin :: PrimFn
LFCos :: PrimFn
LFTan :: PrimFn
LFASin :: PrimFn
LFACos :: PrimFn
LFATan :: PrimFn
LFATan2 :: PrimFn
LFSqrt :: PrimFn
LFFloor :: PrimFn
LFCeil :: PrimFn
LFNegate :: PrimFn
LStrHead :: PrimFn
LStrTail :: PrimFn
LStrCons :: PrimFn
LStrIndex :: PrimFn
LStrRev :: PrimFn
LStrSubstr :: PrimFn
LReadStr :: PrimFn
LWriteStr :: PrimFn
LSystemInfo :: PrimFn
LFork :: PrimFn
LPar :: PrimFn
LExternal :: Name -> PrimFn
LCrash :: PrimFn
LNoOp :: PrimFn
data FCallType
FStatic :: FCallType
FObject :: FCallType
FConstructor :: FCallType
data FType
FArith :: ArithTy -> FType
FFunction :: FType
FFunctionIO :: FType
FString :: FType
FUnit :: FType
FPtr :: FType
FManagedPtr :: FType
FCData :: FType
FAny :: FType
data LAlt' e
LConCase :: Int -> Name -> [Name] -> e -> LAlt' e
LConstCase :: Const -> e -> LAlt' e
LDefaultCase :: e -> LAlt' e
type LAlt = LAlt' LExp
data LDecl
LFun :: [LOpt] -> Name -> [Name] -> LExp -> LDecl
LConstructor :: Name -> Int -> Int -> LDecl
type LDefs = Ctxt LDecl
data LOpt
Inline :: LOpt
NoInline :: LOpt
addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])
data LiftState
LS :: Maybe Name -> Int -> [(Name, LDecl)] -> Map ([Name], LExp) Name -> LiftState
setBaseName :: Name -> State LiftState ()
lname :: Name -> Int -> Name
getNextName :: State LiftState Name
renameArgs :: [Name] -> LExp -> ([Name], LExp)
addFn :: Name -> LDecl -> State LiftState ()
makeFn :: [Name] -> LExp -> State LiftState Name
liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]
liftDef :: (Name, LDecl) -> State LiftState ()
lift :: [Name] -> LExp -> State LiftState LExp
allocUnique :: LDefs -> (Name, LDecl) -> (Name, LDecl)
usedArg :: (Foldable t, Eq a) => t a -> a -> [a]
usedIn :: [Name] -> LExp -> [Name]
lsubst :: Name -> LExp -> LExp -> LExp
rename :: [(Name, Name)] -> LExp -> LExp
occName :: Name -> LExp -> Int
instance GHC.Classes.Ord IRTS.Lang.LDecl
instance GHC.Classes.Eq IRTS.Lang.LDecl
instance GHC.Show.Show IRTS.Lang.LDecl
instance GHC.Classes.Ord IRTS.Lang.LOpt
instance GHC.Classes.Eq IRTS.Lang.LOpt
instance GHC.Show.Show IRTS.Lang.LOpt
instance GHC.Classes.Ord IRTS.Lang.LExp
instance GHC.Classes.Eq IRTS.Lang.LExp
instance Data.Data.Data e => Data.Data.Data (IRTS.Lang.LAlt' e)
instance GHC.Base.Functor IRTS.Lang.LAlt'
instance GHC.Classes.Ord e => GHC.Classes.Ord (IRTS.Lang.LAlt' e)
instance GHC.Classes.Eq e => GHC.Classes.Eq (IRTS.Lang.LAlt' e)
instance GHC.Show.Show e => GHC.Show.Show (IRTS.Lang.LAlt' e)
instance GHC.Classes.Ord IRTS.Lang.FType
instance GHC.Classes.Eq IRTS.Lang.FType
instance GHC.Show.Show IRTS.Lang.FType
instance GHC.Classes.Ord IRTS.Lang.FCallType
instance GHC.Classes.Eq IRTS.Lang.FCallType
instance GHC.Show.Show IRTS.Lang.FCallType
instance GHC.Generics.Generic IRTS.Lang.PrimFn
instance GHC.Classes.Ord IRTS.Lang.PrimFn
instance GHC.Classes.Eq IRTS.Lang.PrimFn
instance GHC.Show.Show IRTS.Lang.PrimFn
instance GHC.Classes.Ord IRTS.Lang.ExportIFace
instance GHC.Classes.Eq IRTS.Lang.ExportIFace
instance GHC.Show.Show IRTS.Lang.ExportIFace
instance GHC.Classes.Ord IRTS.Lang.Export
instance GHC.Classes.Eq IRTS.Lang.Export
instance GHC.Show.Show IRTS.Lang.Export
instance GHC.Classes.Ord IRTS.Lang.FDesc
instance GHC.Classes.Eq IRTS.Lang.FDesc
instance GHC.Show.Show IRTS.Lang.FDesc
instance GHC.Classes.Eq IRTS.Lang.LVar
instance GHC.Show.Show IRTS.Lang.LVar
instance GHC.Classes.Eq IRTS.Lang.Endianness
instance GHC.Show.Show IRTS.Lang.Endianness
instance GHC.Show.Show IRTS.Lang.LExp


module Idris.Primitives
primitives :: [Prim]
data Prim
Prim :: Name -> Type -> Int -> ([Const] -> Maybe Const) -> (Int, PrimFn) -> Totality -> Prim
[p_name] :: Prim -> Name
[p_type] :: Prim -> Type
[p_arity] :: Prim -> Int
[p_def] :: Prim -> [Const] -> Maybe Const
[p_lexp] :: Prim -> (Int, PrimFn)
[p_total] :: Prim -> Totality


module IRTS.LangOpts
inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]


module IRTS.JavaScript.Specialize
type SCtor = [JsExpr] -> JsExpr
type STest = JsExpr -> JsExpr
type SProj = JsExpr -> Int -> JsExpr
specialCased :: Name -> Maybe (SCtor, STest, SProj)
specialCall :: Name -> Maybe SSig
qualifyN :: String -> String -> Name


module IRTS.JavaScript.PrimOp
type PrimF = [JsExpr] -> JsExpr
type PrimDec = (Bool, JsPrimTy, PrimF)
data JsPrimTy
PTBool :: JsPrimTy
PTAny :: JsPrimTy
primDB :: Map PrimFn PrimDec
jsPrimCoerce :: JsPrimTy -> JsPrimTy -> JsExpr -> JsExpr
instance GHC.Classes.Ord IRTS.JavaScript.PrimOp.JsPrimTy
instance GHC.Classes.Eq IRTS.JavaScript.PrimOp.JsPrimTy


module IRTS.JavaScript.Name
jsName :: Name -> Text
jsNameGenerated :: Int -> Text
data Partial
Partial :: Name -> Int -> Int -> Partial
jsNamePartial :: Partial -> Text
jsTailCallOptimName :: Text -> Text
data HiddenClass
HiddenClass :: Name -> Int -> Int -> HiddenClass
jsNameHiddenClass :: HiddenClass -> Text
dataPartName :: Int -> Text
instance GHC.Classes.Ord IRTS.JavaScript.Name.HiddenClass
instance GHC.Classes.Eq IRTS.JavaScript.Name.HiddenClass
instance GHC.Classes.Ord IRTS.JavaScript.Name.Partial
instance GHC.Classes.Eq IRTS.JavaScript.Name.Partial


module IRTS.JavaScript.LangTransforms
removeDeadCode :: Map Name LDecl -> [Name] -> Map Name LDecl
globlToCon :: Map Name LDecl -> Map Name LDecl
instance Data.Data.Data IRTS.Lang.FDesc
instance Data.Data.Data IRTS.Lang.LVar
instance Data.Data.Data IRTS.Lang.PrimFn
instance Data.Data.Data Idris.Core.CaseTree.CaseType
instance Data.Data.Data IRTS.Lang.LExp
instance Data.Data.Data IRTS.Lang.LDecl
instance Data.Data.Data IRTS.Lang.LOpt


-- | To defunctionalise:
--   
--   <ol>
--   <li>Create a data constructor for each function</li>
--   <li>Create a data constructor for each underapplication of a
--   function</li>
--   <li>Convert underapplications to their corresponding constructors</li>
--   <li>Create an EVAL function which calls the appropriate function for
--   data constructors created as part of step 1</li>
--   <li>Create an APPLY function which adds an argument to each
--   underapplication (or calls APPLY again for an exact application)</li>
--   <li>Wrap overapplications in chains of APPLY</li>
--   <li>Wrap unknown applications (i.e. applications of local variables)
--   in chains of APPLY</li>
--   <li>Add explicit EVAL to case, primitives, and foreign calls</li>
--   </ol>
module IRTS.Defunctionalise
data EvalApply a
EvalCase :: (Name -> a) -> EvalApply a
ApplyCase :: a -> EvalApply a
Apply2Case :: a -> EvalApply a
type DDefs = Ctxt DDecl
data DDecl
DFun :: Name -> [Name] -> DExp -> DDecl
DConstructor :: Name -> Int -> Int -> DDecl
data DAlt
DConCase :: Int -> Name -> [Name] -> DExp -> DAlt
DConstCase :: Const -> DExp -> DAlt
DDefaultCase :: DExp -> DAlt
data DExp
DV :: Name -> DExp
DApp :: Bool -> Name -> [DExp] -> DExp
DLet :: Name -> DExp -> DExp -> DExp
DUpdate :: Name -> DExp -> DExp
DProj :: DExp -> Int -> DExp
DC :: Maybe Name -> Int -> Name -> [DExp] -> DExp
DCase :: CaseType -> DExp -> [DAlt] -> DExp
DChkCase :: DExp -> [DAlt] -> DExp
DConst :: Const -> DExp
DForeign :: FDesc -> FDesc -> [(FDesc, DExp)] -> DExp
DOp :: PrimFn -> [DExp] -> DExp
DNothing :: DExp
DError :: String -> DExp
defunctionalise :: Int -> LDefs -> DDefs
getFn :: [(Name, LDecl)] -> [(Name, Int)]
addApps :: LDefs -> (Name, LDecl) -> State ([Name], [(Name, Int)]) (Name, DDecl)
eEVAL :: DExp -> DExp
toCons :: [Name] -> (Name, Int) -> [(Name, Int, EvalApply DAlt)]
toConsA :: [(Name, Int)] -> (Name, Int) -> [(Name, Int, EvalApply DAlt)]
mkApplyCase :: Name -> Int -> Int -> [(Name, Int, EvalApply DAlt)]
mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
mkApply2 :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
declare :: Int -> [(Name, Int, EvalApply DAlt)] -> [(Name, DDecl)]
genArgs :: Int -> [Name]
mkFnCon :: Show a => a -> Name
mkUnderCon :: Name -> Int -> Name

-- | Divide up a large case expression so that each has a maximum of
--   <a>max</a> branches
mkBigCase :: () => p -> Int -> DExp -> [DAlt] -> DExp
groupsOf :: Int -> [DAlt] -> [[DAlt]]
dumpDefuns :: DDefs -> String
instance GHC.Classes.Eq IRTS.Defunctionalise.DDecl
instance GHC.Show.Show IRTS.Defunctionalise.DDecl
instance GHC.Classes.Eq IRTS.Defunctionalise.DExp
instance GHC.Classes.Eq IRTS.Defunctionalise.DAlt
instance GHC.Show.Show IRTS.Defunctionalise.DAlt
instance GHC.Show.Show IRTS.Defunctionalise.DExp


module IRTS.Simplified
simplifyDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]
data SDecl
SFun :: Name -> [Name] -> Int -> SExp -> SDecl
data SExp
SV :: LVar -> SExp
SApp :: Bool -> Name -> [LVar] -> SExp
SLet :: LVar -> SExp -> SExp -> SExp
SUpdate :: LVar -> SExp -> SExp
SCon :: Maybe LVar -> Int -> Name -> [LVar] -> SExp
SCase :: CaseType -> LVar -> [SAlt] -> SExp
SChkCase :: LVar -> [SAlt] -> SExp
SProj :: LVar -> Int -> SExp
SConst :: Const -> SExp
SForeign :: FDesc -> FDesc -> [(FDesc, LVar)] -> SExp
SOp :: PrimFn -> [LVar] -> SExp
SNothing :: SExp
SError :: String -> SExp
data SAlt
SConCase :: Int -> Int -> Name -> [Name] -> SExp -> SAlt
SConstCase :: Const -> SExp -> SAlt
SDefaultCase :: SExp -> SAlt
instance GHC.Show.Show IRTS.Simplified.SDecl
instance GHC.Show.Show IRTS.Simplified.SExp
instance GHC.Show.Show IRTS.Simplified.SAlt


module IRTS.Inliner
inline :: DDefs -> DDefs
inl :: DDefs -> (Name, DDecl) -> (Name, DDecl)
evalD :: () => p -> a -> Maybe a


module IRTS.CodegenCommon
data DbgLevel
NONE :: DbgLevel
DEBUG :: DbgLevel
TRACE :: DbgLevel
data OutputType
Raw :: OutputType
Object :: OutputType
Executable :: OutputType

-- | Everything which might be needed in a code generator.
--   
--   A CG can choose which level of Decls to generate code from
--   (simplified, defunctionalised or merely lambda lifted) and has access
--   to the list of object files, libraries, etc.
data CodegenInfo
CodegenInfo :: String -> OutputType -> String -> String -> [FilePath] -> [FilePath] -> [String] -> [String] -> [String] -> DbgLevel -> [(Name, SDecl)] -> [(Name, DDecl)] -> [(Name, LDecl)] -> Bool -> [ExportIFace] -> [(Name, TTDecl)] -> CodegenInfo
[outputFile] :: CodegenInfo -> String
[outputType] :: CodegenInfo -> OutputType
[targetTriple] :: CodegenInfo -> String
[targetCPU] :: CodegenInfo -> String
[includes] :: CodegenInfo -> [FilePath]
[importDirs] :: CodegenInfo -> [FilePath]
[compileObjs] :: CodegenInfo -> [String]
[compileLibs] :: CodegenInfo -> [String]
[compilerFlags] :: CodegenInfo -> [String]
[debugLevel] :: CodegenInfo -> DbgLevel
[simpleDecls] :: CodegenInfo -> [(Name, SDecl)]
[defunDecls] :: CodegenInfo -> [(Name, DDecl)]
[liftDecls] :: CodegenInfo -> [(Name, LDecl)]
[interfaces] :: CodegenInfo -> Bool
[exportDecls] :: CodegenInfo -> [ExportIFace]
[ttDecls] :: CodegenInfo -> [(Name, TTDecl)]
type CodeGenerator = CodegenInfo -> IO ()
instance GHC.Generics.Generic IRTS.CodegenCommon.OutputType
instance GHC.Show.Show IRTS.CodegenCommon.OutputType
instance GHC.Classes.Eq IRTS.CodegenCommon.OutputType
instance GHC.Classes.Eq IRTS.CodegenCommon.DbgLevel


module Idris.Options
data Codegen
Via :: IRFormat -> String -> Codegen
Bytecode :: Codegen

-- | How wide is the console?
data ConsoleWidth

-- | Have pretty-printer assume that lines should not be broken
InfinitelyWide :: ConsoleWidth

-- | Manually specified - must be positive
ColsWide :: Int -> ConsoleWidth

-- | Attempt to determine width, or 80 otherwise
AutomaticWidth :: ConsoleWidth
data HowMuchDocs
FullDocs :: HowMuchDocs
OverviewDocs :: HowMuchDocs
data IRFormat
IBCFormat :: IRFormat
JSONFormat :: IRFormat
data LanguageExt
TypeProviders :: LanguageExt
ErrorReflection :: LanguageExt
UniquenessTypes :: LanguageExt
DSLNotation :: LanguageExt
ElabReflection :: LanguageExt
FCReflection :: LanguageExt
LinearTypes :: LanguageExt

-- | Recognised logging categories for the Idris compiler.
--   
--   @TODO add in sub categories.
data LogCat
IParse :: LogCat
IElab :: LogCat
ICodeGen :: LogCat
IErasure :: LogCat
ICoverage :: LogCat
IIBC :: LogCat
data Opt
Filename :: String -> Opt
Quiet :: Opt
NoBanner :: Opt
ColourREPL :: Bool -> Opt
Idemode :: Opt
IdemodeSocket :: Opt
IndentWith :: Int -> Opt
IndentClause :: Int -> Opt
ShowAll :: Opt
ShowLibs :: Opt
ShowLibDir :: Opt
ShowDocDir :: Opt
ShowIncs :: Opt
ShowPkgs :: Opt
ShowLoggingCats :: Opt
NoBasePkgs :: Opt
NoPrelude :: Opt
NoBuiltins :: Opt
NoREPL :: Opt
OLogging :: Int -> Opt
OLogCats :: [LogCat] -> Opt
Output :: String -> Opt
Interface :: Opt
TypeCase :: Opt
TypeInType :: Opt
DefaultTotal :: Opt
DefaultPartial :: Opt
WarnPartial :: Opt
WarnReach :: Opt
AuditIPkg :: Opt
EvalTypes :: Opt
NoCoverage :: Opt
ErrContext :: Opt
ShowImpl :: Opt
Verbose :: Int -> Opt

-- | REPL TCP port
Port :: REPLPort -> Opt
IBCSubDir :: String -> Opt
ImportDir :: String -> Opt
SourceDir :: String -> Opt
PkgBuild :: String -> Opt
PkgInstall :: String -> Opt
PkgClean :: String -> Opt
PkgCheck :: String -> Opt
PkgREPL :: String -> Opt
PkgDocBuild :: String -> Opt
PkgDocInstall :: String -> Opt
PkgTest :: String -> Opt
PkgIndex :: FilePath -> Opt
WarnOnly :: Opt
Pkg :: String -> Opt
BCAsm :: String -> Opt
DumpDefun :: String -> Opt
DumpCases :: String -> Opt
UseCodegen :: Codegen -> Opt
CodegenArgs :: String -> Opt
OutputTy :: OutputType -> Opt
Extension :: LanguageExt -> Opt
InterpretScript :: String -> Opt
EvalExpr :: String -> Opt
TargetTriple :: String -> Opt
TargetCPU :: String -> Opt
OptLevel :: Int -> Opt
AddOpt :: Optimisation -> Opt
RemoveOpt :: Optimisation -> Opt
Client :: String -> Opt
ShowOrigErr :: Opt

-- | Automatically adjust terminal width
AutoWidth :: Opt

-- | Automatically issue "solve" tactic in old-style interactive prover
AutoSolve :: Opt
UseConsoleWidth :: ConsoleWidth -> Opt
DumpHighlights :: Opt
DesugarNats :: Opt

-- | Don't show deprecation warnings for old-style tactics
NoOldTacticDeprecationWarnings :: Opt

-- | Allow pattern variables to be capitalized
AllowCapitalizedPatternVariables :: Opt
data Optimisation
PETransform :: Optimisation

-- | partial eval and associated transforms
GeneralisedNatHack :: Optimisation
data OutputFmt
HTMLOutput :: OutputFmt
LaTeXOutput :: OutputFmt
data REPLPort
DontListen :: REPLPort
ListenPort :: PortNumber -> REPLPort
codegenCats :: [LogCat]
elabCats :: [LogCat]
getBC :: Opt -> Maybe String
getClient :: Opt -> Maybe String
getCodegen :: Opt -> Maybe Codegen
getCodegenArgs :: Opt -> Maybe String
getColour :: Opt -> Maybe Bool
getConsoleWidth :: Opt -> Maybe ConsoleWidth
getEvalExpr :: Opt -> Maybe String
getExecScript :: Opt -> Maybe String
getFile :: Opt -> Maybe String
getIBCSubDir :: Opt -> Maybe String
getImportDir :: Opt -> Maybe String
getLanguageExt :: Opt -> Maybe LanguageExt
getOptLevel :: Opt -> Maybe Int
getOptimisation :: Opt -> Maybe (Bool, Optimisation)
getOutput :: Opt -> Maybe String
getOutputTy :: Opt -> Maybe OutputType
getPkg :: Opt -> Maybe (Bool, String)
getPkgCheck :: Opt -> Maybe String
getPkgClean :: Opt -> Maybe String
getPkgDir :: Opt -> Maybe String
getPkgIndex :: Opt -> Maybe FilePath

-- | Returns None if given an Opt which is not PkgMkDoc Otherwise returns
--   Just x, where x is the contents of PkgMkDoc
getPkgMkDoc :: Opt -> Maybe (Bool, String)
getPkgREPL :: Opt -> Maybe String
getPkgTest :: Opt -> Maybe String
getPort :: [Opt] -> Maybe REPLPort
getSourceDir :: Opt -> Maybe String
loggingCatsStr :: String
opt :: (Opt -> Maybe a) -> [Opt] -> [a]
parserCats :: [LogCat]
strLogCat :: LogCat -> String
instance GHC.Generics.Generic Idris.Options.Opt
instance GHC.Classes.Eq Idris.Options.Opt
instance GHC.Show.Show Idris.Options.Opt
instance GHC.Generics.Generic Idris.Options.LogCat
instance GHC.Classes.Ord Idris.Options.LogCat
instance GHC.Classes.Eq Idris.Options.LogCat
instance GHC.Show.Show Idris.Options.LogCat
instance GHC.Generics.Generic Idris.Options.Optimisation
instance GHC.Classes.Eq Idris.Options.Optimisation
instance GHC.Show.Show Idris.Options.Optimisation
instance GHC.Generics.Generic Idris.Options.ConsoleWidth
instance GHC.Classes.Eq Idris.Options.ConsoleWidth
instance GHC.Show.Show Idris.Options.ConsoleWidth
instance GHC.Generics.Generic Idris.Options.Codegen
instance GHC.Classes.Eq Idris.Options.Codegen
instance GHC.Show.Show Idris.Options.Codegen
instance GHC.Generics.Generic Idris.Options.IRFormat
instance GHC.Classes.Eq Idris.Options.IRFormat
instance GHC.Show.Show Idris.Options.IRFormat
instance GHC.Generics.Generic Idris.Options.LanguageExt
instance GHC.Classes.Ord Idris.Options.LanguageExt
instance GHC.Read.Read Idris.Options.LanguageExt
instance GHC.Classes.Eq Idris.Options.LanguageExt
instance GHC.Show.Show Idris.Options.LanguageExt
instance GHC.Show.Show Idris.Options.REPLPort
instance GHC.Generics.Generic Idris.Options.REPLPort
instance GHC.Classes.Eq Idris.Options.REPLPort


-- | BASE: Current stack frame's base TOP: Top of stack OLDBASE: Passed in
--   to each function, the previous stack frame's base
--   
--   L i refers to the stack item at BASE + i T i refers to the stack item
--   at TOP + i
--   
--   RVal is a register in which computed values (essentially, what a
--   function returns) are stored.
module IRTS.Bytecode
data Reg
RVal :: Reg
L :: Int -> Reg
T :: Int -> Reg
Tmp :: Reg
data BC

-- | reg1 = reg2
ASSIGN :: Reg -> Reg -> BC

-- | reg = const
ASSIGNCONST :: Reg -> Const -> BC

-- | reg1 = reg2 (same as assign, it seems)
UPDATE :: Reg -> Reg -> BC

-- | reg = constructor, where constructor consists of a tag and values from
--   registers, e.g. (cons tag args) the 'Maybe Reg', if set, is a register
--   which can be overwritten (i.e. safe for mutable update), though this
--   can be ignored
MKCON :: Reg -> Maybe Reg -> Int -> [Reg] -> BC

-- | Matching on value of reg: usually (but not always) there are
--   constructors, hence <a>Int</a> for patterns (that's a tag on which we
--   should match), and the following [BC] is just a list of instructions
--   for the corresponding case. The last argument is for default case.
--   When it's not necessary a constructor in the reg, the Bool should be
--   False, indicating that it's not safe to work with that as with a
--   constructor, so a check should be added. If it's not a constructor,
--   default case should be used.
CASE :: Bool -> Reg -> [(Int, [BC])] -> Maybe [BC] -> BC

-- | get a value from register, which should be a constructor, and put its
--   arguments into the stack, starting from (base + int1) and onwards;
--   second Int provides arity
PROJECT :: Reg -> Int -> Int -> BC

-- | probably not used
PROJECTINTO :: Reg -> Reg -> Int -> BC

-- | same as CASE, but there's an exact value (not constructor) in reg
CONSTCASE :: Reg -> [(Const, [BC])] -> Maybe [BC] -> BC

-- | just call a function, passing MYOLDBASE (see below) to it
CALL :: Name -> BC

-- | same, perhaps exists just for TCO
TAILCALL :: Name -> BC

-- | set reg to (apply string args),
FOREIGNCALL :: Reg -> FDesc -> FDesc -> [(FDesc, Reg)] -> BC

-- | move this number of elements from TOP to BASE
SLIDE :: Int -> BC

-- | set BASE = OLDBASE
REBASE :: BC

-- | reserve n more stack items (i.e. check there's space, grow if
--   necessary)
RESERVE :: Int -> BC

-- | move the top of stack up
ADDTOP :: Int -> BC

-- | set TOP = BASE + n
TOPBASE :: Int -> BC

-- | set BASE = TOP + n
BASETOP :: Int -> BC

-- | set MYOLDBASE = BASE, where MYOLDBASE is a function-local variable,
--   set to OLDBASE by default, and passed on function call to called
--   functions as their OLDBASE
STOREOLD :: BC

-- | reg = apply primitive_function args
OP :: Reg -> PrimFn -> [Reg] -> BC

-- | clear reg
NULL :: Reg -> BC

-- | throw an error
ERROR :: String -> BC
toBC :: (Name, SDecl) -> (Name, [BC])
clean :: Bool -> [BC]
bc :: Reg -> SExp -> Bool -> [BC]
isConst :: [SAlt] -> Bool
moveReg :: Int -> [LVar] -> [BC]
assign :: Reg -> Reg -> [BC]
conCase :: Bool -> Reg -> Reg -> [SAlt] -> Bool -> [BC]
constCase :: Reg -> Reg -> [SAlt] -> Bool -> [BC]
caseAlt :: Reg -> Reg -> Bool -> SAlt -> Maybe (Int, [BC])
constAlt :: () => p -> Reg -> Bool -> SAlt -> Maybe (Const, [BC])
defaultAlt :: Reg -> [SAlt] -> Bool -> Maybe [BC]
instance GHC.Show.Show IRTS.Bytecode.BC
instance GHC.Classes.Eq IRTS.Bytecode.Reg
instance GHC.Show.Show IRTS.Bytecode.Reg


module IRTS.Portable
writePortable :: Handle -> CodegenInfo -> IO ()
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Portable.CodegenFile
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.CodegenCommon.CodegenInfo
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.TT.Name
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.ExportIFace
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.FDesc
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.Export
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.LDecl
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.LOpt
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.LExp
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.LVar
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.CaseTree.CaseType
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.LAlt
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.TT.Const
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.TT.ArithTy
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.TT.IntTy
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Lang.PrimFn
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Defunctionalise.DDecl
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Defunctionalise.DExp
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Defunctionalise.DAlt
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Simplified.SDecl
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Simplified.SExp
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Simplified.SAlt
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Bytecode.BC
instance Data.Aeson.Types.ToJSON.ToJSON IRTS.Bytecode.Reg
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.TT.RigCount
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.Evaluate.Totality
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.Evaluate.MetaInformation
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.Evaluate.Def
instance Data.Aeson.Types.ToJSON.ToJSON t => Data.Aeson.Types.ToJSON.ToJSON (Idris.Core.TT.TT t)
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.TT.UExp
instance Data.Aeson.Types.ToJSON.ToJSON t => Data.Aeson.Types.ToJSON.ToJSON (Idris.Core.TT.AppStatus t)
instance Data.Aeson.Types.ToJSON.ToJSON t => Data.Aeson.Types.ToJSON.ToJSON (Idris.Core.TT.Binder t)
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.TT.ImplicitInfo
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.TT.NameType
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.Evaluate.CaseDefs
instance Data.Aeson.Types.ToJSON.ToJSON t => Data.Aeson.Types.ToJSON.ToJSON (Idris.Core.CaseTree.SC' t)
instance Data.Aeson.Types.ToJSON.ToJSON t => Data.Aeson.Types.ToJSON.ToJSON (Idris.Core.CaseTree.CaseAlt' t)
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.Evaluate.CaseInfo
instance Data.Aeson.Types.ToJSON.ToJSON Idris.Core.Evaluate.Accessibility


module IRTS.DumpBC
interMap :: [a] -> [b] -> (a -> [b]) -> [b]
indent :: Int -> String
serializeReg :: Reg -> String
serializeCase :: Show a => Int -> (a, [BC]) -> String
serializeDefault :: Int -> [BC] -> String
serializeBC :: Int -> BC -> String
serialize :: [(Name, [BC])] -> String
dumpBC :: [(Name, SDecl)] -> String -> IO ()


-- | Implements a proof state, some primitive tactics for manipulating
--   proofs, and some high level commands for introducing new theorems,
--   evaluation/checking inside the proof system, etc.
module Idris.Core.ProofState
data ProofState
PS :: Name -> [Name] -> [Name] -> Int -> Int -> ProofTerm -> Type -> [Name] -> (Name, [(Name, Term)]) -> [(Name, Term)] -> [(Name, [Name])] -> Maybe (Name, Term) -> Fails -> [Name] -> [Name] -> [Name] -> [(Name, ([FailContext], [Name]))] -> [Name] -> Maybe ProofState -> Context -> Ctxt TypeInfo -> String -> Bool -> Bool -> [Name] -> [FailContext] -> String -> ProofState
[thname] :: ProofState -> Name

-- | holes still to be solved
[holes] :: ProofState -> [Name]

-- | used names, don't use again
[usedns] :: ProofState -> [Name]

-- | name supply, for locally unique names
[nextname] :: ProofState -> Int

-- | a mirror of the global name supply, for generating things like type
--   tags in reflection
[global_nextname] :: ProofState -> Int

-- | current proof term
[pterm] :: ProofState -> ProofTerm

-- | original goal
[ptype] :: ProofState -> Type

-- | explicitly given by programmer, leave it
[dontunify] :: ProofState -> [Name]
[unified] :: ProofState -> (Name, [(Name, Term)])
[notunified] :: ProofState -> [(Name, Term)]

-- | dot pattern holes + environment either hole or something in env must
--   turn up in the <a>notunified</a> list during elaboration
[dotted] :: ProofState -> [(Name, [Name])]
[solved] :: ProofState -> Maybe (Name, Term)
[problems] :: ProofState -> Fails
[injective] :: ProofState -> [Name]

-- | names we'll need to define
[deferred] :: ProofState -> [Name]

-- | implementation arguments (for interfaces)
[implementations] :: ProofState -> [Name]

-- | unsolved <tt>auto</tt> implicits with their holes
[autos] :: ProofState -> [(Name, ([FailContext], [Name]))]

-- | Local names okay to use in proof search
[psnames] :: ProofState -> [Name]

-- | for undo
[previous] :: ProofState -> Maybe ProofState
[context] :: ProofState -> Context
[datatypes] :: ProofState -> Ctxt TypeInfo
[plog] :: ProofState -> String
[unifylog] :: ProofState -> Bool
[done] :: ProofState -> Bool
[recents] :: ProofState -> [Name]
[while_elaborating] :: ProofState -> [FailContext]
[constraint_ns] :: ProofState -> String
newProof :: Name -> String -> Context -> Ctxt TypeInfo -> Int -> Type -> ProofState
envAtFocus :: ProofState -> TC Env
goalAtFocus :: ProofState -> TC (Binder Type)
data Tactic
Attack :: Tactic
Claim :: Name -> Raw -> Tactic
ClaimFn :: Name -> Name -> Raw -> Tactic
Reorder :: Name -> Tactic
Exact :: Raw -> Tactic
Fill :: Raw -> Tactic
MatchFill :: Raw -> Tactic
PrepFill :: Name -> [Name] -> Tactic
CompleteFill :: Tactic
Regret :: Tactic
Solve :: Tactic
StartUnify :: Name -> Tactic
EndUnify :: Tactic
UnifyAll :: Tactic
Compute :: Tactic
ComputeLet :: Name -> Tactic
Simplify :: Tactic
WHNF_Compute :: Tactic
WHNF_ComputeArgs :: Tactic
EvalIn :: Raw -> Tactic
CheckIn :: Raw -> Tactic
Intro :: Maybe Name -> Tactic
IntroTy :: Raw -> Maybe Name -> Tactic
Forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Tactic
LetBind :: Name -> RigCount -> Raw -> Raw -> Tactic
ExpandLet :: Name -> Term -> Tactic
Rewrite :: Raw -> Tactic
Equiv :: Raw -> Tactic
PatVar :: Name -> Tactic
PatBind :: Name -> RigCount -> Tactic
Focus :: Name -> Tactic
Defer :: [Name] -> [Name] -> Name -> Tactic
DeferType :: Name -> Raw -> [Name] -> Tactic
Implementation :: Name -> Tactic
AutoArg :: Name -> Tactic
SetInjective :: Name -> Tactic
MoveLast :: Name -> Tactic
MatchProblems :: Bool -> Tactic
UnifyProblems :: Tactic
UnifyGoal :: Raw -> Tactic
UnifyTerms :: Raw -> Raw -> Tactic
ProofState :: Tactic
Undo :: Tactic
QED :: Tactic
data Goal
GD :: Env -> Binder Term -> Goal
[premises] :: Goal -> Env
[goalType] :: Goal -> Binder Term
processTactic :: Tactic -> ProofState -> TC (ProofState, String)
nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
doneElaboratingAppPS :: Name -> ProofState -> ProofState
doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
dropGiven :: (Eq a, Foldable t1, Foldable t2) => t1 a -> [(a, TT a)] -> t2 a -> [(a, TT a)]
keepGiven :: (Eq a, Foldable t1, Foldable t2) => t1 a -> [(a, TT a)] -> t2 a -> [(a, TT a)]
getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
instance GHC.Show.Show Idris.Core.ProofState.Tactic
instance GHC.Show.Show Idris.Core.ProofState.ProofState
instance Util.Pretty.Pretty Idris.Core.ProofState.ProofState Idris.Core.TT.OutputAnnotation


-- | This is our interface to proof construction, rather than ProofState,
--   because this gives us a language to build derived tactics out of the
--   primitives.
module Idris.Core.Elaborate
type Elab a = Elab' () a
type Elab' aux a = StateT (ElabState aux) TC a
data ElabState aux
ES :: (ProofState, aux) -> String -> Maybe (ElabState aux) -> ElabState aux
proof :: ElabState aux -> ProofState
proofFail :: Elab' aux a -> Elab' aux a
explicit :: Name -> Elab' aux ()
addPSname :: Name -> Elab' aux ()
getPSnames :: Elab' aux [Name]
saveState :: Elab' aux ()
loadState :: Elab' aux ()
getNameFrom :: Name -> Elab' aux Name
setNextName :: Elab' aux ()
initNextNameFrom :: [Name] -> Elab' aux ()

-- | Transform the error returned by an elaboration script, preserving
--   location information and proof search failure messages.
transformErr :: (Err -> Err) -> Elab' aux a -> Elab' aux a
errAt :: String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)
erun :: FC -> Elab' aux a -> Elab' aux a
runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
initElaborator :: Name -> String -> Context -> Ctxt TypeInfo -> Int -> Type -> ProofState
elaborate :: String -> Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

-- | Modify the auxiliary state
updateAux :: (aux -> aux) -> Elab' aux ()

-- | Get the auxiliary state
getAux :: Elab' aux aux

-- | Set whether to show the unifier log
unifyLog :: Bool -> Elab' aux ()
getUnifyLog :: Elab' aux Bool

-- | Process a tactic within the current elaborator state
processTactic' :: Tactic -> Elab' aux ()
updatePS :: (ProofState -> ProofState) -> Elab' aux ()
now_elaborating :: FC -> Name -> Name -> Elab' aux ()
done_elaborating_app :: Name -> Elab' aux ()
done_elaborating_arg :: Name -> Name -> Elab' aux ()
elaborating_app :: Elab' aux [(FC, Name, Name)]

-- | Get the global context
get_context :: Elab' aux Context

-- | Update the context. (should only be used for adding temporary
--   definitions or all sorts of stuff could go wrong)
set_context :: Context -> Elab' aux ()
get_datatypes :: Elab' aux (Ctxt TypeInfo)
set_datatypes :: Ctxt TypeInfo -> Elab' aux ()
get_global_nextname :: Elab' aux Int
set_global_nextname :: Int -> Elab' aux ()

-- | get the proof term
get_term :: Elab' aux Term

-- | modify the proof term
update_term :: (Term -> Term) -> Elab' aux ()

-- | get the local context at the currently in focus hole
get_env :: Elab' aux Env
get_inj :: Elab' aux [Name]
get_holes :: Elab' aux [Name]
get_usedns :: Elab' aux [Name]
get_probs :: Elab' aux Fails

-- | Return recently solved names (that is, the names solved since the last
--   call to get_recents)
get_recents :: Elab' aux [Name]

-- | get the current goal type
goal :: Elab' aux Type
is_guess :: Elab' aux Bool

-- | Get the guess at the current hole, if there is one
get_guess :: Elab' aux Term

-- | Typecheck locally
get_type :: Raw -> Elab' aux Type
get_type_val :: Raw -> Elab' aux (Term, Type)

-- | get holes we've deferred for later definition
get_deferred :: Elab' aux [Name]
checkInjective :: (Term, Term, Term) -> Elab' aux ()

-- | get implementation argument names
get_implementations :: Elab' aux [Name]

-- | get auto argument names
get_autos :: Elab' aux [(Name, ([FailContext], [Name]))]

-- | given a desired hole name, return a unique hole name
unique_hole :: Name -> Elab' aux Name
unique_hole' :: Bool -> Name -> Elab' aux Name
elog :: String -> Elab' aux ()
getLog :: Elab' aux String
attack :: Elab' aux ()
claim :: Name -> Raw -> Elab' aux ()
claimFn :: Name -> Name -> Raw -> Elab' aux ()
unifyGoal :: Raw -> Elab' aux ()
unifyTerms :: Raw -> Raw -> Elab' aux ()
exact :: Raw -> Elab' aux ()
fill :: Raw -> Elab' aux ()
match_fill :: Raw -> Elab' aux ()
prep_fill :: Name -> [Name] -> Elab' aux ()
complete_fill :: Elab' aux ()
solve :: Elab' aux ()
start_unify :: Name -> Elab' aux ()
end_unify :: Elab' aux ()
unify_all :: Elab' aux ()
regret :: Elab' aux ()
compute :: Elab' aux ()
computeLet :: Name -> Elab' aux ()
simplify :: Elab' aux ()
whnf_compute :: Elab' aux ()
whnf_compute_args :: Elab' aux ()
eval_in :: Raw -> Elab' aux ()
check_in :: Raw -> Elab' aux ()
intro :: Maybe Name -> Elab' aux ()
introTy :: Raw -> Maybe Name -> Elab' aux ()
forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
letbind :: Name -> RigCount -> Raw -> Raw -> Elab' aux ()
expandLet :: Name -> Term -> Elab' aux ()
rewrite :: Raw -> Elab' aux ()
equiv :: Raw -> Elab' aux ()

-- | Turn the current hole into a pattern variable with the provided name,
--   made unique if not the same as the head of the hole queue
patvar :: Name -> Elab' aux ()

-- | Turn the current hole into a pattern variable with the provided name,
--   but don't make MNs unique.
patvar' :: Name -> Elab' aux ()
patbind :: Name -> RigCount -> Elab' aux ()
focus :: Name -> Elab' aux ()
movelast :: Name -> Elab' aux ()
dotterm :: Elab' aux ()
get_dotterm :: Elab' aux [(Name, [Name])]

-- | Set the zipper in the proof state to point at the current sub term
--   (This currently happens automatically, so this will have no effect...)
zipHere :: Elab' aux ()
matchProblems :: Bool -> Elab' aux ()
unifyProblems :: Elab' aux ()
defer :: [Name] -> [Name] -> Name -> Elab' aux Name
deferType :: Name -> Raw -> [Name] -> Elab' aux ()
implementationArg :: Name -> Elab' aux ()
autoArg :: Name -> Elab' aux ()
setinj :: Name -> Elab' aux ()
proofstate :: Elab' aux ()
reorder_claims :: Name -> Elab' aux ()
qed :: Elab' aux Term
undo :: Elab' aux ()

-- | Prepare to apply a function by creating holes to be filled by the
--   arguments
prepare_apply :: Raw -> [Bool] -> Elab' aux [(Name, Name)]

-- | Apply an operator, solving some arguments by unification or matching.
apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

-- | Apply an operator, solving some arguments by unification or matching.
match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
checkPiGoal :: Name -> Elab' aux ()
simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
arg :: Name -> RigCount -> Maybe ImplicitInfo -> Name -> Elab' aux ()
no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()
try :: Elab' aux a -> Elab' aux a -> Elab' aux a
handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a
try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a
tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
tryAll :: [(Elab' aux a, Name)] -> Elab' aux a
tryAll' :: Bool -> [(Elab' aux a, Name)] -> Elab' aux a
prunStateT :: Int -> Bool -> [a] -> Maybe [b] -> StateT (ElabState t) TC t1 -> ElabState t -> TC ((t1, Int, Fails), ElabState t)
debugElaborator :: [ErrorReportPart] -> Elab' aux a
qshow :: Fails -> String
dumpprobs :: Show a1 => [(a2, b, c, a1)] -> [Char]
instance GHC.Show.Show aux => GHC.Show.Show (Idris.Core.Elaborate.ElabState aux)


module Idris.AbsSyntaxTree
data ElabWhat
ETypes :: ElabWhat
EDefns :: ElabWhat
EAll :: ElabWhat

-- | Data to pass to recursively called elaborators; e.g. for where blocks,
--   paramaterised declarations, etc.
--   
--   rec_elabDecl is used to pass the top level elaborator into other
--   elaborators, so that we can have mutually recursive elaborators in
--   separate modules without having to muck about with cyclic modules.
data ElabInfo
EInfo :: [(Name, PTerm)] -> Ctxt [Name] -> (Name -> Name) -> [String] -> Maybe FC -> String -> Int -> [Name] -> (PTerm -> PTerm) -> (ElabWhat -> ElabInfo -> PDecl -> Idris ()) -> ElabInfo
[params] :: ElabInfo -> [(Name, PTerm)]

-- | names in the block, and their params
[inblock] :: ElabInfo -> Ctxt [Name]
[liftname] :: ElabInfo -> Name -> Name
[namespace] :: ElabInfo -> [String]
[elabFC] :: ElabInfo -> Maybe FC

-- | filename for adding to constraint variables
[constraintNS] :: ElabInfo -> String
[pe_depth] :: ElabInfo -> Int

-- | types which shouldn't be made arguments to case | We may, recursively,
--   collect transformations to do on the rhs, e.g. rewriting recursive
--   calls to functions defined by <tt>with</tt>
[noCaseLift] :: ElabInfo -> [Name]
[rhs_trans] :: ElabInfo -> PTerm -> PTerm
[rec_elabDecl] :: ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
toplevel :: ElabInfo
toplevelWith :: String -> ElabInfo
eInfoNames :: ElabInfo -> [Name]
data IOption
IOption :: Int -> [LogCat] -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Int -> Bool -> Bool -> Codegen -> OutputType -> FilePath -> [FilePath] -> [FilePath] -> String -> String -> [Opt] -> Bool -> Bool -> [FilePath] -> [Optimisation] -> Maybe Int -> Bool -> Bool -> Bool -> IOption
[opt_logLevel] :: IOption -> Int

-- | List of logging categories.
[opt_logcats] :: IOption -> [LogCat]
[opt_typecase] :: IOption -> Bool
[opt_typeintype] :: IOption -> Bool
[opt_coverage] :: IOption -> Bool

-- | show implicits
[opt_showimp] :: IOption -> Bool
[opt_errContext] :: IOption -> Bool
[opt_repl] :: IOption -> Bool
[opt_verbose] :: IOption -> Int
[opt_nobanner] :: IOption -> Bool
[opt_quiet] :: IOption -> Bool
[opt_codegen] :: IOption -> Codegen
[opt_outputTy] :: IOption -> OutputType
[opt_ibcsubdir] :: IOption -> FilePath
[opt_importdirs] :: IOption -> [FilePath]
[opt_sourcedirs] :: IOption -> [FilePath]
[opt_triple] :: IOption -> String
[opt_cpu] :: IOption -> String

-- | remember whole command line
[opt_cmdline] :: IOption -> [Opt]
[opt_origerr] :: IOption -> Bool

-- | automatically apply "solve" tactic in prover
[opt_autoSolve] :: IOption -> Bool

-- | List of modules to auto import i.e. `Builtins+Prelude`
[opt_autoImport] :: IOption -> [FilePath]
[opt_optimise] :: IOption -> [Optimisation]
[opt_printdepth] :: IOption -> Maybe Int

-- | normalise types in `:t`
[opt_evaltypes] :: IOption -> Bool
[opt_desugarnats] :: IOption -> Bool
[opt_autoimpls] :: IOption -> Bool
defaultOpts :: IOption
data PPOption
PPOption :: Bool -> Bool -> Bool -> Maybe Int -> Bool -> PPOption

-- | whether to show implicits
[ppopt_impl] :: PPOption -> Bool
[ppopt_desugarnats] :: PPOption -> Bool

-- | whether to show names in pi bindings
[ppopt_pinames] :: PPOption -> Bool
[ppopt_depth] :: PPOption -> Maybe Int

-- | whether to display multiplicities in binders
[ppopt_displayrig] :: PPOption -> Bool
defaultOptimise :: [Optimisation]

-- | Pretty printing options with default verbosity.
defaultPPOption :: PPOption

-- | Pretty printing options with the most verbosity.
verbosePPOption :: PPOption

-- | Get pretty printing options from the big options record.
ppOption :: IOption -> PPOption

-- | Get pretty printing options from an idris state record.
ppOptionIst :: IState -> PPOption

-- | The output mode in use
data OutputMode

-- | Print user output directly to the handle
RawOutput :: Handle -> OutputMode

-- | Send IDE output for some request ID to the handle
IdeMode :: Integer -> Handle -> OutputMode

-- | If a function has no totality annotation, what do we assume?
data DefaultTotality

-- | Total
DefaultCheckingTotal :: DefaultTotality

-- | Partial
DefaultCheckingPartial :: DefaultTotality

-- | Total coverage, but may diverge
DefaultCheckingCovering :: DefaultTotality

-- | Configuration options for interactive editing.
data InteractiveOpts
InteractiveOpts :: Int -> Int -> InteractiveOpts
[interactiveOpts_indentWith] :: InteractiveOpts -> Int
[interactiveOpts_indentClause] :: InteractiveOpts -> Int

-- | The global state used in the Idris monad
data IState
IState :: Context -> Set ConstraintFC -> [FixDecl] -> Ctxt [PArg] -> Ctxt [Bool] -> Ctxt InterfaceInfo -> [Name] -> Ctxt RecordInfo -> Ctxt DSL -> Ctxt OptInfo -> Ctxt TypeInfo -> Ctxt [Name] -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm]) -> Ctxt [FnOpt] -> Ctxt CGInfo -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]) -> Ctxt (Docstring DocTerm) -> Ctxt TIData -> Ctxt FnInfo -> Ctxt [(Term, Term)] -> Ctxt [Name] -> [(FC, Name)] -> [(FC, Name)] -> [(FC, String)] -> IOption -> Int -> [((FilePath, Int), PTerm)] -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name] -> [(Term, Term)] -> [Name] -> SyntaxRules -> [String] -> [FilePath] -> [(Name, (Int, PrimFn))] -> [(Codegen, FilePath)] -> [(Codegen, String)] -> [(Codegen, String)] -> [(Codegen, String)] -> [(FilePath, Bool)] -> [(Name, (Bool, [String]))] -> Maybe FC -> [(FC, Err)] -> Maybe Name -> [Int] -> [Maybe Int] -> Maybe FC -> Ctxt Accessibility -> Accessibility -> DefaultTotality -> [IBCWrite] -> Maybe String -> [DynamicLib] -> [LanguageExt] -> OutputMode -> Bool -> ColourTheme -> [Name] -> (Int, Ctxt (Int, Name)) -> Ctxt (Map Name (Set Name)) -> Map [Text] [Text] -> ConsoleWidth -> Set Name -> Set (Name, Int) -> [(Name, Int)] -> [Name] -> [(Name, Bool)] -> Map Name Name -> [Name] -> Set (FC', OutputAnnotation) -> Set (FC', OutputAnnotation) -> Ctxt String -> Set Name -> Map Term (Int, Term) -> Ctxt String -> InteractiveOpts -> IState

-- | All the currently defined names and their terms
[tt_ctxt] :: IState -> Context

-- | A list of universe constraints and their corresponding source
--   locations
[idris_constraints] :: IState -> Set ConstraintFC

-- | Currently defined infix operators
[idris_infixes] :: IState -> [FixDecl]
[idris_implicits] :: IState -> Ctxt [PArg]
[idris_statics] :: IState -> Ctxt [Bool]
[idris_interfaces] :: IState -> Ctxt InterfaceInfo

-- | Privileged implementations, will resolve immediately
[idris_openimpls] :: IState -> [Name]
[idris_records] :: IState -> Ctxt RecordInfo
[idris_dsls] :: IState -> Ctxt DSL
[idris_optimisation] :: IState -> Ctxt OptInfo
[idris_datatypes] :: IState -> Ctxt TypeInfo
[idris_namehints] :: IState -> Ctxt [Name]

-- | list of lhs/rhs, and a list of missing clauses. These are not
--   exported.
[idris_patdefs] :: IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
[idris_flags] :: IState -> Ctxt [FnOpt]

-- | name, args used in each pos
[idris_callgraph] :: IState -> Ctxt CGInfo
[idris_docstrings] :: IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])

-- | module documentation is saved in a special MN so the context mechanism
--   can be used for disambiguation.
[idris_moduledocs] :: IState -> Ctxt (Docstring DocTerm)
[idris_tyinfodata] :: IState -> Ctxt TIData
[idris_fninfo] :: IState -> Ctxt FnInfo
[idris_transforms] :: IState -> Ctxt [(Term, Term)]
[idris_autohints] :: IState -> Ctxt [Name]

-- | names to check totality on
[idris_totcheck] :: IState -> [(FC, Name)]

-- | names to check at the end
[idris_defertotcheck] :: IState -> [(FC, Name)]
[idris_totcheckfail] :: IState -> [(FC, String)]
[idris_options] :: IState -> IOption
[idris_name] :: IState -> Int

-- | Full application LHS on source line
[idris_lineapps] :: IState -> [((FilePath, Int), PTerm)]

-- | The currently defined but not proven metavariables. The Int is the
--   number of vars to display as a context, the Maybe Name is its
--   top-level function, the [Name] is the list of local variables
--   available for proof search and the Bools are whether :p is allowed,
--   and whether the variable is definable at all (Metavariables are not
--   definable if they are applied in a term which still has hole bindings)
[idris_metavars] :: IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
[idris_coercions] :: IState -> [Name]
[idris_errRev] :: IState -> [(Term, Term)]
[idris_errReduce] :: IState -> [Name]
[syntax_rules] :: IState -> SyntaxRules
[syntax_keywords] :: IState -> [String]

-- | The imported modules
[imported] :: IState -> [FilePath]
[idris_scprims] :: IState -> [(Name, (Int, PrimFn))]
[idris_objs] :: IState -> [(Codegen, FilePath)]
[idris_libs] :: IState -> [(Codegen, String)]
[idris_cgflags] :: IState -> [(Codegen, String)]
[idris_hdrs] :: IState -> [(Codegen, String)]

-- | Imported ibc file names, whether public
[idris_imported] :: IState -> [(FilePath, Bool)]
[proof_list] :: IState -> [(Name, (Bool, [String]))]
[errSpan] :: IState -> Maybe FC
[parserWarnings] :: IState -> [(FC, Err)]
[lastParse] :: IState -> Maybe Name
[indent_stack] :: IState -> [Int]
[brace_stack] :: IState -> [Maybe Int]
[idris_parsedSpan] :: IState -> Maybe FC
[hide_list] :: IState -> Ctxt Accessibility
[default_access] :: IState -> Accessibility
[default_total] :: IState -> DefaultTotality
[ibc_write] :: IState -> [IBCWrite]
[compiled_so] :: IState -> Maybe String
[idris_dynamic_libs] :: IState -> [DynamicLib]
[idris_language_extensions] :: IState -> [LanguageExt]
[idris_outputmode] :: IState -> OutputMode
[idris_colourRepl] :: IState -> Bool
[idris_colourTheme] :: IState -> ColourTheme

-- | Global error handlers
[idris_errorhandlers] :: IState -> [Name]
[idris_nameIdx] :: IState -> (Int, Ctxt (Int, Name))

-- | Specific error handlers
[idris_function_errorhandlers] :: IState -> Ctxt (Map Name (Set Name))
[module_aliases] :: IState -> Map [Text] [Text]

-- | How many chars wide is the console?
[idris_consolewidth] :: IState -> ConsoleWidth
[idris_postulates] :: IState -> Set Name
[idris_externs] :: IState -> Set (Name, Int)

-- | Function/constructor name, argument position is used
[idris_erasureUsed] :: IState -> [(Name, Int)]

-- | List of names that were defined in the repl, and can be re-/un-defined
[idris_repl_defs] :: IState -> [Name]

-- | Stack of names currently being elaborated, Bool set if it's an
--   implementation (implementations appear twice; also as a function name)
[elab_stack] :: IState -> [(Name, Bool)]

-- | Symbol table (preserves sharing of names)
[idris_symbols] :: IState -> Map Name Name

-- | Functions with ExportList
[idris_exports] :: IState -> [Name]

-- | Highlighting information to output
[idris_highlightedRegions] :: IState -> Set (FC', OutputAnnotation)

-- | Highlighting information from the parser
[idris_parserHighlights] :: IState -> Set (FC', OutputAnnotation)

-- | Deprecated names and explanation
[idris_deprecated] :: IState -> Ctxt String

-- | Names defined in current module
[idris_inmodule] :: IState -> Set Name
[idris_ttstats] :: IState -> Map Term (Int, Term)

-- | Fragile names and explanation.
[idris_fragile] :: IState -> Ctxt String
[idris_interactiveOpts] :: IState -> InteractiveOpts
data SizeChange
Smaller :: SizeChange
Same :: SizeChange
Bigger :: SizeChange
Unknown :: SizeChange
type SCGEntry = (Name, [Maybe (Int, SizeChange)])
type UsageReason = (Name, Int)
data CGInfo
CGInfo :: [Name] -> Maybe [Name] -> [SCGEntry] -> [(Int, [UsageReason])] -> CGInfo
[calls] :: CGInfo -> [Name]
[allCalls] :: CGInfo -> Maybe [Name]
[scg] :: CGInfo -> [SCGEntry]
[usedpos] :: CGInfo -> [(Int, [UsageReason])]
primDefs :: [Name]
data IBCWrite
IBCFix :: FixDecl -> IBCWrite
IBCImp :: Name -> IBCWrite
IBCStatic :: Name -> IBCWrite
IBCInterface :: Name -> IBCWrite
IBCRecord :: Name -> IBCWrite
IBCImplementation :: Bool -> Bool -> Name -> Name -> IBCWrite
IBCDSL :: Name -> IBCWrite
IBCData :: Name -> IBCWrite
IBCOpt :: Name -> IBCWrite
IBCMetavar :: Name -> IBCWrite
IBCSyntax :: Syntax -> IBCWrite
IBCKeyword :: String -> IBCWrite

-- | True = import public
IBCImport :: (Bool, FilePath) -> IBCWrite
IBCImportDir :: FilePath -> IBCWrite
IBCSourceDir :: FilePath -> IBCWrite
IBCObj :: Codegen -> FilePath -> IBCWrite
IBCLib :: Codegen -> String -> IBCWrite
IBCCGFlag :: Codegen -> String -> IBCWrite
IBCDyLib :: String -> IBCWrite
IBCHeader :: Codegen -> String -> IBCWrite
IBCAccess :: Name -> Accessibility -> IBCWrite
IBCMetaInformation :: Name -> MetaInformation -> IBCWrite
IBCTotal :: Name -> Totality -> IBCWrite
IBCInjective :: Name -> Injectivity -> IBCWrite
IBCFlags :: Name -> IBCWrite
IBCFnInfo :: Name -> FnInfo -> IBCWrite
IBCTrans :: Name -> (Term, Term) -> IBCWrite
IBCErrRev :: (Term, Term) -> IBCWrite
IBCErrReduce :: Name -> IBCWrite
IBCCG :: Name -> IBCWrite
IBCDoc :: Name -> IBCWrite
IBCCoercion :: Name -> IBCWrite

-- | The main context.
IBCDef :: Name -> IBCWrite
IBCNameHint :: (Name, Name) -> IBCWrite
IBCLineApp :: FilePath -> Int -> PTerm -> IBCWrite
IBCErrorHandler :: Name -> IBCWrite
IBCFunctionErrorHandler :: Name -> Name -> Name -> IBCWrite
IBCPostulate :: Name -> IBCWrite
IBCExtern :: (Name, Int) -> IBCWrite
IBCTotCheckErr :: FC -> String -> IBCWrite
IBCParsedRegion :: FC -> IBCWrite

-- | The name is the special name used to track module docs
IBCModDocs :: Name -> IBCWrite
IBCUsage :: (Name, Int) -> IBCWrite
IBCExport :: Name -> IBCWrite
IBCAutoHint :: Name -> Name -> IBCWrite
IBCDeprecate :: Name -> String -> IBCWrite
IBCFragile :: Name -> String -> IBCWrite
IBCConstraint :: FC -> UConstraint -> IBCWrite
IBCImportHash :: FilePath -> Int -> IBCWrite
initialInteractiveOpts :: InteractiveOpts

-- | The initial state for the compiler
idrisInit :: IState

-- | The monad for the main REPL - reading and processing files and
--   updating global state (hence the IO inner monad).
--   
--   <pre>
--   type Idris = WriterT [Either String (IO ())] (State IState a))
--   </pre>
type Idris = StateT IState (ExceptT Err IO)
catchError :: Idris a -> (Err -> Idris a) -> Idris a
throwError :: Err -> Idris a
data ElabShellCmd
EQED :: ElabShellCmd
EAbandon :: ElabShellCmd
EUndo :: ElabShellCmd
EProofState :: ElabShellCmd
EProofTerm :: ElabShellCmd
EEval :: PTerm -> ElabShellCmd
ECheck :: PTerm -> ElabShellCmd
ESearch :: PTerm -> ElabShellCmd
EDocStr :: Either Name Const -> ElabShellCmd
data Fixity
Infixl :: Int -> Fixity
[prec] :: Fixity -> Int
Infixr :: Int -> Fixity
[prec] :: Fixity -> Int
InfixN :: Int -> Fixity
[prec] :: Fixity -> Int
PrefixN :: Int -> Fixity
[prec] :: Fixity -> Int
data FixDecl
Fix :: Fixity -> String -> FixDecl

-- | Mark bindings with their explicitness, and laziness
data Static
Static :: Static
Dynamic :: Static
data Plicity
Imp :: [ArgOpt] -> Static -> Bool -> Maybe ImplicitInfo -> Bool -> RigCount -> Plicity
[pargopts] :: Plicity -> [ArgOpt]
[pstatic] :: Plicity -> Static

-- | this is a param (rather than index)
[pparam] :: Plicity -> Bool

-- | Nothing, if top level
[pscoped] :: Plicity -> Maybe ImplicitInfo

-- | Explicitly written in source
[pinsource] :: Plicity -> Bool
[pcount] :: Plicity -> RigCount
Exp :: [ArgOpt] -> Static -> Bool -> RigCount -> Plicity
[pargopts] :: Plicity -> [ArgOpt]
[pstatic] :: Plicity -> Static

-- | this is a param (rather than index)
[pparam] :: Plicity -> Bool
[pcount] :: Plicity -> RigCount
Constraint :: [ArgOpt] -> Static -> RigCount -> Plicity
[pargopts] :: Plicity -> [ArgOpt]
[pstatic] :: Plicity -> Static
[pcount] :: Plicity -> RigCount
TacImp :: [ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
[pargopts] :: Plicity -> [ArgOpt]
[pstatic] :: Plicity -> Static
[pscript] :: Plicity -> PTerm
[pcount] :: Plicity -> RigCount
is_scoped :: Plicity -> Maybe ImplicitInfo
impl :: Plicity
impl_gen :: Plicity
forall_imp :: Plicity
forall_constraint :: Plicity
expl :: Plicity
expl_param :: Plicity
expl_linear :: Plicity
constraint :: Plicity
tacimpl :: PTerm -> Plicity
data FnOpt

-- | always evaluate when simplifying
Inlinable :: FnOpt
TotalFn :: FnOpt
PartialFn :: FnOpt
CoveringFn :: FnOpt

-- | all delayed arguments guaranteed guarded by constructors
AllGuarded :: FnOpt
AssertTotal :: FnOpt

-- | interface dictionary, eval only when a function argument, and further
--   evaluation results.
Dictionary :: FnOpt

-- | Interface dictionary which may overlap
OverlappingDictionary :: FnOpt

-- | implicit coercion
Implicit :: FnOpt

-- | do not apply implicit coercions
NoImplicit :: FnOpt

-- | export, with a C name
CExport :: String -> FnOpt

-- | an error handler for use with the ErrorReflection extension
ErrorHandler :: FnOpt

-- | attempt to reverse normalise before showing in error
ErrorReverse :: FnOpt

-- | unfold definition before showing an error
ErrorReduce :: FnOpt

-- | a reflecting function, compile-time only
Reflection :: FnOpt

-- | specialise it, freeze these names
Specialise :: [(Name, Maybe Int)] -> FnOpt

-- | Data constructor type
Constructor :: FnOpt

-- | use in auto implicit search
AutoHint :: FnOpt

-- | generated by partial evaluator
PEGenerated :: FnOpt

-- | Marked static, to be evaluated by partial evaluator
StaticFn :: FnOpt
type FnOpts = [FnOpt]
inlinable :: FnOpts -> Bool
dictionary :: FnOpts -> Bool

-- | Type provider - what to provide
data ProvideWhat' t

-- | the first is the goal type, the second is the term
ProvTerm :: t -> t -> ProvideWhat' t

-- | goal type must be Type, so only term
ProvPostulate :: t -> ProvideWhat' t
type ProvideWhat = ProvideWhat' PTerm

-- | Top-level declarations such as compiler directives, definitions,
--   datatypes and interfaces.
data PDecl' t

-- | Fixity declaration
PFix :: FC -> Fixity -> [String] -> PDecl' t

-- | Type declaration (last FC is precise name location)
PTy :: Docstring (Either Err t) -> [(Name, Docstring (Either Err t))] -> SyntaxInfo -> FC -> FnOpts -> Name -> FC -> t -> PDecl' t

-- | Postulate, second FC is precise name location
PPostulate :: Bool -> Docstring (Either Err t) -> SyntaxInfo -> FC -> FC -> FnOpts -> Name -> t -> PDecl' t

-- | Pattern clause
PClauses :: FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t

-- | Top level constant
PCAF :: FC -> Name -> t -> PDecl' t

-- | Data declaration.
PData :: Docstring (Either Err t) -> [(Name, Docstring (Either Err t))] -> SyntaxInfo -> FC -> DataOpts -> PData' t -> PDecl' t

-- | Params block
PParams :: FC -> [(Name, t)] -> [PDecl' t] -> PDecl' t

-- | Open block/declaration
POpenInterfaces :: FC -> [Name] -> [PDecl' t] -> PDecl' t

-- | New namespace, where FC is accurate location of the namespace in the
--   file
PNamespace :: String -> FC -> [PDecl' t] -> PDecl' t

-- | Record name.
PRecord :: Docstring (Either Err t) -> SyntaxInfo -> FC -> DataOpts -> Name -> FC -> [(Name, FC, Plicity, t)] -> [(Name, Docstring (Either Err t))] -> [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -> Maybe (Name, FC) -> Docstring (Either Err t) -> SyntaxInfo -> PDecl' t

-- | Interface: arguments are documentation, syntax info, source location,
--   constraints, interface name, interface name location, parameters,
--   method declarations, optional constructor name
PInterface :: Docstring (Either Err t) -> SyntaxInfo -> FC -> [(Name, t)] -> Name -> FC -> [(Name, FC, t)] -> [(Name, Docstring (Either Err t))] -> [(Name, FC)] -> [PDecl' t] -> Maybe (Name, FC) -> Docstring (Either Err t) -> PDecl' t

-- | Implementation declaration: arguments are documentation, syntax info,
--   source location, constraints, interface name, parameters, full
--   Implementation type, optional explicit name, and definitions
PImplementation :: Docstring (Either Err t) -> [(Name, Docstring (Either Err t))] -> SyntaxInfo -> FC -> [(Name, t)] -> [Name] -> Accessibility -> FnOpts -> Name -> FC -> [t] -> [(Name, t)] -> t -> Maybe Name -> [PDecl' t] -> PDecl' t

-- | DSL declaration
PDSL :: Name -> DSL' t -> PDecl' t

-- | Syntax definition
PSyntax :: FC -> Syntax -> PDecl' t

-- | Mutual block
PMutual :: FC -> [PDecl' t] -> PDecl' t

-- | Compiler directive.
PDirective :: Directive -> PDecl' t

-- | Type provider. The first t is the type, the second is the term. The
--   second FC is precise highlighting location.
PProvider :: Docstring (Either Err t) -> SyntaxInfo -> FC -> FC -> ProvideWhat' t -> Name -> PDecl' t

-- | Source-to-source transformation rule. If bool is True, lhs and rhs
--   must be convertible.
PTransform :: FC -> Bool -> t -> t -> PDecl' t

-- | FC is decl-level, for errors, and Strings represent the namespace
PRunElabDecl :: FC -> t -> [String] -> PDecl' t

-- | The set of source directives
data Directive
DLib :: Codegen -> String -> Directive
DLink :: Codegen -> String -> Directive
DFlag :: Codegen -> String -> Directive
DInclude :: Codegen -> String -> Directive
DHide :: Name -> Directive
DFreeze :: Name -> Directive
DThaw :: Name -> Directive
DInjective :: Name -> Directive
DSetTotal :: Name -> Directive
DAccess :: Accessibility -> Directive
DDefault :: DefaultTotality -> Directive
DLogging :: Integer -> Directive
DDynamicLibs :: [String] -> Directive
DNameHint :: Name -> FC -> [(Name, FC)] -> Directive
DErrorHandlers :: Name -> FC -> Name -> FC -> [(Name, FC)] -> Directive
DLanguage :: LanguageExt -> Directive
DDeprecate :: Name -> String -> Directive
DFragile :: Name -> String -> Directive
DAutoImplicits :: Bool -> Directive
DUsed :: FC -> Name -> Name -> Directive

-- | A set of instructions for things that need to happen in IState after a
--   term elaboration when there's been reflected elaboration.
data RDeclInstructions
RTyDeclInstrs :: Name -> FC -> [PArg] -> Type -> RDeclInstructions
RClausesInstrs :: Name -> [([(Name, Term)], Term, Term)] -> RDeclInstructions
RAddImplementation :: Name -> Name -> RDeclInstructions
RDatatypeDeclInstrs :: Name -> [PArg] -> RDeclInstructions

-- | Datatype, constructors
RDatatypeDefnInstrs :: Name -> Type -> [(Name, [PArg], Type)] -> RDeclInstructions

-- | For elaborator state
data EState
EState :: [(Name, PDecl)] -> [(Int, Elab' EState ())] -> [RDeclInstructions] -> Set (FC', OutputAnnotation) -> [Name] -> [(FC, Name)] -> EState
[case_decls] :: EState -> [(Name, PDecl)]
[delayed_elab] :: EState -> [(Int, Elab' EState ())]
[new_tyDecls] :: EState -> [RDeclInstructions]
[highlighting] :: EState -> Set (FC', OutputAnnotation)

-- | names bound as auto implicits
[auto_binds] :: EState -> [Name]

-- | Implicit warnings to report (location and global name)
[implicit_warnings] :: EState -> [(FC, Name)]
initEState :: EState
type ElabD a = Elab' EState a
highlightSource :: FC -> OutputAnnotation -> ElabD ()

-- | One clause of a top-level definition. Term arguments to constructors
--   are:
--   
--   <ol>
--   <li>The whole application (missing for PClauseR and PWithR because
--   they're within a "with" clause)</li>
--   <li>The list of extra <tt>with</tt> patterns</li>
--   <li>The right-hand side</li>
--   <li>The where block (PDecl' t)</li>
--   </ol>
data PClause' t

-- | A normal top-level definition.
PClause :: FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PWith :: FC -> Name -> t -> [t] -> t -> Maybe (Name, FC) -> [PDecl' t] -> PClause' t
PClauseR :: FC -> [t] -> t -> [PDecl' t] -> PClause' t
PWithR :: FC -> [t] -> t -> Maybe (Name, FC) -> [PDecl' t] -> PClause' t

-- | Data declaration
data PData' t

-- | Data declaration
PDatadecl :: Name -> FC -> t -> [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -> PData' t

-- | The name of the datatype
[d_name] :: PData' t -> Name

-- | The precise location of the type constructor name
[d_name_fc] :: PData' t -> FC

-- | Type constructor
[d_tcon] :: PData' t -> t

-- | Constructors
[d_cons] :: PData' t -> [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]

-- | <a>Placeholder</a> for data whose constructors are defined later
PLaterdecl :: Name -> FC -> t -> PData' t

-- | The name of the datatype
[d_name] :: PData' t -> Name

-- | The precise location of the type constructor name
[d_name_fc] :: PData' t -> FC

-- | Type constructor
[d_tcon] :: PData' t -> t

-- | Transform the FCs in a PData and its associated terms. The first
--   function transforms the general-purpose FCs, and the second transforms
--   those that are used for semantic source highlighting, so they can be
--   treated specially.
mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
type PDecl = PDecl' PTerm
type PData = PData' PTerm
type PClause = PClause' PTerm

-- | Transform the FCs in a PTerm. The first function transforms the
--   general-purpose FCs, and the second transforms those that are used for
--   semantic source highlighting, so they can be treated specially.
mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl

-- | Get all the names declared in a declaration
declared :: PDecl -> [Name]
tldeclared :: PDecl -> [Name]
defined :: PDecl -> [Name]
updateN :: [(Name, Name)] -> Name -> Name
updateNs :: [(Name, Name)] -> PTerm -> PTerm
data PunInfo
IsType :: PunInfo
IsTerm :: PunInfo
TypeOrTerm :: PunInfo

-- | High level language terms
data PTerm

-- | Inclusion of a core term into the high-level language
PQuote :: Raw -> PTerm

-- | A reference to a variable. The FC is its precise source location for
--   highlighting. The list of FCs is a collection of additional
--   highlighting locations.
PRef :: FC -> [FC] -> Name -> PTerm

-- | A name to be defined later
PInferRef :: FC -> [FC] -> Name -> PTerm

-- | A pattern variable
PPatvar :: FC -> Name -> PTerm

-- | A lambda abstraction. Second FC is name span.
PLam :: FC -> Name -> FC -> PTerm -> PTerm -> PTerm

-- | (n : t1) -&gt; t2, where the FC is for the precise location of the
--   variable
PPi :: Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm

-- | A let binding (second FC is precise name location)
PLet :: FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm

-- | Term with explicit type
PTyped :: PTerm -> PTerm -> PTerm

-- | e.g. IO (), List Char, length x
PApp :: FC -> PTerm -> [PArg] -> PTerm

-- | Application plus a <tt>with</tt> argument
PWithApp :: FC -> PTerm -> PTerm -> PTerm

-- | Implicit argument application (introduced during elaboration only)
PAppImpl :: PTerm -> [ImplicitInfo] -> PTerm

-- | implicitly bound application
PAppBind :: FC -> PTerm -> [PArg] -> PTerm

-- | Make an application by type matching
PMatchApp :: FC -> Name -> PTerm

-- | Conditional expressions - elaborated to an overloading of ifThenElse
PIfThenElse :: FC -> PTerm -> PTerm -> PTerm -> PTerm

-- | A case expression. Args are source location, scrutinee, and a list of
--   pattern/RHS pairs
PCase :: FC -> PTerm -> [(PTerm, PTerm)] -> PTerm

-- | Unit type..?
PTrue :: FC -> PunInfo -> PTerm

-- | Solve this dictionary by interface resolution
PResolveTC :: FC -> PTerm

-- | "rewrite" syntax, with optional rewriting function and optional result
--   type
PRewrite :: FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm

-- | A pair (a, b) and whether it's a product type or a pair (solved by
--   elaboration). The list of FCs is its punctuation.
PPair :: FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm

-- | A dependent pair (tm : a ** b) and whether it's a sigma type or a pair
--   that inhabits one (solved by elaboration). The [FC] is its
--   punctuation.
PDPair :: FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm

-- | @-pattern, valid LHS only
PAs :: FC -> Name -> PTerm -> PTerm

-- | (| A, B, C|). Includes unapplied unique name mappings for
--   mkUniqueNames.
PAlternative :: [(Name, Name)] -> PAltType -> [PTerm] -> PTerm

-- | Irrelevant or hidden pattern
PHidden :: PTerm -> PTerm

-- | <a>Type</a> type
PType :: FC -> PTerm

-- | Some universe
PUniverse :: FC -> Universe -> PTerm

-- | quoteGoal, used for %reflection functions
PGoal :: FC -> PTerm -> Name -> PTerm -> PTerm

-- | Builtin types
PConstant :: FC -> Const -> PTerm

-- | Underscore
Placeholder :: PTerm

-- | Do notation
PDoBlock :: [PDo] -> PTerm

-- | Idiom brackets
PIdiom :: FC -> PTerm -> PTerm

-- | A metavariable, ?name, and its precise location
PMetavar :: FC -> Name -> PTerm

-- | Proof script
PProof :: [PTactic] -> PTerm

-- | As PProof, but no auto solving
PTactics :: [PTactic] -> PTerm

-- | Error to report on elaboration
PElabError :: Err -> PTerm

-- | Special case for declaring when an LHS can't typecheck
PImpossible :: PTerm

-- | To mark a coerced argument, so as not to coerce twice
PCoerced :: PTerm -> PTerm

-- | Preferences for explicit namespaces
PDisamb :: [[Text]] -> PTerm -> PTerm

-- | dump a trace of unifications when building term
PUnifyLog :: PTerm -> PTerm

-- | never run implicit converions on the term
PNoImplicits :: PTerm -> PTerm

-- | `(Term [: Term])
PQuasiquote :: PTerm -> Maybe PTerm -> PTerm

-- | ~Term
PUnquote :: PTerm -> PTerm

-- | `{n} where the FC is the precise highlighting for the name in
--   particular. If the Bool is False, then it's `{{n}} and the name won't
--   be resolved.
PQuoteName :: Name -> Bool -> FC -> PTerm

-- | %runElab tm - New-style proof script. Args are location, script,
--   enclosing namespace.
PRunElab :: FC -> PTerm -> [String] -> PTerm

-- | A desugared constant. The FC is a precise source location that will be
--   used to highlight it later.
PConstSugar :: FC -> PTerm -> PTerm
data PAltType

-- | flag sets whether delay is allowed
ExactlyOne :: Bool -> PAltType
FirstSuccess :: PAltType
TryImplicit :: PAltType

-- | Transform the FCs in a PTerm. The first function transforms the
--   general-purpose FCs, and the second transforms those that are used for
--   semantic source highlighting, so they can be treated specially.
mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
data PTactic' t
Intro :: [Name] -> PTactic' t
Intros :: PTactic' t
Focus :: Name -> PTactic' t
Refine :: Name -> [Bool] -> PTactic' t
Rewrite :: t -> PTactic' t
DoUnify :: PTactic' t
Equiv :: t -> PTactic' t
Claim :: Name -> t -> PTactic' t
Unfocus :: PTactic' t
MatchRefine :: Name -> PTactic' t
LetTac :: Name -> t -> PTactic' t
LetTacTy :: Name -> t -> t -> PTactic' t
Exact :: t -> PTactic' t
Compute :: PTactic' t
Trivial :: PTactic' t
TCImplementation :: PTactic' t

-- | the bool is whether to search recursively
ProofSearch :: Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
Solve :: PTactic' t
Attack :: PTactic' t
ProofState :: PTactic' t
ProofTerm :: PTactic' t
Undo :: PTactic' t
Try :: PTactic' t -> PTactic' t -> PTactic' t
TSeq :: PTactic' t -> PTactic' t -> PTactic' t
ApplyTactic :: t -> PTactic' t
ByReflection :: t -> PTactic' t
Reflect :: t -> PTactic' t
Fill :: t -> PTactic' t
GoalType :: String -> PTactic' t -> PTactic' t
TCheck :: t -> PTactic' t
TEval :: t -> PTactic' t
TDocStr :: Either Name Const -> PTactic' t
TSearch :: t -> PTactic' t
Skip :: PTactic' t
TFail :: [ErrorReportPart] -> PTactic' t
Qed :: PTactic' t
Abandon :: PTactic' t
SourceFC :: PTactic' t
type PTactic = PTactic' PTerm
data PDo' t
DoExp :: FC -> t -> PDo' t

-- | second FC is precise name location
DoBind :: FC -> Name -> FC -> t -> PDo' t
DoBindP :: FC -> t -> t -> [(t, t)] -> PDo' t

-- | second FC is precise name location
DoLet :: FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLetP :: FC -> t -> t -> [(t, t)] -> PDo' t
DoRewrite :: FC -> t -> PDo' t
type PDo = PDo' PTerm
data PArg' t
PImp :: Int -> Bool -> [ArgOpt] -> Name -> t -> PArg' t
[priority] :: PArg' t -> Int

-- | true if the machine inferred it
[machine_inf] :: PArg' t -> Bool
[argopts] :: PArg' t -> [ArgOpt]
[pname] :: PArg' t -> Name
[getTm] :: PArg' t -> t
PExp :: Int -> [ArgOpt] -> Name -> t -> PArg' t
[priority] :: PArg' t -> Int
[argopts] :: PArg' t -> [ArgOpt]
[pname] :: PArg' t -> Name
[getTm] :: PArg' t -> t
PConstraint :: Int -> [ArgOpt] -> Name -> t -> PArg' t
[priority] :: PArg' t -> Int
[argopts] :: PArg' t -> [ArgOpt]
[pname] :: PArg' t -> Name
[getTm] :: PArg' t -> t
PTacImplicit :: Int -> [ArgOpt] -> Name -> t -> t -> PArg' t
[priority] :: PArg' t -> Int
[argopts] :: PArg' t -> [ArgOpt]
[pname] :: PArg' t -> Name
[getScript] :: PArg' t -> t
[getTm] :: PArg' t -> t
data ArgOpt
AlwaysShow :: ArgOpt
HideDisplay :: ArgOpt
InaccessibleArg :: ArgOpt
UnknownImp :: ArgOpt
pimp :: () => Name -> t -> Bool -> PArg' t
pexp :: () => t -> PArg' t
pconst :: () => t -> PArg' t
ptacimp :: () => Name -> t -> t -> PArg' t
type PArg = PArg' PTerm

-- | Get the highest FC in a term, if one exists
highestFC :: PTerm -> Maybe FC
data InterfaceInfo
CI :: Name -> [(Name, (Bool, FnOpts, PTerm))] -> [(Name, (Name, PDecl))] -> [PDecl] -> [Name] -> [Name] -> [PTerm] -> [(Name, Bool)] -> [Int] -> InterfaceInfo
[implementationCtorName] :: InterfaceInfo -> Name

-- | flag whether it's a "data" method
[interface_methods] :: InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]

-- | method name -&gt; default impl
[interface_defaults] :: InterfaceInfo -> [(Name, (Name, PDecl))]
[interface_default_super_interfaces] :: InterfaceInfo -> [PDecl]
[interface_impparams] :: InterfaceInfo -> [Name]
[interface_params] :: InterfaceInfo -> [Name]
[interface_constraints] :: InterfaceInfo -> [PTerm]

-- | the Bool is whether to include in implementation search, so named
--   implementations are excluded
[interface_implementations] :: InterfaceInfo -> [(Name, Bool)]
[interface_determiners] :: InterfaceInfo -> [Int]
data RecordInfo
RI :: [(Name, PTerm)] -> Name -> [Name] -> RecordInfo
[record_parameters] :: RecordInfo -> [(Name, PTerm)]
[record_constructor] :: RecordInfo -> Name
[record_projections] :: RecordInfo -> [Name]
data TIData

-- | a function with a partially defined type
TIPartial :: TIData

-- | possible solutions to a metavariable in a type
TISolution :: [Term] -> TIData

-- | Miscellaneous information about functions
data FnInfo
FnInfo :: [Int] -> FnInfo
[fn_params] :: FnInfo -> [Int]
data OptInfo
Optimise :: [(Int, Name)] -> Bool -> [Int] -> OptInfo
[inaccessible] :: OptInfo -> [(Int, Name)]
[detaggable] :: OptInfo -> Bool
[forceable] :: OptInfo -> [Int]

-- | Syntactic sugar info
data DSL' t
DSL :: t -> t -> t -> Maybe t -> Maybe t -> Maybe t -> Maybe t -> Maybe t -> Maybe t -> DSL' t
[dsl_bind] :: DSL' t -> t
[dsl_apply] :: DSL' t -> t
[dsl_pure] :: DSL' t -> t
[dsl_var] :: DSL' t -> Maybe t
[index_first] :: DSL' t -> Maybe t
[index_next] :: DSL' t -> Maybe t
[dsl_lambda] :: DSL' t -> Maybe t
[dsl_let] :: DSL' t -> Maybe t
[dsl_pi] :: DSL' t -> Maybe t
type DSL = DSL' PTerm
data SynContext
PatternSyntax :: SynContext
TermSyntax :: SynContext
AnySyntax :: SynContext
data Syntax
Rule :: [SSymbol] -> PTerm -> SynContext -> Syntax
DeclRule :: [SSymbol] -> [PDecl] -> Syntax
syntaxNames :: Syntax -> [Name]
syntaxSymbols :: Syntax -> [SSymbol]
data SSymbol
Keyword :: Name -> SSymbol
Symbol :: String -> SSymbol
Binding :: Name -> SSymbol
Expr :: Name -> SSymbol
SimpleExpr :: Name -> SSymbol
newtype SyntaxRules
SyntaxRules :: [Syntax] -> SyntaxRules
[syntaxRulesList] :: SyntaxRules -> [Syntax]
emptySyntaxRules :: SyntaxRules
updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
initDSL :: DSL' PTerm
data Using
UImplicit :: Name -> PTerm -> Using
UConstraint :: Name -> [Name] -> Using
data SyntaxInfo
Syn :: [Using] -> [(Name, PTerm)] -> [String] -> [Name] -> [Name] -> (Name -> Name) -> Bool -> Bool -> Bool -> Maybe Int -> Int -> DSL -> Int -> Bool -> Bool -> SyntaxInfo
[using] :: SyntaxInfo -> [Using]
[syn_params] :: SyntaxInfo -> [(Name, PTerm)]
[syn_namespace] :: SyntaxInfo -> [String]
[no_imp] :: SyntaxInfo -> [Name]

-- | interface methods. When expanding implicits, these should be expanded
--   even under binders
[imp_methods] :: SyntaxInfo -> [Name]
[decoration] :: SyntaxInfo -> Name -> Name
[inPattern] :: SyntaxInfo -> Bool
[implicitAllowed] :: SyntaxInfo -> Bool
[constraintAllowed] :: SyntaxInfo -> Bool
[maxline] :: SyntaxInfo -> Maybe Int
[mut_nesting] :: SyntaxInfo -> Int
[dsl_info] :: SyntaxInfo -> DSL
[syn_in_quasiquote] :: SyntaxInfo -> Int
[syn_toplevel] :: SyntaxInfo -> Bool
[withAppAllowed] :: SyntaxInfo -> Bool
defaultSyntax :: SyntaxInfo
expandNS :: SyntaxInfo -> Name -> Name
bi :: FC
primfc :: FC
inferTy :: Name
inferCon :: Name
inferDecl :: PData' PTerm
inferOpts :: () => [a]
infTerm :: PTerm -> PTerm
infP :: TT Name
getInferTerm :: Term -> Term
getInferType :: Term -> Term
primNames :: [Name]
unitTy :: Name
unitCon :: Name
falseDoc :: () => Docstring (Err' t)
falseTy :: Name
pairTy :: Name
pairCon :: Name
upairTy :: Name
upairCon :: Name
eqTy :: Name
eqCon :: Name
eqDoc :: () => Docstring (Either (Err' t) b)
eqDecl :: PData' PTerm
eqParamDoc :: () => [(Name, Docstring (Either (Err' t) b))]
eqOpts :: () => [a]

-- | The special name to be used in the module documentation context - not
--   for use in the main definition context. The namespace around it will
--   determine the module to which the docs adhere.
modDocName :: Name
sigmaTy :: Name
sigmaCon :: Name
piBind :: [(Name, PTerm)] -> PTerm -> PTerm
piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

-- | Colourise annotations according to an Idris state. It ignores the
--   names in the annotation, as there's no good way to show extended
--   information on a terminal.
annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour

-- | Colourise annotations according to an Idris state. It ignores the
--   names in the annotation, as there's no good way to show extended
--   information on a terminal. Note that strings produced this way will
--   not be coloured on Windows, so the use of the colour rendering
--   functions in Idris.Output is to be preferred.
consoleDecorate :: IState -> OutputAnnotation -> String -> String
isPostulateName :: Name -> IState -> Bool

-- | Pretty-print a high-level closed Idris term with no information about
--   precedence/associativity
prettyImp :: PPOption -> PTerm -> Doc OutputAnnotation

-- | Serialise something to base64 using its Binary implementation.
--   
--   Do the right thing for rendering a term in an IState
prettyIst :: IState -> PTerm -> Doc OutputAnnotation

-- | Pretty-print a high-level Idris term in some bindings context with
--   infix info.
pprintPTerm :: PPOption -> [(Name, Bool)] -> [Name] -> [FixDecl] -> PTerm -> Doc OutputAnnotation

-- | Strip away namespace information
basename :: Name -> Name

-- | Determine whether a name was the one inserted for a hole or guess by
--   the delaborator
isHoleName :: Name -> Bool

-- | Check whether a PTerm has been delaborated from a Term containing a
--   Hole or Guess
containsHole :: PTerm -> Bool

-- | Pretty-printer helper for names that attaches the correct annotations
prettyName :: Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
showCImp :: PPOption -> PClause -> Doc OutputAnnotation
showDImp :: PPOption -> PData -> Doc OutputAnnotation
showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
showDeclImp :: PPOption -> PDecl' PTerm -> Doc OutputAnnotation
getImps :: [PArg] -> [(Name, PTerm)]
getExps :: [PArg] -> [PTerm]
getShowArgs :: [PArg] -> [PArg]
getConsts :: [PArg] -> [PTerm]
getAll :: [PArg] -> [PTerm]

-- | Show Idris name
showName :: Maybe IState -> [(Name, Bool)] -> PPOption -> Bool -> Name -> String
showTm :: IState -> PTerm -> String

-- | Show a term with implicits, no colours
showTmImpls :: PTerm -> String

-- | Show a term with specific options
showTmOpts :: PPOption -> PTerm -> String
getPArity :: PTerm -> Int
allNamesIn :: PTerm -> [Name]
boundNamesIn :: PTerm -> [Name]
implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
getErasureInfo :: IState -> Name -> [Int]
instance GHC.Generics.Generic Idris.AbsSyntaxTree.IState
instance GHC.Generics.Generic Idris.AbsSyntaxTree.InterfaceInfo
instance GHC.Show.Show Idris.AbsSyntaxTree.InterfaceInfo
instance GHC.Generics.Generic Idris.AbsSyntaxTree.IBCWrite
instance GHC.Show.Show Idris.AbsSyntaxTree.IBCWrite
instance GHC.Generics.Generic Idris.AbsSyntaxTree.SyntaxRules
instance GHC.Generics.Generic (Idris.AbsSyntaxTree.PClause' t)
instance GHC.Base.Functor Idris.AbsSyntaxTree.PClause'
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Syntax
instance GHC.Show.Show Idris.AbsSyntaxTree.Syntax
instance GHC.Generics.Generic (Idris.AbsSyntaxTree.PDecl' t)
instance GHC.Base.Functor Idris.AbsSyntaxTree.PDecl'
instance GHC.Generics.Generic Idris.AbsSyntaxTree.SyntaxInfo
instance GHC.Show.Show Idris.AbsSyntaxTree.SyntaxInfo
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Using
instance Data.Data.Data Idris.AbsSyntaxTree.Using
instance GHC.Classes.Eq Idris.AbsSyntaxTree.Using
instance GHC.Show.Show Idris.AbsSyntaxTree.Using
instance GHC.Generics.Generic Idris.AbsSyntaxTree.SSymbol
instance GHC.Classes.Eq Idris.AbsSyntaxTree.SSymbol
instance GHC.Show.Show Idris.AbsSyntaxTree.SSymbol
instance GHC.Generics.Generic Idris.AbsSyntaxTree.SynContext
instance GHC.Show.Show Idris.AbsSyntaxTree.SynContext
instance GHC.Generics.Generic (Idris.AbsSyntaxTree.DSL' t)
instance GHC.Base.Functor Idris.AbsSyntaxTree.DSL'
instance GHC.Show.Show t => GHC.Show.Show (Idris.AbsSyntaxTree.DSL' t)
instance GHC.Generics.Generic Idris.AbsSyntaxTree.OptInfo
instance GHC.Show.Show Idris.AbsSyntaxTree.OptInfo
instance GHC.Generics.Generic Idris.AbsSyntaxTree.FnInfo
instance GHC.Show.Show Idris.AbsSyntaxTree.FnInfo
instance GHC.Generics.Generic Idris.AbsSyntaxTree.TIData
instance GHC.Show.Show Idris.AbsSyntaxTree.TIData
instance GHC.Generics.Generic Idris.AbsSyntaxTree.RecordInfo
instance GHC.Show.Show Idris.AbsSyntaxTree.RecordInfo
instance GHC.Classes.Eq Idris.AbsSyntaxTree.ElabShellCmd
instance GHC.Show.Show Idris.AbsSyntaxTree.ElabShellCmd
instance GHC.Generics.Generic (Idris.AbsSyntaxTree.PData' t)
instance GHC.Base.Functor Idris.AbsSyntaxTree.PData'
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Plicity
instance Data.Data.Data Idris.AbsSyntaxTree.Plicity
instance GHC.Classes.Ord Idris.AbsSyntaxTree.Plicity
instance GHC.Classes.Eq Idris.AbsSyntaxTree.Plicity
instance GHC.Show.Show Idris.AbsSyntaxTree.Plicity
instance GHC.Generics.Generic Idris.AbsSyntaxTree.PTerm
instance Data.Data.Data Idris.AbsSyntaxTree.PTerm
instance GHC.Classes.Ord Idris.AbsSyntaxTree.PTerm
instance GHC.Classes.Eq Idris.AbsSyntaxTree.PTerm
instance GHC.Generics.Generic (Idris.AbsSyntaxTree.PArg' t)
instance Data.Data.Data t => Data.Data.Data (Idris.AbsSyntaxTree.PArg' t)
instance GHC.Base.Functor Idris.AbsSyntaxTree.PArg'
instance GHC.Classes.Ord t => GHC.Classes.Ord (Idris.AbsSyntaxTree.PArg' t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Idris.AbsSyntaxTree.PArg' t)
instance GHC.Show.Show t => GHC.Show.Show (Idris.AbsSyntaxTree.PArg' t)
instance GHC.Generics.Generic Idris.AbsSyntaxTree.ArgOpt
instance Data.Data.Data Idris.AbsSyntaxTree.ArgOpt
instance GHC.Classes.Ord Idris.AbsSyntaxTree.ArgOpt
instance GHC.Classes.Eq Idris.AbsSyntaxTree.ArgOpt
instance GHC.Show.Show Idris.AbsSyntaxTree.ArgOpt
instance GHC.Generics.Generic (Idris.AbsSyntaxTree.PDo' t)
instance Data.Data.Data t => Data.Data.Data (Idris.AbsSyntaxTree.PDo' t)
instance GHC.Base.Functor Idris.AbsSyntaxTree.PDo'
instance GHC.Classes.Ord t => GHC.Classes.Ord (Idris.AbsSyntaxTree.PDo' t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Idris.AbsSyntaxTree.PDo' t)
instance GHC.Generics.Generic (Idris.AbsSyntaxTree.PTactic' t)
instance Data.Data.Data t => Data.Data.Data (Idris.AbsSyntaxTree.PTactic' t)
instance Data.Traversable.Traversable Idris.AbsSyntaxTree.PTactic'
instance Data.Foldable.Foldable Idris.AbsSyntaxTree.PTactic'
instance GHC.Base.Functor Idris.AbsSyntaxTree.PTactic'
instance GHC.Classes.Ord t => GHC.Classes.Ord (Idris.AbsSyntaxTree.PTactic' t)
instance GHC.Classes.Eq t => GHC.Classes.Eq (Idris.AbsSyntaxTree.PTactic' t)
instance GHC.Show.Show t => GHC.Show.Show (Idris.AbsSyntaxTree.PTactic' t)
instance GHC.Generics.Generic Idris.AbsSyntaxTree.PAltType
instance Data.Data.Data Idris.AbsSyntaxTree.PAltType
instance GHC.Classes.Ord Idris.AbsSyntaxTree.PAltType
instance GHC.Classes.Eq Idris.AbsSyntaxTree.PAltType
instance GHC.Generics.Generic Idris.AbsSyntaxTree.PunInfo
instance Data.Data.Data Idris.AbsSyntaxTree.PunInfo
instance GHC.Classes.Ord Idris.AbsSyntaxTree.PunInfo
instance GHC.Show.Show Idris.AbsSyntaxTree.PunInfo
instance GHC.Classes.Eq Idris.AbsSyntaxTree.PunInfo
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Directive
instance GHC.Generics.Generic (Idris.AbsSyntaxTree.ProvideWhat' t)
instance GHC.Base.Functor Idris.AbsSyntaxTree.ProvideWhat'
instance GHC.Classes.Eq t => GHC.Classes.Eq (Idris.AbsSyntaxTree.ProvideWhat' t)
instance GHC.Show.Show t => GHC.Show.Show (Idris.AbsSyntaxTree.ProvideWhat' t)
instance GHC.Generics.Generic Idris.AbsSyntaxTree.FnOpt
instance GHC.Classes.Eq Idris.AbsSyntaxTree.FnOpt
instance GHC.Show.Show Idris.AbsSyntaxTree.FnOpt
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Static
instance Data.Data.Data Idris.AbsSyntaxTree.Static
instance GHC.Classes.Ord Idris.AbsSyntaxTree.Static
instance GHC.Classes.Eq Idris.AbsSyntaxTree.Static
instance GHC.Show.Show Idris.AbsSyntaxTree.Static
instance GHC.Generics.Generic Idris.AbsSyntaxTree.FixDecl
instance GHC.Classes.Eq Idris.AbsSyntaxTree.FixDecl
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Fixity
instance GHC.Classes.Eq Idris.AbsSyntaxTree.Fixity
instance GHC.Generics.Generic Idris.AbsSyntaxTree.CGInfo
instance GHC.Show.Show Idris.AbsSyntaxTree.CGInfo
instance GHC.Generics.Generic Idris.AbsSyntaxTree.SizeChange
instance GHC.Classes.Eq Idris.AbsSyntaxTree.SizeChange
instance GHC.Show.Show Idris.AbsSyntaxTree.SizeChange
instance GHC.Generics.Generic Idris.AbsSyntaxTree.InteractiveOpts
instance GHC.Show.Show Idris.AbsSyntaxTree.InteractiveOpts
instance GHC.Generics.Generic Idris.AbsSyntaxTree.DefaultTotality
instance GHC.Classes.Eq Idris.AbsSyntaxTree.DefaultTotality
instance GHC.Show.Show Idris.AbsSyntaxTree.DefaultTotality
instance GHC.Show.Show Idris.AbsSyntaxTree.OutputMode
instance GHC.Show.Show Idris.AbsSyntaxTree.PPOption
instance GHC.Generics.Generic Idris.AbsSyntaxTree.IOption
instance GHC.Classes.Eq Idris.AbsSyntaxTree.IOption
instance GHC.Show.Show Idris.AbsSyntaxTree.IOption
instance GHC.Classes.Eq Idris.AbsSyntaxTree.ElabWhat
instance GHC.Show.Show Idris.AbsSyntaxTree.ElabWhat
instance GHC.Show.Show Idris.AbsSyntaxTree.PClause
instance GHC.Show.Show Idris.AbsSyntaxTree.IState
instance GHC.Show.Show Idris.AbsSyntaxTree.PDecl
instance GHC.Show.Show Idris.AbsSyntaxTree.PData
instance GHC.Show.Show Idris.AbsSyntaxTree.PTerm
instance Util.Pretty.Pretty Idris.AbsSyntaxTree.PTerm Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Sized Idris.AbsSyntaxTree.PTerm
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.AbsSyntaxTree.PArg' a)
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.AbsSyntaxTree.PDo' a)
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.AbsSyntaxTree.PTactic' a)
instance GHC.Show.Show Idris.AbsSyntaxTree.FixDecl
instance GHC.Classes.Ord Idris.AbsSyntaxTree.FixDecl
instance GHC.Show.Show Idris.AbsSyntaxTree.Fixity


module Idris.DeepSeq
instance Control.DeepSeq.NFData Util.DynamicLinker.DynamicLib
instance Control.DeepSeq.NFData Idris.Colours.IdrisColour
instance Control.DeepSeq.NFData Network.Socket.Types.PortNumber
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.OutputMode
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Idris.Docstrings.Docstring a)
instance Control.DeepSeq.NFData Idris.Options.ConsoleWidth
instance Control.DeepSeq.NFData IRTS.Lang.PrimFn
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.SyntaxRules
instance Control.DeepSeq.NFData Idris.Options.Opt
instance Control.DeepSeq.NFData Idris.Options.REPLPort
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.TIData
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.IOption
instance Control.DeepSeq.NFData Idris.Options.LanguageExt
instance Control.DeepSeq.NFData Idris.Options.Optimisation
instance Control.DeepSeq.NFData Idris.Colours.ColourTheme
instance Control.DeepSeq.NFData IRTS.CodegenCommon.OutputType
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.IBCWrite
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Idris.Docstrings.Block a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Idris.Docstrings.Inline a)
instance Control.DeepSeq.NFData Idris.Docstrings.DocTerm
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.SizeChange
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.FnInfo
instance Control.DeepSeq.NFData Idris.Options.Codegen
instance Control.DeepSeq.NFData Idris.Options.IRFormat
instance Control.DeepSeq.NFData Idris.Options.LogCat
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.CGInfo
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.Fixity
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.FixDecl
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.Static
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.ArgOpt
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.Plicity
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.FnOpt
instance Control.DeepSeq.NFData Idris.Core.TT.DataOpt
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.Directive
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.AbsSyntaxTree.PDecl' t)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.AbsSyntaxTree.ProvideWhat' t)
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.PunInfo
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.AbsSyntaxTree.PClause' t)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.AbsSyntaxTree.PData' t)
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.PTerm
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.PAltType
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.AbsSyntaxTree.PTactic' t)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.AbsSyntaxTree.PDo' t)
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.AbsSyntaxTree.PArg' t)
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.InterfaceInfo
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.RecordInfo
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.OptInfo
instance Control.DeepSeq.NFData Idris.Core.TT.TypeInfo
instance Control.DeepSeq.NFData t => Control.DeepSeq.NFData (Idris.AbsSyntaxTree.DSL' t)
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.SynContext
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.Syntax
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.SSymbol
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.Using
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.SyntaxInfo
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.DefaultTotality
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.IState
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.InteractiveOpts


-- | This implements just a few basic lens-like concepts to ease state
--   updates. Similar to fclabels in approach, just without the extra
--   dependency.
--   
--   We don't include an explicit export list because everything here is
--   meant to be exported.
--   
--   Short synopsis: --------------- @ f :: Idris () f = do -- these two
--   steps: detaggable &lt;- fgetState (opt_detaggable . ist_optimisation
--   typeName) fputState (opt_detaggable . ist_optimisation typeName) (not
--   detaggable)
--   
--   <ul>
--   <li>- are equivalent to: fmodifyState (opt_detaggable .
--   ist_optimisation typeName) not</li>
--   <li>- of course, the long accessor can be put in a variable;</li>
--   <li>- everything is first-class let detag n = opt_detaggable .
--   ist_optimisation n fputState (detag n1) True fputState (detag n2)
--   False</li>
--   <li>- Note that all these operations handle missing items
--   consistently</li>
--   <li>- and transparently, as prescribed by the default values
--   included</li>
--   <li>- in the definitions of the ist_* functions.</li>
--   <li>-</li>
--   <li>- Especially, it's no longer necessary to have initial values
--   of</li>
--   <li>- data structures copied (possibly inconsistently) all over the
--   compiler. @</li>
--   </ul>
module Idris.ASTUtils
data Field rec fld
cg_usedpos :: Field CGInfo [(Int, [UsageReason])]

-- | Exact-name context lookup; uses Nothing for deleted values
--   (read+write!).
--   
--   Reading a non-existing value yields Nothing, writing Nothing deletes
--   the value (if it existed).
ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
fgetState :: MonadState s m => Field s a -> m a
fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
fputState :: MonadState s m => Field s a -> a -> m ()

-- | Fixity declarations in an IState
idris_fixities :: Field IState [FixDecl]

-- | callgraph record for the given (exact) name
ist_callgraph :: Name -> Field IState CGInfo

-- | the optimisation record for the given (exact) name
ist_optimisation :: Name -> Field IState OptInfo
known_interfaces :: Field IState (Ctxt InterfaceInfo)

-- | TT Context
--   
--   This has a terrible name, but I'm not sure of a better one that isn't
--   confusingly close to tt_ctxt
known_terms :: Field IState (Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))
opt_detaggable :: Field OptInfo Bool

-- | two fields of the optimisation record
opt_inaccessible :: Field OptInfo [(Int, Name)]
opt_forceable :: Field OptInfo [Int]

-- | Commandline flags
opts_idrisCmdline :: Field IState [Opt]

-- | Names defined at the repl
repl_definitions :: Field IState [Name]
instance Control.Category.Category Idris.ASTUtils.Field


module Util.ScreenSize
getScreenWidth :: IO Int


module Util.System

-- | Create a temp file with the extensiom ext (in the format ".xxx")
tempfile :: String -> IO (FilePath, Handle)
withTempdir :: String -> (FilePath -> IO a) -> IO a
rmFile :: FilePath -> IO ()
catchIO :: IO a -> (IOError -> IO a) -> IO a
isDarwin :: Bool
isWindows :: Bool

-- | Write a source file, same as writeFile except the encoding is set to
--   utf-8
writeSource :: FilePath -> String -> IO ()

-- | Write a utf-8 source file from Text
writeSourceText :: FilePath -> Text -> IO ()

-- | Read a source file, same as readFile but make sure the encoding is
--   utf-8.
readSource :: FilePath -> IO String

-- | Read a source file, make sure that the it all has been read before
--   exiting the function. | This is useful when we want to write the file
--   again and need it to be closed.
readSourceStrict :: FilePath -> IO String
setupBundledCC :: IO ()
isATTY :: IO Bool


module Idris.AbsSyntax
data EitherErr a b
LeftErr :: a -> EitherErr a b
RightOK :: b -> EitherErr a b
getContext :: Idris Context
forCodegen :: Codegen -> [(Codegen, a)] -> [a]
getObjectFiles :: Codegen -> Idris [FilePath]
addObjectFile :: Codegen -> FilePath -> Idris ()
getLibs :: Codegen -> Idris [String]
addLib :: Codegen -> String -> Idris ()
getFlags :: Codegen -> Idris [String]
addFlag :: Codegen -> String -> Idris ()
addDyLib :: [String] -> Idris (Either DynamicLib String)
getAutoImports :: Idris [FilePath]
addAutoImport :: FilePath -> Idris ()
addDefinedName :: Name -> Idris ()
getDefinedNames :: Idris [Name]
addTT :: Term -> Idris (Maybe Term)
dumpTT :: Idris ()
addHdr :: Codegen -> String -> Idris ()
addImported :: Bool -> FilePath -> Idris ()
addLangExt :: LanguageExt -> Idris ()
dropLangExt :: LanguageExt -> Idris ()

-- | Transforms are organised by the function being applied on the lhs of
--   the transform, to make looking up appropriate transforms quicker
addTrans :: Name -> (Term, Term) -> Idris ()

-- | Add transformation rules from a definition, which will reverse the
--   definition for an error to make it more readable
addErrRev :: (Term, Term) -> Idris ()

-- | Say that the name should always be reduced in error messages, to help
--   readability/error reflection
addErrReduce :: Name -> Idris ()
addErasureUsage :: Name -> Int -> Idris ()
addExport :: Name -> Idris ()
addUsedName :: FC -> Name -> Name -> Idris ()
getErasureUsage :: Idris [(Name, Int)]
getExports :: Idris [Name]
totcheck :: (FC, Name) -> Idris ()
defer_totcheck :: (FC, Name) -> Idris ()
clear_totcheck :: Idris ()
setFlags :: Name -> [FnOpt] -> Idris ()
addFnOpt :: Name -> FnOpt -> Idris ()
setFnInfo :: Name -> FnInfo -> Idris ()
setAccessibility :: Name -> Accessibility -> Idris ()

-- | get the accessibility of a name outside this module
getFromHideList :: Name -> Idris (Maybe Accessibility)
setTotality :: Name -> Totality -> Idris ()
setInjectivity :: Name -> Injectivity -> Idris ()
getTotality :: Name -> Idris Totality
getCoercionsTo :: IState -> Type -> [Name]
addToCG :: Name -> CGInfo -> Idris ()
addCalls :: Name -> [Name] -> Idris ()
addTyInferred :: Name -> Idris ()
addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
isTyInferred :: Name -> Idris Bool

-- | Adds error handlers for a particular function and argument. If names
--   are ambiguous, all matching handlers are updated.
addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()

-- | Trace all the names in a call graph starting at the given name
getAllNames :: Name -> Idris [Name]
getCGAllNames :: IState -> Name -> Maybe [Name]
addCGAllNames :: IState -> Name -> [Name] -> Idris ()
allNames :: [Name] -> Name -> Idris [Name]
addCoercion :: Name -> Idris ()
addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addNameHint :: Name -> Name -> Idris ()
getNameHints :: IState -> Name -> [Name]
addDeprecated :: Name -> String -> Idris ()
getDeprecated :: Name -> Idris (Maybe String)
addFragile :: Name -> String -> Idris ()
getFragile :: Name -> Idris (Maybe String)
push_estack :: Name -> Bool -> Idris ()
pop_estack :: Idris ()

-- | Add an interface implementation function.
--   
--   Precondition: the implementation should have the correct type.
--   
--   Dodgy hack 1: Put integer implementations first in the list so they
--   are resolved by default.
--   
--   Dodgy hack 2: put constraint chasers (ParentN) last
addImplementation :: Bool -> Bool -> Name -> Name -> Idris ()

-- | Add a privileged implementation - one which implementation search will
--   happily resolve immediately if it is type correct This is used for
--   naming parent implementations when defining an implementation with
--   constraints. Returns the old list, so we can revert easily at the end
--   of a block
addOpenImpl :: [Name] -> Idris [Name]
setOpenImpl :: [Name] -> Idris ()
getOpenImpl :: Idris [Name]
addInterface :: Name -> InterfaceInfo -> Idris ()
updateIMethods :: Name -> [(Name, PTerm)] -> Idris ()
addRecord :: Name -> RecordInfo -> Idris ()
addAutoHint :: Name -> Name -> Idris ()
getAutoHints :: Name -> Idris [Name]
addIBC :: IBCWrite -> Idris ()
clearIBC :: Idris ()
resetNameIdx :: Idris ()

-- | Used to preserve sharing of names
addNameIdx :: Name -> Idris (Int, Name)
addNameIdx' :: IState -> Name -> (IState, (Int, Name))
getSymbol :: Name -> Idris Name
getHdrs :: Codegen -> Idris [String]
getImported :: Idris [(FilePath, Bool)]
setErrSpan :: FC -> Idris ()
clearErr :: Idris ()
getSO :: Idris (Maybe String)
setSO :: Maybe String -> Idris ()
getIState :: Idris IState
putIState :: IState -> Idris ()
updateIState :: (IState -> IState) -> Idris ()
withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()

-- | A version of liftIO that puts errors into the exception type of the
--   Idris monad
runIO :: IO a -> Idris a
getName :: Idris Int

-- | InternalApp keeps track of the real function application for making
--   case splits from, not the application the programmer wrote, which
--   doesn't have the whole context in any case other than top level
--   definitions
addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
getInternalApp :: FilePath -> Int -> Idris PTerm

-- | Pattern definitions are only used for coverage checking, so erase them
--   when we're done
clearOrigPats :: Idris ()

-- | Erase types from Ps in the context (basically ending up with what's in
--   the .ibc, which is all we need after all the analysis is done)
clearPTypes :: Idris ()
checkUndefined :: FC -> Name -> Idris ()
isUndefined :: FC -> Name -> Idris Bool
setContext :: Context -> Idris ()
updateContext :: (Context -> Context) -> Idris ()
addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
addDeferred :: [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
addDeferredTyCon :: [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()

-- | Save information about a name that is not yet defined
addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
solveDeferred :: FC -> Name -> Idris ()
getUndefined :: Idris [Name]
isMetavarName :: Name -> IState -> Bool
getWidth :: Idris ConsoleWidth
setWidth :: ConsoleWidth -> Idris ()
setDepth :: Maybe Int -> Idris ()
typeDescription :: String
type1Doc :: Doc OutputAnnotation
isetPrompt :: String -> Idris ()

-- | Tell clients how much was parsed and loaded
isetLoadedRegion :: Idris ()
setLogLevel :: Int -> Idris ()
setLogCats :: [LogCat] -> Idris ()
setCmdLine :: [Opt] -> Idris ()
getCmdLine :: Idris [Opt]
getDumpHighlighting :: Idris Bool
getDumpDefun :: Idris (Maybe FilePath)
getDumpCases :: Idris (Maybe FilePath)
logLevel :: Idris Int
setAutoImpls :: Bool -> Idris ()
getAutoImpls :: Idris Bool
setErrContext :: Bool -> Idris ()
errContext :: Idris Bool
getOptimise :: Idris [Optimisation]
setOptimise :: [Optimisation] -> Idris ()
addOptimise :: Optimisation -> Idris ()
removeOptimise :: Optimisation -> Idris ()

-- | Set appropriate optimisation set for the given level. We only have one
--   optimisation that is configurable at the moment, however!
setOptLevel :: Int -> Idris ()
useREPL :: Idris Bool
setREPL :: Bool -> Idris ()
showOrigErr :: Idris Bool
setShowOrigErr :: Bool -> Idris ()
setAutoSolve :: Bool -> Idris ()
setNoBanner :: Bool -> Idris ()
getNoBanner :: Idris Bool
setEvalTypes :: Bool -> Idris ()
getDesugarNats :: Idris Bool
setDesugarNats :: Bool -> Idris ()
setQuiet :: Bool -> Idris ()
getQuiet :: Idris Bool
setCodegen :: Codegen -> Idris ()
codegen :: Idris Codegen
setOutputTy :: OutputType -> Idris ()
outputTy :: Idris OutputType
setIdeMode :: Bool -> Handle -> Idris ()
setTargetTriple :: String -> Idris ()
targetTriple :: Idris String
setTargetCPU :: String -> Idris ()
targetCPU :: Idris String
verbose :: Idris Int
setVerbose :: Int -> Idris ()
iReport :: Int -> String -> Idris ()
typeInType :: Idris Bool
setTypeInType :: Bool -> Idris ()
coverage :: Idris Bool
setCoverage :: Bool -> Idris ()
setIBCSubDir :: FilePath -> Idris ()
valIBCSubDir :: IState -> Idris FilePath
addImportDir :: FilePath -> Idris ()
setImportDirs :: [FilePath] -> Idris ()
allImportDirs :: Idris [FilePath]
rankedImportDirs :: FilePath -> Idris [FilePath]
addSourceDir :: FilePath -> Idris ()
setSourceDirs :: [FilePath] -> Idris ()
allSourceDirs :: Idris [FilePath]
colourise :: Idris Bool
setColourise :: Bool -> Idris ()
impShow :: Idris Bool
setImpShow :: Bool -> Idris ()
setColour :: ColourType -> IdrisColour -> Idris ()
logLvl :: Int -> String -> Idris ()
logCoverage :: Int -> String -> Idris ()
logErasure :: Int -> String -> Idris ()

-- | Log an action of the parser
logParser :: Int -> String -> Idris ()

-- | Log an action of the elaborator.
logElab :: Int -> String -> Idris ()

-- | Log an action of the compiler.
logCodeGen :: Int -> String -> Idris ()
logIBC :: Int -> String -> Idris ()

-- | Log aspect of Idris execution
--   
--   An empty set of logging levels is used to denote all categories.
--   
--   @TODO update IDE protocol
logLvlCats :: [LogCat] -> Int -> String -> Idris ()
cmdOptType :: Opt -> Idris Bool
noErrors :: Idris Bool
setTypeCase :: Bool -> Idris ()
getIndentWith :: Idris Int
setIndentWith :: Int -> Idris ()
getIndentClause :: Idris Int
setIndentClause :: Int -> Idris ()
expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTerm
expandParamsD :: Bool -> IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
mapsnd :: () => (t -> b) -> (a, t) -> (a, b)
expandImplementationScope :: () => p1 -> p2 -> [(Name, t)] -> p3 -> PDecl' t -> PDecl' t

-- | Calculate a priority for a type, for deciding elaboration order * if
--   it's just a type variable or concrete type, do it early (0) * if
--   there's only type variables and injective constructors, do it next (1)
--   * if there's a function type, next (2) * finally, everything else (3)
getPriority :: IState -> PTerm -> Int
addStatics :: Name -> Term -> PTerm -> Idris ()
addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm

-- | Add implicit bindings from using block, and bind any missing names
addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm

-- | Even if auto_implicits is off, we need to call this so we record which
--   arguments are implicit
implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])

-- | Add implicit arguments in function calls
addImplPat :: IState -> PTerm -> PTerm
addImplBound :: IState -> [Name] -> PTerm -> PTerm
addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm

-- | Add the implicit arguments to applications in the term [Name] gives
--   the names to always expend, even when under a binder of that name
--   (this is to expand methods with implicit arguments in dependent
--   interfaces).
addImpl :: [Name] -> IState -> PTerm -> PTerm
addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
aiFn :: Name -> Bool -> Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> FC -> [[Text]] -> [PArg] -> Either Err PTerm

-- | return True if the second argument is an implicit argument which is
--   expected in the implicits, or if it's not an implicit
impIn :: [PArg] -> PArg -> Bool
expArg :: () => PArg' t -> Bool
stripLinear :: IState -> PTerm -> PTerm

-- | Remove functions which aren't applied to anything, which must then be
--   resolved by unification. Assume names resolved and alternatives filled
--   in (so no ambiguity).
stripUnmatchable :: IState -> PTerm -> PTerm
mkPApp :: FC -> Int -> PTerm -> [PArg] -> PTerm

-- | Find <tt>static</tt> argument positions (the declared ones, plus any
--   names in argument position in the declared statics) FIXME: It's
--   possible that this really has to happen after elaboration
findStatics :: IState -> PTerm -> (PTerm, [Bool])
toEither :: EitherErr a b -> Either a b

-- | Syntactic match of a against b, returning pair of variables in a and
--   what they match. Returns the pair that failed if not a match.
matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
substMatch :: Name -> PTerm -> PTerm -> PTerm
substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
shadow :: Name -> Name -> PTerm -> PTerm

-- | Rename any binders which are repeated (so that we don't have to mess
--   about with shadowing anywhere else).
mkUniqueNames :: [Name] -> [(Name, Name)] -> PTerm -> PTerm
instance GHC.Base.Functor (Idris.AbsSyntax.EitherErr a)
instance GHC.Base.Applicative (Idris.AbsSyntax.EitherErr a)
instance GHC.Base.Monad (Idris.AbsSyntax.EitherErr a)


module Idris.WhoCalls
whoCalls :: Name -> Idris [(Name, [Name])]
callsWho :: Name -> Idris [(Name, [Name])]


module Idris.Transforms
transformPats :: IState -> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
transformPatsWith :: [(Term, Term)] -> [Either Term (Term, Term)] -> [Either Term (Term, Term)]

-- | Work on explicitly named terms, so we don't have to manipulate de
--   Bruijn indices
applyTransRulesWith :: [(Term, Term)] -> Term -> Term

-- | Work on explicitly named terms, so we don't have to manipulate de
--   Bruijn indices
applyTransRules :: IState -> Term -> Term


module Idris.REPL.Browse

-- | Find the sub-namespaces of a given namespace. The components should be
--   in display order rather than the order that they are in inside of NS
--   constructors.
namespacesInNS :: [String] -> Idris [[String]]

-- | Find the user-accessible names that occur directly within a given
--   namespace. The components should be in display order rather than the
--   order that they are in inside of NS constructors.
namesInNS :: [String] -> Idris [Name]


module Idris.Inliner
inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]

-- | Inlining is either top level (i.e. not in a function arg) or argument
--   level
--   
--   For each application in a term: * Check if the function is inlinable
--   (Dictionaries are inlinable in an argument, not otherwise) - If so,
--   try inlining without reducing its arguments + If successful, then
--   continue on the result (top level) + If not, reduce the arguments
--   (argument level) and try again - If not, inline all the arguments (top
--   level)
inlineTerm :: IState -> Term -> Term


module Idris.ErrReverse

-- | For display purposes, apply any 'error reversal' transformations so
--   that errors will be more readable, and any 'error reduce'
--   transformations
errReverse :: IState -> Term -> Term


module Idris.Elab.Quasiquote
extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])


module Idris.Elab.AsPat

-- | Desugar by changing x@y on lhs to let x = y in ... or rhs
desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])


module Idris.Delaborate
annName :: Name -> Doc OutputAnnotation
bugaddr :: [Char]

-- | Delaborate a term without resugaring
delab :: IState -> Term -> PTerm
delabWithEnv :: IState -> [(Name, Type)] -> Term -> PTerm

-- | Delaborate a term directly, leaving case applications as they are. We
--   need this for interactive case splitting, where we need access to the
--   underlying function in a delaborated form, to generate the right
--   patterns
delabDirect :: IState -> Term -> PTerm
delab' :: IState -> Term -> Bool -> Bool -> PTerm
delabMV :: IState -> Term -> PTerm

-- | Delaborate and resugar a term
delabSugared :: IState -> Term -> PTerm
delabTy :: IState -> Name -> PTerm
delabTy' :: IState -> [PArg] -> [(Name, Type)] -> Term -> Bool -> Bool -> Bool -> PTerm

-- | Add extra metadata to an output annotation, optionally marking
--   metavariables.
fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation

-- | Pretty-print a core term using delaboration
pprintDelab :: IState -> Term -> Doc OutputAnnotation
pprintNoDelab :: IState -> Term -> Doc OutputAnnotation

-- | Pretty-print the type of some name
pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
pprintErr :: IState -> Err -> Doc OutputAnnotation

-- | Re-add syntactic sugar in a term
resugar :: IState -> PTerm -> PTerm


module Idris.Reflection
data RConstructorDefn
RConstructor :: Name -> [RFunArg] -> Raw -> RConstructorDefn
data RDataDefn
RDefineDatatype :: Name -> [RConstructorDefn] -> RDataDefn
data RFunArg
RFunArg :: Name -> Raw -> RPlicity -> RErasure -> RFunArg
[argName] :: RFunArg -> Name
[argTy] :: RFunArg -> Raw
[argPlicity] :: RFunArg -> RPlicity
[erasure] :: RFunArg -> RErasure
data RFunClause a
RMkFunClause :: a -> a -> RFunClause a
RMkImpossibleClause :: a -> RFunClause a
data RFunDefn a
RDefineFun :: Name -> [RFunClause a] -> RFunDefn a
data RTyDecl
RDeclare :: Name -> [RFunArg] -> Raw -> RTyDecl

-- | Build the reflected datatype definition(s) that correspond(s) to a
--   provided unqualified name
buildDatatypes :: IState -> Name -> [RDatatype]

-- | Build the reflected function definition(s) that correspond(s) to a
--   provided unqualifed name
buildFunDefns :: IState -> Name -> [RFunDefn Term]
envTupleType :: Raw
fromTTMaybe :: Term -> Maybe Term

-- | Apply Idris's implicit info to get a signature. The [PArg] should come
--   from a lookup in idris_implicits on IState.
getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
mkList :: Raw -> [Raw] -> Raw
rawList :: Raw -> [Raw] -> Raw
rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
rawPairTy :: Raw -> Raw -> Raw

-- | Lift a term into its Language.Reflection.TT representation
reflect :: Term -> Raw
reflectArg :: RFunArg -> Raw
reflectDatatype :: RDatatype -> Raw

-- | Reflect the environment of a proof into a List (TTName, Binder TT)
reflectEnv :: Env -> Raw
reflectErr :: Err -> Raw

-- | Reflect a file context
reflectFC :: FC -> Raw
reflectFixity :: Fixity -> Raw
reflectFunDefn :: RFunDefn Term -> Raw
reflectList :: Raw -> [Raw] -> Raw
reflectName :: Name -> Raw
reflectNameType :: NameType -> Raw

-- | Lift a term into its Language.Reflection.Raw representation
reflectRaw :: Raw -> Raw
reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
reflectRawQuote :: [Name] -> Raw -> Raw

-- | Create a reflected TT term, but leave refs to the provided name intact
reflectTTQuote :: [Name] -> Term -> Raw

-- | Convert a reflected term to a more suitable form for pattern-matching.
--   In particular, the less-interesting bits are elaborated to _ patterns.
--   This happens to NameTypes, universe levels, names that are bound but
--   not used, and the type annotation field of the P constructor.
reflectTTQuotePattern :: [Name] -> Term -> ElabD ()

-- | Prefix a name with the <a>Language.Reflection</a> namespace
reflm :: String -> Name

-- | Reify tactics from their reflected representation
reify :: IState -> Term -> ElabD PTactic
reifyBool :: Term -> ElabD Bool
reifyEnv :: Term -> ElabD Env
reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]
reifyRDataDefn :: Term -> ElabD RDataDefn

-- | Reify raw terms from their reflected representation
reifyRaw :: Term -> ElabD Raw

-- | Attempt to reify a report part from TT to the internal representation.
--   Not in Idris or ElabD monads because it should be usable from either.
reifyReportPart :: Term -> Either Err ErrorReportPart
reifyReportParts :: Term -> ElabD [ErrorReportPart]

-- | Reify terms from their reflected representation
reifyTT :: Term -> ElabD Term
reifyTTName :: Term -> ElabD Name
reifyTyDecl :: Term -> ElabD RTyDecl
rFunArgToPArg :: RFunArg -> PArg

-- | Prefix a name with the <a>Language.Reflection.Elab</a> namespace
tacN :: String -> Name
instance GHC.Show.Show a => GHC.Show.Show (Idris.Reflection.RFunDefn a)
instance GHC.Show.Show a => GHC.Show.Show (Idris.Reflection.RFunClause a)
instance GHC.Show.Show Idris.Reflection.RDatatype
instance GHC.Show.Show Idris.Reflection.RCtorArg
instance GHC.Show.Show Idris.Reflection.RTyConArg
instance GHC.Show.Show Idris.Reflection.RTyDecl
instance GHC.Show.Show Idris.Reflection.RFunArg
instance GHC.Show.Show Idris.Reflection.RPlicity
instance GHC.Show.Show Idris.Reflection.RErasure


module Idris.ProofSearch
trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialHoles :: [Name] -> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
proofSearch :: Bool -> Bool -> Bool -> Bool -> Int -> (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] -> [Name] -> IState -> ElabD ()

-- | Resolve interfaces. This will only pick up <tt>normal</tt>
--   implementations, never named implementations (which is enforced by
--   <a>findImplementations</a>).
resolveTC :: Bool -> Bool -> Int -> Term -> Name -> (PTerm -> ElabD ()) -> IState -> ElabD ()


module Idris.PartialEval

-- | Partially evaluates given terms under the given context. It is an
--   error if partial evaluation fails to make any progress. Making
--   progress is defined as: all of the names given with explicit reduction
--   limits (in practice, the function being specialised) must have reduced
--   at least once. If we don't do this, we might end up making an infinite
--   function after applying the transformation.
partial_eval :: Context -> [(Name, Maybe Int)] -> [Either Term (Term, Term)] -> Maybe [Either Term (Term, Term)]

-- | Get specialised applications for a given function
getSpecApps :: IState -> [Name] -> Term -> [(Name, [(PEArgType, Term)])]

-- | Specialises the type of a partially evaluated TT function returning a
--   pair of the specialised type and the types of expected arguments.
specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])

-- | Creates an Idris type declaration given current state and a
--   specialised TT function application type. Can be used in combination
--   with the output of <a>specType</a>.
--   
--   This should: specialise any static argument position, then generalise
--   over any function applications in the result.
mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

-- | Creates a new declaration for a specialised function application.
--   Simple version at the moment: just create a version which is a direct
--   application of the function to be specialised. More complex version to
--   do: specialise the definition clause by clause
mkPE_TermDecl :: IState -> Name -> Name -> PTerm -> [(PEArgType, Term)] -> PEDecl

-- | Data type representing binding-time annotations for partial evaluation
--   of arguments
data PEArgType

-- | Implicit static argument
ImplicitS :: Name -> PEArgType

-- | Implicit dynamic argument
ImplicitD :: Name -> PEArgType

-- | Implementation constraint
ConstraintS :: PEArgType

-- | Implementation constraint
ConstraintD :: PEArgType

-- | Explicit static argument
ExplicitS :: PEArgType

-- | Explicit dynamic argument
ExplicitD :: PEArgType

-- | Erasable dynamic argument (found under unification)
UnifiedD :: PEArgType
pe_app :: PEDecl -> PTerm
pe_def :: PEDecl -> PTerm
pe_clauses :: PEDecl -> [(PTerm, PTerm)]
pe_simple :: PEDecl -> Bool
instance GHC.Show.Show Idris.PartialEval.PEArgType
instance GHC.Classes.Eq Idris.PartialEval.PEArgType


module Idris.Output
clearHighlights :: Idris ()
emitWarning :: Message w => w -> Idris ()
formatMessage :: Message w => w -> Idris OutputDoc
idemodePutSExp :: SExpable a => String -> a -> Idris ()
iPrintError :: String -> Idris ()

-- | Pretty-print a collection of overloadings to REPL or IDEMode -
--   corresponds to :t name
iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
iPrintResult :: String -> Idris ()
iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
iputStr :: String -> Idris ()
iputStrLn :: String -> Idris ()
iRender :: Doc a -> Idris (SimpleDoc a)

-- | Show an error with semantic highlighting
iRenderError :: Doc OutputAnnotation -> Idris ()
iRenderOutput :: Doc OutputAnnotation -> Idris ()
iRenderResult :: Doc OutputAnnotation -> Idris ()
iWarn :: FC -> OutputDoc -> Idris ()
prettyDocumentedIst :: IState -> (Name, PTerm, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation
printUndefinedNames :: [Name] -> Doc OutputAnnotation
pshow :: IState -> Err -> String
renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
sendHighlighting :: Set (FC', OutputAnnotation) -> Idris ()
sendParserHighlighting :: Idris ()

-- | Warn about totality problems without failing to compile
warnTotality :: Idris ()

-- | Write the highlighting information to a file, for use in external
--   tools or in editors that don't support the IDE protocol
writeHighlights :: FilePath -> Idris ()
type OutputDoc = Doc OutputAnnotation
class Message a
messageExtent :: Message a => a -> FC
messageText :: Message a => a -> OutputDoc
messageSource :: Message a => a -> Maybe String
instance Idris.Output.Message Idris.Output.SimpleWarning
instance System.Console.Haskeline.MonadException.MonadException m => System.Console.Haskeline.MonadException.MonadException (Control.Monad.Trans.Except.ExceptT Idris.Core.TT.Err m)


module Idris.Parser.Stack

-- | Our parser stack with state of type <tt>s</tt>
type Parser s = StateT s (WriterT FC (Parsec Void String))

-- | A constraint for parsing without state
type Parsing m = (MonadParsec Void String m, MonadWriter FC m)

-- | Run the Idris parser stack
runparser :: Parser st res -> st -> String -> String -> Either ParseError res
data ParseError

-- | A fully formatted parse error, with caret and bar, etc.
prettyError :: ParseError -> String
type Mark = State String

-- | Retrieve the parser state so we can restart from this point later.
mark :: Parsing m => m Mark
restore :: Parsing m => Mark -> m ()

-- | Get the current parse position.
--   
--   This is useful when the position is needed in a way unrelated to the
--   heirarchy of parsers. Prefer using <tt>withExtent</tt> and friends.
getFC :: Parsing m => m FC

-- | Add an extent (widen) our current parsing context.
addExtent :: MonadWriter FC m => FC -> m ()

-- | Run a parser and track its extent.
--   
--   Wrap bare Megaparsec parsers with this to make them "visible" in error
--   messages. Do not wrap whitespace or comment parsers. If you find an
--   extent is taking trailing whitespace, it's likely there's a
--   double-wrapped parser (usually via
--   <tt>Idris.Parser.Helpers.token</tt>).
trackExtent :: Parsing m => m a -> m a

-- | Run a parser, discard its value, and return its extent.
extent :: MonadWriter FC m => m a -> m FC

-- | Run a parser and return its value and extent.
withExtent :: MonadWriter FC m => m a -> m (a, FC)

-- | Run a parser and inject the extent after via function application.
appExtent :: MonadWriter FC m => m (FC -> a) -> m a
instance Idris.Output.Message Idris.Parser.Stack.ParseError


module Idris.Parser.Helpers

-- | Idris parser with state used during parsing
type IdrisParser = Parser IState
parseErrorDoc :: ParseError -> Doc

-- | Parses some white space
whiteSpace :: Parsing m => m ()
someSpace :: Parsing m => m ()

-- | A parser that succeeds at the end of the line
eol :: Parsing m => m ()

-- | Checks if a charcter is end of line
isEol :: Char -> Bool
char :: Parsing m => Char -> m Char
symbol :: Parsing m => String -> m ()
string :: Parsing m => String -> m String

-- | Checks if the following character matches provided parser
lookAheadMatches :: Parsing m => m a -> m Bool

-- | Parses a character as a token
lchar :: Parsing m => Char -> m Char

-- | Parses a reserved identifier
reserved :: Parsing m => String -> m ()

-- | Parses a documentation comment
--   
--   <pre>
--   DocComment_t ::= DocCommentLine (ArgCommentLine DocCommentLine*)* ;
--   
--   DocCommentLine ::= <tt>|||</tt> ~EOL_t* EOL_t ;
--   ArgCommentLine ::= <tt>|||</tt> '@' ~EOL_t* EOL_t ;
--   </pre>
docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])
token :: Parsing m => m a -> m a

-- | Parses a natural number
natural :: Parsing m => m Integer

-- | Parses a char literal
charLiteral :: Parsing m => m Char

-- | Parses a string literal
stringLiteral :: Parsing m => m String

-- | Parses a floating point number
float :: Parsing m => m Double

-- | Bind constraints to term
bindList :: (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm) -> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm

-- | Parses an string possibly prefixed by a namespace
maybeWithNS :: Parsing m => m String -> [String] -> m Name

-- | Parses an identifier with possible namespace as a name
iName :: Parsing m => [String] -> m Name

-- | Parses a name
name :: (Parsing m, MonadState IState m) => m Name
identifier :: Parsing m => m String

-- | Parses an identifier as a token
identifierWithExtraChars :: Parsing m => String -> m String

-- | Parse a package name
packageName :: Parsing m => m String
accessibility :: IdrisParser Accessibility

-- | Add accessbility option for data declarations (works for interfaces
--   too - <tt>abstract</tt> means the data/interface is visible but
--   members not)
accData :: Accessibility -> Name -> [Name] -> IdrisParser ()

-- | Adds accessibility option for function
addAcc :: Name -> Accessibility -> IdrisParser ()

-- | Error message with possible fixes list
fixErrorMsg :: String -> [String] -> String
parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()
clearParserWarnings :: Idris ()
reportParserWarnings :: Idris ()
highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a

-- | Parse a reserved identfier, highlighting it as a keyword
keyword :: (Parsing m, MonadState IState m) => String -> m ()

-- | Push indentation to stack
pushIndent :: IdrisParser ()

-- | Pops indentation from stack
popIndent :: IdrisParser ()
indentGt :: (Parsing m, MonadState IState m) => m ()

-- | Checks that there are no braces that are not closed
notOpenBraces :: IdrisParser ()

-- | Parses a start of block
openBlock :: IdrisParser ()

-- | Parses an end of block
closeBlock :: IdrisParser ()

-- | Parses a terminator
terminator :: IdrisParser ()

-- | Checks that it is not end of block
notEndBlock :: IdrisParser ()

-- | Applies parser to get a block (which has possibly indented statements)
indentedBlock :: IdrisParser a -> IdrisParser [a]

-- | Applies parser to get a block with at least one statement (which has
--   possibly indented statements)
indentedBlock1 :: IdrisParser a -> IdrisParser [a]

-- | Applies parser to get a block with exactly one (possibly indented)
--   statement
indentedBlockS :: IdrisParser a -> IdrisParser a

-- | Applies parser in an indented position
indented :: IdrisParser a -> IdrisParser a

-- | Checks if application expression does not end
notEndApp :: IdrisParser ()

-- | <tt>commaSeparated p</tt> parses one or more occurences of <tt>p</tt>,
--   separated by commas and optional whitespace.
commaSeparated :: Parsing m => m a -> m [a]


module Idris.Parser.Ops

-- | Creates table for fixity declarations to build expression parser using
--   pre-build and user-defined operator/fixity declarations
table :: [FixDecl] -> [[Operator IdrisParser PTerm]]

-- | Parses a function used as an operator -- enclosed in backticks
--   
--   <pre>
--   BacktickOperator ::=
--     '`' Name '`'
--     ;
--   </pre>
backtickOperator :: (Parsing m, MonadState IState m) => m Name

-- | Parses an operator name (either a symbolic name or a backtick-quoted
--   name)
--   
--   <pre>
--   OperatorName ::=
--       SymbolicOperator
--     | BacktickOperator
--     ;
--   </pre>
operatorName :: (Parsing m, MonadState IState m) => m Name

-- | Parses an operator in function position i.e. enclosed by `()', with an
--   optional namespace
--   
--   <pre>
--   OperatorFront ::=
--     '(' '=' ')'
--     | (Identifier_t <a>.</a>)? '(' Operator_t ')'
--     ;
--   </pre>
operatorFront :: Parsing m => m Name

-- | Parses a function (either normal name or operator)
--   
--   <pre>
--   FnName ::= Name | OperatorFront;
--   </pre>
fnName :: (Parsing m, MonadState IState m) => m Name

-- | Parses a fixity declaration <tt> Fixity ::= FixityType Natural_t
--   OperatorList Terminator ; </tt>
fixity :: IdrisParser PDecl

-- | Check that a declaration of an operator also has fixity declared
checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl

-- | Checks that an operator name also has a fixity declaration
checkNameFixity :: Name -> IdrisParser ()

-- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
--   <tt> FixityType ::= 'infixl' | 'infixr' | 'infix' | <tt>prefix</tt> ;
--   </tt>
fixityType :: IdrisParser (Int -> Fixity)
opChars :: String
operatorLetter :: Parsing m => m Char
commentMarkers :: [String]
invalidOperators :: [String]

-- | Parses an operator
symbolicOperator :: Parsing m => m String

-- | Parses a reserved operator
reservedOp :: Parsing m => String -> m ()


module Idris.Error
getErrSpan :: Err -> FC
idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
ierror :: Err -> Idris a
ifail :: String -> Idris a
iucheck :: Idris ()
report :: IOError -> String
setAndReport :: Err -> Idris ()
showErr :: Err -> Idris String
tclift :: TC a -> Idris a
tcliftAt :: FC -> TC a -> Idris a
tctry :: TC a -> TC a -> Idris a

-- | Issue a warning on "with"-terms whose namespace is empty or
--   nonexistent
warnDisamb :: IState -> PTerm -> Idris ()


module Idris.Termination

-- | Calculate the size change graph for this definition
--   
--   SCG for a function f consists of a list of: (g, [(a1, sizechange1),
--   (a2, sizechange2), ..., (an, sizechangen)])
--   
--   where g is a function called a1 ... an are the arguments of f in
--   positions 1..n of g sizechange1 ... sizechange2 is how their size has
--   changed wrt the input to f Nothing, if the argument is unrelated to
--   the input
buildSCG :: (FC, Name) -> Idris ()

-- | Check whether function and all descendants cover all cases (partial is
--   okay, as long as it's due to recursion)
checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
checkDeclTotality :: (FC, Name) -> Idris Totality

-- | Check whether all <tt>Inf</tt> arguments to the name end up guaranteed
--   to be guarded by constructors (conservatively... maybe this can do
--   better later). Essentially, all it does is check that every branch is
--   a constructor application with no other function applications.
--   
--   If so, set the <a>AllGuarded</a> flag which can be used by the
--   productivity check
checkIfGuarded :: Name -> Idris ()

-- | Check if, in a given group of type declarations mut_ns, the
--   constructor cn : ty is strictly positive, and update the context
--   accordingly
checkPositive :: [Name] -> (Name, Type) -> Idris Totality
checkSizeChange :: Name -> Idris Totality
verifyTotality :: (FC, Name) -> Idris ()
instance GHC.Show.Show Idris.Termination.Guardedness


module Idris.Providers

-- | Wrap a type provider in the type of type providers
providerTy :: FC -> PTerm -> PTerm

-- | Handle an error, if the type provider returned an error. Otherwise
--   return the provided term.
getProvided :: FC -> TT Name -> Idris (Provided (TT Name))
data Provided a
Provide :: a -> Provided a
instance GHC.Base.Functor Idris.Providers.Provided
instance GHC.Classes.Eq a => GHC.Classes.Eq (Idris.Providers.Provided a)
instance GHC.Show.Show a => GHC.Show.Show (Idris.Providers.Provided a)


module Idris.Imports
data IFileType
IDR :: FilePath -> IFileType
LIDR :: FilePath -> IFileType
IBC :: FilePath -> IFileType -> IFileType
findIBC :: [FilePath] -> FilePath -> FilePath -> Idris (Maybe FilePath)
findImport :: [FilePath] -> FilePath -> FilePath -> Idris IFileType
findInPath :: [FilePath] -> FilePath -> IO FilePath
findPkgIndex :: PkgName -> Idris FilePath
ibcPathNoFallback :: FilePath -> FilePath -> FilePath
installedPackages :: IO [String]

-- | Get the index file name for a package name
pkgIndex :: PkgName -> FilePath
data PkgName
pkgName :: String -> Either String PkgName
unPkgName :: PkgName -> String
unInitializedPkgName :: PkgName
instance GHC.Classes.Ord Idris.Imports.IFileType
instance GHC.Show.Show Idris.Imports.IFileType
instance GHC.Show.Show Idris.Imports.PkgName
instance GHC.Classes.Eq Idris.Imports.PkgName
instance GHC.Classes.Eq Idris.Imports.IFileType

module Idris.REPL.Commands

-- | REPL commands
data Command
Quit :: Command
Help :: Command
Eval :: PTerm -> Command

-- | Each <a>PDecl</a> should be either a type declaration (at most one) or
--   a clause defining the same name.
NewDefn :: [PDecl] -> Command
Undefine :: [Name] -> Command
Check :: PTerm -> Command
Core :: PTerm -> Command
DocStr :: Either Name Const -> HowMuchDocs -> Command
TotCheck :: Name -> Command
Reload :: Command
Watch :: Command
Load :: FilePath -> Maybe Int -> Command
RunShellCommand :: FilePath -> Command
ChangeDirectory :: FilePath -> Command
ModImport :: String -> Command
Edit :: Command
Compile :: Codegen -> String -> Command
Execute :: PTerm -> Command
ExecVal :: PTerm -> Command
Metavars :: Command

-- | If false, use prover, if true, use elab shell
Prove :: Bool -> Name -> Command
AddProof :: Maybe Name -> Command
RmProof :: Name -> Command
ShowProof :: Name -> Command
Proofs :: Command
Universes :: Command
LogLvl :: Int -> Command
LogCategory :: [LogCat] -> Command
Verbosity :: Int -> Command
Spec :: PTerm -> Command
WHNF :: PTerm -> Command
TestInline :: PTerm -> Command
Defn :: Name -> Command
Missing :: Name -> Command
DynamicLink :: FilePath -> Command
ListDynamic :: Command
Pattelab :: PTerm -> Command
Search :: [PkgName] -> PTerm -> Command
CaseSplitAt :: Bool -> Int -> Name -> Command
AddClauseFrom :: Bool -> Int -> Name -> Command
AddProofClauseFrom :: Bool -> Int -> Name -> Command
AddMissing :: Bool -> Int -> Name -> Command
MakeWith :: Bool -> Int -> Name -> Command
MakeCase :: Bool -> Int -> Name -> Command
MakeLemma :: Bool -> Int -> Name -> Command
DoProofSearch :: Bool -> Bool -> Int -> Name -> [Name] -> Command
SetOpt :: Opt -> Command
UnsetOpt :: Opt -> Command
NOP :: Command
SetColour :: ColourType -> IdrisColour -> Command
ColourOn :: Command
ColourOff :: Command
ListErrorHandlers :: Command
SetConsoleWidth :: ConsoleWidth -> Command
SetPrinterDepth :: Maybe Int -> Command
Apropos :: [PkgName] -> String -> Command
WhoCalls :: Name -> Command
CallsWho :: Name -> Command
Browse :: [String] -> Command
MakeDoc :: String -> Command
ShowVersion :: Command
Warranty :: Command
PrintDef :: Name -> Command
PPrint :: OutputFmt -> Int -> PTerm -> Command
TransformInfo :: Name -> Command
DebugInfo :: Name -> Command
DebugUnify :: PTerm -> PTerm -> Command


module Idris.Package.Common

-- | Description of an Idris package.
data PkgDesc
PkgDesc :: PkgName -> [PkgName] -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> Maybe String -> [String] -> [String] -> Maybe String -> [Opt] -> String -> [Name] -> Maybe Name -> Maybe String -> [Name] -> PkgDesc

-- | Name associated with a package.
[pkgname] :: PkgDesc -> PkgName

-- | List of packages this package depends on.
[pkgdeps] :: PkgDesc -> [PkgName]

-- | Brief description of the package.
[pkgbrief] :: PkgDesc -> Maybe String

-- | Version string to associate with the package.
[pkgversion] :: PkgDesc -> Maybe String

-- | Location of the README file.
[pkgreadme] :: PkgDesc -> Maybe String

-- | Description of the licensing information.
[pkglicense] :: PkgDesc -> Maybe String

-- | Author information.
[pkgauthor] :: PkgDesc -> Maybe String

-- | Maintainer information.
[pkgmaintainer] :: PkgDesc -> Maybe String

-- | Website associated with the package.
[pkghomepage] :: PkgDesc -> Maybe String

-- | Location of the source files.
[pkgsourceloc] :: PkgDesc -> Maybe String

-- | Location of the project's bug tracker.
[pkgbugtracker] :: PkgDesc -> Maybe String

-- | External dependencies.
[libdeps] :: PkgDesc -> [String]

-- | Object files required by the package.
[objs] :: PkgDesc -> [String]

-- | Makefile used to build external code. Used as part of the FFI process.
[makefile] :: PkgDesc -> Maybe String

-- | List of options to give the compiler.
[idris_opts] :: PkgDesc -> [Opt]

-- | Source directory for Idris files.
[sourcedir] :: PkgDesc -> String

-- | Modules provided by the package.
[modules] :: PkgDesc -> [Name]

-- | If an executable in which module can the Main namespace and function
--   be found.
[idris_main] :: PkgDesc -> Maybe Name

-- | What to call the executable.
[execout] :: PkgDesc -> Maybe String

-- | Lists of tests to execute against the package.
[idris_tests] :: PkgDesc -> [Name]

-- | Default settings for package descriptions.
defaultPkg :: PkgDesc
instance GHC.Show.Show Idris.Package.Common.PkgDesc


module Idris.Directives

-- | Run the action corresponding to a directive
directiveAction :: Directive -> Idris ()


module Idris.IBC
loadIBC :: Bool -> IBCPhase -> FilePath -> Idris ()

-- | Load an entire package from its index file
loadPkgIndex :: PkgName -> Idris ()
writeIBC :: FilePath -> FilePath -> Idris ()

-- | Write a package index containing all the imports in the current IState
--   Used for ':search' of an entire package, to ensure everything is
--   loaded.
writePkgIndex :: FilePath -> Idris ()
hasValidIBCVersion :: FilePath -> Idris Bool

-- | When IBC is being loaded - we'll load different things (and omit
--   different structures/definitions) depending on which phase we're in.
data IBCPhase

-- | when building the module tree
IBC_Building :: IBCPhase

-- | when loading modules for the REPL Bool = True for top level module
IBC_REPL :: Bool -> IBCPhase
getIBCHash :: FilePath -> Idris Int
getImportHashes :: FilePath -> Idris [(FilePath, Int)]
instance GHC.Show.Show Idris.IBC.IBCFile
instance GHC.Classes.Eq Idris.IBC.IBCPhase
instance GHC.Show.Show Idris.IBC.IBCPhase
instance Data.Binary.Class.Binary a => Data.Binary.Class.Binary (Idris.Docstrings.Docstring a)
instance Data.Binary.Class.Binary Cheapskate.Types.Options
instance Data.Binary.Class.Binary Idris.Docstrings.DocTerm
instance Data.Binary.Class.Binary a => Data.Binary.Class.Binary (Idris.Docstrings.Block a)
instance Data.Binary.Class.Binary a => Data.Binary.Class.Binary (Idris.Docstrings.Inline a)
instance Data.Binary.Class.Binary Cheapskate.Types.ListType
instance Data.Binary.Class.Binary Cheapskate.Types.CodeAttr
instance Data.Binary.Class.Binary Cheapskate.Types.NumWrapper
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.SizeChange
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.CGInfo
instance Data.Binary.Class.Binary Idris.Core.CaseTree.CaseType
instance Data.Binary.Class.Binary Idris.Core.CaseTree.SC
instance Data.Binary.Class.Binary Idris.Core.CaseTree.CaseAlt
instance Data.Binary.Class.Binary Idris.Core.Evaluate.CaseDefs
instance Data.Binary.Class.Binary Idris.Core.Evaluate.CaseInfo
instance Data.Binary.Class.Binary Idris.Core.Evaluate.Def
instance Data.Binary.Class.Binary Idris.Core.Evaluate.Accessibility
instance Data.Binary.Class.Binary Idris.Core.Evaluate.PReason
instance Data.Binary.Class.Binary Idris.Core.Evaluate.Totality
instance Data.Binary.Class.Binary Idris.Core.Evaluate.MetaInformation
instance Data.Binary.Class.Binary Idris.Core.TT.DataOpt
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.FnOpt
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.Fixity
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.FixDecl
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.ArgOpt
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.Static
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.Plicity
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.DefaultTotality
instance Data.Binary.Class.Binary Idris.Options.LanguageExt
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.Directive
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Idris.AbsSyntaxTree.PDecl' t)
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Idris.AbsSyntaxTree.ProvideWhat' t)
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.Using
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.SyntaxInfo
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Idris.AbsSyntaxTree.PClause' t)
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Idris.AbsSyntaxTree.PData' t)
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.PunInfo
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.PTerm
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.PAltType
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Idris.AbsSyntaxTree.PTactic' t)
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Idris.AbsSyntaxTree.PDo' t)
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Idris.AbsSyntaxTree.PArg' t)
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.InterfaceInfo
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.RecordInfo
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.OptInfo
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.FnInfo
instance Data.Binary.Class.Binary Idris.Core.TT.TypeInfo
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.SynContext
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.Syntax
instance Data.Binary.Class.Binary t => Data.Binary.Class.Binary (Idris.AbsSyntaxTree.DSL' t)
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.SSymbol
instance Data.Binary.Class.Binary Idris.Options.Codegen
instance Data.Binary.Class.Binary Idris.Options.IRFormat


module Idris.Erasure

-- | Perform usage analysis, write the relevant information in the internal
--   structures, returning the list of reachable names.
performUsageAnalysis :: [Name] -> Idris [Name]

-- | Make a field name out of a data constructor name and field number.
mkFieldName :: Name -> Int -> Name
instance GHC.Show.Show Idris.Erasure.VarInfo
instance GHC.Classes.Ord Idris.Erasure.Arg
instance GHC.Classes.Eq Idris.Erasure.Arg
instance GHC.Show.Show Idris.Erasure.Arg


module Idris.Elab.Utils
recheckC :: String -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type)
recheckC_borrowing :: Bool -> Bool -> [Name] -> String -> FC -> (Err' (TT Name) -> Err) -> Env -> TT Name -> StateT IState (ExceptT Err IO) (Term, Type)
checkDeprecated :: FC -> Name -> Idris ()
checkFragile :: FC -> Name -> Idris ()
iderr :: Name -> Err -> Err
checkDef :: ElabInfo -> FC -> (Name -> Err -> Err) -> Bool -> [(Name, (Int, Maybe Name, Type, [Name]))] -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkAddDef :: Bool -> Bool -> ElabInfo -> FC -> (Name -> Err -> Err) -> Bool -> [(Name, (Int, Maybe Name, Type, [Name]))] -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

-- | Get the list of (index, name) of inaccessible arguments from an
--   elaborated type
inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

-- | Get the list of (index, name) of inaccessible arguments from the type.
inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

-- | Check that the result of type checking matches what the programmer
--   wrote (i.e. - if we inferred any arguments that the user provided,
--   make sure they are the same!)
checkInferred :: FC -> PTerm -> PTerm -> Idris ()

-- | Return whether inferred term is different from given term (as above,
--   but return a Bool)
inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

-- | Check a PTerm against documentation and ensure that every documented
--   argument actually exists. This must be run _after_ implicits have been
--   found, or it will give spurious errors.
checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
decorateid :: (Name -> Name) -> PDecl' PTerm -> PDecl' PTerm
pbinds :: IState -> Term -> ElabD ()
pbty :: () => TT n -> TT n -> TT n
getPBtys :: () => TT a -> [(a, TT a)]
psolve :: () => TT n -> StateT (ElabState aux) TC ()
pvars :: IState -> TT Name -> [(Name, PTerm)]
getFixedInType :: () => IState -> [Name] -> [PArg' t] -> TT Name -> [Name]
getFlexInType :: Foldable t => IState -> [Name] -> t Name -> TT Name -> [Name]

-- | Treat a name as a parameter if it appears in parameter positions in
--   types, and never in a non-parameter position in a (non-param) argument
--   type.
getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
getTCinj :: IState -> TT Name -> [Name]
getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
paramNames :: (Foldable t, Eq a) => [TT a] -> t a -> [Int] -> [a]
getLinearUsed :: Context -> Term -> [Name]
getUniqueUsed :: Context -> Term -> [Name]
getStaticNames :: IState -> Term -> [Name]
getStatics :: [Name] -> Term -> [Bool]
mkStatic :: [Name] -> PDecl -> PDecl
mkStaticTy :: [Name] -> PTerm -> PTerm
checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()

-- | Find the type constructor arguments that are parameters, given a list
--   of constructor types.
--   
--   Parameters are names which are unchanged across the structure. They
--   appear at least once in every constructor type, always appear in the
--   same argument position(s), and nothing else ever appears in those
--   argument positions.
findParams :: Name -> Type -> [Type] -> [Int]

-- | Mark a name as detaggable in the global state (should be called for
--   type and constructor names of single-constructor datatypes)
setDetaggable :: Name -> Idris ()
displayWarnings :: EState -> Idris ()
propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm

-- | Gather up all the outer <a>PVar</a>s and <a>Hole</a>s in an expression
--   and reintroduce them in a canonical order
orderPats :: Term -> Term
liftPats :: Term -> Term
isEmpty :: Context -> Ctxt TypeInfo -> Type -> Bool
hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool
findLinear :: RigCount -> IState -> [Name] -> Term -> [(Name, RigCount)]
setLinear :: [(Name, RigCount)] -> Term -> Term
linearArg :: Type -> Bool
pruneByType :: Bool -> Env -> Term -> Type -> IState -> [PTerm] -> [PTerm]
isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool


module Idris.Elab.Rewrite
elabRewrite :: (PTerm -> ElabD ()) -> IState -> FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()

-- | Make a rewriting lemma for the given type constructor.
--   
--   If it fails, fail silently (it may well fail for some very complex
--   types. We can fix this later, for now this gives us a lot more working
--   rewrites...)
elabRewriteLemma :: ElabInfo -> Name -> Type -> Idris ()
instance GHC.Show.Show Idris.Elab.Rewrite.ParamInfo


module Idris.Docs
pprintDocs :: IState -> Docs -> Doc OutputAnnotation

-- | Given a fully-qualified, disambiguated name, construct the
--   documentation object for it
getDocs :: Name -> HowMuchDocs -> Idris Docs
pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
pprintTypeDoc :: IState -> Doc OutputAnnotation
type FunDoc = FunDoc' (Docstring DocTerm)
data FunDoc' d
FD :: Name -> d -> [(Name, PTerm, Plicity, Maybe d)] -> PTerm -> Maybe Fixity -> FunDoc' d
type Docs = Docs' (Docstring DocTerm)
data Docs' d
FunDoc :: FunDoc' d -> Docs' d
DataDoc :: FunDoc' d -> [FunDoc' d] -> Docs' d
InterfaceDoc :: Name -> d -> [FunDoc' d] -> [(Name, Maybe d)] -> [PTerm] -> [(Maybe Name, PTerm, (d, [(Name, d)]))] -> [PTerm] -> [PTerm] -> Maybe (FunDoc' d) -> Docs' d
RecordDoc :: Name -> d -> FunDoc' d -> [FunDoc' d] -> [(Name, PTerm, Maybe d)] -> Docs' d
NamedImplementationDoc :: Name -> FunDoc' d -> Docs' d
ModDoc :: [String] -> d -> Docs' d
instance GHC.Base.Functor Idris.Docs.Docs'
instance GHC.Base.Functor Idris.Docs.FunDoc'


module Idris.IdrisDoc

-- | Generates HTML documentation for a series of loaded namespaces and
--   their dependencies.
generateDocs :: IState -> [Name] -> FilePath -> IO (Either String ())


module Idris.DataOpts
applyOpts :: Optimisable term => term -> Idris term
instance (Idris.DataOpts.Optimisable a, Idris.DataOpts.Optimisable b) => Idris.DataOpts.Optimisable (a, b)
instance (Idris.DataOpts.Optimisable a, Idris.DataOpts.Optimisable b) => Idris.DataOpts.Optimisable (vs, a, b)
instance Idris.DataOpts.Optimisable a => Idris.DataOpts.Optimisable [a]
instance Idris.DataOpts.Optimisable a => Idris.DataOpts.Optimisable (Data.Either.Either a (a, a))
instance Idris.DataOpts.Optimisable Idris.Core.TT.Raw
instance Idris.DataOpts.Optimisable (Idris.Core.TT.Binder (Idris.Core.TT.TT Idris.Core.TT.Name))
instance Idris.DataOpts.Optimisable (Idris.Core.TT.Binder Idris.Core.TT.Raw)
instance Idris.DataOpts.Optimisable (Idris.Core.TT.TT Idris.Core.TT.Name)


module Idris.DSL
debindApp :: SyntaxInfo -> PTerm -> PTerm
desugar :: SyntaxInfo -> IState -> PTerm -> PTerm


module Idris.Parser.Expr

-- | Allow implicit type declarations
allowImp :: SyntaxInfo -> SyntaxInfo

-- | Disallow implicit type declarations
disallowImp :: SyntaxInfo -> SyntaxInfo

-- | Implicits hare are scoped rather than top level
scopedImp :: SyntaxInfo -> SyntaxInfo

-- | Allow scoped constraint arguments
allowConstr :: SyntaxInfo -> SyntaxInfo

-- | Parses an expression as a whole <tt> FullExpr ::= Expr EOF_t; </tt>
fullExpr :: SyntaxInfo -> IdrisParser PTerm
tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

-- | Parses an expression <tt> Expr ::= Pi </tt>
expr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses an expression with possible operator applied <tt> OpExpr ::= ;
--   </tt>
opExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses either an internally defined expression or a user-defined one
--   <tt> Expr' ::= "External (User-defined) Syntax" | InternalExpr; </tt>
expr' :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a user-defined expression
externalExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a simple user-defined expression
simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Tries to parse a user-defined expression given a list of syntactic
--   extensions
extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
data SynMatch
SynTm :: PTerm -> SynMatch

-- | the FC is for highlighting information
SynBind :: FC -> Name -> SynMatch
extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
updateSynMatch :: [(Name, SynMatch)] -> PTerm -> PTerm

-- | Parses a (normal) built-in expression <tt> InternalExpr ::= UnifyLog |
--   RecordType | SimpleExpr | Lambda | QuoteGoal | Let | If | RewriteTerm
--   | CaseExpr | DoBlock | App ; </tt>
internalExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses the "impossible" keyword <tt> Impossible ::= <a>impossible</a>
--   </tt>
impossible :: IdrisParser PTerm

-- | Parses a case expression <tt> CaseExpr ::= 'case' Expr 'of' OpenBlock
--   CaseOption+ CloseBlock; </tt>
caseExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a case in a case expression <tt> CaseOption ::= Expr
--   (Impossible | '=&gt;' Expr) Terminator ; </tt>
caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
warnTacticDeprecation :: FC -> IdrisParser ()

-- | Parses a proof block <tt> ProofExpr ::= <tt>proof</tt> OpenBlock
--   Tactic'* CloseBlock ; </tt>
proofExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a tactics block <tt> TacticsExpr := <a>tactics</a> OpenBlock
--   Tactic'* CloseBlock ; </tt>
tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a simple expression @ SimpleExpr ::=
--   
--   | <tt>?</tt> Name | % <tt>implementation</tt> | <tt>Refl</tt> ('{'
--   Expr '}')? | ProofExpr | TacticsExpr | FnName | Idiom | List | Alt |
--   Bracketed | Constant | Type | <tt>Void</tt> | Quasiquote | NameQuote |
--   Unquote | '_' ; @
simpleExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses an expression in parentheses <tt> Bracketed ::= '(' Bracketed'
--   </tt>
bracketed :: SyntaxInfo -> IdrisParser PTerm

-- | Parses the rest of an expression in braces <tt> Bracketed' ::= ')' |
--   Expr ')' | ExprList ')' | DependentPair ')' | Operator Expr ')' | Expr
--   Operator ')' ; </tt>
bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm

-- | Parses the rest of a dependent pair after '(' or '(Expr **'
dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm

-- | Parse the contents of parentheses, after an expression has been
--   parsed.
bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm

-- | Finds optimal type for integer constant
modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

-- | Parses an alternative expression @ Alt ::= '(|' Expr_List '|)';
--   
--   Expr_List ::= Expr' | Expr' ',' Expr_List ; @
alt :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a possibly hidden simple expression <tt> HSimpleExpr ::=
--   <a>.</a> SimpleExpr | SimpleExpr ; </tt>
hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a unification log expression UnifyLog ::= <tt>%</tt>
--   <a>unifyLog</a> SimpleExpr ;
unifyLog :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a new-style tactics expression RunTactics ::= <tt>%</tt>
--   <a>runElab</a> SimpleExpr ;
runElab :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a disambiguation expression Disamb ::= <tt>with</tt> NameList
--   Expr ;
disamb :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a no implicits expression <tt> NoImplicits ::= <tt>%</tt>
--   <a>noImplicits</a> SimpleExpr ; </tt>
noImplicits :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a function application expression <tt> App ::=
--   <tt>mkForeign</tt> Arg Arg* | MatchApp | SimpleExpr Arg* ; MatchApp
--   ::= SimpleExpr <tt>&lt;==</tt> FnName ; </tt>
app :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a function argument <tt> Arg ::= ImplicitArg | ConstraintArg |
--   SimpleExpr ; </tt>
arg :: SyntaxInfo -> IdrisParser PArg

-- | Parses an implicit function argument <tt> ImplicitArg ::= '{' Name
--   ('=' Expr)? '}' ; </tt>
implicitArg :: SyntaxInfo -> IdrisParser PArg

-- | Parses a constraint argument (for selecting a named interface
--   implementation)
--   
--   <pre>
--   ConstraintArg ::=
--     '@{' Expr '}'
--     ;
--   </pre>
constraintArg :: SyntaxInfo -> IdrisParser PArg

-- | Parses a quasiquote expression (for building reflected terms using the
--   elaborator)
--   
--   <pre>
--   Quasiquote ::= '`(' Expr ')'
--   </pre>
quasiquote :: SyntaxInfo -> IdrisParser PTerm

-- | Parses an unquoting inside a quasiquotation (for building reflected
--   terms using the elaborator)
--   
--   <pre>
--   Unquote ::= ',' Expr
--   </pre>
unquote :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a quotation of a name (for using the elaborator to resolve
--   boring details)
--   
--   <pre>
--   NameQuote ::= '`{' Name '}'
--   </pre>
namequote :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a record field setter expression <tt> RecordType ::=
--   <tt>record</tt> '{' FieldTypeList '}'; </tt> <tt> FieldTypeList ::=
--   FieldType | FieldType ',' FieldTypeList ; </tt> <tt> FieldType ::=
--   FnName '=' Expr ; </tt>
data SetOrUpdate
FieldSet :: PTerm -> SetOrUpdate
FieldUpdate :: PTerm -> SetOrUpdate
recordType :: SyntaxInfo -> IdrisParser PTerm

-- | Creates setters for record types on necessary functions
mkType :: Name -> Name

-- | Parses a type signature <tt> TypeSig ::= <tt>:</tt> Expr ; </tt> <tt>
--   TypeExpr ::= ConstraintList? Expr; </tt>
typeExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a lambda expression <tt> Lambda ::= <a>\\</a> TypeOptDeclList
--   LambdaTail | <a>\\</a> SimpleExprList LambdaTail ; </tt> <tt>
--   SimpleExprList ::= SimpleExpr | SimpleExpr ',' SimpleExprList ; </tt>
--   <tt> LambdaTail ::= Impossible | '=&gt;' Expr </tt>
lambda :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a term rewrite expression <tt> RewriteTerm ::= <tt>rewrite</tt>
--   Expr (<tt>==&gt;</tt> Expr)? 'in' Expr ; </tt>
rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

-- | Parse rig count for linear types
rigCount :: Parsing m => m RigCount

-- | Parses a let binding @ Let ::= 'let' Name TypeSig'? '=' Expr 'in' Expr
--   | 'let' Expr' '=' Expr' 'in' Expr
--   
--   TypeSig' ::= <tt>:</tt> Expr' ; @
let_ :: SyntaxInfo -> IdrisParser PTerm
let_binding :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])

-- | Parses a conditional expression <tt> If ::= 'if' Expr 'then' Expr
--   'else' Expr </tt>
if_ :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a quote goal
--   
--   <pre>
--   QuoteGoal ::=
--     <a>quoteGoal</a> Name <tt>by</tt> Expr 'in' Expr
--     ;
--   </pre>
quoteGoal :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a dependent type signature
--   
--   <pre>
--   Pi ::= PiOpts Static? Pi'
--   </pre>
--   
--   <pre>
--   Pi' ::=
--       OpExpr ('-&gt;' Pi)?
--     | '(' TypeDeclList           ')'            '-&gt;' Pi
--     | '{' TypeDeclList           '}'            '-&gt;' Pi
--     | '{' <tt>auto</tt>    TypeDeclList '}'            '-&gt;' Pi
--     | '{' 'default' SimpleExpr TypeDeclList '}' '-&gt;' Pi
--     ;
--   </pre>
bindsymbol :: (MonadParsec Void String m, MonadWriter FC m) => [ArgOpt] -> Static -> p -> m Plicity
explicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PTerm
autoImplicit :: () => p -> Static -> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PTerm
defaultImplicit :: () => p -> Static -> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PTerm
normalImplicit :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PTerm
constraintPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PTerm
implicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PTerm
unboundPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PTerm
unboundPiNoConstraint :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PTerm
pi :: SyntaxInfo -> IdrisParser PTerm

-- | Parses Possible Options for Pi Expressions <tt> PiOpts ::= <a>.</a>?
--   </tt>
piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

-- | Parses a type constraint list
--   
--   <pre>
--   ConstraintList ::=
--       '(' Expr_List ')' '=&gt;'
--     | Expr              '=&gt;'
--     ;
--   </pre>
constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

-- | Parses a type declaration list <tt> TypeDeclList ::=
--   FunctionSignatureList | NameList TypeSig ; </tt>
--   
--   <pre>
--   FunctionSignatureList ::=
--       Name TypeSig
--     | Name TypeSig ',' FunctionSignatureList
--     ;
--   </pre>
typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

-- | Parses a type declaration list with optional parameters <tt>
--   TypeOptDeclList ::= NameOrPlaceholder TypeSig? | NameOrPlaceholder
--   TypeSig? ',' TypeOptDeclList ; </tt>
--   
--   <pre>
--   NameOrPlaceHolder ::= Name | '_';
--   </pre>
tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]

-- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x,
--   y) | x &lt;- xs , y &lt;- ys ] <tt> ListExpr ::= '[' ']' | '[' Expr
--   '|' DoList ']' | '[' ExprList ']' ; </tt> <tt> DoList ::= Do | Do ','
--   DoList ; </tt> <tt> ExprList ::= Expr | Expr ',' ExprList ; </tt>
listExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a do-block <tt> Do' ::= Do KeepTerminator; </tt>
--   
--   <pre>
--   DoBlock ::=
--     'do' OpenBlock Do'+ CloseBlock
--     ;
--   </pre>
doBlock :: SyntaxInfo -> IdrisParser PTerm

-- | Parses an expression inside a do block <tt> Do ::= 'let' Name
--   TypeSig'? '=' Expr | 'let' Expr' '=' Expr | 'rewrite Expr | Name
--   '&lt;-' Expr | Expr' '&lt;-' Expr | Expr ; </tt>
do_ :: SyntaxInfo -> IdrisParser PDo
do_alt :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, PTerm)

-- | Parses an expression in idiom brackets <tt> Idiom ::= '[|' Expr '|]';
--   </tt>
idiom :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a constant or literal expression
--   
--   <pre>
--   Constant ::=
--       <a>Integer</a>
--     | <a>Int</a>
--     | <a>Char</a>
--     | <a>Double</a>
--     | <a>String</a>
--     | <tt>Bits8</tt>
--     | <tt>Bits16</tt>
--     | <tt>Bits32</tt>
--     | <tt>Bits64</tt>
--     | Float_t
--     | Natural_t
--     | VerbatimString_t
--     | String_t
--     | Char_t
--     ;
--   </pre>
constants :: [(String, Const)]

-- | Parse a constant and its source span
constant :: Parsing m => m Const

-- | Parses a verbatim multi-line string literal (triple-quoted)
--   
--   <pre>
--   VerbatimString_t ::=
--     '"""' ~'"""' '"'* '"""'
--   ;
--   </pre>
verbatimStringLiteral :: Parsing m => m String

-- | Parses a static modifier
--   
--   <pre>
--   Static ::=
--     '%static'
--   ;
--   </pre>
static :: IdrisParser Static

-- | Parses a tactic script
--   
--   <pre>
--   Tactic ::= <tt>intro</tt> NameList?
--          |   <tt>intros</tt>
--          |   <tt>refine</tt>      Name Imp+
--          |   <tt>mrefine</tt>     Name
--          |   <tt>rewrite</tt>     Expr
--          |   <tt>induction</tt>   Expr
--          |   <tt>equiv</tt>       Expr
--          |   'let'         Name <tt>:</tt> Expr' '=' Expr
--          |   'let'         Name           '=' Expr
--          |   <tt>focus</tt>       Name
--          |   <tt>exact</tt>       Expr
--          |   <tt>applyTactic</tt> Expr
--          |   <tt>reflect</tt>     Expr
--          |   <tt>fill</tt>        Expr
--          |   <tt>try</tt>         Tactic '|' Tactic
--          |   '{' TacticSeq '}'
--          |   <tt>compute</tt>
--          |   <tt>trivial</tt>
--          |   <tt>solve</tt>
--          |   <tt>attack</tt>
--          |   <a>state</a>
--          |   <tt>term</tt>
--          |   <tt>undo</tt>
--          |   <tt>qed</tt>
--          |   <tt>abandon</tt>
--          |   <tt>:</tt> <tt>q</tt>
--          ;
--   
--   Imp ::= <tt>?</tt> | '_';
--   
--   TacticSeq ::=
--       Tactic ';' Tactic
--     | Tactic ';' TacticSeq
--     ;
--   </pre>
--   
--   A specification of the arguments that tactics can take
data TacticArg

-- | Names: n1, n2, n3, ... n
NameTArg :: TacticArg
ExprTArg :: TacticArg
AltsTArg :: TacticArg
StringLitTArg :: TacticArg

-- | A list of available tactics and their argument requirements
tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
tactic :: SyntaxInfo -> IdrisParser PTactic

-- | Parses a tactic as a whole
fullTactic :: SyntaxInfo -> IdrisParser PTactic
instance GHC.Show.Show Idris.Parser.Expr.SynMatch


module Idris.Parser.Data

-- | Parses a record type declaration Record ::= DocComment Accessibility?
--   <a>record</a> FnName TypeSig 'where' OpenBlock Constructor
--   KeepTerminator CloseBlock;
record :: SyntaxInfo -> IdrisParser PDecl
recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)

-- | Parses data declaration type (normal or codata) DataI ::= 'data' |
--   <a>codata</a>;
dataI :: IdrisParser DataOpts
recordI :: IdrisParser DataOpts
dataOpts :: DataOpts -> IdrisParser DataOpts

-- | Parses a data type declaration Data ::= DocComment? Accessibility?
--   DataI FnName TypeSig ExplicitTypeDataRest? | DocComment?
--   Accessibility? DataI FnName Name* DataRest? ; Constructor' ::=
--   Constructor KeepTerminator; ExplicitTypeDataRest ::= 'where' OpenBlock
--   Constructor'* CloseBlock;
--   
--   DataRest ::= '=' SimpleConstructorList Terminator | 'where'! ;
--   SimpleConstructorList ::= SimpleConstructor | SimpleConstructor '|'
--   SimpleConstructorList ;
data_ :: SyntaxInfo -> IdrisParser PDecl

-- | Parses a type constructor declaration Constructor ::= DocComment?
--   FnName TypeSig;
constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])

-- | Parses a constructor for simple discriminated union data types
--   SimpleConstructor ::= FnName SimpleExpr* DocComment?
simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])

-- | Parses a dsl block declaration DSL ::= <a>dsl</a> FnName OpenBlock
--   Overload'+ CloseBlock;
dsl :: SyntaxInfo -> IdrisParser PDecl

-- | Checks DSL for errors
checkDSL :: DSL -> IdrisParser ()

-- | Parses a DSL overload declaration OverloadIdentifier ::= 'let' |
--   Identifier; Overload ::= OverloadIdentifier '=' Expr;
overload :: SyntaxInfo -> IdrisParser (String, PTerm)


module Idris.Coverage

-- | Given a list of LHSs, generate a extra clauses which cover the
--   remaining cases. The ones which haven't been provided are marked
--   <tt>absurd</tt> so that the checker will make sure they can't happen.
--   
--   This will only work after the given clauses have been typechecked and
--   the names are fully explicit!
genClauses :: FC -> Name -> [([Name], Term)] -> [PTerm] -> Idris [PTerm]

-- | Does this error result rule out a case as valid when coverage
--   checking?
validCoverageCase :: Context -> Err -> Bool

-- | Check whether an error is recoverable in the sense needed for coverage
--   checking.
recoverableCoverage :: Context -> Err -> Bool

-- | Generate a pattern from an <tt>impossible</tt> LHS.
--   
--   We need this to eliminate the pattern clauses which have been provided
--   explicitly from new clause generation.
--   
--   This takes a type directed approach to disambiguating names. If we
--   can't immediately disambiguate by looking at the expected type, it's
--   an error (we can't do this the usual way of trying it to see what type
--   checks since the whole point of an impossible case is that it won't
--   type check!)
mkPatTm :: PTerm -> Idris Term


module Idris.Elab.Term
data ElabMode
ETyDecl :: ElabMode
ETransLHS :: ElabMode
ELHS :: ElabMode
EImpossible :: ElabMode
ERHS :: ElabMode
data ElabResult
ElabResult :: Term -> [(Name, (Int, Maybe Name, Type, [Name]))] -> [PDecl] -> Context -> [RDeclInstructions] -> Set (FC', OutputAnnotation) -> Int -> ElabResult

-- | The term resulting from elaboration
[resultTerm] :: ElabResult -> Term

-- | Information about new metavariables
[resultMetavars] :: ElabResult -> [(Name, (Int, Maybe Name, Type, [Name]))]

-- | Deferred declarations as the meaning of case blocks
[resultCaseDecls] :: ElabResult -> [PDecl]

-- | The potentially extended context from new definitions
[resultContext] :: ElabResult -> Context

-- | Meta-info about the new type declarations
[resultTyDecls] :: ElabResult -> [RDeclInstructions]

-- | Saved highlights from elaboration
[resultHighlighting] :: ElabResult -> Set (FC', OutputAnnotation)

-- | The new global name counter
[resultName] :: ElabResult -> Int

-- | Using the elaborator, convert a term in raw syntax to a fully
--   elaborated, typechecked term.
--   
--   If building a pattern match, we convert undeclared variables from
--   holes to pattern bindings.
--   
--   Also find deferred names in the term and their types
build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult

-- | Build a term autogenerated as an interface method definition.
--   
--   (Separate, so we don't go overboard resolving things that we don't
--   know about yet on the LHS of a pattern def)
buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> [Name] -> PTerm -> ElabD ElabResult

-- | return whether arguments of the given constructor name can be matched
--   on. If they're polymorphic, no, unless the type has beed made concrete
--   by the time we get around to elaborating the argument.
getUnmatchable :: Context -> Name -> [Bool]
data ElabCtxt
ElabCtxt :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> ElabCtxt
[e_inarg] :: ElabCtxt -> Bool

-- | Function part of application
[e_isfn] :: ElabCtxt -> Bool
[e_guarded] :: ElabCtxt -> Bool
[e_intype] :: ElabCtxt -> Bool
[e_qq] :: ElabCtxt -> Bool

-- | can't pattern match
[e_nomatching] :: ElabCtxt -> Bool
initElabCtxt :: ElabCtxt
goal_polymorphic :: ElabD Bool

-- | Returns the set of declarations we need to add to complete the
--   definition (most likely case blocks to elaborate) as well as
--   declarations resulting from user tactic scripts (%runElab)
elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ()
pruneAlt :: [PTerm] -> [PTerm]

-- | Use the local elab context to work out the highlighting for a name
findHighlight :: Name -> ElabD OutputAnnotation
solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()
solveAutos :: IState -> Name -> Bool -> ElabD ()
tcRecoverable :: ElabMode -> Err -> Bool
trivial' :: IState -> ElabD ()
trivialHoles' :: [Name] -> [(Name, Int)] -> IState -> ElabD ()
proofSearch' :: IState -> Bool -> Bool -> Int -> Bool -> Maybe Name -> Name -> [Name] -> [Name] -> StateT (ElabState EState) TC ()
resolveTC' :: Bool -> Bool -> Int -> Term -> Name -> IState -> ElabD ()
collectDeferred :: Maybe Name -> [Name] -> Context -> Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term

-- | Compute the appropriate name for a top-level metavariable
metavarName :: [String] -> Name -> Name
runElabAction :: ElabInfo -> IState -> FC -> Env -> Term -> [String] -> ElabD Term
runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
elaboratingArgErr :: [(Name, Name)] -> Err -> Err
withErrorReflection :: Idris a -> Idris a
solveAll :: () => StateT (ElabState aux) TC ()

-- | Do the left-over work after creating declarations in reflected
--   elaborator scripts
processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()
instance GHC.Classes.Eq Idris.Elab.Term.ElabMode


module Idris.Elab.Value
elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)

-- | Elaborate a value, returning any new bindings created (this will only
--   happen if elaborating as a pattern clause)
elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
elabDocTerms :: ElabInfo -> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)

-- | Try running the term directly (as IO ()) or with &gt;&gt;= printLn
--   appended (for other IO _), then printing it as an Integer (as a
--   default numeric type), then printing it as any Showable thing
elabExec :: FC -> PTerm -> PTerm
elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)


module Idris.Elab.Type
buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris (Type, Type, PTerm, [(Int, Name)])

-- | Elaborate a top-level type declaration - for example, "foo : Int -&gt;
--   Int".
elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> FC -> FnOpts -> Name -> FC -> PTerm -> Idris Type
elabType' :: Bool -> ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> FC -> FnOpts -> Name -> FC -> PTerm -> Idris Type
elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()


module Idris.TypeSearch
searchByType :: [PkgName] -> PTerm -> Idris ()

-- | Our default search predicate.
searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]

-- | Convert a <a>Score</a> to an <a>Int</a> to provide an order for search
--   results. Lower scores are better.
defaultScoreFunction :: Score -> Int
instance GHC.Show.Show Idris.TypeSearch.State
instance GHC.Show.Show Idris.TypeSearch.Score
instance GHC.Classes.Eq Idris.TypeSearch.Score
instance GHC.Show.Show a => GHC.Show.Show (Idris.TypeSearch.Sided a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Idris.TypeSearch.Sided a)
instance GHC.Show.Show Idris.TypeSearch.AsymMods
instance GHC.Classes.Eq Idris.TypeSearch.AsymMods
instance GHC.Classes.Ord Idris.TypeSearch.Score
instance GHC.Base.Semigroup Idris.TypeSearch.Score
instance GHC.Base.Monoid Idris.TypeSearch.Score
instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Idris.TypeSearch.Sided a)
instance GHC.Base.Monoid a => GHC.Base.Monoid (Idris.TypeSearch.Sided a)
instance GHC.Base.Semigroup Idris.TypeSearch.AsymMods
instance GHC.Base.Monoid Idris.TypeSearch.AsymMods


module Idris.Elab.Data
elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()


module Idris.Elab.Record

-- | Elaborate a record declaration
elabRecord :: ElabInfo -> ElabWhat -> Docstring (Either Err PTerm) -> SyntaxInfo -> FC -> DataOpts -> Name -> FC -> [(Name, FC, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> Maybe (Name, FC) -> Docstring (Either Err PTerm) -> SyntaxInfo -> Idris ()


module Idris.Elab.Interface
elabInterface :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> ElabWhat -> FC -> [(Name, PTerm)] -> Name -> FC -> [(Name, FC, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, FC)] -> [PDecl] -> Maybe (Name, FC) -> Docstring (Either Err PTerm) -> Idris ()
instance GHC.Show.Show Idris.Elab.Interface.MArgTy


module Idris.Elab.Transform
elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)


module Idris.Elab.RunElab
elabRunElab :: ElabInfo -> FC -> PTerm -> [String] -> Idris ()


module Idris.Elab.Implementation
elabImplementation :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> ElabWhat -> FC -> [(Name, PTerm)] -> [Name] -> Accessibility -> FnOpts -> Name -> FC -> [PTerm] -> [(Name, PTerm)] -> PTerm -> Maybe Name -> [PDecl] -> Idris ()


module Idris.Elab.Clause

-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
--   top-level definition.
elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
forceWith :: Ctxt OptInfo -> Term -> Term

-- | Find <tt>static</tt> applications in a term and partially evaluate
--   them. Return any new transformation rules
elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]

-- | Checks if the clause is a possible left hand side. NOTE: A lot of this
--   is repeated for reflected definitions in Idris.Elab.Term One day,
--   these should be merged, but until then remember that if you edit this
--   you might need to edit the other version...
checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)
checkPossibles :: ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]
findUnique :: Context -> Env -> Term -> [Name]

-- | Return the elaborated LHS/RHS, and the original LHS with implicits
--   added
elabClause :: ElabInfo -> FnOpts -> (Int, PClause) -> Idris (Either Term (Term, Term), PTerm)

-- | Apply a transformation to all RHSes and nested RHSs
mapRHS :: (PTerm -> PTerm) -> PClause -> PClause
mapRHSdecl :: (PTerm -> PTerm) -> PDecl -> PDecl


module Idris.Core.Execute
execute :: Term -> Idris Term


module Idris.Elab.Provider

-- | Elaborate a type provider
elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()


module Idris.ElabDecls
elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' :: ElabWhat -> ElabInfo -> PDecl -> StateT IState (ExceptT Err IO) ()
elabDecls :: ElabInfo -> [PDecl] -> Idris ()

-- | Return the elaborated term which calls <tt>main</tt>
elabMain :: Idris Term

-- | Elaborate primitives
elabPrims :: Idris ()

-- | Top level elaborator info, supporting recursive elaboration
recinfo :: FC -> ElabInfo


module Idris.Parser

-- | Idris parser with state used during parsing
type IdrisParser = Parser IState
data ImportInfo
ImportInfo :: Bool -> FilePath -> Maybe (String, FC) -> [Text] -> FC -> FC -> ImportInfo
[import_reexport] :: ImportInfo -> Bool
[import_path] :: ImportInfo -> FilePath
[import_rename] :: ImportInfo -> Maybe (String, FC)
[import_namespace] :: ImportInfo -> [Text]
[import_location] :: ImportInfo -> FC
[import_modname_location] :: ImportInfo -> FC

-- | Parses module definition
--   
--   <pre>
--   ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
--   </pre>
moduleName :: Parsing m => m Name

-- | Like <a>addSyntax</a>, but no effect on the IBC.
addReplSyntax :: IState -> Syntax -> IState
clearParserWarnings :: Idris ()

-- | Parses a top-level declaration
--   
--   <pre>
--   Decl ::=
--       Decl'
--     | Using
--     | Params
--     | Mutual
--     | Namespace
--     | Interface
--     | Implementation
--     | DSL
--     | Directive
--     | Provider
--     | Transform
--     | Import!
--     | RunElabDecl
--     ;
--   </pre>
decl :: SyntaxInfo -> IdrisParser [PDecl]

-- | Check if the coloring matches the options and corrects if necessary
fixColour :: Bool -> Doc -> Doc

-- | Load idris code from file
loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

-- | Load idris module and show error if something wrong happens
loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)

-- | Parses a name
name :: (Parsing m, MonadState IState m) => m Name
opChars :: String

-- | Parses a do-step from input (used in the elab shell)
parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)

-- | Parses a constant form input
parseConst :: IState -> String -> Either ParseError Const

-- | Parses an expression from input
parseExpr :: IState -> String -> Either ParseError PTerm

-- | Parse module header and imports
parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)

-- | Parses a tactic from input
parseTactic :: IState -> String -> Either ParseError PTactic

-- | Run the Idris parser stack
runparser :: Parser st res -> st -> String -> String -> Either ParseError res
data ParseError
parseErrorDoc :: ParseError -> Doc


module Idris.REPL.Parser
parseCmd :: IState -> String -> String -> Either ParseError (Either String Command)
help :: [([String], CmdArg, String)]
allHelp :: [([String], CmdArg, String)]
setOptions :: [(String, Opt)]


module Idris.Completion

-- | Complete REPL commands and defined identifiers
replCompletion :: CompletionFunc Idris

-- | Complete tactics and their arguments
proverCompletion :: [String] -> CompletionFunc Idris
instance GHC.Classes.Eq Idris.Completion.CompletionMode


module Idris.Prover

-- | Launch the proof shell
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
showProof :: Bool -> Name -> [String] -> String
showRunElab :: Bool -> Name -> [String] -> String


module Idris.Chaser
buildTree :: [FilePath] -> [(FilePath, [ImportInfo])] -> FilePath -> Idris [ModuleTree]
getImports :: [(FilePath, [ImportInfo])] -> [FilePath] -> Idris [(FilePath, [ImportInfo])]

-- | Given a module tree, return the list of files to be loaded. If any
--   module has a descendent which needs reloading, return its source,
--   otherwise return the IBC
getModuleFiles :: [ModuleTree] -> [IFileType]
data ModuleTree
MTree :: IFileType -> Bool -> UTCTime -> [ModuleTree] -> ModuleTree
[mod_path] :: ModuleTree -> IFileType
[mod_needsRecheck] :: ModuleTree -> Bool
[mod_time] :: ModuleTree -> UTCTime
[mod_deps] :: ModuleTree -> [ModuleTree]
instance GHC.Show.Show Idris.Chaser.ModuleTree


-- | Given a pattern clause and a variable <tt>n</tt>, elaborate the clause
--   and find the type of <tt>n</tt>.
--   
--   Make new pattern clauses by replacing <tt>n</tt> with all the possibly
--   constructors applied to '_', and replacing all other variables with
--   '_' in order to resolve other dependencies.
--   
--   Finally, merge the generated patterns with the original, by matching.
--   Always take the "more specific" argument when there is a discrepancy,
--   i.e. names over '_', patterns over names, etc.
module Idris.CaseSplit
splitOnLine :: Int -> Name -> FilePath -> Idris (Bool, [[(Name, PTerm)]])
replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
getClause :: Int -> Name -> Name -> FilePath -> Idris String
getProofClause :: Int -> Name -> FilePath -> Idris String
mkWith :: String -> Name -> Int -> String
nameMissing :: [PTerm] -> Idris [PTerm]
getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
nameRoot :: [String] -> [Char] -> String


module Idris.Interactive
caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
doProofSearch :: FilePath -> Bool -> Bool -> Int -> Name -> [Name] -> Maybe Int -> Idris ()
makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()


module Idris.Apropos

-- | Find definitions that are relevant to all space-delimited components
--   of some string. Relevance is one or more of the following:
--   
--   <ul>
--   <li>the string is a substring of the name</li>
--   <li>the string occurs in the documentation string</li>
--   <li>the type of the definition is apropos</li>
--   </ul>
apropos :: IState -> Text -> [Name]

-- | Find modules whose names or docstrings contain all the space-delimited
--   components of some string.
aproposModules :: IState -> Text -> [(String, Docstring DocTerm)]
instance Idris.Apropos.Apropos Idris.Core.TT.Name
instance Idris.Apropos.Apropos Idris.Core.Evaluate.Def
instance Idris.Apropos.Apropos (Idris.Core.TT.Binder (Idris.Core.TT.TT Idris.Core.TT.Name))
instance Idris.Apropos.Apropos (Idris.Core.TT.TT Idris.Core.TT.Name)
instance Idris.Apropos.Apropos Idris.Core.TT.Const
instance Idris.Apropos.Apropos (Idris.Docstrings.Docstring a)
instance (Idris.Apropos.Apropos a, Idris.Apropos.Apropos b) => Idris.Apropos.Apropos (a, b)
instance Idris.Apropos.Apropos a => Idris.Apropos.Apropos (GHC.Maybe.Maybe a)
instance Idris.Apropos.Apropos a => Idris.Apropos.Apropos [a]


module IRTS.Exports
findExports :: Idris [ExportIFace]
getExpNames :: [ExportIFace] -> [Name]


module IRTS.JavaScript.Codegen
codegenJs :: CGConf -> CodeGenerator
data CGConf
CGConf :: Text -> Text -> String -> String -> CGConf
[header] :: CGConf -> Text
[footer] :: CGConf -> Text
[jsbnPath] :: CGConf -> String
[extraRunTime] :: CGConf -> String

-- | Code generation stats hold information about the generated user code.
--   Based on that information we add additional code to make things work.
data CGStats
CGStats :: Bool -> Set Partial -> Set HiddenClass -> CGStats
[usedBigInt] :: CGStats -> Bool
[partialApplications] :: CGStats -> Set Partial
[hiddenClasses] :: CGStats -> Set HiddenClass
instance GHC.Base.Semigroup IRTS.JavaScript.Codegen.CGStats
instance GHC.Base.Monoid IRTS.JavaScript.Codegen.CGStats


module IRTS.CodegenJavaScript
codegenJavaScript :: CodeGenerator
codegenNode :: CodeGenerator
data JSTarget
Node :: JSTarget
JavaScript :: JSTarget
instance GHC.Classes.Eq IRTS.CodegenJavaScript.JSTarget


module IRTS.CodegenC
codegenC :: CodeGenerator


module IRTS.Compiler

-- | Compile to simplified forms and return CodegenInfo
compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
instance GHC.Show.Show IRTS.Compiler.VarInfo


module Idris.Info
getIdrisDataDir :: IO String
getIdrisCRTSDir :: IO String
getIdrisJSRTSDir :: IO String
getIdrisLibDir :: IO String
getIdrisDocDir :: IO String
getIdrisFlagsLib :: IO [String]
getIdrisFlagsInc :: IO [String]
getIdrisFlagsEnv :: IO [String]
getIdrisCC :: IO String
getIdrisVersion :: [Char]
getIdrisVersionNoGit :: Version

-- | Get the platform-specific, user-specific Idris dir
getIdrisUserDataDir :: IO FilePath

-- | Locate the platform-specific location for the init script
getIdrisInitScript :: IO FilePath
getIdrisHistoryFile :: IO FilePath
getIdrisInstalledPackages :: IO [String]
getIdrisLoggingCategories :: IO [String]
getIdrisDataFileByName :: String -> IO FilePath


module Idris.ModeCommon
banner :: [Char]
defaultPort :: PortNumber
loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
warranty :: [Char]


module Idris.REPL

-- | Run the IdeMode
idemodeStart :: Bool -> IState -> [FilePath] -> Idris ()

-- | Run the REPL server
startServer :: PortNumber -> IState -> [FilePath] -> Idris ()

-- | Run a command on the server on localhost
runClient :: Maybe PortNumber -> String -> IO ()
process :: FilePath -> Command -> Idris ()
replSettings :: Maybe FilePath -> Settings Idris

-- | Run the REPL
repl :: IState -> [FilePath] -> FilePath -> InputT Idris ()
proofs :: IState -> Idris ()


module Idris.Main

-- | The main function of Idris that when given a set of Options will
--   launch Idris into the desired interaction mode either: REPL; Compiler;
--   Script execution; or IDE Mode.
idrisMain :: [Opt] -> Idris ()

-- | Invoke as if from command line. It is an error if there are unresolved
--   totality problems.
idris :: [Opt] -> IO (Maybe IState)

-- | How to run Idris programs.
runMain :: Idris () -> IO ()

-- | Run a command on the server on localhost
runClient :: Maybe PortNumber -> String -> IO ()
loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]

module Idris.Info.Show
showIdrisCRTSDir :: IO ()
showExitIdrisCRTSDir :: IO ()
showIdrisJSRTSDir :: IO ()
showExitIdrisJSRTSDir :: IO ()
showIdrisFlagsLibs :: IO ()
showExitIdrisFlagsLibs :: IO ()
showIdrisDataDir :: IO ()
showExitIdrisDataDir :: IO ()
showIdrisLibDir :: IO ()
showExitIdrisLibDir :: IO ()
showIdrisDocDir :: IO ()
showExitIdrisDocDir :: IO ()
showIdrisFlagsInc :: IO ()
showExitIdrisFlagsInc :: IO ()

-- | List idris packages installed
showIdrisInstalledPackages :: IO ()
showExitIdrisInstalledPackages :: IO ()
showIdrisLoggingCategories :: IO ()
showExitIdrisLoggingCategories :: IO ()
showIdrisInfo :: IO ()
showExitIdrisInfo :: IO ()


module Idris.CmdOptions
opt :: (Opt -> Maybe a) -> [Opt] -> [a]
getClient :: Opt -> Maybe String
getPkg :: Opt -> Maybe (Bool, String)
getPkgCheck :: Opt -> Maybe String
getPkgClean :: Opt -> Maybe String

-- | Returns None if given an Opt which is not PkgMkDoc Otherwise returns
--   Just x, where x is the contents of PkgMkDoc
getPkgMkDoc :: Opt -> Maybe (Bool, String)
getPkgREPL :: Opt -> Maybe String
getPkgTest :: Opt -> Maybe String
getPort :: [Opt] -> Maybe REPLPort
getIBCSubDir :: Opt -> Maybe String
pureArgParser :: [String] -> [Opt]
execArgParserPure :: [String] -> ParserResult [Opt]
runArgParser :: IO [Opt]


module Idris.Package.Parser
type PParser = Parser PkgDesc
parseDesc :: FilePath -> IO PkgDesc
pPkg :: PParser PkgDesc
pPkgName :: PParser PkgName

-- | Parses a filename. | | Treated for now as an identifier or a
--   double-quoted string.
filename :: Parsing m => m String
textUntilEol :: Parsing m => m String
clause :: String -> PParser a -> (PkgDesc -> a -> PkgDesc) -> PParser ()
commaSep :: Parsing m => m a -> m [a]
pOptions :: PParser [Opt]
libIdentifier :: Parsing m => m String
pClause :: PParser ()


module Idris.Package
getPkgDesc :: FilePath -> IO PkgDesc

-- | Run the package through the idris compiler.
buildPkg :: [Opt] -> Bool -> (Bool, FilePath) -> IO ()

-- | Type check packages only
--   
--   This differs from build in that executables are not built, if the
--   package contains an executable.
checkPkg :: [Opt] -> Bool -> Bool -> FilePath -> IO ()

-- | Check a package and start a REPL.
--   
--   This function only works with packages that have a main module.
replPkg :: [Opt] -> FilePath -> Idris ()

-- | Clean Package build files
cleanPkg :: [Opt] -> FilePath -> IO ()

-- | Generate IdrisDoc for package TODO: Handle case where module does not
--   contain a matching namespace E.g. from prelude.ipkg: IO,
--   Prelude.Chars, Builtins
--   
--   Issue number #1572 on the issue tracker
--   <a>https://github.com/idris-lang/Idris-dev/issues/1572</a>
documentPkg :: [Opt] -> (Bool, FilePath) -> IO ()

-- | Build a package with a sythesized main function that runs the tests
testPkg :: [Opt] -> FilePath -> IO ExitCode

-- | Install package
installPkg :: [String] -> PkgDesc -> IO ()
auditPackage :: Bool -> PkgDesc -> IO ()
buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
testLib :: Bool -> PkgName -> String -> IO Bool
rmIBC :: Name -> IO ()
rmIdx :: PkgName -> IO ()
rmExe :: String -> IO ()
toIBCFile :: Name -> String
installIBC :: String -> PkgName -> Name -> IO ()
installIdx :: String -> PkgName -> IO ()
installObj :: String -> PkgName -> String -> IO ()
mkDirCmd :: [Char]
inPkgDir :: PkgDesc -> IO a -> IO a

-- | Invoke a Makefile's target with an enriched system environment
makeTarget :: Maybe String -> Maybe String -> IO ()

-- | Invoke a Makefile's default target.
make :: Maybe String -> IO ()

-- | Invoke a Makefile's clean target.
clean :: Maybe String -> IO ()

-- | Merge an option list representing the command line options into those
--   specified for a package description.
--   
--   This is not a complete union between the two options sets. First, to
--   prevent important package specified options from being overwritten.
--   Second, the semantics for this merge are not fully defined.
--   
--   A discussion for this is on the issue tracker:
--   <a>https://github.com/idris-lang/Idris-dev/issues/1448</a>
mergeOptions :: [Opt] -> [Opt] -> Either String [Opt]