{-# 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
data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)
type PositionsOf a = Positions (ConstantOf a)
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
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
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)
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
data Overlap a f =
Overlap {
forall a f. Overlap a f -> a
overlap_rule1 :: !a,
forall a f. Overlap a f -> a
overlap_rule2 :: !a,
forall a f. Overlap a f -> How
overlap_how :: {-# UNPACK #-} !How,
forall a f. Overlap a f -> Term f
overlap_top :: {-# UNPACK #-} !(Term f),
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 }
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)
{-# 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
{-# 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
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 }
{-# 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
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)
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 {
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 -> 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
data CriticalPair f =
CriticalPair {
forall f. CriticalPair f -> Equation f
cp_eqn :: {-# UNPACK #-} !(Equation f),
forall f. CriticalPair f -> Maybe (Term f)
cp_top :: !(Maybe (Term f)),
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 :: 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 =
[ 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]
++
[ 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
{-# 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))