module Theory (
Axiom(..)
, axName
, axFormula
, LemmaAttribute(..)
, TraceQuantifier(..)
, Lemma
, lName
, lTraceQuantifier
, lFormula
, lAttributes
, lProof
, unprovenLemma
, skeletonLemma
, Theory(..)
, TheoryItem(..)
, thyName
, thySignature
, thyCache
, thyItems
, theoryRules
, theoryLemmas
, theoryAxioms
, addAxiom
, addLemma
, removeLemma
, lookupLemma
, addComment
, addStringComment
, addFormalComment
, cprRuleE
, OpenTheory
, defaultOpenTheory
, addProtoRule
, applyPartialEvaluation
, addIntrRuleACs
, normalizeTheory
, ClosedTheory
, ClosedRuleCache(..)
, closeTheory
, openTheory
, ClosedProtoRule(..)
, getLemmas
, getIntrVariants
, getProtoRuleEs
, getProofContext
, getClassifiedRules
, getInjectiveFactInsts
, getCaseDistinction
, ProofSkeleton
, proveTheory
, lookupLemmaProof
, modifyLemmaProof
, prettyFormalComment
, prettyLemmaName
, prettyAxiom
, prettyLemma
, prettyClosedTheory
, prettyOpenTheory
, prettyClosedSummary
, prettyIntruderVariants
, prettyTraceQuantifier
, module Theory.Model
, module Theory.Proof
) where
import Prelude hiding (id, (.))
import Data.Binary
import Data.DeriveTH
import Data.Foldable (Foldable, foldMap)
import Data.List
import Data.Maybe
import Data.Monoid (Sum(..))
import qualified Data.Set as S
import Data.Traversable (Traversable, traverse)
import Control.Basics
import Control.Category
import Control.DeepSeq
import Control.Monad.Reader
import qualified Control.Monad.State as MS
import Control.Parallel.Strategies
import Extension.Data.Label hiding (get)
import qualified Extension.Data.Label as L
import Theory.Model
import Theory.Proof
import Theory.Text.Pretty
import Theory.Tools.AbstractInterpretation
import Theory.Tools.InjectiveFactInstances
import Theory.Tools.LoopBreakers
import Theory.Tools.RuleVariants
type ProofSkeleton = Proof ()
skeletonToIncrementalProof :: ProofSkeleton -> IncrementalProof
skeletonToIncrementalProof = fmap (fmap (const Nothing))
incrementalToSkeletonProof :: IncrementalProof -> ProofSkeleton
incrementalToSkeletonProof = fmap (fmap (const ()))
type OpenProtoRule = ProtoRuleE
data ClosedProtoRule = ClosedProtoRule
{ _cprRuleE :: ProtoRuleE
, _cprRuleAC :: ProtoRuleAC
}
deriving( Eq, Ord, Show )
type OpenRuleCache = [IntrRuleAC]
data ClosedRuleCache = ClosedRuleCache
{ _crcRules :: ClassifiedRules
, _crcUntypedCaseDists :: [CaseDistinction]
, _crcTypedCaseDists :: [CaseDistinction]
, _crcInjectiveFactInsts :: S.Set FactTag
}
deriving( Eq, Ord, Show )
$(mkLabels [''ClosedProtoRule, ''ClosedRuleCache])
instance HasRuleName ClosedProtoRule where
ruleName = ruleName . L.get cprRuleE
intruderRules :: ClassifiedRules -> [IntrRuleAC]
intruderRules rules = do
Rule (IntrInfo i) ps cs as <- joinAllRules rules
return $ Rule i ps cs as
openRuleCache :: ClosedRuleCache -> OpenRuleCache
openRuleCache = intruderRules . L.get crcRules
openProtoRule :: ClosedProtoRule -> OpenProtoRule
openProtoRule = L.get cprRuleE
closeProtoRule :: MaudeHandle -> OpenProtoRule -> ClosedProtoRule
closeProtoRule hnd ruE = ClosedProtoRule ruE (variantsProtoRule hnd ruE)
closeRuleCache :: [LNGuarded]
-> [LNGuarded]
-> SignatureWithMaude
-> [ClosedProtoRule]
-> OpenRuleCache
-> ClosedRuleCache
closeRuleCache axioms typAsms sig protoRules intrRulesAC =
ClosedRuleCache
classifiedRules untypedCaseDists typedCaseDists injFactInstances
where
ctxt0 = ProofContext
sig classifiedRules injFactInstances UntypedCaseDist [] AvoidInduction
(error "closeRuleCache: trace quantifier should not matter here")
injFactInstances =
simpleInjectiveFactInstances $ L.get cprRuleE <$> protoRules
safetyAxioms = filter isSafetyFormula axioms
untypedCaseDists = precomputeCaseDistinctions ctxt0 safetyAxioms
typedCaseDists = refineWithTypingAsms typAsms ctxt0 untypedCaseDists
rulesAC = (fmap IntrInfo <$> intrRulesAC) <|>
((fmap ProtoInfo . L.get cprRuleAC) <$> protoRules)
anyOf ps = partition (\x -> any ($ x) ps)
(nonProto, proto) = anyOf [isDestrRule, isConstrRule] rulesAC
(constr, destr) = anyOf [isConstrRule] nonProto
classifiedRules = ClassifiedRules
{ _crConstruct = constr
, _crDestruct = destr
, _crProtocol = proto
}
data Axiom = Axiom
{ _axName :: String
, _axFormula :: LNFormula
}
deriving( Eq, Ord, Show )
$(mkLabels [''Axiom])
data LemmaAttribute =
TypingLemma
| ReuseLemma
| InvariantLemma
deriving( Eq, Ord, Show )
data TraceQuantifier = ExistsTrace | AllTraces
deriving( Eq, Ord, Show )
data Lemma p = Lemma
{ _lName :: String
, _lTraceQuantifier :: TraceQuantifier
, _lFormula :: LNFormula
, _lAttributes :: [LemmaAttribute]
, _lProof :: p
}
deriving( Eq, Ord, Show )
$(mkLabels [''Lemma])
instance Functor Lemma where
fmap f (Lemma n qua fm atts prf) = Lemma n qua fm atts (f prf)
instance Foldable Lemma where
foldMap f = f . L.get lProof
instance Traversable Lemma where
traverse f (Lemma n qua fm atts prf) = Lemma n qua fm atts <$> f prf
toSystemTraceQuantifier :: TraceQuantifier -> SystemTraceQuantifier
toSystemTraceQuantifier AllTraces = ExistsNoTrace
toSystemTraceQuantifier ExistsTrace = ExistsSomeTrace
isTypingLemma :: Lemma p -> Bool
isTypingLemma lem =
(AllTraces == L.get lTraceQuantifier lem)
&& (TypingLemma `elem` L.get lAttributes lem)
unprovenLemma :: String -> [LemmaAttribute] -> TraceQuantifier -> LNFormula
-> Lemma ProofSkeleton
unprovenLemma name atts qua fm = Lemma name qua fm atts (unproven ())
skeletonLemma :: String -> [LemmaAttribute] -> TraceQuantifier -> LNFormula
-> ProofSkeleton -> Lemma ProofSkeleton
skeletonLemma name atts qua fm = Lemma name qua fm atts
lemmaCaseDistKind :: Lemma p -> CaseDistKind
lemmaCaseDistKind lem
| TypingLemma `elem` L.get lAttributes lem = UntypedCaseDist
| otherwise = TypedCaseDist
type FormalComment = (String, String)
data TheoryItem r p =
RuleItem r
| LemmaItem (Lemma p)
| AxiomItem Axiom
| TextItem FormalComment
deriving( Show, Eq, Ord, Functor )
data Theory sig c r p = Theory {
_thyName :: String
, _thySignature :: sig
, _thyCache :: c
, _thyItems :: [TheoryItem r p]
}
deriving( Eq, Ord, Show )
$(mkLabels [''Theory])
type OpenTheory =
Theory SignaturePure [IntrRuleAC] OpenProtoRule ProofSkeleton
type ClosedTheory =
Theory SignatureWithMaude ClosedRuleCache ClosedProtoRule IncrementalProof
foldTheoryItem
:: (r -> a) -> (Axiom -> a) -> (Lemma p -> a) -> (FormalComment -> a)
-> TheoryItem r p -> a
foldTheoryItem fRule fAxiom fLemma fText i = case i of
RuleItem ru -> fRule ru
LemmaItem lem -> fLemma lem
TextItem txt -> fText txt
AxiomItem ax -> fAxiom ax
mapTheoryItem :: (r -> r') -> (p -> p') -> TheoryItem r p -> TheoryItem r' p'
mapTheoryItem f g =
foldTheoryItem (RuleItem . f) AxiomItem (LemmaItem . fmap g) TextItem
theoryRules :: Theory sig c r p -> [r]
theoryRules =
foldTheoryItem return (const []) (const []) (const []) <=< L.get thyItems
theoryAxioms :: Theory sig c r p -> [Axiom]
theoryAxioms =
foldTheoryItem (const []) return (const []) (const []) <=< L.get thyItems
theoryLemmas :: Theory sig c r p -> [Lemma p]
theoryLemmas =
foldTheoryItem (const []) (const []) return (const []) <=< L.get thyItems
addAxiom :: Axiom -> Theory sig c r p -> Maybe (Theory sig c r p)
addAxiom l thy = do
guard (isNothing $ lookupAxiom (L.get axName l) thy)
return $ modify thyItems (++ [AxiomItem l]) thy
addLemma :: Lemma p -> Theory sig c r p -> Maybe (Theory sig c r p)
addLemma l thy = do
guard (isNothing $ lookupLemma (L.get lName l) thy)
return $ modify thyItems (++ [LemmaItem l]) thy
removeLemma :: String -> Theory sig c r p -> Maybe (Theory sig c r p)
removeLemma lemmaName thy = do
_ <- lookupLemma lemmaName thy
return $ modify thyItems (concatMap fItem) thy
where
fItem = foldTheoryItem (return . RuleItem)
(return . AxiomItem)
check
(return . TextItem)
check l = do guard (L.get lName l /= lemmaName); return (LemmaItem l)
lookupAxiom :: String -> Theory sig c r p -> Maybe Axiom
lookupAxiom name = find ((name ==) . L.get axName) . theoryAxioms
lookupLemma :: String -> Theory sig c r p -> Maybe (Lemma p)
lookupLemma name = find ((name ==) . L.get lName) . theoryLemmas
addComment :: Doc -> Theory sig c r p -> Theory sig c r p
addComment c = modify thyItems (++ [TextItem ("", render c)])
addStringComment :: String -> Theory sig c r p -> Theory sig c r p
addStringComment = addComment . vcat . map text . lines
addFormalComment :: FormalComment -> Theory sig c r p -> Theory sig c r p
addFormalComment c = modify thyItems (++ [TextItem c])
defaultOpenTheory :: OpenTheory
defaultOpenTheory = Theory "default" emptySignaturePure [] []
openTheory :: ClosedTheory -> OpenTheory
openTheory (Theory n sig c items) =
Theory n (toSignaturePure sig) (openRuleCache c)
(map (mapTheoryItem openProtoRule incrementalToSkeletonProof) items)
lookupOpenProtoRule :: ProtoRuleName -> OpenTheory -> Maybe OpenProtoRule
lookupOpenProtoRule name =
find ((name ==) . L.get rInfo) . theoryRules
addProtoRule :: ProtoRuleE -> OpenTheory -> Maybe OpenTheory
addProtoRule ruE thy = do
guard nameNotUsedForDifferentRule
return $ modify thyItems (++ [RuleItem ruE]) thy
where
nameNotUsedForDifferentRule =
maybe True ((ruE ==)) $ lookupOpenProtoRule (L.get rInfo ruE) thy
addIntrRuleACs :: [IntrRuleAC] -> OpenTheory -> OpenTheory
addIntrRuleACs rs' = modify (thyCache) (\rs -> nub $ rs ++ rs')
normalizeTheory :: OpenTheory -> OpenTheory
normalizeTheory =
L.modify thyCache sort
. L.modify thyItems (\items -> do
item <- items
return $ case item of
LemmaItem lem ->
LemmaItem $ L.modify lProof stripProofAnnotations $ lem
RuleItem _ -> item
TextItem _ -> item
AxiomItem _ -> item)
where
stripProofAnnotations :: ProofSkeleton -> ProofSkeleton
stripProofAnnotations = fmap stripProofStepAnnotations
stripProofStepAnnotations (ProofStep method ()) =
ProofStep (case method of
Sorry _ -> Sorry Nothing
Contradiction _ -> Contradiction Nothing
_ -> method)
()
getLemmas :: ClosedTheory -> [Lemma IncrementalProof]
getLemmas = theoryLemmas
getIntrVariants :: ClosedTheory -> [IntrRuleAC]
getIntrVariants = intruderRules . L.get (crcRules . thyCache)
getProtoRuleEs :: ClosedTheory -> [ProtoRuleE]
getProtoRuleEs = map openProtoRule . theoryRules
getProofContext :: Lemma a -> ClosedTheory -> ProofContext
getProofContext l thy = ProofContext
( L.get thySignature thy)
( L.get (crcRules . thyCache) thy)
( L.get (crcInjectiveFactInsts . thyCache) thy)
kind
( L.get (cases . thyCache) thy)
inductionHint
(toSystemTraceQuantifier $ L.get lTraceQuantifier l)
where
kind = lemmaCaseDistKind l
cases = case kind of UntypedCaseDist -> crcUntypedCaseDists
TypedCaseDist -> crcTypedCaseDists
inductionHint
| any (`elem` [TypingLemma, InvariantLemma]) (L.get lAttributes l) = UseInduction
| otherwise = AvoidInduction
getInjectiveFactInsts :: ClosedTheory -> S.Set FactTag
getInjectiveFactInsts = L.get (crcInjectiveFactInsts . thyCache)
getClassifiedRules :: ClosedTheory -> ClassifiedRules
getClassifiedRules = L.get (crcRules . thyCache)
getCaseDistinction :: CaseDistKind -> ClosedTheory -> [CaseDistinction]
getCaseDistinction UntypedCaseDist = L.get (crcUntypedCaseDists . thyCache)
getCaseDistinction TypedCaseDist = L.get (crcTypedCaseDists . thyCache)
closeTheory :: FilePath
-> OpenTheory
-> IO ClosedTheory
closeTheory maudePath thy0 = do
sig <- toSignatureWithMaude maudePath $ L.get thySignature thy0
return $ closeTheoryWithMaude sig thy0
closeTheoryWithMaude :: SignatureWithMaude -> OpenTheory -> ClosedTheory
closeTheoryWithMaude sig thy0 = do
proveTheory (const True) checkProof
$ Theory (L.get thyName thy0) sig cache items
where
cache = closeRuleCache axioms typAsms sig rules (L.get thyCache thy0)
checkProof = checkAndExtendProver (sorryProver Nothing)
hnd = L.get sigmMaudeHandle sig
(items, _solveRel, _breakers) = (`runReader` hnd) $ addSolvingLoopBreakers
((closeTheoryItem <$> L.get thyItems thy0) `using` parList rdeepseq)
closeTheoryItem = foldTheoryItem
(RuleItem . closeProtoRule hnd)
AxiomItem
(LemmaItem . fmap skeletonToIncrementalProof)
TextItem
axioms = do AxiomItem ax <- items
return $ formulaToGuarded_ $ L.get axFormula ax
typAsms = do LemmaItem lem <- items
guard (isTypingLemma lem)
return $ formulaToGuarded_ $ L.get lFormula lem
rules = theoryRules (Theory errClose errClose errClose items)
errClose = error "closeTheory"
addSolvingLoopBreakers = useAutoLoopBreakersAC
(liftToItem $ enumPrems . L.get cprRuleAC)
(liftToItem $ enumConcs . L.get cprRuleAC)
(liftToItem $ getDisj . L.get (pracVariants . rInfo . cprRuleAC))
addBreakers
where
liftToItem f (RuleItem ru) = f ru
liftToItem _ _ = []
addBreakers bs (RuleItem ru) =
RuleItem (L.set (pracLoopBreakers . rInfo . cprRuleAC) bs ru)
addBreakers _ item = item
applyPartialEvaluation :: EvaluationStyle -> ClosedTheory -> ClosedTheory
applyPartialEvaluation evalStyle thy0 =
closeTheoryWithMaude sig $
L.modify thyItems replaceProtoRules (openTheory thy0)
where
sig = L.get thySignature thy0
ruEs = getProtoRuleEs thy0
(st', ruEs') = (`runReader` L.get sigmMaudeHandle sig) $
partialEvaluation evalStyle ruEs
replaceProtoRules [] = []
replaceProtoRules (item:items)
| isRuleItem item =
[ TextItem ("text", render ppAbsState)
] ++ map RuleItem ruEs' ++ filter (not . isRuleItem) items
| otherwise = item : replaceProtoRules items
isRuleItem (RuleItem _) = True
isRuleItem _ = False
ppAbsState =
(text $ " the abstract state after partial evaluation"
++ " contains " ++ show (S.size st') ++ " facts:") $--$
(numbered' $ map prettyLNFact $ S.toList st') $--$
(text $ "This abstract state results in " ++ show (length ruEs') ++
" refined multiset rewriting rules.\n" ++
"Note that the original number of multiset rewriting rules was "
++ show (length ruEs) ++ ".\n\n")
proveTheory :: (Lemma IncrementalProof -> Bool)
-> Prover
-> ClosedTheory
-> ClosedTheory
proveTheory selector prover thy =
modify thyItems ((`MS.evalState` []) . mapM prove) thy
where
prove item = case item of
LemmaItem l0 -> do l <- MS.gets (LemmaItem . proveLemma l0)
MS.modify (l :)
return l
_ -> do return item
proveLemma lem preItems
| selector lem = modify lProof add lem
| otherwise = lem
where
ctxt = getProofContext lem thy
sys = mkSystem ctxt (theoryAxioms thy) preItems $ L.get lFormula lem
add prf = fromMaybe prf $ runProver prover ctxt 0 sys prf
mkSystem :: ProofContext -> [Axiom] -> [TheoryItem r p]
-> LNFormula -> System
mkSystem ctxt axioms previousItems =
addLemmas
. formulaToSystem (map (formulaToGuarded_ . L.get axFormula) axioms)
(L.get pcCaseDistKind ctxt)
(L.get pcTraceQuantifier ctxt)
where
addLemmas sys =
insertLemmas (gatherReusableLemmas $ L.get sCaseDistKind sys) sys
gatherReusableLemmas kind = do
LemmaItem lem <- previousItems
guard $ lemmaCaseDistKind lem <= kind
&& ReuseLemma `elem` L.get lAttributes lem
&& AllTraces == L.get lTraceQuantifier lem
return $ formulaToGuarded_ $ L.get lFormula lem
type LemmaRef = String
lookupLemmaProof :: LemmaRef -> ClosedTheory -> Maybe IncrementalProof
lookupLemmaProof name thy = L.get lProof <$> lookupLemma name thy
modifyLemmaProof :: Prover -> LemmaRef -> ClosedTheory -> Maybe ClosedTheory
modifyLemmaProof prover name thy =
modA thyItems changeItems thy
where
findLemma (LemmaItem lem) = name == L.get lName lem
findLemma _ = False
change preItems (LemmaItem lem) = do
let ctxt = getProofContext lem thy
sys = mkSystem ctxt (theoryAxioms thy) preItems $ L.get lFormula lem
lem' <- modA lProof (runProver prover ctxt 0 sys) lem
return $ LemmaItem lem'
change _ _ = error "LemmaProof: change: impossible"
changeItems items = case break findLemma items of
(pre, i:post) -> do
i' <- change pre i
return $ pre ++ i':post
(_, []) -> Nothing
prettyFormalComment :: HighlightDocument d => String -> String -> d
prettyFormalComment "" body = multiComment_ [body]
prettyFormalComment header body = text $ header ++ "{*" ++ body ++ "*}"
prettyTheory :: HighlightDocument d
=> (sig -> d) -> (c -> d) -> (r -> d) -> (p -> d)
-> Theory sig c r p -> d
prettyTheory ppSig ppCache ppRule ppPrf thy = vsep $
[ kwTheoryHeader $ text $ L.get thyName thy
, lineComment_ "Function signature and definition of the equational theory E"
, ppSig $ L.get thySignature thy
, ppCache $ L.get thyCache thy
] ++
parMap rdeepseq ppItem (L.get thyItems thy) ++
[ kwEnd ]
where
ppItem = foldTheoryItem
ppRule prettyAxiom (prettyLemma ppPrf) (uncurry prettyFormalComment)
prettyLemmaName :: HighlightDocument d => Lemma p -> d
prettyLemmaName l = case L.get lAttributes l of
[] -> text (L.get lName l)
as -> text (L.get lName l) <->
(brackets $ fsep $ punctuate comma $ map prettyLemmaAttribute as)
where
prettyLemmaAttribute TypingLemma = text "typing"
prettyLemmaAttribute ReuseLemma = text "reuse"
prettyLemmaAttribute InvariantLemma = text "use_induction"
prettyAxiom :: HighlightDocument d => Axiom -> d
prettyAxiom ax =
kwAxiom <-> text (L.get axName ax) <> colon $-$
(nest 2 $ doubleQuotes $ prettyLNFormula $ L.get axFormula ax) $-$
(nest 2 $ if safety then lineComment_ "safety formula" else emptyDoc)
where
safety = isSafetyFormula $ formulaToGuarded_ $ L.get axFormula ax
prettyLemma :: HighlightDocument d => (p -> d) -> Lemma p -> d
prettyLemma ppPrf lem =
kwLemma <-> prettyLemmaName lem <> colon $-$
(nest 2 $
sep [ prettyTraceQuantifier $ L.get lTraceQuantifier lem
, doubleQuotes $ prettyLNFormula $ L.get lFormula lem
]
)
$-$
ppLNFormulaGuarded (L.get lFormula lem)
$-$
ppPrf (L.get lProof lem)
where
ppLNFormulaGuarded fm = case formulaToGuarded fm of
Left err -> multiComment $
text "conversion to guarded formula failed:" $$
nest 2 err
Right gf -> case toSystemTraceQuantifier $ L.get lTraceQuantifier lem of
ExistsNoTrace -> multiComment
( text "guarded formula characterizing all counter-examples:" $-$
doubleQuotes (prettyGuarded (gnot gf)) )
ExistsSomeTrace -> multiComment
( text "guarded formula characterizing all satisfying traces:" $-$
doubleQuotes (prettyGuarded gf) )
prettyIntruderVariants :: HighlightDocument d => [IntrRuleAC] -> d
prettyIntruderVariants vs = vcat . intersperse (text "") $ map prettyIntrRuleAC vs
prettyOpenProtoRule :: HighlightDocument d => OpenProtoRule -> d
prettyOpenProtoRule = prettyProtoRuleE
prettyIncrementalProof :: HighlightDocument d => IncrementalProof -> d
prettyIncrementalProof = prettyProofWith ppStep (const id)
where
ppStep step = sep
[ prettyProofMethod (psMethod step)
, if isNothing (psInfo step) then multiComment_ ["unannotated"]
else emptyDoc
]
prettyClosedProtoRule :: HighlightDocument d => ClosedProtoRule -> d
prettyClosedProtoRule cru =
(prettyProtoRuleE ruE) $--$
(nest 2 $ prettyLoopBreakers (L.get rInfo ruAC) $-$ ppRuleAC)
where
ruAC = L.get cprRuleAC cru
ruE = L.get cprRuleE cru
ppRuleAC
| isTrivialProtoVariantAC ruAC ruE = multiComment_ ["has exactly the trivial AC variant"]
| otherwise = multiComment $ prettyProtoRuleAC ruAC
prettyOpenTheory :: HighlightDocument d => OpenTheory -> d
prettyOpenTheory =
prettyTheory prettySignaturePure
(const emptyDoc) prettyOpenProtoRule prettyProof
prettyClosedTheory :: HighlightDocument d => ClosedTheory -> d
prettyClosedTheory thy =
prettyTheory prettySignatureWithMaude
ppInjectiveFactInsts
prettyClosedProtoRule
prettyIncrementalProof
thy
where
ppInjectiveFactInsts crc =
case S.toList $ L.get crcInjectiveFactInsts crc of
[] -> emptyDoc
tags -> lineComment $ sep
[ text "looping facts with injective instances:"
, nest 2 $ fsepList (text . showFactTagArity) tags ]
prettyClosedSummary :: Document d => ClosedTheory -> d
prettyClosedSummary thy =
vcat lemmaSummaries
where
lemmaSummaries = do
LemmaItem lem <- L.get thyItems thy
let (status, Sum siz) = foldProof proofStepSummary $ L.get lProof lem
quantifier = (toSystemTraceQuantifier $ L.get lTraceQuantifier lem)
analysisType = parens $ prettyTraceQuantifier $ L.get lTraceQuantifier lem
return $ text (L.get lName lem) <-> analysisType <> colon <->
text (showProofStatus quantifier status) <->
parens (integer siz <-> text "steps")
proofStepSummary = proofStepStatus &&& const (Sum (1::Integer))
prettyTraceQuantifier :: Document d => TraceQuantifier -> d
prettyTraceQuantifier ExistsTrace = text "exists-trace"
prettyTraceQuantifier AllTraces = text "all-traces"
$( derive makeBinary ''TheoryItem)
$( derive makeBinary ''LemmaAttribute)
$( derive makeBinary ''TraceQuantifier)
$( derive makeBinary ''Axiom)
$( derive makeBinary ''Lemma)
$( derive makeBinary ''ClosedProtoRule)
$( derive makeBinary ''ClosedRuleCache)
$( derive makeBinary ''Theory)
$( derive makeNFData ''TheoryItem)
$( derive makeNFData ''LemmaAttribute)
$( derive makeNFData ''TraceQuantifier)
$( derive makeNFData ''Axiom)
$( derive makeNFData ''Lemma)
$( derive makeNFData ''ClosedProtoRule)
$( derive makeNFData ''ClosedRuleCache)
$( derive makeNFData ''Theory)