Copyright	(c) Uni Bremen 2005-2007
License	GPLv2 or higher, see LICENSE.txt
Maintainer	luecke@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable(Logic)
Safe Haskell	None

Proofs.AbstractState

Description

The ProofState data structure abstracts the GUI implementation details away by allowing callback function to use it as the sole input and output. It is also used by the CMDL interface.

Synopsis

data ProverOrConsChecker
- = Prover G_prover
- | ConsChecker G_cons_checker
data G_prover = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_prover lid (Prover sign sentence morphism sublogics proof_tree)
data G_proof_tree = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_proof_tree lid proof_tree
getProverName :: G_prover -> String
getCcName :: G_cons_checker -> String
getCcBatch :: G_cons_checker -> Bool
coerceProver :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1 -> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
data G_cons_checker = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_cons_checker lid (ConsChecker sign sentence sublogics morphism proof_tree)
coerceConsChecker :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1 -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
data ProofActions = ProofActions {
- proveF :: ProofState -> IO (Result ProofState)
- fineGrainedSelectionF :: ProofState -> IO (Result ProofState)
- recalculateSublogicF :: ProofState -> IO ProofState
}
data ProofState = ProofState {
- theoryName :: String
- currentTheory :: G_theory
- proversMap :: KnownProversMap
- selectedGoals :: [String]
- includedAxioms :: [String]
- includedTheorems :: [String]
- proverRunning :: Bool
- accDiags :: [Diagnosis]
- comorphismsToProvers :: [(G_prover, AnyComorphism)]
- selectedProver :: Maybe String
- selectedConsChecker :: Maybe String
- selectedTheory :: G_theory
}
sublogicOfTheory :: ProofState -> G_sublogics
logicId :: ProofState -> String
initialState :: String -> G_theory -> KnownProversMap -> ProofState
resetSelection :: ProofState -> ProofState
toAxioms :: ProofState -> [String]
getAxioms :: ProofState -> [(String, Bool)]
getGoals :: ProofState -> [(String, Maybe BasicProof)]
recalculateSublogicAndSelectedTheory :: ProofState -> ProofState
markProved :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => AnyComorphism -> lid -> [ProofStatus proof_tree] -> ProofState -> ProofState
data G_theory_with_prover = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_theory_with_prover lid (Theory sign sentence proof_tree) (Prover sign sentence morphism sublogics proof_tree)
data G_theory_with_cons_checker = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_theory_with_cons_checker lid (TheoryMorphism sign sentence morphism proof_tree) (ConsChecker sign sentence sublogics morphism proof_tree)
prepareForProving :: ProofState -> (G_prover, AnyComorphism) -> Result G_theory_with_prover
prepareForConsChecking :: ProofState -> (G_cons_checker, AnyComorphism) -> Result G_theory_with_cons_checker
isSubElemG :: G_sublogics -> G_sublogics -> Bool
pathToComorphism :: ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t)) -> AnyComorphism
getAllProvers :: ProverKind -> G_sublogics -> LogicGraph -> [(G_prover, AnyComorphism)]
getUsableProvers :: ProverKind -> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)]
getConsCheckers :: [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
getListOfConsCheckers :: [G_cons_checker]
getAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
lookupKnownProver :: MonadFail m => ProofState -> ProverKind -> m (G_prover, AnyComorphism)
lookupKnownConsChecker :: MonadFail m => ProofState -> m (G_cons_checker, AnyComorphism)
autoProofAtNode :: Bool -> Int -> [String] -> [String] -> G_theory -> (G_prover, AnyComorphism) -> ResultT IO ((G_theory, [(String, String, String)]), (ProofState, [ProofStatus G_proof_tree]))
usableCC :: G_cons_checker -> IO Bool

Documentation

data ProverOrConsChecker Source #

Constructors

Prover G_prover
ConsChecker G_cons_checker

Instances

Instances details

Show ProverOrConsChecker Source #
Instance details Defined in Proofs.AbstractState Methods showsPrec :: Int -> ProverOrConsChecker -> ShowS show :: ProverOrConsChecker -> String showList :: [ProverOrConsChecker] -> ShowS

data G_prover Source #

provers and consistency checkers for specific logics

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_prover lid (Prover sign sentence morphism sublogics proof_tree)

Instances

Instances details

Show G_prover Source #
Instance details Defined in Proofs.AbstractState Methods showsPrec :: Int -> G_prover -> ShowS show :: G_prover -> String showList :: [G_prover] -> ShowS

data G_proof_tree Source #

provers and consistency checkers for specific logics

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_proof_tree lid proof_tree

Instances

Instances details

Show G_proof_tree Source #
Instance details Defined in Proofs.AbstractState Methods showsPrec :: Int -> G_proof_tree -> ShowS show :: G_proof_tree -> String showList :: [G_proof_tree] -> ShowS

getProverName :: G_prover -> String Source #

getCcName :: G_cons_checker -> String Source #

getCcBatch :: G_cons_checker -> Bool Source #

coerceProver :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1 -> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2) Source #

