Safe Haskell	None
Language	Haskell2010

Zsyntax.Labelled.Formula

Contents

Labelled formulas
Labelled axioms
Opaque formulas
Basic formulas

Synopsis

data FKind
- = KAtom
- | KConj
- | KImpl
data Label a l
- = L l
- | A a
newtype ElemBase a = ElemBase {
- unEB :: MultiSet a
}
type ReactionList a = RList (ElemBase a) (CtrlSet a)
data LFormula :: FKind -> * -> * -> * where
- 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
ppLFormula :: (a -> String) -> LFormula k a l -> String
elemBase :: Ord a => LFormula k a l -> ElemBase a
label :: LFormula k a l -> Label a l
frmlHetEq :: (Eq a, Eq l) => LFormula k1 a l -> LFormula k2 a l -> Bool
frmlHetOrd :: (Ord a, Ord l) => LFormula k1 a l -> LFormula k2 a l -> Ordering
deepHetComp :: (Ord a, Ord l) => LFormula k1 a l -> LFormula k2 a l -> Ordering
data LAxiom a l = LAx (BFormula a l) (ReactionList a) (BFormula a l) l
axLabel :: LAxiom a l -> l
axToFormula :: Ord a => LAxiom a l -> LFormula KImpl a l
ppLAxiom :: Ord a => (a -> String) -> LAxiom a l -> String
data Opaque a l = O (LFormula k a l)
withOpaque :: (forall k. LFormula k a l -> b) -> Opaque a l -> b
oConj :: Opaque a l -> Opaque a l -> l -> LFormula KConj a l
oImpl :: Opaque a l -> ElemBase a -> ReactionList a -> Opaque a l -> l -> LFormula KImpl a l
data BFormula a l
- = BAtom a
- | BConj (BFormula a l) (BFormula a l) l
bAtom :: a -> BFormula a l
bConj :: l -> BFormula a l -> BFormula a l -> BFormula a l
bfToFormula :: BFormula a l -> Opaque a l
bfToAtoms :: BFormula a l -> NonEmpty a
maybeBFormula :: LFormula k a l -> Maybe (BFormula a l)

Documentation

data FKind Source #

Constructors

KAtom
KConj
KImpl

data Label a l Source #

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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 Source #

Constructors

ElemBase
Fields unEB :: MultiSet a

Instances

Eq a => Eq (ElemBase a) Source #
Instance details Defined in Zsyntax.Labelled.Formula Methods (==) :: ElemBase a -> ElemBase a -> Bool # (/=) :: ElemBase a -> ElemBase a -> Bool #
Ord a => Ord (ElemBase a) Source #
Instance details 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) Source #
Instance details Defined in Zsyntax.Labelled.Formula Methods showsPrec :: Int -> ElemBase a -> ShowS # show :: ElemBase a -> String # showList :: [ElemBase a] -> ShowS #
Ord a => Semigroup (ElemBase a) Source #
Instance details 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) Source #
Instance details 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) Source #

Labelled formulas

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

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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 Source #

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 Source #

Returns the elementary base of a labelled formula.

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

Returns the label of a labelled formula.

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

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 Source #

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 Source #

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 Source #

Constructors

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

Instances

Functor (LAxiom a) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 Source #

Returns the label of a labelled axiom.

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

Converts a labelled axiom to a labelled formula.

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

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 Source #

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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 Source #

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

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 Source #

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 Source #

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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 Source #

Constructs a basic formula from a logical atom.

bConj :: l -> BFormula a l -> BFormula a l -> BFormula a l Source #

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

bfToFormula :: BFormula a l -> Opaque a l Source #

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 Source #

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) Source #

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