{-# 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, Lemma, congPath)
data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)
type PositionsOf a = Positions (ConstantOf a)
instance Show (Positions f) where
show = show . ChurchList.toList . positionsChurch
positions :: Term f -> Positions f
positions t = aux 0 Set.empty (singleton t)
where
aux !_ !_ Empty = NilP
aux n m (Cons (Var _) t) = aux (n+1) m t
aux n m (ConsSym t@App{} u)
| t `Set.member` m = aux (n+1) m u
| otherwise = ConsP n (aux (n+1) (Set.insert t m) u)
{-# INLINE positionsChurch #-}
positionsChurch :: Positions f -> ChurchList Int
positionsChurch posns =
ChurchList $ \c n ->
let
pos NilP = n
pos (ConsP x posns) = c x (pos posns)
in
pos posns
data Overlap f =
Overlap {
overlap_depth :: {-# UNPACK #-} !Depth,
overlap_top :: {-# UNPACK #-} !(Term f),
overlap_inner :: {-# UNPACK #-} !(Term f),
overlap_pos :: {-# UNPACK #-} !Int,
overlap_eqn :: {-# UNPACK #-} !(Equation f) }
deriving Show
type OverlapOf a = Overlap (ConstantOf a)
newtype Depth = Depth Int deriving (Eq, Ord, Num, Real, Enum, Integral, Show)
{-# INLINEABLE overlaps #-}
overlaps ::
(Function f, Has a (Rule f), Has a (Positions f), Has a Depth) =>
Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)]
overlaps max_depth idx rules r =
ChurchList.toList (overlapsChurch max_depth idx rules 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 max_depth idx rules r1 = do
guard (the r1 < max_depth)
r2 <- ChurchList.fromList rules
guard (the r2 < max_depth)
let !depth = 1 + max (the r1) (the r2)
do { o <- asymmetricOverlaps idx depth (the r1) r1' (the r2); return (r1, r2, o) } `mplus`
do { o <- asymmetricOverlaps idx depth (the r2) (the r2) r1'; return (r2, r1, o) }
where
!r1' = renameAvoiding (map the rules :: [Rule f]) (the 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 idx depth posns r1 r2 = do
n <- positionsChurch posns
ChurchList.fromMaybe $
overlapAt n depth r1 r2 >>=
simplifyOverlap idx
{-# INLINE overlapAt #-}
overlapAt :: Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)
overlapAt !n !depth (Rule _ !outer !outer') (Rule _ !inner !inner') = do
let t = at n (singleton outer)
sub <- unifyTri inner t
let
top = {-# SCC overlap_top #-} termSubst sub outer
innerTerm = {-# SCC overlap_inner #-} termSubst sub inner
lhs = {-# SCC overlap_eqn_1 #-} termSubst sub outer'
rhs = {-# SCC overlap_eqn_2 #-}
buildReplacePositionSub sub n (singleton inner') (singleton outer)
guard (lhs /= rhs)
return Overlap {
overlap_depth = depth,
overlap_top = top,
overlap_inner = innerTerm,
overlap_pos = n,
overlap_eqn = lhs :=: rhs }
{-# INLINE simplifyOverlap #-}
simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap f -> Maybe (Overlap f)
simplifyOverlap idx overlap@Overlap{overlap_eqn = lhs :=: rhs, ..}
| lhs == rhs' = Nothing
| lhs' == rhs' = Nothing
| otherwise = Just overlap{overlap_eqn = lhs' :=: rhs'}
where
lhs' = simplify idx lhs
rhs' = simplify idx rhs
buildReplacePositionSub :: TriangleSubst f -> Int -> TermList f -> TermList f -> Term f
buildReplacePositionSub !sub !n !inner' !outer =
build (replacePositionSub sub n inner' outer)
termSubst :: TriangleSubst f -> Term f -> Term f
termSubst sub t = build (Term.subst sub t)
data Config =
Config {
cfg_lhsweight :: !Int,
cfg_rhsweight :: !Int,
cfg_funweight :: !Int,
cfg_varweight :: !Int,
cfg_depthweight :: !Int,
cfg_dupcost :: !Int,
cfg_dupfactor :: !Int }
defaultConfig :: Config
defaultConfig =
Config {
cfg_lhsweight = 3,
cfg_rhsweight = 1,
cfg_funweight = 7,
cfg_varweight = 6,
cfg_depthweight = 16,
cfg_dupcost = 7,
cfg_dupfactor = 0 }
{-# INLINEABLE score #-}
score :: Function f => Config -> Overlap f -> Int
score Config{..} Overlap{..} =
fromIntegral overlap_depth * cfg_depthweight +
(m + n) * cfg_rhsweight +
intMax m n * (cfg_lhsweight - cfg_rhsweight)
where
l :=: r = overlap_eqn
m = size' 0 (singleton l)
n = size' 0 (singleton r)
size' !n Empty = n
size' n (Cons t ts)
| len t > 1, t `isSubtermOfList` ts =
size' (n+cfg_dupcost+cfg_dupfactor*size t) ts
size' n ts
| Cons (App f ws@(Cons a (Cons b us))) vs <- ts,
hasEqualsBonus (fun_value f),
not (isVar a),
not (isVar b),
Just sub <- unify a b =
size' (n+cfg_funweight*size f) ws `min`
size' (size' (n+1) (subst sub us)) (subst sub vs)
size' n (Cons (Var _) ts) =
size' (n+cfg_varweight) ts
size' n (ConsSym (App f _) ts) =
size' (n+cfg_funweight*size f) ts
data CriticalPair f =
CriticalPair {
cp_eqn :: {-# UNPACK #-} !(Equation f),
cp_depth :: {-# UNPACK #-} !Depth,
cp_top :: !(Maybe (Term f)),
cp_proof :: !(Derivation f) }
instance Symbolic (CriticalPair f) where
type ConstantOf (CriticalPair f) = f
termsDL CriticalPair{..} =
termsDL cp_eqn `mplus` termsDL cp_top `mplus` termsDL cp_proof
subst_ sub CriticalPair{..} =
CriticalPair {
cp_eqn = subst_ sub cp_eqn,
cp_depth = cp_depth,
cp_top = subst_ sub cp_top,
cp_proof = subst_ sub cp_proof }
instance PrettyTerm f => Pretty (CriticalPair f) where
pPrint CriticalPair{..} =
vcat [
pPrint cp_eqn,
nest 2 (text "top:" <+> pPrint cp_top) ]
split :: Function f => CriticalPair f -> [CriticalPair f]
split CriticalPair{cp_eqn = l :=: r, ..}
| l == r = []
| otherwise =
[ CriticalPair {
cp_eqn = l :=: r',
cp_depth = cp_depth,
cp_top = eraseExcept (vars l) cp_top,
cp_proof = eraseExcept (vars l) cp_proof }
| ord == Just GT ] ++
[ CriticalPair {
cp_eqn = r :=: l',
cp_depth = cp_depth,
cp_top = eraseExcept (vars r) cp_top,
cp_proof = Proof.symm (eraseExcept (vars r) cp_proof) }
| ord == Just LT ] ++
[ CriticalPair {
cp_eqn = l' :=: r',
cp_depth = cp_depth,
cp_top = eraseExcept (vars l) $ eraseExcept (vars r) cp_top,
cp_proof = eraseExcept (vars l) $ eraseExcept (vars r) cp_proof }
| ord == Nothing ] ++
[ CriticalPair {
cp_eqn = l :=: l',
cp_depth = cp_depth + 1,
cp_top = Nothing,
cp_proof = cp_proof `Proof.trans` Proof.symm (erase ls cp_proof) }
| not (null ls), ord /= Just GT ] ++
[ CriticalPair {
cp_eqn = r :=: r',
cp_depth = cp_depth + 1,
cp_top = Nothing,
cp_proof = Proof.symm cp_proof `Proof.trans` erase rs cp_proof }
| not (null rs), ord /= Just LT ]
where
ord = orientTerms l' r'
l' = erase ls l
r' = erase rs r
ls = usort (vars l) \\ usort (vars r)
rs = usort (vars r) \\ usort (vars l)
eraseExcept vs t =
erase (usort (vars t) \\ usort vs) t
{-# INLINEABLE makeCriticalPair #-}
makeCriticalPair ::
(Has a (Rule f), Has a (Lemma f), Has a Id, Function f) =>
a -> a -> Overlap f -> Maybe (CriticalPair f)
makeCriticalPair r1 r2 overlap@Overlap{..}
| lessEq overlap_top t = Nothing
| lessEq overlap_top u = Nothing
| otherwise =
Just $
CriticalPair overlap_eqn
overlap_depth
(Just overlap_top)
(overlapProof r1 r2 overlap)
where
t :=: u = overlap_eqn
{-# INLINEABLE overlapProof #-}
overlapProof ::
forall a f.
(Has a (Rule f), Has a (Lemma f), Has a Id) =>
a -> a -> Overlap f -> Derivation f
overlapProof left right Overlap{..} =
Proof.symm (reductionProof (step left leftSub))
`Proof.trans`
congPath path overlap_top (reductionProof (step right rightSub))
where
Just leftSub = match (lhs (the left)) overlap_top
Just rightSub = match (lhs (the right)) overlap_inner
path = positionToPath (lhs (the left) :: Term f) overlap_pos