Module Ltac2_plugin.Tac2ffiSource

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 Coq 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

    *)
Sourcetype 'a arity
Sourceval arity_suc : 'a arity -> (valexpr -> 'a) arity
Sourceval mk_closure : 'v arity -> 'v -> closure
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

Sourcemodule Valexpr : sig ... end
Ltac2 FFI
Sourcetype 'a repr
Sourceval repr_of : 'a repr -> 'a -> valexpr
Sourceval repr_to : 'a repr -> valexpr -> 'a
Sourceval make_repr : ('a -> valexpr) -> (valexpr -> 'a) -> 'a repr
Sourceval map_repr : ('a -> 'b) -> ('b -> 'a) -> 'a repr -> 'b repr

These functions allow to convert back and forth between OCaml and Ltac2 data representation. The to_* functions raise an anomaly whenever the data has not expected shape.

Sourceval of_unit : unit -> valexpr
Sourceval to_unit : valexpr -> unit
Sourceval unit : unit repr
Sourceval of_int : int -> valexpr
Sourceval to_int : valexpr -> int
Sourceval int : int repr
Sourceval of_bool : bool -> valexpr
Sourceval to_bool : valexpr -> bool
Sourceval bool : bool repr
Sourceval of_char : char -> valexpr
Sourceval to_char : valexpr -> char
Sourceval char : char repr
Sourceval of_bytes : Stdlib.Bytes.t -> valexpr
Sourceval to_bytes : valexpr -> Stdlib.Bytes.t
Sourceval bytes : Stdlib.Bytes.t repr
Sourceval of_string : string -> valexpr

WARNING these functions copy

Sourceval to_string : valexpr -> string
Sourceval string : string repr
Sourceval of_list : ('a -> valexpr) -> 'a list -> valexpr
Sourceval to_list : (valexpr -> 'a) -> valexpr -> 'a list
Sourceval list : 'a repr -> 'a list repr
Sourceval of_constr : EConstr.t -> valexpr
Sourceval to_constr : valexpr -> EConstr.t
Sourceval constr : EConstr.t repr
Sourceval of_exn : Exninfo.iexn -> valexpr
Sourceval to_exn : valexpr -> Exninfo.iexn
Sourceval of_ident : Names.Id.t -> valexpr
Sourceval to_ident : valexpr -> Names.Id.t
Sourceval of_closure : closure -> valexpr
Sourceval to_closure : valexpr -> closure
Sourceval closure : closure repr
Sourceval of_block : (int * valexpr array) -> valexpr
Sourceval to_block : valexpr -> int * valexpr array
Sourceval block : (int * valexpr array) repr
Sourceval of_array : ('a -> valexpr) -> 'a array -> valexpr
Sourceval to_array : (valexpr -> 'a) -> valexpr -> 'a array
Sourceval array : 'a repr -> 'a array repr
Sourceval of_tuple : valexpr array -> valexpr
Sourceval to_tuple : valexpr -> valexpr array
Sourceval of_pair : ('a -> valexpr) -> ('b -> valexpr) -> ('a * 'b) -> valexpr
Sourceval to_pair : (valexpr -> 'a) -> (valexpr -> 'b) -> valexpr -> 'a * 'b
Sourceval pair : 'a repr -> 'b repr -> ('a * 'b) repr
Sourceval of_triple : ('a -> valexpr) -> ('b -> valexpr) -> ('c -> valexpr) -> ('a * 'b * 'c) -> valexpr
Sourceval to_triple : (valexpr -> 'a) -> (valexpr -> 'b) -> (valexpr -> 'c) -> valexpr -> 'a * 'b * 'c
Sourceval triple : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr
Sourceval of_option : ('a -> valexpr) -> 'a option -> valexpr
Sourceval to_option : (valexpr -> 'a) -> valexpr -> 'a option
Sourceval option : 'a repr -> 'a option repr
Sourceval of_evar : Evar.t -> valexpr
Sourceval to_evar : valexpr -> Evar.t
Sourceval evar : Evar.t repr
Sourceval of_pp : Pp.t -> valexpr
Sourceval to_pp : valexpr -> Pp.t
Sourceval pp : Pp.t repr
Sourceval of_constant : Names.Constant.t -> valexpr
Sourceval to_constant : valexpr -> Names.Constant.t
Sourceval of_reference : Names.GlobRef.t -> valexpr
Sourceval to_reference : valexpr -> Names.GlobRef.t
Sourceval reference : Names.GlobRef.t repr
Sourceval of_ext : 'a Tac2dyn.Val.tag -> 'a -> valexpr
Sourceval to_ext : 'a Tac2dyn.Val.tag -> valexpr -> 'a
Sourceval repr_ext : 'a Tac2dyn.Val.tag -> 'a repr
Sourceval of_open : (Names.KerName.t * valexpr array) -> valexpr
Sourceval to_open : valexpr -> Names.KerName.t * valexpr array
Sourceval open_ : (Names.KerName.t * valexpr array) repr
Sourceval of_uint63 : Uint63.t -> valexpr
Sourceval to_uint63 : valexpr -> Uint63.t
Sourceval uint63 : Uint63.t repr
Sourceval of_float : Float64.t -> valexpr
Sourceval to_float : valexpr -> Float64.t
Sourceval float : Float64.t repr
Sourcetype ('a, 'b) fun1
Sourceval app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
Sourceval to_fun1 : 'a repr -> 'b repr -> valexpr -> ('a, 'b) fun1
Sourceval fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
Sourceval valexpr : valexpr repr
Dynamic tags

Toplevel representation of OCaml exceptions. Invariant: no LtacError should be put into a value with tag val_exn.

Closures

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.

Exception

Sourceexception LtacError of Names.KerName.t * valexpr array

Ltac2-defined exceptions seen from OCaml side