module Language.Hasmtlib.Internal.Render where

import Data.ByteString.Builder
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 Builder where
  render :: Builder -> Builder
render = Builder -> Builder
forall a. a -> a
id
  {-# INLINEABLE 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 #-}