HyLo.Formula

Documentation

data Formula n p r

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

Methods

(|=) :: (Model w n p r, w) -> Formula n p r -> Bool

(Eq n, Eq p, Eq r) => Eq (Formula n p r)

Methods

(==) :: Formula n p r -> Formula n p r -> Bool

(/=) :: Formula n p r -> Formula n p r -> Bool

(Ord n, Ord p, Ord r) => Ord (Formula n p r)

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)

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)

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)

Methods

uniplate :: UniplateType (Formula n p r)

(Ord n, Ord p, Ord r) => HasSignature (Formula n p r)

Associated Types

type NomsOf (Formula n p r) :: *

type PropsOf (Formula n p r) :: *

type RelsOf (Formula n p r) :: *

Methods

getSignature :: Formula n p r -> Signature (NomsOf (Formula n p r)) (PropsOf (Formula n p r)) (RelsOf (Formula n p r))

(Ord w, Ord n, Ord p, Ord r) => ModelsRel (Model w n p r) (Formula n p r) n p r

Methods

(|=) :: Model w n p r -> Formula n p r -> Bool

type NomsOf (Formula n p r)

type NomsOf (Formula n p r) = n

type PropsOf (Formula n p r)

type PropsOf (Formula n p r) = p

type RelsOf (Formula n p r)

type RelsOf (Formula n p r) = r

data Where r

Constructors

Global

Local r

Instances

Eq r => Eq (Where r)

Methods

(==) :: Where r -> Where r -> Bool

(/=) :: Where r -> Where r -> Bool

Ord r => Ord (Where r)

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

Constructors

(:>=:)

(:<=:)

(:>:)

(:<:)

(:=:)

(:/=:)

Instances

Eq CountOp

Methods

(==) :: CountOp -> CountOp -> Bool

(/=) :: CountOp -> CountOp -> Bool

Ord CountOp

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

Methods

readsPrec :: Int -> ReadS CountOp

readList :: ReadS [CountOp]

readPrec :: ReadPrec CountOp

readListPrec :: ReadPrec [CountOp]

Show CountOp

Methods

showsPrec :: Int -> CountOp -> ShowS

show :: CountOp -> String

showList :: [CountOp] -> ShowS

negCount :: CountOp -> CountOp

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

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

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

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

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)

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

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

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

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

compareWith :: CountOp -> Int -> Int -> Bool

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