Reformulate evaluation semantics

[robdockins]

Initially, rewrite the reference interpreter to match the new Moggi-style monadic semantics we've been discussing for some time, which does away with the expensive and error-prone eta-expansion phases. Later, once we're convinced we have the semantics we want, rework the main evaluation infrastructure to match.

[robdockins]

One thing I notice about this semantics pretty quickly is that it is too strict in the sequence rearranging operations (split, join, transpose, etc.) E.g., the reference semantics is now also too strict on the examples from #640. These should probably all be reorganized as "reindexing" operations, such that the spine of the value returned depends only on the types, and individual values in the returned value force their inputs only when required. This basically does the eta-expansion steps that used to be pervasive locally instead.

[robdockins]

Some other strictness questions that arise: how strict should field, tuple and sequence updating be in the structure being updated? How strict should Logic class operations be over structured types?

[brianhuffman]

I took the liberty of pushing a commit to fix the typos I found.

[robdockins]

Regarding the strictness of record updates: it seems like this currently works in the main interpreter, so the reference semantics should make it work too:

recRecord : { x : Integer, y : Integer }
recRecord = r
  where
  r = { r | x = r.y, y = 3 }

[brianhuffman]

I'm getting an "unused imports" compiler warning:

src/Cryptol/Eval/Reference.lhs:25:3: warning: [-Wunused-imports]
    The import of ‘genericDrop, genericSplitAt’
    from module ‘Data.List’ is redundant
   |
25 | > import Data.List
   |   ^^^^^^^^^^^^^^^^...

[brianhuffman]

Concerning questions about strictness: My general opinion is that those choices often don't really matter much to Cryptol programmers, who are unlikely to bump into those corner cases. So we should just define the semantics for things in such a way that they're easy/natural to implement.

[robdockins]

Cryptol programmers end up writing recursive sequences quite a lot of different ways, in my experience, and they mostly expect them to work. I guess it would just feel a little weird if records didn't behave the same. E.g., currently all the following work both with the standard evaluator and this version of the reference evaluator and return [3 , 3], corresponding to the recursive record update above.

recSeq : [2]Integer
recSeq = xs
  where
  xs = updates xs [0,1] [xs@1, 3]

recSeq2 : [2]Integer
recSeq2 = xs
  where
  xs = (drop`{1} xs) # [3]

recSeq3 : [2]Integer
recSeq3 = xs
  where
  xs = update (error "asdf" # [3]) 0 (xs@1)

[brianhuffman]

While we're editing this file, it might be nice to do a bit of formatting to keep the code within 80 columns or so; right now there are some rather wide bits of code that shoot off the right side of the page in the generated pdf. (It looks like the right-margin of the text in the pdf lines up with about column 84 of the code blocks.)