{-# 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 -> forall a e. Exception e => e -> a
throw ParsingError
err
    Right Version
v  -> forall t (m :: Type -> Type). (Lift t, Quote m) => t -> 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 forall a. Maybe a
Nothing forall a. Maybe a
Nothing 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 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 -> 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 } <-
                   forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
find (\Section Position
s -> forall a. Section a -> Text
Config.sectionName Section Position
s forall a. Eq a => a -> a -> Bool
== Text
"solvers") [Section Position]
ss
         -> 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
_ -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"could not parse solver bounds from " 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 <- 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
        forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Text
nm, SolverBounds
b)
   getSolverBound Section Position
v = forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"could not parse solver bounds " forall a. [a] -> [a] -> [a]
++ 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 -> forall e a. Exception e => e -> IO a
throwIO ParsingError
err
       Right Version
v
         | Text
nm forall a. Eq a => a -> a -> Bool
== Text
"lower"       -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { lower :: Maybe Version
lower = forall a. a -> Maybe a
Just Version
v }
         | Text
nm forall a. Eq a => a -> a -> Bool
== Text
"upper"       -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { upper :: Maybe Version
upper = forall a. a -> Maybe a
Just Version
v }
         | Text
nm forall a. Eq a => a -> a -> Bool
== Text
"recommended" -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SolverBounds
bnd { recommended :: Maybe Version
recommended = forall a. a -> Maybe a
Just Version
v }
         | Bool
otherwise -> forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"unrecognized solver bound name" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Text
nm)

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


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