-- | Critical pair generation.
{-# LANGUAGE BangPatterns, FlexibleContexts, ScopedTypeVariables, MultiParamTypeClasses, RecordWildCards, OverloadedStrings, TypeFamilies, GeneralizedNewtypeDeriving #-}
module Twee.CP where

import qualified Twee.Term as Term
import Twee.Base
import Twee.Rule
import Twee.Index(Index)
import qualified Data.Set as Set
import Control.Monad
import Data.List
import qualified Data.ChurchList as ChurchList
import Data.ChurchList (ChurchList(..))
import Twee.Utils
import Twee.Equation
import qualified Twee.Proof as Proof
import Twee.Proof(Derivation, congPath)
import Data.IntSet(IntSet)
import qualified Data.IntSet as IntSet

newtype Max = Max { Max -> IntSet
unMax :: IntSet }
  deriving (Max -> Max -> Bool
(Max -> Max -> Bool) -> (Max -> Max -> Bool) -> Eq Max
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Max -> Max -> Bool
$c/= :: Max -> Max -> Bool
== :: Max -> Max -> Bool
$c== :: Max -> Max -> Bool
Eq, Eq Max
Eq Max
-> (Max -> Max -> Ordering)
-> (Max -> Max -> Bool)
-> (Max -> Max -> Bool)
-> (Max -> Max -> Bool)
-> (Max -> Max -> Bool)
-> (Max -> Max -> Max)
-> (Max -> Max -> Max)
-> Ord Max
Max -> Max -> Bool
Max -> Max -> Ordering
Max -> Max -> Max
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Max -> Max -> Max
$cmin :: Max -> Max -> Max
max :: Max -> Max -> Max
$cmax :: Max -> Max -> Max
>= :: Max -> Max -> Bool
$c>= :: Max -> Max -> Bool
> :: Max -> Max -> Bool
$c> :: Max -> Max -> Bool
<= :: Max -> Max -> Bool
$c<= :: Max -> Max -> Bool
< :: Max -> Max -> Bool
$c< :: Max -> Max -> Bool
compare :: Max -> Max -> Ordering
$ccompare :: Max -> Max -> Ordering
$cp1Ord :: Eq Max
Ord, Int -> Max -> ShowS
[Max] -> ShowS
Max -> String
(Int -> Max -> ShowS)
-> (Max -> String) -> ([Max] -> ShowS) -> Show Max
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Max] -> ShowS
$cshowList :: [Max] -> ShowS
show :: Max -> String
$cshow :: Max -> String
showsPrec :: Int -> Max -> ShowS
$cshowsPrec :: Int -> Max -> ShowS
Show)

-- | The set of positions at which a term can have critical overlaps.
data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)
type PositionsOf a = Positions (ConstantOf a)

instance Show (Positions f) where
  show :: Positions f -> String
show = [Int] -> String
forall a. Show a => a -> String
show ([Int] -> String)
-> (Positions f -> [Int]) -> Positions f -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChurchList Int -> [Int]
forall a. ChurchList a -> [a]
ChurchList.toList (ChurchList Int -> [Int])
-> (Positions f -> ChurchList Int) -> Positions f -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Positions f -> ChurchList Int
forall f. Positions f -> ChurchList Int
positionsChurch

-- | Calculate the set of positions for a term.
positions :: Term f -> Positions f
positions :: Term f -> Positions f
positions Term f
t = Int -> Set (Term f) -> TermList f -> Positions f
forall f f. Int -> Set (Term f) -> TermList f -> Positions f
aux Int
0 Set (Term f)
forall a. Set a
Set.empty (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t)
  where
    -- Consider only general superpositions.
    aux :: Int -> Set (Term f) -> TermList f -> Positions f
aux !Int
_ !Set (Term f)
_ TermList f
Empty = Positions f
forall f. Positions f
NilP
    aux Int
