{- |
Module      :  ./Proofs/InferBasic.hs
Description :  devGraph rule that calls provers for specific logics
Copyright   :  (c) J. Gerken, T. Mossakowski, K. Luettich, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

devGraph rule that calls provers for specific logics

Proof rule "basic inference" in the development graphs calculus.
   Follows Sect. IV:4.4 of the CASL Reference Manual.

   References:

   T. Mossakowski, S. Autexier and D. Hutter:
   Extending Development Graphs With Hiding.
   H. Hussmann (ed.): Fundamental Approaches to Software Engineering 2001,
   Lecture Notes in Computer Science 2029, p. 269-283,
   Springer-Verlag 2001.

-}

module Proofs.InferBasic
  ( basicInferenceNode
  ) where

import Static.GTheory
import Static.DevGraph
import Static.ComputeTheory

import Proofs.EdgeUtils
import Proofs.AbstractState
import Proofs.FreeDefLinks

import Common.LibName
import Common.Result
import Common.ResultT
import Common.AS_Annotation

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

import Comorphisms.KnownProvers

import GUI.Utils
import GUI.ProverGUI

import Interfaces.DataTypes
import Interfaces.Utils

import Data.IORef
import Data.Graph.Inductive.Graph
import Data.Maybe

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

selectProver :: [(G_prover, AnyComorphism)]
             -> ResultT IO (G_prover, AnyComorphism)
selectProver :: [(G_prover, AnyComorphism)] -> ResultT IO (G_prover, AnyComorphism)
selectProver ps :: [(G_prover, AnyComorphism)]
ps = case [(G_prover, AnyComorphism)]
ps of
  [] -> String -> ResultT IO (G_prover, AnyComorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "No prover available"
  [p :: (G_prover, AnyComorphism)
p] -> (G_prover, AnyComorphism) -> ResultT IO (G_prover, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_prover, AnyComorphism)
p
  _ -> do
   Maybe Int
sel <- IO (Maybe Int) -> ResultT IO (Maybe Int)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe Int) -> ResultT IO (Maybe Int))
-> IO (Maybe Int) -> ResultT IO (Maybe Int)
forall a b. (a -> b) -> a -> b
$ String -> [String] -> IO (Maybe Int)
listBox "Choose a translation to a prover-supported logic"
     ([String] -> IO (Maybe Int)) -> [String] -> IO (Maybe Int)
forall a b. (a -> b) -> a -> b
$ ((G_prover, AnyComorphism) -> String)
-> [(G_prover, AnyComorphism)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (aGN :: G_prover
aGN, cm :: AnyComorphism
cm) -> AnyComorphism -> ShowS
forall a. Show a => a -> ShowS
shows AnyComorphism
cm ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ " (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ G_prover -> String
getProverName G_prover
aGN String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")") [(G_prover, AnyComorphism)]
ps
   Int
i <- case Maybe Int
sel of
           Just j :: Int
