module Theory.Constraint.System (
module Theory.Constraint.System.Constraints
, System
, emptySystem
, SystemTraceQuantifier(..)
, formulaToSystem
, sNodes
, allKDConcs
, nodeRule
, nodeConcNode
, nodePremNode
, nodePremFact
, nodeConcFact
, resolveNodePremFact
, resolveNodeConcFact
, allActions
, allKUActions
, unsolvedActionAtoms
, kuActionAtoms
, standardActionAtoms
, sEdges
, unsolvedChains
, sLessAtoms
, rawLessRel
, rawEdgeRel
, alwaysBefore
, isInTrace
, sLastAtom
, isLast
, module Theory.Tools.EquationStore
, sEqStore
, sSubst
, sConjDisjEqs
, sFormulas
, sSolvedFormulas
, sLemmas
, insertLemmas
, CaseDistKind(..)
, sCaseDistKind
, GoalStatus(..)
, gsSolved
, gsLoopBreaker
, gsNr
, sGoals
, sNextGoalNr
, prettySystem
, prettyNonGraphSystem
) where
import Prelude hiding (id, (.))
import Data.Binary
import qualified Data.DAG.Simple as D
import Data.DeriveTH
import Data.List (foldl', partition)
import qualified Data.Map as M
import Data.Maybe (fromMaybe)
import Data.Monoid (Monoid(..))
import qualified Data.Set as S
import Control.Basics
import Control.Category
import Control.DeepSeq
import Data.Label ((:->), mkLabels)
import qualified Extension.Data.Label as L
import Logic.Connectives
import Theory.Constraint.System.Constraints
import Theory.Model
import Theory.Text.Pretty
import Theory.Tools.EquationStore
data SystemTraceQuantifier = ExistsSomeTrace | ExistsNoTrace
deriving( Eq, Ord, Show )
data CaseDistKind = UntypedCaseDist | TypedCaseDist
deriving( Eq )
instance Show CaseDistKind where
show UntypedCaseDist = "untyped"
show TypedCaseDist = "typed"
instance Read CaseDistKind where
readsPrec p0 r
= readParen (p0 > 10)
(\ r0 ->
[(UntypedCaseDist, r1) | ("untyped", r1) <- lex r0])
r
++
readParen (p0 > 10)
(\ r0 -> [(TypedCaseDist, r1) | ("typed", r1) <- lex r0])
r
instance Ord CaseDistKind where
compare UntypedCaseDist UntypedCaseDist = EQ
compare UntypedCaseDist TypedCaseDist = LT
compare TypedCaseDist UntypedCaseDist = GT
compare TypedCaseDist TypedCaseDist = EQ
data GoalStatus = GoalStatus
{ _gsSolved :: Bool
, _gsNr :: Integer
, _gsLoopBreaker :: Bool
}
deriving( Eq, Ord, Show )
data System = System
{ _sNodes :: M.Map NodeId RuleACInst
, _sEdges :: S.Set Edge
, _sLessAtoms :: S.Set (NodeId, NodeId)
, _sLastAtom :: Maybe NodeId
, _sEqStore :: EqStore
, _sFormulas :: S.Set LNGuarded
, _sSolvedFormulas :: S.Set LNGuarded
, _sLemmas :: S.Set LNGuarded
, _sGoals :: M.Map Goal GoalStatus
, _sNextGoalNr :: Integer
, _sCaseDistKind :: CaseDistKind
}
deriving( Eq, Ord )
$(mkLabels [''System, ''GoalStatus])
sSubst :: System :-> LNSubst
sSubst = eqsSubst . sEqStore
sConjDisjEqs :: System :-> Conj (SplitId, S.Set (LNSubstVFresh))
sConjDisjEqs = eqsConj . sEqStore
emptySystem :: CaseDistKind -> System
emptySystem = System
M.empty S.empty S.empty Nothing emptyEqStore
S.empty S.empty S.empty
M.empty 0
formulaToSystem :: [LNGuarded]
-> CaseDistKind
-> SystemTraceQuantifier
-> LNFormula
-> System
formulaToSystem axioms kind traceQuantifier fm =
insertLemmas safetyAxioms
$ L.set sFormulas (S.singleton gf2)
$ (emptySystem kind)
where
(safetyAxioms, otherAxioms) = partition isSafetyFormula axioms
gf0 = formulaToGuarded_ fm
gf1 = case traceQuantifier of
ExistsSomeTrace -> gf0
ExistsNoTrace -> gnot gf0
gf2 = gconj $ gf1 : otherAxioms
insertLemma :: LNGuarded -> System -> System
insertLemma =
go
where
go (GConj conj) = foldr (.) id $ map go $ getConj conj
go fm = L.modify sLemmas (S.insert fm)
insertLemmas :: [LNGuarded] -> System -> System
insertLemmas fms sys = foldl' (flip insertLemma) sys fms
allKDConcs :: System -> [(NodeId, RuleACInst, LNTerm)]
allKDConcs sys = do
(i, ru) <- M.toList $ L.get sNodes sys
(_, kFactView -> Just (DnK, m)) <- enumConcs ru
return (i, ru, m)
nodeRule :: NodeId -> System -> RuleACInst
nodeRule v se =
fromMaybe errMsg $ M.lookup v $ L.get sNodes se
where
errMsg = error $
"nodeRule: node '" ++ show v ++ "' does not exist in sequent\n" ++
render (nest 2 $ prettySystem se)
nodePremFact :: NodePrem -> System -> LNFact
nodePremFact (v, i) se = L.get (rPrem i) $ nodeRule v se
nodePremNode :: NodePrem -> NodeId
nodePremNode = fst
resolveNodePremFact :: NodePrem -> System -> Maybe LNFact
resolveNodePremFact (v, i) se = lookupPrem i =<< M.lookup v (L.get sNodes se)
resolveNodeConcFact :: NodeConc -> System -> Maybe LNFact
resolveNodeConcFact (v, i) se = lookupConc i =<< M.lookup v (L.get sNodes se)
nodeConcFact :: NodeConc -> System -> LNFact
nodeConcFact (v, i) = L.get (rConc i) . nodeRule v
nodeConcNode :: NodeConc -> NodeId
nodeConcNode = fst
unsolvedActionAtoms :: System -> [(NodeId, LNFact)]
unsolvedActionAtoms sys =
do (ActionG i fa, status) <- M.toList (L.get sGoals sys)
guard (not $ L.get gsSolved status)
return (i, fa)
allActions :: System -> [(NodeId, LNFact)]
allActions sys =
unsolvedActionAtoms sys
<|> do (i, ru) <- M.toList $ L.get sNodes sys
(,) i <$> L.get rActs ru
allKUActions :: System -> [(NodeId, LNFact, LNTerm)]
allKUActions sys = do
(i, fa@(kFactView -> Just (UpK, m))) <- allActions sys
return (i, fa, m)
standardActionAtoms :: System -> [(NodeId, LNFact)]
standardActionAtoms = filter (not . isKUFact . snd) . unsolvedActionAtoms
kuActionAtoms :: System -> [(NodeId, LNFact, LNTerm)]
kuActionAtoms sys = do
(i, fa@(kFactView -> Just (UpK, m))) <- unsolvedActionAtoms sys
return (i, fa, m)
unsolvedChains :: System -> [(NodeConc, NodePrem)]
unsolvedChains sys = do
(ChainG from to, status) <- M.toList $ L.get sGoals sys
guard (not $ L.get gsSolved status)
return (from, to)
rawEdgeRel :: System -> [(NodeId, NodeId)]
rawEdgeRel sys = map (nodeConcNode *** nodePremNode) $
[(from, to) | Edge from to <- S.toList $ L.get sEdges sys]
++ unsolvedChains sys
rawLessRel :: System -> [(NodeId,NodeId)]
rawLessRel se = S.toList (L.get sLessAtoms se) ++ rawEdgeRel se
alwaysBefore :: System -> (NodeId -> NodeId -> Bool)
alwaysBefore sys =
check
where
lessRel = rawLessRel sys
check i j =
((i, j) `S.member` L.get sLessAtoms sys)
|| (j `S.member` D.reachableSet [i] lessRel)
isInTrace :: System -> NodeId -> Bool
isInTrace sys i =
i `M.member` L.get sNodes sys
|| isLast sys i
|| any ((i ==) . fst) (unsolvedActionAtoms sys)
isLast :: System -> NodeId -> Bool
isLast sys i = Just i == L.get sLastAtom sys
prettySystem :: HighlightDocument d => System -> d
prettySystem se = vcat $
map combine
[ ("nodes", vcat $ map prettyNode $ M.toList $ L.get sNodes se)
, ("actions", fsepList ppActionAtom $ unsolvedActionAtoms se)
, ("edges", fsepList prettyEdge $ S.toList $ L.get sEdges se)
, ("less", fsepList prettyLess $ S.toList $ L.get sLessAtoms se)
, ("unsolved goals", prettyGoals False se)
]
++ [prettyNonGraphSystem se]
where
combine (header, d) = fsep [keyword_ header <> colon, nest 2 d]
ppActionAtom (i, fa) = prettyNAtom (Action (varTerm i) fa)
prettyNonGraphSystem :: HighlightDocument d => System -> d
prettyNonGraphSystem se = vsep $ map combine
[ ("last", maybe (text "none") prettyNodeId $ L.get sLastAtom se)
, ("formulas", vsep $ map prettyGuarded $ S.toList $ L.get sFormulas se)
, ("equations", prettyEqStore $ L.get sEqStore se)
, ("lemmas", vsep $ map prettyGuarded $ S.toList $ L.get sLemmas se)
, ("allowed cases", text $ show $ L.get sCaseDistKind se)
, ("solved formulas", vsep $ map prettyGuarded $ S.toList $ L.get sSolvedFormulas se)
, ("solved goals", prettyGoals True se)
]
where
combine (header, d) = fsep [keyword_ header <> colon, nest 2 d]
prettyGoals :: HighlightDocument d => Bool -> System -> d
prettyGoals solved sys = vsep $ do
(goal, status) <- M.toList $ L.get sGoals sys
guard (solved == L.get gsSolved status)
let nr = L.get gsNr status
loopBreaker | L.get gsLoopBreaker status = " (loop breaker)"
| otherwise = ""
return $ prettyGoal goal <-> lineComment_ ("nr: " ++ show nr ++ loopBreaker)
deriving instance Show System
instance Apply CaseDistKind where
apply = const id
instance HasFrees CaseDistKind where
foldFrees = const mempty
foldFreesOcc _ _ = const mempty
mapFrees = const pure
instance HasFrees GoalStatus where
foldFrees = const mempty
foldFreesOcc _ _ = const mempty
mapFrees = const pure
instance HasFrees System where
foldFrees fun (System a b c d e f g h i j k) =
foldFrees fun a `mappend`
foldFrees fun b `mappend`
foldFrees fun c `mappend`
foldFrees fun d `mappend`
foldFrees fun e `mappend`
foldFrees fun f `mappend`
foldFrees fun g `mappend`
foldFrees fun h `mappend`
foldFrees fun i `mappend`
foldFrees fun j `mappend`
foldFrees fun k
foldFreesOcc fun ctx (System a _b _c _d _e _f _g _h _i _j _k) =
foldFreesOcc fun ("a":ctx') a
where ctx' = "system":ctx
mapFrees fun (System a b c d e f g h i j k) =
System <$> mapFrees fun a
<*> mapFrees fun b
<*> mapFrees fun c
<*> mapFrees fun d
<*> mapFrees fun e
<*> mapFrees fun f
<*> mapFrees fun g
<*> mapFrees fun h
<*> mapFrees fun i
<*> mapFrees fun j
<*> mapFrees fun k
$( derive makeBinary ''CaseDistKind)
$( derive makeBinary ''GoalStatus)
$( derive makeBinary ''System)
$( derive makeBinary ''SystemTraceQuantifier)
$( derive makeNFData ''CaseDistKind)
$( derive makeNFData ''GoalStatus)
$( derive makeNFData ''System)
$( derive makeNFData ''SystemTraceQuantifier)