n Set (Term f)
m (Cons (Var Var
_) TermList f
t) = Int -> Set (Term f) -> TermList f -> Positions f
aux (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Set (Term f)
m TermList f
t
    aux Int
n Set (Term f)
m ConsSym{hd :: forall f. TermList f -> Term f
hd = t :: Term f
t@App{}, rest :: forall f. TermList f -> TermList f
rest = TermList f
u}
      | Term f
t Term f -> Set (Term f) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Term f)
m = Int -> Set (Term f) -> TermList f -> Positions f
aux (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Set (Term f)
m TermList f
u
      | Bool
otherwise = Int -> Positions f -> Positions f
forall f. Int -> Positions f -> Positions f
ConsP Int
n (Int -> Set (Term f) -> TermList f -> Positions f
aux (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Term f -> Set (Term f) -> Set (Term f)
forall a. Ord a => a -> Set a -> Set a
Set.insert Term f
t Set (Term f)
m) TermList f
u)

{-# INLINE positionsChurch #-}
positionsChurch :: Positions f -> ChurchList Int
positionsChurch :: Positions f -> ChurchList Int
positionsChurch Positions f
posns =
  (forall b. (Int -> b -> b) -> b -> b) -> ChurchList Int
forall a. (forall b. (a -> b -> b) -> b -> b) -> ChurchList a
ChurchList ((forall b. (Int -> b -> b) -> b -> b) -> ChurchList Int)
-> (forall b. (Int -> b -> b) -> b -> b) -> ChurchList Int
forall a b. (a -> b) -> a -> b
$ \Int -> b -> b
c b
n ->
    let
      pos :: Positions f -> b
pos Positions f
NilP = b
n
      pos (ConsP Int
x Positions f
posns) = Int -> b -> b
c Int
x (Positions f -> b
pos Positions f
posns)
    in
      Positions f -> b
pos Positions f
posns

-- | A critical overlap of one rule with another.
data Overlap f =
  Overlap {
    -- | The depth (1 for CPs of axioms, 2 for CPs whose rules have depth 1, etc.)
    Overlap f -> Depth
overlap_depth :: {-# UNPACK #-} !Depth,
    -- | The critical term.
    Overlap f -> Term f
overlap_top   :: {-# UNPACK #-} !(Term f),
    -- | The part of the critical term which the inner rule rewrites.
    Overlap f -> Term f
overlap_inner :: {-# UNPACK #-} !(Term f),
    -- | The position in the critical term which is rewritten.
    Overlap f -> Int
overlap_pos   :: {-# UNPACK #-} !Int,
    -- | The critical pair itself.
    Overlap f -> Equation f
overlap_eqn   :: {-# UNPACK #-} !(Equation f) }
  deriving Int -> Overlap f -> ShowS
[Overlap f] -> ShowS
Overlap f -> String
(Int -> Overlap f -> ShowS)
-> (Overlap f -> String)
-> ([Overlap f] -> ShowS)
-> Show (Overlap f)
forall f. (Labelled f, Show f) => Int -> Overlap f -> ShowS
forall f. (Labelled f, Show f) => [Overlap f] -> ShowS
forall f. (Labelled f, Show f) => Overlap f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Overlap f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Overlap f] -> ShowS
show :: Overlap f -> String
$cshow :: forall f. (Labelled f, Show f) => Overlap f -> String
showsPrec :: Int -> Overlap f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Overlap f -> ShowS
Show
type OverlapOf a = Overlap (ConstantOf a)

-- | Represents the depth of a critical pair.
newtype Depth = Depth Int deriving (Depth -> Depth -> Bool
(Depth -> Depth -> Bool) -> (Depth -> Depth -> Bool) -> Eq Depth
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Depth -> Depth -> Bool
$c/= :: Depth -> Depth -> Bool
== :: Depth -> Depth -> Bool
$c== :: Depth -> Depth -> Bool
Eq, Eq Depth
Eq Depth
-> (Depth -> Depth -> Ordering)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> Ord Depth
Depth -> Depth -> Bool
Depth -> Depth -> Ordering
Depth -> Depth -> Depth
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Depth -> Depth -> Depth
$cmin :: Depth -> Depth -> Depth
max :: Depth -> Depth -> Depth
$cmax :: Depth -> Depth -> Depth
>= :: Depth -> Depth -> Bool
$c>= :: Depth -> Depth -> Bool
> :: Depth -> Depth -> Bool
$c> :: Depth -> Depth -> Bool
<= :: Depth -> Depth -> Bool
$c<= :: Depth -> Depth -> Bool
< :: Depth -> Depth -> Bool
$c< :: Depth -> Depth -> Bool
compare :: Depth -> Depth -> Ordering
$ccompare :: Depth -> Depth -> Ordering
$cp1Ord :: Eq Depth
Ord, Integer -> Depth
Depth -> Depth
Depth -> Depth -> Depth
(Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth)
-> (Depth -> Depth)
-> (Depth -> Depth)
-> (Integer -> Depth)
-> Num Depth
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Depth
$cfromInteger :: Integer -> Depth
signum :: Depth -> Depth
$csignum :: Depth -> Depth
abs :: Depth -> Depth
$cabs :: Depth -> Depth
negate :: Depth -> Depth
$cnegate :: Depth -> Depth
* :: Depth -> Depth -> Depth
$c* :: Depth -> Depth -> Depth
- :: Depth -> Depth -> Depth
$c- :: Depth -> Depth -> Depth
+ :: Depth -> Depth -> Depth
$c+ :: Depth -> Depth -> Depth
Num, Num Depth
Ord Depth
Num Depth -> Ord Depth -> (Depth -> Rational) -> Real Depth
Depth -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Depth -> Rational
$ctoRational :: Depth -> Rational
$cp2Real :: Ord Depth
$cp1Real :: Num Depth
Real, Int -> Depth
Depth -> Int
Depth -> [Depth]
Depth -> Depth
Depth -> Depth -> [Depth]
Depth -> Depth -> Depth -> [Depth]
(Depth -> Depth)
-> (Depth -> Depth)
-> (Int -> Depth)
-> (Depth -> Int)
-> (Depth -> [Depth])
-> (Depth -> Depth -> [Depth])
-> (Depth -> Depth -> [Depth])
-> (Depth -> Depth -> Depth -> [Depth])
-> Enum Depth
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Depth -> Depth -> Depth -> [Depth]
$cenumFromThenTo :: Depth -> Depth -> Depth -> [Depth]
enumFromTo :: Depth -> Depth -> [Depth]
$cenumFromTo :: Depth -> Depth -> [Depth]
enumFromThen :: Depth -> Depth -> [Depth]
$cenumFromThen :: Depth -> Depth -> [Depth]
enumFrom :: Depth -> [Depth]
$cenumFrom :: Depth -> [Depth]
fromEnum :: Depth -> Int
$cfromEnum :: Depth -> Int
toEnum :: Int -> Depth
$ctoEnum :: Int -> Depth
pred :: Depth -> Depth
$cpred :: Depth -> Depth
succ :: Depth -> Depth
$csucc :: Depth -> Depth
Enum, Enum Depth
Real Depth
Real Depth
-> Enum Depth
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> (Depth, Depth))
-> (Depth -> Depth -> (Depth, Depth))
-> (Depth -> Integer)
-> Integral Depth
Depth -> Integer
Depth -> Depth -> (Depth, Depth)
Depth -> Depth -> Depth
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: Depth -> Integer
$ctoInteger :: Depth -> Integer
divMod :: Depth -> Depth -> (Depth, Depth)
$cdivMod :: Depth -> Depth -> (Depth, Depth)
quotRem :: Depth -> Depth -> (Depth, Depth)
$cquotRem :: Depth -> Depth -> (Depth, Depth)
mod :: Depth -> Depth -> Depth
$cmod :: Depth -> Depth -> Depth
div :: Depth -> Depth -> Depth
$cdiv :: Depth -> Depth -> Depth
rem :: Depth -> Depth -> Depth
$crem :: Depth -> Depth -> Depth
quot :: Depth -> Depth -> Depth
$cquot :: Depth -> Depth -> Depth
$cp2Integral :: Enum Depth
$cp1Integral :: Real Depth
Integral, Int -> Depth -> ShowS
[Depth] -> ShowS
Depth -> String
(Int -> Depth -> ShowS)
-> (Depth -> String) -> ([Depth] -> ShowS) -> Show Depth
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Depth] -> ShowS
$cshowList :: [Depth] -> ShowS
show :: Depth -> String
$cshow :: Depth -> String
showsPrec :: Int -> Depth -> ShowS
$cshowsPrec :: Int -> Depth -> ShowS
Show)

-- | Compute all overlaps of a rule with a set of rules.
{-# INLINEABLE overlaps #-}
overlaps ::
  forall a f. (Function f, Has a Id, Has a (Rule f), Has a (Positions f), Has a Depth) =>
  Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)]
overlaps :: Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)]
overlaps Depth
max_depth Index f a
idx [a]
rules a
r =
  ChurchList (a, a, Overlap f) -> [(a, a, Overlap f)]
forall a. ChurchList a -> [a]
ChurchList.toList (Depth -> Index f a -> [a] -> a -> ChurchList (a, a, Overlap f)
forall f a.
(Function f, Has a (Rule f), Has a (Positions f), Has a Depth) =>
Depth -> Index f a -> [a] -> a -> ChurchList (a, a, Overlap f)
overlapsChurch Depth
max_depth Index f a
idx [a]
rules a
r)

{-# INLINE overlapsChurch #-}
overlapsChurch :: forall f a.
  (Function f, Has a (Rule f), Has a (Positions f), Has a Depth) =>
  Depth -> Index f a -> [a] -> a -> ChurchList (a, a, Overlap f)
overlapsChurch :: Depth -> Index f a -> [a] -> a -> ChurchList (a, a, Overlap f)
overlapsChurch Depth
max_depth Index f a
idx [a]
rules a
r1 = do
  Bool -> ChurchList ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a -> Depth
forall a b. Has a b => a -> b
the a
r1 Depth -> Depth -> Bool
forall a. Ord a => a -> a -> Bool
< Depth
max_depth)
  a
r2 <- [a] -> ChurchList a
forall a. [a] -> ChurchList a
ChurchList.fromList [a]
rules
  Bool -> ChurchList ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a -> Depth
forall a b. Has a b => a -> b
the a
r2 Depth -> Depth -> Bool
forall a. Ord a => a -> a -> Bool
< Depth
max_depth)
  let !depth :: Depth
depth = Depth
1 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ Depth -> Depth -> Depth
forall a. Ord a => a -> a -> a
max (a -> Depth
forall a b. Has a b => a -> b
the a
r1) (a -> Depth
forall a b. Has a b => a -> b
the a
r2)
  do { Overlap f
o <- Index f a
-> Depth
-> Positions f
-> Rule f
-> Rule f
-> ChurchList (Overlap f)
forall f a.
(Function f, Has a (Rule f), Has a Depth) =>
Index f a
-> Depth
-> Positions f
-> Rule f
-> Rule f
-> ChurchList (Overlap f)
asymmetricOverlaps Index f a
idx Depth
depth (a -> Positions f
forall a b. Has a b => a -> b
the a
r1) Rule f
r1' (a -> Rule f
forall a b. Has a b => a -> b
the a
r2); (a, a, Overlap f) -> ChurchList (a, a, Overlap f)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
r1, a
r2, Overlap f
o) } ChurchList (a, a, Overlap f)
-> ChurchList (a, a, Overlap f) -> ChurchList (a, a, Overlap f)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
    do { Overlap f
o <- Index f a
-> Depth
-> Positions f
-> Rule f
-> Rule f
-> ChurchList (Overlap f)
forall f a.
(Function f, Has a (Rule f), Has a Depth) =>
Index f a
-> Depth
-> Positions f
-> Rule f
-> Rule f
-> ChurchList (Overlap f)
asymmetricOverlaps Index f a
idx Depth
depth (a -> Positions f
forall a b. Has a b => a -> b
the a
r2) (a -> Rule f
forall a b. Has a b => a -> b
the a
r2) Rule f
r1'; (a, a, Overlap f) -> ChurchList (a, a, Overlap f)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
r2, a
r1, Overlap f
o) }
  where
    !r1' :: Rule f
