-- 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 0.99


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
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
setupBundledCC :: IO ()
isATTY :: IO Bool


module Util.ScreenSize
getScreenWidth :: IO Int


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


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 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


-- | 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 :: !b -> Binder b

-- | 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 :: Maybe ImplicitInfo -> !b -> !b -> Binder b
[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 :: !b -> b -> Binder b

-- | 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 :: !b -> Binder b

-- | 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

-- | Set if an eliminator should be generated for data type
DefaultEliminator :: DataOpt

-- | Set if a case function should be generated for data type
DefaultCaseFun :: 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, 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
NoEliminator :: String -> 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 the parser
--   <a>getFC</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
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 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
ElimN :: !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] -> TypeInfo
[con_names] :: TypeInfo -> [Name]
[codata] :: TypeInfo -> Bool
[data_opts] :: TypeInfo -> DataOpts
[param_pos] :: TypeInfo -> [Int]
[mutual_types] :: TypeInfo -> [Name]

-- | 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 :: (t1 -> t) -> (t1, t1) -> (t, t)

-- | 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, Binder (TT a))] -> TT a -> [Char]
showSep :: String -> [String] -> String
sImplementationN :: Name -> [String] -> SpecialName
sMN :: Int -> String -> Name
sNS :: Name -> [String] -> Name

-- | Get the largest span containing the two FCs
spanFC :: FC -> FC -> FC
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 -> t -> t
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
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.Classes.Eq n, GHC.Show.Show n) => GHC.Show.Show (Idris.Core.TT.Datatype n)
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.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.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.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.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.Eq Idris.Core.TT.TextFormatting
instance GHC.Show.Show Idris.Core.TT.TextFormatting
instance GHC.Generics.Generic 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 GHC.Classes.Eq Idris.Core.TT.FC
instance GHC.Classes.Eq Idris.Core.TT.FC'
instance GHC.Show.Show Idris.Core.TT.FC'
instance Util.Pretty.Sized Idris.Core.TT.FC
instance GHC.Show.Show Idris.Core.TT.FC
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 Util.Pretty.Sized Idris.Core.TT.ErrorReportPart
instance Util.Pretty.Sized Idris.Core.TT.Err
instance GHC.Show.Show Idris.Core.TT.Err
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 GHC.Show.Show a => GHC.Show.Show (Idris.Core.TT.TC a)
instance Util.Pretty.Sized Idris.Core.TT.Name
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 GHC.Show.Show Idris.Core.TT.Name
instance GHC.Show.Show Idris.Core.TT.SpecialName
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 GHC.Classes.Eq Idris.Core.TT.Const
instance Util.Pretty.Sized Idris.Core.TT.Const
instance Util.Pretty.Pretty Idris.Core.TT.Const Idris.Core.TT.OutputAnnotation
instance GHC.Show.Show Idris.Core.TT.Universe
instance Util.Pretty.Sized Idris.Core.TT.Raw
instance Util.Pretty.Pretty Idris.Core.TT.Raw Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.Core.TT.Binder a)
instance Util.Pretty.Sized Idris.Core.TT.UExp
instance GHC.Show.Show Idris.Core.TT.UExp
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.NameType
instance Util.Pretty.Pretty Idris.Core.TT.NameType Idris.Core.TT.OutputAnnotation
instance GHC.Classes.Eq Idris.Core.TT.NameType
instance Idris.Core.TT.TermSize a => Idris.Core.TT.TermSize [a]
instance Idris.Core.TT.TermSize (Idris.Core.TT.TT Idris.Core.TT.Name)
instance Util.Pretty.Sized Idris.Core.TT.Universe
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 GHC.Show.Show Idris.Core.TT.Const


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.Unlit
unlit :: FilePath -> String -> TC String


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 GHC.Show.Show t => GHC.Show.Show (Idris.Core.CaseTree.SC' t)
instance Idris.Core.TT.TermSize Idris.Core.CaseTree.SC
instance Idris.Core.TT.TermSize Idris.Core.CaseTree.CaseAlt


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

-- | 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.
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
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 -> 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
lookupTotal :: Name -> Context -> [Totality]
lookupTotalExact :: Name -> Context -> Maybe Totality
lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
lookupNameTotal :: Name -> Context -> [(Name, Totality)]
lookupMetaInformation :: Name -> Context -> [MetaInformation]
lookupTyEnv :: Name -> Env -> Maybe (Int, 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

-- | 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 :: 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 (Def, Injectivity, Accessibility, Totality, MetaInformation)
isUniverse :: Term -> Bool
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.Value
instance GHC.Show.Show (a -> b)
instance GHC.Classes.Eq Idris.Core.Evaluate.Value
instance Idris.Core.Evaluate.Quote Idris.Core.Evaluate.Value
instance GHC.Show.Show Idris.Core.Evaluate.Def
instance GHC.Show.Show Idris.Core.Evaluate.Accessibility
instance GHC.Show.Show Idris.Core.Evaluate.Totality


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 GHC.Types.Ordering
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 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.Typecheck
convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()
converts :: Context -> Env -> Term -> Term -> TC ()
isHole :: (t1, Binder t) -> Bool
errEnv :: [(t1, Binder t)] -> [(t1, t)]
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


-- | 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.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


-- | 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 -> (Maybe ImplicitInfo) -> Raw -> Tactic
LetBind :: Name -> Raw -> Raw -> Tactic
ExpandLet :: Name -> Term -> Tactic
Rewrite :: Raw -> Tactic
Induction :: Raw -> Tactic
CaseTac :: Raw -> Tactic
Equiv :: Raw -> Tactic
PatVar :: Name -> Tactic
PatBind :: Name -> Tactic
Focus :: Name -> Tactic
Defer :: [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 :: (Foldable t, Foldable t1, Eq a) => t1 a -> [(a, TT a)] -> t a -> [(a, TT a)]
keepGiven :: (Foldable t, Foldable t1, Eq a) => t1 a -> [(a, TT a)] -> t 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
data ElabState aux
ES :: (ProofState, aux) -> String -> (Maybe (ElabState aux)) -> ElabState aux
type Elab' aux a = StateT (ElabState aux) TC a
type Elab a = Elab' () a
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 -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
letbind :: Name -> Raw -> Raw -> Elab' aux ()
expandLet :: Name -> Term -> Elab' aux ()
rewrite :: Raw -> Elab' aux ()
induction :: Raw -> Elab' aux ()
casetac :: Raw -> Elab' aux ()
equiv :: Raw -> Elab' aux ()

-- | Turn the current hole into a pattern variable with the provided name,
--   made unique if MN
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 -> 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 -> 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 -> 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 a => [(t2, t1, t, a)] -> [Char]
instance GHC.Show.Show aux => GHC.Show.Show (Idris.Core.Elaborate.ElabState aux)


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.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
toSExp :: SExpable a => a -> SExp
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.Base.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 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 IRTS.System
getDataFileName :: FilePath -> 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 IRTS.Lang
data Endianness
Native :: Endianness
BE :: Endianness
LE :: Endianness
data LVar
Loc :: Int -> LVar
Glob :: Name -> LVar
data LExp
LV :: LVar -> 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 LVar) -> 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
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
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 :: Name -> Int -> [(Name, LDecl)] -> LiftState
lname :: Name -> Int -> Name
liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]
lambdaLift :: Name -> LDecl -> [(Name, LDecl)]
getNextName :: State LiftState Name
addFn :: Name -> LDecl -> State LiftState ()
lift :: [Name] -> LExp -> State LiftState LExp
allocUnique :: LDefs -> (Name, LDecl) -> (Name, LDecl)
usedArg :: (Eq t, Foldable t1) => t1 t -> t -> [t]
usedIn :: [Name] -> LExp -> [Name]
lsubst :: Name -> LExp -> LExp -> LExp
instance GHC.Classes.Eq IRTS.Lang.LDecl
instance GHC.Show.Show IRTS.Lang.LDecl
instance GHC.Classes.Eq IRTS.Lang.LOpt
instance GHC.Show.Show IRTS.Lang.LOpt
instance GHC.Classes.Eq IRTS.Lang.LExp
instance GHC.Base.Functor IRTS.Lang.LAlt'
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.Eq IRTS.Lang.FType
instance GHC.Show.Show IRTS.Lang.FType
instance GHC.Classes.Eq IRTS.Lang.FCallType
instance GHC.Show.Show IRTS.Lang.FCallType
instance GHC.Generics.Generic IRTS.Lang.PrimFn
instance GHC.Classes.Eq IRTS.Lang.PrimFn
instance GHC.Show.Show IRTS.Lang.PrimFn
instance GHC.Classes.Eq IRTS.Lang.ExportIFace
instance GHC.Show.Show IRTS.Lang.ExportIFace
instance GHC.Classes.Eq IRTS.Lang.Export
instance GHC.Show.Show IRTS.Lang.Export
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 IRTS.LangOpts
inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]
nextN :: State Int Name

