hets/Proofs/AbstractState.hs

	AbstractState.hs revision fdf94376fa12e6f685f87741be2f3d02e03c429e
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen{- |
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenModule      :  $Header$
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenDescription :  State data structure used by the goal management GUI.
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenCopyright   :  (c) Rene Wagner, Klaus L�ttich, Rainer Grabbe, Uni Bremen 2005-2007
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenMaintainer  :  luecke@informatik.uni-bremen.de
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenStability   :  provisional
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenPortability :  non-portable(Logic)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenThe 'ProofState' data structure abstracts the GUI implementation details
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenaway by allowing callback function to use it as the sole input and output.
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenIt is also used by the CMDL interface.
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-}
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenmodule Proofs.AbstractState
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    ( ProofActions(..)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , ProofState
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , theoryName, theory, logicId, sublogicOfTheory, lastSublogic
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , goalMap, proversMap, comorphismsToProvers, selectedGoals
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , includedAxioms, includedTheorems, proverRunning, accDiags
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , selectedProver, selectedTheory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , initialState
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , selectedGoalMap, axiomMap
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , recalculateSublogicAndSelectedTheory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , GetPName(..)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , getGoals, markProved, prepareForProving
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , getProvers, getConsCheckers
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    , lookupKnownProver
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    ) where
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport qualified Data.Map as Map
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport qualified Data.Set as Set
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Data.Graph.Inductive.Graph
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Data.List (find)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport qualified Common.OrderedMap as OMap
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Common.Result as Result
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Common.AS_Annotation
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Common.Utils
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Common.ExtSign
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Logic.Logic
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Logic.Prover
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Logic.Grothendieck
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Logic.Comorphism
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Logic.Coerce
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Syntax.AS_Library (LIB_NAME)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Syntax.Print_AS_Library()
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Comorphisms.KnownProvers
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Static.GTheory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Static.DevGraph
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenimport Static.DGToSpec (computeLocalTheory)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- | Possible actions for GUI which are manipulating ProofState
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowendata ProofActions lid sentence = ProofActions {
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    -- | called whenever the "Prove" button is clicked
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    proveF :: (ProofState lid sentence
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen               -> IO (Result.Result (ProofState lid sentence))),
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    -- | called whenever the "More fine grained selection" button is clicked
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    fineGrainedSelectionF :: (ProofState lid sentence
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                          -> IO (Result.Result (ProofState lid sentence))),
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    -- | called whenever a (de-)selection occured for updating sublogic
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    recalculateSublogicF :: (ProofState lid sentence
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                             -> IO (ProofState lid sentence))
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen  }
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen{- |
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen  Represents the global state of the prover GUI.
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-}
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowendata ProofState lid sentence =
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen     ProofState
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen      { -- | theory name
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        theoryName :: String,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | Grothendieck theory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        theory :: G_theory,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | translated theory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | logic id associated with following maps
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        logicId :: lid,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | sublogic of initial G_theory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        sublogicOfTheory :: G_sublogics,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | last used sublogic to determine fitting comorphisms
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        lastSublogic :: G_sublogics,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | goals are stored in a separate map
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        goalMap :: ThSens sentence (AnyComorphism,BasicProof),
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | currently known provers
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        proversMap :: KnownProversMap,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | comorphisms fitting with sublogic of this G_theory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        comorphismsToProvers :: [(G_prover,AnyComorphism)],
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | currently selected goals
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        selectedGoals :: [String],
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | axioms to include for the proof
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        includedAxioms :: [String],
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | theorems to include for the proof
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        includedTheorems :: [String],
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | whether a prover is running or not
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        proverRunning :: Bool,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | accumulated Diagnosis during Proofs
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        accDiags :: [Diagnosis],
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | which prover (if any) is currently selected
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        selectedProver :: Maybe String,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        -- | Grothendieck theory based upon currently selected goals, axioms
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        --   and proven theorems
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        selectedTheory :: G_theory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen      }
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen{- |
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen  Creates an initial State.
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-}
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BoweninitialState ::
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    (Logic  lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                 sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen     Monad m) =>
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                lid1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen              -> String
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen             -> G_theory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen             -> KnownProversMap
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen             -> [(G_prover,AnyComorphism)]
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen             -> m (ProofState lid1 sentence1)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BoweninitialState lid1 thN th@(G_theory lid2 sig ind thSens _) pm cms =
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    do let (aMap,gMap) = Map.partition (isAxiom . OMap.ele) thSens
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen           g_th = G_theory lid2 sig ind aMap 0
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen           sublTh = sublogicOfTh th
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen       gMap' <- coerceThSens lid2 lid1 "creating initial state" gMap
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen       return $
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen           ProofState { theoryName = thN,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           theory = g_th,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           sublogicOfTheory = sublTh,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           lastSublogic = sublTh,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           logicId = lid1,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           goalMap = gMap',
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           proversMap = pm,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           comorphismsToProvers = cms,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           selectedGoals = OMap.keys gMap',
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           includedAxioms = OMap.keys aMap,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           includedTheorems = OMap.keys gMap,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           accDiags = [],
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           proverRunning = False,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                           selectedProver =
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                               let prvs = Map.keys pm
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                               in if null prvs
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                                  then Nothing
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                                  else
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                                    if defaultGUIProver `elem` prvs
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                                       then Just defaultGUIProver
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                                       else Nothing
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                          ,selectedTheory = g_th
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                         }
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- | prepare the selected theory of the state for proving with the
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- given prover:
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen--
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- * translation along the comorphism
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen--
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- * all coercions
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen--
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- * the lid is valid for the prover and the translated theory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenprepareForProving :: (Logic lid sublogics1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            basic_spec1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            sentence
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            symb_items1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            symb_map_items1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            sign1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            morphism1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            symbol1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            raw_symbol1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            proof_tree1) =>
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                      ProofState lid sentence
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                  -> (G_prover,AnyComorphism)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                  -> Result G_theory_with_prover
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenprepareForProving st (G_prover lid4 p, Comorphism cid) =
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    case selectedTheory st of
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    G_theory lid1 (ExtSign sign _) _ sens _ ->
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen      do
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        let lidT = targetLogic cid
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        bTh' <- coerceBasicTheory lid1 (sourceLogic cid)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   "Proofs.InferBasic.callProver: basic theory"
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   (sign, toNamedList $ sens)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        (sign'',sens'') <- wrapMapTheory cid bTh'
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        p' <- coerceProver lid4 lidT "" p
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        return $
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen           G_theory_with_prover lidT (Theory sign'' (toThSens sens'')) p'
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- | returns the map of currently selected goals
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenselectedGoalMap :: ProofState lid sentence
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                -> ThSens sentence (AnyComorphism,BasicProof)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenselectedGoalMap st = filterMapWithList (selectedGoals st) (goalMap st)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-- | returns the axioms of the state coerced into the state's logicId
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenaxiomMap ::
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    (Logic  lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                 sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen     Monad m) =>
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen       ProofState lid1 sentence1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    -> m (ThSens sentence1 (AnyComorphism,BasicProof))
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenaxiomMap s =
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    case theory s of
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    G_theory lid1 _ _ aM _ ->
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        coerceThSens lid1 (logicId s) "Proofs.GUIState.axiomMap" aM
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen{- |
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen  recalculation of sublogic upon (de)selection of goals, axioms and
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen  proven theorems
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen-}
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenrecalculateSublogicAndSelectedTheory :: (Logic lid sublogics1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   basic_spec1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   sentence
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   symb_items1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   symb_map_items1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   sign1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   morphism1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   symbol1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   raw_symbol1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   proof_tree1) =>
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen       ProofState lid sentence -> IO (ProofState lid sentence)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowenrecalculateSublogicAndSelectedTheory st =
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen  case theory st of
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    G_theory lid1 sign _ sens _ -> do
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen          -- coerce goalMap
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        ths <- coerceThSens (logicId st) lid1
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            "Proofs.InferBasic.recalculateSublogic: selected goals"
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            (goalMap st)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen          -- partition goalMap
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        let (sel_goals,other_goals) =
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                let selected k _ = Set.member k s
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                    s = Set.fromList (selectedGoals st)
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                in Map.partitionWithKey selected ths
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen            provenThs =
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   Map.filter (\x -> (isProvenSenStatus $ OMap.ele x))
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                   other_goals
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen          -- select goals from goalMap
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen            -- sel_goals = filterMapWithList (selectedGoals st) goals
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen          -- select proven theorems from goalMap
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen            sel_provenThs = OMap.map (\ x -> x{isAxiom = True}) $
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                            filterMapWithList (includedTheorems st) provenThs
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen            sel_sens = filterMapWithList (includedAxioms st) sens
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen            currentThSens = Map.union sel_sens $
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                              Map.union sel_provenThs sel_goals
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen            sTh = G_theory lid1 sign 0 currentThSens 0
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen            sLo = sublogicOfTh sTh
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen        return $ st { sublogicOfTheory = sLo,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                      selectedTheory = sTh,
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen                      proversMap = shrinkKnownProvers sLo (proversMap st) }
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowengetGoals :: LibEnv -> LIB_NAME -> LEdge DGLinkLab
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen         -> Result G_theory
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie BowengetGoals libEnv ln (n,_,edge) = do
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen  th <- computeLocalTheory libEnv ln n
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen  translateG_theory (dgl_morphism edge) th
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowenclass GetPName a where
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    getPName :: a -> String
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Boweninstance GetPName G_prover where
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    getPName (G_prover _ p) = prover_name p
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Boweninstance GetPName G_cons_checker where
5c124de5c36bfc236d55578429df5f048f0d0a07Jamie Bowen    getPName (G_cons_checker _ p) = prover_name p

