---------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Plugin.Common
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Common data-structures/utilities
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes        #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Plugin.Common where

import Control.Monad.Reader

import GHC.Plugins

import GHC.Types.Tickish
import GHC.Types.CostCentre
import GHC.Types.Unique (nonDetCmpUnique)

import Data.Maybe (mapMaybe)
import qualified Data.Map as M

import Data.IORef

import qualified Data.SBV         as S
import qualified Data.SBV.Dynamic as S

import Data.SBV.Plugin.Data

-- | Certain "very-polymorphic" things are just special
data Specials = Specials { Specials -> Var -> Maybe Val
isEquality :: Var -> Maybe Val
                         , Specials -> Var -> Maybe Val
isTuple    :: Var -> Maybe Val
                         , Specials -> Var -> Maybe Val
isList     :: Var -> Maybe Val
                         }

-- | TyCon's are no longer Ord in GHC 8.2.1; so we make a newtype
newtype TCKey = TCKey (TyCon, [TyCon])

-- | Extract the unique "key"
tcKeyToUList :: TCKey -> [Unique]
tcKeyToUList :: TCKey -> [Unique]
tcKeyToUList (TCKey (TyCon
a, [TyCon]
as)) = (TyCon -> Unique) -> [TyCon] -> [Unique]
forall a b. (a -> b) -> [a] -> [b]
map TyCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique (TyCon
aTyCon -> [TyCon] -> [TyCon]
forall a. a -> [a] -> [a]
:[TyCon]
as)

-- | Make a rudimentary Eq instance for TCKey
instance Eq TCKey where
  TCKey
k1 == :: TCKey -> TCKey -> Bool
== TCKey
k2 = TCKey -> [Unique]
tcKeyToUList TCKey
k1 [Unique] -> [Unique] -> Bool
forall a. Eq a => a -> a -> Bool
== TCKey -> [Unique]
tcKeyToUList TCKey
k2

-- | Make a rudimentary Ord instance for TCKey
instance Ord TCKey where
  TCKey
k1 compare :: TCKey -> TCKey -> Ordering
`compare` TCKey
k2 = TCKey -> [Unique]
tcKeyToUList TCKey
k1 [Unique] -> [Unique] -> Ordering
`cmp` TCKey -> [Unique]
tcKeyToUList TCKey
k2
    where []     cmp :: [Unique] -> [Unique] -> Ordering
`cmp` []     = Ordering
EQ
          []     `cmp` [Unique]
_      = Ordering
LT
          [Unique]
_      `cmp` []     = Ordering
GT
          (Unique
a:[Unique]
as) `cmp` (Unique
b:[Unique]
bs) = case Unique
a Unique -> Unique -> Ordering
`nonDetCmpUnique` Unique
b of
                                   Ordering
EQ -> [Unique]
as [Unique] -> [Unique] -> Ordering
`cmp` [Unique]
bs
                                   Ordering
r  -> Ordering
r

-- | Interpreter environment
data Env = Env { Env -> [SrcSpan]
curLoc         :: [SrcSpan]
               , Env -> DynFlags
flags          :: DynFlags
               , Env -> Int
machWordSize   :: Int
               , Env -> Maybe Int
mbListSize     :: Maybe Int
               , Env -> [Type]
uninteresting  :: [Type]
               , Env -> IORef [((Var, Type), (Bool, String, Val))]
rUninterpreted :: IORef [((Var, Type), (Bool, String, Val))]
               , Env -> IORef [String]
rUsedNames     :: IORef [String]
               , Env -> IORef [(Type, Kind)]
rUITypes       :: IORef [(Type, S.Kind)]
               , Env -> Specials
specials       :: Specials
               , Env -> Map TCKey Kind
tcMap          :: M.Map TCKey S.Kind
               , Env -> Map (Var, SKind) Val
envMap         :: M.Map (Var, SKind) Val
               , Env
-> Map Var (Val -> [(Var, SKind)] -> (SVal, [((Var, SKind), Val)]))
destMap        :: M.Map Var          (Val -> [(Var, SKind)] -> (S.SVal, [((Var, SKind), Val)]))
               , Env -> Map Var (SrcSpan, CoreExpr)
coreMap        :: M.Map Var          (SrcSpan, CoreExpr)
               , Env -> forall a. String -> [String] -> Eval a
bailOut        :: forall a. String -> [String] -> Eval a
               }


-- | The interpreter monad
type Eval a = ReaderT Env S.Symbolic a

-- | Configuration info as we run the plugin
data Config = Config { Config -> Bool
isGHCi        :: Bool
                     , Config -> [SBVAnnotation]
opts          :: [SBVAnnotation]
                     , Config -> Var -> [SBVAnnotation]
sbvAnnotation :: Var -> [SBVAnnotation]
                     , Config -> Env
cfgEnv        :: Env
                     }