j -> Int -> ResultT IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
j
           _ -> String -> ResultT IO Int
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Proofs.Proofs: selection"
   (G_prover, AnyComorphism) -> ResultT IO (G_prover, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return ((G_prover, AnyComorphism) -> ResultT IO (G_prover, AnyComorphism))
-> (G_prover, AnyComorphism)
-> ResultT IO (G_prover, AnyComorphism)
forall a b. (a -> b) -> a -> b
$ [(G_prover, AnyComorphism)]
ps [(G_prover, AnyComorphism)] -> Int -> (G_prover, AnyComorphism)
forall a. [a] -> Int -> a
!! Int
i

proveTheory :: 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
           -> String -> Theory sign sentence proof_tree
           -> [FreeDefMorphism sentence morphism]
           -> IO ( [ProofStatus proof_tree]
                , [(Named sentence, ProofStatus proof_tree)])
proveTheory :: lid
-> Prover sign sentence morphism sublogics proof_tree
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
proveTheory _ =
    (String
 -> Theory sign sentence proof_tree
 -> [FreeDefMorphism sentence morphism]
 -> IO
      ([ProofStatus proof_tree],
       [(Named sentence, ProofStatus proof_tree)]))
-> Maybe
     (String
      -> Theory sign sentence proof_tree
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
forall a. a -> Maybe a -> a
fromMaybe (\ _ _ -> String
-> [FreeDefMorphism sentence morphism]
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
forall a. HasCallStack => String -> a
error "proveGUI not implemented") (Maybe
   (String
    -> Theory sign sentence proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO
         ([ProofStatus proof_tree],
          [(Named sentence, ProofStatus proof_tree)]))
 -> String
 -> Theory sign sentence proof_tree
 -> [FreeDefMorphism sentence morphism]
 -> IO
      ([ProofStatus proof_tree],
       [(Named sentence, ProofStatus proof_tree)]))
-> (Prover sign sentence morphism sublogics proof_tree
    -> Maybe
         (String
          -> Theory sign sentence proof_tree
          -> [FreeDefMorphism sentence morphism]
          -> IO
               ([ProofStatus proof_tree],
                [(Named sentence, ProofStatus proof_tree)])))
-> Prover sign sentence morphism sublogics proof_tree
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prover sign sentence morphism sublogics proof_tree
-> Maybe
     (String
      -> Theory sign sentence proof_tree
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> Maybe
     (String
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO
           ([ProofStatus proof_tree],
            [(Named sentence, ProofStatus proof_tree)]))
proveGUI


{- | applies basic inference to a given node. The result is a theory which is
     either a model after a consistency check or a new theory for the node
     label -}
basicInferenceNode :: LogicGraph -> LibName -> DGraph -> LNode DGNodeLab
                   -> LibEnv -> IORef IntState
                   -> IO (Result G_theory)
basicInferenceNode :: LogicGraph
-> LibName
-> DGraph
-> LNode DGNodeLab
-> LibEnv
-> IORef IntState
-> IO (Result G_theory)
basicInferenceNode lg :: LogicGraph
lg ln :: LibName
ln dGraph :: DGraph
dGraph (node :: Int
node, lbl :: DGNodeLab
lbl) libEnv :: LibEnv
libEnv intSt :: IORef IntState
intSt =
  ResultT IO G_theory -> IO (Result G_theory)
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO G_theory -> IO (Result G_theory))
-> ResultT IO G_theory -> IO (Result G_theory)
forall a b. (a -> b) -> a -> b
$ do
    -- compute the theory (that may contain proved theorems) and its name
    G_theory
thForProof <- Result G_theory -> ResultT IO G_theory
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result G_theory -> ResultT IO G_theory)
-> Result G_theory -> ResultT IO G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Result G_theory
getGlobalTheory DGNodeLab
lbl
    let thName :: String
thName = LibName -> String
libToFileName LibName
ln String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
lbl
        freedefs :: [GFreeDefMorphism]
freedefs = LibEnv -> LibName -> DGraph -> Int -> [GFreeDefMorphism]
getCFreeDefMorphs LibEnv
libEnv LibName
ln DGraph
dGraph Int
node
    [(G_prover, AnyComorphism)]
ps <- IO [(G_prover, AnyComorphism)]
-> ResultT IO [(G_prover, AnyComorphism)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [(G_prover, AnyComorphism)]
 -> ResultT IO [(G_prover, AnyComorphism)])
-> IO [(G_prover, AnyComorphism)]
-> ResultT IO [(G_prover, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ ProverKind
-> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)]
getUsableProvers ProverKind
ProveGUI (G_theory -> G_sublogics
sublogicOfTh G_theory
thForProof) LogicGraph
lg
    KnownProversMap
kpMap <- Result KnownProversMap -> ResultT IO KnownProversMap
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR Result KnownProversMap
knownProversGUI
    {- let kpMap = foldl (\m (G_prover _ p,c) ->
         case Map.lookup (proverName p) m of
          Just cs -> Map.insert (proverName p) (c:cs) m
          Nothing -> Map.insert (proverName p) [c] m) Map.empty ps -}
    IO (Result G_theory) -> ResultT IO G_theory
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result G_theory) -> ResultT IO G_theory)
-> IO (Result G_theory) -> ResultT IO G_theory
forall a b. (a -> b) -> a -> b
$ ProofActions
-> String
-> String
-> G_theory
-> KnownProversMap
-> [(G_prover, AnyComorphism)]
-> IO (Result G_theory)
proverGUI ProofActions :: (ProofState -> IO (Result ProofState))
-> (ProofState -> IO (Result ProofState))
-> (ProofState -> IO ProofState)
-> ProofActions
ProofActions
      { proveF :: ProofState -> IO (Result ProofState)
proveF = LogicGraph
-> IORef IntState
-> [GFreeDefMorphism]
-> ProofState
-> IO (Result ProofState)
proveKnownPMap LogicGraph
lg IORef IntState
intSt [GFreeDefMorphism]
freedefs
      , fineGrainedSelectionF :: ProofState -> IO (Result ProofState)
fineGrainedSelectionF = LogicGraph
-> IORef IntState
-> [GFreeDefMorphism]
-> ProofState
-> IO (Result ProofState)
proveFineGrainedSelect LogicGraph
lg IORef IntState
intSt [GFreeDefMorphism]
freedefs
      , recalculateSublogicF :: ProofState -> IO ProofState
recalculateSublogicF = ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState -> IO ProofState)
-> (ProofState -> ProofState) -> ProofState -> IO ProofState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofState -> ProofState
recalculateSublogicAndSelectedTheory
      } String