r1' = [Rule f] -> Rule f -> Rule f
forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding ((a -> Rule f) -> [a] -> [Rule f]
forall a b. (a -> b) -> [a] -> [b]
map a -> Rule f
forall a b. Has a b => a -> b
the [a]
rules :: [Rule f]) (a -> Rule f
forall a b. Has a b => a -> b
the a
r1)

{-# INLINE asymmetricOverlaps #-}
asymmetricOverlaps ::
  (Function f, Has a (Rule f), Has a Depth) =>
  Index f a -> Depth -> Positions f -> Rule f -> Rule f -> ChurchList (Overlap f)
asymmetricOverlaps :: Index f a
-> Depth
-> Positions f
-> Rule f
-> Rule f
-> ChurchList (Overlap f)
asymmetricOverlaps Index f a
idx Depth
depth Positions f
posns Rule f
r1 Rule f
r2 = do
  Int
n <- Positions f -> ChurchList Int
forall f. Positions f -> ChurchList Int
positionsChurch Positions f
posns
  Maybe (Overlap f) -> ChurchList (Overlap f)
forall a. Maybe a -> ChurchList a
ChurchList.fromMaybe (Maybe (Overlap f) -> ChurchList (Overlap f))
-> Maybe (Overlap f) -> ChurchList (Overlap f)
forall a b. (a -> b) -> a -> b
$
    Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)
