[SOLVED] How do I check if the result of symTake is equal to a concrete list?

How do I check if the result of symTake is equal to a concrete list?

This is my code:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}

import Grisette

x :: SymInteger
x = "x"

y :: SymInteger
y = "y"

numbers :: [SymInteger]
numbers = [x, y]

n :: SymInteger
n = "n"

result :: UnionM [SymInteger]
result = symTake n numbers

main :: IO ()
main = do
    print $ result .== [1, 2]

I want to check whether result can be equal to [1, 2]. I can test if a simple list of symbolic integers can be equal to [1, 2]. For example, I can do this:

x :: SymInteger
x = "x"

y :: SymInteger
y = "y"

main :: IO ()
main = do
    print $ [x, y] .== [1, 2]

But I can't find a way to do that with the result of symTake. Reading the code/docs in the code, it seems I'm not supposed to unbox the [SymInteger] out of the UnionM, but then I don't know how do check for equality.

Solution

I think you want:

print $ result .== mrgSingle [1, 2]

The issue here is that symTake applied to the list [x,y] can result in a list of size 0, 1, or 2, and unlike the fixed-length list numbers = [x,y], this requires a UnionM to be properly represented. To compare a UnionM to a non-UnionM, you must use mrgSingle to promote the non-union.

The result looks plausible, if a little overcomplicated:

> main
(&& (! (<= 0 (- n))) (&& (! (<= -1 (- n))) (&& (= x 1) (= y 2))))