module Scyther.Theory (
Theorem
, thmProto
, thmName
, thmSequent
, thmProof
, isAxiom
, ThyItem(..)
, Theory(..)
, adaptTheoryName
, insertItem
, shrinkTheory
, proveSequents
, mapTheorySequents
, addMissingTypingInvariants
, ensureUniqueRoleNames
, composeParallel
, lookupProtocol
, unsoundTheorems
, theoryProofSize
, theoryOverview
, classifyProperties
) where
import Safe
import Data.Either (partitionEithers)
import Data.Monoid
import Data.List (isPrefixOf)
import qualified Data.Set as S
import qualified Data.Map as M
import Data.DAG.Simple
import Data.Data
import Data.Generics.Uniplate.Data
import Control.Monad
import Control.Monad.State
import System.FilePath
import Extension.Prelude
import Scyther.Facts
import Scyther.Sequent
import Scyther.Proof
type Theorem = Named Proof
thmName :: Theorem -> String
thmName = fst
thmProof :: Theorem -> Proof
thmProof = snd
thmSequent :: Theorem -> Sequent
thmSequent = prfSequent . thmProof
thmProto :: Theorem -> Protocol
thmProto = prfProto . thmProof
isAxiom :: Theorem -> Bool
isAxiom = isAxiomProof . snd
data ThyItem =
ThyProtocol Protocol
| ThySequent (Named Sequent)
| ThyTheorem (Named Proof)
| ThyText String
deriving( Eq, Show, Data, Typeable )
data Theory = Theory {
thyName :: String
, thyItems :: [ThyItem]
}
deriving( Eq, Show, Data, Typeable )
mapTheoryItems :: ([ThyItem] -> [ThyItem]) -> Theory -> Theory
mapTheoryItems f (Theory name items) = Theory name (f items)
mapTheorySequents :: (Sequent -> Sequent) -> Theory -> Theory
mapTheorySequents f = mapTheoryItems (map mapThyItemSequents)
where
mapThyItemSequents item = case item of
ThySequent (name, se) -> ThySequent (name, f se)
ThyTheorem (name, prf) -> ThyTheorem (name, mapProofSequents f prf)
ThyProtocol _ -> item
ThyText _ -> item
insertItem :: ThyItem -> Theory -> Theory
insertItem item thy = thy { thyItems = thyItems thy ++ [item] }
addMissingTypingInvariants :: Theory -> Theory
addMissingTypingInvariants thy =
Theory (thyName thy) (concatMap add $ thyItems thy)
where
mkTypingSequent p = case mscTyping p of
Just typ -> return $ ThySequent ( protoName p ++ "_msc_typing"
, Sequent (empty p) (FAtom (ATyping typ)))
Nothing -> mzero
add item = case item of
ThyProtocol p
| noTypingInvariant p -> [item] ++ mkTypingSequent p
_ -> [item]
noTypingInvariant p = and $ do
item <- thyItems thy
se <- case item of
ThySequent (_, se) -> return se
ThyTheorem (_, prf) -> return (prfSequent prf)
_ -> mzero
guard (isTypingFormula $ seConcl se)
return (p /= seProto se)
proveSequents :: (Sequent -> Theorem -> Bool)
-> ([Named Sequent] -> Sequent -> Maybe Proof)
-> Theory -> Theory
proveSequents reuse prover thy =
Theory (thyName thy) (flip execState [] . mapM_ prove $ thyItems thy)
where
prove (item@(ThySequent (name, se))) = do
prevItems <- get
let reusableThms = [ (thmName th, thmSequent th)
| ThyTheorem th <- prevItems, reuse se th, thmProto th == seProto se]
case prover reusableThms se of
Just prf -> modify (++[ThyTheorem (name, prf)])
Nothing -> modify (++[item])
prove item = modify (++[item])
shrinkTheory :: (String -> Bool) -> Theory -> Theory
shrinkTheory mustKeep (Theory name items) =
Theory name (filter keep items)
where
thmInfo thm = (thmName thm, thmProto thm)
kept = [ thmInfo thm | ThyTheorem thm <- items, mustKeep $ thmName thm ]
dependencies =
[ (thmInfo thm, dep)
| ThyTheorem thm <- items, dep <- S.toList . depends $ thmProof thm ]
toKeep = reachableSet kept dependencies
keep :: ThyItem -> Bool
keep (ThyTheorem thm) = (thmInfo thm `S.member` toKeep)
keep (ThySequent se) = mustKeep $ fst se
keep _ = True
adaptTheoryName :: FilePath -> Theory -> Theory
adaptTheoryName file thy = thy { thyName = takeBaseName file }
ensureUniqueRoleNames :: Theory -> Theory
ensureUniqueRoleNames thy
| unique rs = thy
| otherwise = mapTheoryItems (map addPrefix) thy
where
rs = [roleName r | ThyProtocol p <- thyItems thy, r <- protoRoles p]
prefixRoleName p r = r {roleName = protoName p ++ "_" ++ roleName r}
getProtocol (ThyProtocol p) = return p
getProtocol (ThySequent s) = return (seProto $ snd s)
getProtocol (ThyTheorem p) = return (thmProto p)
getProtocol (ThyText _) = mzero
addPrefix item = case getProtocol item of
Just p -> transformBi (prefixRoleName p) item
Nothing -> item
composeParallel :: Theory -> Theory
composeParallel thy
| length ps <= 1 = thy
| otherwise = thy { thyItems = [ThyProtocol pc, ThySequent sec] ++ items3 }
where
(ps, items1) = partitionEithers $ do
item <- thyItems thy
case item of
ThyProtocol p -> return $ Left p
_ -> return $ Right item
(typs, items2) = partitionEithers $ do
item <- items1
case item of
ThySequent (_, Sequent _ (FAtom (ATyping (Typing typ))))
-> return $ Left typ
ThySequent x -> return $ Right $ ThySequent $ prefixProtoName (seProto $ snd x) x
ThyTheorem x -> return $ Right $ ThyTheorem $ prefixProtoName (thmProto x) x
_ -> return $ Right item
prefixProtoName :: Protocol -> (String, a) -> (String, a)
prefixProtoName p x@(n, v)
| protoName p `isPrefixOf` n = x
| otherwise = (protoName p ++ "_" ++ n, v)
namec = thyName thy
pc = Protocol namec (concatMap protoRoles ps)
sec = ( namec ++ "_composed_typing"
, Sequent (empty pc) (FAtom (ATyping (Typing (M.unions typs))))
)
replaceProtocol :: Protocol -> Protocol
replaceProtocol = const pc
items3 = transformBi replaceProtocol items2
lookupProtocol :: String -> Theory -> Maybe Protocol
lookupProtocol name thy =
headMay [proto | ThyProtocol proto <- thyItems thy, protoName proto == name]
unsoundTheorems :: Theory -> [(Protocol, String)]
unsoundTheorems (Theory _ items) =
[ (prfProto prf, name)
| ThyTheorem (name, prf) <- items, not (sound prf)
] ++
[ (seProto se, name)
| ThySequent (name, se) <- items
]
theoryProofSize :: Theory -> ProofSize
theoryProofSize (Theory _ items) = mconcat $
[ proofSize (thmProof th) | ThyTheorem th <- items ] ++
[ missingProofSize | ThySequent _ <- items ]
classifyProperties :: (String -> Bool) -> Theory -> (Int, Int, Int)
classifyProperties toClassify = foldl classify (0,0,0) . thyItems
where
getSequent (ThyTheorem thm) = do
guard (toClassify $ thmName thm)
return $ thmSequent thm
getSequent (ThySequent se) = do
guard (toClassify (fst se))
return (snd se)
getSequent _ = mzero
classify counts@(nSec, nAuth, nOther) item = case getSequent item of
Just se | isContradictionProp se -> (succ nSec, nAuth, nOther)
Just se | isExistsStructureProp se -> ( nSec, succ nAuth, nOther)
Just _ -> ( nSec, nAuth, succ nOther)
Nothing -> counts
isContradictionProp :: Sequent -> Bool
isContradictionProp = (FAtom AFalse ==) . seConcl
isExistsStructureProp :: Sequent -> Bool
isExistsStructureProp = hasQuantifiers . seConcl
theoryOverview :: Theory -> Theory
theoryOverview = error "theoryOverview: upgrade to new infrastructure"