-- |
-- Module      : Test.Speculate.Reason.Order
-- Copyright   : (c) 2016-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part o Speculate.
--
-- Orders for term rewriting and completion.
module Test.Speculate.Reason.Order
  ( (|>|)
  , (>|)
  , (|>)
  , kboBy
  , dwoBy
  , weight
  , weightExcept
  , gtExcept
  , funny
  , serious
  )
where

import Test.Speculate.Expr
import Test.Speculate.Utils (nubMerge)

-- | Greater than or equal number of occurences of each variable
(>=\/) :: Expr -> Expr -> Bool
Expr
e1 >=\/ :: Expr -> Expr -> Bool
>=\/ Expr
e2 = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Expr
e -> Expr -> Expr -> Int
countVar Expr
e Expr
e1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Expr -> Expr -> Int
countVar Expr
e Expr
e2)
                 (Expr -> [Expr]
nubVars Expr
e1 [Expr] -> [Expr] -> [Expr]
forall a. Ord a => [a] -> [a] -> [a]
`nubMerge` Expr -> [Expr]
nubVars Expr
e2)
  where
  countVar :: Expr -> Expr -> Int
countVar Expr
e = [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> (Expr -> [Expr]) -> Expr -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e) ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
vars


-- | Strict order between expressions as defined in TRAAT p103.
--
-- > s > t iff |s| > |t| and , for all x in V, |s|_x > |t|_x
--
-- This is perhaps the simplest order that can be used with KBC.
(|>|) :: Expr -> Expr -> Bool
Expr
e1 |>| :: Expr -> Expr -> Bool
|>| Expr
e2 = Expr -> Int
size Expr
e1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Expr -> Int
size Expr
e2
         Bool -> Bool -> Bool
&& Expr
e1 Expr -> Expr -> Bool
>=\/ Expr
e2
infix 4 |>|


