| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.Core.Elaborate
Description
This is our interface to proof construction, rather than ProofState, because this gives us a language to build derived tactics out of the primitives.
- data ElabState aux = ES (ProofState, aux) String (Maybe (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 ()
- 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)
- updateAux :: (aux -> aux) -> Elab' aux ()
- getAux :: Elab' aux aux
- unifyLog :: Bool -> Elab' aux ()
- getUnifyLog :: Elab' aux Bool
- 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_context :: Elab' aux Context
- 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_term :: Elab' aux Term
- update_term :: (Term -> Term) -> Elab' aux ()
- 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
- get_recents :: Elab' aux [Name]
- goal :: Elab' aux Type
- is_guess :: Elab' aux Bool
- get_guess :: Elab' aux Term
- get_type :: Raw -> Elab' aux Type
- get_type_val :: Raw -> Elab' aux (Term, Type)
- get_deferred :: Elab' aux [Name]
- checkInjective :: (Term, Term, Term) -> Elab' aux ()
- get_implementations :: Elab' aux [Name]
- get_autos :: Elab' aux [(Name, ([FailContext], [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 -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
- letbind :: Name -> RigCount -> 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 ()
- patvar :: Name -> Elab' aux ()
- patvar' :: Name -> Elab' aux ()
- patbind :: Name -> RigCount -> Elab' aux ()
- focus :: Name -> Elab' aux ()
- movelast :: Name -> Elab' aux ()
- dotterm :: Elab' aux ()
- get_dotterm :: Elab' aux [(Name, [Name])]
- zipHere :: Elab' aux ()
- matchProblems :: Bool -> Elab' aux ()
- unifyProblems :: Elab' aux ()
- defer :: [Name] -> [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_apply :: Raw -> [Bool] -> Elab' aux [(Name, Name)]
- apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
- 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 -> RigCount -> 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 a1 => [(a2, b, c, a1)] -> [Char]
- module Idris.Core.ProofState
Documentation
Constructors
| ES (ProofState, aux) String (Maybe (ElabState aux)) |
proof :: ElabState aux -> ProofState Source #
getPSnames :: Elab' aux [Name] Source #
setNextName :: Elab' aux () Source #
initNextNameFrom :: [Name] -> Elab' aux () Source #
transformErr :: (Err -> Err) -> Elab' aux a -> Elab' aux a Source #
Transform the error returned by an elaboration script, preserving location information and proof search failure messages.
elaborate :: String -> Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String) Source #
getUnifyLog :: Elab' aux Bool Source #
processTactic' :: Tactic -> Elab' aux () Source #
Process a tactic within the current elaborator state
updatePS :: (ProofState -> ProofState) -> Elab' aux () Source #
done_elaborating_app :: Name -> Elab' aux () Source #
get_context :: Elab' aux Context Source #
Get the global context
set_context :: Context -> Elab' aux () Source #
Update the context. (should only be used for adding temporary definitions or all sorts of stuff could go wrong)
get_global_nextname :: Elab' aux Int Source #
set_global_nextname :: Int -> Elab' aux () Source #
get_usedns :: Elab' aux [Name] Source #
get_recents :: Elab' aux [Name] Source #
Return recently solved names (that is, the names solved since the last call to get_recents)
get_deferred :: Elab' aux [Name] Source #
get holes we've deferred for later definition
get_implementations :: Elab' aux [Name] Source #
get implementation argument names
match_fill :: Raw -> Elab' aux () Source #
complete_fill :: Elab' aux () Source #
start_unify :: Name -> Elab' aux () Source #
computeLet :: Name -> Elab' aux () Source #
whnf_compute :: Elab' aux () Source #
whnf_compute_args :: Elab' aux () Source #
patvar :: Name -> Elab' aux () Source #
Turn the current hole into a pattern variable with the provided name, made unique if not the same as the head of the hole queue
patvar' :: Name -> Elab' aux () Source #
Turn the current hole into a pattern variable with the provided name, but don't make MNs unique.
zipHere :: Elab' aux () Source #
Set the zipper in the proof state to point at the current sub term (This currently happens automatically, so this will have no effect...)
matchProblems :: Bool -> Elab' aux () Source #
unifyProblems :: Elab' aux () Source #
implementationArg :: Name -> Elab' aux () Source #
proofstate :: Elab' aux () Source #
reorder_claims :: Name -> Elab' aux () Source #
Arguments
| :: Raw | The operation being applied |
| -> [Bool] | Whether arguments are implicit |
| -> Elab' aux [(Name, Name)] | The names of the arguments and their holes to be filled with elaborated argument values |
Prepare to apply a function by creating holes to be filled by the arguments
Arguments
| :: Raw | The operator to apply |
| -> [(Bool, Int)] | For each argument, whether to attempt to solve it and the priority in which to do so |
| -> Elab' aux [(Name, Name)] |
Apply an operator, solving some arguments by unification or matching.
Arguments
| :: Raw | The operator to apply |
| -> [(Bool, Int)] | For each argument, whether to attempt to solve it and the priority in which to do so |
| -> Elab' aux [(Name, Name)] |
Apply an operator, solving some arguments by unification or matching.
checkPiGoal :: Name -> Elab' aux () Source #
prunStateT :: Int -> Bool -> [a] -> Maybe [b] -> StateT (ElabState t) TC t1 -> ElabState t -> TC ((t1, Int, Fails), ElabState t) Source #
debugElaborator :: [ErrorReportPart] -> Elab' aux a Source #
module Idris.Core.ProofState