content: {-# LANGUAGE FlexibleContexts    #-}
  {-# LANGUAGE Rank2Types          #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications    #-}
  {-# LANGUAGE TypeFamilies        #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module Main where
  
  import Data.SBV
  import Data.Proxy
  import Numeric
  import Data.List
  import Control.Concurrent.Async ( async, wait )
  
  findBounds :: forall a b. (IEEEFloating a, Integral b, Metric a, Metric b, SymVal b, SymVal a) => SRoundingMode -> Proxy a -> Proxy b -> IO (a, a)
  findBounds rm _pa _pb = (,) <$> opt False <*> opt True
    where
      f up = do
        x :: SBV a <- free "x"
        y :: SBV b <- free "y"
  
        constrain $ sFromIntegral y .== fpRoundToIntegral rm x
  
        obj up "x" x
        obj up "y" y
  
      obj True  = maximize
      obj False = minimize
  
  
      opt up =
        do o <- optimizeWith z3 Lexicographic $ f up
           case o of
             LexicographicResult m -> case getModelValue "x" m of
                                        Just x  -> return x
                                        Nothing -> error "Can't find x"
             _ -> error "Didn't expect this!"
  
  getBounds :: forall b. (Integral b, SymVal b, Metric b) => Proxy b -> RoundingMode -> IO String
  getBounds b m = do f <- async $ findBounds (literal m) (Proxy @Float)  b
                     d <- async $ findBounds (literal m) (Proxy @Double) b
                     (lf, uf) <- wait f
                     (ld, ud) <- wait d
                     let s =    "(("  ++ sh (kindOf b)
                             ++ ", " ++ pad 22 (show m) ++ ")"
                             ++ ", (" ++ "(" ++ pad l1 (showHFloat lf "") ++ ", " ++ pad l2 (showHFloat uf "") ++ ")"
                             ++ ", " ++ "(" ++ pad l3 (showHFloat ld "") ++ ", " ++ pad l4 (showHFloat ud "") ++ ")"
                             ++ ")) -- " ++ show (kindOf b)
                     return s
    where sh (KBounded t sz) = "KBounded " ++ shB t ++ " " ++ shSz sz
          sh _               = error "needs bounded kind"
          shB True  = "True "
          shB False = "False"
          shSz 8    = "8 "
          shSz i    = show i
          pad n s   = s ++ replicate (n - length s) ' '
          l1 = 14
          l2 = 13
          l3 = 22
          l4 = 21
  
  getAllModes :: forall b. (Integral b, SymVal b, Metric b) => Proxy b -> IO [String]
  getAllModes b = traverse (getBounds b) [minBound .. maxBound]
  
  main :: IO ()
  main = do l1 <- async . getAllModes $ Proxy @Word8
            l2 <- async . getAllModes $ Proxy @Word16
            l3 <- async . getAllModes $ Proxy @Word32
            l4 <- async . getAllModes $ Proxy @Word64
            l5 <- async . getAllModes $ Proxy @Int8
            l6 <- async . getAllModes $ Proxy @Int16
            l7 <- async . getAllModes $ Proxy @Int32
            l8 <- async . getAllModes $ Proxy @Int64
            ls <- concat <$> traverse wait [l1, l2, l3, l4, l5, l6, l7, l8]
  
            let out =  unlines [ "-----------------------------------------------------------------------------"
                               , "-- |"
                               , "-- Module    : Data.SBV.Utils.PrettyNum"
                               , "-- Copyright : (c) Matt Peddie"
                               , "--                 Levent Erkok"
                               , "-- License   : BSD3"
                               , "-- Maintainer: erkokl@gmail.com"
                               , "-- Stability : experimental"
                               , "--"
                               , "-- Conversion bounds for floating to integral types. This file is"
                               , "-- automatically generated by buildUtils/generateBounds.hs."
                               , "--"
                               , "-- Please DO NOT modify directly."
                               , "-----------------------------------------------------------------------------"
                               , ""
                               , "{-# LANGUAGE HexFloatLiterals #-}"
                               , ""
                               , "module Data.SBV.Utils.FloatConversionBounds (conversionBounds) where"
                               , ""
                               , "import Data.SBV.Core.Kind     (Kind(..))"
                               , "import Data.SBV.Core.Symbolic (RoundingMode(..))"
                               , ""
                               , "-- | For each target type and rounding mode, returns the valid conversion bounds from floats and doubles."
                               , "-- Each pair on the right hand side shows the inclusive lower and upper bounds that are safely convertible in the"
                               , "-- given rounding mode to the corresponding type, using 'Data.SBV.fromSFloat' and 'Data.SBV.fromSDouble', respectively."
                               , "conversionBounds :: [((Kind, RoundingMode), ((Float, Float), (Double, Double)))]"
                               , "conversionBounds = [\n    " ++ intercalate "\n  , " ls ++ "\n  ]"
                               ]
  
            putStr out
  