-- | 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 hiding (singleton)
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.Bits
import Data.Serialize
import Data.Int

-- | 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)
-- | Like Positions but for an equation (one set of positions per term).
data Positions2 f = ForwardsPos !(Positions f) | BothPos !(Positions f) !(Positions f)

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

-- | Calculate the set of positions for a term.
positions :: Term f -> Positions f
positions :: forall f. Term f -> Positions f
positions Term f
t = forall {f} {f}. Int -> Set (Term f) -> TermList f -> Positions f
aux Int
0 forall a. Set a
Set.empty (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 = 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
nforall 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 forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Term f)
m = Int -> Set (Term f) -> TermList f -> Positions f
aux (Int
nforall a. Num a => a -> a -> a
+Int
1) Set (Term f)
m TermList f
u
      | Bool
otherwise = forall f. Int -> Positions f -> Positions f
ConsP Int
n (Int -> Set (Term f) -> TermList f -> Positions f
aux (Int
nforall a. Num a => a -> a -> a
+Int
1) (forall a. Ord a => a -> Set a -> Set a
Set.insert Term f
t Set (Term f)
m) TermList f
u)

-- | Calculate the set of positions for a rule.
positionsRule :: Rule f -> Positions2 f
positionsRule :: forall f. Rule f -> Positions2 f
positionsRule Rule f
rule
  | forall f. Orientation f -> Bool
oriented (forall f. Rule f -> Orientation f
orientation Rule f
rule) Bool -> Bool -> Bool
||
    forall a. Symbolic a => a -> a
canonicalise Rule f
rule forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> a
canonicalise (forall f. Rule f -> Rule f
backwards Rule f
rule) =
    forall f. Positions f -> Positions2 f
ForwardsPos (forall f. Term f -> Positions f
positions (forall f. Rule f -> Term f
lhs Rule f
rule))
  | Bool
otherwise = forall f. Positions f -> Positions f -> Positions2 f
BothPos (forall f. Term f -> Positions f
positions (forall f. Rule f -> Term f
lhs Rule f
rule)) (forall f. Term f -> Positions f
positions (forall f. Rule f -> Term f
rhs Rule f
rule))

