Idris.Core.ProofState

Documentation

data ProofState

Constructors

PS

Fields

thname :: Name

holes :: [Name]

holes still to be solved

usedns :: [Name]

used names, don't use again

nextname :: Int

name supply, for locally unique names

global_nextname :: Int

a mirror of the global name supply, for generating things like type tags in reflection

pterm :: ProofTerm

current proof term

ptype :: Type

original goal

dontunify :: [Name]

explicitly given by programmer, leave it

unified :: (Name, [(Name, Term)])

notunified :: [(Name, Term)]

dotted :: [(Name, [Name])]

dot pattern holes + environment either hole or something in env must turn up in the notunified list during elaboration

solved :: Maybe (Name, Term)

problems :: Fails

injective :: [Name]

deferred :: [Name]

names we'll need to define

instances :: [Name]

instance arguments (for type classes)

autos :: [(Name, ([FailContext], [Name]))]

unsolved auto implicits with their holes

psnames :: [Name]

Local names okay to use in proof search

previous :: Maybe ProofState

for undo

context :: Context

datatypes :: Ctxt TypeInfo

plog :: String

unifylog :: Bool

done :: Bool

recents :: [Name]

while_elaborating :: [FailContext]

Instances

Show ProofState

newProof

Arguments

:: Name

the name of what's to be elaborated

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

envAtFocus :: ProofState -> TC Env

goalAtFocus :: ProofState -> TC (Binder Type)

data Tactic

Constructors

Attack

Claim Name Raw

ClaimFn Name Name Raw

Reorder Name

Exact Raw

Fill Raw

MatchFill Raw

PrepFill Name [Name]

CompleteFill

Regret

Solve

StartUnify Name

EndUnify

UnifyAll

Compute

ComputeLet Name

Simplify

HNF_Compute

EvalIn Raw

CheckIn Raw

Intro (Maybe Name)

IntroTy Raw (Maybe Name)

Forall Name (Maybe ImplicitInfo) Raw

LetBind Name Raw Raw

ExpandLet Name Term

Rewrite Raw

Induction Raw

CaseTac Raw

Equiv Raw

PatVar Name

PatBind Name

Focus Name

Defer [Name] Name

DeferType Name Raw [Name]

Instance Name

AutoArg Name

SetInjective Name

MoveLast Name

MatchProblems Bool

UnifyProblems

UnifyGoal Raw

UnifyTerms Raw Raw

ProofState

Undo

QED

Instances

Show Tactic

data Goal

Constructors

GD

Fields

premises :: Env

goalType :: Binder Term

processTactic :: Tactic -> ProofState -> TC (ProofState, String)

nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState

doneElaboratingAppPS :: Name -> ProofState -> ProofState

doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState

dropGiven :: (Eq a, Foldable t, Foldable t1) => t1 a -> [(a, TT a)] -> t a -> [(a, TT a)]

keepGiven :: (Eq a, Foldable t, Foldable t1) => t1 a -> [(a, TT a)] -> t a -> [(a, TT a)]

getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)