-- | An implementation of Knuth-Bendix ordering.

{-# LANGUAGE PatternGuards, BangPatterns #-}
module Twee.KBO(lessEq, lessIn, lessEqSkolem, Sized(..), Weighted(..)) where

import Twee.Base hiding (lessEq, lessIn, lessEqSkolem)
import Twee.Equation
import Twee.Constraints hiding (lessEq, lessIn, lessEqSkolem)
import qualified Data.Map.Strict as Map
import Data.Map.Strict(Map)
import Data.Maybe
import Control.Monad
import Twee.Utils

lessEqSkolem :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool
lessEqSkolem :: Term f -> Term f -> Bool
lessEqSkolem !Term f
t !Term f
u
  | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n = Bool
True
  | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n = Bool
False
  where
    m :: Integer
m = Term f -> Integer
forall a. Sized a => a -> Integer
size Term f
t
    n :: Integer
n = Term f -> Integer
forall a. Sized a => a -> Integer
size Term f
u
lessEqSkolem (App Fun f
x TermList f
Empty) Term f
_
  | Fun f
x Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
forall f. Minimal f => Fun f
minimal = Bool
True
lessEqSkolem Term f
_ (App Fun f
x TermList f
Empty)
  | Fun f
x Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
forall f. Minimal f => Fun f
minimal = Bool
False
lessEqSkolem (Var Var
x) (Var Var
y) = Var
x Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
<= Var
y
lessEqSkolem (Var Var
_) Term f
_ = Bool
True
lessEqSkolem Term f
_ (Var Var
_) = Bool
False
lessEqSkolem (App (F Int
_ f
f) TermList f
ts) (App (F Int
_ f
g) TermList f
us) =
  case f -> f -> Ordering
forall a. Ord a => a -> a -> Ordering
compare f
f f
g of
    Ordering
LT -> Bool
True
    Ordering
GT -> Bool
False
    Ordering
EQ ->
      let loop :: TermList f -> TermList f -> Bool
loop TermList f
Empty TermList f
Empty = Bool
True
          loop (Cons Term f
t TermList f
ts) (Cons Term f
u TermList f
us)
            | Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u = TermList f -> TermList f -> Bool
loop TermList f
ts TermList f
us
            | Bool
otherwise = Term f -> Term f -> Bool
forall f.
(Function f, Sized f, Weighted f) =>
Term f -> Term f -> Bool
lessEqSkolem Term f
t Term f
u
      in TermList f -> TermList f -> Bool
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f, Sized f, Weighted f) =>
TermList f -> TermList f -> Bool
loop TermList f
ts TermList f
us

-- | Check if one term is less than another in KBO.
{-# SCC lessEq #-}
lessEq :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool
lessEq :: Term f -> Term f -> Bool
lessEq (App Fun f
f TermList f
Empty) Term f
_ | Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
forall f. Minimal f => Fun f
minimal = Bool
True
lessEq (Var Var
x) (Var Var
y) | Var
x Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
y = Bool
True
lessEq Term f
_ (Var Var
_) = Bool
False
lessEq (Var Var
x) Term f
t = Var
x Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
t
lessEq t :: Term f
t@(App Fun f
f TermList f
ts) u :: Term f
u@(App Fun f
g TermList f
us) =
  (Integer
st Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
su Bool -> Bool -> Bool
||
   (Integer
st Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
su Bool -> Bool -> Bool
&& Fun f
f Fun f -> Fun f -> Bool
forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
g) Bool -> Bool -> Bool
||
   (Integer
st Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
su Bool -> Bool -> Bool
&& Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
g Bool -> Bool -> Bool
&& TermList f -> TermList f -> Bool
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f, Sized f, Weighted f) =>
TermList f -> TermList f -> Bool
lexLess TermList f
ts TermList f
us)) Bool -> Bool -> Bool
&&
  [(Var, Integer)]
xs [(Var, Integer)] -> [(Var, Integer)] -> Bool
forall b a. (Ord b, Ord a) => [(a, b)] -> [(a, b)] -> Bool
`lessVars` [(Var, Integer)]
ys
  where
    lexLess :: TermList f -> TermList f -> Bool