-- | Strict order between expressions loosely as defined in TRAAT p124 (KBO)
--
-- Reversed K @>|@ for Knuth, sorry Bendix.
(>|) :: Expr -> Expr -> Bool
>| :: Expr -> Expr -> Bool
(>|) = (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
kboBy Expr -> Int
weight Expr -> Expr -> Bool
forall a. Ord a => a -> a -> Bool
(>)
infix 4 >|

kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
kboBy Expr -> Int
w Expr -> Expr -> Bool
(->-) Expr
e1 Expr
e2 = Expr
e1 Expr -> Expr -> Bool
>=\/ Expr
e2
                   Bool -> Bool -> Bool
&& ( Expr -> Int
w Expr
e1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>  Expr -> Int
w Expr
e2
                     Bool -> Bool -> Bool
|| Expr -> Int
w Expr
e1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Int
w Expr
e2 Bool -> Bool -> Bool
&& ( Expr
e1 Expr -> Expr -> Bool
`fn` Expr
e2 -- f (f x) > x
                                       Bool -> Bool -> Bool
|| Expr
e1 Expr -> Expr -> Bool
`fg` Expr
e2 -- f x     > g y     if f > g
                                       Bool -> Bool -> Bool
|| Expr
e1 Expr -> Expr -> Bool
`ff` Expr
e2 -- f x y z > f x w v if y > w
                                        )
                      )
  where
  Expr
ef :$ (Expr
eg :$ Expr
ex) fn :: Expr -> Expr -> Bool
`fn` Expr
ey | Expr -> Bool
isVar Expr
ey Bool -> Bool -> Bool
&& Expr
ef Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
eg = Expr -> Expr -> Bool
fn (Expr
eg Expr -> Expr -> Expr
:$ Expr
ex) Expr
ey
  ef :: Expr
ef@(Value String
_ Dynamic
_) :$ Expr
ex `fn` Expr
ey | Expr -> Bool
isVar Expr
ex Bool -> Bool -> Bool
&& Expr -> Bool
isVar Expr
ey Bool -> Bool -> Bool
&& Expr
ex Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ey = Bool
True
  Expr
_ `fn` Expr
_ = Bool
False
  Expr
e1 fg :: Expr -> Expr -> Bool
`fg` Expr
e2 =
    case (Expr -> [Expr]
unfoldApp Expr
e1, Expr -> [Expr]
unfoldApp Expr
e2) of
      -- do I really need the _:_ instead of just _?
      -- do I really need to restrict to functional values?
      (Expr
ef:(Expr
_:[Expr]
_),Expr
eg:(Expr
_:[Expr]
_)) | Expr -> Bool
isConst Expr
ef Bool -> Bool -> Bool
&& Expr -> Bool
isConst Expr
eg -> Expr
ef Expr -> Expr -> Bool
->- Expr
eg
      ([Expr], [Expr])
_ -> Bool
False
  Expr
e1 ff :: Expr -> Expr -> Bool
`ff` Expr
e2 =
    case (Expr -> [Expr]
unfoldApp Expr
e1, Expr -> [Expr]
unfoldApp Expr
e2) of
      -- Not restricting to functional values.
      -- Since we are making an equality comparison,
      -- this hopefully will be strict enough not bo break KBO.
      (Expr
f:[Expr]
xs,Expr
g:[Expr]
ys) -> Expr
f Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
g
                  Bool -> Bool -> Bool
&& [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
ys
                  Bool -> Bool -> Bool
&& case [Expr] -> [Expr] -> ([Expr], [Expr])
forall a. Eq a => [a] -> [a] -> ([a], [a])
dropEq [Expr]
xs [Expr]
ys of
                       (Expr
x:[Expr]
_,Expr
y:[Expr]
_) -> Expr
x Expr -> Expr -> Bool
>=\/ Expr
y
                       ([Expr], [Expr])
_ -> Bool
False
      ([Expr], [Expr])
_           -> Bool
False

-- | Weight function for kboBy:
--
-- * Variables         weigh 1
-- * Nullary functions weigh 1  (a.k.a. constants)
-- * N-ary   functions weigh 0
-- * Unary   functions weigh 1
--
-- This is the weight when using '>|'.
weight :: Expr -> Int
weight :: Expr -> Int
weight = Expr -> Int
w
  where
  w :: Expr -> Int
w (Expr
e1 :$ Expr
e2) = Expr -> Int
weight Expr
e1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Expr -> Int
weight Expr
e2
  w Expr
e | Expr -> Bool
isVar Expr
e   = Int
1
      | Bool
otherwise = case Expr -> Int
arity Expr
e of
                    Int
0 -> Int
1
                    Int
1 -> Int
1
                    Int
_ -> Int
0

-- | Weight function for kboBy:
--
-- * Variables         weigh 1
-- * Nullary functions weigh 1  (a.k.a. constants)
-- * N-ary   functions weigh 0
-- * Unary   functions weigh 1 except for the one given as argument
weightExcept :: Expr -> Expr -> Int
weightExcept :: Expr -> Expr -> Int
weightExcept Expr
f0 = Expr -> Int
forall p. Num p => Expr -> p
w
  where
  w :: Expr -> p
w (Expr
e1 :$ Expr
e2) = Expr -> p
w Expr
e1 p -> p -> p
forall a. Num a => a -> a -> a
+ Expr -> p
w Expr
e2
  w Expr
e | Expr -> Bool
isVar Expr
e   = p
1
      | Bool
otherwise = case Expr -> Int
arity Expr
e of
                  Int
0 -> p
1
                  Int
1 -> if Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
f0 then p
0 else p
1
                  Int
_ -> p
0

-- | To be used alongside weightExcept
gtExcept :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
gtExcept :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool
gtExcept Expr -> Expr -> Bool
(>) Expr
f0 Expr
e1 Expr
e2 | Expr
e2 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
f0  = Bool
False -- nothing can be greater than f0
                      | Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
f0  = Bool
True  -- f0 is greater than everything
                      | Bool
otherwise = Expr
e1 Expr -> Expr -> Bool
> Expr
e2 -- compare normally

-- Note this default Dershowitz order can sometimes be weird:
--
-- > x - y |> x + negate y  -- as (-) > (+)
-- > negate x + y |> negate (x + negate y)  -- as (+) > negate, as I->I->I > I->I
--
-- This is not a simplification order on 'funny' 'Expr's.
(|>) :: Expr -> Expr -> Bool
|> :: Expr -> Expr -> Bool
(|>) = (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
dwoBy Expr -> Expr -> Bool
forall a. Ord a => a -> a -> Bool
(>)
infix 4 |>

-- | Dershowitz reduction order as defined in TRAAT
--
-- @|>@ a "D" for Dershowitz
--
-- This is not a simplification order on 'funny' 'Expr's.
dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
dwoBy Expr -> Expr -> Bool
(>) = Expr -> Expr -> Bool
(|>)
  where
  Expr
e1 |> :: Expr -> Expr -> Bool
|> Expr
e2 | Expr -> Bool
isVar Expr
e2 Bool -> Bool -> Bool
&& Expr
e2 Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Expr]
nubVars Expr
e1 Bool -> Bool -> Bool
&& Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2 = Bool
True
  Expr
e1 |> Expr
e2 = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr -> Expr -> Bool
|>= Expr
e2) [Expr]
xs
          Bool -> Bool -> Bool
|| (Expr -> Bool
notVar Expr
f Bool -> Bool -> Bool
&& Expr -> Bool
notVar Expr
g Bool -> Bool -> Bool
&& Expr
f Expr -> Expr -> Bool
>  Expr
g Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Expr
e1 Expr -> Expr -> Bool
|>) [Expr]
ys)
          Bool -> Bool -> Bool
