-- | 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 {
    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) -> -- 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 :: forall f a.
(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
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 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 ->
      forall a b. b -> Either a b
Right (forall a. Maybe a
Nothing, [])
    Maybe (CriticalPair f)
_ | Config -> Bool
cfg_set_join Config
config Bool -> Bool -> Bool
&&
        Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection
          (forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
normalForms (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite forall f. Function f => Rule f -> Subst f -> Bool
reduces (forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) (forall k a. k -> a -> Map k a
Map.singleton Term f
t []))
          (forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
normalForms (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite forall f. Function f => Rule f -> Subst f -> Bool
reduces (forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) (forall k a. k -> a -> Map k a
Map.singleton Term f
u []))) ->
      forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just CriticalPair f
cp, [])
    Just CriticalPair f
cp ->
      case 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 (forall f.
(Minimal f, Ordered f, Labelled f) =>
Formula f -> [Branch f]
branches (forall f. [Formula f] -> Formula f
And [])) CriticalPair f
cp of
        Left Model f
model -> forall a b. a -> Either a b
Left (CriticalPair f
cp, Model f
model)
        Right (Maybe (CriticalPair f)
mcp, [CriticalPair f]
cps) -> 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 :: 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 =
  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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
  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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
  forall f. Function f => CriticalPair f -> Maybe (CriticalPair f)
checkOrder forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
  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 :: forall f. Function f => CriticalPair f -> Maybe (CriticalPair f)
checkOrder CriticalPair f
cp
  | forall {f}. Ordered f => CriticalPair f -> Bool
tooBig CriticalPair f
cp = forall a. Maybe a
Nothing
  | Bool
otherwise = 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} =
      forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
top Term f
t Bool -> Bool -> Bool
|| forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
top Term f
u
    tooBig CriticalPair f