lexLess TermList f
Empty TermList f
Empty = Bool
True
    lexLess (Cons Term f
t TermList f
ts) (Cons Term f
u TermList f
us)
      | Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u = TermList f -> TermList f -> Bool
lexLess TermList f
ts TermList f
us
      | Bool
otherwise =
        Term f -> Term f -> Bool
forall f.
(Function f, Sized f, Weighted f) =>
Term f -> Term f -> Bool
lessEq Term f
t Term f
u Bool -> Bool -> Bool
&&
        case Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
unify Term f
t Term f
u of
          Maybe (Subst f)
Nothing -> Bool
True
          Just Subst f
sub
            | Bool -> Bool
not ((Var -> TermList f -> Bool) -> Subst f -> Bool
forall f. (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst (\Var
_ (Cons Term f
t TermList f
Empty) -> Term f -> Bool
forall f. Minimal f => Term f -> Bool
isMinimal Term f
t) Subst f
sub) -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"weird term inequality"
            | Bool
otherwise -> TermList f -> TermList f -> Bool
lexLess (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
ts) (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)
    lexLess TermList f
_ TermList f
_ = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"incorrect function arity"
    xs :: [(Var, Integer)]
xs = Term f -> [(Var, Integer)]
forall f. (Weighted f, Labelled f) => Term f -> [(Var, Integer)]
weightedVars Term f
t
    ys :: [(Var, Integer)]
ys = Term f -> [(Var, Integer)]
forall f. (Weighted f, Labelled f) => Term f -> [(Var, Integer)]
weightedVars Term f
u
    st :: Integer
st = Term f -> Integer
forall a. Sized a => a -> Integer
size Term f
t
    su :: Integer
su = Term f -> Integer
forall a. Sized a => a -> Integer
size Term f
u

    [] lessVars :: [(a, b)] -> [(a, b)] -> Bool
`lessVars` [(a, b)]
_ = Bool
True
    ((a
x,b
k1):[(a, b)]
xs) `lessVars` ((a
y,b
k2):[(a, b)]
ys)
      | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = b
k1 b -> b -> Bool
forall a. Ord a => a -> a -> Bool
<= b
k2 Bool -> Bool -> Bool
&& [(a, b)]
xs [(a, b)] -> [(a, b)] -> Bool
`lessVars` [(a, b)]
ys
      | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
y  = ((a
x,b
k1)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
xs) [(a, b)] -> [(a, b)] -> Bool
`lessVars` [(a, b)]
ys
    [(a, b)]
_ `lessVars` [(a, b)]
_ = Bool
False

-- | Check if one term is less than another in a given model.

-- See "notes/kbo under assumptions" for how this works.

{-# SCC lessIn #-}
lessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness
lessIn :: Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
model Term f
t Term f
u =
  case Model f -> Term f -> Term f -> Maybe Strictness
forall f.
(Function f, Sized f, Weighted f) =>
Model f -> Term f -> Term f -> Maybe Strictness
sizeLessIn Model f
model Term f
t Term f
u of
    Maybe Strictness
Nothing -> Maybe Strictness
forall a. Maybe a
Nothing
    Just Strictness
Strict -> Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict
    Just Strictness
Nonstrict -> Model f -> Term f -> Term f -> Maybe Strictness
forall f.
(Function f, Sized f, Weighted f) =>
Model f -> Term f -> Term f -> Maybe Strictness
lexLessIn Model f
model Term f
t Term f
u

sizeLessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness
sizeLessIn :: Model f -> Term f -> Term f -> Maybe Strictness
sizeLessIn Model f
model Term f
t Term f
u =
  case Model f -> Map Var Integer -> Maybe Integer
forall f.
(Function f, Sized f) =>
Model f -> Map Var Integer -> Maybe Integer
minimumIn Model f
model Map Var Integer
m of
    Just Integer
l
      | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>  -Integer
k -> Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict
      | Integer
l Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -Integer
k -> Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Nonstrict
    Maybe Integer
_ -> Maybe Strictness
forall a. Maybe a
Nothing
  where
    (Integer
k, Map Var Integer
m) =
      Integer
-> Term f
-> (Integer, Map Var Integer)
-> (Integer, Map Var Integer)
forall f.
(Weighted f, Labelled f, Sized f) =>
Integer
-> Term f
-> (Integer, Map Var Integer)
-> (Integer, Map Var Integer)
add Integer
1 Term f
u (Integer
-> Term f
-> (Integer, Map Var Integer)
-> (Integer, Map Var Integer)
forall f.
(Weighted f, Labelled f, Sized f) =>
Integer
-> Term f
-> (Integer, Map Var Integer)
-> (Integer, Map Var Integer)
add (-Integer
1) Term f
t (Integer
0, Map Var Integer
forall k a. Map k a
Map.empty))

    add :: Integer
-> Term f
-> (Integer, Map Var Integer)
-> (Integer, Map Var Integer)
add Integer
a (App Fun f
f TermList f
ts) (Integer
k, Map Var Integer
m) =
      (Term f
 -> (Integer, Map Var Integer) -> (Integer, Map Var Integer))
-> (Integer, Map Var Integer)
-> [Term f]
-> (Integer, Map Var Integer)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Integer
-> Term f
-> (Integer, Map Var Integer)
-> (Integer, Map Var Integer)
add (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Fun f -> Integer
forall f. Weighted f => f -> Integer
argWeight Fun f
f)) (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Fun f -> Integer
forall a. Sized a => a -> Integer
size Fun f
f, Map Var Integer
m) (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
ts)
    add Integer
a (Var Var
x) (Integer
k, Map Var Integer
m) = (Integer
k, (Integer -> Integer -> Integer)
-> Var -> Integer -> Map Var Integer -> Map Var Integer
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Var
x Integer
a Map Var Integer
m)

minimumIn :: (Function f, Sized f) => Model f -> Map Var Integer -> Maybe Integer
minimumIn :: Model f -> Map Var Integer -> Maybe Integer
minimumIn Model f
model Map Var Integer
t =
  (Integer -> Integer -> Integer)
-> Maybe Integer -> Maybe Integer -> Maybe Integer
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
    (([Integer] -> Integer) -> Maybe [Integer] -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((Fun f, [Var], Maybe (Fun f)) -> Maybe Integer)
-> [(Fun f, [Var], Maybe (Fun f))] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Fun f, [Var], Maybe (Fun f)) -> Maybe Integer
forall a a.
(Sized a, Sized a) =>
(a, [Var], Maybe a) -> Maybe Integer
minGroup (Model f -> [(Fun f, [Var], Maybe (Fun f))]
forall f.
(Minimal f, Ord f) =>
Model f -> [(Fun f, [Var], Maybe (Fun f))]
varGroups Model f
model)))
    (([Integer] -> Integer) -> Maybe [Integer] -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((Var, Integer) -> Maybe Integer)
-> [(Var, Integer)] -> Maybe [Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var, Integer) -> Maybe Integer
forall a. (Num a, Ord a) => (Var, a) -> Maybe a
minOrphan (Map Var Integer -> [(Var, Integer)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Var Integer
t)))
  where
    minGroup :: (a, [Var], Maybe a) -> Maybe Integer
