{-# LANGUAGE FlexibleContexts, BangPatterns, RecordWildCards, TypeFamilies, ScopedTypeVariables #-}
module Twee.Join where
import Twee.Base
import Twee.Rule
import Twee.Equation
import qualified Twee.Proof as Proof
import Twee.CP hiding (Config)
import Twee.Constraints hiding (funs)
import qualified Twee.Index as Index
import Twee.Index(Index)
import Twee.Rule.Index(RuleIndex(..))
import Twee.Utils
import Data.Maybe
import Data.Either
import Data.Ord
import qualified Data.Map.Strict as Map
data Config =
Config {
Config -> Bool
cfg_ground_join :: !Bool,
Config -> Bool
cfg_use_connectedness_standalone :: !Bool,
Config -> Bool
cfg_use_connectedness_in_ground_joining :: !Bool,
Config -> Bool
cfg_set_join :: !Bool }
defaultConfig :: Config
defaultConfig :: Config
defaultConfig =
Config :: Bool -> Bool -> Bool -> Bool -> Config
Config {
cfg_ground_join :: Bool
cfg_ground_join = Bool
True,
cfg_use_connectedness_standalone :: Bool
cfg_use_connectedness_standalone = Bool
True,
cfg_use_connectedness_in_ground_joining :: Bool
cfg_use_connectedness_in_ground_joining = Bool
False,
cfg_set_join :: Bool
cfg_set_join = Bool
False }
{-# INLINEABLE joinCriticalPair #-}
joinCriticalPair ::
(Function f, Has a (Rule f)) =>
Config ->
(Index f (Equation f), Index f (Rule f)) -> RuleIndex f a ->
Maybe (Model f) ->
CriticalPair f ->
Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
joinCriticalPair :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Maybe (Model f)
-> CriticalPair f
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
joinCriticalPair Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Maybe (Model f)
mmodel cp :: CriticalPair f
cp@CriticalPair{cp_eqn :: forall f. CriticalPair f -> Equation f
cp_eqn = Term f
t :=: Term f
u} =
case Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
allSteps Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx CriticalPair f
cp of
Maybe (CriticalPair f)
Nothing ->
(Maybe (CriticalPair f), [CriticalPair f])
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
forall a b. b -> Either a b
Right (Maybe (CriticalPair f)
forall a. Maybe a
Nothing, [])
Maybe (CriticalPair f)
_ | Config -> Bool
cfg_set_join Config
config Bool -> Bool -> Bool
&&
Bool -> Bool
not (Map (Term f) (Term f, Reduction f) -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Map (Term f) (Term f, Reduction f) -> Bool)
-> Map (Term f) (Term f, Reduction f) -> Bool
forall a b. (a -> b) -> a -> b
$ Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection
(Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
normalForms ((Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) (Term f -> Reduction f -> Map (Term f) (Reduction f)
forall k a. k -> a -> Map k a
Map.singleton Term f
t []))
(Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
normalForms ((Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) (Term f -> Reduction f -> Map (Term f) (Reduction f)
forall k a. k -> a -> Map k a
Map.singleton Term f
u []))) ->
(Maybe (CriticalPair f), [CriticalPair f])
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
forall a b. b -> Either a b
Right (CriticalPair f -> Maybe (CriticalPair f)
forall a. a -> Maybe a
Just CriticalPair f
cp, [])
Just CriticalPair f
cp ->
case Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Maybe (Model f)
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Maybe (Model f)
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFromMaybe Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Maybe (Model f)
mmodel (Formula f -> [Branch f]
forall f.
(Minimal f, Ordered f, Labelled f) =>
Formula f -> [Branch f]
branches ([Formula f] -> Formula f
forall f. [Formula f] -> Formula f
And [])) CriticalPair f
cp of
Left Model f
model -> (CriticalPair f, Model f)
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
forall a b. a -> Either a b
Left (CriticalPair f
cp, Model f
model)
Right (Maybe (CriticalPair f)
mcp, [CriticalPair f]
cps) -> (Maybe (CriticalPair f), [CriticalPair f])
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
forall a b. b -> Either a b
Right (Maybe (CriticalPair f)
mcp, [CriticalPair f]
cps)
{-# INLINEABLE step1 #-}
{-# INLINEABLE step2 #-}
{-# INLINEABLE step3 #-}
{-# INLINEABLE allSteps #-}
step1, step2, step3, allSteps ::
(Function f, Has a (Rule f)) =>
Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
checkOrder :: Function f => CriticalPair f -> Maybe (CriticalPair f)
allSteps :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
allSteps Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx CriticalPair f
cp =
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
step1 Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx CriticalPair f
cp Maybe (CriticalPair f)
-> (CriticalPair f -> Maybe (CriticalPair f))
-> Maybe (CriticalPair f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
step2 Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Maybe (CriticalPair f)
-> (CriticalPair f -> Maybe (CriticalPair f))
-> Maybe (CriticalPair f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
CriticalPair f -> Maybe (CriticalPair f)
forall f. Function f => CriticalPair f -> Maybe (CriticalPair f)
checkOrder Maybe (CriticalPair f)
-> (CriticalPair f -> Maybe (CriticalPair f))
-> Maybe (CriticalPair f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
step3 Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx
checkOrder :: CriticalPair f -> Maybe (CriticalPair f)
checkOrder CriticalPair f
cp
| CriticalPair f -> Bool
forall f. Ordered f => CriticalPair f -> Bool
tooBig CriticalPair f
cp = Maybe (CriticalPair f)
forall a. Maybe a
Nothing
| Bool
otherwise = CriticalPair f -> Maybe (CriticalPair f)
forall a. a -> Maybe a
Just CriticalPair f
cp
where
tooBig :: CriticalPair f -> Bool
tooBig CriticalPair{cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_top = Just Term f
top, cp_eqn :: forall f. CriticalPair f -> Equation f
cp_eqn = Term f
t :=: Term f
u} =
Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
top Term f
t Bool -> Bool -> Bool
|| Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
top Term f
u
tooBig CriticalPair f
_ = Bool
False
step1 :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
step1 Config
cfg (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx = Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> (Term f -> Term f -> Reduction f)
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> (Term f -> Term f -> Reduction f)
-> CriticalPair f
-> Maybe (CriticalPair f)
joinWith Config
cfg (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx (\Term f
t Term f
u -> (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (Bool -> Term f -> Bool
forall a b. a -> b -> a
const Bool
True) ((Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (Term f -> Term f -> Rule f -> Subst f -> Bool
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
Labelled f) =>
Term f -> Term f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u) (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f a
idx)) Term f
t)
where
ok :: Term f -> Term f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u Rule f
rule Subst f
sub = Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reducesOriented Rule f
rule Subst f
sub Bool -> Bool -> Bool
&& Rule f -> Equation f
forall f. Rule f -> Equation f
unorient Rule f
rule Equation f -> Equation f -> Bool
forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u)
step2 :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
step2 Config
cfg (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx = Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> (Term f -> Term f -> Reduction f)
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> (Term f -> Term f -> Reduction f)
-> CriticalPair f
-> Maybe (CriticalPair f)
joinWith Config
cfg (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx (\Term f
t Term f
u -> (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (Bool -> Term f -> Bool
forall a b. a -> b -> a
const Bool
True) ((Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (Term f -> Term f -> Rule f -> Subst f -> Bool
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
Labelled f) =>
Term f -> Term f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u) (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) Term f
t)
where
ok :: Term f -> Term f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u Rule f
rule Subst f
sub = Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces Rule f
rule Subst f
sub Bool -> Bool -> Bool
&& Rule f -> Equation f
forall f. Rule f -> Equation f
unorient Rule f
rule Equation f -> Equation f -> Bool
forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u)
step3 :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
step3 cfg :: Config
cfg@Config{Bool
cfg_set_join :: Bool
cfg_use_connectedness_in_ground_joining :: Bool
cfg_use_connectedness_standalone :: Bool
cfg_ground_join :: Bool
cfg_set_join :: Config -> Bool
cfg_use_connectedness_in_ground_joining :: Config -> Bool
cfg_use_connectedness_standalone :: Config -> Bool
cfg_ground_join :: Config -> Bool
..} (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx CriticalPair f
cp
| Bool -> Bool
not Bool
cfg_use_connectedness_standalone = CriticalPair f -> Maybe (CriticalPair f)
forall a. a -> Maybe a
Just CriticalPair f
cp
| Bool
otherwise =
case CriticalPair f -> Maybe (Term f)
forall f. CriticalPair f -> Maybe (Term f)
cp_top CriticalPair f
cp of
Just Term f
top ->
case ((CriticalPair f, Term f) -> Maybe (CriticalPair f)
join (CriticalPair f
cp, Term f
top), (CriticalPair f, Term f) -> Maybe (CriticalPair f)
join ((CriticalPair f, Term f) -> (CriticalPair f, Term f)
forall a. Symbolic a => a -> a
flipCP (CriticalPair f
cp, Term f
top))) of
(Just CriticalPair f
cp1, Just CriticalPair f
cp2) ->
case Equation f -> Equation f -> Bool
forall f. Function f => Equation f -> Equation f -> Bool
simplerThan (CriticalPair f -> Equation f
forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp1) (CriticalPair f -> Equation f
forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp2) of
Bool
True -> CriticalPair f -> Maybe (CriticalPair f)
forall a. a -> Maybe a
Just CriticalPair f
cp1
Bool
False -> CriticalPair f -> Maybe (CriticalPair f)
forall a. a -> Maybe a
Just CriticalPair f
cp2
(Maybe (CriticalPair f), Maybe (CriticalPair f))
_ -> Maybe (CriticalPair f)
forall a. Maybe a
Nothing
Maybe (Term f)
_ -> CriticalPair f -> Maybe (CriticalPair f)
forall a. a -> Maybe a
Just CriticalPair f
cp
where
join :: (CriticalPair f, Term f) -> Maybe (CriticalPair f)
join (CriticalPair f
cp, Term f
top) =
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> (Term f -> Term f -> Reduction f)
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> (Term f -> Term f -> Reduction f)
-> CriticalPair f
-> Maybe (CriticalPair f)
joinWith Config
cfg (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx (\Term f
t Term f
u -> (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
`lessThan` Term f
top) ((Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (Term f -> Term f -> Rule f -> Subst f -> Bool
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
Labelled f) =>
Term f -> Term f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u) (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) Term f
t) CriticalPair f
cp
ok :: Term f -> Term f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u Rule f
rule Subst f
sub =
Rule f -> Equation f
forall f. Rule f -> Equation f
unorient Rule f
rule Equation f -> Equation f -> Bool
forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u) Bool -> Bool -> Bool
&&
Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reducesSkolem Rule f
rule Subst f
sub
flipCP :: Symbolic a => a -> a
flipCP :: a -> a
flipCP a
t = (Var -> Builder (ConstantOf a)) -> a -> a
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Var -> Builder (ConstantOf a)
sub a
t
where
n :: Int
n = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:(Var -> Int) -> [Var] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Int
forall a. Enum a => a -> Int
fromEnum (a -> [Var]
forall a. Symbolic a => a -> [Var]
vars a
t))
sub :: Var -> Builder (ConstantOf a)
sub (V Int
x) = Var -> Builder (ConstantOf a)
forall f. Var -> Builder f
var (Int -> Var
V (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
x))
{-# INLINEABLE joinWith #-}
joinWith ::
(Function f, Has a (Rule f)) =>
Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> (Term f -> Term f -> Reduction f) -> CriticalPair f -> Maybe (CriticalPair f)
joinWith :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> (Term f -> Term f -> Reduction f)
-> CriticalPair f
-> Maybe (CriticalPair f)
joinWith Config{Bool
cfg_set_join :: Bool
cfg_use_connectedness_in_ground_joining :: Bool
cfg_use_connectedness_standalone :: Bool
cfg_ground_join :: Bool
cfg_set_join :: Config -> Bool
cfg_use_connectedness_in_ground_joining :: Config -> Bool
cfg_use_connectedness_standalone :: Config -> Bool
cfg_ground_join :: Config -> Bool
..} (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Term f -> Term f -> Reduction f
reduce cp :: CriticalPair f
cp@CriticalPair{cp_eqn :: forall f. CriticalPair f -> Equation f
cp_eqn = Term f
lhs :=: Term f
rhs, Maybe (Term f)
Derivation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
..}
| (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a -> Equation f -> Bool
forall a f.
(Has a (Rule f), Function f) =>
(Index f (Equation f), Index f (Rule f))
-> RuleIndex f a -> Equation f -> Bool
subsumed (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Equation f
eqn = Maybe (CriticalPair f)
forall a. Maybe a
Nothing
| Bool
otherwise =
CriticalPair f -> Maybe (CriticalPair f)
forall a. a -> Maybe a
Just CriticalPair f
cp {
cp_eqn :: Equation f
cp_eqn = Equation f
eqn,
cp_proof :: Derivation f
cp_proof =
Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Proof.symm (Term f -> Reduction f -> Derivation f
forall f. Function f => Term f -> Reduction f -> Derivation f
reductionProof Term f
lhs Reduction f
lred) Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans`
Derivation f
cp_proof Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans`
Term f -> Reduction f -> Derivation f
forall f. Function f => Term f -> Reduction f -> Derivation f
reductionProof Term f
rhs Reduction f
rred }
where
lred :: Reduction f
lred = Term f -> Term f -> Reduction f
reduce Term f
lhs Term f
rhs
rred :: Reduction f
rred = Term f -> Term f -> Reduction f
reduce Term f
rhs Term f
lhs
eqn :: Equation f
eqn = Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
lhs Reduction f
lred Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
rhs Reduction f
rred
{-# INLINEABLE subsumed #-}
subsumed ::
(Has a (Rule f), Function f) =>
(Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Equation f -> Bool
subsumed :: (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a -> Equation f -> Bool
subsumed (Index f (Equation f)
eqns, Index f (Rule f)
complete) RuleIndex f a
idx (Term f
t :=: Term f
u)
| Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u = Bool
True
| Bool
otherwise = Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool
forall a f.
Has a (Rule f) =>
Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool
subsumed1 Index f (Equation f)
eqns RuleIndex f a
idx (Term f -> Term f
norm Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f -> Term f
norm Term f
u)
where
norm :: Term f -> Term f
norm Term f
t
| Index f (Rule f) -> Bool
forall f a. Index f a -> Bool
Index.null Index f (Rule f)
complete = Term f
t
| Bool
otherwise = Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
t (Reduction f -> Term f) -> Reduction f -> Term f
forall a b. (a -> b) -> a -> b
$ (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (Bool -> Term f -> Bool
forall a b. a -> b -> a
const Bool
True) ((Rule f -> Subst f -> Bool) -> Index f (Rule f) -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reducesSkolem Index f (Rule f)
complete) Term f
t
subsumed1 :: Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool
subsumed1 Index f (Equation f)
eqns RuleIndex f a
idx (Term f
t :=: Term f
u)
| Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u = Bool
True
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u | Rule f
rule <- TermOf (Rule f) -> Index (ConstantOf (Rule f)) a -> [Rule f]
forall a b.
(Has a b, Symbolic b, Has b (TermOf b)) =>
TermOf b -> Index (ConstantOf b) a -> [b]
Index.lookup Term f
TermOf (Rule f)
t (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx) ] = Bool
True
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
t | Rule f
rule <- TermOf (Rule f) -> Index (ConstantOf (Rule f)) a -> [Rule f]
forall a b.
(Has a b, Symbolic b, Has b (TermOf b)) =>
TermOf b -> Index (ConstantOf b) a -> [b]
Index.lookup Term f
TermOf (Rule f)
u (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx) ] = Bool
True
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Term f
u Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
u'
| (Subst f
sub, Term f
t' :=: Term f
u') <- Term f -> Index f (Equation f) -> [(Subst f, Equation f)]
forall f a. Term f -> Index f a -> [(Subst f, a)]
Index.matches Term f
t Index f (Equation f)
eqns ] = Bool
True
subsumed1 Index f (Equation f)
eqns RuleIndex f a
idx (App Fun f
f TermList f
ts :=: App Fun f
g TermList f
us)
| Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
g =
let
sub :: TermList f -> TermList f -> Bool
sub TermList f
Empty TermList f
Empty = Bool
True
sub (Cons Term f
t TermList f
ts) (Cons Term f
u TermList f
us) =
Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool
subsumed1 Index f (Equation f)
eqns RuleIndex f a
idx (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u) Bool -> Bool -> Bool
&& TermList f -> TermList f -> Bool
sub TermList f
ts TermList f
us
sub TermList f
_ TermList f
_ = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"Function used with multiple arities"
in
TermList f -> TermList f -> Bool
sub TermList f
ts TermList f
us
subsumed1 Index f (Equation f)
_ RuleIndex f a
_ Equation f
_ = Bool
False
{-# INLINEABLE groundJoin #-}
groundJoin ::
(Function f, Has a (Rule f)) =>
Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoin :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoin Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx [Branch f]
ctx cp :: CriticalPair f
cp@CriticalPair{cp_eqn :: forall f. CriticalPair f -> Equation f
cp_eqn = Term f
t :=: Term f
u, Maybe (Term f)
Derivation f
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
..} =
case [Either (Model f) (Subst f)] -> ([Model f], [Subst f])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ((Branch f -> Either (Model f) (Subst f))
-> [Branch f] -> [Either (Model f) (Subst f)]
forall a b. (a -> b) -> [a] -> [b]
map ([Atom f] -> Branch f -> Either (Model f) (Subst f)
forall f.
(Minimal f, Ordered f, PrettyTerm f, Labelled f) =>
[Atom f] -> Branch f -> Either (Model f) (Subst f)
solve ([Atom f] -> [Atom f]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Atom f]
forall f. Term f -> [Atom f]
atoms Term f
t [Atom f] -> [Atom f] -> [Atom f]
forall a. [a] -> [a] -> [a]
++ Term f -> [Atom f]
forall f. Term f -> [Atom f]
atoms Term f
u))) [Branch f]
ctx) of
([], [Subst f]
instances) ->
let cps :: [CriticalPair f]
cps = [ Subst f -> CriticalPair f -> CriticalPair f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub CriticalPair f
cp | Subst f
sub <- [Subst f]
instances ] in
(Maybe (CriticalPair f), [CriticalPair f])
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall a b. b -> Either a b
Right (CriticalPair f -> Maybe (CriticalPair f)
forall a. a -> Maybe a
Just CriticalPair f
cp, (CriticalPair f -> CriticalPair f -> Ordering)
-> [CriticalPair f] -> [CriticalPair f]
forall a. (a -> a -> Ordering) -> [a] -> [a]
usortBy ((CriticalPair f -> Equation f)
-> CriticalPair f -> CriticalPair f -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Equation f -> Equation f
forall f. Function f => Equation f -> Equation f
order (Equation f -> Equation f)
-> (CriticalPair f -> Equation f) -> CriticalPair f -> Equation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CriticalPair f -> Equation f
forall f. CriticalPair f -> Equation f
cp_eqn)) [CriticalPair f]
cps)
(Model f
model:[Model f]
_, [Subst f]
_) ->
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Model f
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Model f
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFrom Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Model f
model [Branch f]
ctx CriticalPair f
cp
{-# INLINEABLE groundJoinFrom #-}
groundJoinFrom ::
(Function f, Has a (Rule f)) =>
Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFrom :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Model f
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFrom config :: Config
config@Config{Bool
cfg_set_join :: Bool
cfg_use_connectedness_in_ground_joining :: Bool
cfg_use_connectedness_standalone :: Bool
cfg_ground_join :: Bool
cfg_set_join :: Config -> Bool
cfg_use_connectedness_in_ground_joining :: Config -> Bool
cfg_use_connectedness_standalone :: Config -> Bool
cfg_ground_join :: Config -> Bool
..} (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Model f
model [Branch f]
ctx cp :: CriticalPair f
cp@CriticalPair{cp_eqn :: forall f. CriticalPair f -> Equation f
cp_eqn = Term f
t :=: Term f
u, Maybe (Term f)
Derivation f
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
..}
| Bool -> Bool
not Bool
cfg_ground_join = Model f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall a b. a -> Either a b
Left Model f
model
| Model f -> Bool
modelOK Model f
model Bool -> Bool -> Bool
&& Maybe (CriticalPair f) -> Bool
forall a. Maybe a -> Bool
isJust (Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
allSteps Config
config' (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx CriticalPair f
cp { cp_eqn :: Equation f
cp_eqn = Term f
t' Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u' }) = Model f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall a b. a -> Either a b
Left Model f
model
| Bool
otherwise =
let
model' :: Model f
model'
| Model f -> Bool
modelOK Model f
model =
(Model f -> [Model f]) -> (Model f -> Bool) -> Model f -> Model f
forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise Model f -> [Model f]
forall f. Model f -> [Model f]
weakenModel (\Model f
m -> Model f -> Bool
modelOK Model f
m Bool -> Bool -> Bool
&& Maybe (CriticalPair f) -> Bool
forall a. Maybe a -> Bool
isNothing (Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> CriticalPair f
-> Maybe (CriticalPair f)
allSteps Config
config' (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx CriticalPair f
cp { cp_eqn :: Equation f
cp_eqn = Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
t (Model f -> Term f -> Term f -> Reduction f
normaliseIn Model f
m Term f
t Term f
u) Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
u (Model f -> Term f -> Term f -> Reduction f
normaliseIn Model f
m Term f
u Term f
t) })) (Model f -> Model f) -> Model f -> Model f
forall a b. (a -> b) -> a -> b
$
(Model f -> [Model f]) -> (Model f -> Bool) -> Model f -> Model f
forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise Model f -> [Model f]
forall f. Model f -> [Model f]
weakenModel (\Model f
m -> Model f -> Bool
modelOK Model f
m Bool -> Bool -> Bool
&& (Model f -> Reduction f -> Bool
forall f. Function f => Model f -> Reduction f -> Bool
valid Model f
m Reduction f
nt Bool -> Bool -> Bool
&& Model f -> Reduction f -> Bool
forall f. Function f => Model f -> Reduction f -> Bool
valid Model f
m Reduction f
nu)) Model f
model
| Bool
otherwise =
(Model f -> [Model f]) -> (Model f -> Bool) -> Model f -> Model f
forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise Model f -> [Model f]
forall f. Model f -> [Model f]
weakenModel (Bool -> Bool
not (Bool -> Bool) -> (Model f -> Bool) -> Model f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model f -> Bool
modelOK) Model f
model
diag :: [Formula f] -> Formula f
diag [] = [Formula f] -> Formula f
forall f. [Formula f] -> Formula f
Or []
diag (Formula f
r:[Formula f]
rs) = Formula f -> Formula f
forall f. Formula f -> Formula f
negateFormula Formula f
r Formula f -> Formula f -> Formula f
forall f. Formula f -> Formula f -> Formula f
||| (Formula f -> Formula f
forall f. Formula f -> Formula f
weaken Formula f
r Formula f -> Formula f -> Formula f
forall f. Formula f -> Formula f -> Formula f
&&& [Formula f] -> Formula f
diag [Formula f]
rs)
weaken :: Formula f -> Formula f
weaken (LessEq Atom f
t Atom f
u) = Atom f -> Atom f -> Formula f
forall f. Atom f -> Atom f -> Formula f
Less Atom f
t Atom f
u
weaken Formula f
x = Formula f
x
ctx' :: [Branch f]
ctx' = Formula f -> [Branch f] -> [Branch f]
forall f.
(Minimal f, Ordered f, Labelled f) =>
Formula f -> [Branch f] -> [Branch f]
formAnd ([Formula f] -> Formula f
forall f. [Formula f] -> Formula f
diag (Model f -> [Formula f]
forall f. Model f -> [Formula f]
modelToLiterals Model f
model')) [Branch f]
ctx in
case Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoin Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx [Branch f]
ctx' CriticalPair f
cp of
Right (Maybe (CriticalPair f)
_, [CriticalPair f]
cps) | Bool -> Bool
not (Model f -> Bool
modelOK Model f
model) ->
(Maybe (CriticalPair f), [CriticalPair f])
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall a b. b -> Either a b
Right (Maybe (CriticalPair f)
forall a. Maybe a
Nothing, [CriticalPair f]
cps)
Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
res -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
res
where
config' :: Config
config' = Config
config{cfg_use_connectedness_standalone :: Bool
cfg_use_connectedness_standalone = Bool
False}
normaliseIn :: Model f -> Term f -> Term f -> Reduction f
normaliseIn Model f
m Term f
t Term f
u =
case Maybe (Term f)
cp_top of
Just Term f
top | Bool
cfg_use_connectedness_in_ground_joining ->
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (Model f -> Term f -> Term f -> Bool
forall f. Ordered f => Model f -> Term f -> Term f -> Bool
connectedIn Model f
m Term f
top) ((Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (Term f -> Term f -> Model f -> Rule f -> Subst f -> Bool
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
Labelled f) =>
Term f -> Term f -> Model f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u Model f
model) (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) Term f
t
Maybe (Term f)
_ -> (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (Bool -> Term f -> Bool
forall a b. a -> b -> a
const Bool
True) ((Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (Term f -> Term f -> Model f -> Rule f -> Subst f -> Bool
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
Labelled f) =>
Term f -> Term f -> Model f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u Model f
m) (RuleIndex f a -> Index f a
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) Term f
t
ok :: Term f -> Term f -> Model f -> Rule f -> Subst f -> Bool
ok Term f
t Term f
u Model f
m Rule f
rule Subst f
sub =
Model f -> Rule f -> Subst f -> Bool
forall f. Function f => Model f -> Rule f -> Subst f -> Bool
reducesInModel Model f
m Rule f
rule Subst f
sub Bool -> Bool -> Bool
&&
Rule f -> Equation f
forall f. Rule f -> Equation f
unorient Rule f
rule Equation f -> Equation f -> Bool
forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u)
connectedIn :: Model f -> Term f -> Term f -> Bool
connectedIn Model f
m Term f
top Term f
t =
Model f -> Term f -> Term f -> Maybe Strictness
forall f.
Ordered f =>
Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
m Term f
t Term f
top Maybe Strictness -> Maybe Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict
nt :: Reduction f
nt = Model f -> Term f -> Term f -> Reduction f
normaliseIn Model f
model Term f
t Term f
u
nu :: Reduction f
nu = Model f -> Term f -> Term f -> Reduction f
normaliseIn Model f
model Term f
u Term f
t
t' :: Term f
t' = Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
nt
u' :: Term f
u' = Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
u Reduction f
nu
modelOK :: Model f -> Bool
modelOK Model f
m =
case Maybe (Term f)
cp_top of
Maybe (Term f)
Nothing -> Bool
True
Just Term f
top ->
Maybe Strictness -> Bool
forall a. Maybe a -> Bool
isNothing (Model f -> Term f -> Term f -> Maybe Strictness
forall f.
Ordered f =>
Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
m Term f
top Term f
t) Bool -> Bool -> Bool
&& Maybe Strictness -> Bool
forall a. Maybe a -> Bool
isNothing (Model f -> Term f -> Term f -> Maybe Strictness
forall f.
Ordered f =>
Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
m Term f
top Term f
u)
{-# INLINEABLE groundJoinFromMaybe #-}
groundJoinFromMaybe ::
(Function f, Has a (Rule f)) =>
Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFromMaybe :: Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Maybe (Model f)
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFromMaybe Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Maybe (Model f)
Nothing = Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoin Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx
groundJoinFromMaybe Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx (Just Model f
model) = Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Model f
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Model f
-> [Branch f]
-> CriticalPair f
-> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
groundJoinFrom Config
config (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx Model f
model
{-# INLINEABLE valid #-}
valid :: Function f => Model f -> Reduction f -> Bool
valid :: Model f -> Reduction f -> Bool
valid Model f
model Reduction f
red =
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ Model f -> Rule f -> Subst f -> Bool
forall f. Function f => Model f -> Rule f -> Subst f -> Bool
reducesInModel Model f
model Rule f
rule Subst f
forall f. Subst f
emptySubst
| Rule f
rule <- Reduction f
red ]
optimise :: (a -> [a]) -> (a -> Bool) -> a -> a
optimise :: (a -> [a]) -> (a -> Bool) -> a -> a
optimise a -> [a]
f a -> Bool
p a
x =
case (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
p (a -> [a]
f a
x) of
a
y:[a]
_ -> (a -> [a]) -> (a -> Bool) -> a -> a
forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise a -> [a]
f a -> Bool
p a
y
[a]
_ -> a
x