Support for local state in meta programs

[aseemr]

This PR adds support for local state in metaprograms. In particular, it adds three primitives:

(** The following primitives provide support for local state
    during execution of a tactic.
    The local state is monotonic, it is not
    reverted when the tactic backtracks (using catch e.g.)
 *)
val alloc (#a:Type) (x:a) : Tac (tref a)
val read (#a:Type) (r:tref a) : Tac a
val write (#a:Type) (r:tref a) (x:a) : Tac unit

Metaprograms can use these to maintain local state during execution.

Under the hood we use native OCaml heap to allocate these references.

[mtzguido]

Hi Aseem, this looks good to me. I have one question though.

In interpreted mode, we use e_any, so the reference points to a term, even if it's a tref int or whatever. But in native tactics, a tref int will be exactly ref int, and use the native alloc/read/write. So they cannot interoperate, right? A reference can only be used in the "mode" it's created.

I don't think it's terrible. We could fix this by deprecating e_any and instead trying to generate an embedding for the type of the reference, but that requires some plumbing.

[mtzguido]

It may be better to "thunk" these to prevent them from reducing before being applied to a proofstate, like so:

let alloc (x:'a) : tac (tref 'a) =
  idtac;!
  ret (BU.mk_ref x)
let read (r:tref 'a) : tac 'a =
  idtac;!
  ret (!r)
let write (r:tref 'a) (x:'a) : tac unit =
  idtac;!
  r := x;
  ret ()

[mtzguido]

Come to think of it, since there is no embedding for tref, I don't think references can cross the native/interpreted boundary...

[TWal]

Could this be used to store state across meta-program calls, e.g. to memoize typeclass resolution?
The example don't showcase this right now.

[nikswamy]

What's the status of this? I would find it convenient to use a bit of local state in the Pulse checker.

[mtzguido]

I think we can merge this. I updated it to the current master and pushed to this branch.