Safe Haskell	None
Language	Haskell2010

HyLo.Formula

Documentation

data Formula n p r Source #

Constructors

Top
Bot
Prop p
Nom n
Neg (Formula n p r)
(Formula n p r) :&: (Formula n p r) infixl 8
(Formula n p r) :\|: (Formula n p r) infixl 8
(Formula n p r) :-->: (Formula n p r) infixr 7
(Formula n p r) :<-->: (Formula n p r) infix 7
Diam r (Formula n p r)
Box r (Formula n p r)
IDiam r (Formula n p r)
IBox r (Formula n p r)
At n (Formula n p r)
A (Formula n p r)
E (Formula n p r)
D (Formula n p r)
B (Formula n p r)
Down n (Formula n p r)
Count CountOp (Where r) Int (Formula n p r)

Instances

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r, w) (Formula n p r) n p r Source #
Instance details Defined in HyLo.Model Methods (\|=) :: (Model w n p r, w) -> Formula n p r -> Bool Source #
(Eq p, Eq n, Eq r) => Eq (Formula n p r) Source #
Instance details Defined in HyLo.Formula Methods (==) :: Formula n p r -> Formula n p r -> Bool # (/=) :: Formula n p r -> Formula n p r -> Bool #
(Ord p, Ord n, Ord r) => Ord (Formula n p r) Source #
Instance details Defined in HyLo.Formula Methods compare :: Formula n p r -> Formula n p r -> Ordering # (<) :: Formula n p r -> Formula n p r -> Bool # (<=) :: Formula n p r -> Formula n p r -> Bool # (>) :: Formula n p r -> Formula n p r -> Bool # (>=) :: Formula n p r -> Formula n p r -> Bool # max :: Formula n p r -> Formula n p r -> Formula n p r # min :: Formula n p r -> Formula n p r -> Formula n p r #
(Read n, Read p, Read r) => Read (Formula n p r) Source #
Instance details Defined in HyLo.Formula Methods readsPrec :: Int -> ReadS (Formula n p r) # readList :: ReadS [Formula n p r] # readPrec :: ReadPrec (Formula n p r) # readListPrec :: ReadPrec [Formula n p r] #
(Show n, Show p, Show r) => Show (Formula n p r) Source #
Instance details Defined in HyLo.Formula Methods showsPrec :: Int -> Formula n p r -> ShowS # show :: Formula n p r -> String # showList :: [Formula n p r] -> ShowS #
Uniplate (Formula n p r) Source #
Instance details Defined in HyLo.Formula Methods uniplate :: Formula n p r -> (Str (Formula n p r), Str (Formula n p r) -> Formula n p r) # descend :: (Formula n p r -> Formula n p r) -> Formula n p r -> Formula n p r # descendM :: Monad m => (Formula n p r -> m (Formula n p r)) -> Formula n p r -> m (Formula n p r) #
(Ord n, Ord p, Ord r) => HasSignature (Formula n p r) Source #
Instance details Defined in HyLo.Formula Associated Types type NomsOf (Formula n p r) :: Type Source # type PropsOf (Formula n p r) :: Type Source # type RelsOf (Formula n p r) :: Type Source # Methods getSignature :: Formula n p r -> Signature (NomsOf (Formula n p r)) (PropsOf (Formula n p r)) (RelsOf (Formula n p r)) Source #
(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r) (Formula n p r) n p r Source #
Instance details Defined in HyLo.Model Methods (\|=) :: Model w n p r -> Formula n p r -> Bool Source #
type NomsOf (Formula n p r) Source #
Instance details Defined in HyLo.Formula type NomsOf (Formula n p r) = n
type PropsOf (Formula n p r) Source #
Instance details Defined in HyLo.Formula type PropsOf (Formula n p r) = p
type RelsOf (Formula n p r) Source #
Instance details Defined in HyLo.Formula type RelsOf (Formula n p r) = r

data Where r Source #

Constructors

Global
Local r

Instances

Eq r => Eq (Where r) Source #
Instance details Defined in HyLo.Formula Methods (==) :: Where r -> Where r -> Bool # (/=) :: Where r -> Where r -> Bool #
Ord r => Ord (Where r) Source #
Instance details Defined in HyLo.Formula Methods compare :: Where r -> Where r -> Ordering # (<) :: Where r -> Where r -> Bool # (<=) :: Where r -> Where r -> Bool # (>) :: Where r -> Where r -> Bool # (>=) :: Where r -> Where r -> Bool # max :: Where r -> Where r -> Where r # min :: Where r -> Where r -> Where r #

data CountOp Source #

Constructors

(:>=:)
(:<=:)
(:>:)
(:<:)
(:=:)
(:/=:)

Instances

Eq CountOp Source #
Instance details Defined in HyLo.Formula Methods (==) :: CountOp -> CountOp -> Bool # (/=) :: CountOp -> CountOp -> Bool #
Ord CountOp Source #
Instance details Defined in HyLo.Formula Methods compare :: CountOp -> CountOp -> Ordering # (<) :: CountOp -> CountOp -> Bool # (<=) :: CountOp -> CountOp -> Bool # (>) :: CountOp -> CountOp -> Bool # (>=) :: CountOp -> CountOp -> Bool # max :: CountOp -> CountOp -> CountOp # min :: CountOp -> CountOp -> CountOp #
Read CountOp Source #
Instance details Defined in HyLo.Formula Methods readsPrec :: Int -> ReadS CountOp # readList :: ReadS [CountOp] # readPrec :: ReadPrec CountOp # readListPrec :: ReadPrec [CountOp] #
Show CountOp Source #
Instance details Defined in HyLo.Formula Methods showsPrec :: Int -> CountOp -> ShowS # show :: CountOp -> String # showList :: [CountOp] -> ShowS #

negCount :: CountOp -> CountOp Source #

nnf :: Formula n p r -> Formula n p r Source #

composeFold :: b -> (b -> b -> b) -> (Formula n p r -> b) -> Formula n p r -> b Source #

composeFoldM :: Monad m => m b -> (b -> b -> m b) -> (Formula n p r -> m b) -> Formula n p r -> m b Source #

composeMap :: (Formula n p r -> Formula n p r) -> (Formula n p r -> Formula n p r) -> Formula n p r -> Formula n p r Source #

composeMapM :: (Monad m, Functor m) => (Formula n p r -> m (Formula n p r)) -> (Formula n p r -> m (Formula n p r)) -> Formula n p r -> m (Formula n p r) Source #

onShape :: (n -> n') -> (p -> p') -> (r -> r') -> (Formula n p r -> Formula n' p' r') -> Formula n p r -> Formula n' p' r' Source #

mapSig :: (n -> n') -> (p -> p') -> (r -> r') -> Formula n p r -> Formula n' p' r' Source #

freeVars :: Eq n => Formula n p r -> [n] Source #

boundVars :: Eq n => Formula n p r -> [n] Source #

compareWith :: CountOp -> Int -> Int -> Bool Source #

cmpListLen :: CountOp -> [a] -> Int -> Bool Source #