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

    -- |
    -- Module      :  Test.ChasingBottoms.ApproxShow
    -- Copyright   :  (c) Nils Anders Danielsson 2004-2022, 2024-2025
    -- License     :  See the file LICENCE.
    --
    -- Maintainer  :  http://www.cse.chalmers.se/~nad/
    -- Stability   :  experimental
    -- Portability :  non-portable (GHC-specific)
    --
    -- Functions for converting arbitrary (non-function, partial,
    -- possibly infinite) values into strings.

    module Test.ChasingBottoms.ApproxShow
      ( Prec
      , ApproxShow(..)
      ) where

    import Data.Generics
    import Test.ChasingBottoms.IsBottom
    import Test.ChasingBottoms.Nat
    import Test.ChasingBottoms.IsType
    import qualified Data.List as List

    -- | Precedence level.
    type Prec = Int

    class ApproxShow a where
      -- | The 'Data' instance of 'ApproxShow' makes sure that
      -- @'approxShowsPrec' n@ behaves (more or less) like the derived
      -- version of 'showsPrec', with the following differences:
      --
      --   * After @n@ levels of descent into a term the output is
      --     replaced by @\"_\"@.
      --
      --   * All detectable occurences of bottoms are replaced by @\"_|_\"@.
      --
      --   * Non-bottom functions are displayed as @\"\<function \/= _|_\>\"@.
      --
      approxShowsPrec :: Nat -> Prec -> a -> ShowS
      approxShows     :: Nat -> a -> ShowS
      approxShow      :: Nat -> a -> String

      approxShows Nat
    n a
    a = Nat -> Prec -> a -> ShowS
    forall a. ApproxShow a => Nat -> Prec -> a -> ShowS
    approxShowsPrec Nat
    n Prec
    0 a
    a
      approxShow Nat
    n a
    a  = Nat -> Prec -> a -> ShowS
    forall a. ApproxShow a => Nat -> Prec -> a -> ShowS
    approxShowsPrec Nat
    n Prec
    0 a
    a String
    ""

    instance Data a => ApproxShow a where
      approxShowsPrec :: Nat -> Prec -> a -> ShowS
    approxShowsPrec Nat
    n Prec
    p = Bool -> Nat -> Prec -> a -> ShowS
    forall a. Data a => Bool -> Nat -> Prec -> a -> ShowS
    gShowsPrec Bool
    False Nat
    n Prec
    p

    -- This is a gigantic hack (due to special treatment of lists and
    -- strings). Now I realise how I should have written it:
    --   A wrapper taking care of n == 0 and bottoms.
    --   A generic case treating ordinary data types
    --   Special cases (type specific extensions) for tuples, functions,
    --     lists and strings.
    -- I'm not sure if it's possible to have a type specific extension that
    -- works for, for instance, all list types, though. I guess that it
    -- would have to be monomorphic.
    --
    -- Anyway, I don't have time improving this right now. All tests go
    -- through, so this should be fine.

    gShowsPrec :: Data a => Bool -> Nat -> Prec -> a -> ShowS
    gShowsPrec :: forall a. Data a => Bool -> Nat -> Prec -> a -> ShowS
    gShowsPrec Bool
    insideList Nat
    n Prec
    p (a
    a :: a)
      | Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0       = String -> ShowS
    showString String
    "_"
      | a -> Bool
    forall a. a -> Bool
    isBottom a
    a   = String -> ShowS
    showString String
    "_|_"
      | a -> Bool
    forall a. Typeable a => a -> Bool
    isFunction a
    a = String -> ShowS
    showString String
    "<function /= _|_>"
      | a -> Bool
    forall a. Typeable a => a -> Bool
    isTuple a
    a    = Bool -> ShowS -> ShowS
    showParen Bool
    True (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ [ShowS] -> ShowS
    forall {b}. [b -> b] -> b -> b
    drive ([ShowS] -> ShowS) -> [ShowS] -> ShowS
    forall a b. (a -> b) -> a -> b
    $
                        ShowS -> [ShowS] -> [ShowS]
    forall a. a -> [a] -> [a]
    List.intersperse (String -> ShowS
    showString String
    ", ") ([ShowS] -> [ShowS]) -> [ShowS] -> [ShowS]
    forall a b. (a -> b) -> a -> b
    $
                         ((ShowS -> [ShowS] -> [ShowS]) -> [ShowS] -> Prec -> a -> [ShowS]
    forall {a} {r}. Data a => (ShowS -> r -> r) -> r -> Prec -> a -> r
    continueR (:) [] Prec
    minPrec a
    a)
      | a -> Bool
    forall a. Typeable a => a -> Bool
    isString a
    a Bool -> Bool -> Bool
    && a -> Bool
    forall {a}. Data a => a -> Bool
    isAtom a
    a = Bool -> ShowS -> ShowS -> ShowS
    forall {c} {a}. Bool -> (c -> c) -> (a -> c) -> a -> c
    when' (Bool -> Bool
    not Bool
    insideList) (String -> ShowS
    showString String
    "\"") (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
                                 String -> ShowS
    showString String
    "\""  -- End of string.
      | a -> Bool
    forall a. Typeable a => a -> Bool
    isString a
    a   = Bool -> ShowS -> ShowS -> ShowS
    forall {c} {a}. Bool -> (c -> c) -> (a -> c) -> a -> c
    when' (Bool -> Bool
    not Bool
    insideList) (String -> ShowS
    showString String
    "\"") (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
                        (ShowS -> ShowS -> ShowS)
    -> ShowS -> (forall d. Data d => d -> ShowS) -> a -> ShowS
    forall a r r'.
    Data a =>
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
    gmapQr ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.) ShowS
    forall a. a -> a
    id
                         ( ShowS
    forall a. a -> a
    id  -- Dummy.
                           ShowS -> (Char -> ShowS) -> d -> ShowS
    forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
    `mkQ`
                           (\Char
    c -> if Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    1 then String -> ShowS
    showString String
    "_" else
                                  if Char -> Bool
    forall a. a -> Bool
    isBottom Char
    c then String -> ShowS
    showString String
    "_|_"
                                  else Char -> ShowS
    showChar Char
    c)
                           (d -> ShowS) -> (String -> ShowS) -> d -> ShowS
    forall a b r.
    (Typeable a, Typeable b) =>
    (a -> r) -> (b -> r) -> a -> r
    `extQ`
                           (\(String
    a :: String) -> if Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    1 then ShowS
    forall a. a -> a
    id else
                             if String -> Bool
    forall a. a -> Bool
    isBottom String
    a then String -> ShowS
    showString String
    "_|_"
                             else Bool -> Nat -> Prec -> String -> ShowS
    forall a. Data a => Bool -> Nat -> Prec -> a -> ShowS
    gShowsPrec Bool
    True (Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n) Prec
    minPrec String
    a
                           )
                         ) a
    a
      | a -> Bool
    forall a. Typeable a => a -> Bool
    isList a
    a Bool -> Bool -> Bool
    && a -> Bool
    forall {a}. Data a => a -> Bool
    isAtom a
    a = Bool -> ShowS -> ShowS -> ShowS
    forall {c} {a}. Bool -> (c -> c) -> (a -> c) -> a -> c
    when' (Bool -> Bool
    not Bool
    insideList) (String -> ShowS
    showString String
    "[") (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
                               String -> ShowS
    showString String
    "]"  -- End of list.
      | a -> Bool
    forall a. Typeable a => a -> Bool
    isList a
    a     = Bool -> ShowS -> ShowS -> ShowS
    forall {c} {a}. Bool -> (c -> c) -> (a -> c) -> a -> c
    when' (Bool -> Bool
    not Bool
    insideList) (String -> ShowS
    showString String
    "[") (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
                        (ShowS -> ShowS -> ShowS)
    -> ShowS -> (forall d. Data d => d -> ShowS) -> a -> ShowS
    forall a r r'.
    Data a =>
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
    gmapQr ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.) ShowS
    forall a. a -> a
    id
                         ( Bool -> Nat -> Prec -> d -> ShowS
    forall a. Data a => Bool -> Nat -> Prec -> a -> ShowS
    gShowsPrec Bool
    False (Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n) Prec
    minPrec
                          (d -> ShowS) -> (a -> ShowS) -> d -> ShowS
    forall a b r.
    (Typeable a, Typeable b) =>
    (a -> r) -> (b -> r) -> a -> r
    `extQ`
                           (\(a
    a :: a) ->
                             if Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    1 then ShowS
    forall a. a -> a
    id
                             else if a -> Bool
    forall a. a -> Bool
    isBottom a
    a then String -> ShowS
    showString String
    "_|_"
                             else (if Bool -> Bool
    not (a -> Bool
    forall {a}. Data a => a -> Bool
    isAtom a
    a) then String -> ShowS
    showString String
    ", "
                                                     else ShowS
    forall a. a -> a
    id) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                                  Bool -> Nat -> Prec -> a -> ShowS
    forall a. Data a => Bool -> Nat -> Prec -> a -> ShowS
    gShowsPrec Bool
    True (Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n) Prec
    minPrec a
    a
                           )
                         ) a
    a
      | a -> Bool
    forall {a}. Data a => a -> Bool
    isInfix a
    a    = Bool -> ShowS -> ShowS
    showParen (Bool -> Bool
    not (a -> Bool
    forall {a}. Data a => a -> Bool
    isAtom a
    a) Bool -> Bool -> Bool
    && Prec
    p Prec -> Prec -> Bool
    forall a. Ord a => a -> a -> Bool
    > Prec
    appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
                           -- We know that we have at least two args,
                           -- because otherwise we would have a function.
                       let (ShowS
    arg1:ShowS
    arg2:[ShowS]
    rest) =
                              (ShowS -> [ShowS] -> [ShowS]) -> [ShowS] -> Prec -> a -> [ShowS]
    forall {a} {r}. Data a => (ShowS -> r -> r) -> r -> Prec -> a -> r
    continueR (:) [] (Prec -> Prec
    forall a. Enum a => a -> a
    succ Prec
    appPrec) a
    a
                       in (Bool -> ShowS -> ShowS
    showParen (Bool -> Bool
    not ([ShowS] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [ShowS]
    rest)) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
                           ShowS
    arg1 ShowS -> ShowS -> ShowS
    forall {c} {a}. (String -> c) -> (a -> String) -> a -> c
    .^. a -> ShowS
    forall d. Data d => d -> ShowS
    showCon a
    a ShowS -> ShowS -> ShowS
    forall {c} {a}. (String -> c) -> (a -> String) -> a -> c
    .^. ShowS
    arg2
                          ) ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ShowS] -> ShowS
    forall {b}. [b -> b] -> b -> b
    drive [ShowS]
    rest
      | Bool
    otherwise    = Bool -> ShowS -> ShowS
    showParen (Bool -> Bool
    not (a -> Bool
    forall {a}. Data a => a -> Bool
    isAtom a
    a) Bool -> Bool -> Bool
    && Prec
    p Prec -> Prec -> Bool
    forall a. Ord a => a -> a -> Bool
    > Prec
    appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
                       a -> ShowS
    forall d. Data d => d -> ShowS
    showCon a
    a ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                       (ShowS -> ShowS -> ShowS) -> ShowS -> Prec -> a -> ShowS
    forall {a} {r}. Data a => (r -> ShowS -> r) -> r -> Prec -> a -> r
    continueL ShowS -> ShowS -> ShowS
    forall {c} {a}. (String -> c) -> (a -> String) -> a -> c
    (.^.) ShowS
    nil (Prec -> Prec
    forall a. Enum a => a -> a
    succ Prec
    appPrec) a
    a

        where
        continueL :: (r -> ShowS -> r) -> r -> Prec -> a -> r
    continueL r -> ShowS -> r
    f r
    x Prec
    p = (r -> ShowS -> r)
    -> r -> (forall d. Data d => d -> ShowS) -> a -> r
    forall a r r'.
    Data a =>
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
    gmapQl r -> ShowS -> r
    f r
    x (Bool -> Nat -> Prec -> d -> ShowS
    forall a. Data a => Bool -> Nat -> Prec -> a -> ShowS
    gShowsPrec Bool
    False (Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n) Prec
    p)
        continueR :: (ShowS -> r -> r) -> r -> Prec -> a -> r
    continueR ShowS -> r -> r
    f r
    x Prec
    p = (ShowS -> r -> r)
    -> r -> (forall d. Data d => d -> ShowS) -> a -> r
    forall a r r'.
    Data a =>
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
    gmapQr ShowS -> r -> r
    f r
    x (Bool -> Nat -> Prec -> d -> ShowS
    forall a. Data a => Bool -> Nat -> Prec -> a -> ShowS
    gShowsPrec Bool
    False (Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n) Prec
    p)

    drive :: [b -> b] -> b -> b
    drive          = ((b -> b) -> (b -> b) -> b -> b) -> (b -> b) -> [b -> b] -> b -> b
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (b -> b) -> (b -> b) -> b -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.) b -> b
    forall a. a -> a
    id
    nil :: ShowS
    nil            = String -> ShowS
    showString String
    ""
    String -> c
    f .^. :: (String -> c) -> (a -> String) -> a -> c
    .^. a -> String
    g        = String -> c
    f (String -> c) -> (a -> String) -> a -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> ShowS
    showChar Char
    ' ' ShowS -> (a -> String) -> a -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> String
    g
    appPrec :: Prec
    appPrec        = Prec
    10
    minPrec :: Prec
    minPrec        = Prec
    0
    -- Some infix constructors seem to have parentheses around them in
    -- their conString representations. Maybe something should be done about
    -- that. See the Q test case, and compare with ordinary lists.
    showCon :: a -> ShowS
    showCon a
    a      = String -> ShowS
    showString (String -> ShowS) -> String -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Constr -> String
    showConstr (Constr -> String) -> Constr -> String
    forall a b. (a -> b) -> a -> b
    $ a -> Constr
    forall a. Data a => a -> Constr
    toConstr a
    a
    isAtom :: a -> Bool
    isAtom a
    a       = a -> Prec
    GenericQ Prec
    glength a
    a Prec -> Prec -> Bool
    forall a. Eq a => a -> a -> Bool
    == Prec
    0
    isPrimitive :: a -> Bool
    isPrimitive a
    a  = Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ DataType -> Bool
    isAlgType (a -> DataType
    forall a. Data a => a -> DataType
    dataTypeOf a
    a)
    isInfix :: a -> Bool
    isInfix a
    a      = if a -> Bool
    forall {a}. Data a => a -> Bool
    isPrimitive a
    a then
                       Bool
    False
                      else
                       Constr -> Fixity
    constrFixity (a -> Constr
    forall a. Data a => a -> Constr
    toConstr a
    a) Fixity -> Fixity -> Bool
    forall a. Eq a => a -> a -> Bool
    == Fixity
    Infix
    wrap :: (a -> b) -> (b -> a) -> a -> b
    wrap a -> b
    s         = \b -> a
    s' -> a -> b
    s (a -> b) -> (a -> a) -> a -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> a
    s' (b -> a) -> (a -> b) -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> b
    s
    when' :: Bool -> (c -> c) -> (a -> c) -> a -> c
    when' Bool
    b c -> c
    s      = if Bool
    b then (c -> c
    s (c -> c) -> (a -> c) -> a -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) else (c -> c
    forall a. a -> a
    id (c -> c) -> (a -> c) -> a -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .)