Zsyntax.Labelled.Formula

Documentation

data FKind

Constructors

KAtom

KConj

KImpl

data Label a l

Type of formula labels. Note that logical atoms are their own labels.

Constructors

L l

Regular label

A a

Logical atom

Instances

(Eq l, Eq a) => Eq (Label a l)

Defined in Zsyntax.Labelled.Formula

Methods

(==) :: Label a l -> Label a l -> Bool

(/=) :: Label a l -> Label a l -> Bool

(Ord l, Ord a) => Ord (Label a l)

Defined in Zsyntax.Labelled.Formula

Methods

compare :: Label a l -> Label a l -> Ordering

(<) :: Label a l -> Label a l -> Bool

(<=) :: Label a l -> Label a l -> Bool

(>) :: Label a l -> Label a l -> Bool

(>=) :: Label a l -> Label a l -> Bool

max :: Label a l -> Label a l -> Label a l

min :: Label a l -> Label a l -> Label a l

(Show l, Show a) => Show (Label a l)

Defined in Zsyntax.Labelled.Formula

Methods

showsPrec :: Int -> Label a l -> ShowS

show :: Label a l -> String

showList :: [Label a l] -> ShowS

newtype ElemBase a

Constructors

ElemBase

Fields

• unEB :: MultiSet a

Instances

Eq a => Eq (ElemBase a)

Defined in Zsyntax.Labelled.Formula

Methods

(==) :: ElemBase a -> ElemBase a -> Bool

(/=) :: ElemBase a -> ElemBase a -> Bool

Ord a => Ord (ElemBase a)

Defined in Zsyntax.Labelled.Formula

Methods

compare :: ElemBase a -> ElemBase a -> Ordering

(<) :: ElemBase a -> ElemBase a -> Bool

(<=) :: ElemBase a -> ElemBase a -> Bool

(>) :: ElemBase a -> ElemBase a -> Bool

(>=) :: ElemBase a -> ElemBase a -> Bool

max :: ElemBase a -> ElemBase a -> ElemBase a

min :: ElemBase a -> ElemBase a -> ElemBase a

Show a => Show (ElemBase a)

Defined in Zsyntax.Labelled.Formula

Methods

showsPrec :: Int -> ElemBase a -> ShowS

show :: ElemBase a -> String

showList :: [ElemBase a] -> ShowS

Ord a => Semigroup (ElemBase a)

Defined in Zsyntax.Labelled.Formula

Methods

(<>) :: ElemBase a -> ElemBase a -> ElemBase a

sconcat :: NonEmpty (ElemBase a) -> ElemBase a

stimes :: Integral b => b -> ElemBase a -> ElemBase a

Ord a => Monoid (ElemBase a)

Defined in Zsyntax.Labelled.Formula

Methods

mempty :: ElemBase a

mappend :: ElemBase a -> ElemBase a -> ElemBase a

mconcat :: [ElemBase a] -> ElemBase a

type ReactionList a = RList (ElemBase a) (CtrlSet a)

Labelled formulas

data LFormula :: FKind -> * -> * -> * where

Type of labelled formulas, indexed by a formula kind and parameterized by the type of the labels and of the logical atoms.

Constructors

Atom :: a -> LFormula KAtom a l

Conj :: LFormula k1 a l -> LFormula k2 a l -> l -> LFormula KConj a l

Impl :: LFormula k1 a l -> ElemBase a -> ReactionList a -> LFormula k2 a l -> l -> LFormula KImpl a l

Instances

Functor (LFormula k a)

Defined in Zsyntax.Labelled.Formula

Methods

fmap :: (a0 -> b) -> LFormula k a a0 -> LFormula k a b

(<$) :: a0 -> LFormula k a b -> LFormula k a a0

Foldable (LFormula k a)

Defined in Zsyntax.Labelled.Formula

Methods

fold :: Monoid m => LFormula k a m -> m

