{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE TemplateHaskell #-} -- | -- Copyright : (c) 2010-2012 Benedikt Schmidt & Simon Meier -- License : GPL v3 (see LICENSE) -- -- Maintainer : Simon Meier -- Portability : GHC only -- -- Types representing constraints. module Theory.Constraint.System.Constraints ( -- * Guarded formulas module Theory.Constraint.System.Guarded -- * Graph constraints , NodePrem , NodeConc , Edge(..) , Less -- * Goal constraints , Goal(..) , isActionGoal , isStandardActionGoal , isPremiseGoal , isChainGoal , isSplitGoal , isDisjGoal -- ** Pretty-printing , 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 ------------------------------------------------------------------------------ -- Graph part of a sequent -- ------------------------------------------------------------------------------ -- | A premise of a node. type NodePrem = (NodeId, PremIdx) -- | A conclusion of a node. type NodeConc = (NodeId, ConcIdx) -- | A labeled edge in a derivation graph. data Edge = Edge { eSrc :: NodeConc , eTgt :: NodePrem } deriving (Show, Ord, Eq, Data, Typeable) -- | A *⋖* constraint between 'NodeId's. type Less = (NodeId, NodeId) -- Instances ------------ 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 ------------------------------------------------------------------------------ -- Goals ------------------------------------------------------------------------------ -- | A 'Goal' denotes that a constraint reduction rule is applicable, which -- might result in case splits. We either use a heuristic to decide what goal -- to solve next or leave the choice to user (in case of the interactive UI). data Goal = ActionG LVar LNFact -- ^ An action that must exist in the trace. | ChainG NodeConc NodePrem -- A destruction chain. | PremiseG NodePrem LNFact -- ^ A premise that must have an incoming direct edge. | SplitG SplitId -- ^ A case split over equalities. | DisjG (Disj LNGuarded) -- ^ A case split over a disjunction. deriving( Eq, Ord, Show ) -- Indicators ------------- 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 -- Instances ------------ 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) ------------------------------------------------------------------------------ -- Pretty printing -- ------------------------------------------------------------------------------ -- | Pretty print a node. prettyNode :: HighlightDocument d => (NodeId, RuleACInst) -> d prettyNode (v,ru) = prettyNodeId v <> colon <-> prettyRuleACInst ru -- | Pretty print a node conclusion. prettyNodeConc :: HighlightDocument d => NodeConc -> d prettyNodeConc (v, ConcIdx i) = parens (prettyNodeId v <> comma <-> int i) -- | Pretty print a node premise. prettyNodePrem :: HighlightDocument d => NodePrem -> d prettyNodePrem (v, PremIdx i) = parens (prettyNodeId v <> comma <-> int i) -- | Pretty print a edge as @src >-i--j-> tgt@. prettyEdge :: HighlightDocument d => Edge -> d prettyEdge (Edge c p) = prettyNodeConc c <-> operator_ ">-->" <-> prettyNodePrem p -- | Pretty print a less-atom as @src < tgt@. prettyLess :: HighlightDocument d => Less -> d prettyLess (i, j) = prettyNAtom $ Less (varTerm i) (varTerm j) -- | Pretty print a goal. 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) = -- Note that we can use "▷" for conclusions once we need them. prettyLNFact fa <-> text ("▶" ++ subscript (show v)) <-> prettyNodeId i -- prettyNodePrem p <> brackets (prettyLNFact fa) prettyGoal (DisjG (Disj [])) = text "Disj" <-> operator_ "(⊥)" prettyGoal (DisjG (Disj gfs)) = fsep $ punctuate (operator_ " ∥") (map (nest 1 . parens . prettyGuarded) gfs) -- punctuate (operator_ " |") (map (nest 1 . parens . prettyGuarded) gfs) prettyGoal (SplitG x) = text "splitEqs" <> parens (text $ show (unSplitId x)) -- Derived instances -------------------- $( derive makeBinary ''Edge) $( derive makeBinary ''Goal) $( derive makeNFData ''Edge) $( derive makeNFData ''Goal)