module Theory.Model.Atom(
Atom(..)
, NAtom
, LNAtom
, isActionAtom
, isLastAtom
, isLessAtom
, isEqAtom
, BLAtom
, prettyNAtom
)
where
import Control.Basics
import Control.DeepSeq
import Data.Binary
import Data.DeriveTH
import Data.Foldable (Foldable, foldMap)
import Data.Generics
import Data.Monoid (mappend, mempty)
import Data.Traversable
import Term.LTerm
import Term.Unification
import Theory.Model.Fact
import Theory.Text.Pretty
data Atom t = Action t (Fact t)
| EqE t t
| Less t t
| Last t
deriving( Eq, Ord, Show, Data, Typeable )
type NAtom v = Atom (VTerm Name v)
type LNAtom = Atom LNTerm
type BLAtom = Atom BLTerm
instance Functor Atom where
fmap f (Action i fa) = Action (f i) (fmap f fa)
fmap f (EqE l r) = EqE (f l) (f r)
fmap f (Less v u) = Less (f v) (f u)
fmap f (Last i) = Last (f i)
instance Foldable Atom where
foldMap f (Action i fa) =
f i `mappend` (foldMap f fa)
foldMap f (EqE l r) = f l `mappend` f r
foldMap f (Less i j) = f i `mappend` f j
foldMap f (Last i) = f i
instance Traversable Atom where
traverse f (Action i fa) =
Action <$> f i <*> traverse f fa
traverse f (EqE l r) = EqE <$> f l <*> f r
traverse f (Less v u) = Less <$> f v <*> f u
traverse f (Last i) = Last <$> f i
instance HasFrees t => HasFrees (Atom t) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc _ _ = const mempty
mapFrees f = traverse (mapFrees f)
instance Apply LNAtom where
apply subst (Action i fact) = Action (apply subst i) (apply subst fact)
apply subst (EqE l r) = EqE (apply subst l) (apply subst r)
apply subst (Less i j) = Less (apply subst i) (apply subst j)
apply subst (Last i) = Last (apply subst i)
instance Apply BLAtom where
apply subst (Action i fact) = Action (apply subst i) (apply subst fact)
apply subst (EqE l r) = EqE (apply subst l) (apply subst r)
apply subst (Less i j) = Less (apply subst i) (apply subst j)
apply subst (Last i) = Last (apply subst i)
isActionAtom :: Atom t -> Bool
isActionAtom ato = case ato of Action _ _ -> True; _ -> False
isLastAtom :: Atom t -> Bool
isLastAtom ato = case ato of Last _ -> True; _ -> False
isLessAtom :: Atom t -> Bool
isLessAtom ato = case ato of Less _ _ -> True; _ -> False
isEqAtom :: Atom t -> Bool
isEqAtom ato = case ato of EqE _ _ -> True; _ -> False
prettyNAtom :: (Show v, HighlightDocument d) => NAtom v -> d
prettyNAtom (Action v fa) =
prettyFact prettyNTerm fa <-> opAction <-> text (show v)
prettyNAtom (EqE l r) =
sep [prettyNTerm l <-> opEqual, prettyNTerm r]
prettyNAtom (Less u v) = text (show u) <-> opLess <-> text (show v)
prettyNAtom (Last i) = operator_ "last" <> parens (text (show i))
$( derive makeNFData ''Atom)
$( derive makeBinary ''Atom)