[x ..] (finite, open-ended enumeration) should be removed from the language

[brianhuffman]

In Cryptol, the syntax [x ..] is actually shorthand for [x..2^^n-1], which often ends up being a vector with 18446744073709551616 elements, or some such. Such large (but finite) sequences are tricky and/or expensive to deal with during evaluation, and can cause problems in SAW or other backends. Usually users actually intend to write the very similar-looking [x ...], which gives a lazy infinite sequence that is easier to work with.

The [x..] construct has caused many problems: #226, #375, GaloisInc/saw-script#11, GaloisInc/saw-script#276, GaloisInc/saw-script#284, and GaloisInc/saw-script#368, to name a few.

I propose to remove the [x..] syntax from Cryptol. It does a poor job of conveying programmer intent, and experience shows that it often leads to nasty surprises. Users should write [x...] or [x..y] instead. We should remove the [x,y..] syntax as well.

[robdockins]

I, for one, am in favor. I've never seen a use of [x..] that isn't better instead as [x...]