package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. Ltac2 FFI
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/ltac2_plugin/Ltac2_plugin/Tac2ffi/index.html

Module Ltac2_plugin.Tac2ffiSource

Ltac2 FFI
Sourcetype 'a repr
Sourceval repr_of : 'a repr -> 'a -> Tac2val.valexpr
Sourceval repr_to : 'a repr -> Tac2val.valexpr -> 'a
Sourceval make_repr : ('a -> Tac2val.valexpr) -> (Tac2val.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 -> Tac2val.valexpr
Sourceval to_unit : Tac2val.valexpr -> unit
Sourceval unit : unit repr
Sourceval of_int : int -> Tac2val.valexpr
Sourceval to_int : Tac2val.valexpr -> int
Sourceval int : int repr
Sourceval of_bool : bool -> Tac2val.valexpr
Sourceval to_bool : Tac2val.valexpr -> bool
Sourceval bool : bool repr
Sourceval of_char : char -> Tac2val.valexpr
Sourceval to_char : Tac2val.valexpr -> char
Sourceval char : char repr
Sourceval of_bytes : Stdlib.Bytes.t -> Tac2val.valexpr
Sourceval to_bytes : Tac2val.valexpr -> Stdlib.Bytes.t
Sourceval bytes : Stdlib.Bytes.t repr
Sourceval of_string : string -> Tac2val.valexpr

WARNING these functions copy

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

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

Sourceval exninfo : Exninfo.info repr
Sourceval of_result : ('a -> Tac2val.valexpr) -> ('a, Exninfo.iexn) Stdlib.result -> Tac2val.valexpr
Sourceval to_result : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> ('a, Exninfo.iexn) Stdlib.result
Sourceval result : 'a repr -> ('a, Exninfo.iexn) Stdlib.result repr
Sourcetype ('a, 'b) fun1 = 'a -> 'b Proofview.tactic
Sourceval of_fun1 : (Tac2val.valexpr -> 'a) -> ('b -> Tac2val.valexpr) -> ('a, 'b) fun1 -> Tac2val.valexpr
Sourceval to_fun1 : ('a -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'b) -> Tac2val.valexpr -> ('a, 'b) fun1
Sourceval fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr
Sourceval thunk : 'a repr -> (unit, 'a) fun1 repr
Sourcetype ('a, 'b, 'c) fun2 = 'a -> 'b -> 'c Proofview.tactic
Sourceval of_fun2 : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> ('c -> Tac2val.valexpr) -> ('a, 'b, 'c) fun2 -> Tac2val.valexpr
Sourceval to_fun2 : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> (Tac2val.valexpr -> 'c) -> Tac2val.valexpr -> ('a, 'b, 'c) fun2
Sourceval fun2 : 'a repr -> 'b repr -> 'c repr -> ('a, 'b, 'c) fun2 repr
Sourceval of_block : (int * Tac2val.valexpr array) -> Tac2val.valexpr
Sourceval to_block : Tac2val.valexpr -> int * Tac2val.valexpr array
Sourceval block : (int * Tac2val.valexpr array) repr
Sourceval of_array : ('a -> Tac2val.valexpr) -> 'a array -> Tac2val.valexpr
Sourceval to_array : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a array
Sourceval array : 'a repr -> 'a array repr
Sourceval of_tuple : Tac2val.valexpr array -> Tac2val.valexpr
Sourceval to_tuple : Tac2val.valexpr -> Tac2val.valexpr array
Sourceval of_pair : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('a * 'b) -> Tac2val.valexpr
Sourceval to_pair : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> Tac2val.valexpr -> 'a * 'b
Sourceval pair : 'a repr -> 'b repr -> ('a * 'b) repr
Sourceval of_triple : ('a -> Tac2val.valexpr) -> ('b -> Tac2val.valexpr) -> ('c -> Tac2val.valexpr) -> ('a * 'b * 'c) -> Tac2val.valexpr
Sourceval to_triple : (Tac2val.valexpr -> 'a) -> (Tac2val.valexpr -> 'b) -> (Tac2val.valexpr -> 'c) -> Tac2val.valexpr -> 'a * 'b * 'c
Sourceval triple : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr
Sourceval of_option : ('a -> Tac2val.valexpr) -> 'a option -> Tac2val.valexpr
Sourceval to_option : (Tac2val.valexpr -> 'a) -> Tac2val.valexpr -> 'a option
Sourceval option : 'a repr -> 'a option repr
Sourceval of_evar : Evar.t -> Tac2val.valexpr
Sourceval to_evar : Tac2val.valexpr -> Evar.t
Sourceval evar : Evar.t repr
Sourceval of_rewstrategy : Rewrite.strategy -> Tac2val.valexpr
Sourceval to_rewstrategy : Tac2val.valexpr -> Rewrite.strategy
Sourceval rewstrategy : Rewrite.strategy repr
Sourceval pp : Pp.t repr
Sourceval of_transparent_state : TransparentState.t -> Tac2val.valexpr
Sourceval to_transparent_state : Tac2val.valexpr -> TransparentState.t
Sourceval transparent_state : TransparentState.t repr
Sourceval of_ind_data : ind_data -> Tac2val.valexpr
Sourceval to_ind_data : Tac2val.valexpr -> ind_data
Sourceval ind_data : ind_data repr
Sourceval inductive : Names.inductive repr
Sourceval constructor : Names.constructor repr
Sourceval of_binder : binder -> Tac2val.valexpr
Sourceval to_binder : Tac2val.valexpr -> binder
Sourceval binder : binder repr
Sourceval reference : Names.GlobRef.t repr
Sourceval of_ext : 'a Tac2dyn.Val.tag -> 'a -> Tac2val.valexpr
Sourceval to_ext : 'a Tac2dyn.Val.tag -> Tac2val.valexpr -> 'a
Sourceval repr_ext : 'a Tac2dyn.Val.tag -> 'a repr
Sourceval open_ : (Names.KerName.t * Tac2val.valexpr array) repr
Sourceval of_uint63 : Uint63.t -> Tac2val.valexpr
Sourceval to_uint63 : Tac2val.valexpr -> Uint63.t
Sourceval uint63 : Uint63.t repr
Sourceval float : Float64.t repr
Sourceval of_pstring : Pstring.t -> Tac2val.valexpr
Sourceval to_pstring : Tac2val.valexpr -> Pstring.t
Sourceval pstring : Pstring.t repr

Exception

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

Ltac2-defined exceptions seen from OCaml side