{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}

-- | This module provides the 'NominalShow' type class, which is an
-- extension of 'Show' with support for renaming of bound variables.
-- We also provide generic programming so that instances of
-- 'NominalShow' can be automatically derived in most cases.
--
-- This module exposes implementation details of the Nominal library,
-- and should not normally be imported. Users of the library should
-- only import the top-level module "Nominal".

module Nominal.NominalShow where

import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics

import Nominal.Atom
import Nominal.Nominal
import Nominal.NominalSupport

-- ----------------------------------------------------------------------
-- * Display of nominal values

-- | 'NominalShow' is similar to 'Show', but with support for renaming
-- of bound variables. With the exception of function types, most
-- 'Nominal' types are also instances of 'NominalShow'.
--
-- In most cases, instances of 'NominalShow' can be automatically
-- derived. See <#DERIVING "Deriving generic instances"> for
-- information on how to do so, and
-- <#CUSTOM "Defining custom instances"> for how to write custom
-- instances.
class (NominalSupport t) => NominalShow t where
  -- | A nominal version of 'showsPrec'. This function takes as its
  -- first argument the support of /t/. This is then passed into the
  -- subterms, making printing O(/n/) instead of O(/n/²).
  -- 
  -- It is recommended to define a 'NominalShow' instance, rather than
  -- a 'Show' instance, for each nominal type, and then either
  -- automatically derive the 'Show' instance, or define it using
  -- 'nominal_showsPrec'. For example:
  --
  -- > instance Show MyType where
  -- >   showsPrec = nominal_showsPrec
  --
  -- Please note: in defining 'showsPrecSup', neither 'show'
  -- nor 'nominal_show' should be used for the recursive cases, or
  -- else the benefit of fast printing will be lost.
  showsPrecSup :: Support -> Int -> t -> ShowS

  -- | The method 'nominal_showList' is provided to allow the
  -- programmer to give a specialized way of showing lists of values,
  -- similarly to 'showList'. The principal use of this is in the
  -- 'NominalShow' instance of the 'Char' type, so that strings are
  -- shown in double quotes, rather than as character lists.
  nominal_showList :: Support -> [t] -> ShowS
  nominal_showList Support
sup [t]
ts = String -> ShowS
showString (String -> ShowS) -> String -> ShowS
forall a b. (a -> b) -> a -> b
$
    String
"["
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," [ Support -> Int -> t -> ShowS
forall t. NominalShow t => Support -> Int -> t -> ShowS
showsPrecSup Support
sup Int
0 t
t String
"" | t
t <- [t]
ts ]
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

  default showsPrecSup :: (Generic t, GNominalShow (Rep t)) => Support -> Int -> t -> ShowS
  showsPrecSup Support
sup Int
d t
x = Separator -> Support -> Int -> Rep t Any -> ShowS
forall a. Separator -> Support -> Int -> Rep t a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
Pre Support
sup Int
d (t -> Rep t Any
forall x. t -> Rep t x
forall a x. Generic a => a -> Rep a x
from t
x)

-- | Like 'show', but for nominal types.  Normally all instances of
-- 'NominalShow' are also instances of 'Show', so 'show' can usually
-- be used instead of 'nominal_show'.
nominal_show :: (NominalShow t) => t -> String
nominal_show :: forall t. NominalShow t => t -> String
nominal_show t
t = Support -> Int -> t -> ShowS
forall t. NominalShow t => Support -> Int -> t -> ShowS
showsPrecSup (t -> Support
forall t. NominalSupport t => t -> Support
support t
t) Int
0 t
t String
""

-- | This function can be used in the definition of 'Show'
-- instances for nominal types, like this:
--
-- > instance Show MyType where
-- >   showsPrec = nominal_showsPrec
nominal_showsPrec :: (NominalShow t) => Int -> t -> ShowS
nominal_showsPrec :: forall t. NominalShow t => Int -> t -> ShowS
nominal_showsPrec Int
d t
t = Support -> Int -> t -> ShowS
forall t. NominalShow t => Support -> Int -> t -> ShowS
showsPrecSup (t -> Support
forall t. NominalSupport t => t -> Support
support t
t) Int
d t
t

-- ----------------------------------------------------------------------
-- * NominalShow instances