-- | Inline inside a declaration.
--   
--   Variables are still Name at this stage. Need to preserve uniqueness of
--   variable names in the resulting definition, so invent a new name for
--   every variable we encounter
doInline :: LDefs -> LDecl -> LDecl


module IRTS.JavaScript.AST
data JSType
JSIntTy :: JSType
JSStringTy :: JSType
JSIntegerTy :: JSType
JSFloatTy :: JSType
JSCharTy :: JSType
JSPtrTy :: JSType
JSForgotTy :: JSType
data JSInteger
JSBigZero :: JSInteger
JSBigOne :: JSInteger
JSBigInt :: Integer -> JSInteger
JSBigIntExpr :: JS -> JSInteger
data JSNum
JSInt :: Int -> JSNum
JSFloat :: Double -> JSNum
JSInteger :: JSInteger -> JSNum
data JSWord
JSWord8 :: Word8 -> JSWord
JSWord16 :: Word16 -> JSWord
JSWord32 :: Word32 -> JSWord
JSWord64 :: Word64 -> JSWord
data JSAnnotation
JSConstructor :: JSAnnotation
data JS
JSRaw :: String -> JS
JSIdent :: String -> JS
JSFunction :: [String] -> JS -> JS
JSType :: JSType -> JS
JSSeq :: [JS] -> JS
JSReturn :: JS -> JS
JSApp :: JS -> [JS] -> JS
JSNew :: String -> [JS] -> JS
JSError :: String -> JS
JSBinOp :: String -> JS -> JS -> JS
JSPreOp :: String -> JS -> JS
JSPostOp :: String -> JS -> JS
JSProj :: JS -> String -> JS
JSNull :: JS
JSUndefined :: JS
JSThis :: JS
JSTrue :: JS
JSFalse :: JS
JSArray :: [JS] -> JS
JSString :: String -> JS
JSNum :: JSNum -> JS
JSWord :: JSWord -> JS
JSAssign :: JS -> JS -> JS
JSAlloc :: String -> (Maybe JS) -> JS
JSIndex :: JS -> JS -> JS
JSSwitch :: JS -> [(JS, JS)] -> (Maybe JS) -> JS
JSCond :: [(JS, JS)] -> JS
JSTernary :: JS -> JS -> JS -> JS
JSParens :: JS -> JS
JSWhile :: JS -> JS -> JS
JSFFI :: String -> [JS] -> JS
JSAnnotation :: JSAnnotation -> JS -> JS
JSDelete :: JS -> JS
JSClear :: JS -> JS
JSNoop :: JS
data FFI
FFICode :: Char -> FFI
FFIArg :: Int -> FFI
FFIError :: String -> FFI
ffi :: String -> [String] -> Text
compileJS :: JS -> Text
compileJS' :: Int -> JS -> Text
jsInstanceOf :: JS -> String -> JS
jsOr :: JS -> JS -> JS
jsAnd :: JS -> JS -> JS
jsMeth :: JS -> String -> [JS] -> JS
jsCall :: String -> [JS] -> JS
jsTypeOf :: JS -> JS
jsEq :: JS -> JS -> JS
jsNotEq :: JS -> JS -> JS
jsIsNumber :: JS -> JS
jsIsNull :: JS -> JS
jsBigInt :: JS -> JS
jsUnPackBits :: JS -> JS
jsPackUBits8 :: JS -> JS
jsPackUBits16 :: JS -> JS
jsPackUBits32 :: JS -> JS
jsPackSBits8 :: JS -> JS
jsPackSBits16 :: JS -> JS
jsPackSBits32 :: JS -> JS
instance GHC.Classes.Eq IRTS.JavaScript.AST.JSInteger
instance GHC.Classes.Eq IRTS.JavaScript.AST.JSNum
instance GHC.Classes.Eq IRTS.JavaScript.AST.JS
instance GHC.Classes.Eq IRTS.JavaScript.AST.JSAnnotation
instance GHC.Classes.Eq IRTS.JavaScript.AST.JSWord
instance GHC.Classes.Eq IRTS.JavaScript.AST.JSType
instance GHC.Show.Show IRTS.JavaScript.AST.JSAnnotation


-- | 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 DExp
DV :: LVar -> DExp
DApp :: Bool -> Name -> [DExp] -> DExp
DLet :: Name -> DExp -> DExp -> DExp
DUpdate :: Name -> DExp -> DExp
DProj :: DExp -> Int -> DExp
DC :: (Maybe LVar) -> 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
data DAlt
DConCase :: Int -> Name -> [Name] -> DExp -> DAlt
DConstCase :: Const -> DExp -> DAlt
DDefaultCase :: DExp -> DAlt
data DDecl
DFun :: Name -> [Name] -> DExp -> DDecl
DConstructor :: Name -> Int -> Int -> DDecl
type DDefs = Ctxt DDecl
defunctionalise :: Int -> LDefs -> DDefs
getFn :: [(Name, LDecl)] -> [(Name, Int)]
addApps :: LDefs -> (Name, LDecl) -> State ([Name], [(Name, Int)]) (Name, DDecl)
eEVAL :: DExp -> DExp
data EvalApply a
EvalCase :: (Name -> a) -> EvalApply a
ApplyCase :: a -> EvalApply a
Apply2Case :: a -> EvalApply a
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 :: t -> 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.Inliner
inline :: DDefs -> DDefs
inl :: DDefs -> (Name, DDecl) -> (Name, DDecl)
evalD :: t -> a -> Maybe a


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.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] -> 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]
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.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 -> (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

-- | We may, recursively, collect transformations to do on the rhs, e.g.
--   rewriting recursive calls to functions defined by <tt>with</tt>
[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 -> Bool -> 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 -> Bool
[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 -> 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
data Optimisation

-- | partial eval and associated transforms
PETransform :: Optimisation
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
data LanguageExt
TypeProviders :: LanguageExt
ErrorReflection :: LanguageExt

-- | 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

-- | 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

-- | 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

-- | 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)] -> 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 -> 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)] -> Maybe (Map Name [Name]) -> Maybe (Map Name [Name]) -> [Name] -> [(Name, Bool)] -> Map Name Name -> [Name] -> [(FC, OutputAnnotation)] -> [(FC, OutputAnnotation)] -> Ctxt String -> Set Name -> Map Term (Int, Term) -> Ctxt String -> 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)]
[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]

