Feature request: subterm evaluation

[msaaltink]

It would be useful to have a command that evaluated all subterms that do not involve variables. It fairly often comes up that I get ite terms, whether from indexing or from explicit if-terms in the Cryptol, where the tests can be evaluated independently of the variables in a goal. They can be as simple as 0 <= 1. These ite terms can interfere with rewriting proofs, and also make the goal bigger and less readable. Similarly, sometimes a proof involves a constant that is computed in two different ways, making terms look more different than they really are, and it would be useful to have a step that made the terms identical, or closer to identical.

For illustration, in

prove do {simplify (cryptol_ss ()); print_goal; z3; } {{ 0x5 ! 2 }}

the output is

      x@2 = Prelude.natToInt 2
    }
 in Prelude.EqTrue
      (Prelude.ite Prelude.Bool
         (Prelude.intLe (Prelude.natToInt 0) x@2)
         (Prelude.at 4 Prelude.Bool x@1 (Prelude.intToNat x@2))
         (Prelude.at 4 Prelude.Bool x@1 0))

where the intLe term could be evaluated to false (and then the ite term rewritten).

[weaversa]

I second that it would be nice to have some kind of constant propagation.

[brianhuffman]

This is a good idea, and it should be doable without too much trouble. More precisely, I think what you want is evaluation of all subterms that do not contain variables, and that have non-function types. I'll assign this to myself.

[msaaltink]

Non-function types would do it, and I can't think of why "evaluating" the functions would be useful. But I hope you mean to look inside those function-typed terms to look for subterms that may be evaluated, as in ite T condition function1 function2 where I'd hope that the condition might be evaluated.

There is one case where a sort of evaluation at a function type would be helpful, in something like [f0, f1, f2, ..., f20] @ 6 which could evaluate to f6. Maybe that's better done with rewriting, and I don't think I've ever used a construction like that anyway.

[brianhuffman]

I have a plan for how to implement this without too much work. In the saw-core evaluator, there is a function mkMemoClosed, which builds a memo table for only the closed subterms of the given term. I should be able to adapt that function to build a memo table for constant folding. I'll have a go at this next week.