{-# 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)
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
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
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
data Overlap f =
Overlap {
Overlap f -> Depth
overlap_depth :: {-# UNPACK #-} !Depth,
Overlap f -> Term f
overlap_top :: {-# UNPACK #-} !(Term f),
Overlap f -> Term f
overlap_inner :: {-# UNPACK #-} !(Term f),
Overlap f -> Int
overlap_pos :: {-# UNPACK #-} !Int,
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)
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)
{-# 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
{-# 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
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 }
{-# 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
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)
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 }
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 }
{-# 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
data CriticalPair f =
CriticalPair {
CriticalPair f -> Equation f
cp_eqn :: {-# UNPACK #-} !(Equation f),
CriticalPair f -> Depth
cp_depth :: {-# UNPACK #-} !Depth,
CriticalPair f -> Max
cp_max :: !Max,
CriticalPair f -> Maybe (Term f)
cp_top :: !(Maybe (Term 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
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 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 :: 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 =
[ 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]
++
[ 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
{-# 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)
{-# 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