-- | What was the span of the latest token parsed?
[lastTokenSpan] :: IState -> Maybe FC
[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)]
[idris_whocalls] :: IState -> Maybe (Map Name [Name])
[idris_callswho] :: IState -> Maybe (Map Name [Name])

-- | 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 funtion 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 -> [(FC, OutputAnnotation)]

-- | Highlighting information from the parser
[idris_parserHighlights] :: IState -> [(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
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
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

-- | 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 Codegen
Via :: IRFormat -> String -> Codegen
Bytecode :: Codegen
data IRFormat
IBCFormat :: IRFormat
JSONFormat :: IRFormat
data HowMuchDocs
FullDocs :: HowMuchDocs
OverviewDocs :: HowMuchDocs
data OutputFmt
HTMLOutput :: OutputFmt
LaTeXOutput :: OutputFmt

-- | 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
strLogCat :: LogCat -> String
codegenCats :: [LogCat]
parserCats :: [LogCat]
elabCats :: [LogCat]
loggingCatsStr :: String
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 Opt
Filename :: String -> Opt
Quiet :: Opt
NoBanner :: Opt
ColourREPL :: Bool -> Opt
Idemode :: Opt
IdemodeSocket :: 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
EvalTypes :: Opt
NoCoverage :: Opt
ErrContext :: Opt
ShowImpl :: Opt
Verbose :: 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 %elim
NoElimDeprecationWarnings :: Opt

-- | Don't show deprecation warnings for old-style tactics
NoOldTacticDeprecationWarnings :: Opt
data REPLPort
DontListen :: REPLPort
ListenPort :: PortNumber -> REPLPort
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 -> 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
Exp :: [ArgOpt] -> Static -> Bool -> Plicity
[pargopts] :: Plicity -> [ArgOpt]
[pstatic] :: Plicity -> Static

-- | this is a param (rather than index)
[pparam] :: Plicity -> Bool
Constraint :: [ArgOpt] -> Static -> Plicity
[pargopts] :: Plicity -> [ArgOpt]
[pstatic] :: Plicity -> Static
TacImp :: [ArgOpt] -> Static -> PTerm -> Plicity
[pargopts] :: Plicity -> [ArgOpt]
[pstatic] :: Plicity -> Static
[pscript] :: Plicity -> PTerm
is_scoped :: Plicity -> Maybe ImplicitInfo
impl :: Plicity
impl_gen :: Plicity
forall_imp :: Plicity
forall_constraint :: Plicity
expl :: Plicity
expl_param :: 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

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

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

-- | Unfold given interface name in the definition, the top level methods,
--   and anything which has the interface name as an argument. This is to
--   unfold things for termination checking, as interfaces will otherwise
--   cause problems
UnfoldIface :: Name -> [Name] -> 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] -> [(FC, OutputAnnotation)] -> [Name] -> [(FC, Name)] -> EState
[case_decls] :: EState -> [(Name, PDecl)]
[delayed_elab] :: EState -> [(Int, Elab' EState ())]
[new_tyDecls] :: EState -> [RDeclInstructions]
[highlighting] :: EState -> [(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 -> 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
Induction :: t -> PTactic' t
CaseTac :: t -> 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 -> Name -> FC -> t -> t -> PDo' t
DoLetP :: FC -> t -> 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 :: [t]
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 :: [t]

-- | 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.IOption
instance GHC.Classes.Eq Idris.AbsSyntaxTree.IOption
instance GHC.Show.Show Idris.AbsSyntaxTree.IOption
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Opt
instance GHC.Classes.Eq Idris.AbsSyntaxTree.Opt
instance GHC.Show.Show Idris.AbsSyntaxTree.Opt
instance GHC.Show.Show Idris.AbsSyntaxTree.REPLPort
instance GHC.Generics.Generic Idris.AbsSyntaxTree.REPLPort
instance GHC.Classes.Eq Idris.AbsSyntaxTree.REPLPort
instance GHC.Generics.Generic Idris.AbsSyntaxTree.LogCat
instance GHC.Classes.Ord Idris.AbsSyntaxTree.LogCat
instance GHC.Classes.Eq Idris.AbsSyntaxTree.LogCat
instance GHC.Show.Show Idris.AbsSyntaxTree.LogCat
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Codegen
instance GHC.Classes.Eq Idris.AbsSyntaxTree.Codegen
instance GHC.Show.Show Idris.AbsSyntaxTree.Codegen
instance GHC.Generics.Generic Idris.AbsSyntaxTree.IRFormat
instance GHC.Classes.Eq Idris.AbsSyntaxTree.IRFormat
instance GHC.Show.Show Idris.AbsSyntaxTree.IRFormat
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.DefaultTotality
instance GHC.Classes.Eq Idris.AbsSyntaxTree.DefaultTotality
instance GHC.Show.Show Idris.AbsSyntaxTree.DefaultTotality
instance GHC.Generics.Generic Idris.AbsSyntaxTree.ConsoleWidth
instance GHC.Classes.Eq Idris.AbsSyntaxTree.ConsoleWidth
instance GHC.Show.Show Idris.AbsSyntaxTree.ConsoleWidth
instance GHC.Show.Show Idris.AbsSyntaxTree.OutputMode
instance GHC.Generics.Generic Idris.AbsSyntaxTree.LanguageExt
instance GHC.Classes.Ord Idris.AbsSyntaxTree.LanguageExt
instance GHC.Read.Read Idris.AbsSyntaxTree.LanguageExt
instance GHC.Classes.Eq Idris.AbsSyntaxTree.LanguageExt
instance GHC.Show.Show Idris.AbsSyntaxTree.LanguageExt
instance GHC.Generics.Generic Idris.AbsSyntaxTree.Optimisation
instance GHC.Classes.Eq Idris.AbsSyntaxTree.Optimisation
instance GHC.Show.Show Idris.AbsSyntaxTree.Optimisation
instance GHC.Show.Show Idris.AbsSyntaxTree.PPOption
instance GHC.Classes.Eq Idris.AbsSyntaxTree.ElabWhat
instance GHC.Show.Show Idris.AbsSyntaxTree.ElabWhat
instance GHC.Show.Show Idris.AbsSyntaxTree.IState
instance GHC.Show.Show Idris.AbsSyntaxTree.Fixity
instance GHC.Show.Show Idris.AbsSyntaxTree.FixDecl
instance GHC.Classes.Ord Idris.AbsSyntaxTree.FixDecl
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.AbsSyntaxTree.PTactic' a)
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.AbsSyntaxTree.PDo' a)
instance Util.Pretty.Sized a => Util.Pretty.Sized (Idris.AbsSyntaxTree.PArg' a)
instance GHC.Show.Show Idris.AbsSyntaxTree.PTerm
instance GHC.Show.Show Idris.AbsSyntaxTree.PDecl
instance GHC.Show.Show Idris.AbsSyntaxTree.PClause
instance GHC.Show.Show Idris.AbsSyntaxTree.PData
instance Util.Pretty.Pretty Idris.AbsSyntaxTree.PTerm Idris.Core.TT.OutputAnnotation
instance Util.Pretty.Sized Idris.AbsSyntaxTree.PTerm


-- | 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, 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 Idris.AbsSyntax
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 ()

-- | 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 ()
addErrRev :: (Term, Term) -> 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 ()
getFunctionErrorHandlers :: Name -> Name -> Idris [Name]

-- | 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 ()
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 Bool
setVerbose :: Bool -> 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]
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 ()
expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTerm
expandParamsD :: Bool -> IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
mapsnd :: (t2 -> t1) -> (t, t2) -> (t, t1)
expandImplementationScope :: t3 -> t2 -> [(Name, t1)] -> t -> PDecl' t1 -> PDecl' t1

-- | 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 -> [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])
data EitherErr a b
LeftErr :: a -> EitherErr a b
RightOK :: b -> EitherErr a b
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
getFile :: Opt -> Maybe String
getBC :: Opt -> Maybe String
getOutput :: Opt -> Maybe String
getIBCSubDir :: Opt -> Maybe String
getImportDir :: Opt -> Maybe String
getSourceDir :: Opt -> Maybe String
getPkgDir :: Opt -> Maybe String
getPkg :: Opt -> Maybe (Bool, String)
getPkgClean :: Opt -> Maybe String
getPkgREPL :: Opt -> Maybe String
getPkgCheck :: 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)
getPkgTest :: Opt -> Maybe String
getCodegen :: Opt -> Maybe Codegen
getCodegenArgs :: Opt -> Maybe String
getConsoleWidth :: Opt -> Maybe ConsoleWidth
getExecScript :: Opt -> Maybe String
getPkgIndex :: Opt -> Maybe FilePath
getEvalExpr :: Opt -> Maybe String
getOutputTy :: Opt -> Maybe OutputType
getLanguageExt :: Opt -> Maybe LanguageExt
getTriple :: Opt -> Maybe String
getCPU :: Opt -> Maybe String
getOptLevel :: Opt -> Maybe Int
getOptimisation :: Opt -> Maybe (Bool, Optimisation)
getColour :: Opt -> Maybe Bool
getClient :: Opt -> Maybe String
getPort :: [Opt] -> Maybe REPLPort
opt :: (Opt -> Maybe a) -> [Opt] -> [a]
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.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.Base.Maybe a)
instance Idris.Apropos.Apropos a => Idris.Apropos.Apropos [a]


module Idris.DSL
debindApp :: SyntaxInfo -> PTerm -> PTerm
dslify :: SyntaxInfo -> IState -> PTerm -> PTerm
desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
mkTTName :: FC -> Name -> PTerm
expandSugar :: DSL -> PTerm -> PTerm

-- | Replace DSL-bound variable in a term
var :: DSL -> Name -> PTerm -> Int -> PTerm
unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
debind :: PTerm -> PTerm -> PTerm


module Idris.Elab.AsPat

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


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


module Idris.ErrReverse

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


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

-- | Delaborate a term without resugaring
delab :: IState -> 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] -> 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.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.Output
pshow :: IState -> Err -> String
iWarn :: FC -> Doc OutputAnnotation -> Idris ()
iRender :: Doc a -> Idris (SimpleDoc a)
hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()

-- | Write a pretty-printed term to the console with semantic coloring
consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

-- | Pretty-print a collection of overloadings to REPL or IDEMode -
--   corresponds to :t name
iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
iRenderOutput :: Doc OutputAnnotation -> Idris ()
iRenderResult :: Doc OutputAnnotation -> Idris ()
ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

-- | Write pretty-printed output to IDEMode with semantic annotations
ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

-- | Show an error with semantic highlighting
iRenderError :: Doc OutputAnnotation -> Idris ()
iPrintWithStatus :: String -> String -> Idris ()
iPrintResult :: String -> Idris ()
iPrintError :: String -> Idris ()
iputStrLn :: String -> Idris ()
idemodePutSExp :: SExpable a => String -> a -> Idris ()
iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

-- | Warn about totality problems without failing to compile
warnTotality :: Idris ()
printUndefinedNames :: [Name] -> Doc OutputAnnotation
prettyDocumentedIst :: IState -> (Name, PTerm, Maybe (Docstring DocTerm)) -> Doc OutputAnnotation
sendParserHighlighting :: Idris ()
sendHighlighting :: [(FC, OutputAnnotation)] -> 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 ()
clearHighlights :: Idris ()
renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String
instance System.Console.Haskeline.MonadException.MonadException m => System.Console.Haskeline.MonadException.MonadException (Control.Monad.Trans.Except.ExceptT Idris.Core.TT.Err m)


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

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


module IRTS.Exports
findExports :: Idris [ExportIFace]
getExpNames :: [ExportIFace] -> [Name]


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.
mkPatTm :: PTerm -> Idris Term


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

-- | Get the index file name for a package name
pkgIndex :: String -> FilePath
instance GHC.Classes.Eq Idris.Imports.IFileType
instance GHC.Show.Show Idris.Imports.IFileType


module Idris.Directives

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


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]

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.Parser.Helpers

