Add saw-script functions term_eval and term_eval_unint.

[brianhuffman]

These are analogous to the goal_eval and goal_eval_unint proof
tactics, but instead of proof goals they work on arbitrary terms.

[brianhuffman]

We might want to reconsider the naming of these operations.

[RyanGlScott]

Landing this would address one aspect of #1788.

[sauclovian-g]

I think the conclusion is that we want this functionality, and I see no reason to start over rather than taking this code. So I'm going to see if it's still buildable.

[sauclovian-g]

Answer: it wasn't, but was easily fixed. I'm going to un-draft it, I think, at least until we identify any reasons it's not ready. @RyanGlScott do you have any examples we could add into the test suite? I am pretty sure I understand what it's doing and why but concocting a simple example involves too many things I'm not yet quite on top of.

[RyanGlScott]

Two potential test cases that come to mind:

1. The test case from Bitblasting of multipliers differs wildly between Cryptol and SAW #1788. But upon closer inspection, the original problem from Bitblasting of multipliers differs wildly between Cryptol and SAW #1788 can no longer be reproduced in modern SAW, as this was fixed in a different way in write_aig: Normalize symmetry in multiplication #1833. As such, this is no longer a good test case...

2. The test case from muxBVal: VInt (0, 1) #1436. This can still be reproduced in modern SAW:

   // test.cry
   hasRepeat : {a, b} (fin a, a >= 2, Eq b) => [a]b -> b -> Integer -> Bit
   hasRepeat xs b num = out == num
     where
       out = foldl (\a x -> if a == num then num
                             | x == b   then a+1
                            else 0) 0 xs
   

   // test.saw
   import "test.cry";
   write_aig "test.aig" {{ \(x : [10]) -> hasRepeat x True 2 }};
   

   $ ./bin/saw test.saw
   [14:39:36.840] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw"
   [14:39:36.890] Stack trace:
   "write_aig" (/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:3:1-3:10)
   muxBVal: VInt (1,0)
   
   

   In principle, one ought to be able to fix this by adding a use of term_eval, i.e.,

   // test.saw
   import "test.cry";
   write_aig "test.aig" (term_eval {{ \(x : [10]) -> hasRepeat x True 2 }});
   

   Unfortunately, that doesn't work either:

   $ ./bin/saw test.saw
   [14:40:24.864] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw"
   [14:40:24.916] Stack trace:
   "term_eval" (/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw:3:23-3:32)
   rebuildTerm VFun
   
   

   Ideally, we would teach rebuildTerm how to look underneath lambdas, as I imagine that that will be a pretty common use case for this feature. I don't have time to look at this right now, but I can't imagine it would be too difficult, given that other Term-manipulation primitives also look underneath lambdas (e.g., normalize_term).