forall f. Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)
overlapAt Int
n Depth
depth Rule f
r1 Rule f
r2 Maybe (Overlap f)
-> (Overlap f -> Maybe (Overlap f)) -> Maybe (Overlap f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    Index f a -> Overlap f -> Maybe (Overlap f)
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap f -> Maybe (Overlap f)
simplifyOverlap Index f a
idx

-- | Create an overlap at a particular position in a term.
-- Doesn't simplify the overlap.
{-# INLINE overlapAt #-}
{-# SCC overlapAt #-}
overlapAt :: Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)
overlapAt :: Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)
overlapAt !Int
n !Depth
depth (Rule Orientation f
_ Proof f
_ !Term f
outer !Term f
outer') (Rule Orientation f
_ Proof f
_ !Term f
inner !Term f
inner') = do
  let t :: Term f
t = Int -> TermList f -> Term f
forall f. Int -> TermList f -> Term f
at Int
n (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
outer)
  TriangleSubst f
sub <- Term f -> Term f -> Maybe (TriangleSubst f)
forall f. Term f -> Term f -> Maybe (TriangleSubst f)
unifyTri Term f
inner Term f
t
  let
    top :: Term f
top = TriangleSubst f -> Term f -> Term f
forall f. TriangleSubst f -> Term f -> Term f
termSubst TriangleSubst f
sub Term f
outer
    innerTerm :: Term f
innerTerm = TriangleSubst f -> Term f -> Term f
forall f. TriangleSubst f -> Term f -> Term f
termSubst TriangleSubst f
sub Term f
inner
    -- Make sure to keep in sync with overlapProof
    lhs :: Term f
lhs = TriangleSubst f -> Term f -> Term f
forall f. TriangleSubst f -> Term f -> Term f
termSubst TriangleSubst f
sub Term f
outer'
    rhs :: Term f
rhs = TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
forall f.
TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
buildReplacePositionSub TriangleSubst f
sub Int
n (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
inner') (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
outer)

  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f
lhs Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
/= Term f
rhs)
  Overlap f -> Maybe (Overlap f)
forall (m :: * -> *) a. Monad m => a -> m a
return Overlap :: forall f.
Depth -> Term f -> Term f -> Int -> Equation f -> Overlap f
Overlap {
    overlap_depth :: Depth
overlap_depth = Depth
depth,
    overlap_top :: Term f
overlap_top = Term f
top,
    overlap_inner :: Term f
overlap_inner = Term f
innerTerm,
    overlap_pos :: Int
overlap_pos = Int
n,
    overlap_eqn :: Equation f
overlap_eqn = Term f
lhs Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
rhs }

-- | Simplify an overlap and remove it if it's trivial.
{-# INLINE simplifyOverlap #-}
simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap f -> Maybe (Overlap f)
simplifyOverlap :: Index f a -> Overlap f -> Maybe (Overlap f)
simplifyOverlap Index f a
idx overlap :: Overlap f
overlap@Overlap{overlap_eqn :: forall f. Overlap f -> Equation f
overlap_eqn = Term f
lhs :=: Term f
rhs, Int
Term f
Depth
overlap_pos :: Int
overlap_inner :: Term f
overlap_top :: Term f
overlap_depth :: Depth
overlap_pos :: forall f. Overlap f -> Int
overlap_inner :: forall f. Overlap f -> Term f
overlap_top :: forall f. Overlap f -> Term f
overlap_depth :: forall f. Overlap f -> Depth
..}
  | Term f
lhs Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
rhs   = Maybe (Overlap f)
forall a. Maybe a
Nothing
  | Term f
lhs' Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
rhs' = Maybe (Overlap f)
forall a. Maybe a
Nothing
  | Bool
otherwise = Overlap f -> Maybe (Overlap f)
forall a. a -> Maybe a
Just Overlap f
overlap{overlap_eqn :: Equation f
overlap_eqn = Term f
lhs' Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
rhs'}
  where
    lhs' :: Term f
lhs' = Index f a -> Term f -> Term f
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify Index f a
idx Term f
lhs
    rhs' :: Term f
rhs' = Index f a -> Term f -> Term f
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify Index f a
idx Term f
rhs

-- Put these in separate functions to avoid code blowup
buildReplacePositionSub :: TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
buildReplacePositionSub :: TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
buildReplacePositionSub !TriangleSubst f
sub !Int
n !TermList f
inner' !TermList f
outer =
  Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (TriangleSubst f -> Int -> TermList f -> TermList f -> Builder f
forall sub f.
(Substitution sub, SubstFun sub ~ f) =>
sub -> Int -> TermList f -> TermList f -> Builder f
replacePositionSub TriangleSubst f
sub Int
n TermList f
inner' TermList f
outer)

termSubst :: TriangleSubst f -> Term f -> Term f
termSubst :: TriangleSubst f -> Term f -> Term f
termSubst TriangleSubst f
sub Term f
t = Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (TriangleSubst f
-> Term (SubstFun (TriangleSubst f))
-> Builder (SubstFun (TriangleSubst f))
forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst TriangleSubst f
sub Term f
Term (SubstFun (TriangleSubst f))
t)

-- | The configuration for the critical pair weighting heuristic.
data Config =
  Config {
    Config -> Int
cfg_lhsweight :: !Int,
    Config -> Int
cfg_rhsweight :: !Int,
    Config -> Int
cfg_funweight :: !Int,
    Config -> Int
cfg_varweight :: !Int,
    Config -> Int
cfg_depthweight :: !Int,
    Config -> Int
cfg_dupcost :: !Int,
    Config -> Int
cfg_dupfactor :: !Int }

-- | The default heuristic configuration.
defaultConfig :: Config
defaultConfig :: Config
defaultConfig =
  Config :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Config
Config {
    cfg_lhsweight :: Int
cfg_lhsweight = Int
4,
    cfg_rhsweight :: Int
cfg_rhsweight = Int
1,
    cfg_funweight :: Int
cfg_funweight = Int
7,
    cfg_varweight :: Int
cfg_varweight = Int
6,
    cfg_depthweight :: Int
cfg_depthweight = Int
16,
    cfg_dupcost :: Int
cfg_dupcost = Int
7,
    cfg_dupfactor :: Int
cfg_dupfactor = Int
0 }

-- | Compute a score for a critical pair.

-- We compute:
--   cfg_lhsweight * size l + cfg_rhsweight * size r
-- where l is the biggest term and r is the smallest,
-- and variables have weight 1 and functions have weight cfg_funweight.
{-# INLINEABLE score #-}
score :: Function f => Config -> Overlap f -> Int
score :: Config -> Overlap f -> Int
score Config{Int
cfg_dupfactor :: Int
cfg_dupcost :: Int
cfg_depthweight :: Int
cfg_varweight :: Int
cfg_funweight :: Int
cfg_rhsweight :: Int
cfg_lhsweight :: Int
cfg_dupfactor :: Config -> Int
cfg_dupcost :: Config -> Int
cfg_depthweight :: Config -> Int
cfg_varweight :: Config -> Int
cfg_funweight :: Config -> Int
cfg_rhsweight :: Config -> Int
cfg_lhsweight :: Config -> Int
..} Overlap{Int
Term f
Equation f
Depth
overlap_eqn :: Equation f
overlap_pos :: Int
overlap_inner :: Term f
overlap_top :: Term f
overlap_depth :: Depth
overlap_eqn :: forall f. Overlap f -> Equation f
overlap_pos :: forall f. Overlap f -> Int
overlap_inner :: forall f. Overlap f -> Term f
overlap_top :: forall f. Overlap f -> Term f
overlap_depth :: forall f. Overlap f -> Depth
..} =
  Depth -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Depth
overlap_depth Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
cfg_depthweight Int -> Int -> Int
forall a. Num a => a -> a -> a
+
  (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
cfg_rhsweight Int -> Int -> Int
forall a. Num a => a -> a -> a
+
  Int -> Int -> Int
intMax Int
m Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* (Int
cfg_lhsweight Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
cfg_rhsweight)
  where
    Term f
l :=: Term f
r = Equation f
overlap_eqn
    m :: Int
m = Int -> TermList f -> Int
size' Int
0 (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
l)
    n :: Int
n = Int -> TermList f -> Int
size' Int
0 (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
r)

    size' :: Int -> TermList f -> Int
size' !Int
n TermList f
Empty = Int
n
    size' Int
n (Cons Term f
t TermList f
ts)
      | Term f -> Int
forall f. Term f -> Int
len Term f
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1, Term f
t Term f -> TermList f -> Bool
forall f. Term f -> TermList f -> Bool
`isSubtermOfList` TermList f
ts =
        Int -> TermList f -> Int
size' (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
cfg_dupcostInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
cfg_dupfactorInt -> Int -> Int
forall a. Num a => a -> a -> a
*Term f -> Int
forall f. Term f -> Int
len Term f
t) TermList f
ts
    size' Int
n TermList f
ts
      | Cons (App Fun f
f ws :: TermList f
ws@(Cons Term f
a (Cons Term f
b TermList f
us))) TermList f
vs <- TermList f
ts,
        Bool -> Bool
not (Term f -> Bool
forall f. Term f -> Bool
isVar Term f
a),
        Bool -> Bool
not (Term f -> Bool
forall f. Term f -> Bool
isVar Term f
b),
        f -> Bool
forall f. EqualsBonus f => f -> Bool
hasEqualsBonus (Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value Fun f
f),
        Just Subst f
sub <- Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
unify Term f
a Term f
b =
        Int -> TermList f -> Int
size' (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
cfg_funweight) TermList f
ws Int -> Int -> Int
forall a. Ord a => a -> a -> a
`min`
        Int -> TermList f -> Int
size' (Int -> TermList f -> Int
size' (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Subst f -> TermList f -> TermList f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub TermList f
us)) (Subst f -> TermList f -> TermList f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub TermList f
vs)
    size' Int
n (Cons (Var Var
_) TermList f
ts) =
      Int -> TermList f -> Int
size' (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
cfg_varweight) TermList f
ts
    size' Int