-- | Idris parser with state used during parsing
type IdrisParser = StateT IState IdrisInnerParser
newtype IdrisInnerParser a
IdrisInnerParser :: Parser a -> IdrisInnerParser a
[runInnerParser] :: IdrisInnerParser a -> Parser a

-- | Generalized monadic parsing constraint type
type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
class HasLastTokenSpan m
getLastTokenSpan :: HasLastTokenSpan m => m (Maybe FC)

-- | Helper to run Idris inner parser based stateT parsers
runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res
highlightP :: FC -> OutputAnnotation -> IdrisParser ()
noDocCommentHere :: String -> IdrisParser ()
clearParserWarnings :: Idris ()
reportParserWarnings :: Idris ()
parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()

-- | Consumes any simple whitespace (any character which satisfies
--   Char.isSpace)
simpleWhiteSpace :: MonadicParsing m => m ()

-- | Checks if a charcter is end of line
isEol :: Char -> Bool

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

-- | Consumes a single-line comment
--   
--   <pre>
--   SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
--   </pre>
singleLineComment :: MonadicParsing m => m ()

-- | Consumes a multi-line comment
--   
--   <pre>
--   MultiLineComment_t ::=
--      '{ -- }'
--    | '{ -' InCommentChars_t
--   ;
--   </pre>
--   
--   <pre>
--   InCommentChars_t ::=
--    '- }'
--    | MultiLineComment_t InCommentChars_t
--    | ~'- }'+ InCommentChars_t
--   ;
--   </pre>
multiLineComment :: MonadicParsing m => m ()

-- | Parses a documentation comment
--   
--   <pre>
--   DocComment_t ::=   <tt>|||</tt> ~EOL_t* EOL_t
--                  ;
--   </pre>
docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])

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

-- | Parses a string literal
stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC)

-- | Parses a char literal
charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC)

-- | Parses a natural number
natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC)

-- | Parses an integral number
integer :: MonadicParsing m => m Integer

-- | Parses a floating point number
float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC)

-- | Idris Style for parsing identifiers/reserved keywords
idrisStyle :: MonadicParsing m => IdentifierStyle m
char :: MonadicParsing m => Char -> m Char
string :: MonadicParsing m => String -> m String

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

-- | Parses a character as a token, returning the source span of the
--   character
lcharFC :: MonadicParsing m => Char -> m FC

-- | Parses string as a token
symbol :: MonadicParsing m => String -> m String
symbolFC :: MonadicParsing m => String -> m FC

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

-- | Parses a reserved identifier, computing its span. Assumes that
--   reserved identifiers never contain line breaks.
reservedFC :: MonadicParsing m => String -> m FC

-- | Parse a reserved identfier, highlighting its span as a keyword
reservedHL :: String -> IdrisParser ()

-- | Parses a reserved operator
reservedOp :: MonadicParsing m => String -> m ()
reservedOpFC :: MonadicParsing m => String -> m FC

