-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Automated theorem prover for the Zsyntax biochemical calculus
--   
--   An automated theorem prover for Zsyntax, a logical calculus for
--   molecular biology inspired by linear logic, that can be used to
--   automatically verify biological pathways expressed as logical
--   sequents. The prover implements automatic proof search for the Zsyntax
--   sequent calculus (ZBS), a logical calculus for a context-sensitive
--   fragment of multiplicative linear logic where sequents are decorated
--   so to account for the biochemical constraints. The theory behind the
--   Zsyntax sequent calculus and its proof search procedure is developed
--   in F. Sestini, S. Crafa, Proof-search in a context-sensitive logic for
--   molecular biology, Journal of Logic and Computation, 2018
--   (<a>https://doi.org/10.1093/logcom/exy028</a>).
@package zsyntax
@version 0.2.0.0

module Otter.Rule

-- | An inference rule schema is just a curried n-ary function where n is
--   an unbounded, unspecified number of input premises, possibly zero (in
--   that case, the rule is an axiom). A <a>Rule</a> element may represent
--   three possible situations:
--   
--   <ol>
--   <li>A failing computation which produces nothing; this is the
--   degenerate case of a rule schema that always fails to match, and also
--   what enables to make <a>Rule</a> an instance of <a>Alternative</a>,
--   <a>MonadPlus</a>, and <a>MonadFail</a>.</li>
--   <li>A successful computation that produces a 0-ary function, i.e. an
--   axiom;</li>
--   <li>A successful computation that produces a unary function, that is,
--   a function accepting one argument and possibly returning a new
--   <a>Rule</a>. Applying such a function to an input corresponds to
--   "matching" the first premise of the rule schema against a candidate
--   input. The result is either a matching failure or a new, partially
--   applied rule.</li>
--   </ol>
newtype Rule a b
Rule :: Maybe (Either b (a -> Rule a b)) -> Rule a b
[unRule] :: Rule a b -> Maybe (Either b (a -> Rule a b))
type ProperRule a b = a -> Rule a b

-- | Constructs a single-premise rule from a matching function.
match :: (a -> Maybe b) -> Rule a b
apply :: ProperRule a b -> a -> ([b], [ProperRule a b])
arrowDimap :: (a -> b) -> (c -> d) -> (b -> c) -> a -> d
relDimap :: (a -> b) -> (c -> d) -> Rule b c -> Rule a d
instance GHC.Base.Applicative (Otter.Rule.Rule a)
instance GHC.Base.Functor (Otter.Rule.Rule a)
instance GHC.Base.Monad (Otter.Rule.Rule a)
instance GHC.Base.Alternative (Otter.Rule.Rule a)
instance GHC.Base.MonadPlus (Otter.Rule.Rule a)
instance Control.Monad.Fail.MonadFail (Otter.Rule.Rule a)

module Otter.Internal.Structures

-- | Stages of proof search
data Stage

-- | Initial node
Initial :: Stage

-- | Active node
Active :: Stage

-- | Inactive node
Inactive :: Stage

-- | Conclusion node
Concl :: Stage

-- | Forward subsumption-checked
FSChecked :: Stage

-- | Backward subsumption-checked
BSChecked :: Stage

-- | Global index node
GlIndex :: Stage

-- | Goal node
Goal :: Stage

-- | Type of search nodes in the search space, given by a node together
--   with a proof search stage.
data SearchNode :: Stage -> * -> *
type ActiveNode n = SearchNode Active n
type FSCheckedNode n = SearchNode FSChecked n
type BSCheckedNode n = SearchNode BSChecked n
type InactiveNode n = SearchNode Inactive n
data ActiveNodes n
data InactiveNodes n
type ConclNode n = SearchNode Concl n
data GlobalIndex n

-- | Type of elements that represent the result of applying an inference
--   rule.
--   
--   Such application may either fail, succeed with a value (when the rule
--   has been fully applied), or succeed with a function (when the rule is
--   only partially applied and has still some premises to match).
type SearchRule n = Rule (ActiveNode n) (ConclNode n)

-- | Type of inference rules. Axioms are not considered rules in this case,
--   so a rule takes at least one premise. Hence the corresponding type is
--   a function from a premise sequent to a rule application result.
type SearchProperRule n = ProperRule (ActiveNode n) (ConclNode n)
class Subsumable n
subsumes :: Subsumable n => n -> n -> Bool
initIsFSCheckd :: SearchNode Initial n -> FSCheckedNode n
initIsBSCheckd :: SearchNode Initial n -> BSCheckedNode n
initialize :: n -> SearchNode Initial n
removeSubsumedByOp :: Subsumable n => FSCheckedNode n -> InactiveNodes n -> (InactiveNodes n, BSCheckedNode n)
fwdSubsumes :: Subsumable n => GlobalIndex n -> SearchNode Concl n -> Maybe (FSCheckedNode n)
activate :: ActiveNodes n -> InactiveNode n -> (ActiveNodes n, ActiveNode n)
popInactiveOp :: InactiveNodes n -> Maybe (InactiveNodes n, InactiveNode n)
addToInactives :: InactiveNodes n -> GlobalIndex n -> BSCheckedNode n -> (InactiveNodes n, GlobalIndex n)
foldActives :: (forall f. Foldable f => f (ActiveNode n) -> b) -> ActiveNodes n -> b
mkGoal :: n -> SearchNode Goal n
emptyActives :: ActiveNodes n
emptyInactives :: InactiveNodes n
emptyGI :: GlobalIndex n
toProperRule :: (n -> Rule n n) -> SearchProperRule n
extractNode :: SearchNode s seq -> seq
instance GHC.Show.Show a => GHC.Show.Show (Otter.Internal.Structures.SearchNode s a)
instance Data.Foldable.Foldable Otter.Internal.Structures.GlobalIndex

module Otter.SearchRes

-- | Type representing the result of proof search. Every element in the
--   list corresponds to the result of analysing node in the search space
--   by the search algorithm. The result is <a>Res</a> in the positive case
--   the node is a goal node, or <a>Delay</a> in the negative case.
--   
--   The search agorithm produces an element of `<a>SearchRes</a> a`
--   lazily, inserting <a>Delay</a> constructors to ensure that the
--   computation is productive even in the case no goal node is found in
--   the search space. This allows to perform proof search in an on-demand
--   fashion, possibly giving up after a certain number of <a>Delay</a>s.
type SearchRes a = [Res a]
data Res a
Res :: a -> Res a
Delay :: Res a

-- | Type of the result of <a>extractResults</a>, which extracts all
--   positive search results from a search result stream. An element of
--   `Extraction a` is either a non-empty list of positive results, or an
--   element of <tt>SpaceExhausted</tt> giving a reason why no result was
--   found.
data Extraction a
AllResults :: NonEmpty a -> Extraction a
NoResults :: FailureReason -> Extraction a

-- | Type of reasons why no result can be extracted from a search result
--   stream.
--   
--   Either the search space has been exhaustively searched and no result
--   was found (the query is not a theorem), or the search was terminated
--   preemptively according to an upper bound imposed on the maximum depth
--   of the search space.
data FailureReason
NotATheorem :: FailureReason
SpaceTooBig :: FailureReason

-- | Extract all the positive results from a search result stream, stopping
--   if no result is found after the given number of delays.
extractResults :: Int -> SearchRes a -> Extraction a

-- | Delays a search result stream.
--   
--   <pre>
--   delay x == Delay : x
--   </pre>
delay :: SearchRes a -> SearchRes a

-- | Appends a result to a search result stream.
--   
--   <pre>
--   cons x y = Res x : y
--   </pre>
cons :: a -> SearchRes a -> SearchRes a
instance GHC.Base.Functor Otter.SearchRes.Res

module Otter.Internal.Search
data ProverState n
PS :: [SearchProperRule n] -> ActiveNodes n -> InactiveNodes n -> GlobalIndex n -> (n -> Bool) -> ProverState n
[_rules] :: ProverState n -> [SearchProperRule n]
[_actives] :: ProverState n -> ActiveNodes n
[_inactives] :: ProverState n -> InactiveNodes n
[_index] :: ProverState n -> GlobalIndex n
[_isGoal] :: ProverState n -> n -> Bool
type Prover s g a = State (ProverState s) a

-- | Result type of matching a list of rules to an input sequent.
type RuleAppRes n = ([ConclNode n], [SearchProperRule n])
popInactive :: Prover s g (Maybe (ActiveNode s))
getActives :: Prover s g (ActiveNodes s)
getRules :: Prover s g [SearchProperRule s]
isGoalM :: FSCheckedNode s -> Prover s g (Maybe (FSCheckedNode s))
haveGoal :: [FSCheckedNode s] -> Prover s g (Maybe (FSCheckedNode s))
filterUnsubsumed :: Subsumable s => [ConclNode s] -> Prover s g [SearchNode FSChecked s]
isNotFwdSubsumed :: Subsumable s => ConclNode s -> Prover s g (Maybe (SearchNode FSChecked s))
removeSubsumedBy :: Subsumable s => SearchNode FSChecked s -> Prover s g (SearchNode BSChecked s)
addRule :: SearchProperRule s -> Prover s g ()
addInactive :: SearchNode BSChecked s -> Prover s g ()
percolate :: ActiveNodes s -> [SearchProperRule s] -> RuleAppRes s
processNewActive :: ActiveNode s -> Prover s g (RuleAppRes s)
merge :: Maybe (SearchNode s a) -> SearchRes a -> SearchRes a
loop :: Subsumable s => Prover s g (SearchRes s)
doSearch :: Subsumable s => [SearchNode Initial s] -> [SearchProperRule s] -> Prover s g (SearchRes s)
search :: Subsumable s => [s] -> [s -> Rule s s] -> (s -> Bool) -> (SearchRes s, [s])

module Otter
class Subsumable n
subsumes :: Subsumable n => n -> n -> Bool
search :: Subsumable s => [s] -> [s -> Rule s s] -> (s -> Bool) -> (SearchRes s, [s])

module Zsyntax.ReactionList
data CtrlType
Regular :: CtrlType
SupersetClosed :: CtrlType
data CtrlSetCtxt af
CSC :: CtrlType -> MultiSet af -> CtrlSetCtxt af
[_cscType] :: CtrlSetCtxt af -> CtrlType
[_cscCtxt] :: CtrlSetCtxt af -> MultiSet af

-- | A control set is a set of linear contexts made up of atomic formulas,
--   that is, multisets of formulas of the bonding language.
--   
--   For a context C in a control set S we may want to consider its
--   superset closure, that is, have that C' is in S for all superset C' of
--   C. We therefore distinguish between superset-closed contexts and
--   normal contexts in a control set. Actually, superset-closed contexts
--   are the only way to specify infinite control sets.
newtype CtrlSet af
CS :: Set (CtrlSetCtxt af) -> CtrlSet af
[unCS] :: CtrlSet af -> Set (CtrlSetCtxt af)
fromCSCtxts :: (Foldable f, Ord af) => f (CtrlSetCtxt af) -> CtrlSet af
toCtxtList :: CtrlSet af -> [CtrlSetCtxt af]

-- | Checks whether a linear context "respects" a control set context.
respectsCC :: Ord af => MultiSet af -> CtrlSetCtxt af -> Bool

-- | Checks whether a linear context "respects" a control set, that is, if
--   it respects all the control set contexts.
msRespectsCS :: Ord af => MultiSet af -> CtrlSet af -> Bool

-- | A reaction list is a list of pairs, where in each pair the first
--   component is an elementary base, and the second component is a control
--   set.
newtype RList eb cs
RL :: [(eb, cs)] -> RList eb cs
[unRL] :: RList eb cs -> [(eb, cs)]
justCS :: Monoid eb => cs -> RList eb cs

-- | Extends a reaction list with an elementary base.
extend :: Semigroup eb => eb -> RList eb cs -> RList eb cs

-- | Checks whether an elementary base "respects" a reaction list, given a
--   function to check whether the base "respects" the list's control sets.
respectsRList :: Semigroup eb => (eb -> cs -> Bool) -> eb -> RList eb cs -> Bool
instance (GHC.Show.Show eb, GHC.Show.Show cs) => GHC.Show.Show (Zsyntax.ReactionList.RList eb cs)
instance GHC.Base.Monoid (Zsyntax.ReactionList.RList eb cs)
instance GHC.Base.Semigroup (Zsyntax.ReactionList.RList eb cs)
instance (GHC.Classes.Ord eb, GHC.Classes.Ord cs) => GHC.Classes.Ord (Zsyntax.ReactionList.RList eb cs)
instance (GHC.Classes.Eq eb, GHC.Classes.Eq cs) => GHC.Classes.Eq (Zsyntax.ReactionList.RList eb cs)
instance GHC.Show.Show af => GHC.Show.Show (Zsyntax.ReactionList.CtrlSet af)
instance GHC.Classes.Ord af => GHC.Base.Monoid (Zsyntax.ReactionList.CtrlSet af)
instance GHC.Classes.Ord af => GHC.Base.Semigroup (Zsyntax.ReactionList.CtrlSet af)
instance GHC.Classes.Ord af => GHC.Classes.Ord (Zsyntax.ReactionList.CtrlSet af)
instance GHC.Classes.Eq af => GHC.Classes.Eq (Zsyntax.ReactionList.CtrlSet af)
instance GHC.Show.Show af => GHC.Show.Show (Zsyntax.ReactionList.CtrlSetCtxt af)
instance GHC.Classes.Ord af => GHC.Classes.Ord (Zsyntax.ReactionList.CtrlSetCtxt af)
instance GHC.Classes.Eq af => GHC.Classes.Eq (Zsyntax.ReactionList.CtrlSetCtxt af)
instance GHC.Show.Show Zsyntax.ReactionList.CtrlType
instance GHC.Classes.Ord Zsyntax.ReactionList.CtrlType
instance GHC.Classes.Eq Zsyntax.ReactionList.CtrlType

module Zsyntax.Labelled.Formula
data FKind
KAtom :: FKind
KConj :: FKind
KImpl :: FKind

-- | Type of formula labels. Note that logical atoms are their own labels.
data Label a l

-- | Regular label
L :: l -> Label a l

-- | Logical atom
A :: a -> Label a l
newtype ElemBase a
ElemBase :: MultiSet a -> ElemBase a
[unEB] :: ElemBase a -> MultiSet a
type ReactionList a = RList (ElemBase a) (CtrlSet a)

-- | Type of labelled formulas, indexed by a formula kind and parameterized
--   by the type of the labels and of the logical atoms.
data LFormula :: FKind -> * -> * -> *
[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

-- | Pretty-print labelled formulas, given a way to pretty-print its atoms.
--   
--   Note that this function ignores labels, for which one should use the
--   <a>Show</a> instance.
ppLFormula :: (a -> String) -> LFormula k a l -> String

-- | Returns the elementary base of a labelled formula.
elemBase :: Ord a => LFormula k a l -> ElemBase a

-- | Returns the label of a labelled formula.
label :: LFormula k a l -> Label a l

-- | 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.
frmlHetEq :: (Eq a, Eq l) => LFormula k1 a l -> LFormula k2 a l -> Bool

-- | Heterogeneous comparison between labelled formulas.
--   
--   This function just compares the formulas' labels, 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

-- | 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 <a>frmlHetOrd</a>,
--   which only compares labels.
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 -> LAxiom a l

-- | Returns the label of a labelled axiom.
axLabel :: LAxiom a l -> l

-- | Converts a labelled axiom to a labelled formula.
axToFormula :: Ord a => LAxiom a l -> LFormula KImpl a l

-- | 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 <a>Show</a> instance.
ppLAxiom :: Ord a => (a -> String) -> LAxiom a l -> String

-- | Type of opaque formulas, that is, those for which we do not care about
--   their formula kind.
data Opaque a l
O :: LFormula k a l -> Opaque a l
withOpaque :: (forall k. LFormula k a l -> b) -> Opaque a l -> b

-- | Constructs the conjunction of two opaque formulas. The result is a
--   provably conjunctive labelled formula.
oConj :: Opaque a l -> Opaque a l -> l -> LFormula KConj 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.
oImpl :: Opaque a l -> ElemBase a -> ReactionList a -> Opaque a l -> l -> LFormula KImpl a l

-- | Type of basic formulas. A basic formula is one composed of
--   conjunctions of atoms.
data BFormula a l
BAtom :: a -> BFormula a l
BConj :: BFormula a l -> BFormula a l -> l -> BFormula a l

-- | Constructs a basic formula from a logical atom.
bAtom :: a -> BFormula a l

-- | Constructs the conjunction of two basic formulas, with a given label.
bConj :: l -> BFormula a l -> BFormula a l -> BFormula 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.
bfToFormula :: BFormula a l -> Opaque a l

-- | Unrolls a basic formula, discarding all labels and returning a
--   (non-empty) list of all its constituent logical atoms.
bfToAtoms :: BFormula a l -> NonEmpty a

-- | Decides whether the input labelled formula is a basic formula, and if
--   so, it returns it wrapped in <a>Just</a> as a proper basic formula.
maybeBFormula :: LFormula k a l -> Maybe (BFormula a l)
instance (GHC.Show.Show l, GHC.Show.Show a) => GHC.Show.Show (Zsyntax.Labelled.Formula.Label a l)
instance (GHC.Classes.Ord l, GHC.Classes.Ord a) => GHC.Classes.Ord (Zsyntax.Labelled.Formula.Label a l)
instance (GHC.Classes.Eq l, GHC.Classes.Eq a) => GHC.Classes.Eq (Zsyntax.Labelled.Formula.Label a l)
instance Data.Traversable.Traversable (Zsyntax.Labelled.Formula.LAxiom a)
instance Data.Foldable.Foldable (Zsyntax.Labelled.Formula.LAxiom a)
instance GHC.Base.Functor (Zsyntax.Labelled.Formula.LAxiom a)
instance (GHC.Show.Show a, GHC.Show.Show l) => GHC.Show.Show (Zsyntax.Labelled.Formula.LAxiom a l)
instance (GHC.Show.Show a, GHC.Show.Show l) => GHC.Show.Show (Zsyntax.Labelled.Formula.BFormula a l)
instance Data.Traversable.Traversable (Zsyntax.Labelled.Formula.BFormula a)
instance Data.Foldable.Foldable (Zsyntax.Labelled.Formula.BFormula a)
instance GHC.Base.Functor (Zsyntax.Labelled.Formula.BFormula a)
instance GHC.Show.Show a => GHC.Show.Show (Zsyntax.Labelled.Formula.ElemBase a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Zsyntax.Labelled.Formula.ElemBase a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Zsyntax.Labelled.Formula.ElemBase a)
instance GHC.Classes.Ord a => GHC.Base.Monoid (Zsyntax.Labelled.Formula.ElemBase a)
instance GHC.Classes.Ord a => GHC.Base.Semigroup (Zsyntax.Labelled.Formula.ElemBase a)
instance (GHC.Show.Show a, GHC.Show.Show l) => GHC.Show.Show (Zsyntax.Labelled.Formula.LFormula k a l)
instance GHC.Base.Functor (Zsyntax.Labelled.Formula.LFormula k a)
instance Data.Foldable.Foldable (Zsyntax.Labelled.Formula.LFormula k a)
instance Data.Traversable.Traversable (Zsyntax.Labelled.Formula.LFormula k a)
instance (GHC.Show.Show a, GHC.Show.Show l) => GHC.Show.Show (Zsyntax.Labelled.Formula.Opaque a l)
instance GHC.Classes.Eq l => GHC.Classes.Eq (Zsyntax.Labelled.Formula.LAxiom a l)
instance GHC.Classes.Ord l => GHC.Classes.Ord (Zsyntax.Labelled.Formula.LAxiom a l)
instance (GHC.Classes.Eq l, GHC.Classes.Eq a) => GHC.Classes.Eq (Zsyntax.Labelled.Formula.Opaque a l)
instance (GHC.Classes.Ord l, GHC.Classes.Ord a) => GHC.Classes.Ord (Zsyntax.Labelled.Formula.Opaque a l)

module Zsyntax.Labelled.Rule.Interface

-- | Type of labelled unrestricted contexts, i.e. sets of labelled axioms.
type UCtxt a l = Set (LAxiom a l)

-- | Type of labelled neutral contexts, i.e. multisets of neutral labelled
--   formulas.
type LCtxt a l = MultiSet (Neutral a l)

-- | Type of labelled sequents.
data LSequent a l
LS :: UCtxt a l -> LCtxt a l -> ReactionList a -> Opaque a l -> LSequent a l
[lsUCtxt] :: LSequent a l -> UCtxt a l
[lsLCtxt] :: LSequent a l -> LCtxt a l
[lsCty] :: LSequent a l -> ReactionList a
[lsConcl] :: LSequent a l -> Opaque a l
data SubCtxt a
SC :: [a] -> [a] -> SubCtxt a
[_scOnOnlyFirst] :: SubCtxt a -> [a]
[_scRestFirst] :: SubCtxt a -> [a]
subCtxtOf :: Ord a => Set a -> Set a -> SubCtxt a

-- | Predicate identifying those formula kinds corresponding to neutral
--   formulas.
class NeutralKind (k :: FKind)
decideNeutral :: NeutralKind k => Either (Dict (k ~ KAtom)) (Dict (k ~ KImpl))

-- | Type of neutral formulas, i.e. all formulas whose formula kind is
--   classified as neutral by <a>NeutralKind</a>.
data Neutral a l
N :: LFormula k a l -> Neutral a l
withMaybeNeutral :: LFormula k a l -> (NeutralKind k => b) -> (LFormula KConj a l -> b) -> b
withNeutral :: (forall k. NeutralKind k => LFormula k a l -> b) -> Neutral a l -> b
switchN :: (LFormula KAtom a l -> b) -> (LFormula KImpl a l -> b) -> Neutral a l -> b

-- | Linear contexts that appear in sequent schemas.
newtype SchemaLCtxt a l
SLC :: LCtxt a l -> SchemaLCtxt a l

-- | Type indicating the possible shapes of an active relation. An active
--   relation has the form
--   
--   act(delta ; omega ==&gt;_zeta xi)[...] -&gt; gamma' ; delta'
--   --&gt;&gt; res
--   
--   where either 1. xi is a formula, zeta is a control set, and res is
--   empty, or 2. xi is empty, zeta is empty, and res is a formula.
data ActCase
FullXiEmptyResult :: ActCase
EmptyXiFullResult :: ActCase

-- | Sequent schemas.
data SSchema :: * -> * -> ActCase -> *
[SSEmptyGoal] :: SchemaLCtxt a l -> SSchema a l EmptyXiFullResult
[SSFullGoal] :: SchemaLCtxt a l -> ReactionList a -> Opaque a l -> SSchema a l FullXiEmptyResult

-- | Pre-sequents to be used as match results.
data MatchRes :: * -> * -> ActCase -> *
[MREmptyGoal] :: UCtxt a l -> LCtxt a l -> MatchRes a l FullXiEmptyResult
[MRFullGoal] :: UCtxt a l -> LCtxt a l -> ReactionList a -> Opaque a l -> MatchRes a l EmptyXiFullResult
data ZetaXi :: * -> * -> ActCase -> *
[FullZetaXi] :: ReactionList a -> Opaque a l -> ZetaXi a l FullXiEmptyResult
[EmptyZetaXi] :: ZetaXi a l EmptyXiFullResult
elemBaseAll :: (Foldable f, Ord a) => f (Opaque a l) -> ElemBase a
lcBase :: Ord a => LCtxt a l -> ElemBase a
instance (GHC.Show.Show a, GHC.Show.Show l) => GHC.Show.Show (Zsyntax.Labelled.Rule.Interface.Neutral a l)
instance (GHC.Classes.Ord l, GHC.Classes.Ord a) => GHC.Base.Semigroup (Zsyntax.Labelled.Rule.Interface.SchemaLCtxt a l)
instance (GHC.Classes.Ord a, GHC.Classes.Ord l) => Otter.Internal.Structures.Subsumable (Zsyntax.Labelled.Rule.Interface.LSequent a l)
instance (GHC.Classes.Eq l, GHC.Classes.Eq a) => GHC.Classes.Eq (Zsyntax.Labelled.Rule.Interface.Neutral a l)
instance (GHC.Classes.Ord l, GHC.Classes.Ord a) => GHC.Classes.Ord (Zsyntax.Labelled.Rule.Interface.Neutral a l)
instance Zsyntax.Labelled.Rule.Interface.NeutralKind 'Zsyntax.Labelled.Formula.KAtom
instance Zsyntax.Labelled.Rule.Interface.NeutralKind 'Zsyntax.Labelled.Formula.KImpl

module Zsyntax.Labelled.DerivationTerm

-- | Derivation term of the labelled forward sequent calculus.
data DerivationTerm a l
[Init] :: a -> DerivationTerm a l
[Copy] :: DerivationTerm a l -> LAxiom a l -> DerivationTerm a l
[ConjR] :: DerivationTerm a l -> DerivationTerm a l -> l -> DerivationTerm a l
[ConjL] :: DerivationTerm a l -> DerivationTerm a l
[ImplR] :: DerivationTerm a l -> LFormula k a l -> ElemBase a -> ReactionList a -> l -> DerivationTerm a l
[ImplL] :: DerivationTerm a l -> DerivationTerm a l -> LFormula k a l -> DerivationTerm a l
concl :: DerivationTerm a l -> Opaque a l
transitions :: DerivationTerm a l -> [(Opaque a l, Opaque a l)]
instance GHC.Base.Functor (Zsyntax.Labelled.DerivationTerm.DerivationTerm a)


-- | Module of derived rule relations.
module Zsyntax.Labelled.Rule.BipoleRelation
respects :: Ord a => ElemBase a -> RList (ElemBase a) (CtrlSet a) -> Bool

-- | Type of derivation terms-decorated data.
data tm ::: pl
(:::) :: tm -> pl -> (:::) tm pl
[_term] :: (:::) tm pl -> tm
[_payload] :: (:::) tm pl -> pl

-- | Type of labelled sequents that are annotated with a derivation term.
type AnnLSequent a l = DerivationTerm a l ::: LSequent a l

-- | A relation is an unbounded curried function with an annotated sequents
--   as input.
type BipoleRel a l = Rule (AnnLSequent a l)

-- | A rule of the derived rule calculus is a relation that has derivation
--   term-decorated sequents as both input and output.
type BipoleRule a l = Rule (AnnLSequent a l) (AnnLSequent a l)

-- | Predicate identifying those formula kinds that correspond to focusable
--   formulas.
class IsFocusable (k :: FKind)
type FocMatchRes a l = MatchRes a l FullXiEmptyResult
type DTFocMatchRes a l = DerivationTerm a l ::: FocMatchRes a l
type DTMatchRes a l actcase = DerivationTerm a l ::: MatchRes a l actcase

-- | Given two multisets m1 and m2, it checks whether m1 is contained in
--   m2, and returns the rest of m2 if it is the case.
matchMultiSet :: Ord a => MultiSet a -> MultiSet a -> Maybe (MultiSet a)
matchLinearCtxt :: (Ord a, Ord l) => SchemaLCtxt a l -> LCtxt a l -> Maybe (LCtxt a l)
matchSchema :: (Ord a, Ord l) => SSchema a l act -> AnnLSequent a l -> Maybe (DTMatchRes a l act)
matchRel :: (Ord a, Ord l) => LCtxt a l -> ZetaXi a l act -> BipoleRel a l (DTMatchRes a l act)
positiveFocalDispatch :: (Ord l, Ord a) => LFormula k a l -> BipoleRel a l (DTFocMatchRes a l)
leftActive :: (Ord l, Ord a) => LCtxt a l -> [Opaque a l] -> ZetaXi a l act -> BipoleRel a l (DTMatchRes a l act)
focus :: (Ord l, Ord a, IsFocusable k) => LFormula k a l -> BipoleRule a l
implLeft :: (Ord l, Ord a) => LFormula KImpl a l -> BipoleRule a l
copyRule :: (Ord a, Ord l) => LAxiom a l -> BipoleRule a l
implRight :: (Ord a, Ord l) => LFormula KImpl a l -> BipoleRule a l
instance (GHC.Show.Show tm, GHC.Show.Show pl) => GHC.Show.Show (tm Zsyntax.Labelled.Rule.BipoleRelation.::: pl)
instance (GHC.Classes.Ord tm, GHC.Classes.Ord pl) => GHC.Classes.Ord (tm Zsyntax.Labelled.Rule.BipoleRelation.::: pl)
instance (GHC.Classes.Eq tm, GHC.Classes.Eq pl) => GHC.Classes.Eq (tm Zsyntax.Labelled.Rule.BipoleRelation.::: pl)
instance Zsyntax.Labelled.Rule.BipoleRelation.IsFocusable 'Zsyntax.Labelled.Formula.KAtom
instance Zsyntax.Labelled.Rule.BipoleRelation.IsFocusable 'Zsyntax.Labelled.Formula.KConj
instance Data.Bifunctor.Bifunctor (Zsyntax.Labelled.Rule.BipoleRelation.:::)
instance Otter.Internal.Structures.Subsumable s => Otter.Internal.Structures.Subsumable (tm Zsyntax.Labelled.Rule.BipoleRelation.::: s)

module Zsyntax.Labelled.Rule.Frontier
data DecoratedFormula :: * -> * -> *
[Unrestr] :: LAxiom a l -> DecoratedFormula a l
[LinNeg] :: LFormula KImpl a l -> DecoratedFormula a l
[LinPos] :: Opaque a l -> DecoratedFormula a l
dfLabel :: DecoratedFormula a l -> Label a l

-- | Type of goal sequents.
--   
--   A goal sequent is characterized by an unrestricted context of axioms,
--   a (non-empty) neutral context, and a consequent formula of unspecified
--   formula kind (i.e., an opaque formula).
data GoalNSequent a l
GNS :: Set (LAxiom a l) -> MultiSet (Neutral a l) -> Opaque a l -> GoalNSequent a l
[_gnsUC] :: GoalNSequent a l -> Set (LAxiom a l)
[_gnsLC] :: GoalNSequent a l -> MultiSet (Neutral a l)
[_gnsConcl] :: GoalNSequent a l -> Opaque a l
toGoalSequent :: LSequent a l -> GoalNSequent a l
filterImpl :: [Neutral a l] -> [LFormula  'KImpl a l]
frNeg :: (Ord l, Ord a) => Neutral a l -> Set (DecoratedFormula a l)
frPos :: (Ord l, Ord a) => LFormula k a l -> Set (DecoratedFormula a l)
foc :: (Ord l, Ord a) => LFormula k a l -> Set (DecoratedFormula a l)
act :: (Ord l, Ord a) => LFormula k a l -> Set (DecoratedFormula a l)

-- | Computes the frontier of a sequent.
frontier :: (Ord l, Ord a) => GoalNSequent a l -> Set (DecoratedFormula a l)
generateRule :: (Ord a, Ord l) => DecoratedFormula a l -> BipoleRule a l

-- | Type of proper rules of the formal system, i.e. <a>BipoleRule</a>s
--   that take at least one premise.
type ProperRule a l = AnnLSequent a l -> BipoleRule a l

-- | Computes the set of initial rules from the frontier of a specified
--   goal sequent.
initialRules :: (Ord a, Ord l) => GoalNSequent a l -> [BipoleRule a l]
mayProperRule :: BipoleRule a l -> Maybe (ProperRule a l)
maySequent :: BipoleRule a l -> Maybe (AnnLSequent a l)
instance (GHC.Show.Show a, GHC.Show.Show l) => GHC.Show.Show (Zsyntax.Labelled.Rule.Frontier.GoalNSequent a l)
instance (GHC.Classes.Ord a, GHC.Classes.Ord l) => Otter.Internal.Structures.Subsumable (Zsyntax.Labelled.Rule.Frontier.GoalNSequent a l)
instance (GHC.Classes.Eq l, GHC.Classes.Eq a) => GHC.Classes.Eq (Zsyntax.Labelled.Rule.Frontier.DecoratedFormula a l)
instance (GHC.Classes.Ord l, GHC.Classes.Ord a) => GHC.Classes.Ord (Zsyntax.Labelled.Rule.Frontier.DecoratedFormula a l)

module Zsyntax.Labelled.Rule

module Zsyntax.Formula

-- | 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.
data BioFormula a
BioAtom :: a -> BioFormula a
BioInter :: BioFormula a -> BioFormula a -> BioFormula a
normalize :: Ord a => BioFormula a -> NonEmpty a

-- | Pretty-prints biochemical formulas, given a way to pretty print its
--   atoms.
--   
--   <pre>
--   &gt;&gt;&gt; ppBioFormula id (BioAtom "foo" &lt;&gt; BioAtom "bar" &lt;&gt; BioAtom "baz")
--   "((foo ⊙ bar) ⊙ baz)"
--   </pre>
ppBioFormula :: (a -> String) -> BioFormula a -> String

-- | Type of logical axioms of Zsyntax.
newtype Axiom a
Axiom :: LAxiom a () -> Axiom a
[unSA] :: Axiom a -> LAxiom a ()
axForget :: LAxiom a l -> Axiom a

-- | Constructs an axiom from non-empty lists of logical atoms as premise
--   and conclusion.
axiom :: NonEmpty a -> ReactionList a -> NonEmpty a -> Axiom a
axiom' :: BFormula a () -> ReactionList a -> BFormula a () -> Axiom a

-- | Type of logical formulas of Zsyntax, parameterized by the type of
--   atoms (which are typically <a>BioFormula</a>s).
data Formula a
Formula :: LFormula k a () -> Formula a

-- | Pretty-prints Zsyntax formulas, given a way to pretty-print its atoms.
ppFormula :: (a -> String) -> Formula a -> String

-- | Constructs an atomic formula from a logical atom.
atom :: a -> Formula a
lToS :: LFormula k a l -> Formula a

-- | Constructs the conjunction of two formulas.
conj :: Formula a -> Formula a -> Formula a

-- | Constructs a Zsyntax conditional (aka linear implication) between two
--   formulas, whose associated biochemical reaction is described by a
--   given elementary base and reaction list.
impl :: Formula a -> ElemBase a -> ReactionList a -> Formula a -> Formula a

-- | Type of ZBS sequents.
data Sequent a
SQ :: Set (Axiom a) -> MultiSet (Formula a) -> Formula a -> Sequent a
[_sqUC] :: Sequent a -> Set (Axiom a)
[_sqLC] :: Sequent a -> MultiSet (Formula a)
[_sqConcl] :: Sequent a -> Formula a
nuLabel :: (Enum l, MonadState l m) => m l

-- | Turns a sequent into a labelled goal sequent.
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]
instance GHC.Show.Show a => GHC.Show.Show (Zsyntax.Formula.Sequent a)
instance GHC.Show.Show a => GHC.Show.Show (Zsyntax.Formula.Axiom a)
instance GHC.Show.Show a => GHC.Show.Show (Zsyntax.Formula.BioFormula a)
instance Data.Traversable.Traversable Zsyntax.Formula.BioFormula
instance Data.Foldable.Foldable Zsyntax.Formula.BioFormula
instance GHC.Base.Functor Zsyntax.Formula.BioFormula
instance GHC.Show.Show a => GHC.Show.Show (Zsyntax.Formula.Formula a)
instance GHC.Classes.Ord a => GHC.Classes.Eq (Zsyntax.Formula.Formula a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Zsyntax.Formula.Formula a)
instance GHC.Classes.Ord a => GHC.Classes.Eq (Zsyntax.Formula.Axiom a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Zsyntax.Formula.Axiom a)
instance GHC.Base.Semigroup (Zsyntax.Formula.BioFormula a)
instance GHC.Classes.Ord a => GHC.Classes.Eq (Zsyntax.Formula.BioFormula a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Zsyntax.Formula.BioFormula a)

module Zsyntax

-- | Searches for a derivation of the specified sequent.
--   
--   <pre>
--   search g == searchLabelled (toLabelledGoal g)
--   </pre>
search :: Ord a => Sequent a -> (SearchRes (DecoratedLSequent a Label), [DecoratedLSequent a Label])

-- | Searches for a derivation of the specified goal sequent. Returns the
--   search results, as well as all searched sequents.
searchLabelled :: Ord a => GoalNSequent a Label -> (SearchRes (DecoratedLSequent a Label), [DecoratedLSequent a Label])

-- | Turns a sequent into a labelled sequent that is suitable for proof
--   search, by breaking the linear context formulas into neutral formulas,
--   and labelling all subformulas with unique labels.
toLabelledGoal :: Ord a => Sequent a -> GoalNSequent a Label

-- | Type representing the result of proof search. Every element in the
--   list corresponds to the result of analysing node in the search space
--   by the search algorithm. The result is <a>Res</a> in the positive case
--   the node is a goal node, or <a>Delay</a> in the negative case.
--   
--   The search agorithm produces an element of `<a>SearchRes</a> a`
--   lazily, inserting <a>Delay</a> constructors to ensure that the
--   computation is productive even in the case no goal node is found in
--   the search space. This allows to perform proof search in an on-demand
--   fashion, possibly giving up after a certain number of <a>Delay</a>s.
type SearchRes a = [Res a]

-- | Type of the result of <a>extractResults</a>, which extracts all
--   positive search results from a search result stream. An element of
--   `Extraction a` is either a non-empty list of positive results, or an
--   element of <tt>SpaceExhausted</tt> giving a reason why no result was
--   found.
data Extraction a
AllResults :: NonEmpty a -> Extraction a
NoResults :: FailureReason -> Extraction a

-- | Type of reasons why no result can be extracted from a search result
--   stream.
--   
--   Either the search space has been exhaustively searched and no result
--   was found (the query is not a theorem), or the search was terminated
--   preemptively according to an upper bound imposed on the maximum depth
--   of the search space.
data FailureReason
NotATheorem :: FailureReason
SpaceTooBig :: FailureReason
type DecoratedLSequent a l = DerivationTerm a l ::: LSequent a l
type Label = Int

-- | Extract all the positive results from a search result stream, stopping
--   if no result is found after the given number of delays.
extractResults :: Int -> SearchRes a -> Extraction a