module Theory.Constraint.System.Constraints (
module Theory.Constraint.System.Guarded
, NodePrem
, NodeConc
, Edge(..)
, Less
, Goal(..)
, isActionGoal
, isStandardActionGoal
, isPremiseGoal
, isChainGoal
, isSplitGoal
, isDisjGoal
, prettyNode
, prettyNodePrem
, prettyNodeConc
, prettyEdge
, prettyLess
, prettyGoal
) where
import Data.Binary
import Data.DeriveTH
import Data.Generics
import Extension.Data.Monoid (Monoid(..))
import Control.Basics
import Control.DeepSeq
import Text.PrettyPrint.Class
import Text.Unicode
import Logic.Connectives
import Theory.Constraint.System.Guarded
import Theory.Model
import Theory.Text.Pretty
import Theory.Tools.EquationStore
type NodePrem = (NodeId, PremIdx)
type NodeConc = (NodeId, ConcIdx)
data Edge = Edge {
eSrc :: NodeConc
, eTgt :: NodePrem
}
deriving (Show, Ord, Eq, Data, Typeable)
type Less = (NodeId, NodeId)
instance Apply Edge where
apply subst (Edge from to) = Edge (apply subst from) (apply subst to)
instance HasFrees Edge where
foldFrees f (Edge x y) = foldFrees f x `mappend` foldFrees f y
foldFreesOcc f c (Edge x y) = foldFreesOcc f ("edge":c) (x, y)
mapFrees f (Edge x y) = Edge <$> mapFrees f x <*> mapFrees f y
data Goal =
ActionG LVar LNFact
| ChainG NodeConc NodePrem
| PremiseG NodePrem LNFact
| SplitG SplitId
| DisjG (Disj LNGuarded)
deriving( Eq, Ord, Show )
isActionGoal :: Goal -> Bool
isActionGoal (ActionG _ _) = True
isActionGoal _ = False
isStandardActionGoal :: Goal -> Bool
isStandardActionGoal (ActionG _ fa) = not (isKUFact fa)
isStandardActionGoal _ = False
isPremiseGoal :: Goal -> Bool
isPremiseGoal (PremiseG _ _) = True
isPremiseGoal _ = False
isChainGoal :: Goal -> Bool
isChainGoal (ChainG _ _) = True
isChainGoal _ = False
isSplitGoal :: Goal -> Bool
isSplitGoal (SplitG _) = True
isSplitGoal _ = False
isDisjGoal :: Goal -> Bool
isDisjGoal (DisjG _) = True
isDisjGoal _ = False
instance HasFrees Goal where
foldFrees f goal = case goal of
ActionG i fa -> foldFrees f i <> foldFrees f fa
PremiseG p fa -> foldFrees f p <> foldFrees f fa
ChainG c p -> foldFrees f c <> foldFrees f p
SplitG i -> foldFrees f i
DisjG x -> foldFrees f x
foldFreesOcc f c goal = case goal of
ActionG i fa -> foldFreesOcc f ("ActionG":c) (i, fa)
ChainG co p -> foldFreesOcc f ("ChainG":c) (co, p)
_ -> mempty
mapFrees f goal = case goal of
ActionG i fa -> ActionG <$> mapFrees f i <*> mapFrees f fa
PremiseG p fa -> PremiseG <$> mapFrees f p <*> mapFrees f fa
ChainG c p -> ChainG <$> mapFrees f c <*> mapFrees f p
SplitG i -> SplitG <$> mapFrees f i
DisjG x -> DisjG <$> mapFrees f x
instance Apply Goal where
apply subst goal = case goal of
ActionG i fa -> ActionG (apply subst i) (apply subst fa)
PremiseG p fa -> PremiseG (apply subst p) (apply subst fa)
ChainG c p -> ChainG (apply subst c) (apply subst p)
SplitG i -> SplitG (apply subst i)
DisjG x -> DisjG (apply subst x)
prettyNode :: HighlightDocument d => (NodeId, RuleACInst) -> d
prettyNode (v,ru) = prettyNodeId v <> colon <-> prettyRuleACInst ru
prettyNodeConc :: HighlightDocument d => NodeConc -> d
prettyNodeConc (v, ConcIdx i) = parens (prettyNodeId v <> comma <-> int i)
prettyNodePrem :: HighlightDocument d => NodePrem -> d
prettyNodePrem (v, PremIdx i) = parens (prettyNodeId v <> comma <-> int i)
prettyEdge :: HighlightDocument d => Edge -> d
prettyEdge (Edge c p) =
prettyNodeConc c <-> operator_ ">-->" <-> prettyNodePrem p
prettyLess :: HighlightDocument d => Less -> d
prettyLess (i, j) = prettyNAtom $ Less (varTerm i) (varTerm j)
prettyGoal :: HighlightDocument d => Goal -> d
prettyGoal (ActionG i fa) = prettyNAtom (Action (varTerm i) fa)
prettyGoal (ChainG c p) =
prettyNodeConc c <-> operator_ "~~>" <-> prettyNodePrem p
prettyGoal (PremiseG (i, (PremIdx v)) fa) =
prettyLNFact fa <-> text ("▶" ++ subscript (show v)) <-> prettyNodeId i
prettyGoal (DisjG (Disj [])) = text "Disj" <-> operator_ "(⊥)"
prettyGoal (DisjG (Disj gfs)) = fsep $
punctuate (operator_ " ∥") (map (nest 1 . parens . prettyGuarded) gfs)
prettyGoal (SplitG x) =
text "splitEqs" <> parens (text $ show (unSplitId x))
$( derive makeBinary ''Edge)
$( derive makeBinary ''Goal)
$( derive makeNFData ''Edge)
$( derive makeNFData ''Goal)