foldMap :: Monoid m => (a0 -> m) -> LFormula k a a0 -> m

foldr :: (a0 -> b -> b) -> b -> LFormula k a a0 -> b

foldr' :: (a0 -> b -> b) -> b -> LFormula k a a0 -> b

foldl :: (b -> a0 -> b) -> b -> LFormula k a a0 -> b

foldl' :: (b -> a0 -> b) -> b -> LFormula k a a0 -> b

foldr1 :: (a0 -> a0 -> a0) -> LFormula k a a0 -> a0

foldl1 :: (a0 -> a0 -> a0) -> LFormula k a a0 -> a0

toList :: LFormula k a a0 -> [a0]

null :: LFormula k a a0 -> Bool

length :: LFormula k a a0 -> Int

elem :: Eq a0 => a0 -> LFormula k a a0 -> Bool

maximum :: Ord a0 => LFormula k a a0 -> a0

minimum :: Ord a0 => LFormula k a a0 -> a0

sum :: Num a0 => LFormula k a a0 -> a0

product :: Num a0 => LFormula k a a0 -> a0

Traversable (LFormula k a)

Defined in Zsyntax.Labelled.Formula

Methods

traverse :: Applicative f => (a0 -> f b) -> LFormula k a a0 -> f (LFormula k a b)

sequenceA :: Applicative f => LFormula k a (f a0) -> f (LFormula k a a0)

mapM :: Monad m => (a0 -> m b) -> LFormula k a a0 -> m (LFormula k a b)

sequence :: Monad m => LFormula k a (m a0) -> m (LFormula k a a0)

(Show a, Show l) => Show (LFormula k a l)

Defined in Zsyntax.Labelled.Formula

Methods

showsPrec :: Int -> LFormula k a l -> ShowS

show :: LFormula k a l -> String

showList :: [LFormula k a l] -> ShowS

ppLFormula :: (a -> String) -> LFormula k a l -> String

Pretty-print labelled formulas, given a way to pretty-print its atoms.

Note that this function ignores labels, for which one should use the Show instance.

elemBase :: Ord a => LFormula k a l -> ElemBase a

Returns the elementary base of a labelled formula.

label :: LFormula k a l -> Label a l

Returns the label of a labelled formula.

frmlHetEq :: (Eq a, Eq l) => LFormula k1 a l -> LFormula k2 a l -> Bool

Heterogeneous equality test between labelled formulas.

This function just compares the formulas' labels for equality, under the assumption that labels have been assigned in a sensible way.

frmlHetOrd :: (Ord a, Ord l) => LFormula k1 a l -> LFormula k2 a l -> Ordering

Heterogeneous comparison between labelled formulas.

This function just compares the formulas' labels, under the assumption that labels have been assigned in a sensible way.

deepHetComp :: (Ord a, Ord l) => LFormula k1 a l -> LFormula k2 a l -> Ordering

Returns the result of a deep heterogeneous comparison between two labelled formulas.

Comparison is "deep" in the sense that is considers the entire recursive structure of formulas. This is unlike frmlHetOrd, which only compares labels.

Labelled axioms

data LAxiom a l

Constructors

LAx (BFormula a l) (ReactionList a) (BFormula a l) l

Instances

Functor (LAxiom a)

Defined in Zsyntax.Labelled.Formula

Methods

fmap :: (a0 -> b) -> LAxiom a a0 -> LAxiom a b

(<$) :: a0 -> LAxiom a b -> LAxiom a a0

Foldable (LAxiom a)

Defined in Zsyntax.Labelled.Formula

Methods

fold :: Monoid m => LAxiom a m -> m

foldMap :: Monoid m => (a0 -> m) -> LAxiom a a0 -> m

foldr :: (a0 -> b -> b) -> b -> LAxiom a a0 -> b

foldr' :: (a0 -> b -> b) -> b -> LAxiom a a0 -> b

