Idris.Elab.Term

Documentation

data ElabMode

Constructors

ETyDecl

ETransLHS

ELHS

ERHS

Instances

Eq ElabMode

Methods

(==) :: ElabMode -> ElabMode -> Bool

(/=) :: ElabMode -> ElabMode -> Bool

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

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

buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> [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)

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

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.

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 -> Type -> 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 :: [String] -> Name -> Name

Compute the appropriate name for a top-level metavariable

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

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

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