Safe Haskell | None |
---|
- data Command
- 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 ()
- saveState :: Elab' aux ()
- loadState :: Elab' aux ()
- getNameFrom :: Name -> Elab' aux Name
- setNextName :: Elab' aux ()
- initNextNameFrom :: [Name] -> Elab' aux ()
- errAt :: String -> Name -> Elab' aux a -> Elab' aux a
- 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 -> Context -> Type -> ProofState
- elaborate :: Context -> 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_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_probs :: Elab' aux Fails
- goal :: Elab' aux Type
- get_guess :: Elab' aux Type
- 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_instances :: Elab' aux [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 ()
- 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 ()
- hnf_compute :: 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 -> Raw -> Elab' aux ()
- letbind :: Name -> 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 ()
- patbind :: Name -> Elab' aux ()
- focus :: Name -> Elab' aux ()
- movelast :: Name -> Elab' aux ()
- zipHere :: Elab' aux ()
- matchProblems :: Bool -> Elab' aux ()
- unifyProblems :: Elab' aux ()
- defer :: [Name] -> Name -> Elab' aux ()
- deferType :: Name -> Raw -> [Name] -> Elab' aux ()
- instanceArg :: 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 :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
- arg :: Name -> 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 -> Bool -> Elab' aux a
- try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
- tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
- tryAll :: [(Elab' aux a, Name)] -> Elab' aux a
- prunStateT :: Int -> Bool -> [a] -> StateT (ElabState t) (TC' Err) t1 -> ElabState t -> TC' Err ((t1, Int, Fails), ElabState t)
- qshow :: Fails -> String
- dumpprobs :: Show a => [(t, t1, t2, a)] -> [Char]
- module Idris.Core.ProofState
Documentation
ES (ProofState, aux) String (Maybe (ElabState aux)) |
Show aux => Show (ElabState aux) |
proof :: ElabState aux -> ProofStateSource
getNameFrom :: Name -> Elab' aux NameSource
setNextName :: Elab' aux ()Source
initNextNameFrom :: [Name] -> Elab' aux ()Source
initElaborator :: Name -> Context -> Type -> ProofStateSource
getUnifyLog :: Elab' aux BoolSource
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
done_elaborating_arg :: Name -> Name -> Elab' aux ()Source
get_context :: Elab' aux ContextSource
set_context :: Context -> Elab' aux ()Source
update_term :: (Term -> Term) -> Elab' aux ()Source
get_deferred :: Elab' aux [Name]Source
get_instances :: Elab' aux [Name]Source
unique_hole :: Name -> Elab' aux NameSource
unique_hole' :: Bool -> Name -> Elab' aux NameSource
match_fill :: Raw -> Elab' aux ()Source
complete_fill :: Elab' aux ()Source
start_unify :: Name -> Elab' aux ()Source
computeLet :: Name -> Elab' aux ()Source
hnf_compute :: Elab' aux ()Source
patvar :: Name -> Elab' aux ()Source
Turn the current hole into a pattern variable with the provided name, made unique if MN
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
instanceArg :: Name -> Elab' aux ()Source
proofstate :: Elab' aux ()Source
reorder_claims :: Name -> Elab' aux ()Source
:: 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
apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()Source
checkPiGoal :: Name -> Elab' aux ()Source
simple_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()Source
prunStateT :: Int -> Bool -> [a] -> StateT (ElabState t) (TC' Err) t1 -> ElabState t -> TC' Err ((t1, Int, Fails), ElabState t)Source
module Idris.Core.ProofState