{-# INLINE positionsChurch #-}
positionsChurch :: Positions f -> ChurchList Int
positionsChurch :: forall f. Positions f -> ChurchList Int
positionsChurch Positions f
posns =
  forall a. (forall b. (a -> b -> b) -> b -> b) -> ChurchList a
ChurchList 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 a f =
  Overlap {
    -- | The rule which applies at the root.
    forall a f. Overlap a f -> a
overlap_rule1 :: !a,
    -- | The rule which applies at some subterm.
    forall a f. Overlap a f -> a
overlap_rule2 :: !a,
    -- | The position in the critical term which is rewritten,
    -- together with the direction of the two rules.
    forall a f. Overlap a f -> How
overlap_how   :: {-# UNPACK #-} !How,
    -- | The top term of the critical pair
    forall a f. Overlap a f -> Term f
overlap_top   :: {-# UNPACK #-} !(Term f),
    -- | The critical pair itself.
    forall a f. Overlap a f -> Equation f
overlap_eqn   :: {-# UNPACK #-} !(Equation f) }
  deriving Int -> Overlap a f -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a f.
(Labelled f, Show a, Show f) =>
Int -> Overlap a f -> ShowS
forall a f. (Labelled f, Show a, Show f) => [Overlap a f] -> ShowS
forall a f. (Labelled f, Show a, Show f) => Overlap a f -> String
showList :: [Overlap a f] -> ShowS
$cshowList :: forall a f. (Labelled f, Show a, Show f) => [Overlap a f] -> ShowS
show :: Overlap a f -> String
$cshow :: forall a f. (Labelled f, Show a, Show f) => Overlap a f -> String
showsPrec :: Int -> Overlap a f -> ShowS
$cshowsPrec :: forall a f.
(Labelled f, Show a, Show f) =>
Int -> Overlap a f -> ShowS
Show

data How =
  How {
    How -> Int
how_pos  :: {-# UNPACK #-} !Int,
    How -> Direction
how_dir1 :: !Direction,
    How -> Direction
how_dir2 :: !Direction }
  deriving (How -> How -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: How -> How -> Bool
$c/= :: How -> How -> Bool
== :: How -> How -> Bool
$c== :: How -> How -> Bool
Eq, Eq How
How -> How -> Bool
How -> How -> Ordering
How -> How -> How
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 :: How -> How -> How
$cmin :: How -> How -> How
max :: How -> How -> How
$cmax :: How -> How -> How
>= :: How -> How -> Bool
$c>= :: How -> How -> Bool
> :: How -> How -> Bool
$c> :: How -> How -> Bool
<= :: How -> How -> Bool
$c<= :: How -> How -> Bool
< :: How -> How -> Bool
$c< :: How -> How -> Bool
compare :: How -> How -> Ordering
$ccompare :: How -> How -> Ordering
Ord, Int -> How -> ShowS
[How] -> ShowS
How -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [How] -> ShowS
$cshowList :: [How] -> ShowS
show :: How -> String
$cshow :: How -> String
showsPrec :: Int -> How -> ShowS
$cshowsPrec :: Int -> How -> ShowS
Show)

data Direction = Forwards | Backwards deriving (Direction -> Direction -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Direction -> Direction -> Bool
$c/= :: Direction -> Direction -> Bool
== :: Direction -> Direction -> Bool
$c== :: Direction -> Direction -> Bool
Eq, Eq Direction
Direction -> Direction -> Bool
Direction -> Direction -> Ordering
Direction -> Direction -> Direction
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 :: Direction -> Direction -> Direction
$cmin :: Direction -> Direction -> Direction
max :: Direction -> Direction -> Direction
$cmax :: Direction -> Direction -> Direction
>= :: Direction -> Direction -> Bool
$c>= :: Direction -> Direction -> Bool
> :: Direction -> Direction -> Bool
$c> :: Direction -> Direction -> Bool
<= :: Direction -> Direction -> Bool
$c<= :: Direction -> Direction -> Bool
< :: Direction -> Direction -> Bool
$c< :: Direction -> Direction -> Bool
compare :: Direction -> Direction -> Ordering
$ccompare :: Direction -> Direction -> Ordering
Ord, Int -> Direction
Direction -> Int
Direction -> [Direction]
Direction -> Direction
Direction -> Direction -> [Direction]
Direction -> Direction -> Direction -> [Direction]
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 :: Direction -> Direction -> Direction -> [Direction]
$cenumFromThenTo :: Direction -> Direction -> Direction -> [Direction]
enumFromTo :: Direction -> Direction -> [Direction]
$cenumFromTo :: Direction -> Direction -> [Direction]
enumFromThen :: Direction -> Direction -> [Direction]
$cenumFromThen :: Direction -> Direction -> [Direction]
enumFrom :: Direction -> [Direction]
$cenumFrom :: Direction -> [Direction]
fromEnum :: Direction -> Int
$cfromEnum :: Direction -> Int
toEnum :: Int -> Direction
$ctoEnum :: Int -> Direction
pred :: Direction -> Direction
$cpred :: Direction -> Direction
succ :: Direction -> Direction
$csucc :: Direction -> Direction
Enum, Int -> Direction -> ShowS
[Direction] -> ShowS
Direction -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Direction] -> ShowS
$cshowList :: [Direction] -> ShowS
show :: Direction -> String
$cshow :: Direction -> String
showsPrec :: Int -> Direction -> ShowS
$cshowsPrec :: Int -> Direction -> ShowS
Show)

direct :: Rule f -> Direction -> Rule f
direct :: forall f. Rule f -> Direction -> Rule f
direct Rule f
rule Direction
Forwards = Rule f
rule
direct Rule f
rule Direction
Backwards = forall f. Rule f -> Rule f
backwards Rule f
rule

instance Serialize How where
  put :: Putter How
put = forall t. Serialize t => Putter t
put forall b c a. (b -> c) -> (a -> b) -> a -> c
. How -> Int32
packHow
    where
      packHow :: How -> Int32
      packHow :: How -> Int32
packHow How{Int
Direction
how_dir2 :: Direction
how_dir1 :: Direction
how_pos :: Int
how_dir2 :: How -> Direction
how_dir1 :: How -> Direction
how_pos :: How -> Int
..} =
        forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$
        forall a. Enum a => a -> Int
fromEnum Direction
how_dir1 forall a. Num a => a -> a -> a
+
        forall a. Enum a => a -> Int
fromEnum Direction
how_dir2 forall a. Bits a => a -> Int -> a
`shiftL` Int
1 forall a. Num a => a -> a -> a
+
        Int
how_pos forall a. Bits a => a -> Int -> a
`shiftL` Int
2

  get :: Get How
get = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int32 -> How
unpackHow forall t. Serialize t => Get t
get
    where
      unpackHow :: Int32 -> How
      unpackHow :: Int32 -> How
unpackHow Int32
n0 =
        let n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
n0 in
        How {
          how_dir1 :: Direction
how_dir1 = forall a. Enum a => Int -> a
toEnum (Int
n forall a. Bits a => a -> a -> a
.&. Int
1),
          how_dir2 :: Direction
how_dir2 = forall a. Enum a => Int -> a
toEnum ((Int
n forall a. Bits a => a -> Int -> a
`shiftR` Int
1) forall a. Bits a => a -> a -> a
.&. Int
1),
          how_pos :: Int
how_pos  = Int
n forall a. Bits a => a -> Int -> a
`shiftR` Int
2 }

-- | Represents the depth of a critical pair.
newtype Depth = Depth Int deriving (Depth -> Depth -> Bool
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
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
Ord, Integer -> Depth
Depth -> Depth
Depth -> Depth -> 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
Depth -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Depth -> Rational
$ctoRational :: Depth -> Rational
Real, Int -> Depth
Depth -> Int
Depth -> [Depth]
Depth -> Depth
Depth -> Depth -> [Depth]
Depth -> Depth -> Depth -> [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
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
Integral, Int -> Depth -> ShowS
[Depth] -> ShowS
Depth -> String
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 b f. (Function f, Has a (Rule f), Has b (Rule f), Has b (Positions2 f)) =>
  Index f a -> [b] -> b -> [Overlap b f]
overlaps :: forall a b f.
(Function f, Has a (Rule f), Has b (Rule f),
 Has b (Positions2 f)) =>
Index f a -> [b] -> b -> [Overlap b f]
overlaps Index f a
idx [b]
rules b
r =
  forall a. ChurchList a -> [a]
ChurchList.toList (forall f a b.
(Function f, Has a (Rule f), Has b (Rule f),
 Has b (Positions2 f)) =>
Index f a -> [b] -> b -> ChurchList (Overlap b f)
overlapsChurch Index f a
idx [b]
rules b
r)

{-# INLINE overlapsChurch #-}
overlapsChurch :: forall f a b.
  (Function f, Has a (Rule f), Has b (Rule f), Has b (Positions2 f)) =>
  Index f a -> [b] -> b -> ChurchList (Overlap b f)
overlapsChurch :: forall f a b.
(Function f, Has a (Rule f), Has b (Rule f),
 Has b (Positions2 f)) =>
Index f a -> [b] -> b -> ChurchList (Overlap b f)
overlapsChurch Index f a
idx [b]
rules b
r1 = do
  (Direction
d1, Positions f
pos1, Equation f
eq1) <- forall f.
Rule f
-> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
directions Rule f
r1' (forall a b. Has a b => a -> b
the b
r1)
  b
r2 <- forall a. [a] -> ChurchList a
ChurchList.fromList [b]
rules
  (Direction
d2, Positions f
pos2, Equation f
eq2) <- forall f.
Rule f
-> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
directions (forall a b. Has a b => a -> b
the b
r2) (forall a b. Has a b => a -> b
the b
r2)
  forall f a b.
(Function f, Has a (Rule f)) =>
Index f a
-> b
-> b
-> Direction
-> Direction
-> Positions f
-> Equation f
-> Equation f
-> ChurchList (Overlap b f)
asymmetricOverlaps Index f a
idx b
r1 b
r2 Direction
d1 Direction
d2 Positions f
pos1 Equation f
eq1 Equation f
eq2 forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
    forall f a b.
(Function f, Has a (Rule f)) =>
Index f a
-> b
-> b
-> Direction
-> Direction
-> Positions f
-> Equation f
-> Equation f
-> ChurchList (Overlap b f)
asymmetricOverlaps Index f a
idx b
r2 b
r1 Direction
d2 Direction
d1 Positions f
pos2 Equation f
eq2 Equation f
eq1
  where
    !r1' :: Rule f
r1' = forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding (forall a b. (a -> b) -> [a] -> [b]
map forall a b. Has a b => a -> b
the [b]
rules :: [Rule f]) (forall a b. Has a b => a -> b
the b
r1)

{-# INLINE directions #-}
directions :: Rule f -> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
directions :: forall f.
Rule f
-> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
directions Rule f
rule (ForwardsPos Positions f
posf) =
  forall (m :: * -> *) a. Monad m => a -> m a
return (Direction
Forwards, Positions f
posf, forall f. Rule f -> Term f
lhs Rule f
rule forall f. Term f -> Term f -> Equation f
:=: forall f. Rule f -> Term f
rhs Rule f
rule)
directions Rule f
rule (BothPos Positions f
posf Positions f
posb) =
  forall (m :: * -> *) a. Monad m => a -> m a
return (Direction
Forwards, Positions f
posf, forall f. Rule f -> Term f
lhs Rule f
rule forall f. Term f -> Term f -> Equation f
:=: forall f. Rule f -> Term f
rhs Rule f
rule) forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
  forall (m :: * -> *) a. Monad m => a -> m a
return (Direction
Backwards, Positions f
posb, forall f. Rule f -> Term f
rhs Rule f
rule forall f. Term f -> Term f -> Equation f
:=: forall f. Rule f -> Term f
lhs Rule f
rule)

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

-- | Create an overlap at a particular position in a term.
-- Doesn't simplify the overlap.
{-# INLINE overlapAt #-}
overlapAt :: How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)
overlapAt :: forall a f.
How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)
overlapAt how :: How
how@(How Int
_ Direction
d1 Direction
d2) a
x1 a
x2 Rule f
r1 Rule f
r2 =
  forall a f.
How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)
overlapAt' How
how a
x1 a
x2 (forall f. Rule f -> Equation f
unorient (forall f. Rule f -> Direction -> Rule f
direct Rule f
r1 Direction
d1)) (forall f. Rule f -> Equation f
unorient (forall f. Rule f -> Direction -> Rule f
direct Rule f
r2 Direction
d2))

{-# INLINE overlapAt' #-}
overlapAt' :: How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)
overlapAt' :: forall a f.
How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)
overlapAt' how :: How
how@How{how_pos :: How -> Int
how_pos = Int
n} a
r1 a
r2 (!Term f
outer :=: (!Term f
outer')) (!Term f
inner :=: (!Term f
inner')) = do
  let t :: Term f
t = forall f. Int -> TermList f -> Term f
at Int
n (forall f. Term f -> TermList f
singleton Term f
outer)
  TriangleSubst f
sub <- forall f. Term f -> Term f -> Maybe (TriangleSubst f)
unifyTri Term f
inner Term f
t
  let
    -- Make sure to keep in sync with overlapProof
    top :: Term f
top = forall f. TriangleSubst f -> Term f -> Term f
termSubst TriangleSubst f
sub Term f
outer
    lhs :: Term f
lhs = forall f. TriangleSubst f -> Term f -> Term f
termSubst TriangleSubst f
sub Term f
outer'
    rhs :: Term f
rhs = forall f.
TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
buildReplacePositionSub TriangleSubst f
sub Int
n (forall f. Term f -> TermList f
singleton Term f
inner') (forall f. Term f -> TermList f
singleton Term f
outer)

  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term f
lhs forall a. Eq a => a -> a -> Bool
/= Term f
rhs)
  forall (m :: * -> *) a. Monad m => a -> m a
return Overlap {
    overlap_rule1 :: a
overlap_rule1 = a
r1,
    overlap_rule2 :: a
overlap_rule2 = a
r2,
    overlap_how :: How
overlap_how = How
how,
    overlap_top :: Term f
overlap_top = Term f
top,
    overlap_eqn :: Equation f
overlap_eqn = Term f
lhs 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 b f -> Maybe (Overlap b f)
simplifyOverlap :: forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap Index f a
idx overlap :: Overlap b f
overlap@Overlap{overlap_eqn :: forall a f. Overlap a f -> Equation f
overlap_eqn = Term f
lhs :=: Term f
rhs, b
Term f
How
overlap_top :: Term f
overlap_how :: How
overlap_rule2 :: b
overlap_rule1 :: b
overlap_top :: forall a f. Overlap a f -> Term f
overlap_how :: forall a f. Overlap a f -> How
overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule1 :: forall a f. Overlap a f -> a
..}
  | Term f
lhs forall a. Eq a => a -> a -> Bool
== Term f
rhs   = forall a. Maybe a
Nothing
  | Term f
lhs' forall a. Eq a => a -> a -> Bool
== Term f
rhs' = forall a. Maybe a
Nothing
  | Bool
otherwise = forall a. a -> Maybe a
Just Overlap b f
overlap{overlap_eqn :: Equation f
overlap_eqn = Term f
lhs' forall f. Term f -> Term f -> Equation f
:=: Term f
rhs'}
  where
    lhs' :: Term f
lhs' = 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' = 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 :: forall f.
TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
buildReplacePositionSub !TriangleSubst f
sub !Int
n !TermList f
inner' !TermList f
outer =
  forall a. Build a => a -> Term (BuildFun a)
build (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 :: forall f. TriangleSubst f -> Term f -> Term f
termSubst TriangleSubst f
sub Term f
t = forall a. Build a => a -> Term (BuildFun a)
build (forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst TriangleSubst f
sub Term 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 {
    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 -> Depth -> Overlap a f -> Int
score :: forall f a. Function f => Config -> Depth -> Overlap a 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
..} Depth
depth Overlap{a
Term f
Equation f
How
overlap_eqn :: Equation f
overlap_top :: Term f
overlap_how :: How
overlap_rule2 :: a
overlap_rule1 :: a
overlap_eqn :: forall a f. Overlap a f -> Equation f
overlap_top :: forall a f. Overlap a f -> Term f
overlap_how :: forall a f. Overlap a f -> How
overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule1 :: forall a f. Overlap a f -> a
..} =
  forall a b. (Integral a, Num b) => a -> b
fromIntegral Depth
depth forall a. Num a => a -> a -> a
* Int
cfg_depthweight forall a. Num a => a -> a -> a
+
  (Int
m forall a. Num a => a -> a -> a
+ Int
n) forall a. Num a => a -> a -> a
* Int
cfg_rhsweight forall a. Num a => a -> a -> a
+
  Int -> Int -> Int
intMax Int
m Int
n forall a. Num a => a -> a -> a
* (Int
cfg_lhsweight 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 (forall f. Term f -> TermList f
singleton Term f
l)
    n :: Int
n = Int -> TermList f -> Int
size' Int
0 (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)
      | forall f. Term f -> Int
len Term f
t forall a. Ord a => a -> a -> Bool
> Int
1, Term f
t forall f. Term f -> TermList f -> Bool
`isSubtermOfList` TermList f
ts =
        Int -> TermList f -> Int
size' (Int
nforall a. Num a => a -> a -> a
+Int
cfg_dupcostforall a. Num a => a -> a -> a
+Int
cfg_dupfactorforall a. Num a => a -> a -> a
*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 (forall f. Term f -> Bool
isVar Term f
a),
        Bool -> Bool
not (forall f. Term f -> Bool
isVar Term f
b),
        forall f. EqualsBonus f => f -> Bool
hasEqualsBonus (forall f. Labelled f => Fun f -> f
fun_value Fun f
f),
        Just Subst f
sub <- forall f. Term f -> Term f -> Maybe (Subst f)
unify Term f
a Term f
b =
        Int -> TermList f -> Int
size' (Int
nforall a. Num a => a -> a -> a
+Int
cfg_funweight) TermList f
ws forall a. Ord a => a -> a -> a
`min`
        Int -> TermList f -> Int
size' (Int -> TermList f -> Int
size' (Int
nforall a. Num a => a -> a -> a
+Int
1) (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub TermList f
us)) (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
nforall 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
nforall 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.
    forall f. CriticalPair f -> Equation f
cp_eqn   :: {-# UNPACK #-} !(Equation f),
    -- | The critical term, if there is one.
    -- (Axioms do not have a critical term.)
    forall f. CriticalPair f -> Maybe (Term f)
cp_top   :: !(Maybe (Term f)),
    -- | A derivation of the critical pair from the axioms.
    forall f. 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
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_eqn :: forall f. CriticalPair f -> Equation f
..} =
    forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Equation f
cp_eqn forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Maybe (Term f)
cp_top forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` 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
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_eqn :: forall f. CriticalPair f -> Equation f
..} =
    CriticalPair {
      cp_eqn :: Equation f
cp_eqn = forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (CriticalPair f)
sub Equation f
cp_eqn,
      cp_top :: Maybe (Term f)
cp_top = forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (CriticalPair f)
sub Maybe (Term f)
cp_top,
      cp_proof :: Derivation f
cp_proof = forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ 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
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_eqn :: forall f. CriticalPair f -> Equation f
..} =
    [Doc] -> Doc
vcat [
      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
<+> 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 :: forall f. Function f => 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
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)
..}
  | Term f
l 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 {
        cp_eqn :: Equation f
cp_eqn   = Term f
l forall f. Term f -> Term f -> Equation f
:=: Term f
r',
        cp_top :: Maybe (Term f)
cp_top   = forall {a}. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Term f
l) Maybe (Term f)
cp_top,
        cp_proof :: Derivation f
cp_proof = forall {a}. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Term f
l) Derivation f
cp_proof }
    | Maybe Ordering
ord forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Ordering
GT ] forall a. [a] -> [a] -> [a]
++
    [ CriticalPair {
        cp_eqn :: Equation f
cp_eqn   = Term f
r forall f. Term f -> Term f -> Equation f
:=: Term f
l',
        cp_top :: Maybe (Term f)
cp_top   = forall {a}. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Term f
r) Maybe (Term f)
cp_top,
        cp_proof :: Derivation f
cp_proof = forall f. Derivation f -> Derivation f
Proof.symm (forall {a}. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Term f
r) Derivation f
cp_proof) }
    | Maybe Ordering
ord forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Ordering
LT ] forall a. [a] -> [a] -> [a]
++
    [ CriticalPair {
        cp_eqn :: Equation f
cp_eqn   = Term f
l' forall f. Term f -> Term f -> Equation f
:=: Term f
r',
        cp_top :: Maybe (Term f)
cp_top   = forall {a}. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Term f
l) forall a b. (a -> b) -> a -> b
$ forall {a}. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Term f
r) Maybe (Term f)
cp_top,
        cp_proof :: Derivation f
cp_proof = forall {a}. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Term f
l) forall a b. (a -> b) -> a -> b
$ forall {a}. (Symbolic a, Minimal (ConstantOf a)) => [Var] -> a -> a
eraseExcept (forall a. Symbolic a => a -> [Var]
vars Term f
r) Derivation f
cp_proof }
    | Maybe Ordering
ord forall a. Eq a => a -> a -> Bool
== forall a. Maybe a
Nothing ] forall a. [a] -> [a] -> [a]
++

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

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

-- | Make a critical pair from two rules and an overlap.
{-# INLINEABLE makeCriticalPair #-}
makeCriticalPair :: (Function f, Has a (Rule f)) => Overlap a f -> CriticalPair f
makeCriticalPair :: forall f a.
(Function f, Has a (Rule f)) =>
Overlap a f -> CriticalPair f
makeCriticalPair Overlap{a
Term f
Equation f
How
overlap_eqn :: Equation f
overlap_top :: Term f
overlap_how :: How
overlap_rule2 :: a
overlap_rule1 :: a
overlap_eqn :: forall a f. Overlap a f -> Equation f
overlap_top :: forall a f. Overlap a f -> Term f
overlap_how :: forall a f. Overlap a f -> How
overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule1 :: forall a f. Overlap a f -> a
..} =
  forall f.
Equation f -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair Equation f
overlap_eqn
    (forall a. a -> Maybe a
Just Term f
overlap_top)
    Derivation f
proof
  where
    left :: Rule f
left = forall f. Rule f -> Direction -> Rule f
direct (forall a b. Has a b => a -> b
the a
overlap_rule1) (How -> Direction
how_dir1 How
overlap_how)
    right :: Rule f
right = forall f. Rule f -> Direction -> Rule f
direct (forall a b. Has a b => a -> b
the a
overlap_rule2) (How -> Direction
how_dir2 How
overlap_how)

    Just Subst f
leftSub = forall f. Term f -> Term f -> Maybe (Subst f)
match (forall f. Rule f -> Term f
lhs Rule f
left) Term f
overlap_top
    Just Subst f
rightSub = forall f. Term f -> Term f -> Maybe (Subst f)
match (forall f. Rule f -> Term f
lhs Rule f
right) Term f
inner

    path :: [Int]
path = forall f. Term f -> Int -> [Int]
positionToPath (forall f. Rule f -> Term f
lhs Rule f
left) (How -> Int
how_pos How
overlap_how)
    inner :: Term f
inner = forall f. Int -> TermList f -> Term f
at (forall f. Term f -> [Int] -> Int
pathToPosition Term f
overlap_top [Int]
path) (forall f. Term f -> TermList f
singleton Term f
overlap_top)

    proof :: Derivation f
proof =
      forall f. Derivation f -> Derivation f
Proof.symm (forall f. Rule f -> Derivation f
ruleDerivation (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
leftSub Rule f
left))
      forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans`
      forall f. [Int] -> Term f -> Derivation f -> Derivation f
congPath [Int]
path Term f
overlap_top (forall f. Rule f -> Derivation f
ruleDerivation (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
rightSub Rule f
right))