minGroup (a
lo, [Var]
xs, Maybe a
mhi)
      | (Integer -> Bool) -> [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) [Integer]
sums = Integer -> Maybe Integer
forall a. a -> Maybe a
Just ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer]
coeffs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* a -> Integer
forall a. Sized a => a -> Integer
size a
lo)
      | Bool
otherwise =
        case Maybe a
mhi of
          Maybe a
Nothing -> Maybe Integer
forall a. Maybe a
Nothing
          Just a
hi ->
            let coeff :: Integer
coeff = Integer -> Integer
forall a. Num a => a -> a
negate ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Integer]
coeffs) in
            Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$
              [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Integer]
coeffs Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* a -> Integer
forall a. Sized a => a -> Integer
size a
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+
              Integer
coeff Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (a -> Integer
forall a. Sized a => a -> Integer
size a
lo Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- a -> Integer
forall a. Sized a => a -> Integer
size a
hi)
      where
        coeffs :: [Integer]
coeffs = (Var -> Integer) -> [Var] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (\Var
x -> Integer -> Var -> Map Var Integer -> Integer
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Integer
0 Var
x Map Var Integer
t) [Var]
xs
        sums :: [Integer]
sums = (Integer -> Integer -> Integer) -> [Integer] -> [Integer]
forall a. (a -> a -> a) -> [a] -> [a]
scanr1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) [Integer]
coeffs

    minOrphan :: (Var, a) -> Maybe a
