ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder{- |

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederModule : $Header$

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederDescription : CMDL interface commands

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederCopyright : uni-bremen and DFKI

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederMaintainer : r.pascanu@jacobs-university.de

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederStability : provisional

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederPortability : portable

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaederCMDL.ProveConsistency contains prove and consistency check command

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-}

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder

7f0e81a8fc10c17b13569f23474a0e3fbfa79e7dChristian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedermodule CMDL.ProveConsistency

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder ( cProver

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder , cConsChecker

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , doLoop

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , sigIntHandler

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder ) where

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Interfaces.Command

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Interfaces.DataTypes

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Interfaces.GenericATPState (ATPTacticScript (..))

f0742398d4587242b1a115de113cd17f63dcb6d0Christian Maederimport Interfaces.History

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Interfaces.Utils

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport CMDL.DataTypes (CmdlState (intState))

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport CMDL.DataTypesUtils

7f0e81a8fc10c17b13569f23474a0e3fbfa79e7dChristian Maederimport CMDL.Utils (checkPresenceProvers)

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederimport Comorphisms.LogicGraph (logicGraph)

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Proofs.AbstractState

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Static.DevGraph

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederimport Static.DgUtils

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport Static.History

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Logic.Comorphism

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Logic.Grothendieck

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Logic.Logic

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Logic.Prover as P

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Logic.Coerce

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Common.Consistency

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Common.LibName (LibName)

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Common.Result (Result (Result))

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Common.Utils (trim)

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport qualified Common.OrderedMap as OMap

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport Common.AS_Annotation

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport Data.List

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport qualified Data.Map as Map

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Control.Concurrent (ThreadId, killThread)

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Control.Concurrent.MVar (MVar, newMVar, putMVar, takeMVar, readMVar,

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder swapMVar, modifyMVar_)

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Control.Monad

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedernegate_th_with_cons_checker :: G_theory_with_cons_checker -> String -> Maybe G_theory_with_cons_checker

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedernegate_th_with_cons_checker g_th goal = case g_th of

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder G_theory_with_cons_checker lid1 th cons_check ->

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder case (P.tTarget th) of

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder P.Theory lid2 sens -> case OMap.lookup goal sens of

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Nothing -> Nothing

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder Just sen -> case negation lid1 $ sentence sen of

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Nothing -> Nothing

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Just sen' -> let

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder negSen = sen { sentence = sen', isAxiom = True }

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder sens' = OMap.insert goal negSen $ OMap.filter isAxiom sens

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder target' = P.Theory lid2 sens'

f0742398d4587242b1a115de113cd17f63dcb6d0Christian Maeder in Just $ G_theory_with_cons_checker lid1 th{P.tTarget = target'} cons_check

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaedergetProversAutomatic :: G_sublogics -> [(G_prover, AnyComorphism)]

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaedergetProversAutomatic sl = getAllProvers P.ProveCMDLautomatic sl logicGraph

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder-- | Select a prover

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaedercProver :: String -> CmdlState -> IO CmdlState

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaedercProver input state =

e289294500ad68fa0706b09521af340bbb356a69Christian Maeder do

e289294500ad68fa0706b09521af340bbb356a69Christian Maeder -- trimed input

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder inpls <- checkPresenceProvers [trim input]

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder let inp = case inpls of

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder [] -> "Unknown"

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder pnme : _ -> pnme

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder case i_state $ intState state of

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder Nothing -> return $ genMsgAndCode "Nothing selected" 1 state

08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder Just pS ->

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder -- check that some theories are selected

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder case elements pS of

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder [] -> return $ genMsgAndCode "Nothing selected" 1 state

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder Element z _ : _ -> let

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder prov = getProversAutomatic (sublogicOfTheory z)

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder pl = filter ((== inp) . getProverName . fst) prov

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder prover_names = map (getProverName . fst) prov

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder in case case cComorphism pS of

3c72be149cf673945cbe07a04c336fb8f4d406a3Christian Maeder Nothing -> pl

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder Just x -> filter ((== x) . snd) pl ++ pl of

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder [] -> (if inp=="" then do

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder mapM_ putStrLn (nub prover_names)

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder return state

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder else return (genMsgAndCode

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder ("No applicable prover with name \"" ++ inp ++ "\" found") 1

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder state))

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder (p, nCm@(Comorphism cid)) : _ ->

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder return $ add2hist [ ProverChange $ prover pS

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder , CComorphismChange $ cComorphism pS ]

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder $ genMessage "" ("Hint: Using comorphism `"

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder ++ language_name cid ++ "`")

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder state {

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder intState = (intState state) {

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder i_state = Just pS

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder { cComorphism = Just nCm

02b62afbc463450900c5285569e9ab6dc2f9a014Christian Maeder , prover = Just p } } }

02b62afbc463450900c5285569e9ab6dc2f9a014Christian Maeder

02b62afbc463450900c5285569e9ab6dc2f9a014Christian Maeder-- | Selects a consistency checker

cConsChecker :: String -> CmdlState -> IO CmdlState

cConsChecker input state =

do

-- trimed input

let inp = trim input

case i_state $ intState state of

Nothing -> return $ genMsgAndCode "Nothing selected" 1 state

Just pS ->

-- check that some theories are selected

case elements pS of

[] -> return $ genMsgAndCode "Nothing selected" 1 state

Element z _ : _ ->

do

let consCheckList = getConsCheckers $ findComorphismPaths

logicGraph $ sublogicOfTheory z

-- see if any comorphism was used

case cComorphism pS of

{- if none use the theory of the first selected node

to find possible comorphisms -}

Nothing -> case find (\ (y, _) -> getCcName y == inp) consCheckList of

Nothing ->if inp =="" then do

let shortConsCList =nub $ map (\ (y, _) -> getCcName y) consCheckList

mapM_ putStrLn shortConsCList

return state

else return $ genMsgAndCode ("No applicable " ++

"consistency checker with this name found") 1

state

Just (p, _) -> return $ add2hist

[ConsCheckerChange $ consChecker pS]

state {

intState = (intState state) {

i_state = Just pS {

consChecker = Just p }

}

}

Just x ->

case find (\ (y, _) -> getCcName y == inp)

$ getConsCheckers [x] of

Nothing ->

case find (\ (y, _) -> getCcName y == inp) $ consCheckList of

Nothing -> if inp =="" then do

let shortConsCList =nub $ map (\ (y, _) -> getCcName y) consCheckList

mapM_ putStrLn shortConsCList

return state

else return $ genMsgAndCode ("No applicable " ++

"consistency checker with this name found") 1

state

Just (p, nCm@(Comorphism cid)) ->

return $ add2hist [ ConsCheckerChange $ consChecker pS

, CComorphismChange $ cComorphism pS ]

$ genMessage "" ("Hint: Using default comorphism `"

++ language_name cid ++ "`")

state {

intState = (intState state) {

i_state = Just pS {

cComorphism = Just nCm,

consChecker = Just p } } }

Just (p, _) -> return

$ add2hist [ConsCheckerChange $ consChecker pS]

$ state {

intState = (intState state) {

i_state = Just pS { consChecker = Just p } } }

{- | Given a proofstatus the function does the actual call of the

prover for consistency checking -}

checkNode ::

-- Tactic script

ATPTacticScript ->

{- proofState of the node that needs proving

all theorems, goals and axioms should have

been selected before, but the theory should have

not been recomputed -}

Int_NodeInfo ->

-- node name

String ->

{- selected prover, if non one will be automatically

selected -}

Maybe G_cons_checker ->

{- selected comorphism, if non one will be automatically

selected -}

Maybe AnyComorphism ->

MVar (Maybe Int_NodeInfo) ->

MVar IntState ->

LibName ->

-- returns an error message if anything happens

IO String

checkNode sTxt ndpf ndnm mp mcm mSt miSt ln =

case ndpf of

Element pf_st nd ->

do

{- recompute the theory (to make effective the selected axioms,

goals) !? needed? -}

let st = recalculateSublogicAndSelectedTheory pf_st

{- compute a prover,comorphism pair to be used in preparing

the theory -}

p_cm@(_, acm) <- case mcm of

Nothing -> lookupKnownConsChecker st

Just cm' -> case mp of

Nothing -> lookupKnownConsChecker st

Just p' -> return (p', cm')

-- try to prepare the theory

prep <- case prepareForConsChecking st p_cm of

Result _ Nothing ->

do

p_cm'@(prv', acm'@(Comorphism cid)) <-

lookupKnownConsChecker st

putStrLn ("Analyzing node for consistency " ++ ndnm)

putStrLn ("Using the comorphism " ++ language_name cid)

putStrLn ("Using consistency checker " ++ getCcName prv')

return $ case prepareForConsChecking st p_cm' of

Result _ Nothing -> Nothing

Result _ (Just sm) -> Just (sm, acm')

Result _ (Just sm) -> return $ Just (sm, acm)

case prep of

-- theory could not be computed

Nothing -> return "No suitable prover and comorphism found"

Just (G_theory_with_cons_checker _ th p, _) ->

case P.ccAutomatic p of

fn ->

do

let st' = st { proverRunning = True}

-- store initial input of the prover

let tLimit = show $ tsTimeLimit sTxt

swapMVar mSt $ Just $ Element st' nd

cstat <- fn (theoryName st)

(P.TacticScript tLimit)

th []

swapMVar mSt $ Just $ Element st nd

putStrLn $ case P.ccResult cstat of

Nothing -> "Timeout after " ++ tLimit ++ "seconds."

Just b -> "node " ++ ndnm ++ " is "

++ (if b then "" else "in") ++ "consistent."

ist <- readMVar miSt

case i_state ist of

Nothing -> return "no library"

Just iist -> case P.ccResult cstat of

Nothing -> return ""

Just b -> do

let le = i_libEnv iist

dg = lookupDGraph ln le

nl = labDG dg nd

nn = getDGNodeName nl

newDg0 = changeDGH dg $ SetNodeLab nl (nd,

markNodeConsistency

(if b then Cons else Inconsistent) "" nl)

newDg = groupHistory dg (DGRule "Consistency check") newDg0

nst = add2history

(CommentCmd $ "consistency check done on " ++ nn ++ "\n")

ist [DgCommandChange ln]

nwst = nst { i_state =

Just iist { i_libEnv = Map.insert ln newDg le } }

swapMVar miSt nwst

return ""

{- | Given a proofstatus the function does the actual call of the

prover for proving the node or check consistency -}

proveNode ::

-- use theorems is subsequent proofs

Bool ->

-- save problem file for each goal

Bool ->

-- Tactic script

ATPTacticScript ->

{- proofState of the node that needs proving

all theorems, goals and axioms should have

been selected before,but the theory should have

not beed recomputed -}

Int_NodeInfo ->

-- node name

String ->

{- selected prover, if non one will be automatically

selected -}

Maybe G_prover ->

{- selected comorphism, if non one will be automatically

selected -}

Maybe AnyComorphism ->

MVar (Maybe ThreadId) ->

MVar (Maybe Int_NodeInfo) ->

MVar IntState ->

LibName ->

-- returns an error message if anything happens

IO String

proveNode useTh save2File sTxt ndpf ndnm mp mcm mThr mSt miSt libname =

case ndpf of

Element pf_st nd ->

do

{- recompute the theory (to make effective the selected axioms,

goals) -}

let st = recalculateSublogicAndSelectedTheory pf_st

{- compute a prover,comorphism pair to be used in preparing

the theory -}

p_cm@(_, acm) <- case mcm of

Nothing -> lookupKnownProver st P.ProveCMDLautomatic

Just cm' -> case mp of

Nothing -> lookupKnownProver st P.ProveCMDLautomatic

Just p' -> return (p', cm')

-- try to prepare the theory

prep <- case prepareForProving st p_cm of

Result _ Nothing ->

do

p_cm'@(prv', acm'@(Comorphism cid)) <-

lookupKnownProver st P.ProveCMDLautomatic

putStrLn ("Analyzing node " ++ ndnm)

putStrLn ("Using the comorphism " ++ language_name cid)

putStrLn ("Using prover " ++ getProverName prv')

return $ case prepareForProving st p_cm' of

Result _ Nothing -> Nothing

Result _ (Just sm) -> Just (sm, acm')

Result _ (Just sm) -> return $ Just (sm, acm)

case prep of

-- theory could not be computed

Nothing -> return "No suitable prover and comorphism found"

Just (G_theory_with_prover lid1 th p, cmp) ->

case P.proveCMDLautomaticBatch p of

Nothing -> return "Error obtaining the prover"

Just fn ->

do

-- mVar to poll the prover for results

answ <- newMVar (return [])

let st' = st { proverRunning = True}

-- store initial input of the prover

swapMVar mSt $ Just $ Element st' nd

{- putStrLn ((theoryName st)++"\n"++

(showDoc sign "") ++

show (vsep (map (print_named lid1)

$ P.toNamedList sens))) -}

case selectedGoals st' of

[] -> return "No goals selected. Nothing to prove"

_ ->

do

putStrLn "selectedGoals:"

putStrLn $ unlines (selectedGoals st')

tmp <- fn useTh

save2File

answ

(theoryName st)

(P.TacticScript $ show sTxt)

th []

swapMVar mThr $ Just $ fst tmp

getResults lid1 cmp (snd tmp) answ mSt

swapMVar mThr Nothing

ist <- readMVar miSt

state <- readMVar mSt

case state of

Nothing -> return ""

Just state' ->

do

swapMVar mSt Nothing

swapMVar miSt $ addResults ist libname state'

return ""

disproveNode ::

-- Tactic script

ATPTacticScript ->

{- proofState of the node that needs proving

all theorems, goals and axioms should have

been selected before, but the theory should have

not been recomputed -}

Int_NodeInfo ->

-- node name

String ->

{- selected prover, if non one will be automatically

selected -}

Maybe G_cons_checker ->

{- selected comorphism, if non one will be automatically

selected -}

Maybe AnyComorphism ->

MVar (Maybe Int_NodeInfo) ->

MVar IntState ->

LibName ->

-- returns an error message if anything happens

IO String

disproveNode sTxt ndpf ndnm mp mcm mSt miSt ln =

case ndpf of

Element pf_st nd ->

do

{- recompute the theory (to make effective the selected axioms,

goals) !? needed? -}

let st = recalculateSublogicAndSelectedTheory pf_st

{- compute a prover,comorphism pair to be used in preparing

the theory -}

p_cm@(_, acm) <- case mcm of

Nothing -> lookupKnownConsChecker st

Just cm' -> case mp of

Nothing -> lookupKnownConsChecker st

Just p' -> return (p', cm')

-- try to prepare the theory

prep <- case prepareForConsChecking st p_cm of

Result _ Nothing ->

do

p_cm'@(prv', acm'@(Comorphism cid)) <-

lookupKnownConsChecker st

putStrLn ("Analyzing node for consistency " ++ ndnm)

putStrLn ("Using the comorphism " ++ language_name cid)

putStrLn ("Using consistency checker " ++ getCcName prv')

return $ case prepareForConsChecking st p_cm' of

Result _ Nothing -> Nothing

Result _ (Just sm) -> Just (sm, acm')

Result _ (Just sm) -> return $ Just (sm, acm)

case prep of

-- theory could not be computed

Nothing -> return "No suitable prover and comorphism found"

Just (theory@(G_theory_with_cons_checker l _ p), _) ->

case P.ccAutomatic p of

fn ->

do

let goals = selectedGoals st

let st' = st{ proverRunning = True }

negate_theory = negate_th_with_cons_checker theory

theories = map negate_theory goals

th_and_goals = zip theories goals

disprove_goal (theory',goal) =

case theory' of

Nothing -> return $ "Negating goal " ++ goal ++" failed"

Just (G_theory_with_cons_checker l2 th' _) ->

do

-- store initial input of the prover

let tLimit = show $ tsTimeLimit sTxt

th2 <- coerceTheoryMorphism l2 l "coerce error CMDL.ProveConsistency " th'

swapMVar mSt $ Just $ Element st' nd

cstat <- fn (theoryName st)

(P.TacticScript tLimit)

th2 []

swapMVar mSt $ Just $ Element st nd

putStrLn $ case P.ccResult cstat of

Nothing -> "Timeout after " ++ tLimit ++ "seconds."

Just b -> "node " ++ ndnm ++ " is "

++ (if b then "not " else "") ++ "disproved."

ist <- readMVar miSt

case i_state ist of

Nothing -> return $ "goal " ++ goal ++ ": no library"

Just iist -> case P.ccResult cstat of

Nothing -> return ""

Just b -> do

let le = i_libEnv iist

dg = lookupDGraph ln le

nl = labDG dg nd

nn = getDGNodeName nl

newDg0 = changeDGH dg $ SetNodeLab nl (nd,

markNodeConsistency

(if b then Cons else Inconsistent) "" nl)

newDg = groupHistory dg (DGRule "Consistency check") newDg0

nst = add2history

(CommentCmd $ "disprove at goal " ++ goal ++ ", node " ++ nn ++ "\n")

ist [DgCommandChange ln]

nwst = nst { i_state =

Just iist { i_libEnv = Map.insert ln newDg le } }

swapMVar miSt nwst

return ""

mapM_ (\x -> do y <- x

putStrLn y

return () ) $ map disprove_goal th_and_goals

return ""

getResults :: (Logic lid sublogics basic_spec sentence

symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree) =>

lid ->

AnyComorphism ->

MVar () ->

MVar (Result [P.ProofStatus proof_tree]) ->

MVar (Maybe Int_NodeInfo) ->

IO ()

getResults lid acm mStop mData mState =

do

takeMVar mStop

d <- takeMVar mData

case d of

Result _ Nothing -> return ()

Result _ (Just d') -> do

mapM_ (\ gs -> putStrLn $ "Goal " ++ P.goalName gs

++ " used " ++ unwords (P.usedAxioms gs))

$ filter P.isProvedStat d'

modifyMVar_ mState (\ s -> case s of

Nothing -> return s

Just (Element st node) -> return $ Just $ Element

(markProved acm lid d' st) node)

-- | inserts the results of the proof in the development graph

addResults :: IntState -> LibName -> Int_NodeInfo -> IntState

addResults ist libname ndps =

case i_state ist of

Nothing -> ist

Just pS ->

case ndps of

Element ps'' node -> let

dGraph = lookupDGraph libname (i_libEnv pS)

nl = labDG dGraph node

in fst $ updateNodeProof libname ist (node, nl)

$ currentTheory ps''

{- | Signal handler that stops the prover from running

when SIGINT is send -}

sigIntHandler :: MVar (Maybe ThreadId) ->

MVar IntState ->

MVar (Maybe Int_NodeInfo) ->

ThreadId ->

MVar IntState ->

LibName ->

IO ()

sigIntHandler mthr miSt mSt thr mOut libname =

do

{- print a message

? shellputStr ! should be used ! -}

putStrLn "Prover stopped."

-- check if the prover is runnig

tmp <- readMVar mthr

case tmp of

Nothing -> return ()

Just sm -> killThread sm

-- kill the prove/prove-all thread

killThread thr

-- update LibEnv with intermidiar results !?

ist <- readMVar miSt

st <- readMVar mSt

-- add to the output mvar results until now

putMVar mOut $ case st of

Nothing -> ist

Just st' -> addResults ist libname st'

return ()

doLoop :: MVar IntState

-> MVar (Maybe ThreadId)

-> MVar (Maybe Int_NodeInfo)

-> MVar IntState

-> [Int_NodeInfo]

-> Int

-> IO ()

doLoop miSt mThr mSt mOut ls checkCons = do

ist <- readMVar miSt

case i_state ist of

Nothing -> do

putMVar mOut ist

return ()

Just pS ->

case ls of

-- we are done

[] -> do

putMVar mOut ist

return ()

x : l -> do

let nodeName x' = case x' of

Element _ t -> case lookup t $ getAllNodes pS of

Nothing -> "Unkown node"

Just ll -> getDGNodeName ll

putStrLn ("Analyzing node " ++ nodeName x)

err <- if (checkCons == 1)

then checkNode (script pS)

x

(nodeName x)

(consChecker pS)

(cComorphism pS)

mSt

miSt

(i_ln pS)

else if (checkCons == 0) then proveNode (useTheorems pS)

(save2file pS)

(script pS)

x

(nodeName x)

(prover pS)

(cComorphism pS)

mThr

mSt

miSt

(i_ln pS)

else disproveNode (script pS)

x

(nodeName x)

(consChecker pS)

(cComorphism pS)

mSt

miSt

(i_ln pS)

unless (null err) (putStrLn err)

doLoop miSt mThr mSt mOut l checkCons