Safe Haskell	None
Language	Haskell2010

Zsyntax.Formula

Synopsis

data BioFormula a
- = BioAtom a
- | BioInter (BioFormula a) (BioFormula a)
normalize :: Ord a => BioFormula a -> NonEmpty a
ppBioFormula :: (a -> String) -> BioFormula a -> String
newtype Axiom a = Axiom {
- unSA :: LAxiom a ()
}
axForget :: LAxiom a l -> Axiom a
axiom :: NonEmpty a -> ReactionList a -> NonEmpty a -> Axiom a
axiom' :: BFormula a () -> ReactionList a -> BFormula a () -> Axiom a
data Formula a = Formula (LFormula k a ())
ppFormula :: (a -> String) -> Formula a -> String
atom :: a -> Formula a
lToS :: LFormula k a l -> Formula a
conj :: Formula a -> Formula a -> Formula a
impl :: Formula a -> ElemBase a -> ReactionList a -> Formula a -> Formula a
data Sequent a = SQ {
- _sqUC :: Set (Axiom a)
- _sqLC :: MultiSet (Formula a)
- _sqConcl :: Formula a
}
nuLabel :: (Enum l, MonadState l m) => m l
neutralize :: (MonadState l m, Enum l, Ord a, Ord l) => Sequent a -> m (GoalNSequent a l)
maybeNeutral :: Opaque a l -> Either (Neutral a l) [Opaque a l]
neutralizeOs :: (Ord a, Ord l) => [Opaque a l] -> [Neutral a l]
neutralizeFormula :: (MonadState l m, Enum l, Ord a, Ord l) => Formula a -> m [Neutral a l]

Documentation

data BioFormula a Source #

Type of biochemical (non-logical) formulas, which constitute the logical atoms of logical formulas of Zsyntax. It is parameterized over the type of biochemical atoms.

Constructors

BioAtom a
BioInter (BioFormula a) (BioFormula a)

Instances

Functor BioFormula Source #
Instance details Defined in Zsyntax.Formula Methods fmap :: (a -> b) -> BioFormula a -> BioFormula b # (<$) :: a -> BioFormula b -> BioFormula a #
Foldable BioFormula Source #
Instance details Defined in Zsyntax.Formula Methods fold :: Monoid m => BioFormula m -> m # foldMap :: Monoid m => (a -> m) -> BioFormula a -> m # foldr :: (a -> b -> b) -> b -> BioFormula a -> b # foldr' :: (a -> b -> b) -> b -> BioFormula a -> b # foldl :: (b -> a -> b) -> b -> BioFormula a -> b # foldl' :: (b -> a -> b) -> b -> BioFormula a -> b # foldr1 :: (a -> a -> a) -> BioFormula a -> a # foldl1 :: (a -> a -> a) -> BioFormula a -> a # toList :: BioFormula a -> [a] # null :: BioFormula a -> Bool # length :: BioFormula a -> Int # elem :: Eq a => a -> BioFormula a -> Bool # maximum :: Ord a => BioFormula a -> a # minimum :: Ord a => BioFormula a -> a # sum :: Num a => BioFormula a -> a # product :: Num a => BioFormula a -> a #
Traversable BioFormula Source #
Instance details Defined in Zsyntax.Formula Methods traverse :: Applicative f => (a -> f b) -> BioFormula a -> f (BioFormula b) # sequenceA :: Applicative f => BioFormula (f a) -> f (BioFormula a) # mapM :: Monad m => (a -> m b) -> BioFormula a -> m (BioFormula b) # sequence :: Monad m => BioFormula (m a) -> m (BioFormula a) #
Ord a => Eq (BioFormula a) Source #	Custom equality instance for biological atoms. It includes commutativity of the biological interaction operator.
Instance details Defined in Zsyntax.Formula Methods (==) :: BioFormula a -> BioFormula a -> Bool # (/=) :: BioFormula a -> BioFormula a -> Bool #
Ord a => Ord (BioFormula a) Source #
Instance details Defined in Zsyntax.Formula Methods compare :: BioFormula a -> BioFormula a -> Ordering # (<) :: BioFormula a -> BioFormula a -> Bool # (<=) :: BioFormula a -> BioFormula a -> Bool # (>) :: BioFormula a -> BioFormula a -> Bool # (>=) :: BioFormula a -> BioFormula a -> Bool # max :: BioFormula a -> BioFormula a -> BioFormula a # min :: BioFormula a -> BioFormula a -> BioFormula a #
Show a => Show (BioFormula a) Source #
Instance details Defined in Zsyntax.Formula Methods showsPrec :: Int -> BioFormula a -> ShowS # show :: BioFormula a -> String # showList :: [BioFormula a] -> ShowS #
Semigroup (BioFormula a) Source #
Instance details Defined in Zsyntax.Formula Methods (<>) :: BioFormula a -> BioFormula a -> BioFormula a # sconcat :: NonEmpty (BioFormula a) -> BioFormula a # stimes :: Integral b => b -> BioFormula a -> BioFormula a #

