```{- |
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
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 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

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.
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.
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 :: * -> *).
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.
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.
(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,
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.
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.
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.
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 ()
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.
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
```