tactics: ctrl_rewrite: perform rewrite under arrows

[amosr]

I wanted to perform rewrites on the environment, but when I reverted the environment it wouldn't rewrite. It looks like ctrl_rewrite was missing part of the implementation.

I implemented rewrite for Total and GTotal computations, but it wasn't clear to me what to do for effectful computations. (I assume that they won't occur in reverts, anyway.) How often does this case occur - should it perhaps print a warning?

[amosr]

no good...

let id (a: Type) (x: a) = x

let test = assert (let id (a: Type) (x: a) = x in id Type0 True)
      by (pointwise (fun () -> dump "outer"; trefl ()))

  - Tactic failed
  - "uncaught exception: Failure("Impossible")"
  - See also FStar.Tactics.V2.Derived.fst(239,2-239,24)

[amosr]

Hmm, actually I think the above "Impossible" error is a pre-existing bug. I can reproduce it on master, and on a six-month-old master gives a different, perhaps more helpful error message:

tests/tactics/RewriteInArrow.fst(12,13-12,19): (Error 228) user tactic failed: `Violation of locally nameless convention: a` (see also FStar.Tactics.Derived.fst(228,2-228,24))
1 error was reported (see above)

[amosr]

Superseded by #3104