-- | Parses an identifier as a token
identifier :: (MonadicParsing m) => m (String, FC)

-- | Parses an identifier with possible namespace as a name
iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)

-- | Parses an string possibly prefixed by a namespace
maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

-- | Parses a name
name :: IdrisParser (Name, FC)

-- | List of all initial segments in ascending order of a list. Every such
--   initial segment ends right before an element satisfying the given
--   condition.
initsEndAt :: (a -> Bool) -> [a] -> [[a]]

-- | Create a <a>Name</a> from a pair of strings representing a base name
--   and its namespace.
mkName :: (String, String) -> Name
opChars :: String
operatorLetter :: MonadicParsing m => m Char
commentMarkers :: [String]
invalidOperators :: [String]

-- | Parses an operator
operator :: MonadicParsing m => m String

-- | Parses an operator
operatorFC :: MonadicParsing m => m (String, FC)

-- | Get filename from position (returns "(interactive)" when no source
--   file is given)
fileName :: Delta -> String

-- | Get line number from position
lineNum :: Delta -> Int

-- | Get column number from position
columnNum :: Delta -> Int

-- | Get file position as FC
getFC :: MonadicParsing m => m FC

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

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

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

-- | Pops indentation from stack
popIndent :: IdrisParser ()

-- | Gets current indentation
indent :: IdrisParser Int

-- | Gets last indentation
lastIndent :: IdrisParser Int

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

-- | 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

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

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

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

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

-- | Parses and keeps a terminator
keepTerminator :: IdrisParser ()

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

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

-- | Representation of an operation that can compare the current
--   indentation with the last indentation, and an error message if it
--   fails
data IndentProperty
IndentProperty :: (Int -> Int -> Bool) -> String -> IndentProperty

-- | Allows comparison of indent, and fails if property doesn't hold
indentPropHolds :: IndentProperty -> IdrisParser ()

-- | Greater-than indent property
gtProp :: IndentProperty

-- | Greater-than or equal to indent property
gteProp :: IndentProperty

-- | Equal indent property
eqProp :: IndentProperty

-- | Less-than indent property
ltProp :: IndentProperty

-- | Less-than or equal to indent property
lteProp :: IndentProperty

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

-- | Parses an accessibilty modifier (e.g. public, private)
accessibility' :: IdrisParser Accessibility
accessibility :: IdrisParser Accessibility

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

-- | 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 ()

-- | Error message with possible fixes list
fixErrorMsg :: String -> [String] -> String

-- | Collect <a>PClauses</a> with the same function name
collect :: [PDecl] -> [PDecl]
instance Text.Parser.Token.TokenParsing Idris.Parser.Helpers.IdrisInnerParser
instance GHC.Base.Monoid a => GHC.Base.Monoid (Idris.Parser.Helpers.IdrisInnerParser a)
instance Text.Trifecta.Combinators.MarkParsing Text.Trifecta.Delta.Delta Idris.Parser.Helpers.IdrisInnerParser
instance Text.Trifecta.Combinators.DeltaParsing Idris.Parser.Helpers.IdrisInnerParser
instance Text.Parser.LookAhead.LookAheadParsing Idris.Parser.Helpers.IdrisInnerParser
instance Text.Parser.Char.CharParsing Idris.Parser.Helpers.IdrisInnerParser
instance GHC.Base.Alternative Idris.Parser.Helpers.IdrisInnerParser
instance GHC.Base.Applicative Idris.Parser.Helpers.IdrisInnerParser
instance GHC.Base.MonadPlus Idris.Parser.Helpers.IdrisInnerParser
instance GHC.Base.Functor Idris.Parser.Helpers.IdrisInnerParser
instance GHC.Base.Monad Idris.Parser.Helpers.IdrisInnerParser
instance Text.Parser.Combinators.Parsing Idris.Parser.Helpers.IdrisInnerParser
instance Text.Trifecta.Combinators.DeltaParsing Idris.Parser.Helpers.IdrisParser
instance Text.Parser.Token.TokenParsing Idris.Parser.Helpers.IdrisParser
instance Idris.Parser.Helpers.HasLastTokenSpan Idris.Parser.Helpers.IdrisParser


module Idris.Parser.Ops

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

-- | Calculates table for fixity declarations
toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

-- | Binary operator
binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm

-- | Prefix operator
prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm

-- | Backtick operator
backtick :: Operator IdrisParser PTerm

-- | Operator without fixity (throws an error)
nofixityoperator :: Operator IdrisParser PTerm

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

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

-- | 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' | <a>prefix</a> ;
--   </tt>
fixityType :: IdrisParser (Int -> Fixity)


module Idris.Parser.Expr

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

-- | Disallow implicit type declarations
disallowImp :: 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

