strictness of indexing

[msaaltink]

Here's another place where the reference evaluator and REPL evaluator disagree:

Cryptol> :eval [(),()] @ 3
()
Cryptol> [(),()] @ 3

invalid sequence index: 3

I think the reference evaluator actually is strict in the index, but the domain for () has no room for an error, as we see in

Cryptol> (error "?"):()
()

We of course see the same issue with the other three indexing operators !, @@, and !!.

[msaaltink]

This issue afflicts other primitives that take a strict number, in cases where the type of the result is a singleton. For example

Cryptol>  [(),()] << [True, error "x"]

Run-time error: x
Cryptol> :eval [(),()] << [True, error "x"]
[(), ()]

or

Cryptol> :eval [(),()] <<< [True, f 0x0] where f n = f(n+1)
[(), ()]
Cryptol> [(),()] <<< [True, f 0x0] where f n = f(n+1)

where the REPL gets in an infinite loop.

So the REPL does not appear to have the domains advertised in the Reference implementation, in particular we have extra error and bottom elements.

[robdockins]

Indeed, these are pretty tricky issues. We could solve them by doing the necessary eta-expansion at every indexing call, but I suspect that would result in an enormous performance degradation in the common cases.

I have some vague ideas in mind for how we could deal with these issues better. The most fully formed is this: in the evaluator, always be evaluating in the context of a "demand shape", which identifies both the desired result type, and how much of the resulting shape the use site promises to examine. This would essentially perform a runtime analogue of demand analysis. Then, using that information, we would have enough context to know when we need to perform expensive eta-expansions, and when we can just go ahead and force things. In many cases, I hypothesize, we would get the more efficient eager evaluation behavior, while still correctly handling the tricky corner cases.

[robdockins]

The reference interpreter was updated in #866, which removes some, but not all, of these mismatches.

[robdockins]

Fixed via #1136