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