-- | 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 IdrisInnerParser (FC, 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 :: (LookAheadParsing m, DeltaParsing m) => [ArgOpt] -> Static -> t -> m Plicity
explicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm
autoImplicit :: t -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm
defaultImplicit :: t -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm
normalImplicit :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm
constraintPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm
implicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm
unboundPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm
unboundPiNoConstraint :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser 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 [(Name, FC, PTerm)]
constraintList1 :: SyntaxInfo -> IdrisParser [(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 [(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 [(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 | Name '&lt;-' Expr | Expr'
--   '&lt;-' Expr | Expr ; </tt>
do_ :: SyntaxInfo -> IdrisParser PDo
do_alt :: SyntaxInfo -> StateT IState IdrisInnerParser (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 :: IdrisParser (Const, FC)

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

-- | 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
--          |   <a>try</a>         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

-- | Parses if a data should not have a default eliminator
--   DefaultEliminator ::= <tt>noelim</tt>?
dataOpts :: DataOpts -> IdrisParser DataOpts

-- | Parses a data type declaration Data ::= DocComment? Accessibility?
--   DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest? |
--   DocComment? Accessibility? DataI DefaultEliminator 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.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.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 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.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.Termination

-- | 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 ()

-- | 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

-- | Calculate the totality of a function from its patterns. Either follow
--   the size change graph (if inductive) or check for productivity (if
--   coinductive)
calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
checkTotality :: [Name] -> FC -> Name -> Idris Totality
checkDeclTotality :: (FC, Name) -> Idris Totality
verifyTotality :: (FC, Name) -> Idris ()

-- | 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 ()
delazy :: TT Name -> TT Name
delazy' :: Bool -> TT Name -> TT Name
data Guardedness
Toplevel :: Guardedness
Unguarded :: Guardedness
Guarded :: Guardedness
Delayed :: Guardedness
buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
checkSizeChange :: Name -> Idris Totality
type MultiPath = [SCGEntry]
mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
checkMP :: IState -> Name -> Int -> MultiPath -> Totality
allNothing :: [Maybe a] -> Bool
collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
noPartial :: [Totality] -> Totality
collapse :: [Totality] -> Totality
collapse' :: Totality -> [Totality] -> Totality
totalityCheckBlock :: Idris ()
instance GHC.Show.Show Idris.Termination.Guardedness


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.WhoCalls
whoCalls :: Name -> Idris [(Name, [Name])]
callsWho :: Name -> Idris [(Name, [Name])]


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


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.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.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.Package.Common

-- | Description of an Idris package.
data PkgDesc
PkgDesc :: String -> [String] -> 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 -> String

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

-- | 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.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.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.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
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
Spec :: PTerm -> Command
WHNF :: PTerm -> Command
TestInline :: PTerm -> Command
Defn :: Name -> Command
Missing :: Name -> Command
DynamicLink :: FilePath -> Command
ListDynamic :: Command
Pattelab :: PTerm -> Command
Search :: [String] -> 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 :: [String] -> String -> Command
WhoCalls :: Name -> Command
CallsWho :: Name -> Command
Browse :: [String] -> Command
MakeDoc :: String -> Command
Warranty :: Command
PrintDef :: Name -> Command
PPrint :: OutputFmt -> Int -> PTerm -> Command
TransformInfo :: Name -> Command
DebugInfo :: Name -> Command
DebugUnify :: PTerm -> PTerm -> Command


module Idris.Reflection
data RErasure
RErased :: RErasure
RNotErased :: RErasure
data RPlicity
RExplicit :: RPlicity
RImplicit :: RPlicity
RConstraint :: RPlicity
data RFunArg
RFunArg :: Name -> Raw -> RPlicity -> RErasure -> RFunArg
[argName] :: RFunArg -> Name
[argTy] :: RFunArg -> Raw
[argPlicity] :: RFunArg -> RPlicity
[erasure] :: RFunArg -> RErasure
data RTyDecl
RDeclare :: Name -> [RFunArg] -> Raw -> RTyDecl
data RTyConArg
RParameter :: RFunArg -> RTyConArg
RIndex :: RFunArg -> RTyConArg
data RCtorArg
RCtorParameter :: RFunArg -> RCtorArg
RCtorField :: RFunArg -> RCtorArg
data RDatatype
RDatatype :: Name -> [RTyConArg] -> Raw -> [(Name, [RCtorArg], Raw)] -> RDatatype
data RConstructorDefn
RConstructor :: Name -> [RFunArg] -> Raw -> RConstructorDefn
data RDataDefn
RDefineDatatype :: Name -> [RConstructorDefn] -> RDataDefn
rArgOpts :: RErasure -> [ArgOpt]
rFunArgToPArg :: RFunArg -> PArg
data RFunClause a
RMkFunClause :: a -> a -> RFunClause a
RMkImpossibleClause :: a -> RFunClause a
data RFunDefn a
RDefineFun :: Name -> [RFunClause a] -> RFunDefn a

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

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

-- | Reify tactics from their reflected representation
reify :: IState -> Term -> ElabD PTactic
reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
reifyBool :: Term -> ElabD Bool
reifyInt :: Term -> ElabD Int
reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]
reifyReportParts :: Term -> ElabD [ErrorReportPart]

-- | Reify terms from their reflected representation
reifyTT :: Term -> ElabD Term
reifyTTApp :: Name -> [Term] -> ElabD Term
reifyUniverse :: Term -> ElabD Universe

-- | Reify raw terms from their reflected representation
reifyRaw :: Term -> ElabD Raw
reifyRawApp :: Name -> [Term] -> ElabD Raw
reifyTTName :: Term -> ElabD Name
reifyTTNameApp :: Name -> [Term] -> ElabD Name
reifyTTNamespace :: Term -> ElabD [String]
reifyTTNameType :: Term -> ElabD NameType
reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
reifyTTConst :: Term -> ElabD Const
reifyTTConstApp :: Name -> Term -> ElabD Const
reifyArithTy :: Term -> ElabD ArithTy
reifyNativeTy :: Term -> ElabD NativeTy
reifyIntTy :: Term -> ElabD IntTy
reifyTTUExp :: Term -> ElabD UExp

-- | Create a reflected call to a named function/constructor
reflCall :: String -> [Raw] -> Raw

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

-- | Lift a term into its Language.Reflection.Raw representation
reflectRaw :: Raw -> Raw
claimTy :: Name -> Raw -> ElabD Name
intToReflectedNat :: Int -> Raw
reflectFixity :: Fixity -> 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 ()
reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
reflectUniverse :: Universe -> Raw

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

-- | Elaborate a name to a pattern. This means that NS and UN will be
--   intact. MNs corresponding to will care about the string but not the
--   number. All others become _.
reflectNameQuotePattern :: Name -> ElabD ()
reflectBinder :: Binder Term -> Raw
reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
mkList :: Raw -> [Raw] -> Raw
reflectConstant :: Const -> Raw
reflectUExp :: UExp -> Raw

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

-- | Reflect an error into the internal datatype of Idris -- TODO
rawBool :: Bool -> Raw
rawNil :: Raw -> Raw
rawCons :: Raw -> Raw -> Raw -> Raw
rawList :: Raw -> [Raw] -> Raw
rawPairTy :: Raw -> Raw -> Raw
rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

-- | Idris tuples nest to the right
rawTripleTy :: Raw -> Raw -> Raw -> Raw
rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
reflectCtxt :: [(Name, Type)] -> Raw
reflectErr :: Err -> Raw

-- | Reflect a file context
reflectFC :: FC -> Raw
reifyFC :: Term -> ElabD FC
fromTTMaybe :: Term -> Maybe Term
reflErrName :: String -> Name

-- | 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
reifyErasure :: Term -> ElabD RErasure
reifyPlicity :: Term -> ElabD RPlicity
reifyRFunArg :: Term -> ElabD RFunArg
reifyTyDecl :: Term -> ElabD RTyDecl
reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
reifyRConstructorDefn :: Term -> ElabD RConstructorDefn
reifyRDataDefn :: Term -> ElabD RDataDefn
envTupleType :: Raw
reflectList :: Raw -> [Raw] -> Raw

-- | 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)
unApplyRaw :: Raw -> (Raw, [Raw])

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

-- | Build the reflected datatype definition(s) that correspond(s) to a
--   provided unqualified name
buildDatatypes :: IState -> Name -> [RDatatype]
reflectErasure :: RErasure -> Raw
reflectPlicity :: RPlicity -> Raw
reflectArg :: RFunArg -> Raw
reflectCtorArg :: RCtorArg -> Raw
reflectDatatype :: RDatatype -> Raw
reflectFunClause :: RFunClause Term -> Raw
reflectFunDefn :: RFunDefn Term -> Raw
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.CmdOptions
runArgParser :: IO [Opt]
pureArgParser :: [String] -> [Opt]
parser :: Parser [Opt]
parseFlags :: Parser [Opt]
parseVersion :: Parser (a -> a)
preProcOpts :: [Opt] -> [Opt]
parseCodegen :: String -> Codegen
parseLogCats :: Monad m => String -> m [LogCat]
parseConsoleWidth :: Monad m => String -> m ConsoleWidth
integerReader :: ReadP Int
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


module Idris.DeepSeq
instance Control.DeepSeq.NFData Cheapskate.Types.Options
instance Control.DeepSeq.NFData Cheapskate.Types.ListType
instance Control.DeepSeq.NFData Cheapskate.Types.CodeAttr
instance Control.DeepSeq.NFData Cheapskate.Types.NumWrapper
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.AbsSyntaxTree.ConsoleWidth
instance Control.DeepSeq.NFData IRTS.Lang.PrimFn
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.SyntaxRules
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.Opt
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.REPLPort
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.TIData
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.IOption
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.LanguageExt
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.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.AbsSyntaxTree.Codegen
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.IRFormat
instance Control.DeepSeq.NFData Idris.AbsSyntaxTree.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


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 t -> [(t, TT t)]
psolve :: TT t -> 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 :: (Eq t1, Foldable t) => [TT t1] -> t t1 -> [Int] -> [t1]
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


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] -> [(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 -> [(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]
pruneByType :: Bool -> Env -> Term -> Type -> IState -> [PTerm] -> [PTerm]
isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

-- | 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
case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

-- | 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.Transform
elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)


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 ()), then printing it as an
--   Integer (as a default numeric tye), then printing it as any Showable
--   thing
elabExec :: FC -> PTerm -> PTerm
elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)


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


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.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]
getUnfolds :: [FnOpt] -> Maybe (Name, [Name])
getNamesToUnfold :: Name -> [Name] -> 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.Elab.Data
elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> 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.Interface
elabInterface :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> 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.Provider

-- | Elaborate a type provider
elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> 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.ElabDecls

-- | Top level elaborator info, supporting recursive elaboration
recinfo :: FC -> ElabInfo

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

-- | Elaborate primitives
elabPrims :: Idris ()
elabDecls :: ElabInfo -> [PDecl] -> Idris ()
elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' :: ElabWhat -> ElabInfo -> PDecl -> StateT IState (ExceptT Err IO) ()


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

-- | Load an entire package from its index file
loadPkgIndex :: String -> 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
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 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.AbsSyntaxTree.Codegen
instance Data.Binary.Class.Binary Idris.AbsSyntaxTree.IRFormat


module Idris.Parser

-- | Parses module definition
--   
--   <pre>
--   ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
--   </pre>
moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
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 an import statement
--   
--   <pre>
--   Import ::= 'import' Identifier_t ';'?;
--   </pre>
import_ :: IdrisParser ImportInfo

-- | Parses program source
--   
--   <pre>
--   Prog ::= Decl* EOF;
--   </pre>
prog :: SyntaxInfo -> IdrisParser [PDecl]

-- | 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]
internalDecl :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a top-level declaration with possible syntax sugar
--   
--   <pre>
--   Decl' ::=
--       Fixity
--     | FunDecl'
--     | Data
--     | Record
--     | SyntaxDecl
--     ;
--   </pre>
decl' :: SyntaxInfo -> IdrisParser PDecl
externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser [PDecl]

-- | Parses a syntax extension declaration (and adds the rule to parser
--   state)
--   
--   <pre>
--   SyntaxDecl ::= SyntaxRule;
--   </pre>
syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

-- | Extend an <a>IState</a> with a new syntax extension. See also
--   <a>addReplSyntax</a>.
addSyntax :: IState -> Syntax -> IState

-- | Like <a>addSyntax</a>, but no effect on the IBC.
addReplSyntax :: IState -> Syntax -> IState

-- | Parses a syntax extension declaration
--   
--   <pre>
--   SyntaxRuleOpts ::= <tt>term</tt> | <a>pattern</a>;
--   </pre>
--   
--   <pre>
--   SyntaxRule ::=
--     SyntaxRuleOpts? <tt>syntax</tt> SyntaxSym+ '=' TypeExpr Terminator;
--   </pre>
--   
--   <pre>
--   SyntaxSym ::=   '[' Name_t ']'
--                |  '{' Name_t '}'
--                |  Name_t
--                |  StringLiteral_t
--                ;
--   </pre>
syntaxRule :: SyntaxInfo -> IdrisParser Syntax

-- | Parses a syntax symbol (either binding variable, keyword or
--   expression)
--   
--   <pre>
--   SyntaxSym ::=   '[' Name_t ']'
--                |  '{' Name_t '}'
--                |  Name_t
--                |  StringLiteral_t
--                ;
--   </pre>
syntaxSym :: IdrisParser SSymbol

-- | Parses a function declaration with possible syntax sugar
--   
--   <pre>
--   FunDecl ::= FunDecl';
--   </pre>
fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a function declaration
--   
--   <pre>
--   FunDecl' ::=
--    DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
--    | Postulate
--    | Pattern
--    | CAF
--    ;
--   </pre>
fnDecl' :: SyntaxInfo -> IdrisParser PDecl

-- | Parses a series of function and accessbility options
--   
--   <pre>
--   FnOpts ::= FnOpt* Accessibility FnOpt*
--   </pre>
fnOpts :: IdrisParser ([FnOpt], Accessibility)

-- | Parses a function option
--   
--   <pre>
--   FnOpt ::= <tt>total</tt>
--     | <tt>partial</tt>
--     | <tt>covering</tt>
--     | <a>implicit</a>
--     | <tt>%</tt> <tt>no_implicit</tt>
--     | <tt>%</tt> <tt>assert_total</tt>
--     | <tt>%</tt> <tt>error_handler</tt>
--     | <tt>%</tt> <tt>reflection</tt>
--     | <tt>%</tt> <a>specialise</a> '[' NameTimesList? ']'
--     ;
--   </pre>
--   
--   <pre>
--   NameTimes ::= FnName Natural?;
--   </pre>
--   
--   <pre>
--   NameTimesList ::=
--     NameTimes
--     | NameTimes ',' NameTimesList
--     ;
--   </pre>
fnOpt :: IdrisParser FnOpt

-- | Parses a postulate
--   
--   <pre>
--   Postulate ::=
--     DocComment_t? <a>postulate</a> FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
--     ;
--   </pre>
postulate :: SyntaxInfo -> IdrisParser PDecl

-- | Parses a using declaration
--   
--   <pre>
--   Using ::=
--     <a>using</a> '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
--     ;
--   </pre>
using_ :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a parameters declaration
--   
--   <pre>
--   Params ::=
--     <tt>parameters</tt> '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
--     ;
--   </pre>
params :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses an open block
openInterface :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a mutual declaration (for mutually recursive functions)
--   
--   <pre>
--   Mutual ::=
--     <a>mutual</a> OpenBlock Decl* CloseBlock
--     ;
--   </pre>
mutual :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a namespace declaration
--   
--   <pre>
--   Namespace ::=
--     <a>namespace</a> identifier OpenBlock Decl+ CloseBlock
--     ;
--   </pre>
namespace :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a methods block (for implementations)
--   
--   <pre>
--   ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock
--   </pre>
implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a methods and implementations block (for interfaces)
--   
--   <pre>
--   MethodOrImplementation ::=
--      FnDecl
--      | Implementation
--      ;
--   </pre>
--   
--   <pre>
--   InterfaceBlock ::=
--     'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
--     ;
--   </pre>
interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

-- | Parses an interface declaration
--   
--   <pre>
--   InterfaceArgument ::=
--      Name
--      | '(' Name <tt>:</tt> Expr ')'
--      ;
--   </pre>
--   
--   <pre>
--   Interface ::=
--     DocComment_t? Accessibility? <tt>interface</tt> ConstraintList? Name InterfaceArgument* InterfaceBlock?
--     ;
--   </pre>
interface_ :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses an interface implementation declaration
--   
--   <pre>
--   Implementation ::=
--     DocComment_t? <a>implementation</a> ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
--     ;
--   </pre>
--   
--   <pre>
--   ImplementationName ::= '[' Name ']';
--   </pre>
implementation :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

-- | Parse a docstring
docstring :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))])

