idris-0.11: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Core.ProofState

Documentation

data ProofState Source

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]
 

newProof Source

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 

data Goal Source

Constructors

GD 

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