n ConsSym{hd :: forall f. TermList f -> Term f
hd = App{}, rest :: forall f. TermList f -> TermList f
rest = TermList f
ts} =
      Int -> TermList f -> Int
size' (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
cfg_funweight) TermList f
ts

----------------------------------------------------------------------
-- * Higher-level handling of critical pairs.
----------------------------------------------------------------------

-- | A critical pair together with information about how it was derived
data CriticalPair f =
  CriticalPair {
    -- | The critical pair itself.
    CriticalPair f -> Equation f
cp_eqn   :: {-# UNPACK #-} !(Equation f),
    -- | The depth of the critical pair.
    CriticalPair f -> Depth
cp_depth :: {-# UNPACK #-} !Depth,
    CriticalPair f -> Max
cp_max :: !Max,
    -- | The critical term, if there is one.
    -- (Axioms do not have a critical term.)
    CriticalPair f -> Maybe (Term f)
cp_top   :: !(Maybe (Term f)),
    -- | A derivation of the critical pair from the axioms.
    CriticalPair f -> Derivation f
cp_proof :: !(Derivation f) }

instance Symbolic (CriticalPair f) where
  type ConstantOf (CriticalPair f) = f
  termsDL :: CriticalPair f -> DList (TermListOf (CriticalPair f))
termsDL CriticalPair{Maybe (Term f)
Equation f
Derivation f
Depth
Max
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_max :: Max
cp_depth :: Depth
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_max :: forall f. CriticalPair f -> Max
cp_depth :: forall f. CriticalPair f -> Depth
cp_eqn :: forall f. CriticalPair f -> Equation f
..} =
    Equation f -> DList (TermListOf (Equation f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Equation f
cp_eqn DList (TermList f) -> DList (TermList f) -> DList (TermList f)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (Term f) -> DList (TermListOf (Maybe (Term f)))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Maybe (Term f)
cp_top DList (TermList f) -> DList (TermList f) -> DList (TermList f)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Derivation f -> DList (TermListOf (Derivation f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Derivation f
cp_proof
  subst_ :: (Var -> BuilderOf (CriticalPair f))
-> CriticalPair f -> CriticalPair f
subst_ Var -> BuilderOf (CriticalPair f)
sub CriticalPair{Maybe (Term f)
Equation f
Derivation f
Depth
Max
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_max :: Max
cp_depth :: Depth
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_max :: forall f. CriticalPair f -> Max
cp_depth :: forall f. CriticalPair f -> Depth
cp_eqn :: forall f. CriticalPair f -> Equation f
..} =
    CriticalPair :: forall f.
Equation f
-> Depth -> Max -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
      cp_eqn :: Equation f
cp_eqn = (Var -> BuilderOf (Equation f)) -> Equation f -> Equation f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Equation f)
Var -> BuilderOf (CriticalPair f)
sub Equation f
cp_eqn,
      cp_depth :: Depth
cp_depth = Depth
cp_depth,
      cp_max :: Max
cp_max = Max
cp_max,
      cp_top :: Maybe (Term f)
cp_top = (Var -> BuilderOf (Maybe (Term f)))
-> Maybe (Term f) -> Maybe (Term f)
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Maybe (Term f))
Var -> BuilderOf (CriticalPair f)
sub Maybe (Term f)
cp_top,
      cp_proof :: Derivation f
cp_proof = (Var -> BuilderOf (Derivation f)) -> Derivation f -> Derivation f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Derivation f)
Var -> BuilderOf (CriticalPair f)
sub Derivation f
cp_proof }

instance (Labelled f, PrettyTerm f) => Pretty (CriticalPair f) where
  pPrint :: CriticalPair f -> Doc
pPrint CriticalPair{Maybe (Term f)
Equation f
Derivation f
Depth
Max
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_max :: Max
cp_depth :: Depth
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_max :: forall f. CriticalPair f -> Max
cp_depth :: forall f. CriticalPair f -> Depth
cp_eqn :: forall f. CriticalPair f -> Equation f
..} =
    [Doc] -> Doc
vcat [
      Equation f -> Doc
forall a. Pretty a => a -> Doc
pPrint Equation f
cp_eqn,
      Int -> Doc -> Doc
nest Int
2 (String -> Doc
text String
"top:" Doc -> Doc -> Doc
<+> Maybe (Term f) -> Doc
forall a. Pretty a => a -> Doc
pPrint Maybe (Term f)
cp_top) ]

-- | Split a critical pair so that it can be turned into rules.
--
-- The resulting critical pairs have the property that no variable appears on
-- the right that is not on the left.

-- See the comment below.
split :: Function f => CriticalPair f -> [CriticalPair f]
split :: CriticalPair f -> [CriticalPair f]
split CriticalPair{cp_eqn :: forall f. CriticalPair f -> Equation f
cp_eqn = Term f
l :=: Term f
r, 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_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_max :: forall f. CriticalPair f -> Max
cp_depth :: forall f. CriticalPair f -> Depth
..}
  | Term f
l Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
r = []
  | Bool
otherwise =
    -- If we have something which is almost a rule, except that some
    -- variables appear only on the right-hand side, e.g.:
    --   f x y -> g x z
    -- then we replace it with the following two rules:
    --   f x y -> g x ?
    --   g x z -> g x ?
    -- where the second rule is weakly oriented and ? is the minimal
    -- constant.
    --
    -- If we have an unoriented equation with a similar problem, e.g.:
    --   f x y = g x z
    -- then we replace it with potentially three rules:
    --   f x ? = g x ?
    --   f x y -> f x ?
    --   g x z -> g x ?

    -- The main rule l -> r' or r -> l' or l' = r'
    [ CriticalPair :: forall f.
Equation f
-> Depth -> Max -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
        cp_eqn :: Equation f
cp_eqn   = Term f
l Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
r',
        cp_depth :: Depth
cp_depth = Depth
cp_depth,
        cp_max :: Max
cp_max   = Max
cp_max,
        cp_top :: Maybe (Term f)
cp_top   = [Var] -> Maybe (Term f) -> Maybe (Term f)
forall a. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
l) Maybe (Term f)
cp_top,
        cp_proof :: Derivation f
cp_proof = [Var] -> Derivation f -> Derivation f
forall a. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
l) Derivation f
cp_proof }
    | Maybe Ordering
