module Language.Hasmtlib.Internal.Render where

import Data.ByteString.Builder
import Data.Foldable (foldl')
import Data.Sequence
import qualified Data.Text as Text
import qualified Data.Text.Encoding as Text.Enc
import GHC.TypeNats

-- | Render values to their SMTLib2-Lisp form, represented as 'Builder'.
class Render a where
  render :: a -> Builder

instance Render Bool where
  render :: Bool -> Builder
render Bool
b = if Bool
b then Builder
"true" else Builder
"false"
  {-# INLINEABLE render #-}

instance Render Nat where
  render :: Nat -> Builder
render = Integer -> Builder
integerDec (Integer -> Builder) -> (Nat -> Integer) -> Nat -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINEABLE render #-}

instance Render Integer where
  render :: Integer -> Builder
render Integer
x
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = Builder
"(- " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec (Integer -> Integer
forall a. Num a => a -> a
abs Integer
x) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    | Bool
otherwise = Integer -> Builder
integerDec Integer
x
  {-# INLINEABLE render #-}

instance Render Double where
  render :: Double -> Builder
render Double
x
    | Double
x Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0     = Builder
"(- " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> FloatFormat -> Double -> Builder
formatDouble FloatFormat
standardDefaultPrecision (Double -> Double
forall a. Num a => a -> a
abs Double
x) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    | Bool
otherwise = FloatFormat -> Double -> Builder
formatDouble FloatFormat
standardDefaultPrecision Double
x
  {-# INLINEABLE render #-}

instance Render Char where
  render :: Char -> Builder
render = Char -> Builder
char8
  {-# INLINE render #-}

instance Render String where
  render :: String -> Builder
render = String -> Builder
string8
  {-# INLINE render #-}

instance Render Builder where
  render :: Builder -> Builder
render = Builder -> Builder
forall a. a -> a
id
  {-# INLINE render #-}

instance Render Text.Text where
  render :: Text -> Builder
render = Text -> Builder
Text.Enc.encodeUtf8Builder
  {-# INLINE render #-}

renderUnary :: Render a => Builder -> a -> Builder
renderUnary :: forall a. Render a => Builder -> a -> Builder
renderUnary Builder
op a
x = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
{-# INLINEABLE renderUnary #-}

renderBinary :: (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary :: forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
op a
x b
y = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> b -> Builder
forall a. Render a => a -> Builder
render b
y Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
{-# INLINEABLE renderBinary #-}

renderTernary :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
renderTernary :: forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
renderTernary Builder
op a
x b
y c
z = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> b -> Builder
forall a. Render a => a -> Builder
render b
y Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> c -> Builder
forall a. Render a => a -> Builder
render c
z Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
{-# INLINEABLE renderTernary #-}

renderNary :: Render a => Builder -> [a] -> Builder
renderNary :: forall a. Render a => Builder -> [a] -> Builder
renderNary Builder
op [a]
xs = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
renderedXs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  where
    renderedXs :: Builder
renderedXs = (Builder -> a -> Builder) -> Builder -> [a] -> Builder
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Builder
s a
x -> Builder
s Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
x) Builder
forall a. Monoid a => a
mempty [a]
xs
{-# INLINEABLE renderNary #-}

-- | Render values to their sequential SMTLib2-Lisp form, represented as a 'Seq' 'Builder'.
class RenderSeq a where
  renderSeq :: a -> Seq Builder