-- | Given the user options, determine which solver(s) to use
pickSolvers :: [SBVOption] -> IO [S.SMTConfig]
pickSolvers :: [SBVOption] -> IO [SMTConfig]
pickSolvers [SBVOption]
slvrs
  | SBVOption
AnySolver SBVOption -> [SBVOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SBVOption]
slvrs = IO [SMTConfig]
S.getAvailableSolvers
  | Bool
True                   = case (SBVOption -> Maybe SMTConfig) -> [SBVOption] -> [SMTConfig]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (SBVOption -> [(SBVOption, SMTConfig)] -> Maybe SMTConfig
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(SBVOption, SMTConfig)]
solvers) [SBVOption]
slvrs of
                                [] -> [SMTConfig] -> IO [SMTConfig]
forall (m :: * -> *) a. Monad m => a -> m a
return [SMTConfig
S.defaultSMTCfg]
                                [SMTConfig]
xs -> [SMTConfig] -> IO [SMTConfig]
forall (m :: * -> *) a. Monad m => a -> m a
return [SMTConfig]
xs
  where solvers :: [(SBVOption, SMTConfig)]
solvers = [ (SBVOption
Z3,        SMTConfig
S.z3)
                  , (SBVOption
Yices,     SMTConfig
S.yices)
                  , (SBVOption
Boolector, SMTConfig
S.boolector)
                  , (SBVOption
CVC4,      SMTConfig
S.cvc4)
                  , (SBVOption
MathSAT,   SMTConfig
S.mathSAT)
                  , (SBVOption
ABC,       SMTConfig
S.abc)
                  ]

-- | The kinds used by the plugin
data SKind = KBase S.Kind
           | KTup  [SKind]
           | KLst  SKind
           | KFun  SKind SKind
           deriving (SKind -> SKind -> Bool
(SKind -> SKind -> Bool) -> (SKind -> SKind -> Bool) -> Eq SKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SKind -> SKind -> Bool
$c/= :: SKind -> SKind -> Bool
== :: SKind -> SKind -> Bool
$c== :: SKind -> SKind -> Bool
Eq, Eq SKind
Eq SKind
-> (SKind -> SKind -> Ordering)
-> (SKind -> SKind -> Bool)
-> (SKind -> SKind -> Bool)
-> (SKind -> SKind -> Bool)
-> (SKind -> SKind -> Bool)
-> (SKind -> SKind -> SKind)
-> (SKind -> SKind -> SKind)
-> Ord SKind
SKind -> SKind -> Bool
SKind -> SKind -> Ordering
SKind -> SKind -> SKind
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
min :: SKind -> SKind -> SKind
$cmin :: SKind -> SKind -> SKind
max :: SKind -> SKind -> SKind
$cmax :: SKind -> SKind -> SKind
>= :: SKind -> SKind -> Bool
$c>= :: SKind -> SKind -> Bool
> :: SKind -> SKind -> Bool
$c> :: SKind -> SKind -> Bool
<= :: SKind -> SKind -> Bool
$c<= :: SKind -> SKind -> Bool
< :: SKind -> SKind -> Bool
$c< :: SKind -> SKind -> Bool
compare :: SKind -> SKind -> Ordering
$ccompare :: SKind -> SKind -> Ordering
Ord)

-- | The values kept track of by the interpreter
data Val = Base S.SVal
         | Typ  SKind
         | Tup  [Val]
         | Lst  [Val]
         | Func (Maybe String) (Val -> Eval Val)

-- | Outputable instance for SKind
instance Outputable SKind where
   ppr :: SKind -> SDoc