-- | Parses a using declaration list
--   
--   <pre>
--   UsingDeclList ::=
--     UsingDeclList'
--     | NameList TypeSig
--     ;
--   </pre>
--   
--   <pre>
--   UsingDeclList' ::=
--     UsingDecl
--     | UsingDecl ',' UsingDeclList'
--     ;
--   </pre>
--   
--   <pre>
--   NameList ::=
--     Name
--     | Name ',' NameList
--     ;
--   </pre>
usingDeclList :: SyntaxInfo -> IdrisParser [Using]

-- | Parses a using declaration
--   
--   <pre>
--   UsingDecl ::=
--     FnName TypeSig
--     | FnName FnName+
--     ;
--   </pre>
usingDecl :: SyntaxInfo -> IdrisParser Using

-- | Parse a clause with patterns
--   
--   <pre>
--   Pattern ::= Clause;
--   </pre>
pattern :: SyntaxInfo -> IdrisParser PDecl

-- | Parse a constant applicative form declaration
--   
--   <pre>
--   CAF ::= 'let' FnName '=' Expr Terminator;
--   </pre>
caf :: SyntaxInfo -> IdrisParser PDecl

-- | Parse an argument expression
--   
--   <pre>
--   ArgExpr ::= HSimpleExpr | ;
--   </pre>
argExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parse a right hand side of a function
--   
--   <pre>
--   RHS ::= '='            Expr
--        |  <tt>?=</tt>  RHSName? Expr
--        |  Impossible
--        ;
--   </pre>
--   
--   <pre>
--   RHSName ::= '{' FnName '}';
--   </pre>
rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

