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

{-# OPTIONS_GHC -Wno-orphans #-}

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

-- NB, orphan instances :-(
deriving instance Lift Versions.VUnit
deriving instance Lift Versions.Version

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. Lift t => t -> Q 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 :: FilePath -> IO [(Text, SolverBounds)]
parseSolverBounds FilePath
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
<$> FilePath -> IO Text
Text.readFile FilePath
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)
mapM Section Position -> IO (Text, SolverBounds)
getSolverBound [Section Position]
vs

       Right Value Position
_ -> FilePath -> IO [(Text, SolverBounds)]
forall (m :: Type -> Type) a. MonadFail m => FilePath -> m a
fail (FilePath
"could not parse solver bounds from " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
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 (f :: Type -> Type) a. Applicative f => a -> f a
pure (Text
nm, SolverBounds
b)
   getSolverBound Section Position
v = FilePath -> IO (Text, SolverBounds)
forall (m :: Type -> Type) a. MonadFail m => FilePath -> m a
fail (FilePath
"could not parse solver bounds " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Section Position -> FilePath
forall a. Show a => a -> FilePath
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 (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { lower :: Maybe Version
lower = Version -> Maybe Version
forall a. a -> Maybe a
Just Version
v }
         | Text
nm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"upper"       -> SolverBounds -> IO SolverBounds
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { upper :: Maybe Version
upper = Version -> Maybe Version
forall a. a -> Maybe a
Just Version
v }
         | Text
nm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"recommended" -> SolverBounds -> IO SolverBounds
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { recommended :: Maybe Version
recommended = Version -> Maybe Version
forall a. a -> Maybe a
Just Version
v }
         | Bool
otherwise -> FilePath -> IO SolverBounds
forall (m :: Type -> Type) a. MonadFail m => FilePath -> m a
fail (FilePath
"unrecognized solver bound name" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
forall a. Show a => a -> FilePath
show Text
nm)

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


computeDefaultSolverBounds :: Q Exp
computeDefaultSolverBounds :: Q Exp
computeDefaultSolverBounds =
  [(Text, SolverBounds)] -> Q Exp
forall t. Lift t => t -> Q 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 (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO [(Text, SolverBounds)]
parseSolverBounds FilePath
"solverBounds.config"))