ord Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT ] [CriticalPair f] -> [CriticalPair f] -> [CriticalPair f]
forall a. [a] -> [a] -> [a]
++
    [ CriticalPair :: forall f.
Equation f
-> Depth -> Max -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
        cp_eqn :: Equation f
cp_eqn   = Term f
r Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
l',
        cp_depth :: Depth
cp_depth = Depth
cp_depth,
        cp_max :: Max
cp_max   = Max
cp_max,
        cp_top :: Maybe (Term f)
cp_top   = [Var] -> Maybe (Term f) -> Maybe (Term f)
forall a. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
r) Maybe (Term f)
cp_top,
        cp_proof :: Derivation f
cp_proof = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Proof.symm ([Var] -> Derivation f -> Derivation f
forall a. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
r) Derivation f
cp_proof) }
    | Maybe Ordering
ord Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT ] [CriticalPair f] -> [CriticalPair f] -> [CriticalPair f]
forall a. [a] -> [a] -> [a]
++
    [ CriticalPair :: forall f.
Equation f
-> Depth -> Max -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
        cp_eqn :: Equation f
cp_eqn   = Term f
l' Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
r',
        cp_depth :: Depth
cp_depth = Depth
cp_depth,
        cp_max :: Max
cp_max   = Max
cp_max,
        cp_top :: Maybe (Term f)
cp_top   = [Var] -> Maybe (Term f) -> Maybe (Term f)
forall a. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
l) (Maybe (Term f) -> Maybe (Term f))
-> Maybe (Term f) -> Maybe (Term f)
forall a b. (a -> b) -> a -> b
$ [Var] -> Maybe (Term f) -> Maybe (Term f)
forall a. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
r) Maybe (Term f)
cp_top,
        cp_proof :: Derivation f
