Превращение значений Haskell Int в константы для ограничений SBV

Question

Я вижу много примеров использования библиотеки SBV следующим образом:

f :: IO SatResult
f = sat $ do
      x <- sInteger "x"
      constraint $ x .< 200

Для функции, которая принимает Haskell Int, я хотел бы использовать этот Int в моих формулах ограничений, передаваемых в Z3 через библиотеку Data.SBV:

f :: Int -> IO SatResult
f i = sat $ do
          x <- sInteger "x"
          constraint $ x .< (g i)
        where
          g = ???

Как я могу преобразовать из Haskell Int в SInteger или какой-нибудь подходящий экземпляр OrdSymbolic и EqSymbolic для использования с (.<) И (. ==)?

Спасибо!

Answer 1

Функциональный литерал должен сделать это. Вы, вероятно, должны быть более четкими в отношении типа, такие как Integer, Int8, Int16 и т. д. вместо просто Int,

Вы также можете просто сделать fromIntegral, поскольку числовые символические типы являются экземплярами Num учебный класс:

Prelude Data.SBV> (fromIntegral (2::Int)) :: SInteger
2 :: SInteger