Safe Haskell	None
Language	Haskell98

Idris.Elab.Term

Synopsis

Documentation

data ElabMode Source

Constructors

ETyDecl
ELHS
ERHS

Instances

Eq ElabMode

data ElabResult Source

Constructors

ElabResult

Fields

resultTerm :: Term: The term resulting from elaboration
resultMetavars :: [(Name, (Int, Maybe Name, Type))]: 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)]

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

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

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

data ElabCtxt Source

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 Source

goal_polymorphic :: ElabD Bool Source

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

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

pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm] Source

findHighlight :: Name -> ElabD OutputAnnotation Source

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

findInstances :: IState -> Term -> [Name] Source

Find the names of instances that have been designeated for searching (i.e. non-named instances or instances from Elab scripts)

solveAuto :: IState -> Name -> Bool -> Name -> ElabD () Source

solveAutos :: IState -> Name -> Bool -> ElabD () Source

trivial' :: IState -> ElabD () Source

trivialHoles' :: [(Name, Int)] -> IState -> ElabD () Source

proofSearch' :: IState -> Bool -> Bool -> Int -> Bool -> Maybe Name -> Name -> [Name] -> StateT (ElabState EState) TC () Source

resolveTC Source

Arguments

:: Bool	using default Int
-> Bool	allow metavariables in the goal
-> Int	depth
-> Term	top level goal, for error messages
-> Name	top level function name, to prevent loops
-> IState
-> ElabD ()

Resolve type classes. This will only pick up normal instances, never named instances (which is enforced by findInstances).

resTC' :: (Num a, Eq a) => [TT Name] -> Bool -> [Name] -> a -> Term -> Name -> IState -> StateT (ElabState EState) TC () Source

collectDeferred :: Maybe Name -> [Name] -> Context -> Term -> State [(Name, (Int, Maybe Name, Type))] Term Source

case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD () Source

runTactical :: IState -> FC -> Env -> Term -> ElabD () Source

runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD () Source

elaboratingArgErr :: [(Name, Name)] -> Err -> Err Source

withErrorReflection :: Idris a -> Idris a Source

solveAll :: Elab' aux () Source

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

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