{-# 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)
type UCtxt a l = Set (LAxiom a l)
type LCtxt a l = MultiSet (Neutral a l)
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'))
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
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)
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
newtype SchemaLCtxt a l = SLC (LCtxt a l)
deriving instance (Ord l, Ord a) => Semigroup (SchemaLCtxt a l)
data ActCase = FullXiEmptyResult | EmptyXiFullResult
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
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
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)