AbstractState.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
ccf9d4a5c6453fa9f8b839baeee25147865fbb7dJames Phillpotts{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterDescription : State data structure used by the goal management GUI.
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterCopyright : (c) Uni Bremen 2005-2007
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterLicense : GPLv2 or higher, see LICENSE.txt
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterMaintainer : luecke@informatik.uni-bremen.de
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterStability : provisional
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterPortability : non-portable(Logic)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterThe 'ProofState' data structure abstracts the GUI implementation details
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosteraway by allowing callback function to use it as the sole input and output.
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterIt is also used by the CMDL interface.
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ( ProverOrConsChecker (..)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , G_prover (..)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , G_proof_tree (..)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , getProverName
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , getCcBatch
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , coerceProver
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , G_cons_checker (..)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , coerceConsChecker
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington , ProofActions (..)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , ProofState (..)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , sublogicOfTheory
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , initialState
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnell , resetSelection
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , recalculateSublogicAndSelectedTheory
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , markProved
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , G_theory_with_prover (..)
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , G_theory_with_cons_checker (..)
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , prepareForProving
997d6667b8c483bf582a231b1b24f84fbe6c8390Neil Madden , prepareForConsChecking
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , isSubElemG
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , pathToComorphism
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , getAllProvers
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , getUsableProvers
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , getConsCheckers
a90aba9cbcbb8e7fe95e45590d853959efe0d354Tom Rumsey , getAllConsCheckers
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , lookupKnownProver
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , lookupKnownConsChecker
26304a2a091af368cfc16c977bcce6d17195360aTom Rumsey , autoProofAtNode
26304a2a091af368cfc16c977bcce6d17195360aTom Rumseyimport qualified Data.Map as Map
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnellimport qualified Common.OrderedMap as OMap
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnellimport Common.Result as Result
01a939641aeb0a095851921879620c3fab295cb2Robert Wapshottimport Unsafe.Coerce (unsafeCoerce)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- import Interfaces.DataTypes (IntState)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata ProverOrConsChecker = Prover G_prover
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster | ConsChecker G_cons_checker
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster deriving (Show)
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey-- | provers and consistency checkers for specific logics
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumseydata G_prover =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster forall lid sublogics basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnell . Logic lid sublogics basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnell => G_prover lid (Prover sign sentence morphism sublogics proof_tree)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster deriving Typeable
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Show G_prover where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster show = getProverName
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetProverName :: G_prover -> String
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetProverName (G_prover _ p) = proverName p
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterusable :: G_prover -> IO Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterusable (G_prover _ p) = fmap isNothing $ proverUsable p
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercoerceProver ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => lid1 -> lid2 -> String
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercoerceProver = primCoerce
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata G_cons_checker =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster forall lid sublogics basic_spec sentence symb_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster symb_map_items sign morphism symbol raw_symbol proof_tree
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster . Logic lid sublogics basic_spec sentence symb_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster symb_map_items sign morphism symbol raw_symbol proof_tree
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => G_cons_checker lid
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (ConsChecker sign sentence sublogics morphism proof_tree)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster deriving (Typeable)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Show G_cons_checker where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster show _ = "G_cons_checker "
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetCcName :: G_cons_checker -> String
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetCcName (G_cons_checker _ p) = ccName p
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill CunningtongetCcBatch :: G_cons_checker -> Bool
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill CunningtongetCcBatch (G_cons_checker _ p) = ccBatch p
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill CunningtonusableCC :: G_cons_checker -> IO Bool
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill CunningtonusableCC (G_cons_checker _ p) = fmap isNothing $ ccUsable p
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercoerceConsChecker ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign1 morphism1 symbol1 raw_symbol1 proof_tree1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign2 morphism2 symbol2 raw_symbol2 proof_tree2
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell => lid1 -> lid2 -> String
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnell -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnellcoerceConsChecker = primCoerce
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell-- | provers and consistency checkers for specific logics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata G_proof_tree =
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnell forall lid sublogics basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell . Logic lid sublogics basic_spec sentence symb_items symb_map_items
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell sign morphism symbol raw_symbol proof_tree
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell => G_proof_tree lid proof_tree
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell deriving Typeable
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnellinstance Show G_proof_tree where
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell show (G_proof_tree _ pt) = show pt
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott-- | Possible actions for GUI which are manipulating ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata ProofActions = ProofActions {
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | called whenever the "Prove" button is clicked
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proveF :: ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> IO (Result.Result ProofState),
bbffed9376e4fad86c443ca698c2fae6e9e81358David Luna -- | called whenever the "More fine grained selection" button is clicked
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster fineGrainedSelectionF :: ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> IO (Result.Result ProofState),
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | called whenever a (de-)selection occured for updating sublogic
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey recalculateSublogicF :: ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> IO ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Represents the global state of the prover GUI.
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata ProofState =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster { -- | theory name
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster theoryName :: String,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | Grothendieck theory
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster currentTheory :: G_theory,
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey -- | currently known provers
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proversMap :: KnownProversMap,
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott -- | currently selected goals
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott selectedGoals :: [String],
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | axioms to include for the proof
d0da70ccbba38b773e7a7cc71bc124b06206d201Robert Wapshott includedAxioms :: [String],
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | theorems to include for the proof
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford includedTheorems :: [String],
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | whether a prover is running or not
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proverRunning :: Bool,
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey -- | accumulated Diagnosis during Proofs
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster accDiags :: [Diagnosis],
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | comorphisms fitting with sublogic of this G_theory
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster comorphismsToProvers :: [(G_prover, AnyComorphism)],
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | which prover (if any) is currently selected
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster selectedProver :: Maybe String,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | which consistency checker (if any) is currently selected
72450cb9c2ca854c6d3479832c2738196c1d3282Robert Wapshott selectedConsChecker :: Maybe String,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- | theory based on selected goals, axioms and proven theorems
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster selectedTheory :: G_theory
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott } deriving Show
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottresetSelection :: ProofState -> ProofState
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony BamfordresetSelection s = case currentTheory s of
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott G_theory _ _ _ _ sens _ ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let (aMap, gMap) = OMap.partition isAxiom sens
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott { selectedGoals = Map.keys gMap
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , includedAxioms = Map.keys aMap
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , includedTheorems = gs }
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshotttoAxioms :: ProofState -> [String]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostertoAxioms = map (\ (k, wTh) -> if wTh then "(Th) " ++ k else k)
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottgetAxioms :: ProofState -> [(String, Bool)]
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottgetAxioms = getThAxioms . currentTheory
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetGoals :: ProofState -> [(String, Maybe BasicProof)]
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottgetGoals = getThGoals . currentTheory
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott Creates an initial State.
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottinitialState :: String
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott -> KnownProversMap
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott -> ProofState
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottinitialState thN th pm = resetSelection
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott { theoryName = thN
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , currentTheory = th
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , proversMap = pm
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , selectedGoals = []
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , includedAxioms = []
a90aba9cbcbb8e7fe95e45590d853959efe0d354Tom Rumsey , includedTheorems = []
3cfef899c650ea8fa23c64ad5a66b8986bf77bb2Tom Rumsey , proverRunning = False
3cfef899c650ea8fa23c64ad5a66b8986bf77bb2Tom Rumsey , accDiags = []
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , comorphismsToProvers = []
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , selectedProver =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let prvs = Map.keys pm
a90aba9cbcbb8e7fe95e45590d853959efe0d354Tom Rumsey in if null prvs
a90aba9cbcbb8e7fe95e45590d853959efe0d354Tom Rumsey then Nothing
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott if defaultGUIProver `elem` prvs
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster then Just defaultGUIProver
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , selectedConsChecker = Nothing
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott , selectedTheory = th }
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottlogicId :: ProofState -> String
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottlogicId s = case currentTheory s of
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott G_theory lid _ _ _ _ _ -> language_name lid
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottsublogicOfTheory :: ProofState -> G_sublogics
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottsublogicOfTheory = sublogicOfTh . selectedTheory
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshottdata G_theory_with_cons_checker =
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott forall lid sublogics basic_spec sentence symb_items symb_map_items
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott sign morphism symbol raw_symbol proof_tree
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott . Logic lid sublogics basic_spec sentence symb_items symb_map_items
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott sign morphism symbol raw_symbol proof_tree
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott => G_theory_with_cons_checker lid
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott (TheoryMorphism sign sentence morphism proof_tree)
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott (ConsChecker sign sentence sublogics morphism proof_tree)
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott-- | a Grothendieck pair of prover and theory which are in the same logic
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshottdata G_theory_with_prover =
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott forall lid sublogics basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford . Logic lid sublogics basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => G_theory_with_prover lid
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (Theory sign sentence proof_tree)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (Prover sign sentence morphism sublogics proof_tree)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata GPlainTheory =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster forall lid sublogics basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree
6309b849c2de831a0eaed9c27b5794bed9bd8fd1Neil Madden . Logic lid sublogics basic_spec sentence symb_items symb_map_items
6309b849c2de831a0eaed9c27b5794bed9bd8fd1Neil Madden sign morphism symbol raw_symbol proof_tree
6309b849c2de831a0eaed9c27b5794bed9bd8fd1Neil Madden => GPlainTheory lid (Theory sign sentence proof_tree)
6309b849c2de831a0eaed9c27b5794bed9bd8fd1Neil MaddenprepareForConsChecking :: ProofState
6309b849c2de831a0eaed9c27b5794bed9bd8fd1Neil Madden -> (G_cons_checker, AnyComorphism)
6309b849c2de831a0eaed9c27b5794bed9bd8fd1Neil Madden -> Result G_theory_with_cons_checker
6309b849c2de831a0eaed9c27b5794bed9bd8fd1Neil MaddenprepareForConsChecking st (G_cons_checker lid4 p, co) = do
6309b849c2de831a0eaed9c27b5794bed9bd8fd1Neil Madden GPlainTheory lidT th@(Theory sign'' _) <- prepareTheory st co
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster incl <- subsig_inclusion lidT (empty_signature lidT) sign''
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let mor = TheoryMorphism
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford { tSource = emptyTheory lidT
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , tTarget = th
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , tMorphism = incl }
7b3fa0c4c626865e92012ef9f885e91d945850eaCraig McDonnell p' <- coerceConsChecker lid4 lidT "" p
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster return $ G_theory_with_cons_checker lidT mor p'
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterprepareTheory :: ProofState -> AnyComorphism -> Result GPlainTheory
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterprepareTheory st (Comorphism cid) = case selectedTheory st of
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford G_theory lid _ (ExtSign sign _) _ sens _ -> do
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster bTh' <- coerceBasicTheory lid (sourceLogic cid)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster "Proofs.AbstractState.prepareTheory: basic theory"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (sign, toNamedList sens)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (sign'', sens'') <- wrapMapTheory cid bTh'
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster return . GPlainTheory (targetLogic cid) . Theory sign''
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster $ toThSens sens''
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster{- | prepare the selected theory of the state for proving with the
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamfordgiven prover:
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster * translation along the comorphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster * all coercions
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster * the lid is valid for the prover and the translated theory
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterprepareForProving :: ProofState
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford -> (G_prover, AnyComorphism)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> Result G_theory_with_prover
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterprepareForProving st (G_prover lid4 p, co) = do
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster GPlainTheory lidT th <- prepareTheory st co
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster p' <- coerceProver lid4 lidT "" p
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster return $ G_theory_with_prover lidT th p'
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | creates the currently selected theory
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermakeSelectedTheory :: ProofState -> G_theory
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony BamfordmakeSelectedTheory s = case currentTheory s of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster G_theory lid syn sig si sens _ ->
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford -- axiom map, goal map
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let (aMap, gMap) = OMap.partition isAxiom sens
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- proven goals map
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster pMap = OMap.filter isProvenSenStatus gMap
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster G_theory lid syn sig si
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster [ filterMapWithList (selectedGoals s) gMap
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , filterMapWithList (includedAxioms s) aMap
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , markAsAxiom True $ filterMapWithList (includedTheorems s) pMap
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ]) startThId
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster recalculation of sublogic upon (de)selection of goals, axioms and
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proven theorems
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterrecalculateSublogicAndSelectedTheory :: ProofState -> ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterrecalculateSublogicAndSelectedTheory st = let
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sTh = makeSelectedTheory st
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey sLo = sublogicOfTh sTh
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster { selectedTheory = sTh
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , proversMap = shrinkKnownProvers sLo $ proversMap st }
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom RumseygetConsCheckers :: [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetConsCheckers = filterM (usableCC . fst) . getAllConsCheckers
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetAllConsCheckers = concatMap (\ cm@(Comorphism cid) ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster map (\ cc -> (G_cons_checker (targetLogic cid) cc, cm))
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster $ cons_checkers $ targetLogic cid)
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony BamfordlookupKnownConsChecker :: Monad m => ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> m (G_cons_checker, AnyComorphism)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterlookupKnownConsChecker st =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let sl = sublogicOfTh (selectedTheory st)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster pr_s <- selectedConsChecker st
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ps <- Map.lookup pr_s (proversMap st)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster return (pr_s, ps)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster matchingCC s (gp, _) = case gp of
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford G_cons_checker _ p -> ccName p == s
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster findCC (pr_n, cms) =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster case filter (matchingCC pr_n) $ getAllConsCheckers
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster $ filter (lessSublogicComor sl) cms of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster [] -> fail ("CMDL.ProverConsistency.lookupKnownConsChecker" ++
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ": no consistency checker found")
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster p : _ -> return p
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington in maybe ( fail ("CMDL.ProverConsistency.lookupKnownConsChecker: " ++
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster "no matching known prover")) findCC mt
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterlookupKnownProver :: Monad m => ProofState -> ProverKind
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> m (G_prover, AnyComorphism)
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony BamfordlookupKnownProver st pk =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let sl = sublogicOfTh (selectedTheory st)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster mt = do -- Monad Maybe
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster pr_s <- selectedProver st
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ps <- Map.lookup pr_s (proversMap st)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster return (pr_s, ps)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster matchingPr s (gp, _) = case gp of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster G_prover _ p -> proverName p == s
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington findProver (pr_n, cms) =
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington case filter (matchingPr pr_n) $ getProvers pk sl
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington $ filter (lessSublogicComor sl) cms of
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington [] -> fail "Proofs.InferBasic: no prover found"
fd21d481e26774c37a197c7cc8ab56096a21e7aaPhill Cunnington p : _ -> return p
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey in maybe (fail "Proofs.InferBasic: no matching known prover")
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster findProver mt
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | Pairs each target prover of these comorphisms with its comorphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetProvers :: ProverKind -> G_sublogics -> [AnyComorphism]
87d68743726585ee101ba2e7be2cf06cd34ebb80Neil Madden -> [(G_prover, AnyComorphism)]
87d68743726585ee101ba2e7be2cf06cd34ebb80Neil MaddengetProvers pk (G_sublogics lid sl) =
87d68743726585ee101ba2e7be2cf06cd34ebb80Neil Madden foldl addProvers [] where
87d68743726585ee101ba2e7be2cf06cd34ebb80Neil Madden addProvers acc cm = case cm of
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington Comorphism cid -> let
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington slid = sourceLogic cid
87d68743726585ee101ba2e7be2cf06cd34ebb80Neil Madden tlid = targetLogic cid
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington in acc ++ foldl
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington if hasProverKind pk p
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington && language_name lid == language_name slid
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington && maybe False (flip isSubElem $ proverSublogic p)
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington (mapSublogic cid $ forceCoerceSublogic lid slid sl)
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington then (G_prover tlid p, cm) : l else l)
47c2be2db219abf98d491a0a6625380421d61e42Phill Cunnington [] (provers tlid)
87d68743726585ee101ba2e7be2cf06cd34ebb80Neil MaddenknownProvers :: LogicGraph -> ProverKind -> Map.Map G_sublogics [G_prover]
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom RumseyknownProvers lg pk =
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey let l = Map.elems $ logics lg
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey in foldl (\ m (Logic lid) -> foldl (\ m' p ->
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey let lgx = G_sublogics lid (proverSublogic p)
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey p' = G_prover lid p
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey in case Map.lookup lgx m' of
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey Just ps -> Map.insert lgx (p' : ps) m'
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey Nothing -> Map.insert lgx [p'] m') m $
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster filter (hasProverKind pk)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (provers lid)) Map.empty l
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterunsafeCompComorphism :: AnyComorphism -> AnyComorphism -> AnyComorphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterunsafeCompComorphism c1 c2 = case compComorphism c1 c2 of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Result _ (Just c_new) -> c_new
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster r -> propagateErrors "Proofs.AbstractState.unsafeCompComorphism" r
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisSubElemG :: G_sublogics -> G_sublogics -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisSubElemG (G_sublogics lid sl) (G_sublogics lid1 sl1) =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Logic lid == Logic lid1 &&
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster isSubElem sl (Unsafe.Coerce.unsafeCoerce sl1)
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnellpathToComorphism :: ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey -> AnyComorphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterpathToComorphism (path, (G_sublogics lid sub, _)) =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster case path of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster [] -> Comorphism $ mkIdComorphism lid sub
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ((G_sublogics lid1 sub1, _), c) : cs ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster foldl unsafeCompComorphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (Comorphism $ mkIdComorphism lid1 sub1)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (c : snd (unzip cs))
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetUsableProvers :: ProverKind -> G_sublogics -> LogicGraph
c184142912cff04e5442d8bf70febe477285fb1cCraig McDonnell -> IO [(G_prover, AnyComorphism)]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetUsableProvers pk start =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster filterM (usable . fst) . getAllProvers pk start
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostergetAllProvers :: ProverKind -> G_sublogics -> LogicGraph
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> [(G_prover, AnyComorphism)]
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony BamfordgetAllProvers pk start lg =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let kp = knownProvers lg pk
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster g = logicGraph2Graph lg
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster in concatMap (mkComorphism kp) $
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster concatMap (\ end ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster yen 10 (start, Nothing) (\ (l, _) -> isSubElemG l end) g)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster mkComorphism :: Map.Map G_sublogics [t2]
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott -> ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey -> [(t2, AnyComorphism)]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster mkComorphism kp path@(_, (end, _)) =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let fullComorphism = pathToComorphism path
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster cs = Map.toList $ Map.filterWithKey (\ l _ -> isSubElemG end l) kp
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford in concatMap (\ x -> case x of
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell (_, ps) -> map (\ p -> (p, fullComorphism)) ps) cs
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster{- | the list of proof statuses is integrated into the goalMap of the state
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterafter validation of the Disproved Statuses -}
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermarkProved ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree )
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => AnyComorphism -> lid -> [ProofStatus proof_tree]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> ProofState
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermarkProved c lid status st = st
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster { currentTheory = markProvedGoalMap c lid status (currentTheory st) }
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | mark all newly proven goals with their proof tree
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert WapshottmarkProvedGoalMap ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree )
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => AnyComorphism -> lid -> [ProofStatus proof_tree]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> G_theory -> G_theory
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermarkProvedGoalMap c lid status th = case th of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster G_theory lid1 syn sig si thSens _ ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let updStat ps s = Just $
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster s { senAttr = ThmStatus $ (c, BasicProof lid ps) : thmStatus s }
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster upd pStat = OMap.update (updStat pStat) (goalName pStat)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster in G_theory lid1 syn sig si (foldl (flip upd) thSens status)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterautoProofAtNode ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- use theorems is subsequent proofs
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- Timeout Limit
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- selected goals
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- selected axioms
321cc59fdbbb9b6eebdfc714f2d86b785965d50eTom Rumsey -- Node selected for proving
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- selected Prover and Comorphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> ( G_prover, AnyComorphism )
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- returns new GoalStatus for the Node
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford -> ResultT IO ((G_theory, [(String, String, String)]),
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (ProofState, [ProofStatus G_proof_tree]))
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterautoProofAtNode useTh timeout goals axioms g_th p_cm = do
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford let knpr = propagateErrors "autoProofAtNode"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster $ knownProversWithKind ProveCMDLautomatic
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster pf_st = initialState "" g_th knpr
35ab1c5bca11317474fe12bdd8d22c17cdaf2697Robert Wapshott sg_st = if null goals then pf_st else pf_st
cc7c18212481f5e9ee508afe2ffcaecb6b9330f5Craig McDonnell { selectedGoals = filter (`elem` goals) $ selectedGoals pf_st }
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sa_st = if null axioms then sg_st else sg_st
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster { includedAxioms = filter (`elem` axioms) $ includedAxioms sg_st }
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster st = recalculateSublogicAndSelectedTheory sa_st
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- try to prepare the theory
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster if null $ selectedGoals st then fail "autoProofAtNode: no goals selected"
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford (G_theory_with_prover lid1 th p) <- liftR $ prepareForProving st p_cm
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster case proveCMDLautomaticBatch p of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster fail "autoProofAtNode: failed to init CMDLautomaticBatch"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Just fn -> do
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let encapsulate_pt ps =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ps {proofTree = G_proof_tree lid1 $ proofTree ps}
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster d <- lift $ do
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- mVar to poll the prover for results
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster answ <- newMVar (return [])
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (_, mV) <- fn useTh False answ (theoryName st)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (TacticScript $ show timeout) th []
a90aba9cbcbb8e7fe95e45590d853959efe0d354Tom Rumsey takeMVar answ
72450cb9c2ca854c6d3479832c2738196c1d3282Robert Wapshott case maybeResult d of
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Nothing -> fail "autoProofAtNode: proving failed"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster return (( currentTheory $ markProved (snd p_cm) lid1 d' st
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , map (\ ps -> ( goalName ps
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , show $ goalStatus ps
0c893a059f84246bf91e2f0fbf63e4c92f8e5165Tony Bamford , show $ proofTree ps)) d')
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , (st, map encapsulate_pt d'))