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

-- |
-- Module      :  Test.ChasingBottoms.ApproxShow
-- 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)
--
-- 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
.)