Hets - the Heterogeneous Tool Set

Copyright(c) Uni Bremen 2005-2007
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

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

Documentation

data G_prover Source #

provers and consistency checkers for specific logics

Constructors

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

Show G_prover Source # 

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

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

Show G_proof_tree Source # 

Methods

showsPrec :: Int -> G_proof_tree -> ShowS

show :: G_proof_tree -> String

showList :: [G_proof_tree] -> ShowS

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) Source #

data G_cons_checker Source #

Constructors

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

Show G_cons_checker Source # 

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, Monad 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

data ProofState Source #

Represents the global state of the prover GUI.

Constructors

ProofState 

Fields

Instances

Show ProofState Source # 

Methods

showsPrec :: Int -> ProofState -> ShowS

show :: ProofState -> String

showList :: [ProofState] -> ShowS

logicId :: ProofState -> String Source #

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

Creates an initial State.

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

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

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

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