{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable, StandaloneDeriving #-}
{- |
Module      :  ./Proofs/AbstractState.hs
Description :  State data structure used by the goal management GUI.
Copyright   :  (c) Uni Bremen 2005-2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

The 'ProofState' data structure abstracts the GUI implementation details
away by allowing callback function to use it as the sole input and output.
It is also used by the CMDL interface.
-}

module Proofs.AbstractState
    ( ProverOrConsChecker (..)
    , G_prover (..)
    , G_proof_tree (..)
    , getProverName
    , getCcName
    , getCcBatch
    , coerceProver
    , G_cons_checker (..)
    , coerceConsChecker
    , ProofActions (..)
    , ProofState (..)
    , sublogicOfTheory
    , logicId
    , initialState
    , resetSelection
    , toAxioms
    , getAxioms
    , getGoals
    , recalculateSublogicAndSelectedTheory
    , markProved
    , G_theory_with_prover (..)
    , G_theory_with_cons_checker (..)
    , prepareForProving
    , prepareForConsChecking
    , isSubElemG
    , pathToComorphism
    , getAllProvers
    , getUsableProvers
    , getConsCheckers
    , getListOfConsCheckers
    , getAllConsCheckers
    , lookupKnownProver
    , lookupKnownConsChecker
    , autoProofAtNode
    , usableCC
    ) where

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Data.Typeable

import Control.Concurrent.MVar
import Control.Monad.Trans
import Control.Monad
import qualified Control.Monad.Fail as Fail

import qualified Common.OrderedMap as OMap
import Common.Result as Result
import Common.ResultT
import Common.AS_Annotation
import Common.ExtSign
import Common.Utils
import Common.GraphAlgo (yen)

import Unsafe.Coerce (unsafeCoerce)

import Logic.Logic
import Logic.Prover
import Logic.Grothendieck
import Logic.Comorphism
import Logic.Coerce

import Comorphisms.KnownProvers
import Comorphisms.LogicGraph (logicGraph)

import Static.GTheory

-- import Interfaces.DataTypes (IntState)

-- * Provers

data ProverOrConsChecker = Prover G_prover
                         | ConsChecker G_cons_checker
                         deriving (Int -> ProverOrConsChecker -> ShowS
[ProverOrConsChecker] -> ShowS
ProverOrConsChecker -> String
(Int -> ProverOrConsChecker -> ShowS)
-> (ProverOrConsChecker -> String)
-> ([ProverOrConsChecker] -> ShowS)
-> Show ProverOrConsChecker
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProverOrConsChecker] -> ShowS
$cshowList :: [ProverOrConsChecker] -> ShowS
show :: ProverOrConsChecker -> String
$cshow :: ProverOrConsChecker -> String
showsPrec :: Int -> ProverOrConsChecker -> ShowS
$cshowsPrec :: Int -> ProverOrConsChecker -> ShowS
Show)

-- | provers and consistency checkers for specific logics
data G_prover =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => G_prover lid (Prover sign sentence morphism sublogics proof_tree)
  deriving Typeable

instance Show G_prover where
  show :: G_prover -> String
show = G_prover -> String
getProverName

getProverName :: G_prover -> String
getProverName :: G_prover -> String
getProverName (G_prover _ p :: Prover sign sentence morphism sublogics proof_tree
p) = Prover sign sentence morphism sublogics proof_tree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover sign sentence morphism sublogics proof_tree
p

usable :: G_prover -> IO Bool
usable :: G_prover -> IO Bool
usable (G_prover _ p :: Prover sign sentence morphism sublogics proof_tree
p) = (Maybe String -> Bool) -> IO (Maybe String) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (IO (Maybe String) -> IO Bool) -> IO (Maybe String) -> IO Bool
forall a b. (a -> b) -> a -> b
$ Prover sign sentence morphism sublogics proof_tree
-> IO (Maybe String)
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> IO (Maybe String)
proverUsable Prover sign sentence morphism sublogics proof_tree
p

coerceProver ::
  ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
  , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
  , Fail.MonadFail m )
  => lid1 -> lid2 -> String
  -> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1
  -> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
coerceProver :: lid1
-> lid2
-> String
-> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1
-> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
coerceProver = lid1
-> lid2
-> String
-> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1
-> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce

data G_cons_checker =
  forall lid sublogics basic_spec sentence symb_items
    symb_map_items sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items
      symb_map_items sign morphism symbol raw_symbol proof_tree
  => G_cons_checker lid
       (ConsChecker sign sentence sublogics morphism proof_tree)
  deriving (Typeable)

instance Eq G_cons_checker where
  G_cons_checker _ cc1 :: ConsChecker sign sentence sublogics morphism proof_tree
cc1 == :: G_cons_checker -> G_cons_checker -> Bool
== G_cons_checker _ cc2 :: ConsChecker sign sentence sublogics morphism proof_tree
cc2 = ConsChecker sign sentence sublogics morphism proof_tree -> String
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName ConsChecker sign sentence sublogics morphism proof_tree
cc1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== ConsChecker sign sentence sublogics morphism proof_tree -> String
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName ConsChecker sign sentence sublogics morphism proof_tree
cc2

instance Show G_cons_checker where
 show :: G_cons_checker -> String
show _ = "G_cons_checker "

getCcName :: G_cons_checker -> String
getCcName :: G_cons_checker -> String
getCcName (G_cons_checker _ p :: ConsChecker sign sentence sublogics morphism proof_tree
p) = ConsChecker sign sentence sublogics morphism proof_tree -> String
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName ConsChecker sign sentence sublogics morphism proof_tree
p

getCcBatch :: G_cons_checker -> Bool
getCcBatch :: G_cons_checker -> Bool
getCcBatch (G_cons_checker _ p :: ConsChecker sign sentence sublogics morphism proof_tree
p) = ConsChecker sign sentence sublogics morphism proof_tree -> Bool
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> Bool
ccBatch ConsChecker sign sentence sublogics morphism proof_tree
p

usableCC :: G_cons_checker -> IO Bool
usableCC :: G_cons_checker -> IO Bool
usableCC (G_cons_checker _ p :: ConsChecker sign sentence sublogics morphism proof_tree
p) = (Maybe String -> Bool) -> IO (Maybe String) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (IO (Maybe String) -> IO Bool) -> IO (Maybe String) -> IO Bool
forall a b. (a -> b) -> a -> b
$ ConsChecker sign sentence sublogics morphism proof_tree
-> IO (Maybe String)
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree
-> IO (Maybe String)
ccUsable ConsChecker sign sentence sublogics morphism proof_tree
p

coerceConsChecker ::
  ( Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1
  , Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2
  , Fail.MonadFail m )
  => lid1 -> lid2 -> String
  -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
  -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
coerceConsChecker :: lid1
-> lid2
-> String
-> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
-> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
coerceConsChecker = lid1
-> lid2
-> String
-> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
-> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce


-- | provers and consistency checkers for specific logics
data G_proof_tree =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => G_proof_tree lid proof_tree
  deriving Typeable
instance Show G_proof_tree where
  show :: G_proof_tree -> String
show (G_proof_tree _ pt :: proof_tree
pt) = proof_tree -> String
forall a. Show a => a -> String
show proof_tree
pt

-- | Possible actions for GUI which are manipulating ProofState
data ProofActions = ProofActions {
    -- | called whenever the "Prove" button is clicked
    ProofActions -> ProofState -> IO (Result ProofState)
proveF :: ProofState
      -> IO (Result.Result ProofState),
    -- | called whenever the "More fine grained selection" button is clicked
    ProofActions -> ProofState -> IO (Result ProofState)
fineGrainedSelectionF :: ProofState
      -> IO (Result.Result ProofState),
    -- | called whenever a (de-)selection occured for updating sublogic
    ProofActions -> ProofState -> IO ProofState
recalculateSublogicF :: ProofState
      -> IO ProofState
  }

