content: {-# 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 nm =
    case Versions.version nm of
      Left err -> throw err
      Right v  -> lift v
  
  data SolverBounds =
    SolverBounds
    { lower :: Maybe Version
    , upper :: Maybe Version
    , recommended :: Maybe Version
    }
  
  deriving instance Lift SolverBounds
  
  emptySolverBounds :: SolverBounds
  emptySolverBounds = SolverBounds Nothing Nothing 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 fname =
    do cf <- Config.parse <$> Text.readFile fname
       case cf of
         Left err -> throwIO err
         Right (Config.Sections _ ss)
           | Just Config.Section{ Config.sectionValue = Config.Sections _ vs } <-
                     find (\s -> Config.sectionName s == "solvers") ss
           -> mapM getSolverBound vs
  
         Right _ -> fail ("could not parse solver bounds from " ++ fname)
  
   where
     getSolverBound :: Config.Section Config.Position -> IO (Text, SolverBounds)
     getSolverBound Config.Section{ Config.sectionName = nm, Config.sectionValue = Config.Sections _ vs } =
       do b <- foldM updateBound emptySolverBounds vs
          pure (nm, b)
     getSolverBound v = fail ("could not parse solver bounds " ++ show v)
  
  
     updateBound :: SolverBounds -> Config.Section Config.Position -> IO SolverBounds
     updateBound bnd Config.Section{ Config.sectionName = nm, Config.sectionValue = Config.Text _ val} =
       case Versions.version val of
         Left err -> throwIO err
         Right v
           | nm == "lower"       -> pure bnd { lower = Just v }
           | nm == "upper"       -> pure bnd { upper = Just v }
           | nm == "recommended" -> pure bnd { recommended = Just v }
           | otherwise -> fail ("unrecognized solver bound name" ++ show nm)
  
     updateBound _ v = fail ("could not parse solver bound " ++ show v)
  
  
  computeDefaultSolverBounds :: Q Exp
  computeDefaultSolverBounds =
    lift =<< (liftIO (parseSolverBounds "solverBounds.config"))
  