-- | Tactics for joining critical pairs.
{-# 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 #-}
{-# SCC joinCriticalPair #-}
joinCriticalPair ::
  (Function f, Has a (Rule f)) =>
  Config ->
  (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a ->
  Maybe (Model f) -> -- A model to try before checking ground joinability
  CriticalPair f ->
  Either
    -- Failed to join critical pair.
    -- Returns simplified critical pair and model in which it failed to hold.
    (CriticalPair f, Model f)
    -- Split critical pair into several instances.
    -- Returns list of instances which must be joined,
    -- and an optional equation which can be added to the joinable set
    -- after successfully joining all instances.
    (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 _ _ = reducesOriented
   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 _ _ = reduces
    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
Depth
Max
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_max :: forall f. CriticalPair f -> Max
cp_depth :: forall f. CriticalPair f -> Depth
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_max :: Max
cp_depth :: Depth
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
    -- No need to do this symmetrically because addJoinable adds
    -- both orientations of each equation
  | [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'
       | Term f
t' :=: Term f
u' <- Term f -> Index f (Equation f) -> [Equation f]
forall f a. Term f -> Index f a -> [a]
Index.approxMatches Term f
t Index f (Equation f)
eqns,
         Subst f
sub <- Maybe (Subst f) -> [Subst f]
forall a. Maybe a -> [a]
maybeToList (Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
match Term f
t' Term f
t) ] = 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
Depth
Max
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_max :: Max
cp_depth :: Depth
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_max :: forall f. CriticalPair f -> Max
cp_depth :: forall f. CriticalPair f -> Depth
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 a. Symbolic a => a -> a
canonicalise (Equation f -> Equation f)
-> (CriticalPair f -> Equation f) -> CriticalPair f -> Equation f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
Depth
Max
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_max :: Max
cp_depth :: Depth
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_max :: forall f. CriticalPair f -> Max
cp_depth :: forall f. CriticalPair f -> Depth
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