|| (Expr -> Bool
notVar Expr
f Bool -> Bool -> Bool
&& Expr -> Bool
notVar Expr
g Bool -> Bool -> Bool
&& Expr
f Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
g Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Expr
e1 Expr -> Expr -> Bool
|>) [Expr]
ys
              Bool -> Bool -> Bool
&& case [Expr] -> [Expr] -> ([Expr], [Expr])
forall a. Eq a => [a] -> [a] -> ([a], [a])
dropEq [Expr]
xs [Expr]
ys of
                   (Expr
x:[Expr]
_,Expr
y:[Expr]
_) -> Expr
x Expr -> Expr -> Bool
|> Expr
y
                   ([Expr], [Expr])
_         -> Bool
False)
    where
    (Expr
f:[Expr]
xs) = Expr -> [Expr]
unfoldApp Expr
e1
    (Expr
g:[Expr]
ys) = Expr -> [Expr]
unfoldApp Expr
e2
    notVar :: Expr -> Bool
notVar = Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
isVar
    Expr
e1 |>= :: Expr -> Expr -> Bool
|>= Expr
e2 = Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2
             Bool -> Bool -> Bool
|| Expr
e1 Expr -> Expr -> Bool
|> Expr
e2

-- | Returns 'True' when an 'Expr'ession has either
--   a functional type or functional 'var'iables.
--
-- > funny xx        =  False
-- > funny one       =  False
-- > funny idE       =  True
-- > funny (ff one)  =  True
funny :: Expr -> Bool
funny :: Expr -> Bool
funny Expr
e  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TypeRep -> Bool
isFunTy (TypeRep -> Bool) -> (Expr -> TypeRep) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> TypeRep
typ) ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ Expr
eExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:Expr -> [Expr]
vars Expr
e

-- | Returns 'True' when an 'Expr'ession has
--   no functional return type and no functional 'var'iables.
--
-- > serious xx        =  True
-- > serious one       =  True
-- > serious idE       =  False
-- > serious (ff one)  =  False
serious :: Expr -> Bool
serious :: Expr -> Bool
serious  =  Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
funny


--- Misc Utilities ---

dropEq :: Eq a => [a] -> [a] -> ([a],[a])
dropEq :: [a] -> [a] -> ([a], [a])
dropEq (a
x:[a]
xs) (a
y:[a]
ys) | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [a] -> [a] -> ([a], [a])
forall a. Eq a => [a] -> [a] -> ([a], [a])
dropEq [a]
xs [a]
ys
dropEq [a]
xs [a]
ys = ([a]
xs,[a]
ys)