{- |
  Represents the global state of the prover GUI.
-}
data ProofState =
     ProofState
      { -- | theory name
        ProofState -> String
theoryName :: String,
        -- | Grothendieck theory
        ProofState -> G_theory
currentTheory :: G_theory,
        -- | currently known provers
        ProofState -> KnownProversMap
proversMap :: KnownProversMap,
        -- | currently selected goals
        ProofState -> [String]
selectedGoals :: [String],
        -- | axioms to include for the proof
        ProofState -> [String]
includedAxioms :: [String],
        -- | theorems to include for the proof
        ProofState -> [String]
includedTheorems :: [String],
        -- | whether a prover is running or not
        ProofState -> Bool
proverRunning :: Bool,
        -- | accumulated Diagnosis during Proofs
        ProofState -> [Diagnosis]
accDiags :: [Diagnosis],
        -- | comorphisms fitting with sublogic of this G_theory
        ProofState -> [(G_prover, AnyComorphism)]
comorphismsToProvers :: [(G_prover, AnyComorphism)],
        -- | which prover (if any) is currently selected
        ProofState -> Maybe String
selectedProver :: Maybe String,
        -- | which consistency checker (if any) is currently selected
        ProofState -> Maybe String
selectedConsChecker :: Maybe String,
        -- | theory based on selected goals, axioms and proven theorems
        ProofState -> G_theory
selectedTheory :: G_theory
      } deriving Int -> ProofState -> ShowS
[ProofState] -> ShowS
ProofState -> String
(Int -> ProofState -> ShowS)
-> (ProofState -> String)
-> ([ProofState] -> ShowS)
-> Show ProofState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProofState] -> ShowS
$cshowList :: [ProofState] -> ShowS
show :: ProofState -> String
$cshow :: ProofState -> String
showsPrec :: Int -> ProofState -> ShowS
$cshowsPrec :: Int -> ProofState -> ShowS
Show

resetSelection :: ProofState -> ProofState
resetSelection :: ProofState -> ProofState
resetSelection s :: ProofState
s = case ProofState -> G_theory
currentTheory ProofState
s of
  G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ ->
    let (aMap :: ThSens sentence (AnyComorphism, BasicProof)
aMap, gMap :: ThSens sentence (AnyComorphism, BasicProof)
gMap) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> (ThSens sentence (AnyComorphism, BasicProof),
    ThSens sentence (AnyComorphism, BasicProof))
forall k a.
Ord k =>
(a -> Bool) -> OMap k a -> (OMap k a, OMap k a)
OMap.partition SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
sens
        gs :: [String]
gs = ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall k a. Map k a -> [k]
Map.keys ThSens sentence (AnyComorphism, BasicProof)
gMap
    in ProofState
s
    { selectedGoals :: [String]
selectedGoals = ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall k a. Map k a -> [k]
Map.keys ThSens sentence (AnyComorphism, BasicProof)
gMap
    , includedAxioms :: [String]
includedAxioms = ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall k a. Map k a -> [k]
Map.keys ThSens sentence (AnyComorphism, BasicProof)
aMap
    , includedTheorems :: [String]
includedTheorems = [String]
gs }

toAxioms :: ProofState -> [String]
toAxioms :: ProofState -> [String]
toAxioms = ((String, Bool) -> String) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (k :: String
k, wTh :: Bool
wTh) -> if Bool
wTh then "(Th) " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
k else String
k)
  ([(String, Bool)] -> [String])
-> (ProofState -> [(String, Bool)]) -> ProofState -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofState -> [(String, Bool)]
getAxioms

