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