{-# LANGUAGE ScopedTypeVariables, RankNTypes,
             FlexibleInstances, UndecidableInstances,
             MonoLocalBinds #-}

-- |
-- Module      :  Test.ChasingBottoms.SemanticOrd
-- Copyright   :  (c) Nils Anders Danielsson 2004-2022, 2024
-- License     :  See the file LICENCE.
--
-- Maintainer  :  http://www.cse.chalmers.se/~nad/
-- Stability   :  experimental
-- Portability :  non-portable (GHC-specific)
--
-- Generic semantic equality and order. The semantic order referred
-- to is that of a typical CPO for Haskell types, where e.g. @('True',
-- 'bottom') '<=!' ('True', 'False')@, but where @('True', 'True')@
-- and @('True', 'False')@ are incomparable.
--
-- The implementation is based on 'isBottom', and has the same
-- limitations. Note that non-bottom functions are not handled by any
-- of the functions described below.
--
-- One could imagine using QuickCheck for testing equality of
-- functions, but I have not managed to tweak the type system so that
-- it can be done transparently.

module Test.ChasingBottoms.SemanticOrd
  ( Tweak(..)
  , noTweak
  , SemanticEq(..)
  , SemanticOrd(..)
  ) where

import Data.Generics
import Test.ChasingBottoms.IsBottom
import Test.ChasingBottoms.IsType
import qualified Data.Maybe as Maybe
import Test.ChasingBottoms.Nat
import Test.ChasingBottoms.Approx

infix 4 <!, <=!, ==!, >=!, >!, /=!
infix 5 \/!
infixl 5 /\!

-- | The behaviour of some of the functions below can be tweaked.

data Tweak = Tweak
  { Tweak -> Maybe Nat
approxDepth :: Maybe Nat
    -- ^ If equal to @'Just' n@, an @'approxAll' n@ is performed on
    -- all arguments before doing whatever the function is supposed to
    -- be doing.
  , Tweak -> Maybe Int
timeOutLimit :: Maybe Int
    -- ^ If equal to @'Just' n@, then all computations that take more
    -- than @n@ seconds to complete are considered to be equal to
    -- 'bottom'. This functionality is implemented using
    -- 'isBottomTimeOut'.
  }
  deriving (Tweak -> Tweak -> Bool
(Tweak -> Tweak -> Bool) -> (Tweak -> Tweak -> Bool) -> Eq Tweak
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Tweak -> Tweak -> Bool
== :: Tweak -> Tweak -> Bool
$c/= :: Tweak -> Tweak -> Bool
/= :: Tweak -> Tweak -> Bool
Eq, Eq Tweak
Eq Tweak =>
(Tweak -> Tweak -> Ordering)
-> (Tweak -> Tweak -> Bool)
-> (Tweak -> Tweak -> Bool)
-> (Tweak -> Tweak -> Bool)
-> (Tweak -> Tweak -> Bool)
-> (Tweak -> Tweak -> Tweak)
-> (Tweak -> Tweak -> Tweak)
-> Ord Tweak
Tweak -> Tweak -> Bool
Tweak -> Tweak -> Ordering
Tweak -> Tweak -> Tweak
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Tweak -> Tweak -> Ordering
compare :: Tweak -> Tweak -> Ordering
$c< :: Tweak -> Tweak -> Bool
< :: Tweak -> Tweak -> Bool
$c<= :: Tweak -> Tweak -> Bool
<= :: Tweak -> Tweak -> Bool
$c> :: Tweak -> Tweak -> Bool
> :: Tweak -> Tweak -> Bool
$c>= :: Tweak -> Tweak -> Bool
>= :: Tweak -> Tweak -> Bool
$cmax :: Tweak -> Tweak -> Tweak
max :: Tweak -> Tweak -> Tweak
$cmin :: Tweak -> Tweak -> Tweak
min :: Tweak -> Tweak -> Tweak
Ord, Int -> Tweak -> ShowS
[Tweak] -> ShowS
Tweak -> String
(Int -> Tweak -> ShowS)
-> (Tweak -> String) -> ([Tweak] -> ShowS) -> Show Tweak
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Tweak -> ShowS
showsPrec :: Int -> Tweak -> ShowS
$cshow :: Tweak -> String
show :: Tweak -> String
$cshowList :: [Tweak] -> ShowS
showList :: [Tweak] -> ShowS
Show)

-- | No tweak (both fields are 'Nothing').

noTweak :: Tweak
noTweak :: Tweak
noTweak = Tweak
  { approxDepth :: Maybe Nat
approxDepth  = Maybe Nat
forall a. Maybe a
Nothing
  , timeOutLimit :: Maybe Int
timeOutLimit = Maybe Int
forall a. Maybe a
Nothing
  }

-- | 'SemanticEq' contains methods for testing whether two terms are
-- semantically equal.

-- Note that we only allow a -> a -> Bool here, not a -> b ->
-- Bool. Otherwise we would allow behaviour like the following:
--   > (bottom : bottom :: [Int]) <=!! ("tr" :: String)
--   True

class SemanticEq a where
  (==!), (/=!) :: a -> a -> Bool
  semanticEq :: Tweak -> a -> a -> Bool

  (/=!) = \a
x a
y -> Bool -> Bool
not (a
x a -> a -> Bool
forall a. SemanticEq a => a -> a -> Bool
==! a
y)
  (==!) = Tweak -> a -> a -> Bool
forall a. SemanticEq a => Tweak -> a -> a -> Bool
semanticEq Tweak
noTweak

-- | 'SemanticOrd' contains methods for testing whether two terms are
-- related according to the semantic domain ordering.

class SemanticEq a => SemanticOrd a where
  (<!), (<=!), (>=!), (>!) :: a -> a -> Bool

  semanticCompare :: Tweak -> a -> a -> Maybe Ordering
  -- ^ @'semanticCompare' tweak x y@ returns 'Nothing' if @x@ and @y@ are
  -- incomparable, and @'Just' o@ otherwise, where @o :: 'Ordering'@
  -- represents the relation between @x@ and @y@.

  (\/!) :: a -> a -> Maybe a
  (/\!) :: a -> a -> a
  semanticJoin :: Tweak -> a -> a -> Maybe a
  semanticMeet :: Tweak -> a -> a -> a
  -- ^ @x '\/!' y@ and @x '/\!' y@ compute the least upper and greatest
  -- lower bounds, respectively, of @x@ and @y@ in the semantical
  -- domain ordering. Note that the least upper bound may not always
  -- exist.
  -- This functionality was implemented just because it was
  -- possible (and to provide analogues of 'max' and 'min' in the 'Ord'
  -- class). If anyone finds any use for it, please let me know.

  (>=!) = (a -> a -> Bool) -> a -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> Bool
forall a. SemanticOrd a => a -> a -> Bool
(<=!)
  (<!)  = \a
x a
y -> a
x a -> a -> Bool
forall a. SemanticOrd a => a -> a -> Bool
<=! a
y Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. SemanticEq a => a -> a -> Bool
/=! a
y
  (>!)  = \a
x a
y -> a
x a -> a -> Bool
forall a. SemanticOrd a => a -> a -> Bool
>=! a
y Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. SemanticEq a => a -> a -> Bool
/=! a
y

  a
x <=! a
y = case Tweak -> a -> a -> Maybe Ordering
forall a. SemanticOrd a => Tweak -> a -> a -> Maybe Ordering
semanticCompare Tweak
noTweak a
x a
y of
    Just Ordering
LT -> Bool
True
    Just Ordering
EQ -> Bool
True
    Maybe Ordering
_       -> Bool
False

  (\/!) = Tweak -> a -> a -> Maybe a
forall a. SemanticOrd a => Tweak -> a -> a -> Maybe a
semanticJoin Tweak
noTweak
  (/\!) = Tweak -> a -> a -> a
forall a. SemanticOrd a => Tweak -> a -> a -> a
semanticMeet Tweak
noTweak

instance Data a => SemanticEq a where
  semanticEq :: Tweak -> a -> a -> Bool
semanticEq Tweak
tweak = Tweak -> (Tweak -> a -> a -> Bool) -> a -> a -> Bool
forall a b.
(Data a, Data b) =>
Tweak -> (Tweak -> a -> a -> b) -> a -> a -> b
liftAppr Tweak
tweak Tweak -> a -> a -> Bool
Rel'
semanticEq'

instance Data a => SemanticOrd a where
  semanticCompare :: Tweak -> a -> a -> Maybe Ordering
semanticCompare Tweak
tweak = Tweak
-> (Tweak -> a -> a -> Maybe Ordering) -> a -> a -> Maybe Ordering
forall a b.
(Data a, Data b) =>
Tweak -> (Tweak -> a -> a -> b) -> a -> a -> b
liftAppr Tweak
tweak Tweak -> a -> a -> Maybe Ordering
forall {b} {a}.
(Data b, Data a) =>
Tweak -> b -> a -> Maybe Ordering
semanticCompare'
    where
    semanticCompare' :: Tweak -> b -> a -> Maybe Ordering
semanticCompare' Tweak
tweak b
x a
y =
      case ( Tweak -> b -> a -> Bool
Rel'
semanticEq' Tweak
tweak b
x a
y
           , Tweak -> b -> a -> Bool
Rel'
semanticLE' Tweak
tweak b
x a
y
           , Tweak -> a -> b -> Bool
Rel'
semanticLE' Tweak
tweak a
y b
x ) of
        (Bool
True,  Bool
_,    Bool
_)    -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
EQ
        (Bool
_,     Bool
True, Bool
_)    -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
LT
        (Bool
_,     Bool
_,    Bool
True) -> Ordering -> Maybe Ordering
forall a. a -> Maybe a
Just Ordering
Prelude.GT
        (Bool
_,     Bool
_,    Bool
_)    -> Maybe Ordering
forall a. Maybe a
Nothing
  semanticJoin :: Tweak -> a -> a -> Maybe a
semanticJoin Tweak
tweak    = Tweak -> (Tweak -> a -> a -> Maybe a) -> a -> a -> Maybe a
forall a b.
(Data a, Data b) =>
Tweak -> (Tweak -> a -> a -> b) -> a -> a -> b
liftAppr Tweak
tweak Tweak -> a -> a -> Maybe a
forall a b. (Data a, Data b) => Tweak -> a -> b -> Maybe b
semanticJoin'
  semanticMeet :: Tweak -> a -> a -> a
semanticMeet Tweak
tweak    = Tweak -> (Tweak -> a -> a -> a) -> a -> a -> a
forall a b.
(Data a, Data b) =>
Tweak -> (Tweak -> a -> a -> b) -> a -> a -> b
liftAppr Tweak
tweak Tweak -> a -> a -> a
forall a b. (Data a, Data b) => Tweak -> a -> b -> b
semanticMeet'

liftAppr :: (Data a, Data b) => Tweak -> (Tweak -> a -> a -> b) -> a -> a -> b
liftAppr :: forall a b.
(Data a, Data b) =>
Tweak -> (Tweak -> a -> a -> b) -> a -> a -> b
liftAppr Tweak
tweak Tweak -> a -> a -> b
op a
x a
y = Tweak -> a -> a -> b
op Tweak
tweak (a -> a
appr a
x) (a -> a
appr a
y)
  where appr :: a -> a
appr = (a -> a) -> (Nat -> a -> a) -> Maybe Nat -> a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a -> a
forall a. a -> a
id Nat -> a -> a
forall a. Approx a => Nat -> a -> a
approxAll (Tweak -> Maybe Nat
approxDepth Tweak
tweak)

------------------------------------------------------------------------

type Rel' = forall a b. (Data a, Data b) => Tweak -> a -> b -> Bool
type Rel  = forall a b. (Data a, Data b) => a -> b -> Bool

semanticEq', semanticLE' :: Rel'

semanticEq' :: Rel'
semanticEq' Tweak
tweak a
a b
b = case ( Maybe Int -> a -> Bool
forall a. Maybe Int -> a -> Bool
isBottomTimeOut (Tweak -> Maybe Int
timeOutLimit Tweak
tweak) a
a
                             , Maybe Int -> b -> Bool
forall a. Maybe Int -> a -> Bool
isBottomTimeOut (Tweak -> Maybe Int
timeOutLimit Tweak
tweak) b
b ) of
  (Bool
True, Bool
True)   -> Bool
True
  (Bool
False, Bool
False) -> Rel -> Rel
allOK (Tweak -> a -> b -> Bool
Rel'
semanticEq' Tweak
tweak) a
a b
b
  (Bool, Bool)
_              -> Bool
False

semanticLE' :: Rel'
semanticLE' Tweak
tweak a
a b
b = case ( Maybe Int -> a -> Bool
forall a. Maybe Int -> a -> Bool
isBottomTimeOut (Tweak -> Maybe Int
timeOutLimit Tweak
tweak) a
a
                             , Maybe Int -> b -> Bool
forall a. Maybe Int -> a -> Bool
isBottomTimeOut (Tweak -> Maybe Int
timeOutLimit Tweak
tweak) b
b ) of
  (Bool
True, Bool
_)      -> Bool
True
  (Bool
False, Bool
False) -> Rel -> Rel
allOK (Tweak -> a -> b -> Bool
Rel'
semanticLE' Tweak
tweak) a
a b
b
  (Bool, Bool)
_              -> Bool
False

allOK :: Rel -> Rel
allOK :: Rel -> Rel
allOK Rel
op a
a b
b =
  -- It's really enough to test just a, since we restrict the types
  -- above, but why complicate things?
  if a -> Bool
forall a. Typeable a => a -> Bool
isFunction a
a Bool -> Bool -> Bool
|| b -> Bool
forall a. Typeable a => a -> Bool
isFunction b
b then
    -- cast' a `fop` cast' b
    String -> Bool
forall a. String -> a
nonBottomError
      String
"The generic versions of (==!) and friends do not accept non-bottom \
      \functions."
   else
    a
a a -> b -> Bool
Rel
=^= b
b Bool -> Bool -> Bool
&& Rel -> Rel
childrenOK a -> b -> Bool
Rel
op a
a b
b

-- Check top-level. Note that this test always fails for "function
-- constructors".
(=^=) :: Rel
a
a =^= :: Rel
=^= b
b = a -> Constr
forall a. Data a => a -> Constr
toConstr a
a Constr -> Constr -> Bool
forall a. Eq a => a -> a -> Bool
== b -> Constr
forall a. Data a => a -> Constr
toConstr b
b

-- Check children.
childrenOK :: Rel -> Rel
childrenOK :: Rel -> Rel
childrenOK Rel
op a
x b
y = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (GenericQ (GenericQ Bool) -> GenericQ (GenericQ [Bool])
forall r. GenericQ (GenericQ r) -> GenericQ (GenericQ [r])
gzipWithQ (\a
x a
y -> a -> a -> Bool
Rel
op a
x a
y) a
x b
y)

------------------------------------------------------------------------

semanticMeet' :: (Data a, Data b) => Tweak -> a -> b -> b
semanticMeet' :: forall a b. (Data a, Data b) => Tweak -> a -> b -> b
semanticMeet' Tweak
tweak a
a (b
b :: b) =
  if Maybe Int -> a -> Bool
forall a. Maybe Int -> a -> Bool
isBottomTimeOut (Tweak -> Maybe Int
timeOutLimit Tweak
tweak) a
a Bool -> Bool -> Bool
||
     Maybe Int -> b -> Bool
forall a. Maybe Int -> a -> Bool
isBottomTimeOut (Tweak -> Maybe Int
timeOutLimit Tweak
tweak) b
b then
    b
forall a. a
bottom
   else if a -> Bool
forall a. Typeable a => a -> Bool
isFunction a
a Bool -> Bool -> Bool
|| b -> Bool
forall a. Typeable a => a -> Bool
isFunction b
b then
    String -> b
forall a. String -> a
nonBottomError String
"/\\! does not handle non-bottom functions."
   else if Bool -> Bool
not (a
a a -> b -> Bool
Rel
=^= b
b) then
    b
forall a. a
bottom
   else
    GenericQ GenericT -> GenericQ GenericT
gzipWithT (\a
x a
y -> Tweak -> a -> a -> a
forall a b. (Data a, Data b) => Tweak -> a -> b -> b
semanticMeet' Tweak
tweak a
x a
y) a
a b
b

semanticJoin' :: (Data a, Data b) => Tweak -> a -> b -> Maybe b
semanticJoin' :: forall a b. (Data a, Data b) => Tweak -> a -> b -> Maybe b
semanticJoin' Tweak
tweak a
a (b
b :: b) =
  case ( Maybe Int -> a -> Bool
forall a. Maybe Int -> a -> Bool
isBottomTimeOut (Tweak -> Maybe Int
timeOutLimit Tweak
tweak) a
a
       , Maybe Int -> b -> Bool
forall a. Maybe Int -> a -> Bool
isBottomTimeOut (Tweak -> Maybe Int
timeOutLimit Tweak
tweak) b
b ) of
    (Bool
True,  Bool
True)  -> b -> Maybe b
forall a. a -> Maybe a
Just b
forall a. a
bottom
    (Bool
True,  Bool
False) -> b -> Maybe b
forall a. a -> Maybe a
Just b
b
    (Bool
False, Bool
True)  -> a -> Maybe b
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
a
    (Bool
False, Bool
False)
      | a -> Bool
forall a. Typeable a => a -> Bool
isFunction a
a Bool -> Bool -> Bool
|| b -> Bool
forall a. Typeable a => a -> Bool
isFunction b
b ->
          String -> Maybe b
forall a. String -> a
nonBottomError String
"\\/! does not handle non-bottom functions."
      | Bool -> Bool
not (a
a a -> b -> Bool
Rel
=^= b
b) -> Maybe b
forall a. Maybe a
Nothing
      | Bool
otherwise     -> GenericQ (GenericM Maybe) -> GenericQ (GenericM Maybe)
forall (m :: * -> *).
Monad m =>
GenericQ (GenericM m) -> GenericQ (GenericM m)
gzipWithM (\a
x a
y -> Tweak -> a -> a -> Maybe a
forall a b. (Data a, Data b) => Tweak -> a -> b -> Maybe b
semanticJoin' Tweak
tweak a
x a
y) a
a b
b

------------------------------------------------------------------------

-- Variant of cast.

-- cast' :: (Typeable a, Typeable b) => a -> b
-- cast' = Maybe.fromJust . cast

------------------------------------------------------------------------

-- TODO: Implement a comparison operator which also works for functions.

-- newtype EqFun = EqFun { unEqFun ::
--   forall a b . (Data a, Data b) => a -> b -> Bool }

-- class SemanticFunEq a where
--   (!==!), (!/=!) :: a -> a -> Bool

--   (!/=!) = \x y -> not (x !==! y)

-- instance Data a => SemanticFunEq a where
--  x !==! y =
--   let test :: (Arbitrary b, Show b, Data c) =>
--               (b -> c1) -> (b -> c2) -> Bool
--       test f g = testIt (forAll arbitrary $ \(x :: b) -> f x !==!! g x)
--   in let ?funTest = EqFun test
--   in x !==!! y

-- (!==!!) :: (Data a, Data b, ?funTest :: EqFun) => a -> b -> Bool
-- x !==!! y = case (isBottom x, isBottom y) of
--   (True, True)   -> True
--   (False, False) | isFunction x -> unEqFun ?funTest x y
--                  | otherwise -> x =^= y && tmapQl (&&) True (!==!!) x y
--   _              -> False

-- This one works, but it only handles functions on the top level, not
-- functions inside e.g. lists.

-- instance (Show a, Arbitrary a, SemanticFunEq b) => SemanticFunEq (a -> b) where
--   f !==! g = case (isBottom f, isBottom g) of
--     (True, True)   -> True
--     (False, False) -> testIt (forAll arbitrary $ \x -> f x !==! g x)
--     _              -> False

-- instance SemanticEq a => SemanticFunEq a where
--   a !==! b = case (isBottom a, isBottom b) of
--     (True, True)   -> True
--     (False, False) -> -- We know that we are not dealing with functions.
--                       a ==! b
--     _              -> False