foldl :: (b -> a0 -> b) -> b -> LAxiom a a0 -> b

foldl' :: (b -> a0 -> b) -> b -> LAxiom a a0 -> b

foldr1 :: (a0 -> a0 -> a0) -> LAxiom a a0 -> a0

foldl1 :: (a0 -> a0 -> a0) -> LAxiom a a0 -> a0

toList :: LAxiom a a0 -> [a0]

null :: LAxiom a a0 -> Bool

length :: LAxiom a a0 -> Int

elem :: Eq a0 => a0 -> LAxiom a a0 -> Bool

maximum :: Ord a0 => LAxiom a a0 -> a0

minimum :: Ord a0 => LAxiom a a0 -> a0

sum :: Num a0 => LAxiom a a0 -> a0

product :: Num a0 => LAxiom a a0 -> a0

Traversable (LAxiom a)

Defined in Zsyntax.Labelled.Formula

Methods

traverse :: Applicative f => (a0 -> f b) -> LAxiom a a0 -> f (LAxiom a b)

sequenceA :: Applicative f => LAxiom a (f a0) -> f (LAxiom a a0)

mapM :: Monad m => (a0 -> m b) -> LAxiom a a0 -> m (LAxiom a b)

sequence :: Monad m => LAxiom a (m a0) -> m (LAxiom a a0)

Eq l => Eq (LAxiom a l)

Defined in Zsyntax.Labelled.Formula

Methods

(==) :: LAxiom a l -> LAxiom a l -> Bool

(/=) :: LAxiom a l -> LAxiom a l -> Bool

Ord l => Ord (LAxiom a l)

Defined in Zsyntax.Labelled.Formula

Methods

compare :: LAxiom a l -> LAxiom a l -> Ordering

(<) :: LAxiom a l -> LAxiom a l -> Bool

(<=) :: LAxiom a l -> LAxiom a l -> Bool

(>) :: LAxiom a l -> LAxiom a l -> Bool

(>=) :: LAxiom a l -> LAxiom a l -> Bool

max :: LAxiom a l -> LAxiom a l -> LAxiom a l

min :: LAxiom a l -> LAxiom a l -> LAxiom a l

(Show a, Show l) => Show (LAxiom a l)

Defined in Zsyntax.Labelled.Formula

Methods

showsPrec :: Int -> LAxiom a l -> ShowS

show :: LAxiom a l -> String

showList :: [LAxiom a l] -> ShowS

axLabel :: LAxiom a l -> l

Returns the label of a labelled axiom.

axToFormula :: Ord a => LAxiom a l -> LFormula KImpl a l

Converts a labelled axiom to a labelled formula.

ppLAxiom :: Ord a => (a -> String) -> LAxiom a l -> String

Pretty-prints a labelled axiom, given a way to pretty-print its atoms.

Note that this function ignores labels, for which one should rely on the Show instance.

Opaque formulas

data Opaque a l

Type of opaque formulas, that is, those for which we do not care about their formula kind.

Constructors

O (LFormula k a l)

Instances

(Eq l, Eq a) => Eq (Opaque a l)

Defined in Zsyntax.Labelled.Formula

Methods

(==) :: Opaque a l -> Opaque a l -> Bool

(/=) :: Opaque a l -> Opaque a l -> Bool

(Ord l, Ord a) => Ord (Opaque a l)

Defined in Zsyntax.Labelled.Formula

Methods

compare :: Opaque a l -> Opaque a l -> Ordering

(<) :: Opaque a l -> Opaque a l -> Bool

(<=) :: Opaque a l -> Opaque a l -> Bool

(>) :: Opaque a l -> Opaque a l -> Bool

(>=) :: Opaque a l -> Opaque a l -> Bool

max :: Opaque a l -> Opaque a l -> Opaque a l

min :: Opaque a l -> Opaque a l -> Opaque a l

(Show a, Show l) => Show (Opaque a l)