minOrphan (Var
x, a
k)
      | Model f -> Var -> Bool
forall f. (Minimal f, Ord f) => Model f -> Var -> Bool
varInModel Model f
model Var
x = a -> Maybe a
forall a. a -> Maybe a
Just a
0
      | a
k a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = Maybe a
forall a. Maybe a
Nothing
      | Bool
otherwise = a -> Maybe a
forall a. a -> Maybe a
Just a
k

lexLessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness
lexLessIn :: Model f -> Term f -> Term f -> Maybe Strictness
lexLessIn Model f
_ Term f
t Term f
u | Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Nonstrict
lexLessIn Model f
cond Term f
t Term f
u
  | Just Atom f
a <- Term f -> Maybe (Atom f)
forall f. Term f -> Maybe (Atom f)
fromTerm Term f
t,
    Just Atom f
b <- Term f -> Maybe (Atom f)
forall f. Term f -> Maybe (Atom f)
fromTerm Term f
u,
    Just Strictness
x <- Model f -> Atom f -> Atom f -> Maybe Strictness
forall f.
(Minimal f, Ordered f, Labelled f) =>
Model f -> Atom f -> Atom f -> Maybe Strictness
lessEqInModel Model f
cond Atom f
a Atom f
b = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
x
  | Just Atom f
a <- Term f -> Maybe (Atom f)
forall f. Term f -> Maybe (Atom f)
fromTerm Term f
t,
    (Maybe Strictness -> Bool) -> [Maybe Strictness] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe Strictness -> Bool
forall a. Maybe a -> Bool
isJust
      [ Model f -> Atom f -> Atom f -> Maybe Strictness
forall f.
(Minimal f, Ordered f, Labelled f) =>
Model f -> Atom f -> Atom f -> Maybe Strictness
lessEqInModel Model f
cond Atom f
a Atom f
b
      | Term f
v <- Term f -> [Term f]
forall f. Term f -> [Term f]
properSubterms Term f
u, Just Atom f
b <- [Term f -> Maybe (Atom f)
forall f. Term f -> Maybe (Atom f)
fromTerm Term f
v]] =
        Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict
lexLessIn Model f
cond (App Fun f
f TermList f
ts) (App Fun f
g TermList f
us)
  | Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
g = TermList f -> TermList f -> Maybe Strictness
loop TermList f
ts TermList f
us
  | Fun f
f Fun f -> Fun f -> Bool
forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
g = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict
  | Bool
otherwise = Maybe Strictness
forall a. Maybe a
Nothing
  where
    loop :: TermList f -> TermList f -> Maybe Strictness
loop TermList f
Empty TermList f
Empty = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Nonstrict
    loop (Cons Term f
t TermList f
ts) (Cons Term f
u TermList f
us)
      | Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u = TermList f -> TermList f -> Maybe Strictness
loop TermList f
ts TermList f
us
      | Bool
otherwise =
        case Model f -> Term f -> Term f -> Maybe Strictness
forall f.
(Function f, Sized f, Weighted f) =>
Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
cond Term f
t Term f
u of
          Maybe Strictness
Nothing -> Maybe Strictness
forall a. Maybe a
Nothing
          Just Strictness