lookupKnownProver :: (Logic lid sublogics1
                       basic_spec1
                       sentence
                       symb_items1
                       symb_map_items1
                       sign1
                       morphism1
                       symbol1
                       raw_symbol1
                       proof_tree1
                , Monad m) =>
                ProofState lid sentence -> ProverKind
             -> m (G_prover,AnyComorphism)
lookupKnownProver st pk =
    let sl = sublogicOfTheory st
        mt = do -- Monad Maybe
           pr_s <- selectedProver st
           ps <- Map.lookup pr_s (proversMap st)
           cm <- find (lessSublogicComor sl) ps
           return (pr_s,cm)
        matchingPr s (gp,_) = case gp of
                               G_prover _ p -> prover_name p == s
        findProver (pr_n,cm) =
            (case filter (matchingPr pr_n) $ getProvers pk sl [cm] of
               [] -> fail "Proofs.InferBasic: no prover found"
               [p] -> return p
               _ -> fail $ "Proofs.InferBasic: more than one"++
                           " matching prover found")
    in maybe (fail "Proofs.InferBasic: no matching known prover")
             findProver mt

-- | Pairs each target prover of these comorphisms with its comorphism
getProvers :: ProverKind -> G_sublogics
           -> [AnyComorphism] -> [(G_prover, AnyComorphism)]