Defined in Zsyntax.Labelled.Formula

Methods

showsPrec :: Int -> Opaque a l -> ShowS

show :: Opaque a l -> String

showList :: [Opaque a l] -> ShowS

withOpaque :: (forall k. LFormula k a l -> b) -> Opaque a l -> b

oConj :: Opaque a l -> Opaque a l -> l -> LFormula KConj a l

Constructs the conjunction of two opaque formulas. The result is a provably conjunctive labelled formula.

oImpl :: Opaque a l -> ElemBase a -> ReactionList a -> Opaque a l -> l -> LFormula KImpl a l

Constructs the Zsyntax conditional (aka linear implication) between two opaque formulas, whose reaction is described by a given elementary base and reaction list. The result is a provably implicational labelled formula.

Basic formulas

data BFormula a l

Type of basic formulas. A basic formula is one composed of conjunctions of atoms.

Constructors

BAtom a

BConj (BFormula a l) (BFormula a l) l

Instances

Functor (BFormula a)

Defined in Zsyntax.Labelled.Formula

Methods

fmap :: (a0 -> b) -> BFormula a a0 -> BFormula a b

(<$) :: a0 -> BFormula a b -> BFormula a a0

Foldable (BFormula a)

Defined in Zsyntax.Labelled.Formula

Methods

fold :: Monoid m => BFormula a m -> m

foldMap :: Monoid m => (a0 -> m) -> BFormula a a0 -> m

foldr :: (a0 -> b -> b) -> b -> BFormula a a0 -> b

foldr' :: (a0 -> b -> b) -> b -> BFormula a a0 -> b

foldl :: (b -> a0 -> b) -> b -> BFormula a a0 -> b

foldl' :: (b -> a0 -> b) -> b -> BFormula a a0 -> b

foldr1 :: (a0 -> a0 -> a0) -> BFormula a a0 -> a0

foldl1 :: (a0 -> a0 -> a0) -> BFormula a a0 -> a0

toList :: BFormula a a0 -> [a0]

null :: BFormula a a0 -> Bool

length :: BFormula a a0 -> Int

elem :: Eq a0 => a0 -> BFormula a a0 -> Bool

maximum :: Ord a0 => BFormula a a0 -> a0

minimum :: Ord a0 => BFormula a a0 -> a0

sum :: Num a0 => BFormula a a0 -> a0

product :: Num a0 => BFormula a a0 -> a0

Traversable (BFormula a)

Defined in Zsyntax.Labelled.Formula

Methods

traverse :: Applicative f => (a0 -> f b) -> BFormula a a0 -> f (BFormula a b)

sequenceA :: Applicative f => BFormula a (f a0) -> f (BFormula a a0)

mapM :: Monad m => (a0 -> m b) -> BFormula a a0 -> m (BFormula a b)

sequence :: Monad m => BFormula a (m a0) -> m (BFormula a a0)

(Show a, Show l) => Show (BFormula a l)

Defined in Zsyntax.Labelled.Formula

Methods

showsPrec :: Int -> BFormula a l -> ShowS

show :: BFormula a l -> String

showList :: [BFormula a l] -> ShowS

bAtom :: a -> BFormula a l

Constructs a basic formula from a logical atom.

bConj :: l -> BFormula a l -> BFormula a l -> BFormula a l

Constructs the conjunction of two basic formulas, with a given label.

bfToFormula :: BFormula a l -> Opaque a l

Returns the labelled formula corresponding to a given basic formula.

Note that the result formula is opaque, since it could be an atom as well as a conjunction, and thus has no determined index.

bfToAtoms :: BFormula a l -> NonEmpty a

Unrolls a basic formula, discarding all labels and returning a (non-empty) list of all its constituent logical atoms.

maybeBFormula :: LFormula k a l -> Maybe (BFormula a l)

Decides whether the input labelled formula is a basic formula, and if so, it returns it wrapped in Just as a proper basic formula.