normalize :: Ord a => BioFormula a -> NonEmpty a Source #

ppBioFormula :: (a -> String) -> BioFormula a -> String Source #

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

>>> ppBioFormula id (BioAtom "foo" <> BioAtom "bar" <> BioAtom "baz")
"((foo ⊙ bar) ⊙ baz)"

newtype Axiom a Source #

Type of logical axioms of Zsyntax.

Constructors

Axiom
Fields unSA :: LAxiom a ()

Instances

Ord a => Eq (Axiom a) Source #
Instance details Defined in Zsyntax.Formula Methods (==) :: Axiom a -> Axiom a -> Bool # (/=) :: Axiom a -> Axiom a -> Bool #
Ord a => Ord (Axiom a) Source #
Instance details Defined in Zsyntax.Formula Methods compare :: Axiom a -> Axiom a -> Ordering # (<) :: Axiom a -> Axiom a -> Bool # (<=) :: Axiom a -> Axiom a -> Bool # (>) :: Axiom a -> Axiom a -> Bool # (>=) :: Axiom a -> Axiom a -> Bool # max :: Axiom a -> Axiom a -> Axiom a # min :: Axiom a -> Axiom a -> Axiom a #
Show a => Show (Axiom a) Source #
Instance details Defined in Zsyntax.Formula Methods showsPrec :: Int -> Axiom a -> ShowS # show :: Axiom a -> String # showList :: [Axiom a] -> ShowS #

axForget :: LAxiom a l -> Axiom a Source #

axiom :: NonEmpty a -> ReactionList a -> NonEmpty a -> Axiom a Source #

Constructs an axiom from non-empty lists of logical atoms as premise and conclusion.

axiom' :: BFormula a () -> ReactionList a -> BFormula a () -> Axiom a Source #

data Formula a Source #

Type of logical formulas of Zsyntax, parameterized by the type of atoms (which are typically BioFormulas).

Constructors

Formula (LFormula k a ())

Instances

Ord a => Eq (Formula a) Source #
Instance details Defined in Zsyntax.Formula Methods (==) :: Formula a -> Formula a -> Bool # (/=) :: Formula a -> Formula a -> Bool #
Ord a => Ord (Formula a) Source #
Instance details Defined in Zsyntax.Formula Methods compare :: Formula a -> Formula a -> Ordering # (<) :: Formula a -> Formula a -> Bool # (<=) :: Formula a -> Formula a -> Bool # (>) :: Formula a -> Formula a -> Bool # (>=) :: Formula a -> Formula a -> Bool # max :: Formula a -> Formula a -> Formula a # min :: Formula a -> Formula a -> Formula a #
Show a => Show (Formula a) Source #
Instance details Defined in Zsyntax.Formula Methods showsPrec :: Int -> Formula a -> ShowS # show :: Formula a -> String # showList :: [Formula a] -> ShowS #

ppFormula :: (a -> String) -> Formula a -> String Source #

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

atom :: a -> Formula a Source #

Constructs an atomic formula from a logical atom.

lToS :: LFormula k a l -> Formula a Source #

conj :: Formula a -> Formula a -> Formula a Source #

Constructs the conjunction of two formulas.

impl :: Formula a -> ElemBase a -> ReactionList a -> Formula a -> Formula a Source #

Constructs a Zsyntax conditional (aka linear implication) between two formulas, whose associated biochemical reaction is described by a given elementary base and reaction list.

data Sequent a Source #

Type of ZBS sequents.

Constructors

SQ
Fields _sqUC :: Set (Axiom a) _sqLC :: MultiSet (Formula a) _sqConcl :: Formula a

Instances

Show a => Show (Sequent a) Source #
Instance details Defined in Zsyntax.Formula Methods showsPrec :: Int -> Sequent a -> ShowS # show :: Sequent a -> String # showList :: [Sequent a] -> ShowS #

nuLabel :: (Enum l, MonadState l m) => m l Source #

neutralize :: (MonadState l m, Enum l, Ord a, Ord l) => Sequent a -> m (GoalNSequent a l) Source #

Turns a sequent into a labelled goal sequent.

maybeNeutral :: Opaque a l -> Either (Neutral a l) [Opaque a l] Source #

neutralizeOs :: (Ord a, Ord l) => [Opaque a l] -> [Neutral a l] Source #

neutralizeFormula :: (MonadState l m, Enum l, Ord a, Ord l) => Formula a -> m [Neutral a l] Source #