packages feed

zsyntax (empty) → 0.2.0.0

raw patch · 19 files changed

+1747/−0 lines, 19 filesdep +basedep +constraintsdep +containers

Dependencies added: base, constraints, containers, mtl, multiset, zsyntax

Files

+ CHANGELOG.md view
@@ -0,0 +1,4 @@+0.2.0.0+-------+* Separation of the core library (this package) from client code.+* Substantial simplification of the API and internals.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Author name here (c) 2017++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Author name here nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,16 @@+# zsyntax core library++This library is a Haskell implementation of 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 fully-automatic forward 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 (https://doi.org/10.1093/logcom/exy028).
+ src/Otter.hs view
@@ -0,0 +1,11 @@+module Otter+  ( module Otter.Rule+  , module Otter.SearchRes+  , Subsumable(..)+  , search+  ) where++import Otter.Rule+import Otter.SearchRes+import Otter.Internal.Search+import Otter.Internal.Structures
+ src/Otter/Internal/Search.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE DataKinds #-}++module Otter.Internal.Search where++import Data.Bifunctor (second)+import Data.Maybe+import Control.Monad.State.Lazy+import Data.Foldable+import Control.Applicative++import Otter.Rule+import Otter.Internal.Structures+import Otter.SearchRes++data ProverState n = PS+  { _rules :: [SearchProperRule n]+  , _actives :: ActiveNodes n+  , _inactives :: InactiveNodes n+  , _index :: GlobalIndex n+  , _isGoal :: 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))+popInactive = do+  (PS r as is gi g) <- get+  case popInactiveOp is of+    Just (newIs, inactive) -> do+      let (newAs, active) = activate as inactive+      put (PS r newAs newIs gi g)+      return (Just active)+    Nothing -> return Nothing++getActives :: Prover s g (ActiveNodes s)+getActives = _actives <$> get++getRules :: Prover s g [SearchProperRule s]+getRules = _rules <$> get++isGoalM :: FSCheckedNode s -> Prover s g (Maybe (FSCheckedNode s))+isGoalM s = do+  g <- fmap _isGoal get+  if g (extractNode s) then pure (Just s) else pure Nothing++haveGoal :: [FSCheckedNode s] -> Prover s g (Maybe (FSCheckedNode s))+haveGoal = fmap (foldr (<|>) mzero) . mapM isGoalM++filterUnsubsumed+  :: Subsumable s+  => [ConclNode s] -> Prover s g [SearchNode FSChecked s]+filterUnsubsumed = fmap catMaybes . mapM isNotFwdSubsumed++isNotFwdSubsumed+  :: Subsumable s+  => ConclNode s -> Prover s g (Maybe (SearchNode FSChecked s))+isNotFwdSubsumed concl = fmap (flip fwdSubsumes concl . _index) get++removeSubsumedBy+  :: Subsumable s+  => SearchNode FSChecked s -> Prover s g (SearchNode BSChecked s)+removeSubsumedBy fschecked = do+  (PS r as is gi g) <- get+  let (newIs, bschecked) = removeSubsumedByOp fschecked is+  put (PS r as newIs gi g)+  return bschecked++addRule :: SearchProperRule s -> Prover s g ()+addRule r = do+  (PS rls as is gi g) <- get+  put (PS (r : rls) as is gi g)++addInactive :: SearchNode BSChecked s -> Prover s g ()+addInactive i = do+  (PS r as is gi g) <- get+  let (newIs, newInd) = addToInactives is gi i+  put (PS r as newIs newInd g)++percolate :: ActiveNodes s -> [SearchProperRule s] -> RuleAppRes s+percolate _ [] = mempty+percolate actives rules = r1 `mappend` r2+  where+    activeList = foldActives toList actives+    r1 = foldMap (uncurry apply) ((,) <$> rules <*> activeList)+    r2 = percolate actives . snd $ r1++processNewActive :: ActiveNode s -> Prover s g (RuleAppRes s)+processNewActive node = do+  actives <- getActives+  rules <- getRules+  let r1 = foldMap (`apply` node) rules+      r2 = percolate actives . snd $ r1+  return $ r1 <> r2++merge :: Maybe (SearchNode s a) -> SearchRes a -> SearchRes a+merge m sr = maybe (delay sr) (\x -> cons (extractNode x) sr) m++loop :: Subsumable s => Prover s g (SearchRes s)+loop = do+  inactive <- popInactive+  case inactive of+    Nothing -> pure []+    Just node -> do+      res <- processNewActive node+      unsubSeqs <- filterUnsubsumed (fst res)+      unsubSeqs' <- mapM removeSubsumedBy unsubSeqs+      mapM_ addInactive unsubSeqs'+      mapM_ addRule (snd res)+      liftM2 merge (haveGoal unsubSeqs) loop++doSearch+  :: Subsumable s+  => [SearchNode Initial s] -> [SearchProperRule s] -> Prover s g (SearchRes s)+doSearch initSeqs initRls = do+  mapM_ addInactive (fmap initIsBSCheckd initSeqs)+  mapM_ addRule initRls+  liftM2 merge (haveGoal (fmap initIsFSCheckd initSeqs)) loop++search+  :: Subsumable s+  => [s] -> [s -> Rule s s] -> (s -> Bool) -> (SearchRes s, [s])+search initial rls isGl = second (toList . _index) $+  runState+    (doSearch (fmap initialize initial) (fmap toProperRule rls))+    (PS [] emptyActives emptyInactives emptyGI isGl)
+ src/Otter/Internal/Structures.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE GADTs #-}++module Otter.Internal.Structures+  ( Stage(..)+  , SearchNode+  , ActiveNode+  , FSCheckedNode+  , BSCheckedNode+  , InactiveNode+  , ActiveNodes+  , InactiveNodes+  , ConclNode+  , GlobalIndex+  , SearchRule+  , SearchProperRule+  , Subsumable(..)+  -- , OrdSearchGoal(..)+  -- , applyRule+  , initIsFSCheckd+  , initIsBSCheckd+  , initialize+  -- , subsumesGoalOp+  , removeSubsumedByOp+  , fwdSubsumes+  , activate+  , popInactiveOp+  , addToInactives+  , foldActives+  , mkGoal+  , emptyActives+  , emptyInactives+  , emptyGI+  , toProperRule+  , extractNode+  )+   where++import Otter.Rule++class Subsumable n where+  subsumes :: n -> n -> Bool++-- | Stages of proof search+data Stage+  = Initial    -- ^ Initial node+  | Active     -- ^ Active node+  | Inactive   -- ^ Inactive node+  | Concl      -- ^ Conclusion node+  | FSChecked  -- ^ Forward subsumption-checked+  | BSChecked  -- ^ Backward subsumption-checked+  | GlIndex    -- ^ Global index node+  | Goal       -- ^ Goal node++-- | Type of search nodes in the search space, given by+-- a node together with a proof search stage.+data SearchNode :: Stage -> * -> * where+  InitN :: seq -> SearchNode Initial seq+  ActiveN :: seq -> SearchNode Active seq+  InactiveN :: seq -> SearchNode Inactive seq+  ConclN :: seq -> SearchNode Concl seq+  FSCheckedN :: seq -> SearchNode FSChecked seq+  BSCheckedN :: seq -> SearchNode BSChecked seq+  GoalN :: seq -> SearchNode Goal seq++deriving instance Show a => Show (SearchNode s a)++extractNode :: SearchNode s seq -> seq+extractNode (InitN s) = s+extractNode (ActiveN s) = s+extractNode (InactiveN s) = s+extractNode (ConclN s) = s+extractNode (BSCheckedN s) = s+extractNode (FSCheckedN s) = s+extractNode (GoalN s) = s++type ActiveNode n = SearchNode Active n+type BSCheckedNode n = SearchNode BSChecked n+type FSCheckedNode n = SearchNode FSChecked n+newtype ActiveNodes n = AS [SearchNode Active n]+type InactiveNode n = SearchNode Inactive n+newtype InactiveNodes n = IS [InactiveNode n]++type ConclNode n = SearchNode Concl n+data GlobalIndex n = GI !Int ![n]++instance Foldable GlobalIndex where+  foldr f z (GI _ l) = foldr f z l++--------------------------------------------------------------------------------++initialize :: n -> SearchNode Initial n+initialize = InitN++initIsFSCheckd :: SearchNode Initial n -> FSCheckedNode n+initIsFSCheckd (InitN s) = FSCheckedN s++initIsBSCheckd :: SearchNode Initial n -> BSCheckedNode n+initIsBSCheckd (InitN s) = BSCheckedN s++mkGoal :: n -> SearchNode Goal n+mkGoal = GoalN++emptyActives :: ActiveNodes n+emptyActives = AS mempty++emptyInactives :: InactiveNodes n+emptyInactives = IS mempty++emptyGI :: GlobalIndex n+emptyGI = GI 0 mempty++--------------------------------------------------------------------------------++{-| 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)++toProperRule :: (n -> Rule n n) -> SearchProperRule n+toProperRule = arrowDimap extractNode (relDimap extractNode ConclN)++--------------------------------------------------------------------------------+-- Operations++foldActives+  :: (forall f. Foldable f => f (ActiveNode n) -> b) -> ActiveNodes n -> b+foldActives folder (AS actives) = folder actives++activate+  :: ActiveNodes n -> InactiveNode n -> (ActiveNodes n, ActiveNode n)+activate (AS as) (InactiveN s) = (AS (ActiveN s : as), ActiveN s)++popInactiveOp+  :: InactiveNodes n -> Maybe (InactiveNodes n, InactiveNode n)+popInactiveOp (IS is) =+  case is of+    (x : xs) -> Just (IS xs, x)+    [] -> Nothing++addToInactives+  :: InactiveNodes n -> GlobalIndex n -> BSCheckedNode n+  -> (InactiveNodes n, GlobalIndex n)+addToInactives (IS ins) (GI n gi) (BSCheckedN s) =+  (IS (InactiveN s : ins), GI (n + 1) (s : gi))++fwdSubsumes+  :: Subsumable n+  => GlobalIndex n -> SearchNode Concl n -> Maybe (FSCheckedNode n)+fwdSubsumes (GI _ globalIndex) (ConclN s) =+  if any (`subsumes` s) globalIndex+    then Nothing+    else Just (FSCheckedN s)++removeSubsumedByOp+  :: Subsumable n+  => FSCheckedNode n -> InactiveNodes n -> (InactiveNodes n, BSCheckedNode n)+removeSubsumedByOp (FSCheckedN s) (IS is) =+  let ff = filter filterer is+  in (IS ff, BSCheckedN s)+  where filterer = not . (s `subsumes`) . extractNode
+ src/Otter/Rule.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE DerivingVia #-}++module Otter.Rule where++import Data.Bifunctor (bimap)+import Control.Monad (MonadPlus(..))+import Control.Monad.Fail (MonadFail(..))+import Control.Applicative (Alternative(..), WrappedMonad(..))++{-| 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 'Rule' element may represent three possible+    situations:++    1. 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 'Rule' an instance of 'Alternative', 'MonadPlus', and 'MonadFail'.+    2. A successful computation that produces a 0-ary function, i.e. an axiom;+    3. A successful computation that produces a unary function, that is,+       a function accepting one argument and possibly returning a new 'Rule'.+       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.+ -}+newtype Rule a b = Rule { unRule :: Maybe (Either b (a -> Rule a b)) }+  deriving (Functor, Applicative) via WrappedMonad (Rule a)+type ProperRule a b = a -> Rule a b++-- | Constructs a single-premise rule from a matching function. +match :: (a -> Maybe b) -> Rule a b+match p = Rule . Just . Right $ Rule . fmap Left . p++apply :: ProperRule a b -> a -> ([b], [ProperRule a b])+apply f = maybe mempty (either ((,[]) . pure) (([],) . pure)) . unRule . f++instance Monad (Rule a) where+  return = Rule . Just . Left+  (Rule rel) >>= f =+    Rule $ rel >>= either (unRule . f) (Just . Right . fmap (>>= f))++instance Alternative (Rule a) where+  empty = Rule Nothing+  (Rule Nothing) <|> rel = rel+  rel <|> _ = rel++instance MonadPlus (Rule a) where++instance MonadFail (Rule a) where+  fail _ = Rule Nothing++arrowDimap :: (a -> b) -> (c -> d) -> (b -> c) -> (a -> d)+arrowDimap f g h x = g (h (f x))++-- This is just 'dimap' from the 'Profunctor' typeclass, but defined here+-- standalone to avoid pulling in profunctors for just a couple of uses of+-- 'dimap'.+relDimap :: (a -> b) -> (c -> d) -> Rule b c -> Rule a d+relDimap f g = Rule . fmap (bimap g (arrowDimap f (relDimap f g))) . unRule
+ src/Otter/SearchRes.hs view
@@ -0,0 +1,70 @@+{-# LANGUAGE DeriveFunctor #-}++module Otter.SearchRes+  ( SearchRes+  , Res(..)+  , Extraction(..)+  , FailureReason(..)+  , extractResults+  , delay+  , cons+  ) where++import Data.List.NonEmpty (NonEmpty(..))++data Res a = Res a | Delay deriving (Functor)++-- | 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 'Res' in the positive case the node is a goal node,+-- or 'Delay' in the negative case.+--+-- The search agorithm produces an element of `'SearchRes' a` lazily, inserting+-- 'Delay' 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+-- 'Delay's.+type SearchRes a = [Res a]++-- | Delays a search result stream.+--+-- @+-- delay x == Delay : x+-- @+delay :: SearchRes a -> SearchRes a+delay = (Delay :)++-- | Appends a result to a search result stream.+--+-- @+-- cons x y = Res x : y+-- @+cons :: a -> SearchRes a -> SearchRes a+cons x = (Res x :)++-- | 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 | SpaceTooBig++-- | Type of the result of 'extractResults', 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 'SpaceExhausted' giving a reason why no result was found.+data Extraction a = AllResults (NonEmpty a) | NoResults FailureReason++resListUntil :: Int -> SearchRes a -> ([a], FailureReason)+resListUntil _ [] = ([], NotATheorem)+resListUntil 0 (_ : _)  = ([], SpaceTooBig)+resListUntil i (Res x : xs) = let (ys, b) = resListUntil i xs in (x : ys, b)+resListUntil i (Delay : xs) = resListUntil (i - 1) xs++-- | 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+extractResults i res = case resListUntil i res of+  ([], b) -> NoResults b+  (x : xs, _) -> AllResults (x :| xs)+
+ src/Zsyntax.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE TypeOperators #-}++module Zsyntax+  ( module Zsyntax.Formula+  , search+  , searchLabelled+  , toLabelledGoal+  , O.SearchRes+  , O.Extraction(..)+  , O.FailureReason(..)+  , DecoratedLSequent+  , Label+  , O.extractResults+  ) where++import qualified Otter as O+import Zsyntax.Formula+import Zsyntax.Labelled.Rule.Interface+import Zsyntax.Labelled.Rule+import Zsyntax.Labelled.DerivationTerm+import Data.Foldable+import Control.Monad.State+import Data.Maybe (mapMaybe)++type DecoratedLSequent a l = DerivationTerm a l ::: LSequent a l+type Label = Int++-- | 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+toLabelledGoal s = evalState (neutralize s) 0++-- | Searches for a derivation of the specified sequent.+--+-- @+-- search g == searchLabelled (toLabelledGoal g)+-- @+search :: Ord a+       => Sequent a+       -> ( O.SearchRes (DecoratedLSequent a Label)+          , [DecoratedLSequent a Label])+search = searchLabelled . toLabelledGoal++-- | 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+       -> ( O.SearchRes (DecoratedLSequent a Label)+          , [DecoratedLSequent a Label])+searchLabelled goal = O.search (toList seqs) rules isGoal+  where+    initial = initialRules goal+    seqs    = mapMaybe maySequent initial+    rules   = mapMaybe mayProperRule initial+    isGoal s' = (toGoalSequent . _payload $ s') `O.subsumes` goal
+ src/Zsyntax/Formula.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-}++module Zsyntax.Formula where+  -- (+  --   -- * Biochemical formulas+  --   BioFormula(..)+  -- , ppBioFormula+  -- -- * Logical formulas+  -- , Axiom+  -- , axiom+  -- , axiom'+  -- , axForget+  -- , Formula+  -- , atom+  -- , conj+  -- , impl+  -- , ppFormula+  -- -- * Sequents+  -- , Sequent(..)+  -- , neutralize+  -- ) where++import Control.Arrow ((>>>))+import Data.Bifunctor (second)+import Zsyntax.Labelled.Formula+import Zsyntax.Labelled.Rule (Neutral(..),GoalNSequent(..))+-- import Data.MultiSet.NonEmpty+import Data.MultiSet (MultiSet, fromList)+import Data.Foldable (toList)+import Data.Set (Set)+import qualified Data.Set as S (fromList)+import Data.List.NonEmpty (NonEmpty(..), sort)+import Control.Monad.State+import Data.Either (partitionEithers)+import Data.Function (on)++--------------------------------------------------------------------------------+-- Biochemical atomic formulas++{-| 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+                  | BioInter (BioFormula a) (BioFormula a)+                  deriving (Functor, Foldable, Traversable, Show)++instance Semigroup (BioFormula a) where+  (<>) = BioInter++normalize :: Ord a => BioFormula a -> NonEmpty a+normalize (BioAtom x) = x :| []+normalize (BioInter f1 f2) = sort (normalize f1 <> normalize f2)++-- | Custom equality instance for biological atoms.+-- It includes commutativity of the biological interaction operator.+instance Ord a => Eq (BioFormula a) where+  (==) = on (==) normalize++instance Ord a => Ord (BioFormula a) where+  compare = on compare normalize++-- | Pretty-prints biochemical formulas, given a way to pretty print its atoms.+--+-- @+-- >>> ppBioFormula id (BioAtom "foo" <> BioAtom "bar" <> BioAtom "baz")+-- "((foo ⊙ bar) ⊙ baz)"+-- @+ppBioFormula :: (a -> String) -> BioFormula a -> String+ppBioFormula p (BioAtom x) = p x+ppBioFormula p (BioInter x y) =+  "(" ++ ppBioFormula p x ++ " ⊙ " ++ ppBioFormula p y ++ ")"++--------------------------------------------------------------------------------+-- Simple formulas++-- | Type of logical axioms of Zsyntax.+newtype Axiom a = Axiom { unSA :: LAxiom a () }+  deriving Show++axForget :: LAxiom a l -> Axiom a+axForget = Axiom . void++-- | Constructs an axiom from non-empty lists of logical atoms as premise and+-- conclusion.+axiom :: NonEmpty a -> ReactionList a -> NonEmpty a -> Axiom a+axiom prms cty concl = axiom' (f prms) cty (f concl)+  where f = foldl1 (bConj ()) . fmap BAtom++axiom' :: BFormula a () -> ReactionList a -> BFormula a () -> Axiom a+axiom' b1 r b2 = Axiom (LAx b1 r b2 ())++-- | Type of logical formulas of Zsyntax, parameterized by the type of atoms+-- (which are typically 'BioFormula's).+data Formula a = forall k . Formula (LFormula k a ())++-- | Pretty-prints Zsyntax formulas, given a way to pretty-print its atoms.+ppFormula :: (a -> String) -> Formula a -> String+ppFormula p (Formula f) = ppLFormula p f+-- TODO: wut?+-- @+-- >>> ppFormula id (impl (conj (atom "foo") (atom "bar")) mempty mempty (atom "baz"))+-- "(foo \8855 bar \8594 baz)"+-- @++deriving instance Show a => Show (Formula a)++instance Ord a => Eq (Formula a) where+  (Formula f1) == (Formula f2) = deepHetComp f1 f2 == EQ++instance Ord a => Ord (Formula a) where+  compare (Formula f1) (Formula f2) = deepHetComp f1 f2++instance Ord a => Eq (Axiom a) where+  (Axiom ax1) == (Axiom ax2) = deepHetComp (axToFormula ax1) (axToFormula ax2) == EQ++instance Ord a => Ord (Axiom a) where+  compare (Axiom ax1) (Axiom ax2) = deepHetComp (axToFormula ax1) (axToFormula ax2)++-- | Constructs an atomic formula from a logical atom.+atom :: a -> Formula a+atom = Formula . Atom++lToS :: LFormula k a l -> Formula a+lToS = Formula . void++-- | Constructs the conjunction of two formulas.+conj :: Formula a -> Formula a -> Formula a+conj (Formula f1) (Formula f2) = lToS (Conj f1 f2 ())++-- | 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+impl (Formula f1) eb cs (Formula f2) = Formula (Impl f1 eb cs f2 ())++--------------------------------------------------------------------------------+-- Sequents++-- | Type of ZBS sequents.+data Sequent a =+  SQ { _sqUC    :: Set (Axiom a)+     , _sqLC    :: MultiSet (Formula a)+     , _sqConcl :: (Formula a)+     }+  deriving Show++nuLabel :: (Enum l, MonadState l m) => m l+nuLabel = do { s <- get ; put (succ s) ; return s }++-- | Turns a sequent into a labelled goal sequent.+neutralize+  :: (MonadState l m, Enum l, Ord a, Ord l)+  => Sequent a -> m (GoalNSequent a l)+neutralize (SQ unrestr linear (Formula concl)) = GNS <$> ul <*> ln <*> nGoal+  where+    ul = fmap S.fromList . mapM (traverse (const nuLabel) . unSA)+       . toList $ unrestr+    ln = fmap (fromList . join) . mapM neutralizeFormula . toList $ linear+    nGoal = O <$> traverse (const nuLabel) concl++maybeNeutral :: Opaque a l -> Either (Neutral a l) [Opaque a l]+maybeNeutral (O f@(Atom _)) = Left (N f)+maybeNeutral (O (Conj a b _)) = Right [O a, O b]+maybeNeutral (O f@Impl{}) = Left (N f)++neutralizeOs :: (Ord a, Ord l) => [Opaque a l] -> [Neutral a l]+neutralizeOs [] = []+neutralizeOs xs =+  uncurry (<>) . second (neutralizeOs . join) .+    partitionEithers . fmap maybeNeutral $ xs++neutralizeFormula+  :: (MonadState l m, Enum l, Ord a, Ord l) => Formula a -> m [Neutral a l]+neutralizeFormula = labelSF >>> fmap (return >>> neutralizeOs)+  where labelSF (Formula f) = fmap O . traverse (const nuLabel) $ f
+ src/Zsyntax/Labelled/DerivationTerm.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE StandaloneDeriving #-}++module Zsyntax.Labelled.DerivationTerm where++import Zsyntax.Labelled.Formula++-- | Derivation term of the labelled forward sequent calculus.+data DerivationTerm a l where+  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++deriving instance Functor (DerivationTerm a)++concl :: DerivationTerm a l -> Opaque a l+concl (Init a) = O (Atom a)+concl (Copy d _) = concl d+concl (ConjR d d' l) = O (oConj (concl d) (concl d') l)+concl (ConjL d) = concl d+concl (ImplR d a eb cty l) = O (oImpl (O a) eb cty (concl d) l)+concl (ImplL _ d' _) = concl d'++transitions :: DerivationTerm a l -> [(Opaque a l, Opaque a l)]+transitions (Init _) = []+transitions (Copy d _) = transitions d+transitions (ConjR d1 d2 _) = transitions d1 ++ transitions d2+transitions (ConjL d) = transitions d+transitions (ImplR d _ _ _ _) = transitions d+transitions (ImplL d1 d2 b) = transitions d1 ++ [(concl d1, O b)] ++ transitions d2
+ src/Zsyntax/Labelled/Formula.hs view
@@ -0,0 +1,296 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE MultiParamTypeClasses #-}++{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}++module Zsyntax.Labelled.Formula+  ( FKind(..)+  , Label(..)+  , ElemBase(..)+  , ReactionList+  -- * Labelled formulas+  , LFormula(..)+  , ppLFormula+  , elemBase+  , label+  , frmlHetEq+  , frmlHetOrd+  , deepHetComp+  -- * Labelled axioms+  , LAxiom(..)+  , axLabel+  , axToFormula+  , ppLAxiom+  -- * Opaque formulas+  , Opaque(..)+  , withOpaque+  , oConj+  , oImpl+  -- * Basic formulas+  , BFormula(..)+  , bAtom+  , bConj+  , bfToFormula+  , bfToAtoms+  , maybeBFormula+  ) where++import Zsyntax.ReactionList+import Data.MultiSet (MultiSet, singleton)+import Data.Foldable (fold)+import Data.List.NonEmpty (NonEmpty(..))++newtype ElemBase a = ElemBase { unEB :: MultiSet a }+  deriving (Semigroup, Monoid, Eq, Ord, Show)++data FKind = KAtom | KConj | KImpl++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 -> * -> * -> * 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++deriving instance (Show a, Show l) => Show (LFormula k 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+frmlHetEq f1 f2 = label f1 == label f2++-- | 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+frmlHetOrd f1 f2 = compare (label f1) (label f2)++foldF+  :: (a -> b)+  -> (b -> b -> l -> b)+  -> (b -> ElemBase a -> ReactionList a -> b -> l -> b)+  -> LFormula k a l -> b+foldF f _ _ (Atom a) = f a+foldF f g h (Conj f1 f2 l) = g (foldF f g h f1) (foldF f g h f2) l+foldF f g h (Impl f1 eb cty f2 l) = h (foldF f g h f1) eb cty (foldF f g h f2) l++deriving instance Functor (LFormula k a)+deriving instance Foldable (LFormula k a)+deriving instance Traversable (LFormula k a)++-- | 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.+ppLFormula :: (a -> String) -> LFormula k a l -> String+ppLFormula p = foldF p (\a b _ -> fold [a, " ⊗ ", b])+                     (\a _ _ b _ -> fold ["(", a, " → ", b, ")"])++-- | Returns the elementary base of a labelled formula.+elemBase :: Ord a => LFormula k a l -> ElemBase a+elemBase = foldF (ElemBase . singleton) (\a b _ -> a <> b) (\_ e _ _ _ -> e)++--------------------------------------------------------------------------------+-- Opaque formulas++-- | Type of opaque formulas, that is, those for which we do not care about+-- their formula kind.+data Opaque a l = forall k . O (LFormula k a l)++deriving instance (Show a, Show l) => Show (Opaque a l)++instance (Eq l, Eq a) => Eq (Opaque a l) where+  O f1 == O f2 = frmlHetEq f1 f2++instance (Ord l, Ord a) => Ord (Opaque a l) where+  compare (O f1) (O f2) = frmlHetOrd f1 f2++withOpaque :: (forall k . LFormula k a l -> b) -> Opaque a l -> b+withOpaque f (O fr) = f fr++-- | 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+oConj (O f1) (O f2) = Conj f1 f2++-- | 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+oImpl (O f1) eb cty (O f2) = Impl f1 eb cty f2++--------------------------------------------------------------------------------+-- Basic formulas++-- | Type of basic formulas.+-- A basic formula is one composed of conjunctions of atoms.+data BFormula a l = BAtom a | BConj (BFormula a l) (BFormula a l) l+  deriving (Functor, Foldable, Traversable, Show)++-- | Constructs a basic formula from a logical atom.+bAtom :: a -> BFormula a l+bAtom = BAtom++-- | Constructs the conjunction of two basic formulas, with a given label.+bConj :: l -> BFormula a l -> BFormula a l -> BFormula a l+bConj l f1 f2 = BConj f1 f2 l++-- data ExBFormula a l = forall k . ExBFormula (LFormula k 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+bfToFormula (BAtom x) = O (Atom x)+bfToFormula (BConj f1 f2 l) = O (oConj (bfToFormula f1) (bfToFormula f2) 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+bfToAtoms (BAtom bf) = bf :| []+bfToAtoms (BConj f1 f2 _) = bfToAtoms f1 <> bfToAtoms f2++-- | Decides whether the input labelled formula is a basic formula, and if so,+-- it returns it wrapped in 'Just' as a proper basic formula.+maybeBFormula :: LFormula k a l -> Maybe (BFormula a l)+maybeBFormula (Atom x) = pure (BAtom x)+maybeBFormula (Conj f1 f2 l) =+  BConj <$> maybeBFormula f1 <*> maybeBFormula f2 <*> pure l+maybeBFormula Impl {} = Nothing+-- was: decideF++--------------------------------------------------------------------------------++data LAxiom a l = LAx (BFormula a l) (ReactionList a) (BFormula a l) l+  deriving (Show, Functor, Foldable, Traversable)++-- | Converts a labelled axiom to a labelled formula.+axToFormula :: Ord a => LAxiom a l -> LFormula KImpl a l+axToFormula (LAx f1 _ f2 l) = case (bfToFormula f1, bfToFormula f2) of+  (O f1', O f2') ->+    Impl (mapCty (const mempty) f1') mempty mempty (mapCty (const mempty) f2') 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+-- 'Show' instance.+ppLAxiom :: Ord a => (a -> String) -> LAxiom a l -> String+ppLAxiom p ax = ppLFormula p (axToFormula ax)++-- | Type of formula labels. Note that logical atoms are their own labels.+data Label a l+  = L l -- ^ Regular label+  | A a -- ^ Logical atom+  deriving (Eq, Ord, Show)++-- | Returns the label of a labelled axiom.+axLabel :: LAxiom a l -> l+axLabel (LAx _ _ _ l) = l++-- | Returns the label of a labelled formula.+label :: LFormula k a l -> Label a l+label = foldF A (\_ _ -> L) (\_ _ _ _ -> L)++--------------------------------------------------------------------------------+-- Mapping functions++-- mapAtoms :: Ord a' => (a -> a') -> LFormula k a l -> LFormula k a' l+-- mapAtoms f (Atom a) = Atom (f a)+-- mapAtoms f (Conj a b l) = Conj (mapAtoms f a) (mapAtoms f b) l+-- mapAtoms f (Impl a e c b l) =+--   Impl (mapAtoms f a) (over pack (MS.map f) e) c (mapAtoms f b) l++mapCty :: (ReactionList a -> ReactionList a) -> LFormula k a l -> LFormula k a l+mapCty _ (Atom a) = Atom a+mapCty f (Conj f1 f2 l) = Conj (mapCty f f1) (mapCty f f2) l+mapCty f (Impl f1 eb cty f2 l) = Impl (mapCty f f1) eb (f cty) (mapCty f f2) l++-- mapCtyAx :: (cty1 -> cty2) -> LAxiom a l -> LAxiom a l+-- mapCtyAx f (LAx f1 cty f2 l) = LAx f1 (f cty) f2 l++--------------------------------------------------------------------------------+-- Deep heterogeneous comparison functions++isEq :: Ordering -> Either Ordering Ordering+isEq x = if x == EQ then Right x else Left x++-- | 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.+deepHetComp+  :: (Ord a, Ord l)+  => LFormula k1 a l -> LFormula k2 a l -> Ordering+deepHetComp (Atom x1) (Atom x2) = compare x1 x2+deepHetComp (Atom _) _ = LT+deepHetComp (Conj a1 b1 l1) (Conj a2 b2 l2) =+  either id id $ isEq ca >> isEq cb >> pure cl+  where ca = deepHetComp a1 a2 ; cb = deepHetComp b1 b2 ; cl = compare l1 l2+deepHetComp Conj{} (Atom _) = GT+deepHetComp Conj{} Impl{} = LT+deepHetComp (Impl a1 eb1 cs1 b1 l1) (Impl a2 eb2 cs2 b2 l2) =+  either id id $ isEq ca >> isEq cb >> isEq ceb >> isEq ccs >> pure cl+  where+    ca = deepHetComp a1 a2 ; cb = deepHetComp b1 b2 ; ceb = compare eb1 eb2+    ccs = compare cs1 cs2 ; cl = compare l1 l2+deepHetComp Impl{} _ = GT++--------------------------------------------------------------------------------++-- -- | Type of labelled formulas to be used during proof search.+-- newtype SrchFormula a l k = Srch { unSrch :: LFormula k a l }++-- instance (Show a, Show l) => Show1 (SrchFormula a l) where+--   show1 (Srch f) = show f++-- instance (Ord a, Ord l) => HEq (SrchFormula cty a l) where+--   hetCompare (Srch f1) (Srch f2) = compare (label f1) (label f2)++instance Eq l => Eq (LAxiom a l) where+  ax1 == ax2 = axLabel ax1 == axLabel ax2++instance Ord l => Ord (LAxiom a l) where+  compare ax1 ax2 = compare (axLabel ax1) (axLabel ax2)++-- type instance Atom (SrchFormula cty a l) = a+-- type instance Eb (SrchFormula cty a l) = ElemBase a+-- type instance Ax (SrchFormula cty a l) = LAxiom cty a l++-- sfrmlView :: SrchFormula cty a l k+--           -> FrmlView (SrchFormula cty a l) k (ElemBase a) cty a+-- sfrmlView (Srch (Atom a)) = AtomRepr a+-- sfrmlView (Srch (Conj f1 f2 _)) = ConjRepr (Srch f1) (Srch f2)+-- sfrmlView (Srch (Impl f1 e c f2 _)) = ImplRepr (Srch f1) e c (Srch f2)++-- decideN :: Neutral (SrchFormula cty a l) -> Maybe (BFormula a l)+-- decideN = switchN (\(Srch (Atom x)) -> Just (BAtom x)) (const Nothing)++-- decideOF :: Opaque (SrchFormula cty a l) -> Maybe (BFormula a l)+-- decideOF (O (Srch f)) = decideF f
+ src/Zsyntax/Labelled/Rule.hs view
@@ -0,0 +1,12 @@+module Zsyntax.Labelled.Rule+  ( module Zsyntax.Labelled.Rule.Interface+  -- * Bipole generation+  , module Zsyntax.Labelled.Rule.BipoleRelation+  -- * Initial sequents and rules generation+  , module Zsyntax.Labelled.Rule.Frontier+  ) where++import Zsyntax.Labelled.Rule.BipoleRelation+import Zsyntax.Labelled.Rule.Frontier+import Zsyntax.Labelled.Rule.Interface+  -- (UCtxt, LCtxt, LSequent(..), NeutralKind, Neutral(..), withNeutral, lcBase)
+ src/Zsyntax/Labelled/Rule/BipoleRelation.hs view
@@ -0,0 +1,152 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}++{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++{-| Module of derived rule relations. -}++module Zsyntax.Labelled.Rule.BipoleRelation where+  -- ( (:::)+  -- , AnnLSequent+  -- , IsFocusable+  -- , BipoleRule+  -- , focus+  -- , implLeft+  -- , copyRule+  -- , implRight+  -- ) where++import Data.Function (on)+import Data.Bifunctor (Bifunctor(..))+import Control.Monad (guard)++import Otter+import Data.Set (insert)+import Data.MultiSet (MultiSet, isSubsetOf, (\\), singleton)+import qualified Data.MultiSet as MS (insert)++import Zsyntax.Labelled.Rule.Interface+import Zsyntax.Labelled.Formula+import Zsyntax.Labelled.DerivationTerm+import Zsyntax.ReactionList++respects :: Ord a => ElemBase a -> RList (ElemBase a) (CtrlSet a) -> Bool+respects = respectsRList (\eb cty -> msRespectsCS (unEB eb) cty)++--------------------------------------------------------------------------------++-- | Type of derivation terms-decorated data.+data tm ::: pl = (:::) { _term :: tm, _payload :: pl } deriving (Eq, Ord, Show)++instance Bifunctor (:::) where+  bimap f g (x ::: y) = f x ::: g y++-- | 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) where+instance IsFocusable KAtom where+instance IsFocusable KConj where++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++instance Subsumable s => Subsumable (tm ::: s) where+  subsumes = subsumes `on` _payload++--------------------------------------------------------------------------------++-- | 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)+matchMultiSet m1 m2 = if isSubsetOf m1 m2 then Just (m2 \\ m1) else Nothing++matchLinearCtxt+  :: (Ord a, Ord l) => SchemaLCtxt a l -> LCtxt a l -> Maybe (LCtxt a l)+matchLinearCtxt (SLC slc) = matchMultiSet slc++matchSchema :: (Ord a, Ord l)+            => SSchema a l act -> AnnLSequent a l -> Maybe (DTMatchRes a l act)+matchSchema (SSEmptyGoal delta) (term ::: LS gamma delta' cty goal) = do+  delta'' <- matchLinearCtxt delta delta'+  pure (term ::: MRFullGoal gamma delta'' cty goal)+matchSchema (SSFullGoal delta cty cncl) (tm ::: LS gamma delta' cty' cncl') = do+  delta'' <- matchLinearCtxt delta delta'+  guard (cty == cty')+  guard (cncl == cncl')+  pure (tm ::: MREmptyGoal gamma delta'')++matchRel :: (Ord a, Ord l)+         => LCtxt a l -> ZetaXi a l act -> BipoleRel a l (DTMatchRes a l act)+matchRel delta zetaxi = match . matchSchema $+  case zetaxi of+    EmptyZetaXi -> SSEmptyGoal (SLC delta)+    FullZetaXi cty g -> SSFullGoal (SLC delta) cty g++positiveFocalDispatch+  :: (Ord l, Ord a)+  => LFormula k a l+  -> BipoleRel a l (DTFocMatchRes a l)+positiveFocalDispatch fr = case fr of+  Atom a -> pure (Init a ::: MREmptyGoal mempty (singleton (N fr)))+  Impl {} -> match (matchSchema (SSFullGoal (SLC mempty) mempty (O fr)))+  Conj f1 f2 l -> do+    d ::: MREmptyGoal g1 d1 <- positiveFocalDispatch f1+    d' ::: MREmptyGoal g2 d2 <- positiveFocalDispatch f2+    pure $ ConjR d d' l ::: MREmptyGoal (g1 <> g2) (d1 <> d2)++leftActive+  :: (Ord l, Ord a) => LCtxt a l -> [Opaque a l] -> ZetaXi a l act+  -> BipoleRel a l (DTMatchRes a l act)+leftActive delta [] zetaxi = matchRel delta zetaxi+leftActive delta (O f : rest) zetaxi = withMaybeNeutral f+  (leftActive (MS.insert (N f) delta) rest zetaxi)+  (\(Conj f1 f2 _) -> do+      d ::: res <- leftActive delta (O f2 : O f1 : rest) zetaxi+      pure $ ConjL d ::: res)++focus :: (Ord l, Ord a, IsFocusable k) => LFormula k a l -> BipoleRule a l+focus formula = do+  d ::: MREmptyGoal gamma delta <- positiveFocalDispatch formula+  pure (d ::: LS gamma delta mempty (O formula))++implLeft :: (Ord l, Ord a) => LFormula KImpl a l -> BipoleRule a l+implLeft fr@(Impl f1 _ cty f2 _) = do+  d  ::: MREmptyGoal g1 d1 <- positiveFocalDispatch f1+  d' ::: MRFullGoal g2 d2 cty' cl <- leftActive mempty [(O f2)] EmptyZetaXi+  let b = lcBase d2+      ext = extend b cty+  guard (respects b cty)+  pure $ ImplL d d' f2+     ::: LS (g1 <> g2) (MS.insert (N fr) (d1 <> d2)) (ext <> cty') cl++copyRule :: (Ord a, Ord l) => LAxiom a l -> BipoleRule a l+copyRule ax = let fr = axToFormula ax in case fr of+  Impl f1 _ cty f2 _ -> do+    d  ::: MREmptyGoal g1 d1 <- positiveFocalDispatch f1+    d' ::: MRFullGoal g2 d2 cty' cl <- leftActive mempty [(O f2)] EmptyZetaXi+    let b = lcBase d2 ; ext = extend b cty+    guard (respects b cty)+    pure $ Copy (ImplL d d' f2) ax+       ::: LS (insert ax (g1 <> g2)) (d1 <> d2) (ext <> cty') cl++implRight :: (Ord a, Ord l) => LFormula KImpl a l -> BipoleRule a l+implRight fr@(Impl f1 eb cty f2 l) = do+  tm ::: MREmptyGoal g d <- leftActive mempty [(O f1)] (FullZetaXi cty (O f2))+  guard (lcBase d == eb)+  pure $ ImplR tm fr eb cty l ::: LS g d mempty (O fr)
+ src/Zsyntax/Labelled/Rule/Frontier.hs view
@@ -0,0 +1,133 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE GADTs #-}++module Zsyntax.Labelled.Rule.Frontier where+  -- ( GoalNSequent(..)+  -- , Rule+  -- , initialSequentsAndRules+  -- ) where++import Data.Maybe (mapMaybe)+import Data.Constraint (Dict(..))+import Otter (unRule, Subsumable(..))+import Data.MultiSet (MultiSet)+import Data.Foldable (toList)+import Data.Set (Set)+import qualified Data.Set as S (singleton, fromList)+import Data.Function (on)+import Control.Monad (join)++import Zsyntax.Labelled.Rule.BipoleRelation+import Zsyntax.Labelled.Rule.Interface+import Zsyntax.Labelled.Formula++data DecoratedFormula :: * -> * -> * where+  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+dfLabel (Unrestr ax) = L (axLabel ax)+dfLabel (LinNeg f) = label f+dfLabel (LinPos (O f)) = label f++instance (Eq l, Eq a) => Eq (DecoratedFormula a l) where+  (==) = on (==) dfLabel++instance (Ord l, Ord a) => Ord (DecoratedFormula a l) where+  compare = on compare dfLabel++--------------------------------------------------------------------------------+-- Goal and result sequents.++-- | 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+  { _gnsUC :: Set (LAxiom a l)+  , _gnsLC :: MultiSet (Neutral a l) -- NonEmptyMultiSet (Neutral a l)+  , _gnsConcl :: Opaque a l -- Opaque (LFormula' cty l l)+  }+  deriving Show++instance (Ord a, Ord l) => Subsumable (GoalNSequent a l) where+  subsumes  (GNS uc lc fr) (GNS uc' lc' fr') =+    fr == fr' && lc == lc' && null (_scOnOnlyFirst (uc `subCtxtOf` uc'))++toGoalSequent :: LSequent a l -> GoalNSequent a l+toGoalSequent (LS uc lc _ c) = GNS uc lc c++--------------------------------------------------------------------------------+ -- Frontier computation++filterImpl :: [Neutral a l] -> [LFormula 'KImpl a l]+filterImpl = mapMaybe aux+  where+    aux :: Neutral a l -> Maybe (LFormula 'KImpl a l)+    aux (N (f :: LFormula k a l)) =+      either (const Nothing) (\Dict -> Just f) (decideNeutral @k)++frNeg :: (Ord l, Ord a) => Neutral a l -> Set (DecoratedFormula a l)+frNeg = switchN (const mempty) (\(Impl a _ _ b _) -> foc a <> act b)++frPos, foc, act :: (Ord l, Ord a) => LFormula k a l -> Set (DecoratedFormula a l)+frPos f = case f of+  Atom _ -> mempty+  Conj {} -> foc f+  Impl a _ _ b _ -> mconcat [act a, frPos b, S.singleton (LinPos (O b))]+foc f = case f of+  Atom _ -> mempty+  Conj a b _ -> foc a <> foc b+  Impl {} -> S.singleton (LinPos (O f)) <> frPos f+act f = case f of+  Atom _ -> mempty+  Conj f1 f2 _ -> act f1 <> act f2+  Impl {} -> S.singleton (LinNeg f) <> frPos f++-- | Computes the frontier of a sequent.+frontier :: (Ord l, Ord a) => GoalNSequent a l -> Set (DecoratedFormula a l)+frontier (GNS uc lc goal@(O fgoal)) =+  mconcat +    [ toplevelUC, toplevelLC+    , ucFrontier, linFrontier+    , goalFrontier, S.singleton (LinPos goal)+    ]+  where+    lcList = toList lc+    toplevelUC = S.fromList . map Unrestr . toList $ uc+    toplevelLC = S.fromList . fmap LinNeg . filterImpl $ lcList+    ucFrontier = mconcat . fmap (frNeg . N . axToFormula) . toList $ uc+    linFrontier = mconcat . fmap frNeg $ lcList+    goalFrontier = frPos fgoal++--------------------------------------------------------------------------------+-- Generation of initial rules from the frontier.++generateRule :: (Ord a, Ord l) => DecoratedFormula a l -> BipoleRule a l+generateRule (Unrestr axiom) = copyRule axiom+generateRule (LinNeg impl) = implLeft impl+generateRule (LinPos (O f)) =+  case f of { Atom _ -> focus f ; Conj {} -> focus f ; Impl {} -> implRight f }+  +--------------------------------------------------------------------------------+-- Main function++-- | Type of proper rules of the formal system, i.e. 'BipoleRule'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]+initialRules = fmap generateRule . toList . frontier++mayProperRule :: BipoleRule a l -> Maybe (ProperRule a l)+mayProperRule = join . fmap (either (const Nothing) Just) . unRule++maySequent :: BipoleRule a l -> Maybe (AnnLSequent a l)+maySequent = join . fmap (either Just (const Nothing)) . unRule
+ src/Zsyntax/Labelled/Rule/Interface.hs view
@@ -0,0 +1,186 @@+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE GADTs #-}++{-# OPTIONS_GHC -Wno-unticked-promoted-constructors -Wno-orphans -Wno-unused-imports #-}++module Zsyntax.Labelled.Rule.Interface where++import Otter (Subsumable(..))+import Data.Foldable (toList)+import Data.List (intersperse)+import Data.Set (Set, (\\), isSubsetOf)+import Data.Map (Map)+import Data.Maybe (fromMaybe)+import qualified Data.Map as M (lookup)+import Zsyntax.Labelled.Formula+import Data.Constraint (Dict(..))+import Data.MultiSet (MultiSet)+import Data.Function (on)++-- import Core.FormulaKind+-- import Formula+-- import LinearContext++--------------------------------------------------------------------------------+-- Neutral sequents++-- -- | Type of unrestricted contexts. Unrestricted contexts are made out of+-- -- elements of some type of axiomatic formulas.+-- type UCtxt = Set Ax+-- -- | Type of linear contexts. Linear contexts are made out of neutral formulas.+-- type LCtxt = LinearCtxt -- (Neutral Frml)++-- data NSequent' cty = NS+--   { _nsUC :: UCtxt+--   , _nsLC :: LCtxt+--   , _nsCty :: cty+--   , _nsConcl :: Opaque Frml+--   } deriving (Functor)++-- type NSequent = NSequent' Cty++-- prettyNS :: NSequent -> String+-- prettyNS (NS _ lc _ c) =+--   concat (intersperse "," (fmap (withNeutral prettyF) (lcList lc))) ++ " ==> " +++--   withOpaque prettyF c++-- deriving instance Eq cty => Eq (NSequent' cty)+-- deriving instance Ord cty => Ord (NSequent' cty)++--------------------------------------------------------------------------------+-- Labelled sequents++-- | 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+  { lsUCtxt :: UCtxt a l+  , lsLCtxt :: LCtxt a l+  , lsCty :: ReactionList a+  , lsConcl :: Opaque a l+  }++data SubCtxt a = SC+  { _scOnOnlyFirst :: [a]+  , _scRestFirst :: [a]+  }++subCtxtOf :: Ord a => Set a -> Set a -> SubCtxt a+subCtxtOf s1 s2 =+  if isSubsetOf s1 s2 then SC [] (toList s1) else SC (toList df) df'+  where df = s1 \\ s2 ; df' = toList (s1 \\ df)++instance (Ord a, Ord l) => Subsumable (LSequent a l) where+  subsumes  (LS uc lc c fr) (LS uc' lc' c' fr') =+    fr == fr' && lc == lc' && c == c' && null (_scOnOnlyFirst (uc `subCtxtOf` uc'))++--------------------------------------------------------------------------------+-- Neutral formulas.++-- | Predicate identifying those formula kinds corresponding to neutral+-- formulas.+class NeutralKind (k :: FKind) where+  decideNeutral :: Either (Dict (k ~ KAtom)) (Dict (k ~ KImpl))+instance NeutralKind KAtom where decideNeutral = Left Dict+instance NeutralKind KImpl where decideNeutral = Right Dict++-- | Type of neutral formulas, i.e. all formulas whose formula kind is+-- classified as neutral by 'NeutralKind'.+data Neutral a l = forall k . NeutralKind k => N (LFormula k a l)++deriving instance (Show a, Show l) => Show (Neutral a l)++withMaybeNeutral+  :: LFormula k a l+  -> (NeutralKind k => b)+  -> (LFormula KConj a l -> b)+  -> b+withMaybeNeutral fr f g = case fr of+  Atom {} -> f+  Impl {} -> f+  Conj {} -> g fr++withNeutral :: (forall k. NeutralKind k => LFormula k a l -> b) -> Neutral a l -> b+withNeutral f (N fr) = f fr++switchN :: (LFormula KAtom a l -> b) -> (LFormula KImpl a l -> b) -> Neutral a l -> b+switchN f g (N (x :: LFormula k a l)) =+  either (\Dict -> f x) (\Dict -> g x) (decideNeutral @k)++-- class Show1 (fr :: k -> *) where show1 :: fr a -> String+-- instance Show (Opaque a l) where show (O f) = "O " ++ show1 f+-- instance Show (Neutral a l) where show (N f) = "N " ++ show1 f++instance (Eq l, Eq a) => Eq (Neutral a l) where+  N f1 == N f2 = frmlHetEq f1 f2++instance (Ord l, Ord a) => Ord (Neutral a l) where+  compare (N f1) (N f2) = frmlHetOrd f1 f2++--------------------------------------------------------------------------------++-- | Linear contexts that appear in sequent schemas.+newtype SchemaLCtxt a l = SLC (LCtxt a l)++deriving instance (Ord l, Ord a) => Semigroup (SchemaLCtxt a l)+-- deriving instance Monoid SchemaLCtxt++{-| Type indicating the possible shapes of an active relation.+    An active relation has the form++      act(delta ; omega ==>_zeta xi)[...] -> gamma' ; delta' -->> 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 | EmptyXiFullResult++-- | Sequent schemas.+data SSchema :: * -> * -> ActCase -> * where+  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 -> * where+  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 -> * where+  FullZetaXi+    :: ReactionList a+    -> Opaque a l+    -> ZetaXi a l FullXiEmptyResult+  EmptyZetaXi :: ZetaXi a l EmptyXiFullResult++--------------------------------------------------------------------------------+-- Elementary bases and control sets++elemBaseAll :: (Foldable f, Ord a) => f (Opaque a l) -> ElemBase a+elemBaseAll = mconcat . fmap (withOpaque elemBase) . toList+  +lcBase :: Ord a => LCtxt a l -> ElemBase a+lcBase = foldMap (withNeutral elemBase)
+ src/Zsyntax/ReactionList.hs view
@@ -0,0 +1,65 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Zsyntax.ReactionList where++-- import Core.LinearContext+import Data.Set (Set)+import qualified Data.Set as S (map,fromList)+import Data.Bifunctor (first)+import Data.Foldable (toList)+import Data.MultiSet (MultiSet, isSubsetOf)+-- import Data.MultiSet.NonEmpty++data CtrlType = Regular | SupersetClosed deriving (Eq, Ord, Show)+data CtrlSetCtxt af = CSC+  { _cscType :: CtrlType+  , _cscCtxt :: MultiSet af+  } deriving (Eq, Ord, Show)++{-| 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+  { unCS :: Set (CtrlSetCtxt af)+  } deriving (Eq, Ord, Semigroup, Monoid, Show)++fromCSCtxts :: (Foldable f, Ord af) => f (CtrlSetCtxt af) -> CtrlSet af+fromCSCtxts = CS . S.fromList . toList++toCtxtList :: CtrlSet af -> [CtrlSetCtxt af]+toCtxtList = toList . unCS++-- | Checks whether a linear context "respects" a control set context.+respectsCC :: Ord af => MultiSet af -> CtrlSetCtxt af -> Bool+respectsCC ms (CSC Regular ctxt) = ms /= ctxt+respectsCC ms (CSC SupersetClosed ctxt) = not (ctxt `isSubsetOf` ms)++-- | 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+msRespectsCS ms = and . S.map (respectsCC ms) . unCS++-- | 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+  { unRL :: [(eb, cs)]+  } deriving (Eq, Ord, Semigroup, Monoid, Show)++justCS :: Monoid eb => cs -> RList eb cs+justCS cs = RL [(mempty, cs)]++-- | Extends a reaction list with an elementary base.+extend :: Semigroup eb => eb -> RList eb cs -> RList eb cs+extend base = RL . map (first (base <>)) . unRL+-- was: extendRList++-- | 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+respectsRList resp base = and . fmap (uncurry resp . first (base <>)) . unRL
+ test/Main.hs view
@@ -0,0 +1,50 @@+import Zsyntax+import qualified Otter as O+import System.Exit (exitFailure)+import qualified Data.Set as S (fromList)+import qualified Data.MultiSet as M+import Data.List.NonEmpty (fromList)+import Zsyntax.ReactionList++type Atom = BioFormula String++main :: IO ()+main = checkSequent goal++checkSequent :: Sequent Atom -> IO ()+checkSequent g =+  case O.extractResults 2000 (fst $ search (toLabelledGoal g)) of+    O.AllResults _ -> putStrLn "test passed."+    O.NoResults _  -> putStrLn "test failed." >> exitFailure++ax :: Ord a => [a] -> [a] -> [a] -> Axiom (BioFormula a)+ax xs ys rl =+  axiom (fromList $ fmap BioAtom xs)+        (justCS $ fromCSCtxts [CSC SupersetClosed+                                (M.fromList (fmap BioAtom rl))])+        (fromList $ fmap BioAtom ys)++goal :: Sequent Atom+goal = SQ (S.fromList axioms) (M.fromList from) to+  where+    axioms :: [Axiom Atom]+    axioms =+      [ ax ["ICL"] ["MUS81"] mempty+      , ax ["MUS81", "FANCD21"] ["FAN1"] mempty+      , ax ["FANCM", "ATR"] ["FAcore"] ["CHKREC"]+      , ax ["FANCM", "ATM"] ["FAcore"] ["CHKREC"]+      , ax ["FAcore", "ATM"] ["FANCD21"] ["USP1"]+      , ax ["FAcore", "ATR"] ["FANCD21"] ["USP1"]+      , ax ["FAcore", "H2AX", "DSB"] ["FANCD21"] ["USP1"]+      , ax ["ICL"] ["FANCM"] ["CHKREC"]+      , ax ["FAN1"] ["DSB"] ["HRR", "NHEJ"]+      , ax ["XPF"] ["DBS"] ["HRR", "NHEJ"]+      , ax ["MUS81", "FAN1"] ["ADD"] ["PCNATLS"]+      , ax ["ATM"] ["ATM", "ATM"] mempty+      , ax ["ICL"] ["ICL", "ICL"] mempty+      ]+    from :: [Formula Atom]+    from = [atom (BioAtom "ICL"), atom (BioAtom "ATM")]+    to :: Formula Atom+    to = conj (atom (BioAtom "DSB")) (atom (BioAtom "ADD"))+
+ zsyntax.cabal view
@@ -0,0 +1,91 @@+name:           zsyntax+version:        0.2.0.0+description:    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+                (<https://doi.org/10.1093/logcom/exy028>).++category:       Logic, Theorem Provers, Bioinformatics+synopsis:       Automated theorem prover for the Zsyntax biochemical calculus+homepage:       https://github.com/fsestini/zsyntax#readme                 +bug-reports:    https://github.com/fsestini/zsyntax/issues+author:         Filippo Sestini+maintainer:     sestini.filippo@gmail.com+copyright:      2018 Filippo Sestini+license:        BSD3+license-file:   LICENSE+build-type:     Simple+cabal-version:  2++extra-source-files:+    README+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/fsestini/zsyntax++library++  exposed-modules:+      Zsyntax+      Zsyntax.Formula+      Zsyntax.ReactionList++      Zsyntax.Labelled.Rule+      Zsyntax.Labelled.Formula+      Zsyntax.Labelled.DerivationTerm++      Zsyntax.Labelled.Rule.BipoleRelation+      Zsyntax.Labelled.Rule.Frontier+      Zsyntax.Labelled.Rule.Interface++      Otter+      Otter.Rule+      Otter.SearchRes+      Otter.Internal.Search+      Otter.Internal.Structures++  default-extensions:+      LambdaCase+      TupleSections+  hs-source-dirs: src+  ghc-options:+      -Wall+      -Wcompat+      -Wincomplete-record-updates+      -Wincomplete-uni-patterns+      -Wredundant-constraints+      -Wno-unticked-promoted-constructors+      -- -Werror+  build-depends:+      base >=4.7 && <5+    , constraints >= 0.10.1 && < 0.11+    , containers >= 0.6.0 && < 0.7+    , multiset >= 0.3.4 && < 0.4+    , mtl >= 2.2.2 && < 2.3+  default-language: Haskell2010++test-suite zsyntax-test+  type:             exitcode-stdio-1.0+  hs-source-dirs:   test+  build-depends:    base >=4.7 && <5+                  , zsyntax+                  , containers >= 0.6.0 && < 0.7+                  , multiset >= 0.3.4 && < 0.4+                  , mtl >= 2.2.2 && < 2.3+  main-is:          Main.hs+  default-language: Haskell2010