{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Zsyntax.Labelled.Rule.BipoleRelation 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)
data tm ::: pl = (:::) { _term :: tm, _payload :: pl } deriving (Eq, Ord, Show)
instance Bifunctor (:::) where
bimap f g (x ::: y) = f x ::: g y
type AnnLSequent a l = DerivationTerm a l ::: LSequent a l
type BipoleRel a l = Rule (AnnLSequent a l)
type BipoleRule a l = Rule (AnnLSequent a l) (AnnLSequent a l)
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
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)