-- | Parses a function clause
--   
--   <pre>
--   RHSOrWithBlock ::= RHS WhereOrTerminator
--                  | <tt>with</tt> SimpleExpr OpenBlock FnDecl+ CloseBlock
--                  ;
--   </pre>
--   
--   <pre>
--   Clause ::=                                                               WExpr+ RHSOrWithBlock
--          |   SimpleExpr <tt>&lt;==</tt>  FnName                                             RHS WhereOrTerminator
--          |   ArgExpr Operator ArgExpr                                      WExpr* RHSOrWithBlock 
--          |                     FnName ConstraintArg* ImplicitOrArgExpr*    WExpr* RHSOrWithBlock
--          ;
--   </pre>
--   
--   <pre>
--   ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
--   </pre>
--   
--   <pre>
--   WhereOrTerminator ::= WhereBlock | Terminator;
--   </pre>
clause :: SyntaxInfo -> IdrisParser PClause

-- | Parses with pattern
--   
--   <pre>
--   WExpr ::= '|' Expr';
--   </pre>
wExpr :: SyntaxInfo -> IdrisParser PTerm

-- | Parses a where block
--   
--   <pre>
--   WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
--   </pre>
whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])

-- | Parses a code generation target language name
--   
--   <pre>
--   Codegen ::= <tt>C</tt>
--           |   <tt>Java</tt>
--           |   <tt>JavaScript</tt>
--           |   <tt>Node</tt>
--           |   <tt>LLVM</tt>
--           |   <a>Bytecode</a>
--           ;
--   </pre>
codegen_ :: IdrisParser Codegen

-- | Parses a compiler directive <tt> StringList ::= String | String ','
--   StringList ; </tt>
--   
--   <pre>
--   Directive ::= <tt>%</tt> Directive';
--   </pre>
--   
--   <pre>
--   Directive' ::= <tt>lib</tt>            CodeGen String_t
--              |   <tt>link</tt>           CodeGen String_t
--              |   <tt>flag</tt>           CodeGen String_t
--              |   <tt>include</tt>        CodeGen String_t
--              |   <tt>hide</tt>           Name
--              |   <tt>freeze</tt>         Name
--              |   <tt>thaw</tt>           Name
--              |   <tt>access</tt>         Accessibility
--              |   'default'        Totality
--              |   <tt>logging</tt>        Natural
--              |   <tt>dynamic</tt>        StringList
--              |   <a>name</a>           Name NameList
--              |   <tt>error_handlers</tt> Name NameList
--              |   <tt>language</tt>       <a>TypeProviders</a>
--              |   <tt>language</tt>       <a>ErrorReflection</a>
--              |   <tt>deprecated</tt> Name String
--              |   <tt>fragile</tt>    Name Reason
--              ;
--   </pre>
directive :: SyntaxInfo -> IdrisParser [PDecl]
pLangExt :: IdrisParser LanguageExt

-- | Parses a totality
--   
--   <pre>
--   Totality ::= <tt>partial</tt> | <tt>total</tt> | <tt>covering</tt>
--   </pre>
totality :: IdrisParser DefaultTotality

-- | Parses a type provider
--   
--   <pre>
--   Provider ::= DocComment_t? <tt>%</tt> <tt>provide</tt> Provider_What? '(' FnName TypeSig ')' <tt>with</tt> Expr;
--   ProviderWhat ::= <tt>proof</tt> | <tt>term</tt> | 'type' | <a>postulate</a>
--   </pre>
provider :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a transform
--   
--   <pre>
--   Transform ::= <tt>%</tt> <a>transform</a> Expr <tt>==&gt;</tt> Expr
--   </pre>
transform :: SyntaxInfo -> IdrisParser [PDecl]

-- | Parses a top-level reflected elaborator script
--   
--   <pre>
--   RunElabDecl ::= <tt>%</tt> <a>runElab</a> Expr
--   </pre>
runElabDecl :: SyntaxInfo -> IdrisParser PDecl

-- | Parses an expression from input
parseExpr :: IState -> String -> Result PTerm

-- | Parses a constant form input
parseConst :: IState -> String -> Result Const

-- | Parses a tactic from input
parseTactic :: IState -> String -> Result PTactic

-- | Parses a do-step from input (used in the elab shell)
parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)

-- | Parse module header and imports
parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)

-- | There should be a better way of doing this...
findFC :: Doc -> (FC, String)

-- | Check if the coloring matches the options and corrects if necessary
fixColour :: Bool -> Doc -> Doc

-- | A program is a list of declarations, possibly with associated
--   documentation strings.
parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta -> Idris [PDecl]

-- | Load idris module and show error if something wrong happens
loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)

-- | Load idris module
loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)

-- | Load idris code from file
loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

-- | Load idris source code and show error if something wrong happens
loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()

-- | Load Idris source code
loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

-- | Adds names to hide list
addHides :: Ctxt Accessibility -> Idris ()


-- | 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 -> 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.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


module Idris.ModeCommon
defaultPort :: PortNumber
loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
banner :: [Char]
warranty :: [Char]


module Idris.REPL.Parser
parseCmd :: IState -> String -> String -> Result (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.TypeSearch
searchByType :: [String] -> 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.Monoid a => GHC.Base.Monoid (Idris.TypeSearch.Sided a)
instance GHC.Base.Monoid Idris.TypeSearch.AsymMods
instance GHC.Base.Monoid Idris.TypeSearch.Score


module Idris.Prover

-- | Launch the proof shell
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
showProof :: Bool -> Name -> [String] -> String
showRunElab :: Bool -> Name -> [String] -> String


-- | 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 :: t -> 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.CodegenC
codegenC :: CodeGenerator


module IRTS.CodegenJavaScript
codegenJavaScript :: CodeGenerator
codegenNode :: CodeGenerator
data JSTarget
Node :: JSTarget
JavaScript :: JSTarget
instance GHC.Classes.Eq IRTS.CodegenJavaScript.JSTarget


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 ()


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


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.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.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 ()
buildMods :: [Opt] -> [Name] -> IO (Maybe IState)
testLib :: Bool -> String -> String -> IO Bool
rmIBC :: Name -> IO ()
rmIdx :: String -> IO ()
rmExe :: String -> IO ()
toIBCFile :: Name -> String
installIBC :: String -> String -> Name -> IO ()
installIdx :: String -> String -> IO ()
installObj :: String -> String -> String -> IO ()
mkDirCmd :: [Char]
inPkgDir :: PkgDesc -> IO a -> IO a

-- | 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]


module IRTS.BCImp
data Reg
RVal :: Reg
L :: Int -> Reg
data BC
NOP :: BC
toBC :: (Name, SDecl) -> (Name, [BC])
bc :: Reg -> SExp -> [BC]