data G_cons_checker Source #

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_cons_checker lid (ConsChecker sign sentence sublogics morphism proof_tree)

Instances

Instances details

Eq G_cons_checker Source #
Instance details Defined in Proofs.AbstractState Methods (==) :: G_cons_checker -> G_cons_checker -> Bool (/=) :: G_cons_checker -> G_cons_checker -> Bool
Show G_cons_checker Source #
Instance details Defined in Proofs.AbstractState Methods showsPrec :: Int -> G_cons_checker -> ShowS show :: G_cons_checker -> String showList :: [G_cons_checker] -> ShowS

coerceConsChecker :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1 -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2) Source #

data ProofActions Source #

Possible actions for GUI which are manipulating ProofState

Constructors

ProofActions
Fields proveF :: ProofState -> IO (Result ProofState) called whenever the Prove button is clicked fineGrainedSelectionF :: ProofState -> IO (Result ProofState) called whenever the "More fine grained selection" button is clicked recalculateSublogicF :: ProofState -> IO ProofState called whenever a (de-)selection occured for updating sublogic

data ProofState Source #

Represents the global state of the prover GUI.

Constructors

ProofState

Fields

theoryName :: String
theory name
currentTheory :: G_theory
Grothendieck theory
proversMap :: KnownProversMap
currently known provers
selectedGoals :: [String]
currently selected goals
includedAxioms :: [String]
axioms to include for the proof
includedTheorems :: [String]
theorems to include for the proof
proverRunning :: Bool
whether a prover is running or not
accDiags :: [Diagnosis]
accumulated Diagnosis during Proofs
comorphismsToProvers :: [(G_prover, AnyComorphism)]
comorphisms fitting with sublogic of this G_theory
selectedProver :: Maybe String
which prover (if any) is currently selected
selectedConsChecker :: Maybe String
which consistency checker (if any) is currently selected
selectedTheory :: G_theory
theory based on selected goals, axioms and proven theorems

Instances

Instances details

Show ProofState Source #
Instance details Defined in Proofs.AbstractState Methods showsPrec :: Int -> ProofState -> ShowS show :: ProofState -> String showList :: [ProofState] -> ShowS

sublogicOfTheory :: ProofState -> G_sublogics Source #

logicId :: ProofState -> String Source #

initialState :: String -> G_theory -> KnownProversMap -> ProofState Source #

Creates an initial State.

resetSelection :: ProofState -> ProofState Source #

toAxioms :: ProofState -> [String] Source #

getAxioms :: ProofState -> [(String, Bool)] Source #

getGoals :: ProofState -> [(String, Maybe BasicProof)] Source #

recalculateSublogicAndSelectedTheory :: ProofState -> ProofState Source #

recalculation of sublogic upon (de)selection of goals, axioms and proven theorems

markProved :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => AnyComorphism -> lid -> [ProofStatus proof_tree] -> ProofState -> ProofState Source #

the list of proof statuses is integrated into the goalMap of the state after validation of the Disproved Statuses

data G_theory_with_prover Source #

a Grothendieck pair of prover and theory which are in the same logic

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_theory_with_prover lid (Theory sign sentence proof_tree) (Prover sign sentence morphism sublogics proof_tree)

data G_theory_with_cons_checker Source #

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_theory_with_cons_checker lid (TheoryMorphism sign sentence morphism proof_tree) (ConsChecker sign sentence sublogics morphism proof_tree)

prepareForProving :: ProofState -> (G_prover, AnyComorphism) -> Result G_theory_with_prover Source #

prepare the selected theory of the state for proving with the given prover:

translation along the comorphism
all coercions
the lid is valid for the prover and the translated theory

prepareForConsChecking :: ProofState -> (G_cons_checker, AnyComorphism) -> Result G_theory_with_cons_checker Source #

isSubElemG :: G_sublogics -> G_sublogics -> Bool Source #

pathToComorphism :: ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t)) -> AnyComorphism Source #

getAllProvers :: ProverKind -> G_sublogics -> LogicGraph -> [(G_prover, AnyComorphism)] Source #

getUsableProvers :: ProverKind -> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)] Source #

getConsCheckers :: [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)] Source #

getListOfConsCheckers :: [G_cons_checker] Source #

getAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)] Source #

lookupKnownProver :: MonadFail m => ProofState -> ProverKind -> m (G_prover, AnyComorphism) Source #

lookupKnownConsChecker :: MonadFail m => ProofState -> m (G_cons_checker, AnyComorphism) Source #

autoProofAtNode :: Bool -> Int -> [String] -> [String] -> G_theory -> (G_prover, AnyComorphism) -> ResultT IO ((G_theory, [(String, String, String)]), (ProofState, [ProofStatus G_proof_tree])) Source #

usableCC :: G_cons_checker -> IO Bool Source #