saw-core: Move 'Variable' constructor from FlatTermF to TermF.

[brianhuffman]

With the plan to move away from de Bruijn indices for variable binding, the 'Variable' constructor will play a more specialized role, and so it makes more sense to be out of FlatTermF.

[brianhuffman]

There are a few regression test failures. Maybe this has to do with putting scWhnf in the wrong place in a TypeInfer instance in SCTypeCheck? I'll look into it.

[sauclovian-g]

It's odd that all the failures are specifically timeouts.

[brianhuffman]

Not all of the failures are timeouts: test_hoist_ifs_in_goal gets a real failure. I ran it locally, and here's the output:

[20:25:00.636] Loading file "test.saw"
[20:25:00.684] WARNING: assuming goal prove_print is unsat
[20:25:00.689] Run-time error: encountered call to the Cryptol 'error' function: undefined

Very interesting! Now I'm thinking that I made something slightly more strict than before. I'll read over the diffs carefully and try to find something. But the business with cryptol error makes me think there's another latent bug that I just uncovered.

[sauclovian-g]

Hmm, apparently I can't read. :-|

but yes, that's definitely plausible, could definitely result in timeouts...

[brianhuffman]

It turns out I made a couple of mistakes in Rewriter.doHoistIfs and SharedTerm.instantiateLocalVars. I'll see if that taking care of those fixes the problem.

[brianhuffman]

Investigating test_hoist_ifs_in_goal, I can see that there are differences in the behavior of the rewriter on this branch. I must have broken something in the matching algorithm.

[brianhuffman]

I found it: I needed to add a case to the alphaEquiv function. There was no incomplete pattern-match warning because alphaEquiv matches on two constructors at once, and uses a wildcard pattern to cover all the different-constructor cases. We should think about whether there's a better way to do this.

[sauclovian-g]

For things like that I'll often leave a collection of cases at the bottom:

-- Make sure the compiler warns if new constructors appear and we forget to
-- add cases
  :
termf (Pi _) _ = False
termf (LocalVar _) _ = False
termf (Constant _) _ = False
termf (Variable _) _ = False