Idris.Elab.Term

Documentation

data ElabMode

Constructors

ETyDecl

ETransLHS

ELHS

ERHS

Instances

Eq ElabMode

data ElabResult

Constructors

ElabResult

Fields

resultTerm :: Term

The term resulting from elaboration

resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]

Information about new metavariables

resultCaseDecls :: [PDecl]

Deferred declarations as the meaning of case blocks

resultContext :: Context

The potentially extended context from new definitions

resultTyDecls :: [RDeclInstructions]

Meta-info about the new type declarations

resultHighlighting :: [(FC, OutputAnnotation)]

Saved highlights from elaboration

resultName :: Int

The new global name counter

build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult

buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> [Name] -> PTerm -> ElabD ElabResult

getUnmatchable :: Context -> Name -> [Bool]

data ElabCtxt

Constructors

ElabCtxt

Fields

e_inarg :: Bool

e_isfn :: Bool

Function part of application

e_guarded :: Bool

e_intype :: Bool

e_qq :: Bool

e_nomatching :: Bool

can't pattern match

initElabCtxt :: ElabCtxt

goal_polymorphic :: ElabD Bool

elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ()

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)

pruneAlt :: [PTerm] -> [PTerm]

pruneByType :: Env -> Term -> IState -> [PTerm] -> [PTerm]

isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

findHighlight :: Name -> ElabD OutputAnnotation

Use the local elab context to work out the highlighting for a name

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

metavarName :: Maybe [String] -> Name -> Name

Compute the appropriate name for a top-level metavariable

runElabAction :: 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 :: Elab' aux ()

processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()

Do the left-over work after creating declarations in reflected elaborator scripts