_ = Bool
False
step1 :: 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
cfg (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx = 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 -> forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (forall a b. a -> b -> a
const Bool
True) (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (forall {f}.
(Ordered 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) (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 = forall f. Function f => Rule f -> Subst f -> Bool
reducesOriented Rule f
rule Subst f
sub Bool -> Bool -> Bool
&& forall f. Rule f -> Equation f
unorient Rule f
rule forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` (Term f
t forall f. Term f -> Term f -> Equation f
:=: Term f
u)
step2 :: 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
cfg (Index f (Equation f), Index f (Rule f))
eqns RuleIndex f a
idx = 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 -> forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (forall a b. a -> b -> a
const Bool
True) (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (forall {f}.
(Ordered 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) (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 = forall f. Function f => Rule f -> Subst f -> Bool
reduces Rule f
rule Subst f
sub Bool -> Bool -> Bool
&& forall f. Rule f -> Equation f
unorient Rule f
rule forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` (Term f
t forall f. Term f -> Term f -> Equation f
:=: Term f
u)
step3 :: 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 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 = forall a. a -> Maybe a
Just CriticalPair f
cp
  | Bool
otherwise =
    case 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 (forall a. Symbolic a => a -> a
flipCP (CriticalPair f
cp, Term f
top))) of
          (Just CriticalPair f
cp1, Just CriticalPair f
cp2) ->
            case forall f. Function f => Equation f -> Equation f -> Bool
simplerThan (forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp1) (forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp2) of
              Bool
True -> forall a. a -> Maybe a
Just CriticalPair f
cp1
              Bool
False -> forall a. a -> Maybe a
Just CriticalPair f
cp2
          (Maybe (CriticalPair f), Maybe (CriticalPair f))
_ -> forall a. Maybe a
Nothing
      Maybe (Term 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) =
      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 -> forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (forall f. Ordered f => Term f -> Term f -> Bool
`lessThan` Term f
top) (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (forall {f}.
(Ordered 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) (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 =
      forall f. Rule f -> Equation f
unorient Rule f
rule forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` (Term f
t forall f. Term f -> Term f -> Equation f
:=: Term f
u) Bool -> Bool -> Bool
&&
      forall f. Function f => Rule f -> Subst f -> Bool
reducesSkolem Rule f
rule Subst f
sub

    flipCP :: Symbolic a => a -> a
    flipCP :: forall a. Symbolic a => a -> a
flipCP a
t = 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 = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0forall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map forall a. Enum a => a -> Int
fromEnum (forall a. Symbolic a => a -> [Var]
vars a
t))
        sub :: Var -> Builder (ConstantOf a)
sub (V Int
x) = forall f. Var -> Builder f
var (Int -> Var
V (Int
n 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 :: 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{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)
..}
  | 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 = forall a. Maybe a
Nothing
  | Bool
otherwise =
    forall a. a -> Maybe a
Just CriticalPair f
cp {
      cp_eqn :: Equation f
cp_eqn = Equation f
eqn,
      cp_proof :: Derivation f
cp_proof =
        forall f. Derivation f -> Derivation f
Proof.symm (forall f. Function f => Term f -> Reduction f -> Derivation f
reductionProof Term f
lhs Reduction f
lred) forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans`
        Derivation f
cp_proof forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans`
        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 = forall f. Term f -> Reduction f -> Term f
result Term f
lhs Reduction f
lred forall f. Term f -> Term f -> Equation 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 :: 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)
eqns, Index f (Rule f)
complete) RuleIndex f a
idx (Term f
t :=: Term f
u)
  | Term f
t forall a. Eq a => a -> a -> Bool
== Term f
u = Bool
True
  | Bool
otherwise = 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 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
      | forall f a. Index f a -> Bool
Index.null Index f (Rule f)
complete = Term f
t
      | Bool
otherwise = forall f. Term f -> Reduction f -> Term f
result Term f
t forall a b. (a -> b) -> a -> b
$ forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (forall a b. a -> b -> a
const Bool
True) (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite 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 forall a. Eq a => a -> a -> Bool
== Term f
u = Bool
True
  | forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ forall f. Rule f -> Term f
rhs Rule f
rule forall a. Eq a => a -> a -> Bool
== Term f
u | Rule f
rule <- forall a b.
(Has a b, Symbolic b, Has b (TermOf b)) =>
TermOf b -> Index (ConstantOf b) a -> [b]
Index.lookup Term f
t (forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx) ] = Bool
True
  | forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ forall f. Rule f -> Term f
rhs Rule f
rule forall a. Eq a => a -> a -> Bool
== Term f
t | Rule f
rule <- forall a b.
(Has a b, Symbolic b, Has b (TermOf b)) =>
TermOf b -> Index (ConstantOf b) a -> [b]
Index.lookup Term f
u (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
  | forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Term f
u forall a. Eq a => a -> a -> Bool
== 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
_ :=: Term f
u') <- 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 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 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
_ = 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 :: 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 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 forall a b. [Either a b] -> ([a], [b])
partitionEithers (forall a b. (a -> b) -> [a] -> [b]
map (forall f.
(Minimal f, Ordered f, PrettyTerm f, Labelled f) =>
[Atom f] -> Branch f -> Either (Model f) (Subst f)
solve (forall a. Ord a => [a] -> [a]
usort (forall f. Term f -> [Atom f]
atoms Term f
t forall a. [a] -> [a] -> [a]
++ forall f. Term f -> [Atom f]
atoms Term f
u))) [Branch f]
ctx) of
    ([], [Subst f]
instances) ->
      let cps :: [CriticalPair f]
cps = [ 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
      forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Just CriticalPair f
cp, forall a. (a -> a -> Ordering) -> [a] -> [a]
usortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (forall f. Function f => Equation f -> Equation f
order forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. CriticalPair f -> Equation f
cp_eqn)) [CriticalPair f]
cps)
    (Model f
model:[Model f]
_, [Subst 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 :: 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
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 = forall a b. a -> Either a b
Left Model f
model
  | Model f -> Bool
modelOK Model f
model Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isJust (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' forall f. Term f -> Term f -> Equation f
:=: Term f
u' }) = 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 =
            forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise forall f. Model f -> [Model f]
weakenModel (\Model f
m -> Model f -> Bool
modelOK Model f
m Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (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 = 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) forall f. Term f -> Term f -> Equation 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) })) forall a b. (a -> b) -> a -> b
$
            forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise forall f. Model f -> [Model f]
weakenModel (\Model f
m -> Model f -> Bool
modelOK Model f
m Bool -> Bool -> Bool
&& (forall f. Function f => Model f -> Reduction f -> Bool
valid Model f
m Reduction f
nt Bool -> Bool -> Bool
&& forall f. Function f => Model f -> Reduction f -> Bool
valid Model f
m Reduction f
nu)) Model f
model
          | Bool
otherwise =
            forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise forall f. Model f -> [Model f]
weakenModel (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model f -> Bool
modelOK) Model f
model

        diag :: [Formula f] -> Formula f
diag [] = forall f. [Formula f] -> Formula f
Or []
        diag (Formula f
r:[Formula f]
rs) = forall f. Formula f -> Formula f
negateFormula Formula f
r forall {f}. Formula f -> Formula f -> Formula f
||| (forall f. Formula f -> Formula f
weaken Formula f
r 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) = 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' = forall f.
(Minimal f, Ordered f, Labelled f) =>
Formula f -> [Branch f] -> [Branch f]
formAnd (forall f. [Formula f] -> Formula f
diag (forall f. Model f -> [Formula f]
modelToLiterals Model f
model')) [Branch f]
ctx in

      case 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) ->
          forall a b. b -> Either a b
Right (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 ->
          forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (forall {f}. Ordered f => Model f -> Term f -> Term f -> Bool
connectedIn Model f
m Term f
top) (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (forall {f}.
(Ordered 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) (forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f a
idx)) Term f
t
        Maybe (Term f)
_ -> forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (forall a b. a -> b -> a
const Bool
True) (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite (forall {f}.
(Ordered 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) (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 =
      forall f. Function f => Model f -> Rule f -> Subst f -> Bool
reducesInModel Model f
m Rule f
rule Subst f
sub Bool -> Bool -> Bool
&&
      forall f. Rule f -> Equation f
unorient Rule f
rule forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` (Term f
t 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 =
      forall f.
Ordered f =>
Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
m Term f
t Term f
top forall a. Eq a => a -> a -> Bool
== 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' = forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
nt
    u' :: Term f
u' = 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 ->
          forall a. Maybe a -> Bool
isNothing (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
&& forall a. Maybe a -> Bool
isNothing (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 :: 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)
Nothing = 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) = 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 :: forall f. Function f => Model f -> Reduction f -> Bool
valid Model f
model Reduction f
red =
  forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ forall f. Function f => Model f -> Rule f -> Subst f -> Bool
reducesInModel Model f
model Rule f
rule forall f. Subst f
emptySubst
      | Rule f
rule <- Reduction f
red ]

optimise :: (a -> [a]) -> (a -> Bool) -> a -> a
optimise :: forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise a -> [a]
f a -> Bool
p a
x =
  case forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
p (a -> [a]
f a
x) of
    a
y:[a]
_ -> forall a. (a -> [a]) -> (a -> Bool) -> a -> a
optimise a -> [a]
f a -> Bool
p a
y
    [a]
_   -> a
x