    {-# 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. (HasCallStack, 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 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 cf of
           Left ParseError
    err -> ParseError -> IO [(Text, SolverBounds)]
    forall e a. (HasCallStack, 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 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
            pure (nm, 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. (HasCallStack, 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"))