ppr (KBase Kind
k)   = String -> SDoc
text (Kind -> String
forall a. Show a => a -> String
show Kind
k)
   ppr (KTup  [SKind]
ks)  = SDoc -> SDoc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep (SDoc -> [SDoc] -> [SDoc]
punctuate (String -> SDoc
text String
",") ((SKind -> SDoc) -> [SKind] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map SKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr [SKind]
ks))
   ppr (KLst  SKind
k)   = SDoc -> SDoc
brackets (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr SKind
k
   ppr (KFun  SKind
k SKind
r) = SDoc -> SDoc
parens (SKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr SKind
k) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"->" SDoc -> SDoc -> SDoc
<+> SKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr SKind
r

-- | Outputable instance for S.Kind
instance Outputable S.Kind where
   ppr :: Kind -> SDoc
ppr = String -> SDoc
text (String -> SDoc) -> (Kind -> String) -> Kind -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> String
forall a. Show a => a -> String
show

-- | Outputable instance for Val
instance Outputable Val where
   ppr :: Val -> SDoc
ppr (Base SVal
s)   = String -> SDoc
text (SVal -> String
forall a. Show a => a -> String
show SVal
s)
   ppr (Typ  SKind
k)   = SKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr SKind
k
   ppr (Tup  [Val]
vs)  = SDoc -> SDoc
parens   (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate (String -> SDoc
text String
",") ((Val -> SDoc) -> [Val] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Val]
vs)
   ppr (Lst  [Val]
vs)  = SDoc -> SDoc
brackets (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate (String -> SDoc
text String
",") ((Val -> SDoc) -> [Val] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Val]
vs)
   ppr (Func Maybe String
k Val -> Eval Val
_) = String -> SDoc
text (String
"Func<" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe String -> String
forall a. Show a => a -> String
show Maybe String
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
">")

-- | Structural lifting of a boolean function (eq/neq) over Val
liftEqVal :: (S.SVal -> S.SVal -> S.SVal) -> Val -> Val -> S.SVal
liftEqVal :: (SVal -> SVal -> SVal) -> Val -> Val -> SVal
liftEqVal SVal -> SVal -> SVal
baseEq Val
v1 Val
v2 = Val -> Val -> SVal
k Val
v1 Val
v2
  where k :: Val -> Val -> SVal
k (Base SVal
a) (Base SVal
b)                          = SVal
a SVal -> SVal -> SVal
`baseEq` SVal
b
        k (Tup [Val]
as) (Tup [Val]
bs) | [Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
bs = (SVal -> SVal -> SVal) -> SVal -> [SVal] -> SVal
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SVal -> SVal -> SVal
S.svAnd SVal
S.svTrue                            ((Val -> Val -> SVal) -> [Val] -> [Val] -> [SVal]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Val -> Val -> SVal
k [Val]
as [Val]
bs)
        k (Lst [Val]
as) (Lst [Val]
bs)                          = (SVal -> SVal -> SVal) -> SVal -> [SVal] -> SVal
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SVal -> SVal -> SVal
S.svAnd (Bool -> SVal
S.svBool ([Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
bs)) ((Val -> Val -> SVal) -> [Val] -> [Val] -> [SVal]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Val -> Val -> SVal
k [Val]
as [Val]
bs)
        k Val
_ Val
_                                        = String -> SVal
forall a. HasCallStack => String -> a
error  (String -> SVal) -> String -> SVal
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened: liftEq received unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe ((Val, Val) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Val
v1, Val
v2))

-- | Symbolic equality over values
eqVal :: Val -> Val -> S.SVal
eqVal :: Val -> Val -> SVal
eqVal = (SVal -> SVal -> SVal) -> Val -> Val -> SVal
liftEqVal SVal -> SVal -> SVal
S.svEqual

-- | Symbolic if-then-else over values.
iteVal :: ([String] -> Eval Val) -> S.SVal -> Val -> Val -> Eval Val
iteVal :: ([String] -> Eval Val) -> SVal -> Val -> Val -> Eval Val
iteVal [String] -> Eval Val
die SVal
t Val
v1 Val
v2 = Val -> Val -> Eval Val
k Val
v1 Val
v2
  where k :: Val -> Val -> Eval Val
k (Base SVal
a) (Base SVal
b)                          = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ SVal -> Val
Base (SVal -> Val) -> SVal -> Val
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal -> SVal
S.svIte SVal
t SVal
a SVal
b
        k (Tup [Val]
as) (Tup [Val]
bs) | [Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
bs = [Val] -> Val
Tup ([Val] -> Val) -> ReaderT Env Symbolic [Val] -> Eval Val
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Val -> Val -> Eval Val)
-> [Val] -> [Val] -> ReaderT Env Symbolic [Val]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Val -> Val -> Eval Val
k [Val]
as [Val]
bs
        k (Lst [Val]
as) (Lst [Val]
bs) | [Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
bs = [Val] -> Val
Lst ([Val] -> Val) -> ReaderT Env Symbolic [Val] -> Eval Val
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (Val -> Val -> Eval Val)
-> [Val] -> [Val] -> ReaderT Env Symbolic [Val]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Val -> Val -> Eval Val
k [Val]
as [Val]
bs
                            | Bool
True                   = [String] -> Eval Val
die [ String
"Alternatives are producing lists of differing sizes:"
                                                           , String
"   Length " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
as) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([Val] -> Val
Lst [Val]
as))
                                                           , String
"vs Length " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Val] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
bs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([Val] -> Val
Lst [Val]
bs))
                                                           ]
        k (Func Maybe String
n1 Val -> Eval Val
f) (Func Maybe String
n2 Val -> Eval Val
g)                    = Val -> Eval Val
forall (m :: * -> *) a. Monad m => a -> m a
return (Val -> Eval Val) -> Val -> Eval Val
forall a b. (a -> b) -> a -> b
$ Maybe String -> (Val -> Eval Val) -> Val
Func (Maybe String
n1 Maybe String -> Maybe String -> Maybe String
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe String
n2) ((Val -> Eval Val) -> Val) -> (Val -> Eval Val) -> Val
forall a b. (a -> b) -> a -> b
$ \Val
a -> Val -> Eval Val
f Val
a Eval Val -> (Val -> Eval Val) -> Eval Val
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Val
fa -> Val -> Eval Val
g Val
a Eval Val -> (Val -> Eval Val) -> Eval Val
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Val
ga -> Val -> Val -> Eval Val
k Val
fa Val
ga
        k Val
