| 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.
- 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)
- 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, Monad 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, Monad 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)]
- getAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
- lookupKnownProver :: Monad m => ProofState -> ProverKind -> m (G_prover, AnyComorphism)
- lookupKnownConsChecker :: Monad m => ProofState -> m (G_cons_checker, AnyComorphism)
- autoProofAtNode :: Bool -> Int -> [String] -> G_theory -> (G_prover, AnyComorphism) -> ResultT IO ((G_theory, [(String, String, String)]), (ProofState, [ProofStatus G_proof_tree]))
Documentation
data G_prover
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) |
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, Monad m) => lid1 -> lid2 -> String -> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1 -> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
data G_cons_checker
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
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, Monad m) => lid1 -> lid2 -> String -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1 -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
data ProofActions
Possible actions for GUI which are manipulating ProofState
Constructors
| ProofActions | |
Fields
| |
data ProofState
Represents the global state of the prover GUI.
Constructors
| ProofState | |
Fields
| |
Instances
logicId :: ProofState -> String
initialState :: String -> G_theory -> KnownProversMap -> ProofState
Creates an initial State.
toAxioms :: ProofState -> [String]
getAxioms :: ProofState -> [(String, Bool)]
getGoals :: ProofState -> [(String, Maybe BasicProof)]
recalculateSublogicAndSelectedTheory :: ProofState -> ProofState
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
the list of proof statuses is integrated into the goalMap of the state after validation of the Disproved Statuses
data G_theory_with_prover
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
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
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
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)]
getAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
lookupKnownProver :: Monad m => ProofState -> ProverKind -> m (G_prover, AnyComorphism)
lookupKnownConsChecker :: Monad m => ProofState -> m (G_cons_checker, AnyComorphism)
autoProofAtNode :: Bool -> Int -> [String] -> G_theory -> (G_prover, AnyComorphism) -> ResultT IO ((G_theory, [(String, String, String)]), (ProofState, [ProofStatus G_proof_tree]))