Idris.Core.Elaborate

Documentation

data Command

Constructors

Theorem Name Raw

Eval Raw

Quit

Print Name

Tac (Elab ())

data ElabState aux

Constructors

ES (ProofState, aux) String (Maybe (ElabState aux))

Instances

Show aux => Show (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 ()

Modify the auxiliary state

getAux :: Elab' aux aux

Get the auxiliary state

unifyLog :: Bool -> Elab' aux ()

Set whether to show the unifier log

getUnifyLog :: Elab' aux Bool

processTactic' :: Tactic -> Elab' aux ()

Process a tactic within the current elaborator state

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

get_recents :: Elab' aux [Name]

goal :: Elab' aux Type

is_guess :: Elab' aux Bool

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]

get_autos :: Elab' aux [(Name, [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 -> Maybe ImplicitInfo -> 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 ()

Turn the current hole into a pattern variable with the provided name, made unique if MN

patbind :: Name -> Elab' aux ()

focus :: Name -> Elab' aux ()

movelast :: Name -> Elab' aux ()

dotterm :: Elab' aux ()

get_dotterm :: Elab' aux [(Name, [Name])]

zipHere :: Elab' aux ()

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

unifyProblems :: Elab' aux ()

defer :: [Name] -> Name -> Elab' aux ()

deferType :: Name -> Raw -> [Name] -> Elab' aux ()

instanceArg :: 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

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

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 -> 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 -> 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 t1 -> ElabState t -> TC ((t1, Int, Fails), ElabState t)

qshow :: Fails -> String

dumpprobs :: Show a => [(t, t1, t2, a)] -> [Char]

module Idris.Core.ProofState