getAxioms :: ProofState -> [(String, Bool)]
getAxioms :: ProofState -> [(String, Bool)]
getAxioms = G_theory -> [(String, Bool)]
getThAxioms (G_theory -> [(String, Bool)])
-> (ProofState -> G_theory) -> ProofState -> [(String, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofState -> G_theory
currentTheory

getGoals :: ProofState -> [(String, Maybe BasicProof)]
getGoals :: ProofState -> [(String, Maybe BasicProof)]
getGoals = G_theory -> [(String, Maybe BasicProof)]
getThGoals (G_theory -> [(String, Maybe BasicProof)])
-> (ProofState -> G_theory)
-> ProofState
-> [(String, Maybe BasicProof)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofState -> G_theory
currentTheory

{- |
  Creates an initial State.
-}
initialState :: String
    -> G_theory
    -> KnownProversMap
    -> ProofState
initialState :: String -> G_theory -> KnownProversMap -> ProofState
initialState thN :: String
thN th :: G_theory
th pm :: KnownProversMap
pm = 
    case G_theory
th of 
     G_theory lid :: lid
lid _ _ _ _ _ -> ProofState -> ProofState
resetSelection
       ProofState :: String
-> G_theory
-> KnownProversMap
-> [String]
-> [String]
-> [String]
-> Bool
-> [Diagnosis]
-> [(G_prover, AnyComorphism)]
-> Maybe String
-> Maybe String
-> G_theory
-> ProofState
ProofState
         { theoryName :: String
theoryName = String
thN
         , currentTheory :: G_theory
currentTheory = G_theory
th
         , proversMap :: KnownProversMap
proversMap = KnownProversMap
pm
         , selectedGoals :: [String]
selectedGoals = []
         , includedAxioms :: [String]
includedAxioms = []
         , includedTheorems :: [String]
includedTheorems = []
         , proverRunning :: Bool
proverRunning = Bool
False
         , accDiags :: [Diagnosis]
accDiags = []
         , comorphismsToProvers :: [(G_prover, AnyComorphism)]
comorphismsToProvers = []
         , selectedProver :: Maybe String
selectedProver =
             let prvs :: [String]
prvs = KnownProversMap -> [String]
forall k a. Map k a -> [k]
Map.keys KnownProversMap
pm
             in if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
prvs
                then Maybe String
forall a. Maybe a
Nothing
                else 
                 let lidProver :: String
lidProver = lid -> String
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String
default_prover lid
lid
                 in if String
lidProver String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
prvs 
                    then String -> Maybe String
forall a. a -> Maybe a
Just String
lidProver
                    else 
                     if String
defaultGUIProver String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
prvs
                     then String -> Maybe String
forall a. a -> Maybe a
Just String
defaultGUIProver
                     else Maybe String
forall a. Maybe a
Nothing
         , selectedConsChecker :: Maybe String
selectedConsChecker = Maybe String
forall a. Maybe a
Nothing
         , selectedTheory :: G_theory
selectedTheory = G_theory
th }

logicId :: ProofState -> String
logicId :: ProofState -> String
logicId s :: ProofState
s = case ProofState -> G_theory
currentTheory ProofState
s of
  G_theory lid :: lid
lid _ _ _ _ _ -> lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid

sublogicOfTheory :: ProofState -> G_sublogics
sublogicOfTheory :: ProofState -> G_sublogics
sublogicOfTheory = G_theory -> G_sublogics
sublogicOfTh (G_theory -> G_sublogics)
-> (ProofState -> G_theory) -> ProofState -> G_sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofState -> G_theory
selectedTheory

data G_theory_with_cons_checker =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => G_theory_with_cons_checker lid
       (TheoryMorphism sign sentence morphism proof_tree)
       (ConsChecker sign sentence sublogics morphism proof_tree)

-- | a Grothendieck pair of prover and theory which are in the same logic
data G_theory_with_prover =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => G_theory_with_prover lid
       (Theory sign sentence proof_tree)
       (Prover sign sentence morphism sublogics proof_tree)

data GPlainTheory =
  forall lid sublogics basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
  . Logic lid sublogics basic_spec sentence symb_items symb_map_items
      sign morphism symbol raw_symbol proof_tree
  => GPlainTheory lid (Theory sign sentence proof_tree)

prepareForConsChecking :: ProofState
    -> (G_cons_checker, AnyComorphism)
    -> Result G_theory_with_cons_checker
prepareForConsChecking :: ProofState
-> (G_cons_checker, AnyComorphism)
-> Result G_theory_with_cons_checker
prepareForConsChecking st :: ProofState
st (G_cons_checker lid4 :: lid
lid4 p :: ConsChecker sign sentence sublogics morphism proof_tree
p, co :: AnyComorphism
co) = do
  GPlainTheory lidT :: lid
lidT th :: Theory sign sentence proof_tree
th@(Theory sign'' :: sign
sign'' _) <- ProofState -> AnyComorphism -> Result GPlainTheory
prepareTheory ProofState
st AnyComorphism
co
  morphism
incl <- lid -> sign -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result morphism
subsig_inclusion lid
lidT (lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lidT) sign
sign''
  let mor :: TheoryMorphism sign sentence morphism proof_tree
mor = TheoryMorphism :: forall sign sen mor proof_tree.
Theory sign sen proof_tree
-> Theory sign sen proof_tree
-> mor
-> TheoryMorphism sign sen mor proof_tree
TheoryMorphism
                    { tSource :: Theory sign sentence proof_tree
tSource = lid -> Theory sign sentence proof_tree
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol proof_tree.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Theory sign sentence proof_tree
emptyTheory lid
lidT
                    , tTarget :: Theory sign sentence proof_tree
tTarget = Theory sign sentence proof_tree
th
                    , tMorphism :: morphism
tMorphism = morphism
incl }
  ConsChecker sign sentence sublogics morphism proof_tree
p' <- lid
-> lid
-> String
-> ConsChecker sign sentence sublogics morphism proof_tree
-> Result (ConsChecker sign sentence sublogics morphism proof_tree)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
-> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
coerceConsChecker lid
lid4 lid
lidT "" ConsChecker sign sentence sublogics morphism proof_tree
p
  G_theory_with_cons_checker -> Result G_theory_with_cons_checker
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory_with_cons_checker -> Result G_theory_with_cons_checker)
-> G_theory_with_cons_checker -> Result G_theory_with_cons_checker
forall a b. (a -> b) -> a -> b
$ lid
-> TheoryMorphism sign sentence morphism proof_tree
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_theory_with_cons_checker
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> TheoryMorphism sign sentence morphism proof_tree
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_theory_with_cons_checker
G_theory_with_cons_checker lid
lidT TheoryMorphism sign sentence morphism proof_tree
mor ConsChecker sign sentence sublogics morphism proof_tree
p'


prepareTheory :: ProofState -> AnyComorphism -> Result GPlainTheory
prepareTheory :: ProofState -> AnyComorphism -> Result GPlainTheory
prepareTheory st :: ProofState
st (Comorphism cid :: cid
cid) = case ProofState -> G_theory
selectedTheory ProofState
st of
    G_theory lid :: lid
lid _ (ExtSign sign :: sign
sign _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> do
        (sign1, [Named sentence1])
bTh' <- lid
-> lid1
-> String
-> (sign, [Named sentence])
-> Result (sign1, [Named sentence1])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid)
                   "Proofs.AbstractState.prepareTheory: basic theory"
                   (sign
sign, ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens)
        (sign'' :: sign2
sign'', sens'' :: [Named sentence2]
sens'') <- cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory cid
cid (sign1, [Named sentence1])
bTh'
        GPlainTheory -> Result GPlainTheory
forall (m :: * -> *) a. Monad m => a -> m a
return (GPlainTheory -> Result GPlainTheory)
-> (ThSens sentence2 (ProofStatus proof_tree2) -> GPlainTheory)
-> ThSens sentence2 (ProofStatus proof_tree2)
-> Result GPlainTheory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid2 -> Theory sign2 sentence2 proof_tree2 -> GPlainTheory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Theory sign sentence proof_tree -> GPlainTheory
GPlainTheory (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) (Theory sign2 sentence2 proof_tree2 -> GPlainTheory)
-> (ThSens sentence2 (ProofStatus proof_tree2)
    -> Theory sign2 sentence2 proof_tree2)
-> ThSens sentence2 (ProofStatus proof_tree2)
-> GPlainTheory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sign2
-> ThSens sentence2 (ProofStatus proof_tree2)
-> Theory sign2 sentence2 proof_tree2
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
Theory sign2
sign''
          (ThSens sentence2 (ProofStatus proof_tree2) -> Result GPlainTheory)
-> ThSens sentence2 (ProofStatus proof_tree2)
-> Result GPlainTheory
forall a b. (a -> b) -> a -> b
$ [Named sentence2] -> ThSens sentence2 (ProofStatus proof_tree2)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence2]
sens''

{- | prepare the selected theory of the state for proving with the
given prover:

 * translation along the comorphism

 * all coercions

 * the lid is valid for the prover and the translated theory
-}
prepareForProving :: ProofState
    -> (G_prover, AnyComorphism)
    -> Result G_theory_with_prover
prepareForProving :: ProofState
-> (G_prover, AnyComorphism) -> Result G_theory_with_prover
prepareForProving st :: ProofState
st (G_prover lid4 :: lid
lid4 p :: Prover sign sentence morphism sublogics proof_tree
p, co :: AnyComorphism
co) = do
  GPlainTheory lidT :: lid
lidT th :: Theory sign sentence proof_tree
th <- ProofState -> AnyComorphism -> Result GPlainTheory
prepareTheory ProofState
st AnyComorphism
co
  Prover sign sentence morphism sublogics proof_tree
p' <- lid
-> lid
-> String
-> Prover sign sentence morphism sublogics proof_tree
-> Result (Prover sign sentence morphism sublogics proof_tree)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> Prover sign1 sentence1 morphism1 sublogics1 proof_tree1
-> m (Prover sign2 sentence2 morphism2 sublogics2 proof_tree2)
coerceProver lid
lid4 lid
lidT "" Prover sign sentence morphism sublogics proof_tree
p
  G_theory_with_prover -> Result G_theory_with_prover
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory_with_prover -> Result G_theory_with_prover)
-> G_theory_with_prover -> Result G_theory_with_prover
forall a b. (a -> b) -> a -> b
$ lid
-> Theory sign sentence proof_tree
-> Prover sign sentence morphism sublogics proof_tree
-> G_theory_with_prover
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Theory sign sentence proof_tree
-> Prover sign sentence morphism sublogics proof_tree
-> G_theory_with_prover
G_theory_with_prover lid
lidT Theory sign sentence proof_tree
th Prover sign sentence morphism sublogics proof_tree
p'

-- | creates the currently selected theory
makeSelectedTheory :: ProofState -> G_theory
makeSelectedTheory :: ProofState -> G_theory
makeSelectedTheory s :: ProofState
s = case ProofState -> G_theory
currentTheory ProofState
s of
  G_theory lid :: lid
lid syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig si :: SigId
si sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ ->
    -- axiom map, goal map
    let (aMap :: ThSens sentence (AnyComorphism, BasicProof)
aMap, gMap :: ThSens sentence (AnyComorphism, BasicProof)
gMap) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> (ThSens sentence (AnyComorphism, BasicProof),
    ThSens sentence (AnyComorphism, BasicProof))
forall k a.
Ord k =>
(a -> Bool) -> OMap k a -> (OMap k a, OMap k a)
OMap.partition SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
sens
        -- proven goals map
        pMap :: ThSens sentence (AnyComorphism, BasicProof)
pMap = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus ThSens sentence (AnyComorphism, BasicProof)
gMap
    in
    lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
