module Test.Speculate.Reason.Order
( (|>|)
, (>|)
, (|>)
, kboBy
, dwoBy
, weight
, weightExcept
, gtExcept
)
where
import Test.Speculate.Expr
import Test.Speculate.Utils (nubMerge)
(>=\/) :: Expr -> Expr -> Bool
e1 >=\/ e2 = all (\(t,n) -> countVar t n e1 >= countVar t n e2)
(vars e1 `nubMerge` vars e2)
(|>|) :: Expr -> Expr -> Bool
e1 |>| e2 = lengthE e1 > lengthE e2
&& e1 >=\/ e2
infix 4 |>|
(>|) :: Expr -> Expr -> Bool
(>|) = kboBy weight (>)
infix 4 >|
kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
kboBy w (->-) e1 e2 = e1 >=\/ e2
&& ( w e1 > w e2
|| w e1 == w e2 && ( e1 `fn` e2
|| e1 `fg` e2
|| e1 `ff` e2
)
)
where
ef :$ (eg :$ ex) `fn` ey@(Var _ _) | ef == eg = fn (eg :$ ex) ey
ef@(Constant _ _) :$ ex@(Var _ _) `fn` ey@(Var _ _) | ex == ey = True
_ `fn` _ = False
e1 `fg` e2 =
case (unfoldApp e1, unfoldApp e2) of
(ef@(Constant _ _):(_:_),eg@(Constant _ _):(_:_)) -> ef ->- eg
_ -> False
e1 `ff` e2 =
case (unfoldApp e1, unfoldApp e2) of
(f:xs,g:ys) -> f == g
&& length xs == length ys
&& case dropEq xs ys of
(x:_,y:_) -> x >=\/ y
_ -> False
_ -> False
weight :: Expr -> Int
weight = w
where
w (e1 :$ e2) = weight e1 + weight e2
w (Var _ _) = 1
w e = case arity e of
0 -> 1
1 -> 1
_ -> 0
weightExcept :: Expr -> Expr -> Int
weightExcept f0 = w
where
w (e1 :$ e2) = w e1 + w e2
w (Var _ _) = 1
w e = case arity e of
0 -> 1
1 -> if e == f0 then 0 else 1
_ -> 0
gtExcept :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
gtExcept (>) f0 e1 e2 | e2 == f0 = False
| e1 == f0 = True
| otherwise = e1 > e2
(|>) :: Expr -> Expr -> Bool
(|>) = dwoBy (>)
infix 4 |>
dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
dwoBy (>) = (|>)
where
e1 |> e2@(Var n t) | (t,n) `elem` vars e1 && e1 /= e2 = True
e1 |> e2 = any (|>= e2) xs
|| (notVar f && notVar g && f > g && all (e1 |>) ys)
|| (notVar f && notVar g && f == g && all (e1 |>) ys
&& case dropEq xs ys of
(x:_,y:_) -> x |> y
_ -> False)
where
(f:xs) = unfoldApp e1
(g:ys) = unfoldApp e2
notVar (Var _ _) = False
notVar _ = True
e1 |>= e2 = e1 == e2
|| e1 |> e2
dropEq :: Eq a => [a] -> [a] -> ([a],[a])
dropEq (x:xs) (y:ys) | x == y = dropEq xs ys
dropEq xs ys = (xs,ys)