thName (DGNodeLab -> String
hidingLabelWarning DGNodeLab
lbl) G_theory
thForProof KnownProversMap
kpMap [(G_prover, AnyComorphism)]
ps

proveKnownPMap :: LogicGraph
    -> IORef IntState
    -> [GFreeDefMorphism]
    -> ProofState -> IO (Result ProofState)
proveKnownPMap :: LogicGraph
-> IORef IntState
-> [GFreeDefMorphism]
-> ProofState
-> IO (Result ProofState)
proveKnownPMap lg :: LogicGraph
lg intSt :: IORef IntState
intSt freedefs :: [GFreeDefMorphism]
freedefs st :: ProofState
st =
    IO (Result ProofState)
-> ((G_prover, AnyComorphism) -> IO (Result ProofState))
-> Maybe (G_prover, AnyComorphism)
-> IO (Result ProofState)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (LogicGraph
-> IORef IntState
-> [GFreeDefMorphism]
-> ProofState
-> IO (Result ProofState)
proveFineGrainedSelect LogicGraph
lg IORef IntState
intSt [GFreeDefMorphism]
freedefs ProofState
st)
          (ProofState
-> IORef IntState
-> Bool
-> [GFreeDefMorphism]
-> (G_prover, AnyComorphism)
-> IO (Result ProofState)
callProver ProofState
st IORef IntState
intSt Bool
False [GFreeDefMorphism]
freedefs) (Maybe (G_prover, AnyComorphism) -> IO (Result ProofState))
-> Maybe (G_prover, AnyComorphism) -> IO (Result ProofState)
forall a b. (a -> b) -> a -> b
$
          ProofState -> ProverKind -> Maybe (G_prover, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> ProverKind -> m (G_prover, AnyComorphism)
lookupKnownProver ProofState
st ProverKind
ProveGUI

callProver :: ProofState
    -> IORef IntState
    -> Bool -- indicates if a translation was chosen
    -> [GFreeDefMorphism]
    -> (G_prover, AnyComorphism) -> IO (Result ProofState)
callProver :: ProofState
-> IORef IntState
-> Bool
-> [GFreeDefMorphism]
-> (G_prover, AnyComorphism)
-> IO (Result ProofState)
callProver st :: ProofState
st intSt :: IORef IntState
intSt trans_chosen :: Bool
trans_chosen freedefs :: [GFreeDefMorphism]
freedefs p_cm :: (G_prover, AnyComorphism)
p_cm@(_, acm :: AnyComorphism
acm) =
       ResultT IO ProofState -> IO (Result ProofState)
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO ProofState -> IO (Result ProofState))
-> ResultT IO ProofState -> IO (Result ProofState)
forall a b. (a -> b) -> a -> b
$ do
        (_, exit :: IO ()
exit) <- IO (String -> IO (), IO ()) -> ResultT IO (String -> IO (), IO ())
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (String -> IO (), IO ())
 -> ResultT IO (String -> IO (), IO ()))
-> IO (String -> IO (), IO ())
-> ResultT IO (String -> IO (), IO ())
forall a b. (a -> b) -> a -> b
$ String -> String -> IO (String -> IO (), IO ())
pulseBar "prepare for proving" "please wait..."
        G_theory_with_prover lid :: lid
lid 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
        [FreeDefMorphism sentence morphism]
freedefs1 <- (GFreeDefMorphism
 -> ResultT IO (FreeDefMorphism sentence morphism))
-> [GFreeDefMorphism]
-> ResultT IO [FreeDefMorphism sentence morphism]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (GFreeDefMorphism fdlid :: lid
fdlid fd :: FreeDefMorphism sentence morphism
fd) ->
                       lid