-- $ Most of the time, instances of 'NominalShow' should be derived using
-- @deriving (Generic, NominalSupport, NominalShow)@, as in this example:
--
-- > {-# LANGUAGE DeriveGeneric #-}
-- > {-# LANGUAGE DeriveAnyClass #-}
-- >
-- > data Term = Var Atom | App Term Term | Abs (Bind Atom Term)
-- >   deriving (Generic, NominalSupport, NominalShow)
--
-- In the case of non-nominal types (typically base types such as
-- 'Double'), a 'NominalShow' instance can be defined using
-- 'basic_showsPrecSup':
--
-- > instance NominalShow MyType where
-- >   showsPrecSup = basic_showsPrecSup

-- | A helper function for defining 'NominalShow' instances
-- for non-nominal types. This requires an existing 'Show' instance.
basic_showsPrecSup :: (Show t) => Support -> Int -> t -> ShowS
basic_showsPrecSup :: forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup Support
sup Int
d t
x = Int -> t -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d t
x

-- Base cases

instance NominalShow Atom where
  showsPrecSup :: Support -> Int -> Atom -> ShowS
showsPrecSup Support
sup Int
d Atom
t = String -> ShowS
showString (Atom -> String
atom_show Atom
t)

instance NominalShow Bool where
  showsPrecSup :: Support -> Int -> Bool -> ShowS
showsPrecSup = Support -> Int -> Bool -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup

instance NominalShow Integer where
  showsPrecSup :: Support -> Int -> Integer -> ShowS
showsPrecSup = Support -> Int -> Integer -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup

instance NominalShow Int where
  showsPrecSup :: Support -> Int -> Int -> ShowS
showsPrecSup = Support -> Int -> Int -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup

instance NominalShow Char where
  showsPrecSup :: Support -> Int -> Char -> ShowS
showsPrecSup = Support -> Int -> Char -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup
  nominal_showList :: Support -> String -> ShowS
nominal_showList Support
sup String
ts = String -> ShowS
forall a. Show a => a -> ShowS
shows String
ts

instance NominalShow Double where
  showsPrecSup :: Support -> Int -> Double -> ShowS
showsPrecSup = Support -> Int -> Double -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup

instance NominalShow Float where
  showsPrecSup :: Support -> Int -> Float -> ShowS
showsPrecSup = Support -> Int -> Float -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup

instance NominalShow Ordering where
  showsPrecSup :: Support -> Int -> Ordering -> ShowS
showsPrecSup = Support -> Int -> Ordering -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup

instance (Show t) => NominalShow (Basic t) where
  showsPrecSup :: Support -> Int -> Basic t -> ShowS
showsPrecSup = Support -> Int -> Basic t -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup

instance NominalShow Literal where
  showsPrecSup :: Support -> Int -> Literal -> ShowS
showsPrecSup = Support -> Int -> Literal -> ShowS
forall t. Show t => Support -> Int -> t -> ShowS
basic_showsPrecSup

-- Generic instances

instance NominalShow ()
instance (NominalShow t, NominalShow s) => NominalShow (t,s)
instance (NominalShow t, NominalShow s, NominalShow r) => NominalShow (t,s,r)
instance (NominalShow t, NominalShow s, NominalShow r, NominalShow q) => NominalShow (t,s,r,q)
instance (NominalShow t, NominalShow s, NominalShow r, NominalShow q, NominalShow p) => NominalShow (t,s,r,q,p)
instance (NominalShow t, NominalShow s, NominalShow r, NominalShow q, NominalShow p, NominalShow o) => NominalShow (t,s,r,q,p,o)
instance (NominalShow t, NominalShow s, NominalShow r, NominalShow q, NominalShow p, NominalShow o, NominalShow n) => NominalShow (t,s,r,q,p,o,n)
instance (NominalShow a) => NominalShow (Maybe a)
instance (NominalShow a, NominalShow b) => NominalShow (Either a b)

-- Special instances

instance (NominalShow t) => NominalShow [t] where
  showsPrecSup :: Support -> Int -> [t] -> ShowS
showsPrecSup Support
sup Int
d [t]
ts = Support -> [t] -> ShowS
forall t. NominalShow t => Support -> [t] -> ShowS
nominal_showList Support
sup [t]
ts

instance (NominalShow t) => NominalShow (Defer t) where
  showsPrecSup :: Support -> Int -> Defer t -> ShowS
showsPrecSup Support
sup Int
d Defer t
t = Support -> Int -> t -> ShowS
forall t. NominalShow t => Support -> Int -> t -> ShowS
showsPrecSup Support
sup Int
d (Defer t -> t
forall t. Nominal t => Defer t -> t
force Defer t
t)

instance (Ord k, NominalShow k, NominalShow v) => NominalShow (Map k v) where
  showsPrecSup :: Support -> Int -> Map k v -> ShowS
showsPrecSup Support
sup Int
d Map k v
m =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"fromList " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Support -> Int -> [(k, v)] -> ShowS
forall t. NominalShow t => Support -> Int -> t -> ShowS
showsPrecSup Support
sup Int
11 (Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m)

instance (Ord k, NominalShow k) => NominalShow (Set k) where
  showsPrecSup :: Support -> Int -> Set k -> ShowS
showsPrecSup Support
sup Int
d Set k
s =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"fromList " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Support -> Int -> [k] -> ShowS
forall t. NominalShow t => Support -> Int -> t -> ShowS
showsPrecSup Support
sup Int
11 (Set k -> [k]
forall a. Set a -> [a]
Set.toList Set k
s)

-- ----------------------------------------------------------------------
-- * Generic programming for NominalShow

-- | This type keeps track of which separator to use for the next tuple.
data Separator = Rec | Tup | Inf String | Pre

-- | A version of the 'NominalShow' class suitable for generic
-- programming. The implementation uses ideas from
-- "Generics.Deriving.Show".
class GNominalShow f where
  gshowsPrecSup :: Separator -> Support -> Int -> f a -> ShowS
  isNullary :: f a -> Bool
  isNullary f a
x = Bool
False

instance GNominalShow V1 where
  -- Does not occur, because V1 is an empty type.
  gshowsPrecSup :: forall a. Separator -> Support -> Int -> V1 a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d V1 a
t String
s = String
forall a. HasCallStack => a
undefined 
  
instance GNominalShow U1 where
  gshowsPrecSup :: forall a. Separator -> Support -> Int -> U1 a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d U1 a
t String
s = String
s
  isNullary :: forall a. U1 a -> Bool
isNullary U1 a
x = Bool
True

instance (GNominalShow a, GNominalShow b) => GNominalShow (a :*: b) where
  gshowsPrecSup :: forall a. Separator -> Support -> Int -> (:*:) a b a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d (a a
x :*: b a
y) = 
    Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
prec a a
x
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
separator
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Separator -> Support -> Int -> b a -> ShowS
forall a. Separator -> Support -> Int -> b a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
prec b a
y
    where
      (String
separator, Int
prec) = case Separator
sep of
        Separator
Rec -> (String
", ", Int
d)
        Separator
Tup -> (String
",", Int
d)
        Inf String
s -> (String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ", Int
d)
        Separator
Pre -> (String
" ", Int
11)

instance (GNominalShow a, GNominalShow b) => GNominalShow (a :+: b) where
  gshowsPrecSup :: forall a. Separator -> Support -> Int -> (:+:) a b a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d (L1 a a
x) = Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d a a
x
  gshowsPrecSup Separator
sep Support
sup Int
d (R1 b a
x) = Separator -> Support -> Int -> b a -> ShowS
forall a. Separator -> Support -> Int -> b a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d b a
x

instance (GNominalShow a) => GNominalShow (M1 D c a) where
  gshowsPrecSup :: forall a. Separator -> Support -> Int -> M1 D c a a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d (M1 a a
x) = Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d a a
x

instance (GNominalShow a, Constructor c) => GNominalShow (M1 C c a) where
  gshowsPrecSup :: forall a. Separator -> Support -> Int -> M1 C c a a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d c :: M1 C c a a
c@(M1 a a
x) =
    case Fixity
fixity of
      Fixity
Prefix
        | a a -> Bool
forall a. a a -> Bool
forall (f :: * -> *) a. GNominalShow f => f a -> Bool
isNullary a a
x -> String -> ShowS
showString (ShowS
prefix String
name)
        | String -> Bool
isTuple String
name -> Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
Tup Support
sup Int
0 a a
x
        | M1 C c a a -> Bool
forall {k} (c :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Constructor c =>
t c f a -> Bool
forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
t c f a -> Bool
conIsRecord M1 C c a a
c -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
          String -> ShowS
showString (ShowS
prefix String
name)
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"{"
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
Rec Support
sup Int
0 a a
x
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"}"
        | Bool
otherwise -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString (ShowS
prefix String
name)
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
Pre Support
sup Int
11 a a
x
      Infix Associativity
assoc Int
prec -> Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup (String -> Separator
Inf String
name) Support
sup (Int
precInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) a a
x
    where
      name :: String
name = M1 C c a a -> String
forall {k} (c :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Constructor c =>
t c f a -> String
forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
t c f a -> String
conName M1 C c a a
c
      prefix :: ShowS
prefix n :: String
n@(Char
':':String
s) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      prefix String
n = String
n
      fixity :: Fixity
fixity = M1 C c a a -> Fixity
forall {k} (c :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Constructor c =>
t c f a -> Fixity
forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
t c f a -> Fixity
conFixity M1 C c a a
c
      isTuple :: String -> Bool
isTuple (Char
'(' : Char
',' : String
_) = Bool
True
      isTuple String
_ = Bool
False

instance (GNominalShow a, Selector c) => GNominalShow (M1 S c a) where
  gshowsPrecSup :: forall a. Separator -> Support -> Int -> M1 S c a a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d s :: M1 S c a a
s@(M1 a a
x)
    | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
name = Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d a a
x
    | Bool
otherwise =
      String -> ShowS
showString String
name
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" = "
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Separator -> Support -> Int -> a a -> ShowS
forall a. Separator -> Support -> Int -> a a -> ShowS
forall (f :: * -> *) a.
GNominalShow f =>
Separator -> Support -> Int -> f a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d a a
x
    where
      name :: String
name = M1 S c a a -> String
forall {k} (s :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Selector s =>
t s f a -> String
forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
t c f a -> String
selName M1 S c a a
s

instance (NominalShow a) => GNominalShow (K1 i a) where
  gshowsPrecSup :: forall a. Separator -> Support -> Int -> K1 i a a -> ShowS
gshowsPrecSup Separator
sep Support
sup Int
d (K1 a
x) = Support -> Int -> a -> ShowS
forall t. NominalShow t => Support -> Int -> t -> ShowS
showsPrecSup Support
sup Int
d a
x