-- | 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

-- | 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 = [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)

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

{-# 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 a f =
  Overlap {
    -- | The rule which applies at the root.
    Overlap a f -> a
overlap_rule1 :: !a,
    -- | The rule which applies at some subterm.
    Overlap a f -> a
overlap_rule2 :: !a,
    -- | The position in the critical term which is rewritten.
    Overlap a f -> How
overlap_how   :: {-# UNPACK #-} !How,
    -- | The top term of the critical pair
    Overlap a f -> Term f
overlap_top   :: {-# UNPACK #-} !(Term f),
    -- | The critical pair itself.
    Overlap a f -> Equation f
overlap_eqn   :: {-# UNPACK #-} !(Equation f) }
  deriving Int -> Overlap a f -> ShowS
[Overlap a f] -> ShowS
Overlap a f -> String
(Int -> Overlap a f -> ShowS)
-> (Overlap a f -> String)
-> ([Overlap a f] -> ShowS)
-> Show (Overlap a f)
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 Direction = Forwards | Backwards deriving (Direction -> Direction -> Bool
(Direction -> Direction -> Bool)
-> (Direction -> Direction -> Bool) -> Eq Direction
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, Int -> Direction
Direction -> Int
Direction -> [Direction]
Direction -> Direction
Direction -> Direction -> [Direction]
Direction -> Direction -> Direction -> [Direction]
(Direction -> Direction)
-> (Direction -> Direction)
-> (Int -> Direction)
-> (Direction -> Int)
-> (Direction -> [Direction])
-> (Direction -> Direction -> [Direction])
-> (Direction -> Direction -> [Direction])
-> (Direction -> Direction -> Direction -> [Direction])
-> Enum 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
(Int -> Direction -> ShowS)
-> (Direction -> String)
-> ([Direction] -> ShowS)
-> Show Direction
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 :: Rule f -> Direction -> Rule f
direct Rule f
rule Direction
Forwards = Rule f
rule
direct Rule f
rule Direction
Backwards = Rule f -> Rule f
forall f. Rule f -> Rule f
backwards Rule f
rule

data How =
  How {
    How -> Direction
how_dir1 :: !Direction,
    How -> Direction
how_dir2 :: !Direction,
    How -> Int
how_pos  :: {-# UNPACK #-} !Int }
  deriving Int -> How -> ShowS
[How] -> ShowS
How -> String
(Int -> How -> ShowS)
-> (How -> String) -> ([How] -> ShowS) -> Show How
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

packHow :: How -> Int
packHow :: How -> Int
packHow How{Int
Direction
how_pos :: Int
how_dir2 :: Direction
how_dir1 :: Direction
how_pos :: How -> Int
how_dir2 :: How -> Direction
how_dir1 :: How -> Direction
..} =
  Direction -> Int
forall a. Enum a => a -> Int
fromEnum Direction
how_dir1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+
  Direction -> Int
forall a. Enum a => a -> Int
fromEnum Direction
how_dir2 Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftL` Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+
  Int
how_pos Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftL` Int
2

unpackHow :: Int -> How
unpackHow :: Int -> How
unpackHow Int
n =
  How :: Direction -> Direction -> Int -> How
How {
    how_dir1 :: Direction
how_dir1 = Int -> Direction
forall a. Enum a => Int -> a
toEnum (Int
n Int -> Int -> Int
forall a. Bits a => a -> a -> a
.&. Int
1),
    how_dir2 :: Direction
how_dir2 = Int -> Direction
forall a. Enum a => Int -> a
toEnum ((Int
n Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) Int -> Int -> Int
forall a. Bits a => a -> a -> a
.&. Int
1),
    how_pos :: Int
how_pos  = Int
n Int -> Int -> Int
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
(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 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 -> [b] -> b -> [Overlap b f]
overlaps Index f a
idx [b]
rules b
r =
  ChurchList (Overlap b f) -> [Overlap b f]
forall a. ChurchList a -> [a]
ChurchList.toList (Index f a -> [b] -> b -> ChurchList (Overlap b f)
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 :: 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) <- Rule f
-> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
forall f.
Rule f
-> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
directions Rule f
r1' (b -> Positions2 f
forall a b. Has a b => a -> b
the b
r1)
  b
r2 <- [b] -> ChurchList b
forall a. [a] -> ChurchList a
ChurchList.fromList [b]
rules
  (Direction
d2, Positions f
pos2, Equation f
eq2) <- Rule f
-> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
forall f.
Rule f
-> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
directions (b -> Rule f
forall a b. Has a b => a -> b
the b
r2) (b -> Positions2 f
forall a b. Has a b => a -> b
the b
r2)
  Index f a
-> b
-> b
-> Direction
-> Direction
-> Positions f
-> Equation f
-> Equation f
-> ChurchList (Overlap b f)
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 ChurchList (Overlap b f)
-> ChurchList (Overlap b f) -> ChurchList (Overlap b f)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
    Index f a
-> b
-> b
-> Direction
-> Direction
-> Positions f
-> Equation f
-> Equation f
-> ChurchList (Overlap b f)
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' = [Rule f] -> Rule f -> Rule f
forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding ((b -> Rule f) -> [b] -> [Rule f]
forall a b. (a -> b) -> [a] -> [b]
map b -> Rule f
forall a b. Has a b => a -> b
the [b]
rules :: [Rule f]) (b -> 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 :: Rule f
-> Positions2 f -> ChurchList (Direction, Positions f, Equation f)
directions Rule f
rule (ForwardsPos Positions f
posf) =
  (Direction, Positions f, Equation f)
-> ChurchList (Direction, Positions f, Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Direction
Forwards, Positions f
posf, Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule)
directions Rule f
rule (BothPos Positions f
posf Positions f
posb) =
  (Direction, Positions f, Equation f)
-> ChurchList (Direction, Positions f, Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Direction
Forwards, Positions f
posf, Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule) ChurchList (Direction, Positions f, Equation f)
-> ChurchList (Direction, Positions f, Equation f)
-> ChurchList (Direction, Positions f, Equation f)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
  (Direction, Positions f, Equation f)
-> ChurchList (Direction, Positions f, Equation f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Direction
Backwards, Positions f
posb, Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Rule f -> Term 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 :: 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 <- Positions f -> ChurchList Int
forall f. Positions f -> ChurchList Int
positionsChurch Positions f
posns
  Maybe (Overlap b f) -> ChurchList (Overlap b f)
forall a. Maybe a -> ChurchList a
ChurchList.fromMaybe (Maybe (Overlap b f) -> ChurchList (Overlap b f))
-> Maybe (Overlap b f) -> ChurchList (Overlap b f)
forall a b. (a -> b) -> a -> b
$
    How -> b -> b -> Equation f -> Equation f -> Maybe (Overlap b f)
forall a f.
How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)
overlapAt' (Direction -> Direction -> Int -> How
How Direction
d1 Direction
d2 Int
n) b
r1 b
r2 Equation f
eq1 Equation f
eq2 Maybe (Overlap b f)
-> (Overlap b f -> Maybe (Overlap b f)) -> Maybe (Overlap b f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    Index f a -> Overlap b f -> Maybe (Overlap b f)
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 :: How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)
overlapAt how :: How
how@(How Direction
d1 Direction
d2 Int
_) a
x1 a
x2 Rule f
r1 Rule f
r2 =
  How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)
forall a f.
How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f)
overlapAt' How
how a
x1 a
x2 (Rule f -> Equation f
forall f. Rule f -> Equation f
unorient (Rule f -> Direction -> Rule f
forall f. Rule f -> Direction -> Rule f
direct Rule f
r1 Direction
d1)) (Rule f -> Equation f
forall f. Rule f -> Equation f
unorient (Rule f -> Direction -> Rule f
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' :: 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 = 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
    -- Make sure to keep in sync with overlapProof
    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
    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 a f -> Maybe (Overlap a f)
forall (m :: * -> *) a. Monad m => a -> m a
return Overlap :: forall a f. a -> a -> How -> Term f -> Equation f -> Overlap a f
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 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 b f -> Maybe (Overlap b f)
simplifyOverlap :: 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 Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
rhs   = Maybe (Overlap b 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 b f)
forall a. Maybe a
Nothing
  | Bool
otherwise = Overlap b f -> Maybe (Overlap b f)
forall a. a -> Maybe a
Just Overlap b 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 -> Depth -> Overlap a f -> Int
score :: 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
..} =
  Depth -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Depth
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 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
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
..} =
    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
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 :: forall f.
Equation f -> 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_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
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 [
      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
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 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 -> 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_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 -> 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_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 -> 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_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 -> 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_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 -> 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_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 :: (Function f, Has a (Rule f)) => Overlap a f -> CriticalPair f
makeCriticalPair :: 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
..} =
  Equation f -> Maybe (Term f) -> Derivation f -> CriticalPair f
forall f.
Equation f -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair Equation f
overlap_eqn
    (Term f -> Maybe (Term f)
forall a. a -> Maybe a
Just Term f
overlap_top)
    Derivation f
proof
  where
    left :: Rule f
left = Rule f -> Direction -> Rule f
forall f. Rule f -> Direction -> Rule f
direct (a -> Rule f
forall a b. Has a b => a -> b
the a
overlap_rule1) (How -> Direction
how_dir1 How
overlap_how)
    right :: Rule f
right = Rule f -> Direction -> Rule f
forall f. Rule f -> Direction -> Rule f
direct (a -> Rule f
forall a b. Has a b => a -> b
the a
overlap_rule2) (How -> Direction
how_dir2 How
overlap_how)

    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 Rule f
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 Rule f
right) Term f
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 Rule f
left) (How -> Int
how_pos How
overlap_how)
    inner :: Term f
inner = Int -> TermList f -> Term f
forall f. Int -> TermList f -> Term f
at (Term f -> [Int] -> Int
forall f. Term f -> [Int] -> Int
pathToPosition Term f
overlap_top [Int]
path) (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
overlap_top)

    proof :: Derivation f
proof =
      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 Rule f
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 Rule f
right))