Редактировать после получения комментариев

После получения комментариев я думаю, что вам нужна функция deleteFirst, подобная той, которая обсуждается в этом ТАК ответьте.

Чтобы сделать это символическим, вам не обязательно заключать аргументы функции в UnionM, вместо этого вам нужно просто обернуть в них результат.

symDeleteFirst :: [SymInteger] -> SymInteger -> UnionM [SymInteger]
symDeleteFirst [] _ = mrgReturn []
symDeleteFirst (x:xs) v = mrgIf (x .== v) (mrgReturn xs) (mrgFmap (x:) $ symDeleteFirst xs v)

Эту функцию все еще можно использовать на UnionM [SymInteger] следующим образом:

a :: UnionM [SymInteger]
a = mrgIf "x" (return ["a", "b"]) (return ["c", "d", "e"])

n :: SymInteger
n = "n"

do
  v <- a
  symDeleteFirst v n

Результат будет следующим. Это немного сложно, хотя, вероятно, это один из самых простых результатов, поскольку в программе много ветвей.

{If (&& x (|| (= a n) (= b n)))
  [(ite (= a n) b a)]
  (If (|| x (|| (= c n) (|| (= d n) (= e n))))
    [(ite x a (ite (= c n) d c)),(ite x b (ite (|| (= c n) (= d n)) e d))]
    [c,d,e])
}

Для функции минимума, упомянутой в комментарии, есть функция symMinimum, которая работает на [SymInteger].

Чтобы использовать его на UnionM [SymInteger], вы можете использовать fmap для получения результата UnionM SymInteger, а затем объединить UnionM SymInteger с SymInteger с помощью simpleMerge:

a :: UnionM [SymInteger]
a = mrgIf "x" (return ["a", "b"]) (return ["c", "d", "e"])

simpleMerge $ symMinimum <$> a

Это даст вам

(ite x (ite (<= b a) b a) (ite (<= e (ite (<= d c) d c)) e (ite (<= d c) d c)))

Первая версия

Спасибо за интерес к библиотеке Гризетт, автором которой являюсь я. Я только что создал обсуждения GitHub, чтобы дальнейшие обсуждения могли проходить там.

ТЛ;ДР

Если вы еще не ознакомились, недавно для Grisette был создан небольшой туториал.

В большинстве случаев вам не обязательно использовать UnionM SymInteger, а ваш pickLargest можно реализовать с помощью mrgIte.

pickLargest :: [SymInteger] -> [SymInteger] -> [SymInteger]
-- skip simple cases
pickLargest (x:xs) (y:ys) = (mrgIte (x .> y) x y) : (sumSym xs ys)

symDrop это не то, что вам нужно. Возможно, вы захотите обновить Grisette до последней версии и использовать mrgDelete . symMax там же доступен.

С symMax существует еще более простое решение:

pickLargest :: [SymInteger] -> [SymInteger] -> [SymInteger]
pickLargest = zipWith symMax

Ваш symListDrop вызывает себя с теми же операндами, и поэтому он бесконечно рекурсивно.

Перед обсуждением SymInteger

У меня к вам первый вопрос: нужна ли symDrop функция? Его семантика аналогична drop в base, где второй SymInteger — это количество элементов, которые нужно удалить из головы списка, а не сам элемент.

Я предлагаю вам обновиться до последней версии пакета Grisette (v0.5.0.1 на сегодняшний день), который доступен на ночных снимках Hackage или Stackage. Почти все функции из Data.List имеют символическую версию, и функция mrgDelete может оказаться тем, что вам нужно. Ожидайте некоторой несовместимости между версиями, поскольку некоторые функции переименованы с использованием более последовательной схемы именования, например, symDrop был переименован в mrgDrop, поскольку он возвращает объединение. (Оценочные) сложности для операторов также доступны в документации.

SimpleMergeable и mrgIte

Контейнер UnionM представлен для обработки многопутевого выполнения сложных структур данных. Эти структуры данных не способны самостоятельно обрабатывать условия пути, поэтому мы храним их в нескольких ветвях контейнера UnionM.

Однако некоторые структуры данных, например, символические примитивные типы (SymBool, SymInteger и т. д.), кортежи символических примитивных типов ((SymBool, SymInteger)), способны самостоятельно содержать условия пути. Эти структуры данных реализуют класс типа SimpleMergeable, который предоставляет функцию mrgIte.

mrgIte :: (SimpleMergeable a) => SymBool -> a -> a -> a

На первый взгляд это может сбить с толку, потому что у нас есть две разные версии «разделения путей», но на самом деле это сделано намеренно, а mrgIf и mrgIte имеют разную семантику. mrgIf аналогичен структуре потока управления, например, оператору if в C, тогда как mrgIte является тернарным оператором для построения выражения, например, ?: в C.

Если вам нужно работать с UnionM SymInteger...

Иногда невозможно избежать использования UnionM просто объединяемых типов, например, когда у вас есть общая структура данных, которая использует UnionM внутри себя. Grisette предоставляет помощники для работы с ними (например, (.#) и onUnion), а сигнатура типа следующая:

onUnion :: (SimpleMergeable r, Mergeable a) => (a -> r) -> UnionM a -> r

Для бесконечной рекурсии

Ваша функция вызывает саму себя (symListDrop m_ls m_el) с точно такими же операндами в последней строке.

Реализация вашего исходного вопроса

Теперь предположим, что мы хотим создать функцию, которая принимает два [SymInteger] и возвращает [SymInteger], имеющее поэлементный максимум из двух списков.

Это можно реализовать с помощью zipWith и symMax с последней версией Grisette:

pickLargest :: [SymInteger] -> [SymInteger] -> [SymInteger]
pickLargest = zipWith symMax