Объединение кортежей в SBV? - PullRequest
Новая
       31

Объединение кортежей в SBV?

2 голосов
/ 03 июля 2019

В основном мне интересно, есть ли способ написать функцию следующего типа с библиотекой SBV: 

(SBV a, SBV b) -> SBV (a,b)

Кажется, что должно быть возможным: еслиу нас есть два символических значения, мы можем создать новое символическое значение, как конкретную пару, элементы которой являются символическими или конкретными значениями двух входов.Но я не могу найти ничего подобного, и у типа SBV нет конструкторов.

Возможно ли это?

1 Ответ

3 голосов
/ 04 июля 2019

Похоже, вам нужна функция tuple.Вот пример: 

import Data.SBV
import Data.SBV.Tuple

tup :: (SymVal a, SymVal b) => (SBV a, SBV b) -> SBV (a, b)
tup = tuple

tst :: Predicate
tst = do x <- sInteger "x"
         y <- sInteger "y"
         z <- sTuple "xy"

         return $ tup (x, y) .== z

Конечно, tuple сам может обрабатывать arity до 8;Выше приведен только один экземпляр того типа, который вы хотели.У нас есть: 

$ ghci a.hs
GHCi, version 8.6.4: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( a.hs, interpreted )
Ok, one module loaded.
*Main> sat tst
Satisfiable. Model:
  x  =     0 :: Integer
  y  =     1 :: Integer
  xy = (0,1) :: (Integer, Integer)

Также есть функция untuple, которая идет в другом направлении.Оба они находятся в модуле Data.SBV.Tuple, который необходимо явно импортировать.(Вы можете также найти линзовидные аксессоры в том же модуле, который позволяет писать ^._1, ^._2 и т. Д. Для извлечения полей кортежей; как в z^._2 для приведенного выше примера.)

...