conjure icon indicating copy to clipboard operation
conjure copied to clipboard

`sequence` documentation and implementation do not agree

Open stylpe opened this issue 2 years ago • 1 comments

Here's two problems I've found while using the sequence type that I think might have a common root cause:

The documentation says

  • "Sequences are indexed by a contiguous list of increasing integers, beginning at 1."
  • Nothing to the effect that there's anything special about using a sequence in a comprehension

But this example contradicts both of these points:

letting N be domain int(1..9)
letting s be sequence((2,5),(8,4))
letting l be [x | x <- s]

find t,u : (N,N)
such that t=s[1]
such that u=l[1]

The error message explains it well enough:

Error 1:
    In a 'such that' statement: t = s[1]
    Error:
        Indexing something other than a matrix or a tuple:
            The expression: s[1]
            Indexing: s
            With type: sequence of (int, int)
Error 2:
    In a 'such that' statement: u = l[1]
    Error:
        When type checking: u = l[1]
        Cannot unify the types of the following.
        lhs        : u
        type of lhs: (int, int)
        rhs        : l[1]
        type of rhs: (int, (int, int))

And my suspicion is that there's something wrong with the indexing implementation that causes the index values to combine with the actual values instead.

Bonus issue:

$ Here's l's actual type:
$ But the examples cause a json formatting error (backslashes in /\ and \/ aren't escaped)
$find v : matrix indexed by [int(1..2)] of (int(1..2),(N,N))
$such that v = l
$find t2,u2 : (int(1..2),(N,N))
$such that t2=l[1],u2=l[2]

Context: Some variant Sudoku rules use lines to indicate constraints like digits must strictly increase or form a palindrome or many others. I chose letting N be domain int(1..9) letting Coord be domain (N,N) given Path : sequence of Coord find Grid : matrix indexed by [N,N] of N (some details elided) to represent this since the given lines can be of any length, and I need to be able to index it in reverse to write a palindrome constraint and therefore need to be able to use |Path| to determine the last index. That's not possible if it's a matrix domain. If you have any advice for a better approach to design a palindrome constraint like this, like a way to find the cardinality of a given Path : matrix indexed by [int(1..)] of Coord, please let me know.

Replit: https://replit.com/@SuperMikal/Conjure-and-Essence-20220507#feedback/Sequence%20unexpected%20behaviour/minimal.essence

stylpe avatar May 21 '22 22:05 stylpe

A sequence is not an array, and if s is a sequence then s(1) is the first element. The error here is not very helpful, admittedly. Moreover, s(1) is a tuple (2,5):

letting s be sequence((2,5),(8,4))
find t : tuple(int(1..9),int(1..9))
such that t = s(1)

has solution

letting t be (2, 5)

However, there does seem to be something wrong with indexing tuples, which I'll post as a separate issue.

ott2 avatar Sep 06 '22 12:09 ott2

I'll close this since I don't think there is anything to fix? Please reopen @stylpe if needed.

ozgurakgun avatar Feb 20 '23 12:02 ozgurakgun