syn ExtSign sign symbol
sig SigId
si
      ([ThSens sentence (AnyComorphism, BasicProof)]
-> ThSens sentence (AnyComorphism, BasicProof)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions
        [ [String]
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k e. Ord k => [k] -> Map k e -> Map k e
filterMapWithList (ProofState -> [String]
selectedGoals ProofState
s) ThSens sentence (AnyComorphism, BasicProof)
gMap
        , [String]
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k e. Ord k => [k] -> Map k e -> Map k e
filterMapWithList (ProofState -> [String]
includedAxioms ProofState
s) ThSens sentence (AnyComorphism, BasicProof)
aMap
        , Bool
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => Bool -> ThSens a b -> ThSens a b
markAsAxiom Bool
True (ThSens sentence (AnyComorphism, BasicProof)
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ [String]
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k e. Ord k => [k] -> Map k e -> Map k e
filterMapWithList (ProofState -> [String]
includedTheorems ProofState
s) ThSens sentence (AnyComorphism, BasicProof)
pMap
        ]) ThId
startThId

{- |
  recalculation of sublogic upon (de)selection of goals, axioms and
  proven theorems
-}
recalculateSublogicAndSelectedTheory :: ProofState -> ProofState
recalculateSublogicAndSelectedTheory :: ProofState -> ProofState
recalculateSublogicAndSelectedTheory st :: ProofState
st = let
  sTh :: G_theory
sTh = ProofState -> G_theory
makeSelectedTheory ProofState
st
  sLo :: G_sublogics
sLo = G_theory -> G_sublogics
sublogicOfTh G_theory
sTh
  in ProofState
st
    { selectedTheory :: G_theory
selectedTheory = G_theory
sTh
    , proversMap :: KnownProversMap
proversMap = G_sublogics -> KnownProversMap -> KnownProversMap
shrinkKnownProvers G_sublogics
sLo (KnownProversMap -> KnownProversMap)
-> KnownProversMap -> KnownProversMap
forall a b. (a -> b) -> a -> b
$ ProofState -> KnownProversMap
proversMap ProofState
st }

getConsCheckers :: [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
getConsCheckers :: [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
getConsCheckers = ((G_cons_checker, AnyComorphism) -> IO Bool)
-> [(G_cons_checker, AnyComorphism)]
-> IO [(G_cons_checker, AnyComorphism)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (G_cons_checker -> IO Bool
usableCC (G_cons_checker -> IO Bool)
-> ((G_cons_checker, AnyComorphism) -> G_cons_checker)
-> (G_cons_checker, AnyComorphism)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_cons_checker, AnyComorphism) -> G_cons_checker
forall a b. (a, b) -> a
fst) ([(G_cons_checker, AnyComorphism)]
 -> IO [(G_cons_checker, AnyComorphism)])
-> ([AnyComorphism] -> [(G_cons_checker, AnyComorphism)])
-> [AnyComorphism]
-> IO [(G_cons_checker, AnyComorphism)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
getAllConsCheckers

getAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
getAllConsCheckers :: [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
getAllConsCheckers lst :: [AnyComorphism]
lst =
  (Set String, [(G_cons_checker, AnyComorphism)])
-> [(G_cons_checker, AnyComorphism)]
forall a b. (a, b) -> b
snd ((Set String, [(G_cons_checker, AnyComorphism)])
 -> [(G_cons_checker, AnyComorphism)])
-> (Set String, [(G_cons_checker, AnyComorphism)])
-> [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$
    ((G_cons_checker, AnyComorphism)
 -> (Set String, [(G_cons_checker, AnyComorphism)])
 -> (Set String, [(G_cons_checker, AnyComorphism)]))
-> (Set String, [(G_cons_checker, AnyComorphism)])
-> [(G_cons_checker, AnyComorphism)]
-> (Set String, [(G_cons_checker, AnyComorphism)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
      ( \el :: (G_cons_checker, AnyComorphism)
el@(G_cons_checker _ cc :: ConsChecker sign sentence sublogics morphism proof_tree
cc, _) (s, l) ->
          if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (ConsChecker sign sentence sublogics morphism proof_tree -> String
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName ConsChecker sign sentence sublogics morphism proof_tree
cc) Set String
s
            then (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (ConsChecker sign sentence sublogics morphism proof_tree -> String
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName ConsChecker sign sentence sublogics morphism proof_tree
cc) Set String
s, (G_cons_checker, AnyComorphism)
el (G_cons_checker, AnyComorphism)
-> [(G_cons_checker, AnyComorphism)]
-> [(G_cons_checker, AnyComorphism)]
forall a. a -> [a] -> [a]
: [(G_cons_checker, AnyComorphism)]
l)
            else (Set String
s, [(G_cons_checker, AnyComorphism)]
l)
      )
      (Set String
forall a. Set a
Set.empty, [])
      ([(G_cons_checker, AnyComorphism)]
 -> (Set String, [(G_cons_checker, AnyComorphism)]))
-> [(G_cons_checker, AnyComorphism)]
-> (Set String, [(G_cons_checker, AnyComorphism)])
forall a b. (a -> b) -> a -> b
$
      (AnyComorphism -> [(G_cons_checker, AnyComorphism)])
-> [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
        ( \cm :: AnyComorphism
cm@(Comorphism cid :: cid
cid) ->
            (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2
 -> (G_cons_checker, AnyComorphism))
-> [ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2]
-> [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> [a] -> [b]
map
              ( \cc :: ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2
cc ->
                  (lid2
-> ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2
-> G_cons_checker
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_cons_checker
G_cons_checker (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2
cc, AnyComorphism
cm)
              )
              ([ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2]
 -> [(G_cons_checker, AnyComorphism)])
-> [ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2]
-> [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ lid2
-> [ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
cons_checkers (lid2
 -> [ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2])
-> lid2
-> [ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2]
forall a b. (a -> b) -> a -> b
$ cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid
        )
        ([AnyComorphism] -> [(G_cons_checker, AnyComorphism)])
-> [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ [AnyComorphism]
lst

getListOfConsCheckers :: [G_cons_checker]
getListOfConsCheckers :: [G_cons_checker]
getListOfConsCheckers = (AnyLogic -> [G_cons_checker])
-> Map String AnyLogic -> [G_cons_checker]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Logic lid :: lid
lid) -> (ConsChecker sign sentence sublogics morphism proof_tree
 -> G_cons_checker)
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> [G_cons_checker]
forall a b. (a -> b) -> [a] -> [b]
map (\cc :: ConsChecker sign sentence sublogics morphism proof_tree
cc -> lid
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_cons_checker
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_cons_checker
G_cons_checker lid
lid ConsChecker sign sentence sublogics morphism proof_tree
cc) ([ConsChecker sign sentence sublogics morphism proof_tree]
 -> [G_cons_checker])
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> [G_cons_checker]
forall a b. (a -> b) -> a -> b
$ lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
cons_checkers lid
lid) (LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph)

lookupKnownConsChecker :: Fail.MonadFail m => ProofState
    -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker :: ProofState -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker st :: ProofState
st =
       let sl :: G_sublogics
sl = G_theory -> G_sublogics
sublogicOfTh (ProofState -> G_theory
selectedTheory ProofState
st)
           mt :: Maybe (String, [AnyComorphism])
mt = do
                 String
pr_s <- ProofState -> Maybe String
selectedConsChecker ProofState
st
                 [AnyComorphism]
ps <- String -> KnownProversMap -> Maybe [AnyComorphism]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
pr_s (ProofState -> KnownProversMap
proversMap ProofState
st)
                 (String, [AnyComorphism]) -> Maybe (String, [AnyComorphism])
forall (m :: * -> *) a. Monad m => a -> m a
return (String
pr_s, [AnyComorphism]
ps)
           matchingCC :: String -> (G_cons_checker, b) -> Bool
matchingCC s :: String
s (gp :: G_cons_checker
gp, _) = case G_cons_checker
gp of
                                  G_cons_checker _ p :: ConsChecker sign sentence sublogics morphism proof_tree
p -> ConsChecker sign sentence sublogics morphism proof_tree -> String
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree -> String
ccName ConsChecker sign sentence sublogics morphism proof_tree
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s
           findCC :: (String, [AnyComorphism]) -> m (G_cons_checker, AnyComorphism)
findCC (pr_n :: String
pr_n, cms :: [AnyComorphism]
cms) =
               case ((G_cons_checker, AnyComorphism) -> Bool)
-> [(G_cons_checker, AnyComorphism)]
-> [(G_cons_checker, AnyComorphism)]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> (G_cons_checker, AnyComorphism) -> Bool
forall b. String -> (G_cons_checker, b) -> Bool
matchingCC String
pr_n) ([(G_cons_checker, AnyComorphism)]
 -> [(G_cons_checker, AnyComorphism)])
-> [(G_cons_checker, AnyComorphism)]
-> [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
getAllConsCheckers
                    ([AnyComorphism] -> [(G_cons_checker, AnyComorphism)])
-> [AnyComorphism] -> [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> Bool) -> [AnyComorphism] -> [AnyComorphism]
forall a. (a -> Bool) -> [a] -> [a]
filter (G_sublogics -> AnyComorphism -> Bool
lessSublogicComor G_sublogics
sl) [AnyComorphism]
cms of
                 [] -> String -> m (G_cons_checker, AnyComorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("CMDL.ProverConsistency.lookupKnownConsChecker" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                 ": no consistency checker found")
                 p :: (G_cons_checker, AnyComorphism)
p : _ -> (G_cons_checker, AnyComorphism)
-> m (G_cons_checker, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_cons_checker, AnyComorphism)
p
       in m (G_cons_checker, AnyComorphism)
-> ((String, [AnyComorphism]) -> m (G_cons_checker, AnyComorphism))
-> Maybe (String, [AnyComorphism])
-> m (G_cons_checker, AnyComorphism)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ( String -> m (G_cons_checker, AnyComorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("CMDL.ProverConsistency.lookupKnownConsChecker: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      "no matching known prover")) (String, [AnyComorphism]) -> m (G_cons_checker, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
(String, [AnyComorphism]) -> m (G_cons_checker, AnyComorphism)
findCC Maybe (String, [AnyComorphism])
mt


lookupKnownProver :: Fail.MonadFail m => ProofState -> ProverKind
    -> m (G_prover, AnyComorphism)
lookupKnownProver :: ProofState -> ProverKind -> m (G_prover, AnyComorphism)
lookupKnownProver st :: ProofState
st pk :: ProverKind
pk =
    let sl :: G_sublogics
sl = G_theory -> G_sublogics
sublogicOfTh (ProofState -> G_theory
selectedTheory ProofState
st)
        mt :: Maybe (String, [AnyComorphism])
mt = do -- Monad Maybe
           String
pr_s <- ProofState -> Maybe String
selectedProver ProofState
st
           [AnyComorphism]
ps <- String -> KnownProversMap -> Maybe [AnyComorphism]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
pr_s (ProofState -> KnownProversMap
proversMap ProofState
st)
           (String, [AnyComorphism]) -> Maybe (String, [AnyComorphism])
forall (m :: * -> *) a. Monad m => a -> m a
return (String
pr_s, [AnyComorphism]
ps)
        matchingPr :: String -> (G_prover, b) -> Bool
matchingPr s :: String
s (gp :: G_prover
gp, _) = case G_prover
gp of
          G_prover _ p :: Prover sign sentence morphism sublogics proof_tree
p -> Prover sign sentence morphism sublogics proof_tree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover sign sentence morphism sublogics proof_tree
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
s
        findProver :: (String, [AnyComorphism]) -> m (G_prover, AnyComorphism)
findProver (pr_n :: String
pr_n, cms :: [AnyComorphism]
cms) =
            case ((G_prover, AnyComorphism) -> Bool)
-> [(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> (G_prover, AnyComorphism) -> Bool
forall b. String -> (G_prover, b) -> Bool
matchingPr String
pr_n) ([(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)])
-> [(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ ProverKind
-> G_sublogics -> [AnyComorphism] -> [(G_prover, AnyComorphism)]
getProvers ProverKind
pk G_sublogics
sl
                 ([AnyComorphism] -> [(G_prover, AnyComorphism)])
-> [AnyComorphism] -> [(G_prover, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> Bool) -> [AnyComorphism] -> [AnyComorphism]
forall a. (a -> Bool) -> [a] -> [a]
filter (G_sublogics -> AnyComorphism -> Bool
lessSublogicComor G_sublogics
sl) [AnyComorphism]
cms of
               [] -> String -> m (G_prover, AnyComorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Proofs.InferBasic: no prover found"
               p :: (G_prover, AnyComorphism)
p : _ -> (G_prover, AnyComorphism) -> m (G_prover, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_prover, AnyComorphism)
p
    in m (G_prover, AnyComorphism)
-> ((String, [AnyComorphism]) -> m (G_prover, AnyComorphism))
-> Maybe (String, [AnyComorphism])
-> m (G_prover, AnyComorphism)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> m (G_prover, AnyComorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Proofs.InferBasic: no matching known prover")
             (String, [AnyComorphism]) -> m (G_prover, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
(String, [AnyComorphism]) -> m (G_prover, AnyComorphism)
findProver Maybe (String, [AnyComorphism])
mt

-- | Pairs each target prover of these comorphisms with its comorphism
getProvers :: ProverKind -> G_sublogics -> [AnyComorphism]
  -> [(G_prover, AnyComorphism)]
getProvers :: ProverKind
-> G_sublogics -> [AnyComorphism] -> [(G_prover, AnyComorphism)]
getProvers pk :: ProverKind
pk (G_sublogics lid :: lid
lid sl :: sublogics
sl) =
  ([(G_prover, AnyComorphism)]
 -> AnyComorphism -> [(G_prover, AnyComorphism)])
-> [(G_prover, AnyComorphism)]
-> [AnyComorphism]
-> [(G_prover, AnyComorphism)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [(G_prover, AnyComorphism)]
-> AnyComorphism -> [(G_prover, AnyComorphism)]
addProvers [] where
  addProvers :: [(G_prover, AnyComorphism)]
-> AnyComorphism -> [(G_prover, AnyComorphism)]
addProvers acc :: [(G_prover, AnyComorphism)]
acc cm :: AnyComorphism
cm = case AnyComorphism
cm of
    Comorphism cid :: cid
cid -> let
      slid :: lid1
slid = cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid
      tlid :: lid2
tlid = cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid
      in [(G_prover, AnyComorphism)]
acc [(G_prover, AnyComorphism)]
-> [(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)]
forall a. [a] -> [a] -> [a]
++ ([(G_prover, AnyComorphism)]
 -> ProverTemplate
      (Theory sign2 sentence2 proof_tree2)
      sentence2
      morphism2
      sublogics2
      proof_tree2
 -> [(G_prover, AnyComorphism)])
-> [(G_prover, AnyComorphism)]
-> [ProverTemplate
      (Theory sign2 sentence2 proof_tree2)
      sentence2
      morphism2
      sublogics2
      proof_tree2]
-> [(G_prover, AnyComorphism)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
             (\ l :: [(G_prover, AnyComorphism)]
l p :: ProverTemplate
  (Theory sign2 sentence2 proof_tree2)
  sentence2
  morphism2
  sublogics2
  proof_tree2
p ->
                  if ProverKind
-> ProverTemplate
     (Theory sign2 sentence2 proof_tree2)
     sentence2
     morphism2
     sublogics2
     proof_tree2
-> Bool
forall x s m y z. ProverKind -> ProverTemplate x s m y z -> Bool
hasProverKind ProverKind
pk ProverTemplate
  (Theory sign2 sentence2 proof_tree2)
  sentence2
  morphism2
  sublogics2
  proof_tree2
p
                    Bool -> Bool -> Bool
&& lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== lid1 -> String
forall lid. Language lid => lid -> String
language_name lid1
slid
                         Bool -> Bool -> Bool
&& Bool -> (sublogics2 -> Bool) -> Maybe sublogics2 -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((sublogics2 -> sublogics2 -> Bool)
-> sublogics2 -> sublogics2 -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip sublogics2 -> sublogics2 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem (sublogics2 -> sublogics2 -> Bool)
-> sublogics2 -> sublogics2 -> Bool
forall a b. (a -> b) -> a -> b
$ ProverTemplate
  (Theory sign2 sentence2 proof_tree2)
  sentence2
  morphism2
  sublogics2
  proof_tree2
-> sublogics2
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> sublogics
proverSublogic ProverTemplate
  (Theory sign2 sentence2 proof_tree2)
  sentence2
  morphism2
  sublogics2
  proof_tree2
p)
                           (cid -> sublogics1 -> Maybe sublogics2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1 -> Maybe sublogics2
mapSublogic cid
cid (sublogics1 -> Maybe sublogics2) -> sublogics1 -> Maybe sublogics2
forall a b. (a -> b) -> a -> b
$ lid -> lid1 -> sublogics -> sublogics1
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
lid1 -> lid2 -> sublogics1 -> sublogics2
forceCoerceSublogic lid
lid lid1
slid sublogics
sl)
                  then (lid2
-> ProverTemplate
     (Theory sign2 sentence2 proof_tree2)
     sentence2
     morphism2
     sublogics2
     proof_tree2
-> G_prover
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Prover sign sentence morphism sublogics proof_tree -> G_prover
G_prover lid2
tlid ProverTemplate
  (Theory sign2 sentence2 proof_tree2)
  sentence2
  morphism2
  sublogics2
  proof_tree2
p, AnyComorphism
cm) (G_prover, AnyComorphism)
-> [(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)]
forall a. a -> [a] -> [a]
: [(G_prover, AnyComorphism)]
l else [(G_prover, AnyComorphism)]
l)
             [] (lid2
-> [ProverTemplate
      (Theory sign2 sentence2 proof_tree2)
      sentence2
      morphism2
      sublogics2
      proof_tree2]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [Prover sign sentence morphism sublogics proof_tree]
provers lid2
tlid)

knownProvers :: LogicGraph -> ProverKind -> Map.Map G_sublogics [G_prover]
knownProvers :: LogicGraph -> ProverKind -> Map G_sublogics [G_prover]
knownProvers lg :: LogicGraph
lg pk :: ProverKind
pk =
 let l :: [AnyLogic]
l = Map String AnyLogic -> [AnyLogic]
forall k a. Map k a -> [a]
Map.elems (Map String AnyLogic -> [AnyLogic])
-> Map String AnyLogic -> [AnyLogic]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
lg
 in (Map G_sublogics [G_prover]
 -> AnyLogic -> Map G_sublogics [G_prover])
-> Map G_sublogics [G_prover]
-> [AnyLogic]
-> Map G_sublogics [G_prover]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map G_sublogics [G_prover]
m (Logic lid :: lid
lid) -> (Map G_sublogics [G_prover]
 -> ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree
 -> Map G_sublogics [G_prover])
-> Map G_sublogics [G_prover]
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> Map G_sublogics [G_prover]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m' :: Map G_sublogics [G_prover]
m' p :: ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
p ->
     let lgx :: G_sublogics
lgx = lid -> sublogics -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics lid
lid (ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
-> sublogics
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> sublogics
proverSublogic ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
p)
         p' :: G_prover
p' = lid
-> ProverTemplate
     (Theory sign sentence proof_tree)
     sentence
     morphism
     sublogics
     proof_tree
-> G_prover
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Prover sign sentence morphism sublogics proof_tree -> G_prover
G_prover lid
lid ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
p
     in case G_sublogics -> Map G_sublogics [G_prover] -> Maybe [G_prover]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup G_sublogics
lgx Map G_sublogics [G_prover]
m' of
         Just ps :: [G_prover]
ps -> G_sublogics
-> [G_prover]
-> Map G_sublogics [G_prover]
-> Map G_sublogics [G_prover]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert G_sublogics
lgx (G_prover
p' G_prover -> [G_prover] -> [G_prover]
forall a. a -> [a] -> [a]
: [G_prover]
ps) Map G_sublogics [G_prover]
m'
         Nothing -> G_sublogics
-> [G_prover]
-> Map G_sublogics [G_prover]
-> Map G_sublogics [G_prover]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert G_sublogics
lgx [G_prover
p'] Map G_sublogics [G_prover]
m') Map G_sublogics [G_prover]
m ([ProverTemplate
    (Theory sign sentence proof_tree)
    sentence
    morphism
    sublogics
    proof_tree]
 -> Map G_sublogics [G_prover])
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> Map G_sublogics [G_prover]
forall a b. (a -> b) -> a -> b
$
     (ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree
 -> Bool)
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
forall a. (a -> Bool) -> [a] -> [a]
filter (ProverKind
-> ProverTemplate
     (Theory sign sentence proof_tree)
     sentence
     morphism
     sublogics
     proof_tree
-> Bool
forall x s m y z. ProverKind -> ProverTemplate x s m y z -> Bool
hasProverKind ProverKind
pk)
            (lid
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [Prover sign sentence morphism sublogics proof_tree]
provers lid
lid)) Map G_sublogics [G_prover]
forall k a. Map k a
Map.empty [AnyLogic]
l

unsafeCompComorphism :: AnyComorphism -> AnyComorphism -> AnyComorphism
unsafeCompComorphism :: AnyComorphism -> AnyComorphism -> AnyComorphism
unsafeCompComorphism c1 :: AnyComorphism
c1 c2 :: AnyComorphism
c2 = case AnyComorphism -> AnyComorphism -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism AnyComorphism
c1 AnyComorphism
c2 of
 Result _ (Just c_new :: AnyComorphism
c_new) -> AnyComorphism
c_new
 r :: Result AnyComorphism
r -> String -> Result AnyComorphism -> AnyComorphism
forall a. String -> Result a -> a
propagateErrors "Proofs.AbstractState.unsafeCompComorphism" Result AnyComorphism
r

isSubElemG :: G_sublogics -> G_sublogics -> Bool
isSubElemG :: G_sublogics -> G_sublogics -> Bool
isSubElemG (G_sublogics lid :: lid
lid sl :: sublogics
sl) (G_sublogics lid1 :: lid
lid1 sl1 :: sublogics
sl1) =
 lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lid AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lid1 Bool -> Bool -> Bool
&&
 sublogics -> sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem sublogics
sl (sublogics -> sublogics
forall a b. a -> b
Unsafe.Coerce.unsafeCoerce sublogics
sl1)

pathToComorphism :: ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
                    -> AnyComorphism
pathToComorphism :: ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
-> AnyComorphism
pathToComorphism (path :: [((G_sublogics, t1), AnyComorphism)]
path, (G_sublogics lid :: lid
lid sub :: sublogics
sub, _)) =
 case [((G_sublogics, t1), AnyComorphism)]
path of
  [] -> InclComorphism lid sublogics -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism (InclComorphism lid sublogics -> AnyComorphism)
-> InclComorphism lid sublogics -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ lid -> sublogics -> InclComorphism lid sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> InclComorphism lid sublogics
mkIdComorphism lid
lid sublogics
sub
  ((G_sublogics lid1 :: lid
lid1 sub1 :: sublogics
sub1, _), c :: AnyComorphism
c) : cs :: [((G_sublogics, t1), AnyComorphism)]
cs ->
   (AnyComorphism -> AnyComorphism -> AnyComorphism)
-> AnyComorphism -> [AnyComorphism] -> AnyComorphism
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl AnyComorphism -> AnyComorphism -> AnyComorphism
unsafeCompComorphism
    (InclComorphism lid sublogics -> AnyComorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> AnyComorphism
Comorphism (InclComorphism lid sublogics -> AnyComorphism)
-> InclComorphism lid sublogics -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ lid -> sublogics -> InclComorphism lid sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> InclComorphism lid sublogics
mkIdComorphism lid
lid1 sublogics
sub1)
    (AnyComorphism
c AnyComorphism -> [AnyComorphism] -> [AnyComorphism]
forall a. a -> [a] -> [a]
: ([(G_sublogics, t1)], [AnyComorphism]) -> [AnyComorphism]
forall a b. (a, b) -> b
snd ([((G_sublogics, t1), AnyComorphism)]
-> ([(G_sublogics, t1)], [AnyComorphism])
forall a b. [(a, b)] -> ([a], [b])
unzip [((G_sublogics, t1), AnyComorphism)]
cs))

getUsableProvers :: ProverKind -> G_sublogics -> LogicGraph
 -> IO [(G_prover, AnyComorphism)]
getUsableProvers :: ProverKind
-> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)]
getUsableProvers pk :: ProverKind
pk start :: G_sublogics
start =
  ((G_prover, AnyComorphism) -> IO Bool)
-> [(G_prover, AnyComorphism)] -> IO [(G_prover, AnyComorphism)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (G_prover -> IO Bool
usable (G_prover -> IO Bool)
-> ((G_prover, AnyComorphism) -> G_prover)
-> (G_prover, AnyComorphism)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_prover, AnyComorphism) -> G_prover
forall a b. (a, b) -> a
fst) ([(G_prover, AnyComorphism)] -> IO [(G_prover, AnyComorphism)])
-> (LogicGraph -> [(G_prover, AnyComorphism)])
-> LogicGraph
-> IO [(G_prover, AnyComorphism)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProverKind
-> G_sublogics -> LogicGraph -> [(G_prover, AnyComorphism)]
getAllProvers ProverKind
pk G_sublogics
start

getAllProvers :: ProverKind -> G_sublogics -> LogicGraph
 -> [(G_prover, AnyComorphism)]
getAllProvers :: ProverKind
-> G_sublogics -> LogicGraph -> [(G_prover, AnyComorphism)]
getAllProvers pk :: ProverKind
pk start :: G_sublogics
start lg :: LogicGraph
lg =
  let kp :: Map G_sublogics [G_prover]
kp = LogicGraph -> ProverKind -> Map G_sublogics [G_prover]
knownProvers LogicGraph
lg ProverKind
pk
      g :: Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
g = LogicGraph
-> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
logicGraph2Graph LogicGraph
lg
  in (([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
  (G_sublogics, Maybe AnyComorphism))
 -> [(G_prover, AnyComorphism)])
-> [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
     (G_sublogics, Maybe AnyComorphism))]
-> [(G_prover, AnyComorphism)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Map G_sublogics [G_prover]
-> ([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
    (G_sublogics, Maybe AnyComorphism))
-> [(G_prover, AnyComorphism)]
forall t2 t1 t.
Map G_sublogics [t2]
-> ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
-> [(t2, AnyComorphism)]
mkComorphism Map G_sublogics [G_prover]
kp) ([([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
   (G_sublogics, Maybe AnyComorphism))]
 -> [(G_prover, AnyComorphism)])
-> [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
     (G_sublogics, Maybe AnyComorphism))]
-> [(G_prover, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$
      (G_sublogics
 -> [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
      (G_sublogics, Maybe AnyComorphism))])
-> [G_sublogics]
-> [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
     (G_sublogics, Maybe AnyComorphism))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ end :: G_sublogics
end ->
       Int
-> (G_sublogics, Maybe AnyComorphism)
-> ((G_sublogics, Maybe AnyComorphism) -> Bool)
-> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
-> [([((G_sublogics, Maybe AnyComorphism), AnyComorphism)],
     (G_sublogics, Maybe AnyComorphism))]
forall node edge.
(Ord node, Eq edge, Show node, Show edge) =>
Int
-> node
-> (node -> Bool)
-> Graph node edge
-> [([(node, edge)], node)]
yen 10 (G_sublogics
start, Maybe AnyComorphism
forall a. Maybe a
Nothing) (\ (l :: G_sublogics
l, _) -> G_sublogics -> G_sublogics -> Bool
isSubElemG G_sublogics
l G_sublogics
end) Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
g)
       (Map G_sublogics [G_prover] -> [G_sublogics]
forall k a. Map k a -> [k]
Map.keys Map G_sublogics [G_prover]
kp)
 where
  mkComorphism :: Map.Map G_sublogics [t2]
   -> ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
   -> [(t2, AnyComorphism)]
  mkComorphism :: Map G_sublogics [t2]
-> ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
-> [(t2, AnyComorphism)]
mkComorphism kp :: Map G_sublogics [t2]
kp path :: ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
path@(_, (end :: G_sublogics
end, _)) =
   let fullComorphism :: AnyComorphism
fullComorphism = ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
-> AnyComorphism
forall t1 t.
([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
-> AnyComorphism
pathToComorphism ([((G_sublogics, t1), AnyComorphism)], (G_sublogics, t))
path
       cs :: [(G_sublogics, [t2])]
cs = Map G_sublogics [t2] -> [(G_sublogics, [t2])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map G_sublogics [t2] -> [(G_sublogics, [t2])])
-> Map G_sublogics [t2] -> [(G_sublogics, [t2])]
forall a b. (a -> b) -> a -> b
$ (G_sublogics -> [t2] -> Bool)
-> Map G_sublogics [t2] -> Map G_sublogics [t2]
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ l :: G_sublogics
l _ -> G_sublogics -> G_sublogics -> Bool
isSubElemG G_sublogics
end G_sublogics
l) Map G_sublogics [t2]
kp
   in ((G_sublogics, [t2]) -> [(t2, AnyComorphism)])
-> [(G_sublogics, [t2])] -> [(t2, AnyComorphism)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ x :: (G_sublogics, [t2])
x -> case (G_sublogics, [t2])
x of
                        (_, ps :: [t2]
ps) -> (t2 -> (t2, AnyComorphism)) -> [t2] -> [(t2, AnyComorphism)]
forall a b. (a -> b) -> [a] -> [b]
map (\ p :: t2
p -> (t2
p, AnyComorphism
fullComorphism)) [t2]
ps) [(G_sublogics, [t2])]
cs

{- | the list of proof statuses is integrated into the goalMap of the state
after validation of the Disproved Statuses -}
markProved ::
  ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
                sign morphism symbol raw_symbol proof_tree )
  => AnyComorphism -> lid -> [ProofStatus proof_tree]
  -> ProofState
  -> ProofState
markProved :: AnyComorphism
-> lid -> [ProofStatus proof_tree] -> ProofState -> ProofState
markProved c :: AnyComorphism
c lid :: lid
lid status :: [ProofStatus proof_tree]
status st :: ProofState
st = ProofState
st
    { currentTheory :: G_theory
currentTheory = AnyComorphism
-> lid -> [ProofStatus proof_tree] -> G_theory -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
AnyComorphism
-> lid -> [ProofStatus proof_tree] -> G_theory -> G_theory
markProvedGoalMap AnyComorphism
c lid
lid [ProofStatus proof_tree]
status (ProofState -> G_theory
currentTheory ProofState
st) }

-- | mark all newly proven goals with their proof tree
markProvedGoalMap ::
    ( Logic lid sublogics basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree )
    => AnyComorphism -> lid -> [ProofStatus proof_tree]
    -> G_theory -> G_theory
markProvedGoalMap :: AnyComorphism
-> lid -> [ProofStatus proof_tree] -> G_theory -> G_theory
markProvedGoalMap c :: AnyComorphism
c lid :: lid
lid status :: [ProofStatus proof_tree]
status th :: G_theory
th = case G_theory
th of
  G_theory lid1 :: lid
lid1 syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig si :: SigId
si thSens :: ThSens sentence (AnyComorphism, BasicProof)
thSens _ ->
      let updStat :: ProofStatus proof_tree
-> SenAttr a (ThmStatus (AnyComorphism, BasicProof))
-> Maybe (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
updStat ps :: ProofStatus proof_tree
ps s :: SenAttr a (ThmStatus (AnyComorphism, BasicProof))
s = SenAttr a (ThmStatus (AnyComorphism, BasicProof))
-> Maybe (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
forall a. a -> Maybe a
Just (SenAttr a (ThmStatus (AnyComorphism, BasicProof))
 -> Maybe (SenAttr a (ThmStatus (AnyComorphism, BasicProof))))
-> SenAttr a (ThmStatus (AnyComorphism, BasicProof))
-> Maybe (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
forall a b. (a -> b) -> a -> b
$
                SenAttr a (ThmStatus (AnyComorphism, BasicProof))
s { senAttr :: ThmStatus (AnyComorphism, BasicProof)
senAttr = [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a. [a] -> ThmStatus a
ThmStatus ([(AnyComorphism, BasicProof)]
 -> ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ (AnyComorphism
c, lid -> ProofStatus proof_tree -> BasicProof
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ProofStatus proof_tree -> BasicProof
BasicProof lid
lid ProofStatus proof_tree
ps) (AnyComorphism, BasicProof)
-> [(AnyComorphism, BasicProof)] -> [(AnyComorphism, BasicProof)]
forall a. a -> [a] -> [a]
: SenAttr a (ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenAttr a (ThmStatus (AnyComorphism, BasicProof))
s }
          upd :: ProofStatus proof_tree
-> OMap String (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
-> OMap String (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
upd pStat :: ProofStatus proof_tree
pStat = (SenAttr a (ThmStatus (AnyComorphism, BasicProof))
 -> Maybe (SenAttr a (ThmStatus (AnyComorphism, BasicProof))))
-> String
-> OMap String (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
-> OMap String (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
forall k a. Ord k => (a -> Maybe a) -> k -> OMap k a -> OMap k a
OMap.update (ProofStatus proof_tree
-> SenAttr a (ThmStatus (AnyComorphism, BasicProof))
-> Maybe (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
forall sublogics basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol proof_tree a.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
ProofStatus proof_tree
-> SenAttr a (ThmStatus (AnyComorphism, BasicProof))
-> Maybe (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
updStat ProofStatus proof_tree
pStat) (ProofStatus proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
goalName ProofStatus proof_tree
pStat)
      in lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid1 Maybe IRI
syn ExtSign sign symbol
sig SigId
si ((ThSens sentence (AnyComorphism, BasicProof)
 -> ProofStatus proof_tree
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> [ProofStatus proof_tree]
-> ThSens sentence (AnyComorphism, BasicProof)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((ProofStatus proof_tree
 -> ThSens sentence (AnyComorphism, BasicProof)
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ProofStatus proof_tree
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ProofStatus proof_tree
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall sublogics basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol proof_tree a.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
ProofStatus proof_tree
-> OMap String (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
-> OMap String (SenAttr a (ThmStatus (AnyComorphism, BasicProof)))
upd) ThSens sentence (AnyComorphism, BasicProof)
thSens [ProofStatus proof_tree]
status)
        ThId
startThId

autoProofAtNode ::
                   -- use theorems is subsequent proofs
                  Bool
                   -- Timeout Limit
                  -> Int
                   -- selected goals
                  -> [String]
                   -- selected axioms
                  -> [String]
                   -- Node selected for proving
                  -> G_theory
                   -- selected Prover and Comorphism
                  -> ( G_prover, AnyComorphism )
                   -- returns new GoalStatus for the Node
                  -> ResultT IO ((G_theory, [(String, String, String)]),
                                 (ProofState, [ProofStatus G_proof_tree]))
autoProofAtNode :: Bool
-> Int
-> [String]
-> [String]
-> G_theory
-> (G_prover, AnyComorphism)
-> ResultT
     IO
     ((G_theory, [(String, String, String)]),
      (ProofState, [ProofStatus G_proof_tree]))
autoProofAtNode useTh :: Bool
useTh timeout :: Int
timeout goals :: [String]
goals axioms :: [String]
axioms g_th :: G_theory
g_th p_cm :: (G_prover, AnyComorphism)
p_cm = do
      let knpr :: KnownProversMap
knpr = String -> Result KnownProversMap -> KnownProversMap
forall a. String -> Result a -> a
propagateErrors "autoProofAtNode"
            (Result KnownProversMap -> KnownProversMap)
-> Result KnownProversMap -> KnownProversMap
forall a b. (a -> b) -> a -> b
$ ProverKind -> Result KnownProversMap
knownProversWithKind ProverKind
ProveCMDLautomatic
          pf_st :: ProofState
pf_st = String -> G_theory -> KnownProversMap -> ProofState
initialState "" G_theory
g_th KnownProversMap
knpr
          sg_st :: ProofState
sg_st = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
goals then ProofState
pf_st else ProofState
pf_st
            { selectedGoals :: [String]
selectedGoals = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
goals) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ ProofState -> [String]
selectedGoals ProofState
pf_st }
          sa_st :: ProofState
sa_st = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
axioms then ProofState
sg_st else ProofState
sg_st
            { includedAxioms :: [String]
includedAxioms = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
axioms) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ ProofState -> [String]
includedAxioms ProofState
sg_st }
          st :: ProofState
st = ProofState -> ProofState
recalculateSublogicAndSelectedTheory ProofState
sa_st
      -- try to prepare the theory
      if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ ProofState -> [String]
selectedGoals ProofState
st then String
-> ResultT
     IO
     ((G_theory, [(String, String, String)]),
      (ProofState, [ProofStatus G_proof_tree]))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "autoProofAtNode: no goals selected"
        else do
          (G_theory_with_prover lid1 :: lid
lid1 th :: Theory sign sentence proof_tree
th p :: Prover sign sentence morphism sublogics proof_tree
p) <- Result G_theory_with_prover -> ResultT IO G_theory_with_prover
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result G_theory_with_prover -> ResultT IO G_theory_with_prover)
-> Result G_theory_with_prover -> ResultT IO G_theory_with_prover
forall a b. (a -> b) -> a -> b
$ ProofState
-> (G_prover, AnyComorphism) -> Result G_theory_with_prover
prepareForProving ProofState
st (G_prover, AnyComorphism)
p_cm
          case Prover sign sentence morphism sublogics proof_tree
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> Theory sign sentence proof_tree
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
proveCMDLautomaticBatch Prover sign sentence morphism sublogics proof_tree
p of
            Nothing ->
              String
-> ResultT
     IO
     ((G_theory, [(String, String, String)]),
      (ProofState, [ProofStatus G_proof_tree]))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "autoProofAtNode: failed to init CMDLautomaticBatch"
            Just fn :: Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> TacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (ThreadId, MVar ())
fn -> do
              let encapsulate_pt :: ProofStatus proof_tree -> ProofStatus G_proof_tree
encapsulate_pt ps :: ProofStatus proof_tree
ps =
                   ProofStatus proof_tree
ps {proofTree :: G_proof_tree
proofTree = lid -> proof_tree -> G_proof_tree
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> proof_tree -> G_proof_tree
G_proof_tree lid
lid1 (proof_tree -> G_proof_tree) -> proof_tree -> G_proof_tree
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> proof_tree
forall proof_tree. ProofStatus proof_tree -> proof_tree
proofTree ProofStatus proof_tree
ps}
              Result [ProofStatus proof_tree]
d <- IO (Result [ProofStatus proof_tree])
-> ResultT IO (Result [ProofStatus proof_tree])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Result [ProofStatus proof_tree])
 -> ResultT IO (Result [ProofStatus proof_tree]))
-> IO (Result [ProofStatus proof_tree])
-> ResultT IO (Result [ProofStatus proof_tree])
forall a b. (a -> b) -> a -> b
$ do
                -- mVar to poll the prover for results
                MVar (Result [ProofStatus proof_tree])
answ <- Result [ProofStatus proof_tree]
-> IO (MVar (Result [ProofStatus proof_tree]))
forall a. a -> IO (MVar a)
newMVar ([ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
                (_, mV :: MVar ()
mV) <- Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> TacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (ThreadId, MVar ())
fn Bool
useTh Bool
False MVar (Result [ProofStatus proof_tree])
answ (ProofState -> String
theoryName ProofState
st)
                                       (String -> TacticScript
TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
timeout) Theory sign sentence proof_tree
th []
                MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
mV
                MVar (Result [ProofStatus proof_tree])
-> IO (Result [ProofStatus proof_tree])
forall a. MVar a -> IO a
takeMVar MVar (Result [ProofStatus proof_tree])
answ
              case Result [ProofStatus proof_tree] -> Maybe [ProofStatus proof_tree]
forall a. Result a -> Maybe a
maybeResult Result [ProofStatus proof_tree]
d of
                Nothing -> String
-> ResultT
     IO
     ((G_theory, [(String, String, String)]),
      (ProofState, [ProofStatus G_proof_tree]))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "autoProofAtNode: proving failed"
                Just d' :: [ProofStatus proof_tree]
d' ->
                 ((G_theory, [(String, String, String)]),
 (ProofState, [ProofStatus G_proof_tree]))
-> ResultT
     IO
     ((G_theory, [(String, String, String)]),
      (ProofState, [ProofStatus G_proof_tree]))
forall (m :: * -> *) a. Monad m => a -> m a
return (( ProofState -> G_theory
currentTheory (ProofState -> G_theory) -> ProofState -> G_theory
forall a b. (a -> b) -> a -> b
$ AnyComorphism
-> lid -> [ProofStatus proof_tree] -> ProofState -> ProofState
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
AnyComorphism
-> lid -> [ProofStatus proof_tree] -> ProofState -> ProofState
markProved ((G_prover, AnyComorphism) -> AnyComorphism
forall a b. (a, b) -> b
snd (G_prover, AnyComorphism)
p_cm) lid
lid1 [ProofStatus proof_tree]
d' ProofState
st
                         , (ProofStatus proof_tree -> (String, String, String))
-> [ProofStatus proof_tree] -> [(String, String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\ ps :: ProofStatus proof_tree
ps -> ( ProofStatus proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
goalName ProofStatus proof_tree
ps
                                        , GoalStatus -> String
forall a. Show a => a -> String
show (GoalStatus -> String) -> GoalStatus -> String
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus proof_tree
ps
                                        , proof_tree -> String
forall a. Show a => a -> String
show (proof_tree -> String) -> proof_tree -> String
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> proof_tree
forall proof_tree. ProofStatus proof_tree -> proof_tree
proofTree ProofStatus proof_tree
ps)) [ProofStatus proof_tree]
d')
                         , (ProofState
st, (ProofStatus proof_tree -> ProofStatus G_proof_tree)
-> [ProofStatus proof_tree] -> [ProofStatus G_proof_tree]
forall a b. (a -> b) -> [a] -> [b]
map ProofStatus proof_tree -> ProofStatus G_proof_tree
forall sublogics basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
ProofStatus proof_tree -> ProofStatus G_proof_tree
encapsulate_pt [ProofStatus proof_tree]
d'))