idris-0.11.2: Functional Programming Language with Dependent Types

Safe HaskellNone



data ProofState Source




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]

newProof Source


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

data Goal Source



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

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