cp_proof = [Var] -> Derivation f -> Derivation f
forall a. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
l) (Derivation f -> Derivation f) -> Derivation f -> Derivation f
forall a b. (a -> b) -> a -> b
$ [Var] -> Derivation f -> Derivation f
forall a. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
r) Derivation f
cp_proof }
    | Maybe Ordering
ord Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Ordering
forall a. Maybe a
Nothing ] [CriticalPair f] -> [CriticalPair f] -> [CriticalPair f]
forall a. [a] -> [a] -> [a]
++

    -- Weak rules l -> l' or r -> r'
    [ CriticalPair :: forall f.
Equation f
-> Depth -> Max -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
        cp_eqn :: Equation f
cp_eqn   = Term f
l Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
l',
        cp_depth :: Depth
cp_depth = Depth
cp_depth Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ Depth
1,
        cp_max :: Max
cp_max   = Max
cp_max,
        cp_top :: Maybe (Term f)
cp_top   = Maybe (Term f)
forall a. Maybe a
Nothing,
        cp_proof :: Derivation f
cp_proof = Derivation f
cp_proof Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Proof.symm ([Var] -> Derivation f -> Derivation f
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase [Var]
ls Derivation f
cp_proof) }
    | Bool -> Bool
not ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
ls), Maybe Ordering
ord Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
GT ] [CriticalPair f] -> [CriticalPair f] -> [CriticalPair f]
forall a. [a] -> [a] -> [a]
++
    [ CriticalPair :: forall f.
Equation f
-> Depth -> Max -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
        cp_eqn :: Equation f
cp_eqn   = Term f
r Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
r',
        cp_depth :: Depth
cp_depth = Depth
cp_depth Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ Depth
1,
        cp_max :: Max
cp_max   = Max
cp_max,
        cp_top :: Maybe (Term f)
cp_top   = Maybe (Term f)
forall a. Maybe a
Nothing,
        cp_proof :: Derivation f
cp_proof = Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Proof.symm Derivation f
cp_proof Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` [Var] -> Derivation f -> Derivation f
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase [Var]
rs Derivation f
cp_proof }
    | Bool -> Bool
not ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
rs), Maybe Ordering
ord Maybe Ordering -> Maybe Ordering -> Bool
forall a. Eq a => a -> a -> Bool
/= Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT ]
    where
      ord :: Maybe Ordering
ord = Term f -> Term f -> Maybe Ordering
forall f. Ordered f => Term f -> Term f -> Maybe Ordering
orientTerms Term f
l' Term f
r'
      l' :: Term f
l' = [Var] -> Term f -> Term f
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase [Var]
ls Term f
l
      r' :: Term f
r' = [Var] -> Term f -> Term f
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase [Var]
rs Term f
r
      ls :: [Var]
ls = [Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
l) [Var] -> [Var] -> [Var]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
r)
      rs :: [Var]
rs = [Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
r) [Var] -> [Var] -> [Var]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
l)

      eraseExcept :: [Var] -> a -> a
eraseExcept [Var]
vs a
t =
        [Var] -> a -> a
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase ([Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (a -> [Var]
forall a. Symbolic a => a -> [Var]
vars a
t) [Var] -> [Var] -> [Var]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort [Var]
vs) a
t

-- | Make a critical pair from two rules and an overlap.
{-# INLINEABLE makeCriticalPair #-}
makeCriticalPair ::
  forall f a. (Has a (Rule f), Has a Id, Has a Max, Function f) =>
  a -> a -> Overlap f -> CriticalPair f
makeCriticalPair :: a -> a -> Overlap f -> CriticalPair f
makeCriticalPair a
r1 a
r2 overlap :: Overlap f
overlap@Overlap{Int
Term f
Equation f
Depth
overlap_eqn :: Equation f
overlap_pos :: Int
overlap_inner :: Term f
overlap_top :: Term f
overlap_depth :: Depth
overlap_eqn :: forall f. Overlap f -> Equation f
overlap_pos :: forall f. Overlap f -> Int
overlap_inner :: forall f. Overlap f -> Term f
overlap_top :: forall f. Overlap f -> Term f
overlap_depth :: forall f. Overlap f -> Depth
..} =
  Equation f
-> Depth -> Max -> Maybe (Term f) -> Derivation f -> CriticalPair f
forall f.
Equation f
-> Depth -> Max -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair Equation f
overlap_eqn
    Depth
overlap_depth
    (IntSet -> Max
Max (Max -> IntSet
unMax (a -> Max
forall a b. Has a b => a -> b
the a
r1) IntSet -> IntSet -> IntSet
`IntSet.union` Max -> IntSet
unMax (a -> Max
forall a b. Has a b => a -> b
the a
r2)))
    (Term f -> Maybe (Term f)
forall a. a -> Maybe a
Just Term f
overlap_top)
    (a -> a -> Overlap f -> Derivation f
forall a f.
(Has a (Rule f), Has a Id) =>
a -> a -> Overlap f -> Derivation f
overlapProof a
r1 a
r2 Overlap f
overlap)

-- | Return a proof for a critical pair.
{-# INLINEABLE overlapProof #-}
overlapProof ::
  forall a f.
  (Has a (Rule f), Has a Id) =>
  a -> a -> Overlap f -> Derivation f
overlapProof :: a -> a -> Overlap f -> Derivation f
overlapProof a
left a
right Overlap{Int
Term f
Equation f
Depth
overlap_eqn :: Equation f
overlap_pos :: Int
overlap_inner :: Term f
overlap_top :: Term f
overlap_depth :: Depth
overlap_eqn :: forall f. Overlap f -> Equation f
overlap_pos :: forall f. Overlap f -> Int
overlap_inner :: forall f. Overlap f -> Term f
overlap_top :: forall f. Overlap f -> Term f
overlap_depth :: forall f. Overlap f -> Depth
..} =
  Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Proof.symm (Rule f -> Derivation f
forall f. Rule f -> Derivation f
ruleDerivation (Subst f -> Rule f -> Rule f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
leftSub (a -> Rule f
forall a b. Has a b => a -> b
the a
left)))
  Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans`
  [Int] -> Term f -> Derivation f -> Derivation f
forall f. [Int] -> Term f -> Derivation f -> Derivation f
congPath [Int]
path Term f
overlap_top (Rule f -> Derivation f
forall f. Rule f -> Derivation f
ruleDerivation (Subst f -> Rule f -> Rule f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
rightSub (a -> Rule f
forall a b. Has a b => a -> b
the a
right)))
  where
    Just Subst f
leftSub = Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
match (Rule f -> Term f
forall f. Rule f -> Term f
lhs (a -> Rule f
forall a b. Has a b => a -> b
the a
left)) Term f
overlap_top
    Just Subst f
rightSub = Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
match (Rule f -> Term f
forall f. Rule f -> Term f
lhs (a -> Rule f
forall a b. Has a b => a -> b
the a
right)) Term f
overlap_inner

    path :: [Int]
path = Term f -> Int -> [Int]
forall f. Term f -> Int -> [Int]
positionToPath (Rule f -> Term f
forall f. Rule f -> Term f
lhs (a -> Rule f
forall a b. Has a b => a -> b
the a
left) :: Term f) Int
overlap_pos