package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ltac2_plugin.Tac2ffiSource

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

    Immediate integers

    *)
  2. | ValBlk of Tac2expr.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

    *)
  7. | ValUint63 of Uint63.t
    (*

    Primitive integers

    *)
  8. | ValFloat of Float64.t
    (*

    Primitive floats

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct