Idris.Core.ProofState

Implements a proof state, some primitive tactics for manipulating proofs, and some high level commands for introducing new theorems, evaluation/checking inside the proof system, etc.

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

• implementations :: [Name]

  implementation arguments (for interfaces)

• 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]
• constraint_ns :: String

Instances

Show ProofState

Methods

showsPrec :: Int -> ProofState -> ShowS

show :: ProofState -> String

showList :: [ProofState] -> ShowS

newProof

Arguments

:: Name

the name of what's to be elaborated

-> String

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

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

WHNF_Compute

WHNF_ComputeArgs

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]

Implementation Name

AutoArg Name

SetInjective Name

MoveLast Name

MatchProblems Bool

UnifyProblems

UnifyGoal Raw

UnifyTerms Raw Raw

ProofState

Undo

QED

Instances

Show Tactic

Methods

showsPrec :: Int -> Tactic -> ShowS

show :: Tactic -> String

showList :: [Tactic] -> ShowS

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 :: (Foldable t, Foldable t1, Eq a) => t1 a -> [(a, TT a)] -> t a -> [(a, TT a)]

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

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