Strict -> Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict
          Just Strictness
Nonstrict ->
            let Just Subst f
sub = Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
unify Term f
t Term f
u in
            TermList f -> TermList f -> Maybe Strictness
loop (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
ts) (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)
    loop TermList f
_ TermList f
_ = [Char] -> Maybe Strictness
forall a. HasCallStack => [Char] -> a
error [Char]
"incorrect function arity"
lexLessIn Model f
_ Term f
t Term f
_ | Term f -> Bool
forall f. Minimal f => Term f -> Bool
isMinimal Term f
t = Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Nonstrict
lexLessIn Model f
_ Term f
_ Term f
_ = Maybe Strictness
forall a. Maybe a
Nothing

class Sized a where
  -- | Compute the size.
  size  :: a -> Integer

class Weighted f where
  argWeight :: f -> Integer

instance (Weighted f, Labelled f) => Weighted (Fun f) where
  argWeight :: Fun f -> Integer
argWeight = f -> Integer
forall f. Weighted f => f -> Integer
argWeight (f -> Integer) -> (Fun f -> f) -> Fun f -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value

weightedVars :: (Weighted f, Labelled f) => Term f -> [(Var, Integer)]
weightedVars :: Term f -> [(Var, Integer)]
weightedVars Term f
t = ([Integer] -> Integer) -> [(Var, Integer)] -> [(Var, Integer)]
forall a b c. Ord a => ([b] -> c) -> [(a, b)] -> [(a, c)]
collate [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Integer -> Term f -> [(Var, Integer)]
forall f.
(Weighted f, Labelled f) =>
Integer -> Term f -> [(Var, Integer)]
loop Integer
1 Term f
t)
  where
    loop :: Integer -> Term f -> [(Var, Integer)]
loop Integer
k (Var Var
x) = [(Var
x, Integer
k)]
    loop Integer
k (App Fun f
f TermList f
ts) =
      (Term f -> [(Var, Integer)]) -> [Term f] -> [(Var, Integer)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Integer -> Term f -> [(Var, Integer)]
loop (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Fun f -> Integer
forall f. Weighted f => f -> Integer
argWeight Fun f
f)) (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
ts)

instance (Labelled f, Sized f) => Sized (Fun f) where
  size :: Fun f -> Integer
size = f -> Integer
forall a. Sized a => a -> Integer
size (f -> Integer) -> (Fun f -> f) -> Fun f -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value

instance (Labelled f, Sized f, Weighted f) => Sized (TermList f) where
  size :: TermList f -> Integer
size = Integer -> TermList f -> Integer
forall f.
(Labelled f, Sized f, Weighted f) =>
Integer -> TermList f -> Integer
aux Integer
0
    where
      aux :: Integer -> TermList f -> Integer
aux Integer
n TermList f
Empty = Integer
n
      aux Integer
n (Cons (App Fun f
f TermList f
t) TermList f
u) =
        Integer -> TermList f -> Integer
aux (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Fun f -> Integer
forall a. Sized a => a -> Integer
size Fun f
f Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Fun f -> Integer
forall f. Weighted f => f -> Integer
argWeight Fun f
f Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* TermList f -> Integer
forall a. Sized a => a -> Integer
size TermList f
t) TermList f
u
      aux Integer
n (Cons (Var Var
_) TermList f
t) = Integer -> TermList f -> Integer
aux (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) TermList f
t

instance (Labelled f, Sized f, Weighted f) => Sized (Term f) where
  size :: Term f -> Integer
size = TermList f -> Integer
forall a. Sized a => a -> Integer
size (TermList f -> Integer)
-> (Term f -> TermList f) -> Term f -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> TermList f
forall f. Term f -> TermList f
singleton

instance (Labelled f, Sized f, Weighted f) => Sized (Equation f) where
  size :: Equation f -> Integer
size (Term f
x :=: Term f
y) = Term f -> Integer
forall a. Sized a => a -> Integer
size Term f
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Term f -> Integer
forall a. Sized a => a -> Integer
size Term f
y