{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
module Data.SBV.Plugin.Common where
import Control.Monad (zipWithM, mplus)
import Control.Monad.Reader
import GHC.Plugins
import qualified GHC.Data.Strict as GDS (Maybe(Nothing))
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
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
}
newtype TCKey = TCKey (TyCon, [TyCon])
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)
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
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
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
}
type Eval a = ReaderT Env S.Symbolic a
data Config = Config { Config -> Bool
isGHCi :: Bool
, Config -> [SBVAnnotation]
opts :: [SBVAnnotation]
, Config -> Var -> [SBVAnnotation]
sbvAnnotation :: Var -> [SBVAnnotation]
, Config -> Env
cfgEnv :: Env
}
pickSolvers :: [SBVOption] -> IO [S.SMTConfig]
pickSolvers :: [SBVOption] -> IO [SMTConfig]
pickSolvers [SBVOption]
slvrs
| SBVOption
AnySolver SBVOption -> [SBVOption] -> Bool
forall a. Eq a => a -> [a] -> 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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [SMTConfig
S.defaultSMTCfg]
[SMTConfig]
xs -> [SMTConfig] -> IO [SMTConfig]
forall a. a -> IO a
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)
]
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
$c== :: SKind -> SKind -> Bool
== :: SKind -> SKind -> Bool
$c/= :: SKind -> SKind -> Bool
/= :: 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
$ccompare :: SKind -> SKind -> Ordering
compare :: SKind -> SKind -> Ordering
$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
>= :: SKind -> SKind -> Bool
$cmax :: SKind -> SKind -> SKind
max :: SKind -> SKind -> SKind
$cmin :: SKind -> SKind -> SKind
min :: SKind -> SKind -> SKind
Ord)
data Val = Base S.SVal
| Typ SKind
| Tup [Val]
| Lst [Val]
| Func (Maybe String) (Val -> Eval Val)
instance Outputable SKind where
ppr :: SKind -> SDoc
ppr (KBase Kind
k) = String -> SDoc
forall doc. IsLine doc => String -> doc
text (Kind -> String
forall a. Show a => a -> String
show Kind
k)
ppr (KTup [SKind]
ks) = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep (SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate (String -> SDoc
forall doc. IsLine doc => String -> doc
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
forall doc. IsLine doc => doc -> doc
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
forall doc. IsLine doc => doc -> doc
parens (SKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr SKind
k) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SKind -> SDoc
forall a. Outputable a => a -> SDoc
ppr SKind
r
instance Outputable S.Kind where
ppr :: Kind -> SDoc
ppr = String -> SDoc
forall doc. IsLine doc => String -> doc
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
instance Outputable Val where
ppr :: Val -> SDoc
ppr (Base SVal
s) = String -> SDoc
forall doc. IsLine doc => String -> doc
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
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate (String -> SDoc
forall doc. IsLine doc => String -> doc
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
forall doc. IsLine doc => doc -> doc
brackets (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate (String -> SDoc
forall doc. IsLine doc => String -> doc
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
forall doc. IsLine doc => String -> doc
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
">")
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 a. [a] -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
bs = (SVal -> SVal -> SVal) -> SVal -> [SVal] -> SVal
forall a b. (a -> b -> b) -> b -> [a] -> b
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 a b. (a -> b -> b) -> b -> [a] -> b
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 a. [a] -> 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 a. [a] -> 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))
eqVal :: Val -> Val -> S.SVal
eqVal :: Val -> Val -> SVal
eqVal = (SVal -> SVal -> SVal) -> Val -> Val -> SVal
liftEqVal SVal -> SVal -> SVal
S.svEqual
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 a. a -> ReaderT Env Symbolic a
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 a. [a] -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
bs = [Val] -> Val
Tup ([Val] -> Val) -> ReaderT Env Symbolic [Val] -> Eval Val
forall a b.
(a -> b) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic b
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 a. [a] -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Val]
bs = [Val] -> Val
Lst ([Val] -> Val) -> ReaderT Env Symbolic [Val] -> Eval Val
forall a b.
(a -> b) -> ReaderT Env Symbolic a -> ReaderT Env Symbolic b
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 a. [a] -> 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 a. [a] -> 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 a. a -> ReaderT Env Symbolic a
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 a. Maybe a -> Maybe a -> Maybe a
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 a b.
ReaderT Env Symbolic a
-> (a -> ReaderT Env Symbolic b) -> ReaderT Env Symbolic b
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 a b.
ReaderT Env Symbolic a
-> (a -> ReaderT Env Symbolic b) -> ReaderT Env Symbolic b
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)
]
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 LexicalFastString
_) = RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan RealSrcSpan
s Maybe BufSpan
forall a. Maybe a
GDS.Nothing
tickSpan GenTickish t
_ = SrcSpan
noSrcSpan
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
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
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)
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 ...)"