AbstractState.hs revision aed438ce70de05d86d51932a078d829a3f6be5c2
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : State data structure used by the goal management GUI.
2725abe920f91de62ae5c0b7230c1627cccf5fabChristian MaederCopyright : (c) Uni Bremen 2005-2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : luecke@informatik.uni-bremen.de
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederStability : provisional
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : non-portable(Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThe 'ProofState' data structure abstracts the GUI implementation details
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederaway by allowing callback function to use it as the sole input and output.
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederIt is also used by the CMDL interface.
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder ( G_prover (..)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder , getProverName
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder , getCcName
93603bd881e43d4ff5a57d7ca4e2b9fa619f25b4cmaeder , coerceProver
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder , G_cons_checker (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , coerceConsChecker
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , ProofActions (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , ProofState (..)
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist , initialState
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist , selectedGoalMap
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , recalculateSublogicAndSelectedTheory
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , G_theory_with_prover (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , G_theory_with_cons_checker (..)
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder , prepareForProving
85e1d54a475bfc30b3eac5ae6c5e42a2d7e93f10Christian Maeder , prepareForConsChecking
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , getAllProvers
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa , getConsCheckers
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder , lookupKnownProver
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , lookupKnownConsChecker
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , autoProofAtNode
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport qualified Data.Map as Map
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport qualified Data.Set as Set
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport qualified Common.OrderedMap as OMap
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | provers and consistency checkers for specific logics
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maederdata G_prover =
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder sign morphism symbol raw_symbol proof_tree
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sign morphism symbol raw_symbol proof_tree
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder => G_prover lid (Prover sign sentence morphism sublogics proof_tree)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder deriving Typeable
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergetProverName :: G_prover -> String
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedergetProverName (G_prover _ p) = proverName p
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedercoerceProver ::
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder => lid1 -> lid2 -> String
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder -> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder -> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian MaedercoerceProver = primCoerce
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maederdata G_cons_checker =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
2353f65833a3da763392f771223250cd50b8d873Christian Maeder sign morphism symbol raw_symbol proof_tree
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sign morphism symbol raw_symbol proof_tree
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder => G_cons_checker lid
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder (ConsChecker sign sentence sublogics morphism proof_tree)
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder deriving Typeable
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergetCcName :: G_cons_checker -> String
d81905a5b924415c524d702df26204683c82c12eChristian MaedergetCcName (G_cons_checker _ p) = ccName p
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercoerceConsChecker ::
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
cb2044812811d66efe038d914966e04290be93faChristian Maeder => lid1 -> lid2 -> String
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaedercoerceConsChecker = primCoerce
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder-- | Possible actions for GUI which are manipulating ProofState
6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanudata ProofActions lid sentence = ProofActions {
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu -- | called whenever the "Prove" button is clicked
b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanu proveF :: ProofState lid sentence
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu -> IO (Result.Result (ProofState lid sentence)),
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa -- | called whenever the "More fine grained selection" button is clicked
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder fineGrainedSelectionF :: ProofState lid sentence
966519955f5f7111abac20118563132b9dd41165Christian Maeder -> IO (Result.Result (ProofState lid sentence)),
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder -- | called whenever a (de-)selection occured for updating sublogic
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder recalculateSublogicF :: ProofState lid sentence
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder -> IO (ProofState lid sentence)
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder Represents the global state of the prover GUI.
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maederdata ProofState lid sentence =
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder { -- | theory name
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder theoryName :: String,
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder -- | Grothendieck theory
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder theory :: G_theory,
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder -- | translated theory logic id associated with following maps
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder logicId :: lid,
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder -- | sublogic of initial G_theory
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder sublogicOfTheory :: G_sublogics,
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder -- | last used sublogic to determine fitting comorphisms
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder lastSublogic :: G_sublogics,
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -- | goals are stored in a separate map
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder goalMap :: ThSens sentence (AnyComorphism, BasicProof),
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -- | currently known provers
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder proversMap :: KnownProversMap,
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -- | comorphisms fitting with sublogic of this G_theory
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder comorphismsToProvers :: [(G_prover, AnyComorphism)],
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder -- | currently selected goals
93603bd881e43d4ff5a57d7ca4e2b9fa619f25b4cmaeder selectedGoals :: [String],
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder -- | axioms to include for the proof
8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder includedAxioms :: [String],
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- | theorems to include for the proof
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder includedTheorems :: [String],
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- | whether a prover is running or not
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder proverRunning :: Bool,
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaeder -- | accumulated Diagnosis during Proofs
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaeder accDiags :: [Diagnosis],
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- | which prover (if any) is currently selected
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder selectedProver :: Maybe String,
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder -- | which consistency checker (if any) is currently selected
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder selectedConsChecker :: Maybe String,
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder -- | theory based on selected goals, axioms and proven theorems
a9e804dbec424ec36e34bab955cbe90edac5baa6Christian Maeder selectedTheory :: G_theory
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke Creates an initial State.
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus LuettichinitialState ::
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
2353f65833a3da763392f771223250cd50b8d873Christian Maeder sign morphism symbol raw_symbol proof_tree
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> KnownProversMap
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> [(G_prover, AnyComorphism)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> m (ProofState lid sentence)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederinitialState lid thN th@(G_theory lid2 sig ind thSens _) pm cms =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do let (aMap, gMap) = Map.partition (isAxiom . OMap.ele) thSens
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder g_th = G_theory lid2 sig ind aMap startThId
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder sublTh = sublogicOfTh th
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder gMap' <- coerceThSens lid2 lid "creating initial state" gMap
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return ProofState
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder { theoryName = thN
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , theory = g_th
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder , sublogicOfTheory = sublTh
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , lastSublogic = sublTh
cb2044812811d66efe038d914966e04290be93faChristian Maeder , logicId = lid
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , goalMap = gMap'
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder , proversMap = pm
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , comorphismsToProvers = cms
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , selectedGoals = OMap.keys gMap'
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder , includedAxioms = OMap.keys aMap
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , includedTheorems = OMap.keys gMap
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , accDiags = []
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , proverRunning = False
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder , selectedProver =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in if null prvs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder if defaultGUIProver `elem` prvs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder then Just defaultGUIProver
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder , selectedConsChecker = Nothing
966519955f5f7111abac20118563132b9dd41165Christian Maeder , selectedTheory = g_th }
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maederdata G_theory_with_cons_checker =
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder sign morphism symbol raw_symbol proof_tree
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder sign morphism symbol raw_symbol proof_tree
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas => G_theory_with_cons_checker lid
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (TheoryMorphism sign sentence morphism proof_tree)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (ConsChecker sign sentence sublogics morphism proof_tree)
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder-- | a Grothendieck pair of prover and theory which are in the same logic
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maederdata G_theory_with_prover =
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder forall lid sublogics basic_spec sentence symb_items symb_map_items
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder sign morphism symbol raw_symbol proof_tree
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder . Logic lid sublogics basic_spec sentence symb_items symb_map_items
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder sign morphism symbol raw_symbol proof_tree
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder => G_theory_with_prover lid
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder (Theory sign sentence proof_tree)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder (Prover sign sentence morphism sublogics proof_tree)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederprepareForConsChecking ::
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (Logic lid sublogics basic_spec sentence symb_items symb_map_items
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder sign morphism symbol raw_symbol proof_tree)
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder => ProofState lid sentence
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -> (G_cons_checker, AnyComorphism)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> Result G_theory_with_cons_checker
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederprepareForConsChecking st (G_cons_checker lid4 p, Comorphism cid) =
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder case selectedTheory st of
2360728d4185c0c04279c999941c64d36626af79Christian Maeder G_theory lid (ExtSign sign _) _ sens _ ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let lidT = targetLogic cid
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder bTh' <- coerceBasicTheory lid (sourceLogic cid)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder "Proofs.InferBasic.callProver: basic theory"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (sign, toNamedList sens)
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder (sign'', sens'') <- wrapMapTheory cid bTh'
2360728d4185c0c04279c999941c64d36626af79Christian Maeder incl <- subsig_inclusion lidT (empty_signature lidT) sign''
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let mor = TheoryMorphism
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder { tSource = emptyTheory lidT
2360728d4185c0c04279c999941c64d36626af79Christian Maeder , tTarget = Theory sign'' (toThSens sens'')
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , tMorphism = incl }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder p' <- coerceConsChecker lid4 lidT "" p
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return $ G_theory_with_cons_checker lidT mor p'
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder{- | prepare the selected theory of the state for proving with the
966519955f5f7111abac20118563132b9dd41165Christian Maeder * translation along the comorphism
5a448e9be8c4482a978b174b744237757335140fChristian Maeder * all coercions
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder * the lid is valid for the prover and the translated theory
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras JakubauskasprepareForProving ::
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (Logic lid sublogics basic_spec sentence symb_items symb_map_items
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder sign morphism symbol raw_symbol proof_tree)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder => ProofState lid sentence
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder -> (G_prover, AnyComorphism)
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder -> Result G_theory_with_prover
a31430de8b0632d29f42634d6395e982bf31b14dChristian MaederprepareForProving st (G_prover lid4 p, Comorphism cid) =
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder case selectedTheory st of
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder G_theory lid (ExtSign sign _) _ sens _ ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let lidT = targetLogic cid
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder bTh' <- coerceBasicTheory lid (sourceLogic cid)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder "Proofs.InferBasic.callProver: basic theory"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (sign, toNamedList sens)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (sign'', sens'') <- wrapMapTheory cid bTh'
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder p' <- coerceProver lid4 lidT "" p
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder G_theory_with_prover lidT (Theory sign'' (toThSens sens'')) p'
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder-- | returns the map of currently selected goals
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaederselectedGoalMap :: ProofState lid sentence
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder -> ThSens sentence (AnyComorphism, BasicProof)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederselectedGoalMap st = filterMapWithList (selectedGoals st) (goalMap st)
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder-- | returns the axioms of the state coerced into the state's logicId
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder sign morphism symbol raw_symbol proof_tree
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder => ProofState lid sentence
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder -> m (ThSens sentence (AnyComorphism, BasicProof))
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaederaxiomMap s =
cb2044812811d66efe038d914966e04290be93faChristian Maeder case theory s of
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder G_theory lid _ _ aM _ ->
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder coerceThSens lid (logicId s) "Proofs.GUIState.axiomMap" aM
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder recalculation of sublogic upon (de)selection of goals, axioms and
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder proven theorems
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaederrecalculateSublogicAndSelectedTheory ::
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder (Logic lid sublogics basic_spec sentence symb_items symb_map_items
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder sign morphism symbol raw_symbol proof_tree)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa => ProofState lid sentence -> ProofState lid sentence
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederrecalculateSublogicAndSelectedTheory st = case theory st of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder G_theory lid sign _ sens _ ->
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder -- coerce goalMap
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder case coerceThSens (logicId st) lid "" $ goalMap st of
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder Nothing -> error
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder "Proofs.InferBasic.recalculateSublogic: selected goals"
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder Just ths -> let
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder -- partition goalMap
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder (sel_goals, other_goals) =
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder let selected k _ = Set.member k s
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder s = Set.fromList (selectedGoals st)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder {- to properly rerun proofs only proven theorems
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder before the first open one should be included! -}
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder provenThs = OMap.filter isProvenSenStatus other_goals
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder sel_provenThs = markAsAxiom True $
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder filterMapWithList (includedTheorems st) provenThs
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder sel_sens = filterMapWithList (includedAxioms st) sens
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder selAxs = Map.union sel_sens sel_provenThs
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder currentThSens = Map.union selAxs sel_goals
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder sTh = G_theory lid sign startSigId currentThSens startThId
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder sLo = sublogicOfTh sTh
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in st { sublogicOfTheory = sLo
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , selectedTheory = sTh
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , proversMap = shrinkKnownProvers sLo (proversMap st) }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedergetConsCheckers = concatMap (\ cm@(Comorphism cid) ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder map (\ cc -> (G_cons_checker (targetLogic cid) cc, cm))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $ cons_checkers $ targetLogic cid)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederlookupKnownConsChecker ::
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa sign morphism symbol raw_symbol proof_tree
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder => ProofState lid sentence -> m (G_cons_checker, AnyComorphism)
966519955f5f7111abac20118563132b9dd41165Christian MaederlookupKnownConsChecker st =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder let sl = sublogicOfTheory st
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder pr_s <- selectedConsChecker st
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ps <- Map.lookup pr_s (proversMap st)
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder return (pr_s, ps)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder matchingCC s (gp, _) = case gp of
cb2044812811d66efe038d914966e04290be93faChristian Maeder G_cons_checker _ p -> ccName p == s
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder findCC (pr_n, cms) =
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder case filter (matchingCC pr_n) $ getConsCheckers
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $ filter (lessSublogicComor sl) cms of
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder [] -> fail ("CMDL.ProverConsistency.lookupKnownConsChecker" ++
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ": no consistency checker found")
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder p : _ -> return p
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in maybe ( fail ("CMDL.ProverConsistency.lookupKnownConsChecker: " ++
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder "no matching known prover")) findCC mt
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederlookupKnownProver ::
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder sign morphism symbol raw_symbol proof_tree
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder => ProofState lid sentence -> ProverKind -> m (G_prover, AnyComorphism)
33fcc19ef2b59493b4e91eebf701df95fd230765Christian MaederlookupKnownProver st pk =
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder let sl = sublogicOfTheory st
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder mt = do -- Monad Maybe
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa pr_s <- selectedProver st
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ps <- Map.lookup pr_s (proversMap st)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder return (pr_s, ps)
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas matchingPr s (gp, _) = case gp of
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder G_prover _ p -> proverName p == s
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder findProver (pr_n, cms) =
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder case filter (matchingPr pr_n) $ getProvers pk sl
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder $ filter (lessSublogicComor sl) cms of
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder [] -> fail "Proofs.InferBasic: no prover found"
9b3e946be44391d35acb2168f4e67d629e560f79Till Mossakowski p : _ -> return p
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in maybe (fail "Proofs.InferBasic: no matching known prover")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder findProver mt
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder-- | Pairs each target prover of these comorphisms with its comorphism
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedergetProvers :: ProverKind -> G_sublogics -> [AnyComorphism]
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -> [(G_prover, AnyComorphism)]
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian MaedergetProvers pk (G_sublogics lid sl) =
2360728d4185c0c04279c999941c64d36626af79Christian Maeder foldl addProvers [] . filter hasModelExpansion where
2360728d4185c0c04279c999941c64d36626af79Christian Maeder addProvers acc cm = case cm of
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa Comorphism cid -> let
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder slid = sourceLogic cid
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder tlid = targetLogic cid
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in acc ++ foldl
2360728d4185c0c04279c999941c64d36626af79Christian Maeder if hasProverKind pk p
2360728d4185c0c04279c999941c64d36626af79Christian Maeder && language_name lid == language_name slid
0130083f314580170af1195037be3325f125fbceChristian Maeder && maybe False (flip isSubElem $ proverSublogic p)
d81905a5b924415c524d702df26204683c82c12eChristian Maeder (mapSublogic cid $ forceCoerceSublogic lid slid sl)
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder then (G_prover tlid p, cm) : l else l)
2360728d4185c0c04279c999941c64d36626af79Christian Maeder [] (provers tlid)
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian MaedergetAllProvers :: ProverKind -> G_sublogics -> LogicGraph
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -> [(G_prover, AnyComorphism)]
bc263f610d20a9cd3014ddfca903026127fa0d48Christian MaedergetAllProvers pk sl lg = getProvers pk sl $ findComorphismPaths lg sl
2360728d4185c0c04279c999941c64d36626af79Christian Maeder{- | the list of proof statuses is integrated into the goalMap of the state
2360728d4185c0c04279c999941c64d36626af79Christian Maederafter validation of the Disproved Statuses -}
2360728d4185c0c04279c999941c64d36626af79Christian Maeder ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder sign morphism symbol raw_symbol proof_tree
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2360728d4185c0c04279c999941c64d36626af79Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 )
2360728d4185c0c04279c999941c64d36626af79Christian Maeder => AnyComorphism -> lid -> [ProofStatus proof_tree]
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -> ProofState lid2 sentence2
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -> ProofState lid2 sentence2
2360728d4185c0c04279c999941c64d36626af79Christian MaedermarkProved c lid status st =
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder st { goalMap = markProvedGoalMap c lid status (goalMap st)}
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder-- | mark all newly proven goals with their proof tree
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaedermarkProvedGoalMap ::
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder sign morphism symbol raw_symbol proof_tree
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder => AnyComorphism -> lid -> [ProofStatus proof_tree]
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder -> ThSens a (AnyComorphism, BasicProof)
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder -> ThSens a (AnyComorphism, BasicProof)
2360728d4185c0c04279c999941c64d36626af79Christian MaedermarkProvedGoalMap c lid status thSens = foldl upd thSens status
2360728d4185c0c04279c999941c64d36626af79Christian Maeder where upd m pStat = OMap.update (updStat pStat) (goalName pStat) m
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa updStat ps s = Just $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder s { senAttr = ThmStatus $ (c, BasicProof lid ps) : thmStatus s}
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederautoProofAtNode :: -- use theorems is subsequent proofs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- Timeout Limit
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- Node selected for proving
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- selected Prover and Comorphism
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> ( G_prover, AnyComorphism )
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder -- returns new GoalStatus for the Node
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder -> IO (Maybe G_theory, Maybe [(String, String)])
91e24fc45834b35f2a3830d72565640251149bf3Christian MaederautoProofAtNode useTh timeout g_th@( G_theory lid _ _ _ _ ) p_cm = do
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder let knpr = propagateErrors "autoProofAtNode"
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder $ knownProversWithKind ProveCMDLautomatic
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder pf_st <- initialState lid "" g_th knpr [p_cm]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let st = recalculateSublogicAndSelectedTheory pf_st
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- try to prepare the theory
d56ece59c372cb887355825901222b9f3377f7e6Thiemo Wiedemeyer if null $ selectedGoals st then return (Nothing, Just []) else
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case maybeResult $ prepareForProving st p_cm of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Nothing -> return (Nothing, Nothing)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just (G_theory_with_prover lid1 th p) ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case proveCMDLautomaticBatch p of
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Nothing -> return (Nothing, Nothing)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just fn -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -- mVar to poll the prover for results
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder answ <- newMVar (return [])
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (_, mV) <- fn useTh False answ (theoryName st)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (TacticScript $ show timeout) th []
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist d <- takeMVar answ
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder return $ case maybeResult d of
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder Nothing -> (Nothing, Nothing)
a166da43d4e8f9dfa7a2651d033c6bea02627ca6Mihai Codescu let ps' = markProved (snd p_cm) lid1 d' st
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder in case theory ps' of
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder G_theory lidT sigT indT sensT _ ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case coerceThSens (logicId ps') lidT "" (goalMap ps') of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> (Nothing, Nothing)
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz Just gMap -> (Just $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder G_theory lidT sigT indT (Map.union sensT gMap)
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz map (\ ps -> (goalName ps, show $ goalStatus ps)) d')