{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}

module What4.Utils.Versions where

import qualified Config as Config
import           Control.Exception (throw, throwIO)
import           Control.Monad (foldM)
import           Control.Monad.IO.Class
import           Data.List (find)
import           Data.Text (Text)
import qualified Data.Text.IO as Text
import           Data.Versions (Version(..))
import qualified Data.Versions as Versions
import           Instances.TH.Lift ()

import           Language.Haskell.TH
import           Language.Haskell.TH.Lift

ver :: Text -> Q Exp
ver :: Text -> Q Exp
ver Text
nm =
  case Text -> Either ParsingError Version
Versions.version Text
nm of
    Left ParsingError
err -> ParsingError -> Q Exp
forall a e. Exception e => e -> a
throw ParsingError
err
    Right Version
v  -> Version -> Q Exp
forall t (m :: Type -> Type). (Lift t, Quote m) => t -> m Exp
forall (m :: Type -> Type). Quote m => Version -> m Exp
lift Version
v

data SolverBounds =
  SolverBounds
  { SolverBounds -> Maybe Version
lower :: Maybe Version
  , SolverBounds -> Maybe Version
upper :: Maybe Version
  , SolverBounds -> Maybe Version
recommended :: Maybe Version
  }

deriving instance Lift SolverBounds

emptySolverBounds :: SolverBounds
emptySolverBounds :: SolverBounds
emptySolverBounds = Maybe Version -> Maybe Version -> Maybe Version -> SolverBounds
SolverBounds Maybe Version
forall a. Maybe a
Nothing Maybe Version
forall a. Maybe a
Nothing Maybe Version
forall a. Maybe a
Nothing

-- | This method parses configuration files describing the
--   upper and lower bounds of solver versions we expect to
--   work correctly with What4.  See the file \"solverBounds.config\"
--   for examples of how such bounds are specified.
parseSolverBounds :: FilePath -> IO [(Text,SolverBounds)]
parseSolverBounds :: [Char] -> IO [(Text, SolverBounds)]
parseSolverBounds [Char]
fname =
  do Either ParseError (Value Position)
cf <- Text -> Either ParseError (Value Position)
Config.parse (Text -> Either ParseError (Value Position))
-> IO Text -> IO (Either ParseError (Value Position))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO Text
Text.readFile [Char]
fname
     case Either ParseError (Value Position)
cf of
       Left ParseError
err -> ParseError -> IO [(Text, SolverBounds)]
forall e a. Exception e => e -> IO a
throwIO ParseError
err
       Right (Config.Sections Position
_ [Section Position]
ss)
         | Just Config.Section{ sectionValue :: forall a. Section a -> Value a
Config.sectionValue = Config.Sections Position
_ [Section Position]
vs } <-
                   (Section Position -> Bool)
-> [Section Position] -> Maybe (Section Position)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
find (\Section Position
s -> Section Position -> Text
forall a. Section a -> Text
Config.sectionName Section Position
s Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"solvers") [Section Position]
ss
         -> (Section Position -> IO (Text, SolverBounds))
-> [Section Position] -> IO [(Text, SolverBounds)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM Section Position -> IO (Text, SolverBounds)
getSolverBound [Section Position]
vs

       Right Value Position
_ -> [Char] -> IO [(Text, SolverBounds)]
forall a. [Char] -> IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"could not parse solver bounds from " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fname)

 where
   getSolverBound :: Config.Section Config.Position -> IO (Text, SolverBounds)
   getSolverBound :: Section Position -> IO (Text, SolverBounds)
getSolverBound Config.Section{ sectionName :: forall a. Section a -> Text
Config.sectionName = Text
nm, sectionValue :: forall a. Section a -> Value a
Config.sectionValue = Config.Sections Position
_ [Section Position]
vs } =
     do SolverBounds
b <- (SolverBounds -> Section Position -> IO SolverBounds)
-> SolverBounds -> [Section Position] -> IO SolverBounds
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM SolverBounds -> Section Position -> IO SolverBounds
updateBound SolverBounds
emptySolverBounds [Section Position]
vs
        (Text, SolverBounds) -> IO (Text, SolverBounds)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Text
nm, SolverBounds
b)
   getSolverBound Section Position
v = [Char] -> IO (Text, SolverBounds)
forall a. [Char] -> IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"could not parse solver bounds " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Section Position -> [Char]
forall a. Show a => a -> [Char]
show Section Position
v)


   updateBound :: SolverBounds -> Config.Section Config.Position -> IO SolverBounds
   updateBound :: SolverBounds -> Section Position -> IO SolverBounds
updateBound SolverBounds
bnd Config.Section{ sectionName :: forall a. Section a -> Text
Config.sectionName = Text
nm, sectionValue :: forall a. Section a -> Value a
Config.sectionValue = Config.Text Position
_ Text
val} =
     case Text -> Either ParsingError Version
Versions.version Text
val of
       Left ParsingError
err -> ParsingError -> IO SolverBounds
forall e a. Exception e => e -> IO a
throwIO ParsingError
err
       Right Version
v
         | Text
nm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"lower"       -> SolverBounds -> IO SolverBounds
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { lower = Just v }
         | Text
nm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"upper"       -> SolverBounds -> IO SolverBounds
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { upper = Just v }
         | Text
nm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"recommended" -> SolverBounds -> IO SolverBounds
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { recommended = Just v }
         | Bool
otherwise -> [Char] -> IO SolverBounds
forall a. [Char] -> IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"unrecognized solver bound name" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
nm)

   updateBound SolverBounds
_ Section Position
v = [Char] -> IO SolverBounds
forall a. [Char] -> IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"could not parse solver bound " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Section Position -> [Char]
forall a. Show a => a -> [Char]
show Section Position
v)


computeDefaultSolverBounds :: Q Exp
computeDefaultSolverBounds :: Q Exp
computeDefaultSolverBounds =
  [(Text, SolverBounds)] -> Q Exp
forall t (m :: Type -> Type). (Lift t, Quote m) => t -> m Exp
forall (m :: Type -> Type).
Quote m =>
[(Text, SolverBounds)] -> m Exp
lift ([(Text, SolverBounds)] -> Q Exp)
-> Q [(Text, SolverBounds)] -> Q Exp
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (IO [(Text, SolverBounds)] -> Q [(Text, SolverBounds)]
forall a. IO a -> Q a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO ([Char] -> IO [(Text, SolverBounds)]
parseSolverBounds [Char]
"solverBounds.config"))