getProvers pk (G_sublogics lid sl) = foldl addProvers []
    where addProvers acc cm =
              case cm of
              Comorphism cid -> let slid = sourceLogic cid in acc ++
                  foldl (\ l p -> if hasProverKind pk p
                                    && language_name lid == language_name slid
                                    && maybe False
                                     (flip isSubElem $ prover_sublogic p)
                                     (mapSublogic cid
                                     $ forceCoerceSublogic lid slid sl)
                                     then (G_prover (targetLogic cid) p,cm):l
                                     else l)
                        []
                        (provers $ targetLogic cid)

getConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
getConsCheckers = foldl addCCs []
    where addCCs acc cm =
              case cm of
              Comorphism cid -> acc ++
                  map (\p -> (G_cons_checker (targetLogic cid) p,cm))
                      (cons_checkers $ targetLogic cid)

-- | the list of proof statuses is integrated into the goalMap of the state
-- after validation of the Disproved Statuses
markProved :: (Logic lid1 sublogics1
                     basic_spec1 sentence1 symb_items1 symb_map_items1
                     sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
               Logic lid sublogics
                     basic_spec sentence symb_items symb_map_items
                     sign morphism symbol raw_symbol proof_tree) =>
       AnyComorphism -> lid -> [Proof_status proof_tree]
    -> ProofState lid1 sentence1
    -> ProofState lid1 sentence1
markProved c lid status st =
      st { goalMap = markProvedGoalMap c lid
                                       (filterValidProof_status st status)
                                       (goalMap st)}


-- | mark all newly proven goals with their proof tree
markProvedGoalMap :: (Ord a, Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree) =>
       AnyComorphism -> lid -> [Proof_status proof_tree]
    -> ThSens a (AnyComorphism,BasicProof)
    -> ThSens a (AnyComorphism,BasicProof)
markProvedGoalMap c lid status thSens = foldl upd thSens status
    where upd m pStat = OMap.update (updStat pStat) (goalName pStat) m
          updStat ps s = Just $
                s { senAttr = ThmStatus $ (c, BasicProof lid ps) : thmStatus s}

filterValidProof_status :: (Logic lid sublogics1
                                  basic_spec1
                                  sentence
                                  symb_items1
                                  symb_map_items1
                                  sign1
                                  morphism1
                                  symbol1
                                  raw_symbol1
                                  proof_tree1) =>
                           ProofState lid sentence
                        -> [Proof_status proof_tree]
                        -> [Proof_status proof_tree]
filterValidProof_status st =
    case selectedTheory st of
      G_theory _ _ _ sens _ ->
          filter (provedOrDisproved (includedAxioms st == OMap.keys sens))
    where provedOrDisproved allSentencesIncluded senStat =
              isProvedStat senStat ||
             (allSentencesIncluded && case goalStatus senStat of
                                      Disproved -> True
                                      _ -> False)