Module Ltac2_plugin.Tac2ffi

Ltac2 FFI
type 'a repr
val repr_of : 'a repr -> 'a -> Tac2val.valexpr
val repr_to : 'a repr -> Tac2val.valexpr -> 'a
val make_repr : ('a -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'a) -> 'a repr
val 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.

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

WARNING these functions copy

val to_string : Tac2val.valexpr -> string
val string : string repr
val of_list : ('a -> Tac2val.valexpr) -> 'a list -> Tac2val.valexpr
val to_list : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a list
val list : 'a repr -> 'a list repr
val of_constr : EConstr.t -> Tac2val.valexpr
val to_constr : Tac2val.valexpr -> EConstr.t
val constr : EConstr.t repr
val of_matching_context : Constr_matching.context -> Tac2val.valexpr
val to_matching_context : Tac2val.valexpr -> Constr_matching.context
val matching_context : Constr_matching.context repr

Toplevel representation of OCaml exceptions. Invariant: no LtacError should be used with err.

val err : Exninfo.iexn repr
val exn : Exninfo.iexn repr
val of_exninfo : Exninfo.info -> Tac2val.valexpr
val to_exninfo : Tac2val.valexpr -> Exninfo.info
val exninfo : Exninfo.info repr
val of_ident : Names.Id.t -> Tac2val.valexpr
val to_ident : Tac2val.valexpr -> Names.Id.t
val ident : Names.Id.t repr
val of_closure : Tac2val.closure -> Tac2val.valexpr
val to_closure : Tac2val.valexpr -> Tac2val.closure
val closure : Tac2val.closure repr
val of_block : (int * Tac2val.valexpr array) -> Tac2val.valexpr
val to_block : Tac2val.valexpr -> int * Tac2val.valexpr array
val block : (int * Tac2val.valexpr array) repr
val of_array : ('a -> Tac2val.valexpr) -> 'a array -> Tac2val.valexpr
val to_array : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a array
val array : 'a repr -> 'a array repr
val of_tuple : Tac2val.valexpr array -> Tac2val.valexpr
val to_tuple : Tac2val.valexpr -> Tac2val.valexpr array
val of_pair : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('a * 'b) -> Tac2val.valexpr
val to_pair : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> Tac2val.valexpr -> 'a * 'b
val pair : 'a repr -> 'b repr -> ('a * 'b) repr
val of_triple : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('c -> Tac2val.valexpr) -> ('a * 'b * 'c) -> Tac2val.valexpr
val to_triple : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> (Tac2val.valexpr -> 'c) -> Tac2val.valexpr -> 'a * 'b * 'c
val triple : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr
val of_option : ('a -> Tac2val.valexpr) -> 'a option -> Tac2val.valexpr
val to_option : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a option
val option : 'a repr -> 'a option repr
val of_evar : Evar.t -> Tac2val.valexpr
val to_evar : Tac2val.valexpr -> Evar.t
val evar : Evar.t repr
val of_pp : Pp.t -> Tac2val.valexpr
val to_pp : Tac2val.valexpr -> Pp.t
val pp : Pp.t repr
val of_transparent_state : TransparentState.t -> Tac2val.valexpr
val to_transparent_state : Tac2val.valexpr -> TransparentState.t
val transparent_state : TransparentState.t repr
val of_pretype_flags : Pretyping.inference_flags -> Tac2val.valexpr
val to_pretype_flags : Tac2val.valexpr -> Pretyping.inference_flags
val pretype_flags : Pretyping.inference_flags repr
val expected_type : Pretyping.typing_constraint repr
val of_ind_data : ind_data -> Tac2val.valexpr
val to_ind_data : Tac2val.valexpr -> ind_data
val ind_data : ind_data repr
val of_inductive : Names.inductive -> Tac2val.valexpr
val to_inductive : Tac2val.valexpr -> Names.inductive
val inductive : Names.inductive repr
val of_constant : Names.Constant.t -> Tac2val.valexpr
val to_constant : Tac2val.valexpr -> Names.Constant.t
val constant : Names.Constant.t repr
val of_constructor : Names.constructor -> Tac2val.valexpr
val to_constructor : Tac2val.valexpr -> Names.constructor
val constructor : Names.constructor repr
val of_projection : Names.Projection.t -> Tac2val.valexpr
val to_projection : Tac2val.valexpr -> Names.Projection.t
val projection : Names.Projection.t repr
val of_qvar : Sorts.QVar.t -> Tac2val.valexpr
val to_qvar : Tac2val.valexpr -> Sorts.QVar.t
val qvar : Sorts.QVar.t repr
val of_binder : binder -> Tac2val.valexpr
val to_binder : Tac2val.valexpr -> binder
val binder : binder repr
val instance : EConstr.EInstance.t repr
val of_reference : Names.GlobRef.t -> Tac2val.valexpr
val to_reference : Tac2val.valexpr -> Names.GlobRef.t
val reference : Names.GlobRef.t repr
val of_ext : 'a Tac2dyn.Val.tag -> 'a -> Tac2val.valexpr
val to_ext : 'a Tac2dyn.Val.tag -> Tac2val.valexpr -> 'a
val repr_ext : 'a Tac2dyn.Val.tag -> 'a repr
val open_ : (Names.KerName.t * Tac2val.valexpr array) repr
val of_uint63 : Uint63.t -> Tac2val.valexpr
val to_uint63 : Tac2val.valexpr -> Uint63.t
val uint63 : Uint63.t repr
val of_float : Float64.t -> Tac2val.valexpr
val to_float : Tac2val.valexpr -> Float64.t
val float : Float64.t repr
val of_pstring : Pstring.t -> Tac2val.valexpr
val to_pstring : Tac2val.valexpr -> Pstring.t
val pstring : Pstring.t repr
type ('a, 'b) fun1
val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
val to_fun1 : 'a repr -> 'b repr -> Tac2val.valexpr -> ('a, 'b) fun1
val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
val valexpr : Tac2val.valexpr repr

Exception

exception LtacError of Names.KerName.t * Tac2val.valexpr array

Ltac2-defined exceptions seen from OCaml side