module Theory.Tools.Wellformedness (
WfErrorReport
, checkWellformedness
, noteWellformedness
, prettyWfErrorReport
) where
import Prelude hiding (id, (.))
import Control.Basics
import Control.Category
import Data.Char
import Data.Generics.Uniplate.Data (universeBi)
import Data.Label
import Data.List
import Data.Maybe
import Data.Monoid (mappend, mempty)
import qualified Data.Set as S
import Data.Traversable (traverse)
import Control.Monad.Bind
import Extension.Prelude
import Term.LTerm
import Term.Maude.Signature
import Theory
import Theory.Text.Pretty
type Topic = String
type WfError = (Topic, Doc)
type WfErrorReport = [WfError]
prettyWfErrorReport :: WfErrorReport -> Doc
prettyWfErrorReport =
vcat . intersperse (text "") . map ppTopic . groupOn fst
where
ppTopic [] = error "prettyWfErrorReport: groupOn returned empty list"
ppTopic errs@((topic,_):_) =
text topic <> colon $-$
(nest 2 . vcat . intersperse (text "") $ map snd errs)
thyProtoRules :: OpenTheory -> [ProtoRuleE]
thyProtoRules thy = [ ru | RuleItem ru <- get thyItems thy ]
lowerCase :: String -> String
lowerCase = map toLower
prettyVarList :: Document d => [LVar] -> d
prettyVarList = fsep . punctuate comma . map prettyLVar
prettyLNTermList :: Document d => [LNTerm] -> d
prettyLNTermList = fsep . punctuate comma . map prettyLNTerm
wrappedText :: Document d => String -> d
wrappedText = fsep . map text . words
clashesOn :: (Ord b, Ord c)
=> (a -> b)
-> (a -> c)
-> [a] -> [[a]]
clashesOn f g xs = do
grp <- groupOn f $ sortOn f xs
guard (length (sortednubOn g grp) >= 2)
return grp
quote :: String -> String
quote cs = '`' : cs ++ "'"
sortsClashCheck :: HasFrees t => String -> t -> WfErrorReport
sortsClashCheck info t = case clashesOn removeSort id $ frees t of
[] -> []
cs -> return $
( "sorts"
, text info $-$ (nest 2 $ numbered' $ map prettyVarList cs)
)
where
removeSort lv = (lowerCase (lvarName lv), lvarIdx lv)
ruleSortsReport :: OpenTheory -> WfErrorReport
ruleSortsReport thy = do
ru <- thyProtoRules thy
sortsClashCheck ("rule " ++ quote (showRuleCaseName ru) ++
" clashing sorts, casings, or multiplicities:") ru
freshNamesReport :: OpenTheory -> WfErrorReport
freshNamesReport thy = do
ru <- thyProtoRules thy
case filter ((LSortFresh ==) . sortOfName) $ universeBi ru of
[] -> []
names -> return $ (,) "fresh names" $ fsep $
text ( "rule " ++ quote (showRuleCaseName ru) ++ ": " ++
"fresh names are not allowed in rule:" )
: punctuate comma (map (nest 2 . text . show) names)
publicNamesReport :: OpenTheory -> WfErrorReport
publicNamesReport thy =
case findClashes publicNames of
[] -> []
clashes -> return $ (,) topic $ numbered' $
map (nest 2 . fsep . punctuate comma . map ppRuleAndName) clashes
where
topic = "public names with mismatching capitalization"
publicNames = do
ru <- thyProtoRules thy
(,) (showRuleCaseName ru) <$>
(filter ((LSortPub ==) . sortOfName) $ universeBi ru)
findClashes = clashesOn (map toLower . show . snd) (show . snd)
ppRuleAndName (ruName, pub) =
text $ "rule " ++ show ruName ++ " name " ++ show pub
unboundCheck :: HasFrees i => String -> Rule i -> WfErrorReport
unboundCheck info ru
| null unboundVars = []
| otherwise = return $
( "unbound"
, text info $-$ (nest 2 $ prettyVarList unboundVars) )
where
boundVars = S.fromList $ frees (get rPrems ru)
unboundVars = do
v <- frees (get rConcs ru, get rActs ru, get rInfo ru)
guard $ not (lvarSort v == LSortPub || v `S.member` boundVars)
return v
unboundReport :: OpenTheory -> WfErrorReport
unboundReport thy = do
RuleItem ru <- get thyItems thy
unboundCheck ("rule " ++ quote (showRuleCaseName ru) ++
" has unbound variables: "
) ru
factReports :: OpenTheory -> WfErrorReport
factReports thy = concat
[ reservedReport, freshFactArguments, specialFactsUsage
, factUsage, inexistentActions
]
where
ruleFacts ru =
( "rule " ++ quote (showRuleCaseName ru)
, extFactInfo <$> concatMap (`get` ru) [rPrems, rActs, rConcs])
theoryFacts =
do ruleFacts <$> get thyCache thy
<|> do RuleItem ru <- get thyItems thy
return $ ruleFacts ru
<|> do LemmaItem l <- get thyItems thy
return $ (,) ("lemma " ++ quote (get lName l)) $ do
fa <- formulaFacts (get lFormula l)
return $ (text (show fa), factInfo fa)
extFactInfo fa = (prettyLNFact fa, factInfo fa)
factInfo :: Fact t -> (FactTag, Int, Multiplicity)
factInfo fa = (factTag fa, factArity fa, factMultiplicity fa)
reservedReport = do
(origin, fas) <- theoryFacts
case mapMaybe reservedFactName fas of
[] -> []
errs -> return $ (,) "reseved names" $ foldr1 ($--$) $
wrappedText ("The " ++ origin ++
" contains facts with reserved names:")
: map (nest 2) errs
reservedFactName (ppFa, info@(ProtoFact _ name _, _,_))
| map toLower name `elem` ["fr","ku","kd","out","in"] =
return $ ppFa $-$ text ("show:" ++ show info)
reservedFactName _ = Nothing
freshFactArguments = do
ru <- thyProtoRules thy
fa@(Fact FreshFact [m]) <- get rPrems ru
guard (not (isMsgVar m || isFreshVar m))
return $ (,) "Fr facts must only use a fresh- or a msg-variable" $
text ("rule " ++ quote (showRuleCaseName ru)) <->
text "fact:" <-> prettyLNFact fa
specialFactsUsage = do
ru <- thyProtoRules thy
let lhs = [ fa | fa <- get rPrems ru
, factTag fa `elem` [KUFact, KDFact, OutFact] ]
rhs = [ fa | fa <- get rConcs ru
, factTag fa `elem` [FreshFact, KUFact, KDFact, InFact] ]
check _ [] = mzero
check msg fas = return $ (,) "special fact usage" $
text ("rule " ++ quote (showRuleCaseName ru)) <-> text msg $-$
(nest 2 $ fsep $ punctuate comma $ map prettyLNFact fas)
msum [ check "uses disallowed facts on left-hand-side:" lhs
, check "uses disallowed facts on right-hand-side:" rhs ]
factUsage = do
clash <- clashesOn factIdentifier (snd . snd) theoryFacts'
return $ (,) "fact usage" $ numbered' $ do
(origin, (ppFa, info@(tag, _, _))) <- clash
return $ text (origin ++
", fact " ++ show (map toLower $ factTagName tag) ++
": " ++ showInfo info)
$-$ nest 2 ppFa
where
showInfo (tag, k, multipl) = show $ (showFactTag tag, k, multipl)
theoryFacts' = [ (ru, fa) | (ru, fas) <- theoryFacts, fa <- fas ]
factIdentifier (_, (_, (tag, _, _))) = map toLower $ factTagName tag
ruleActions = S.fromList $ map factInfo $
kLogFact undefined
: dedLogFact undefined
: kuFact undefined
: (do RuleItem ru <- get thyItems thy; get rActs ru)
inexistentActions = do
LemmaItem l <- get thyItems thy
fa <- sortednub $ formulaFacts (get lFormula l)
let info = factInfo fa
name = get lName l
if info `S.member` ruleActions
then []
else return $ (,) "lemma actions" $
text ("lemma " ++ quote name ++ " references action ") $-$
nest 2 (text $ show info) $-$
text "but no rule has such an action."
formulaFacts :: Formula s c v -> [Fact (VTerm c (BVar v))]
formulaFacts =
foldFormula atomFacts
(const mempty)
id
(const mappend) (const $ const id)
where
atomFacts (Action _ fa) = [fa]
atomFacts (EqE _ _) = mempty
atomFacts (Less _ _) = mempty
atomFacts (Last _) = mempty
formulaTerms :: Formula s c v -> [VTerm c (BVar v)]
formulaTerms =
foldFormula atomTerms (const mempty) id (const mappend) (const $ const id)
where
atomTerms (Action i fa) = i : factTerms fa
atomTerms (EqE t s) = [t, s]
atomTerms (Less i j) = [i, j]
atomTerms (Last i) = [i]
lemmaAttributeReport :: OpenTheory -> WfErrorReport
lemmaAttributeReport thy = do
lem <- theoryLemmas thy
guard $ get lTraceQuantifier lem == ExistsTrace
&& ReuseLemma `elem` get lAttributes lem
return ( "attributes"
, text "lemma" <-> (text $ quote $ get lName lem) <> colon <->
text "cannot reuse 'exists-trace' lemmas"
)
formulaReports :: OpenTheory -> WfErrorReport
formulaReports thy = do
(header, fm) <- annFormulas
msum [ ((,) "quantifier sorts") <$> checkQuantifiers header fm
, ((,) "formula terms") <$> checkTerms header fm
, ((,) "guardedness") <$> checkGuarded header fm
]
where
annFormulas = do LemmaItem l <- get thyItems thy
let header = "lemma " ++ quote (get lName l)
fm = get lFormula l
return (header, fm)
<|> do AxiomItem ax <- get thyItems thy
let header = "axiom " ++ quote (get axName ax)
fm = get axFormula ax
return (header, fm)
checkQuantifiers header fm
| null disallowed = []
| otherwise = return $ fsep $
(text $ header ++ "uses quantifiers with wrong sort:") :
(punctuate comma $ map (nest 2 . text . show) disallowed)
where
binders = foldFormula (const mempty) (const mempty) id (const mappend)
(\_ binder rest -> binder : rest) fm
disallowed = filter (not . (`elem` [LSortMsg, LSortNode]) . snd) binders
checkTerms header fm
| null offenders = []
| otherwise = return $
(fsep $
(text $ header ++ " uses terms of the wrong form:") :
(punctuate comma $ map (nest 2 . text . quote . show) offenders)
) $--$
wrappedText
"The only allowed terms are public names and bound node and message\
\ variables. If you encounter free message variables, then you might\
\ have forgotten a #-prefix. Sort prefixes can only be dropped where\
\ this is unambiguous."
where
irreducible = irreducibleFunSyms $ get (sigpMaudeSig . thySignature) thy
offenders = filter (not . allowed) $ formulaTerms fm
allowed (viewTerm -> Lit (Var (Bound _))) = True
allowed (viewTerm -> Lit (Con (Name PubName _))) = True
allowed (viewTerm2 -> FUnion args) = all allowed args
allowed (viewTerm -> FApp o args) | o `S.member` irreducible = all allowed args
allowed _ = False
checkGuarded header fm = case formulaToGuarded fm of
Left err -> return $
text (header ++ " cannot be converted to a guarded formula:") $-$
nest 2 err
Right _ -> []
multRestrictedReport :: OpenTheory -> WfErrorReport
multRestrictedReport thy = do
ru <- theoryRules thy
(,) "multiplication restriction of rules" <$>
case restrictedFailures ru of
([],[]) -> []
(mults, unbounds) ->
return $
(text "The following rule is not multiplication restricted:")
$-$ (nest 2 (prettyProtoRuleE ru))
$-$ (text "")
$-$ (text "After replacing reducible function symbols in lhs with variables:")
$-$ (nest 2 $ prettyProtoRuleE (abstractRule ru))
$-$ (text "")
$-$ (if null mults then mempty
else nest 2 $ (text "Terms with multiplication: ") <-> (prettyLNTermList mults))
$-$ (if null unbounds then mempty
else nest 2 $ (text "Variables that occur only in rhs: ") <-> (prettyVarList unbounds))
where
abstractRule ru@(Rule i lhs acts rhs) =
(`evalFreshAvoiding` ru) . (`evalBindT` noBindings) $ do
Rule i <$> mapM (traverse abstractTerm) lhs
<*> mapM (traverse replaceAbstracted) acts
<*> mapM (traverse replaceAbstracted) rhs
abstractTerm (viewTerm -> FApp o args) | o `S.member` irreducible =
fApp o <$> mapM abstractTerm args
abstractTerm (viewTerm -> Lit l) = return $ lit l
abstractTerm t = varTerm <$> importBinding (`LVar` sortOfLNTerm t) t "x"
replaceAbstracted t = do
b <- lookupBinding t
case b of
Just v -> return $ varTerm v
Nothing ->
case viewTerm t of
FApp o args ->
fApp o <$> mapM replaceAbstracted args
Lit l -> return $ lit l
restrictedFailures ru = (mults, unbound ruAbstr \\ unbound ru)
where
ruAbstr = abstractRule ru
mults = [ mt | Fact _ ts <- get rConcs ru, t <- ts, mt <- multTerms t ]
multTerms t@(viewTerm -> FApp (AC Mult) _) = [t]
multTerms (viewTerm -> FApp _ as) = concatMap multTerms as
multTerms _ = []
unbound ru = [v | v <- frees (get rConcs ru) \\ frees (get rPrems ru)
, lvarSort v /= LSortPub ]
irreducible = irreducibleFunSyms $ get (sigpMaudeSig . thySignature) thy
checkWellformedness :: OpenTheory
-> WfErrorReport
checkWellformedness thy = concatMap ($ thy)
[ unboundReport
, freshNamesReport
, publicNamesReport
, ruleSortsReport
, factReports
, formulaReports
, lemmaAttributeReport
, multRestrictedReport
]
noteWellformedness :: WfErrorReport -> OpenTheory -> OpenTheory
noteWellformedness report thy =
addComment wfErrorReport thy
where
wfErrorReport
| null report = text "All well-formedness checks were successful."
| otherwise = vsep
[ text "WARNING: the following wellformedness checks failed!"
, prettyWfErrorReport report
]