module Theory.Constraint.Solver.Goals (
Usefulness(..)
, AnnotatedGoal
, openGoals
, solveGoal
) where
import Prelude hiding (id, (.))
import qualified Data.DAG.Simple as D (cyclic)
import Data.Foldable (foldMap)
import qualified Data.Map as M
import qualified Data.Monoid as Mono
import qualified Data.Set as S
import Control.Basics
import Control.Category
import Control.Monad.Disj
import Control.Monad.State (gets)
import Extension.Data.Label
import Theory.Constraint.Solver.Contradictions (substCreatesNonNormalTerms)
import Theory.Constraint.Solver.Reduction
import Theory.Constraint.Solver.Types
import Theory.Constraint.System
import Theory.Tools.IntruderRules (mkDUnionRule, isDExpRule, isDPMultRule, isDEMapRule)
import Theory.Model
data Usefulness =
Useful
| LoopBreaker
| ProbablyConstructible
| CurrentlyDeducible
deriving (Show, Eq, Ord)
type AnnotatedGoal = (Goal, (Integer, Usefulness))
openGoals :: System -> [AnnotatedGoal]
openGoals sys = do
(goal, status) <- M.toList $ get sGoals sys
let solved = get gsSolved status
guard $ case goal of
ActionG _ (kFactView -> Just (UpK, m)) ->
not $ solved
|| isMsgVar m || sortOfLNTerm m == LSortPub
|| isPair m || isInverse m || isProduct m
|| isUnion m || isNullaryPublicFunction m
ActionG _ _ -> not solved
PremiseG _ _ -> not solved
DisjG (Disj []) -> False
DisjG _ -> not solved
ChainG c _ ->
case kFactView (nodeConcFact c sys) of
Just (DnK, viewTerm2 -> FUnion args) ->
not solved && allMsgVarsKnownEarlier c args
Just (DnK, m) | isMsgVar m -> False
| otherwise -> not solved
fa -> error $ "openChainGoals: impossible fact: " ++ show fa
SplitG idx -> splitExists (get sEqStore sys) idx
let
useful = case goal of
_ | get gsLoopBreaker status -> LoopBreaker
ActionG i (kFactView -> Just (UpK, m))
| hasKUGuards -> Useful
| currentlyDeducible i m -> CurrentlyDeducible
| probablyConstructible m -> ProbablyConstructible
_ -> Useful
return (goal, (get gsNr status, useful))
where
existingDeps = rawLessRel sys
hasKUGuards =
any ((KUFact `elem`) . guardFactTags) $ S.toList $ get sFormulas sys
checkTermLits :: (LSort -> Bool) -> LNTerm -> Bool
checkTermLits p =
Mono.getAll . foldMap (Mono.All . p . sortOfLit)
probablyConstructible m = checkTermLits (LSortFresh /=) m
&& not (containsPrivate m)
currentlyDeducible i m = (checkTermLits (LSortPub ==) m
&& not (containsPrivate m))
|| extractible i m
extractible i m = or $ do
(j, ru) <- M.toList $ get sNodes sys
guard (not $ isLast sys j)
let derivedMsgs = concatMap toplevelTerms $
[ t | Fact OutFact [t] <- get rConcs ru] <|>
[ t | Just (DnK, t) <- kFactView <$> get rConcs ru]
return $ m `elem` derivedMsgs &&
not (D.cyclic ((j, i) : existingDeps))
toplevelTerms t@(viewTerm2 -> FPair t1 t2) =
t : toplevelTerms t1 ++ toplevelTerms t2
toplevelTerms t@(viewTerm2 -> FInv t1) = t : toplevelTerms t1
toplevelTerms t = [t]
allMsgVarsKnownEarlier (i,_) args =
all (`elem` earlierMsgVars) (filter isMsgVar args)
where earlierMsgVars = do (j, _, t) <- allKUActions sys
guard $ isMsgVar t && alwaysBefore sys j i
return t
solveGoal :: Goal -> Reduction String
solveGoal goal = do
markGoalAsSolved "directly" goal
rules <- askM pcRules
case goal of
ActionG i fa -> solveAction (nonSilentRules rules) (i, fa)
PremiseG p fa ->
solvePremise (get crProtocol rules ++ get crConstruct rules) p fa
ChainG c p -> solveChain (get crDestruct rules) (c, p)
SplitG i -> solveSplit i
DisjG disj -> solveDisjunction disj
solveAction :: [RuleAC]
-> (NodeId, LNFact)
-> Reduction String
solveAction rules (i, fa) = do
mayRu <- M.lookup i <$> getM sNodes
showRuleCaseName <$> case mayRu of
Nothing -> do ru <- labelNodeId i rules
act <- disjunctionOfList $ get rActs ru
void (solveFactEqs SplitNow [Equal fa act])
return ru
Just ru -> do unless (fa `elem` get rActs ru) $ do
act <- disjunctionOfList $ get rActs ru
void (solveFactEqs SplitNow [Equal fa act])
return ru
solvePremise :: [RuleAC]
-> NodePrem
-> LNFact
-> Reduction String
solvePremise rules p faPrem
| isKDFact faPrem = do
iLearn <- freshLVar "vl" LSortNode
mLearn <- varTerm <$> freshLVar "t" LSortMsg
let concLearn = kdFact mLearn
premLearn = outFact mLearn
ruLearn = Rule (IntrInfo IRecvRule) [premLearn] [concLearn] []
cLearn = (iLearn, ConcIdx 0)
pLearn = (iLearn, PremIdx 0)
modM sNodes (M.insert iLearn ruLearn)
insertChain cLearn p
solvePremise rules pLearn premLearn
| otherwise = do
(ru, c, faConc) <- insertFreshNodeConc rules
insertEdges [(c, faConc, faPrem, p)]
return $ showRuleCaseName ru
solveChain :: [RuleAC]
-> (NodeConc, NodePrem)
-> Reduction String
solveChain rules (c, p) = do
faConc <- gets $ nodeConcFact c
(do
cRule <- gets $ nodeRule (nodeConcNode c)
pRule <- gets $ nodeRule (nodePremNode p)
faPrem <- gets $ nodePremFact p
contradictoryIf (forbiddenEdge cRule pRule)
insertEdges [(c, faConc, faPrem, p)]
let mPrem = case kFactView faConc of
Just (DnK, m') -> m'
_ -> error $ "solveChain: impossible"
caseName (viewTerm -> FApp o _) = showFunSymName o
caseName t = show t
return $ caseName mPrem
`disjunction`
case kFactView faConc of
Just (DnK, viewTerm2 -> FUnion args) ->
do
i <- freshLVar "vr" LSortNode
let rus = map (ruleACIntrToRuleACInst . mkDUnionRule args)
(filter (not . isMsgVar) args)
ru <- disjunctionOfList rus
modM sNodes (M.insert i ru)
let v = PremIdx 0
faPrem <- gets $ nodePremFact (i,v)
extendAndMark i ru v faPrem faConc
_ ->
do
cRule <- gets $ nodeRule (nodeConcNode c)
(i, ru) <- insertFreshNode rules
contradictoryIf (forbiddenEdge cRule ru)
(v, faPrem) <- disjunctionOfList $ take 1 $ enumPrems ru
extendAndMark i ru v faPrem faConc
)
where
extendAndMark i ru v faPrem faConc = do
insertEdges [(c, faConc, faPrem, (i, v))]
markGoalAsSolved "directly" (PremiseG (i, v) faPrem)
insertChain (i, ConcIdx 0) p
return $ showRuleCaseName ru
forbiddenEdge cRule pRule = isDExpRule cRule && isDExpRule pRule ||
isDPMultRule cRule && isDPMultRule pRule ||
isDPMultRule cRule && isDEMapRule pRule
solveSplit :: SplitId -> Reduction String
solveSplit x = do
split <- gets ((`performSplit` x) . get sEqStore)
let errMsg = error "solveSplit: inexistent split-id"
store <- maybe errMsg disjunctionOfList split
hnd <- getMaudeHandle
substCheck <- gets (substCreatesNonNormalTerms hnd)
store' <- simp hnd substCheck store
contradictoryIf (eqsIsFalse store')
sEqStore =: store'
return "split"
solveDisjunction :: Disj LNGuarded -> Reduction String
solveDisjunction disj = do
(i, gfm) <- disjunctionOfList $ zip [(1::Int)..] $ getDisj disj
insertFormula gfm
return $ "case_" ++ show i