-> lid
-> String
-> FreeDefMorphism sentence morphism
-> ResultT IO (FreeDefMorphism sentence morphism)
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
-> FreeDefMorphism sentence1 morphism1
-> m (FreeDefMorphism sentence2 morphism2)
coerceFreeDefMorphism lid
fdlid lid
lid "" FreeDefMorphism sentence morphism
fd) [GFreeDefMorphism]
freedefs
        IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift IO ()
exit
        (ps :: [ProofStatus proof_tree]
ps, _) <- IO
  ([ProofStatus proof_tree],
   [(Named sentence, ProofStatus proof_tree)])
-> ResultT
     IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO
   ([ProofStatus proof_tree],
    [(Named sentence, ProofStatus proof_tree)])
 -> ResultT
      IO
      ([ProofStatus proof_tree],
       [(Named sentence, ProofStatus proof_tree)]))
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
-> ResultT
     IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
forall a b. (a -> b) -> a -> b
$ lid
-> Prover sign sentence morphism sublogics proof_tree
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus 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
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO
     ([ProofStatus proof_tree],
      [(Named sentence, ProofStatus proof_tree)])
proveTheory lid
lid Prover sign sentence morphism sublogics proof_tree
p (ProofState -> String
theoryName ProofState
st) Theory sign sentence proof_tree
th [FreeDefMorphism sentence morphism]
freedefs1
        let st' :: ProofState
st' = 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 AnyComorphism
acm lid
lid [ProofStatus proof_tree]
ps ProofState
st
        IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ IORef IntState
-> ProofState
-> Maybe (G_prover, AnyComorphism)
-> [ProofStatus proof_tree]
-> String
-> (Bool, Int)
-> IO ()
forall proof_tree.
IORef IntState
-> ProofState
-> Maybe (G_prover, AnyComorphism)
-> [ProofStatus proof_tree]
-> String
-> (Bool, Int)
-> IO ()
addCommandHistoryToState IORef IntState
intSt ProofState
st'
               (if Bool
trans_chosen then (G_prover, AnyComorphism) -> Maybe (G_prover, AnyComorphism)
forall a. a -> Maybe a
Just (G_prover, AnyComorphism)
p_cm else Maybe (G_prover, AnyComorphism)
forall a. Maybe a
Nothing) [ProofStatus proof_tree]
ps "" (Bool
False, 0)
        ProofState -> ResultT IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
st'

proveFineGrainedSelect :: LogicGraph
    -> IORef IntState
    -> [GFreeDefMorphism]
    -> ProofState -> IO (Result ProofState)
proveFineGrainedSelect :: LogicGraph
-> IORef IntState
-> [GFreeDefMorphism]
-> ProofState
-> IO (Result ProofState)
proveFineGrainedSelect lg :: LogicGraph
lg intSt :: IORef IntState
intSt freedefs :: [GFreeDefMorphism]
freedefs st :: ProofState
st =
    ResultT IO ProofState -> IO (Result ProofState)
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO ProofState -> IO (Result ProofState))
-> ResultT IO ProofState -> IO (Result ProofState)
forall a b. (a -> b) -> a -> b
$ do
       let sl :: G_sublogics
sl = ProofState -> G_sublogics
sublogicOfTheory ProofState
st
       [(G_prover, AnyComorphism)]
cmsToProvers <- IO [(G_prover, AnyComorphism)]
-> ResultT IO [(G_prover, AnyComorphism)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [(G_prover, AnyComorphism)]
 -> ResultT IO [(G_prover, AnyComorphism)])
-> IO [(G_prover, AnyComorphism)]
-> ResultT IO [(G_prover, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ ProverKind
-> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)]
getUsableProvers ProverKind
ProveGUI G_sublogics
sl LogicGraph
lg
       (G_prover, AnyComorphism)
pr <- [(G_prover, AnyComorphism)] -> ResultT IO (G_prover, AnyComorphism)
selectProver [(G_prover, AnyComorphism)]
cmsToProvers
       IO (Result ProofState) -> ResultT IO ProofState
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result ProofState) -> ResultT IO ProofState)
-> IO (Result ProofState) -> ResultT IO ProofState
forall a b. (a -> b) -> a -> b
$ ProofState
-> IORef IntState
-> Bool
-> [GFreeDefMorphism]
-> (G_prover, AnyComorphism)
-> IO (Result ProofState)
callProver ProofState
st { comorphismsToProvers :: [(G_prover, AnyComorphism)]
comorphismsToProvers = [(G_prover, AnyComorphism)]
cmsToProvers }
                               IORef IntState
intSt Bool
True [GFreeDefMorphism]
freedefs (G_prover, AnyComorphism)
pr