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.

Synopsis

type Elab a = Elab' () a
type Elab' aux a = StateT (ElabState aux) TC a
data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
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 ()
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

type Elab a = Elab' () a Source #

type Elab' aux a = StateT (ElabState aux) TC a Source #

data ElabState aux Source #

Constructors

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

Instances

Show aux => Show (ElabState aux) Source #
Instance details Defined in Idris.Core.Elaborate Methods showsPrec :: Int -> ElabState aux -> ShowS # show :: ElabState aux -> String # showList :: [ElabState aux] -> ShowS #

proof :: ElabState aux -> ProofState Source #

proofFail :: Elab' aux a -> Elab' aux a Source #

explicit :: Name -> Elab' aux () Source #

addPSname :: Name -> Elab' aux () Source #

getPSnames :: Elab' aux [Name] Source #

saveState :: Elab' aux () Source #

loadState :: Elab' aux () Source #

getNameFrom :: Name -> 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.

errAt :: String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a Source #

erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux) Source #

erun :: FC -> Elab' aux a -> Elab' aux a Source #

runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux) Source #

execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux) Source #

initElaborator Source #

Arguments

:: Name	the name of what's to be elaborated
-> String	the current source file
-> Context	the current global context
-> Ctxt TypeInfo	the value of the idris_datatypes field of IState
-> Int	the value of the idris_name field of IState
-> Type	the goal type
-> ProofState

elaborate :: String -> Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String) Source #

updateAux :: (aux -> aux) -> Elab' aux () Source #

Modify the auxiliary state

getAux :: Elab' aux aux Source #

Get the auxiliary state

unifyLog :: Bool -> Elab' aux () Source #

Set whether to show the unifier log

getUnifyLog :: Elab' aux Bool Source #

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

Process a tactic within the current elaborator state

updatePS :: (ProofState -> ProofState) -> Elab' aux () Source #

now_elaborating :: FC -> Name -> Name -> Elab' aux () Source #

done_elaborating_app :: Name -> Elab' aux () Source #

done_elaborating_arg :: Name -> Name -> Elab' aux () Source #

elaborating_app :: Elab' aux [(FC, Name, Name)] 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_datatypes :: Elab' aux (Ctxt TypeInfo) Source #

set_datatypes :: Ctxt TypeInfo -> Elab' aux () Source #

get_global_nextname :: Elab' aux Int Source #

set_global_nextname :: Int -> Elab' aux () Source #

get_term :: Elab' aux Term Source #

get the proof term

update_term :: (Term -> Term) -> Elab' aux () Source #

modify the proof term

get_env :: Elab' aux Env Source #

get the local context at the currently in focus hole

get_inj :: Elab' aux [Name] Source #

get_holes :: Elab' aux [Name] Source #

get_usedns :: Elab' aux [Name] Source #

get_probs :: Elab' aux Fails Source #

get_recents :: Elab' aux [Name] Source #

Return recently solved names (that is, the names solved since the last call to get_recents)

goal :: Elab' aux Type Source #

get the current goal type

is_guess :: Elab' aux Bool Source #

get_guess :: Elab' aux Term Source #

Get the guess at the current hole, if there is one

get_type :: Raw -> Elab' aux Type Source #

Typecheck locally

get_type_val :: Raw -> Elab' aux (Term, Type) Source #

get_deferred :: Elab' aux [Name] Source #

get holes we've deferred for later definition

checkInjective :: (Term, Term, Term) -> Elab' aux () Source #

get_implementations :: Elab' aux [Name] Source #

get implementation argument names

get_autos :: Elab' aux [(Name, ([FailContext], [Name]))] Source #

get auto argument names

unique_hole :: Name -> Elab' aux Name Source #

given a desired hole name, return a unique hole name

unique_hole' :: Bool -> Name -> Elab' aux Name Source #

elog :: String -> Elab' aux () Source #

getLog :: Elab' aux String Source #

attack :: Elab' aux () Source #

claim :: Name -> Raw -> Elab' aux () Source #

claimFn :: Name -> Name -> Raw -> Elab' aux () Source #

unifyGoal :: Raw -> Elab' aux () Source #

unifyTerms :: Raw -> Raw -> Elab' aux () Source #

exact :: Raw -> Elab' aux () Source #

fill :: Raw -> Elab' aux () Source #

match_fill :: Raw -> Elab' aux () Source #

prep_fill :: Name -> [Name] -> Elab' aux () Source #

complete_fill :: Elab' aux () Source #

solve :: Elab' aux () Source #

start_unify :: Name -> Elab' aux () Source #

end_unify :: Elab' aux () Source #

unify_all :: Elab' aux () Source #

regret :: Elab' aux () Source #

compute :: Elab' aux () Source #

computeLet :: Name -> Elab' aux () Source #

simplify :: Elab' aux () Source #

whnf_compute :: Elab' aux () Source #

whnf_compute_args :: Elab' aux () Source #

eval_in :: Raw -> Elab' aux () Source #

check_in :: Raw -> Elab' aux () Source #

intro :: Maybe Name -> Elab' aux () Source #

introTy :: Raw -> Maybe Name -> Elab' aux () Source #

forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux () Source #

letbind :: Name -> RigCount -> Raw -> Raw -> Elab' aux () Source #

expandLet :: Name -> Term -> Elab' aux () Source #

rewrite :: Raw -> Elab' aux () Source #

equiv :: Raw -> 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.

patbind :: Name -> RigCount -> Elab' aux () Source #

focus :: Name -> Elab' aux () Source #

movelast :: Name -> Elab' aux () Source #

dotterm :: Elab' aux () Source #

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

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 #

defer :: [Name] -> [Name] -> Name -> Elab' aux Name Source #

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

implementationArg :: Name -> Elab' aux () Source #

autoArg :: Name -> Elab' aux () Source #

setinj :: Name -> Elab' aux () Source #

proofstate :: Elab' aux () Source #

reorder_claims :: Name -> Elab' aux () Source #

qed :: Elab' aux Term Source #

undo :: Elab' aux () Source #

prepare_apply 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

apply Source #

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.

match_apply Source #

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.

apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)] Source #

apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux () Source #

apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux () Source #

checkPiGoal :: Name -> Elab' aux () Source #

simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux () Source #

infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux () Source #

dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux () Source #

arg :: Name -> RigCount -> Maybe ImplicitInfo -> Name -> Elab' aux () Source #

no_errors :: Elab' aux () -> Maybe Err -> Elab' aux () Source #

try :: Elab' aux a -> Elab' aux a -> Elab' aux a Source #

handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a Source #

try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a Source #

tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a Source #

tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a Source #

tryAll :: [(Elab' aux a, Name)] -> Elab' aux a Source #

tryAll' :: Bool -> [(Elab' aux a, Name)] -> Elab' aux a 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 #

qshow :: Fails -> String Source #

dumpprobs :: Show a1 => [(a2, b, c, a1)] -> [Char] Source #

module Idris.Core.ProofState