{- |

Module : ./CMDL/ProveConsistency.hs

Description : CMDL interface commands

Copyright : uni-bremen and DFKI

License : GPLv2 or higher, see LICENSE.txt

Maintainer : r.pascanu@jacobs-university.de

Stability : provisional

Portability : portable

CMDL.ProveConsistency contains prove and consistency check command

-}

module CMDL.ProveConsistency

( cProver

, cConsChecker

, doLoop

, sigIntHandler

) where

import Interfaces.Command

import Interfaces.DataTypes

import Interfaces.GenericATPState (ATPTacticScript (..))

import Interfaces.History

import Interfaces.Utils

import CMDL.DataTypes (CmdlState (intState), ProveCmdType (..))

import CMDL.DataTypesUtils

import Comorphisms.LogicGraph (logicGraph)

import Proofs.AbstractState

import Static.DevGraph

import Static.DgUtils

import Static.History

import Common.DocUtils

import Logic.Comorphism

import Logic.Grothendieck

import Logic.Logic

import Logic.Prover as P

import Logic.Coerce

import Common.Consistency

import Common.LibName (LibName)

import Common.Result (Result (Result))

import Common.Utils (trim)

import qualified Common.OrderedMap as OMap

import Common.AS_Annotation

import Data.List

import qualified Data.Map as Map

import Control.Concurrent (ThreadId, killThread)

import Control.Concurrent.MVar (MVar, newMVar, putMVar, takeMVar, readMVar,

swapMVar, modifyMVar_)

import Control.Monad

import Data.Foldable (forM_)

negate_th_with_cons_checker :: G_theory_with_cons_checker -> String ->

Maybe G_theory_with_cons_checker

negate_th_with_cons_checker g_th goal = case g_th of

G_theory_with_cons_checker lid1 th cons_check ->

case P.tTarget th of

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

Nothing -> Nothing

Just sen -> case negation lid1 $ sentence sen of

Nothing -> Nothing

Just sen' -> let

negSen = sen { sentence = sen',

isAxiom = True }

sens' = OMap.insert goal negSen $

OMap.filter isAxiom sens

target' = P.Theory lid2 sens'

in Just $ G_theory_with_cons_checker lid1 th

{P.tTarget = target'} cons_check

getProversAutomatic :: G_sublogics -> IO [(G_prover, AnyComorphism)]

getProversAutomatic sl = getUsableProvers P.ProveCMDLautomatic sl logicGraph

-- | Select a prover

cProver :: String -> CmdlState -> IO CmdlState

cProver 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

prov <- getProversAutomatic (sublogicOfTheory z)

let pl = filter ((== inp) . getProverName . fst) prov

prover_names = map (getProverName . fst) prov

case case cComorphism pS of

Nothing -> pl

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

[] -> if inp == "" then do

mapM_ putStrLn (nub prover_names)

return state

else return (genMsgAndCode

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

state)

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

return $ add2hist [ ProverChange $ prover pS

, CComorphismChange $ cComorphism pS ]

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

++ language_name cid ++ "`")

state {

intState = (intState state) {

i_state = Just pS

{ cComorphism = Just nCm

, prover = Just p } } }

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

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 -> do

cs <- getConsCheckers [x]

case find (\ (y, _) -> getCcName y == inp) cs 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

if showOutput iist then

do

putStrLn "____________________________"

print $ P.ccProofTree cstat

putStrLn "____________________________"

else putStr ""

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 th

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

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 -> "goal " ++ goal ++ " is "

++ (if b then "" else "not ") ++ "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 () ) . 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, Pretty sentence) =>

lid ->

AnyComorphism ->

MVar () ->

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

MVar (Maybe Int_NodeInfo) ->

P.Theory sign sentence proof_tree ->

IO ()

getResults lid acm mStop mData mState (P.Theory _ sensMap) =

do

takeMVar mStop

d <- takeMVar mData

case d of

Result _ Nothing -> return ()

Result _ (Just d') -> do

mapM_ (\ gs -> let

uAx = map

(\x -> let ax = case OMap.lookup x sensMap of

Nothing -> error "Proof using a missing axiom"

Just s -> show $ pretty $ sentence s

in x ++" : " ++ ax ++ "\n") $

P.usedAxioms gs

in

putStrLn $ "Goal " ++ P.goalName gs

++ " used \n" ++ unwords uAx)

$ 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

Data.Foldable.forM_ tmp killThread

-- 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]

-> ProveCmdType

-> IO ()

doLoop miSt mThr mSt mOut ls proveCmdType = 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 <- case proveCmdType of

ConsCheck -> checkNode (script pS)

x

(nodeName x)

(consChecker pS)

(cComorphism pS)

mSt

miSt

(i_ln pS)

Prove -> proveNode (useTheorems pS)

(save2file pS)

(script pS)

x

(nodeName x)

(prover pS)

(cComorphism pS)

mThr

mSt

miSt

(i_ln pS)

Disprove -> 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 proveCmdType