Make generate and lhs-indexing work for infinite sequences indexed by Integer.

[brianhuffman]

Currently generate, which is used for lhs-indexing syntactic sugar, can only be used for finite lists of length at least 1:

Cryptol> :? generate

    generate : {n, a, ix} (fin n, n >= 1, Integral ix,
                           Literal (n - 1) ix) =>
                 (ix -> a) -> [n]a

Produce a sequence using a generating function.
Satisfies 'generate f @ i == f i' for all 'i' between '0' and 'n-1'.

Declarations of the form 'x @ i = e' are syntactic sugar for
'x = generate (\i -> e)'.

It would be nice if we could use it for lists of any length, specifically for infinite sequences which could be indexed by an Integer. Being able to define zero-length sequences would be useful too, e.g. for defining sequences that are polymorphic in the length.

Implementing this will probably require adding a new type predicate as a constraint.

[weaversa]

While I wholeheartedly agree generate should be more general, I think we considered this is #848 and couldn't figure out a way to do it.

[brianhuffman]

I think #973 is closely related to this one. If we had a way to write [0..<n] for a list of length n, and it worked even when n is 0 or inf, then we could use that to define generate as generate f = [ f i | i <- [0 .. <n] ].

Actually, I suppose we could define generate as generate f = [ f i | i <- take`{n} [0...] ], but that would have a type that is a little more general than we really want: It is nice if the type of generate can prevent you from choosing an index type that is too small and wraps around before you get to the end of the list.