| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.Elab.Term
Description
- data ElabMode
- = ETyDecl
- | ETransLHS
- | ELHS
- | EImpossible
- | ERHS
- data ElabResult = ElabResult {
- resultTerm :: Term
- resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]
- resultCaseDecls :: [PDecl]
- resultContext :: Context
- resultTyDecls :: [RDeclInstructions]
- resultHighlighting :: [(FC, OutputAnnotation)]
- resultName :: Int
- 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 = ElabCtxt {}
- initElabCtxt :: ElabCtxt
- goal_polymorphic :: ElabD Bool
- elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ()
- pruneAlt :: [PTerm] -> [PTerm]
- 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
- 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 ()
- processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()
Documentation
Constructors
| ETyDecl | |
| ETransLHS | |
| ELHS | |
| EImpossible | |
| ERHS |
data ElabResult Source #
Constructors
| ElabResult | |
Fields
| |
build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult Source #
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 Source #
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] Source #
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.
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)
findHighlight :: Name -> ElabD OutputAnnotation Source #
Use the local elab context to work out the highlighting for a name
proofSearch' :: IState -> Bool -> Bool -> Int -> Bool -> Maybe Name -> Name -> [Name] -> [Name] -> StateT (ElabState EState) TC () Source #
collectDeferred :: Maybe Name -> [Name] -> Context -> Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term Source #
metavarName :: [String] -> Name -> Name Source #
Compute the appropriate name for a top-level metavariable
withErrorReflection :: Idris a -> Idris a Source #
processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris () Source #
Do the left-over work after creating declarations in reflected elaborator scripts