Module Ltac2_plugin.Tac2valSource

Toplevel values
Dynamic semantics

Values are represented in a way similar to OCaml, i.e. they contrast immediate integers (integers, constructors without arguments) and structured blocks (tuples, arrays, constructors with arguments), as well as a few other base cases, namely closures, strings, named constructors, and dynamic type coming from the Rocq implementation.

Sourcetype tag = int
Sourcetype closure
Sourcetype valexpr =
  1. | ValInt of int
    (*

    Immediate integers

    *)
  2. | ValBlk of tag * valexpr array
    (*

    Structured blocks

    *)
  3. | ValStr of Stdlib.Bytes.t
    (*

    Strings

    *)
  4. | ValCls of closure
    (*

    Closures

    *)
  5. | ValOpn of Names.KerName.t * valexpr array
    (*

    Open constructors

    *)
  6. | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
    (*

    Arbitrary data

    *)
Sourcemodule Valexpr : sig ... end

Closures

Sourcetype 'a arity
Sourceval arity_suc : 'a arity -> (valexpr -> 'a) arity
Sourceval mk_closure : 'v arity -> 'v -> closure

The arrows in 'v should be pure. Use tclLIFT or do tclUNIT () >>= fun () -> f args when you need effects.

Sourceval mk_closure_val : 'v arity -> 'v -> valexpr

Composition of mk_closure and ValCls

Sourceval annotate_closure : Tac2expr.frame -> closure -> closure

The closure must not be already annotated

Sourceval purify_closure : 'v arity -> 'v -> 'v

For internal use (Tac2externals). Wraps the applications of the 'v argument to make it pure.

Sourceval to_closure : valexpr -> closure

Given a closure, apply it to some arguments. Handling of argument mismatches is done automatically, i.e. in case of over or under-application.

Sourceval apply_val : valexpr -> valexpr list -> valexpr Proofview.tactic

Composition of to_closure and apply

Sourceval abstract : int -> (valexpr list -> valexpr Proofview.tactic) -> closure

Turn a fixed-arity function into a closure. The inner function is guaranteed to be applied to a list whose size is the integer argument.