Fix the SAWScript interpreter's environment handling

[sauclovian-g]

This has been a target for months. But it's not the end; now that it's possible to reason about what the interpreter's actually doing with its environments, it becomes possible to fix the interaction between the interpreter and the typechecker, which is also accursed. No rest for the wicked, or something.

Closes #1646, and possibly others, as the bizarre implementation has given rise to all manner of weirdness.

[sauclovian-g]

force-push was: left something off at the last minute before I pushed. :-|

[sauclovian-g]

If anyone's wondering whether git's inability to track renames reliably is real, this right here is evidence. I renamed both the .saw and .good files...

[sauclovian-g]

There's also something horrible going on with the Cryptol environment that's broken a bunch of tests.

I think what's happening is:

• the old code added to the Cryptol environment at extendEnv time; the new code does as well, but without the LocalEnv stuff this happens sooner and more aggressively now;
• the Cryptol environment doesn't scope, which is a known issue;
• there's therefore more opportunities for a nested function to add stuff to the Cryptol environment that blitzes something already there and causes problems in the caller.

At least the first failure in test0043_invariant_3 seems to have this pattern: one function binds a local n, then it calls a function with an argument n, and the argument overwrites the Cryptol binding for the original n and later references get the wrong thing and fail.

With the various woolly ways the LocalEnv was getting manipulated it's quite likely that there have always been ways to step on this rake and it's just easier now.

I don't want to try fixing the scoping of the Cryptol environment in this pull request, because it's not trivial and may need design discussions to do correctly, so I think I'm going to hack up something ugly as a stopgap.

[sauclovian-g]

This push fixes the oversights, the miscellaneous suggestions above, and the ScopedMap haddocks (I actually built the haddocks for a change and they render ok now) ... but not the Cryptol environment problem yet.

[sauclovian-g]

So, it's even more broken that way. It'll proabably be Monday or Tuesday evening before I can get back to this...

[sauclovian-g]

force-push: seems it needed to be rebased over or merged with #2593 for the CI to run. This also crossed some other recent merges.

If the current batch of changes works (or, likely, even if it doesn't) I'm going to retcon the whole patchset anyway as it needs some attention to naming and some factoring out of common logic in saw-server and in the REPL code.

[sauclovian-g]

Foo.

[21:19:52.086] Attempted to register the following name twice: cryptol:thm#5921

FAIL (1.96s)
    intTests/IntegrationTest.hs:185:
    expected: ExitSuccess
     but got: ExitFailure 2
    Use -p '/test_ecdsa/' to rerun this test only.

(that's the behavior when the lack of SAWCore scoping bites)

I'm inclined to rejigger that test to avoid the problem, instead of committing to hack around it right now. Any objections?

[RyanGlScott]

I assume that this happens because there are multiple inner scopes that each define something local named thm? If so, then I would be fine with working around it, perhaps by renaming the thms to avoid "conflicts".

[sauclovian-g]

Yes; it turns out there's twelve of them, of the form let {{ thm x = ... }}; let t = unfold_term ["thm"] {{ thm }}; whereas other things in the file just do let t = {{ \x -> ... }}. I am going to try changing them all to the latter format, since that ought to work perfectly well.

[RyanGlScott]

It took quite a bit of huffing and puffing, but it looks like you've finally patched things up. I'm content to land this and make further improvements later.

[sauclovian-g]

Ok, now it at least works. Next step is to whip it into committable shape...

[sauclovian-g]

(that is: can definitely make further improvements later, but the last few commits were hacks and ideally the commits that eventually get merged should all build and pass tests)

[sauclovian-g]

This force-push rearranges commits and improves commit messages, with no net resultant difference.

[sauclovian-g]

This force-push tidies up the Cryptol environment changes and moves them to before the main environment cleanup commit, which allows them to be their own commit without incurring a broken intermediate state.

Changes from the previous version (since there's no way to put this in the commit messages):

Naming:

• Use CryptolEnvStack instead of CryptolScopeStack as the type name for the stack of environments; then we have CryptolEnv and CryptolEnvStack.
• The canonical variable name for a CryptolEnv will be ce or cenv.
• The canonical name for a CryptolEnvStack will be cryenvs.

Accessors:

• Because saw-erver and the REPL both use TopLevelRW from a monad context that isn't TopLevel, provide an additional set of Cryptol environment accessors that work on an explicit TopLevelRW. Use these to avoid exposing exactly how the Cryptol environment appears in TopLevelRW.

Simplify:

• Use CryptolEnvStack CryptolEnv [CryptolEnv] instead of an explicit NonEmpty; we don't use any NonEmpty ops on the NonEmpty and this avoids the need to import the :| operator all over the place.
• Use the new accessors.
• Tidy some of the code.

[sauclovian-g]

This force-push rebases on master.

[sauclovian-g]

This should be ready to go for real; it is probably worth at least glancing at the tidy-up force-push diff in case I did something stoopid.

[sauclovian-g]

Also, this closes #2304 and #2243, in addition to #1646, but I can't get the issue-linking widget to recognize that they exist.