_ Val
_                                        = [String] -> Eval Val
die [ String
"Unsupported if-then-else/case with alternatives:"
                                                           , String
"    Value:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
v1)
                                                           , String
"       vs:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SDoc -> String
showSDocUnsafe (Val -> SDoc
forall a. Outputable a => a -> SDoc
ppr Val
v2)
                                                           ]

-- | Compute the span given a Tick. Returns the old-span if the tick span useless.
tickSpan :: GenTickish t -> SrcSpan
tickSpan :: forall (t :: TickishPass). GenTickish t -> SrcSpan
tickSpan (ProfNote CostCentre
cc Bool
_ Bool
_) = CostCentre -> SrcSpan
cc_loc CostCentre
cc
tickSpan (SourceNote RealSrcSpan
s String
_)  = RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan RealSrcSpan
s Maybe BufSpan
forall a. Maybe a
Nothing
tickSpan GenTickish t
_                 = SrcSpan
noSrcSpan

-- | Compute the span for a binding.
varSpan :: Var -> SrcSpan
varSpan :: Var -> SrcSpan
varSpan = Name -> SrcSpan
nameSrcSpan (Name -> SrcSpan) -> (Var -> Name) -> Var -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Name
varName

-- | Pick the first "good" span, hopefully corresponding to
-- the closest location to where we are in the code
-- when we issue an error message.
pickSpan :: [SrcSpan] -> SrcSpan
pickSpan :: [SrcSpan] -> SrcSpan
pickSpan [SrcSpan]
ss = case (SrcSpan -> Bool) -> [SrcSpan] -> [SrcSpan]
forall a. (a -> Bool) -> [a] -> [a]
filter SrcSpan -> Bool
isGoodSrcSpan [SrcSpan]
ss of
                (SrcSpan
s:[SrcSpan]
_) -> SrcSpan
s
                []    -> SrcSpan
noSrcSpan

-- | Show a GHC span in user-friendly form
showSpan :: DynFlags -> SrcSpan -> String
showSpan :: DynFlags -> SrcSpan -> String
showSpan DynFlags
fs SrcSpan
s = DynFlags -> SDoc -> String
showSDoc DynFlags
fs (SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
s)

-- | This comes mighty handy! Wonder why GHC doesn't have it already:
instance Show CoreExpr where
  show :: CoreExpr -> String
show = CoreExpr -> String
forall {a}. OutputableBndr a => Expr a -> String
go
    where sh :: a -> String
sh a
x = SDoc -> String
showSDocUnsafe (a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
x)
          go :: Expr a -> String
go (Var   Var
i)      = String
"(Var "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Var -> String
forall {a}. Outputable a => a -> String
sh Var
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          go (Lit   Literal
l)      = String
"(Lit "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Literal -> String
forall {a}. Outputable a => a -> String
sh Literal
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          go (App Expr a
f Expr a
a)      = String
"(App "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
go Expr a
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
go Expr a
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          go (Lam a
b Expr a
e)      = String
"(Lam "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Outputable a => a -> String
sh a
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
go Expr a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          go (Let Bind a
b Expr a
e)      = String
"(Let "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bind a -> String
forall {a}. Outputable a => a -> String
sh Bind a
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
go Expr a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          go (Case Expr a
e a
b Type
t [Alt a]
_) = String
"(Case " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
go Expr a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall {a}. Outputable a => a -> String
sh a
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall {a}. Outputable a => a -> String
sh Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"...)"
          go (Cast Expr a
e CoercionR
_)     = String
"(Cast " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
go Expr a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ...)"
          go (Tick CoreTickish
_ Expr a
e)     = String
"(Tick " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
go Expr a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          go (Type Type
t)       = String
"(Type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall {a}. Outputable a => a -> String
sh Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          go (Coercion CoercionR
_)   = String
"(Coercion ...)"