AbstractState.hs revision d8a6d1101a0e3d09fb8f8566590cb209c103498a
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian MaederModule : $Header$
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederDescription : State data structure used by the goal management GUI.
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Uni Bremen 2005-2007
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederMaintainer : luecke@informatik.uni-bremen.de
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederStability : provisional
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiPortability : non-portable(Logic)
679d3f541f7a9ede4079e045f7758873bb901872Till MossakowskiThe 'ProofState' data structure abstracts the GUI implementation details
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowskiaway by allowing callback function to use it as the sole input and output.
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederIt is also used by the CMDL interface.
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder ( G_prover (..)
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , getProverName
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder , coerceProver
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder , G_cons_checker (..)
953127f27b7854580057a92e8269fd7a8716a800Christian Maeder , coerceConsChecker
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder , ProofActions (..)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder , ProofState (..)
74b841a4b332085d5fd79975a13313c2681ae595Christian Maeder , sublogicOfTheory
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maeder , initialState
010997ddd12186698c1ebdbcddb63a670552b3c2Adrián Riesco , resetSelection
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , recalculateSublogicAndSelectedTheory
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder , G_theory_with_prover (..)
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder , G_theory_with_cons_checker (..)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , prepareForProving
7bf4436b6f9987b070033a323757b206c898c1beChristian Maeder , prepareForConsChecking
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , getAllProvers
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder , getConsCheckers
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder , lookupKnownProver
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder , lookupKnownConsChecker
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder , autoProofAtNode
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maederimport qualified Data.Map as Map
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maederimport qualified Common.OrderedMap as OMap
152c178f9f9969ce729361a5c61aa4ff2c9ed840Christian Maederimport Unsafe.Coerce (unsafeCoerce)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder-- | provers and consistency checkers for specific logics
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maederdata G_prover =
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder sign morphism symbol raw_symbol proof_tree
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder sign morphism symbol raw_symbol proof_tree
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder => G_prover lid (Prover sign sentence morphism sublogics proof_tree)
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian Maeder deriving Typeable
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maederinstance Show G_prover where
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder show = getProverName
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian MaedergetProverName :: G_prover -> String
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian MaedergetProverName (G_prover _ p) = proverName p
57dd851a0c98fe681443c74bfcb2d6ec8b07fbf5Christian MaedercoerceProver ::
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maeder => lid1 -> lid2 -> String
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder -> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder -> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
f1b14608f0f3db464c3aded480e49522d73b08e5Christian MaedercoerceProver = primCoerce
f1b14608f0f3db464c3aded480e49522d73b08e5Christian Maederdata G_cons_checker =
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder sign morphism symbol raw_symbol proof_tree
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder sign morphism symbol raw_symbol proof_tree
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder => G_cons_checker lid
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder (ConsChecker sign sentence sublogics morphism proof_tree)
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder deriving (Typeable)
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maederinstance Show G_cons_checker where show x = "G_cons_checker "
be3f5e3e69900ececafea5b010a8400f26af5362Christian MaedergetCcName :: G_cons_checker -> String
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian MaedergetCcName (G_cons_checker _ p) = ccName p
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian MaedergetCcBatch :: G_cons_checker -> Bool
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian MaedergetCcBatch (G_cons_checker _ p) = ccBatch p
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian MaedercoerceConsChecker ::
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
8528053a6a766c3614276df0f59fb2a2e8ab6d18Christian Maeder => lid1 -> lid2 -> String
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
0d0047d6eb457b56ff10987569769a420754a56fChristian MaedercoerceConsChecker = primCoerce
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder-- | Possible actions for GUI which are manipulating ProofState
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maederdata ProofActions = ProofActions {
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -- | called whenever the "Prove" button is clicked
d11391a2447a2005329a95b5d770f24e62bf5b63Christian Maeder proveF :: ProofState
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder -> IO (Result.Result ProofState),
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -- | called whenever the "More fine grained selection" button is clicked
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder fineGrainedSelectionF :: ProofState
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -> IO (Result.Result ProofState),
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -- | called whenever a (de-)selection occured for updating sublogic
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder recalculateSublogicF :: ProofState
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder -> IO ProofState
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder Represents the global state of the prover GUI.
3086cb15387bd2d08398aad31b8b7a891d45d249Christian Maederdata ProofState =
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder { -- | theory name
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder theoryName :: String,
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder -- | Grothendieck theory
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder currentTheory :: G_theory,
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder -- | currently known provers
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder proversMap :: KnownProversMap,
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder -- | currently selected goals
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder selectedGoals :: [String],
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder -- | axioms to include for the proof
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder includedAxioms :: [String],
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder -- | theorems to include for the proof
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder includedTheorems :: [String],
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder -- | whether a prover is running or not
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder proverRunning :: Bool,
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder -- | accumulated Diagnosis during Proofs
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder accDiags :: [Diagnosis],
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder -- | comorphisms fitting with sublogic of this G_theory
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder comorphismsToProvers :: [(G_prover, AnyComorphism)],
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder -- | which prover (if any) is currently selected
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder selectedProver :: Maybe String,
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder -- | which consistency checker (if any) is currently selected
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder selectedConsChecker :: Maybe String,
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maeder -- | theory based on selected goals, axioms and proven theorems
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder selectedTheory :: G_theory
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder } deriving Show
6505786996adb0239e26bb669ea579d630fa46a4Christian MaederresetSelection :: ProofState -> ProofState
6505786996adb0239e26bb669ea579d630fa46a4Christian MaederresetSelection s = case currentTheory s of
aeb4e74b8b3328d8ea15512ec4e1e1b8d0919f01Christian Maeder G_theory _ _ _ _ sens _ ->
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder let (aMap, gMap) = OMap.partition isAxiom sens
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder { selectedGoals = Map.keys gMap
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , includedAxioms = Map.keys aMap
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , includedTheorems = gs }
6505786996adb0239e26bb669ea579d630fa46a4Christian MaedertoAxioms :: ProofState -> [String]
6505786996adb0239e26bb669ea579d630fa46a4Christian MaedertoAxioms = map (\ (k, wTh) -> if wTh then "(Th) " ++ k else k)
6505786996adb0239e26bb669ea579d630fa46a4Christian MaedergetAxioms :: ProofState -> [(String, Bool)]
6505786996adb0239e26bb669ea579d630fa46a4Christian MaedergetAxioms = getThAxioms . currentTheory
6505786996adb0239e26bb669ea579d630fa46a4Christian MaedergetGoals :: ProofState -> [(String, Maybe BasicProof)]
6505786996adb0239e26bb669ea579d630fa46a4Christian MaedergetGoals = getThGoals . currentTheory
9b4d59bb654421c8fe405636bba0f12e09c65641Christian Maeder Creates an initial State.
ea8e98e298f33f9362293f392c8fb192722b8904Eugen KuksainitialState :: String
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder -> KnownProversMap
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder -> ProofState
6505786996adb0239e26bb669ea579d630fa46a4Christian MaederinitialState thN th pm = resetSelection
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder { theoryName = thN
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder , currentTheory = th
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , proversMap = pm
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , selectedGoals = []
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , includedAxioms = []
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , includedTheorems = []
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , proverRunning = False
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder , accDiags = []
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , comorphismsToProvers = []
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder , selectedProver =
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder in if null prvs
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder if defaultGUIProver `elem` prvs
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder then Just defaultGUIProver
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder , selectedConsChecker = Nothing
04d3cae33dab3092150060a8a5c8b0b046275725Christian Maeder , selectedTheory = th }
04d3cae33dab3092150060a8a5c8b0b046275725Christian MaederlogicId :: ProofState -> String
04d3cae33dab3092150060a8a5c8b0b046275725Christian MaederlogicId s = case currentTheory s of
a07b1088ec14605a305cd48245f804b79cdce7b7Christian Maeder G_theory lid _ _ _ _ _ -> language_name lid
04d3cae33dab3092150060a8a5c8b0b046275725Christian MaedersublogicOfTheory :: ProofState -> G_sublogics
04d3cae33dab3092150060a8a5c8b0b046275725Christian MaedersublogicOfTheory = sublogicOfTh . selectedTheory
b39504a1be2dc590fb06e313749b6d3690da3fe9Christian Maederdata G_theory_with_cons_checker =
9b4d59bb654421c8fe405636bba0f12e09c65641Christian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
9b4d59bb654421c8fe405636bba0f12e09c65641Christian Maeder sign morphism symbol raw_symbol proof_tree
6505786996adb0239e26bb669ea579d630fa46a4Christian Maeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder sign morphism symbol raw_symbol proof_tree
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder => G_theory_with_cons_checker lid
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder (TheoryMorphism sign sentence morphism proof_tree)
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder (ConsChecker sign sentence sublogics morphism proof_tree)
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder-- | a Grothendieck pair of prover and theory which are in the same logic
46947810076241f06f3e2919edb2289ed84d6c15Christian Maederdata G_theory_with_prover =
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder sign morphism symbol raw_symbol proof_tree
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder sign morphism symbol raw_symbol proof_tree
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder => G_theory_with_prover lid
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder (Theory sign sentence proof_tree)
bd986fa9d0f451b8166efdb9027c153d101aa65bChristian Maeder (Prover sign sentence morphism sublogics proof_tree)
46947810076241f06f3e2919edb2289ed84d6c15Christian Maederdata GPlainTheory =
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder sign morphism symbol raw_symbol proof_tree
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder sign morphism symbol raw_symbol proof_tree
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder => GPlainTheory lid (Theory sign sentence proof_tree)
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian MaederprepareForConsChecking :: ProofState
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder -> (G_cons_checker, AnyComorphism)
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder -> Result G_theory_with_cons_checker
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian MaederprepareForConsChecking st (G_cons_checker lid4 p, co) = do
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder GPlainTheory lidT th@(Theory sign'' _) <- prepareTheory st co
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder incl <- subsig_inclusion lidT (empty_signature lidT) sign''
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder let mor = TheoryMorphism
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder { tSource = emptyTheory lidT
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder , tTarget = th
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder , tMorphism = incl }
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder p' <- coerceConsChecker lid4 lidT "" p
8c2e26231e509251734d474a6dc9a0c9970081d4Christian Maeder return $ G_theory_with_cons_checker lidT mor p'
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian MaederprepareTheory :: ProofState -> AnyComorphism -> Result GPlainTheory
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian MaederprepareTheory st (Comorphism cid) = case selectedTheory st of
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder G_theory lid _ (ExtSign sign _) _ sens _ -> do
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder bTh' <- coerceBasicTheory lid (sourceLogic cid)
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder "Proofs.AbstractState.prepareTheory: basic theory"
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder (sign, toNamedList sens)
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder (sign'', sens'') <- wrapMapTheory cid bTh'
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder return . GPlainTheory (targetLogic cid) . Theory sign''
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder $ toThSens sens''
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder{- | prepare the selected theory of the state for proving with the
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder * translation along the comorphism
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder * all coercions
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder * the lid is valid for the prover and the translated theory
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian MaederprepareForProving :: ProofState
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -> (G_prover, AnyComorphism)
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder -> Result G_theory_with_prover
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian MaederprepareForProving st (G_prover lid4 p, co) = do
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder GPlainTheory lidT th <- prepareTheory st co
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder p' <- coerceProver lid4 lidT "" p
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder return $ G_theory_with_prover lidT th p'
d75d2d11170f1339ebe37d9d9c06aff148637b13Christian Maeder-- | creates the currently selected theory
d75d2d11170f1339ebe37d9d9c06aff148637b13Christian MaedermakeSelectedTheory :: ProofState -> G_theory
9bbe44a0670a21990fcaf328661ef03a8efd9fecChristian MaedermakeSelectedTheory s = case currentTheory s of
9bbe44a0670a21990fcaf328661ef03a8efd9fecChristian Maeder G_theory lid syn sig si sens _ ->
9bbe44a0670a21990fcaf328661ef03a8efd9fecChristian Maeder let (aMap, gMap) = OMap.partition isAxiom sens
9bbe44a0670a21990fcaf328661ef03a8efd9fecChristian Maeder pMap = OMap.filter isProvenSenStatus gMap
83259a366597461d24e6b9236a8a33e201798e4dChristian Maeder G_theory lid syn sig si
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder [ filterMapWithList (selectedGoals s) gMap
da4b55f4795a4b585f513eaceb67cda10485febfChristian Maeder , filterMapWithList (includedAxioms s) aMap
c30cfe2a6ab063befdfb47449bc286caee6d8fc3Christian Maeder , markAsAxiom True $ filterMapWithList (includedTheorems s) pMap
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder recalculation of sublogic upon (de)selection of goals, axioms and
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder proven theorems
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian MaederrecalculateSublogicAndSelectedTheory :: ProofState -> ProofState
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian MaederrecalculateSublogicAndSelectedTheory st = let
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder sTh = makeSelectedTheory st
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder sLo = sublogicOfTh sTh
1c8c2b04b40b5c054da07b8d059e5ef29d4dbc32Christian Maeder { selectedTheory = sTh
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian Maeder , proversMap = shrinkKnownProvers sLo $ proversMap st }
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
c0380b947eef252db81ee562246bb732555427f4Till MossakowskigetConsCheckers = concatMap (\ cm@(Comorphism cid) ->
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder map (\ cc -> (G_cons_checker (targetLogic cid) cc, cm))
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder $ cons_checkers $ targetLogic cid)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederlookupKnownConsChecker :: Monad m => ProofState
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder -> m (G_cons_checker, AnyComorphism)
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian MaederlookupKnownConsChecker st =
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder let sl = sublogicOfTh (selectedTheory st)
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder pr_s <- selectedConsChecker st
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder ps <- Map.lookup pr_s (proversMap st)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder return (pr_s, ps)
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder matchingCC s (gp, _) = case gp of
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder G_cons_checker _ p -> ccName p == s
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder findCC (pr_n, cms) =
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski case filter (matchingCC pr_n) $ getConsCheckers
b4a750119742b015a815e6f370a7d58e7a4de634Christian Maeder $ filter (lessSublogicComor sl) cms of
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder [] -> fail ("CMDL.ProverConsistency.lookupKnownConsChecker" ++
1c8293dcdc80913c9d1188a62682ad85f0eb21e1Christian Maeder ": no consistency checker found")
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder p : _ -> return p
b4a750119742b015a815e6f370a7d58e7a4de634Christian Maeder in maybe ( fail ("CMDL.ProverConsistency.lookupKnownConsChecker: " ++
e44da4d9d6af17dd91b3542fb3a1522439fe7c18Christian Maeder "no matching known prover")) findCC mt
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian MaederlookupKnownProver :: Monad m => ProofState -> ProverKind
d07992323218d9d6db42302fe91fdaab2d7f9ec0Christian Maeder -> m (G_prover, AnyComorphism)
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian MaederlookupKnownProver st pk =
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht let sl = sublogicOfTh (selectedTheory st)
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht mt = do -- Monad Maybe
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht pr_s <- selectedProver st
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht ps <- Map.lookup pr_s (proversMap st)
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht return (pr_s, ps)
e44da4d9d6af17dd91b3542fb3a1522439fe7c18Christian Maeder matchingPr s (gp, _) = case gp of
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht G_prover _ p -> proverName p == s
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder findProver (pr_n, cms) =
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder case filter (matchingPr pr_n) $ getProvers pk sl
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder $ filter (lessSublogicComor sl) cms of
fa15ba427d20bfe2b50fbe6e2f6f51616aaed016Christian Maeder [] -> fail "Proofs.InferBasic: no prover found"
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder p : _ -> return p
e44da4d9d6af17dd91b3542fb3a1522439fe7c18Christian Maeder in maybe (fail "Proofs.InferBasic: no matching known prover")
f223a90d51db0fb060381211cfc07fc5b0672f58Christian Maeder findProver mt
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder-- | Pairs each target prover of these comorphisms with its comorphism
f223a90d51db0fb060381211cfc07fc5b0672f58Christian MaedergetProvers :: ProverKind -> G_sublogics -> [AnyComorphism]
f223a90d51db0fb060381211cfc07fc5b0672f58Christian Maeder -> [(G_prover, AnyComorphism)]
f223a90d51db0fb060381211cfc07fc5b0672f58Christian MaedergetProvers pk (G_sublogics lid sl) =
60aa3aecbe2f2e85211d5d018eb4affd5d81ab81Christian Maeder foldl addProvers [] where
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder addProvers acc cm = case cm of
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder Comorphism cid -> let
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder slid = sourceLogic cid
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder tlid = targetLogic cid
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in acc ++ foldl
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder if hasProverKind pk p
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder && language_name lid == language_name slid
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder && maybe False (flip isSubElem $ proverSublogic p)
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder (mapSublogic cid $ forceCoerceSublogic lid slid sl)
6b00a9239fe7c804524099ca3d25f4ffc6079ceeChristian Maeder then (G_prover tlid p, cm) : l else l)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder [] (provers tlid)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederknownProvers :: LogicGraph -> ProverKind -> Map.Map G_sublogics [G_prover]
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian MaederknownProvers lg pk=
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder let l = Map.elems $ logics lg
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder in foldl (\m (Logic lid) -> foldl (\m' p ->
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder let lgx = G_sublogics lid (proverSublogic p)
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder p' = G_prover lid p
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder in case Map.lookup lgx m' of
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder Just ps -> Map.insert lgx (p':ps) m'
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder Nothing -> Map.insert lgx [p'] m') m $
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder filter (hasProverKind pk)
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder (provers lid)) Map.empty l
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian MaederunsafeCompComorphism :: AnyComorphism -> AnyComorphism -> AnyComorphism
c0380b947eef252db81ee562246bb732555427f4Till MossakowskiunsafeCompComorphism c1 c2 = case compComorphism c1 c2 of
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder Result _ (Just c_new) -> c_new
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder r -> propagateErrors "Proofs.AbstractState.unsafeCompComorphism" r
f8c8c3e92d02616c7a2994b3aa62a541870796d8Christian MaederisSubElemG :: G_sublogics -> G_sublogics -> Bool
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian MaederisSubElemG (G_sublogics lid sl) (G_sublogics lid1 sl1) =
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder Logic lid == Logic lid1 &&
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder isSubElem sl (Unsafe.Coerce.unsafeCoerce sl1)
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian MaedergetAllProvers :: ProverKind -> G_sublogics -> LogicGraph
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder -> [(G_prover, AnyComorphism)]
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian MaedergetAllProvers pk start lg =
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder let kp = knownProvers lg pk
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder g = logicGraph2Graph lg
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder in concat $ map (mkComorphism kp) $
064de40ef459b7d64b96a2296bbde25449a2a4c2Christian Maeder concat $ map (\end ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski yen 10 (start, Nothing) (\(l,_) -> isSubElemG l end) g)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz mkComorphism :: Map.Map G_sublogics [t2]
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder -> ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder -> [(t2, AnyComorphism)]
89ab08979dc23d72e9e09c8990a8c44847041d6fChristian Maeder mkComorphism kp (path,(end@(G_sublogics lid sub),_)) =
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder let fullComorphism = case path of
9dfa1c020a030abdbcfce17b18000cc4e1f28462Christian Maeder [] -> Comorphism $ mkIdComorphism lid sub
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder ((G_sublogics lid1 sub1,_),c):cs ->
f8c8c3e92d02616c7a2994b3aa62a541870796d8Christian Maeder foldl unsafeCompComorphism
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht (Comorphism $ mkIdComorphism lid1 sub1)
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht (c:(snd $ unzip $ cs))
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski in case Map.toList $ Map.filterWithKey (\l _ -> isSubElemG end l) kp of
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski [(_,ps)] -> map (\p -> (p,fullComorphism)) ps
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder _ -> error "error1"
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder{- | the list of proof statuses is integrated into the goalMap of the state
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maederafter validation of the Disproved Statuses -}
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski sign morphism symbol raw_symbol proof_tree )
4dfed20c33d6c11a723c0c34d4a38006b9f8d4c1Christian Maeder => AnyComorphism -> lid -> [ProofStatus proof_tree]
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder -> ProofState
b51ddb1ac112b948afbf0e1e5c02939f2b99d72eChristian Maeder -> ProofState
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian MaedermarkProved c lid status st = st
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder { currentTheory = markProvedGoalMap c lid status (currentTheory st) }
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder-- | mark all newly proven goals with their proof tree
412aa5e819f3cd18f0be10b5571661036515b151Christian MaedermarkProvedGoalMap ::
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder sign morphism symbol raw_symbol proof_tree )
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder => AnyComorphism -> lid -> [ProofStatus proof_tree]
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder -> G_theory -> G_theory
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian MaedermarkProvedGoalMap c lid status th = case th of
7d5f239f3f1c1397e5d80caea12929bdf8abe2d8Christian Maeder G_theory lid1 syn sig si thSens _ ->
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder let updStat ps s = Just $
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder s { senAttr = ThmStatus $ (c, BasicProof lid ps) : thmStatus s }
6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7Christian Maeder upd pStat = OMap.update (updStat pStat) (goalName pStat)
ba10e88b85904494bb9695da8d9a72ec683e2b0dChristian Maeder in G_theory lid1 syn sig si (foldl (flip upd) thSens status)
63fb549acb4eddfd045bb55da66c1fd4ff5b1ac5Christian MaederautoProofAtNode :: -- use theorems is subsequent proofs
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -- Timeout Limit
d0bdd8509225b64accad2f9420d6a608e2dcffcaChristian Maeder -- selected goals
f8065e835104ae5eaa148e9b37a81e768990724bEugen Kuksa -- Node selected for proving
a67bea25edc56bbab82c1a1fc6b51e132452188cChristian Maeder -- selected Prover and Comorphism
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder -> ( G_prover, AnyComorphism )
ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder -- returns new GoalStatus for the Node
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder -> ResultT IO (G_theory, [(String, String)])
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederautoProofAtNode useTh timeout goals g_th p_cm = do
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder let knpr = propagateErrors "autoProofAtNode"
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder $ knownProversWithKind ProveCMDLautomatic
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder pf_st = initialState "" g_th knpr
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder sg_st = if null goals then pf_st else pf_st
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder { selectedGoals = filter (`elem` goals) $ selectedGoals pf_st }
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder st = recalculateSublogicAndSelectedTheory sg_st
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder -- try to prepare the theory
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder if null $ selectedGoals st then fail "autoProofAtNode: no goals selected"
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder (G_theory_with_prover lid1 th p) <- liftR $ prepareForProving st p_cm
c5653d37b37dcc025ff6dd1eada95ae67116e699Christian Maeder case proveCMDLautomaticBatch p of
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder fail "autoProofAtNode: failed to init CMDLautomaticBatch"
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder Just fn -> do
61fe8c57f8232d051ad9b483ece8d87b03ced2c7Christian Maeder d <- lift $ do
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder -- mVar to poll the prover for results
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder answ <- newMVar (return [])
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (_, mV) <- fn useTh False answ (theoryName st)
fe9fabab6e959e383a746711b078c8fddbd5e553Christian Maeder (TacticScript $ show timeout) th []
da3ef027f936e2fc0b053e27c9f01bd0c1213d90Christian Maeder takeMVar answ
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder case maybeResult d of
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder Nothing -> fail "autoProofAtNode: proving failed"
58665d6a311aec23a2a6afd33f83b6911f4a9b6fChristian Maeder Just d' -> return
58665d6a311aec23a2a6afd33f83b6911f4a9b6fChristian Maeder ( currentTheory $ markProved (snd p_cm) lid1 d' st
58665d6a311aec23a2a6afd33f83b6911f4a9b6fChristian Maeder , map (\ ps -> (goalName ps, show $ goalStatus ps)) d')