Quelle tac2ffi.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Names
open EConstr
open Tac2dyn
open Tac2val

(** {5 Ltac2 FFI} *)

type 'a repr

val repr_of : 'a repr -> 'a -> valexpr
val repr_to : 'a repr -> valexpr -> 'a

val make_repr : ('a -> valexpr) -> (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 -> valexpr
val to_unit : valexpr -> unit
val unit : unit repr

val of_int : int -> valexpr
val to_int : valexpr -> int
val int : int repr

val of_bool : bool -> valexpr
val to_bool : valexpr -> bool
val bool : bool repr

val of_char : char -> valexpr
val to_char : valexpr -> char
val char : char repr

val of_bytes : Bytes.t -> valexpr
val to_bytes : valexpr -> Bytes.t
val bytes : Bytes.t repr

(** WARNING these functions copy *)
val of_string : string -> valexpr
val to_string : valexpr -> string
val string : string repr

val of_list : ('a -> valexpr) -> 'a list -> valexpr
val to_list : (valexpr -> 'a) -> valexpr -> 'a list
val list : 'a repr -> 'a list repr

val of_constr : EConstr.t -> valexpr
val to_constr : valexpr -> EConstr.t
val constr : EConstr.t repr

val of_matching_context : Constr_matching.context -> valexpr
val to_matching_context : valexpr -> Constr_matching.context
val matching_context : Constr_matching.context repr

val of_preterm : Ltac_pretype.closed_glob_constr -> valexpr
val to_preterm : valexpr -> Ltac_pretype.closed_glob_constr
val preterm : Ltac_pretype.closed_glob_constr repr

val of_cast : Constr.cast_kind -> valexpr
val to_cast : valexpr -> Constr.cast_kind
val cast : Constr.cast_kind repr

(** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]
    should be used with [err]. *)
val of_err : Exninfo.iexn -> valexpr
val to_err : valexpr -> Exninfo.iexn
val err : Exninfo.iexn repr

val of_exn : Exninfo.iexn -> valexpr
val to_exn : valexpr -> Exninfo.iexn
val exn : Exninfo.iexn repr

val of_exninfo : Exninfo.info -> valexpr
val to_exninfo : valexpr -> Exninfo.info
val exninfo : Exninfo.info repr

val of_result : ('a -> valexpr) -> ('a, Exninfo.iexn) result -> valexpr
val to_result : (valexpr -> 'a) -> valexpr -> ('a, Exninfo.iexn) result
val result : 'a repr -> ('a, Exninfo.iexn) result repr

val of_ident : Id.t -> valexpr
val to_ident : valexpr -> Id.t
val ident : Id.t repr

val of_closure : closure -> valexpr
val to_closure : valexpr -> closure
val closure : closure repr

type ('a, 'b) fun1 = 'a -> 'b Proofview.tactic

val of_fun1 : (valexpr -> 'a) -> ('b -> valexpr) -> ('a, 'b) fun1 -> valexpr
val to_fun1 : ('a -> valexpr) -> (valexpr -> 'b) -> valexpr -> ('a, 'b) fun1
val fun1 : 'a repr -> 'b repr -> ('a, 'b) fun1 repr

val thunk : 'a repr -> (unit,'a) fun1 repr

type ('a, 'b, 'c) fun2 = 'a -> 'b -> 'c Proofview.tactic

val of_fun2 : (valexpr -> 'a) -> (valexpr -> 'b) -> ('c -> valexpr) -> ('a, 'b, 'c) fun2 -> valexpr
val to_fun2 : ('a -> valexpr) -> ('b -> valexpr) -> (valexpr -> 'c) -> valexpr -> ('a, 'b, 'c) fun2
val fun2 : 'a repr -> 'b repr -> 'c repr -> ('a, 'b, 'c) fun2 repr

val of_block : (int * valexpr array) -> valexpr
val to_block : valexpr -> (int * valexpr array)
val block : (int * valexpr array) repr

val of_array : ('a -> valexpr) -> 'a array -> valexpr
val to_array : (valexpr -> 'a) -> valexpr -> 'a array
val array : 'a repr -> 'a array repr

val of_tuple : valexpr array -> valexpr
val to_tuple : valexpr -> valexpr array

val of_pair : ('a -> valexpr) -> ('b -> valexpr) -> 'a * 'b -> valexpr
val to_pair : (valexpr -> 'a) -> (valexpr -> 'b) -> valexpr -> 'a * 'b
val pair : 'a repr -> 'b repr -> ('a * 'b) repr

val of_triple : ('a -> valexpr) -> ('b -> valexpr) -> ('c -> valexpr) -> 'a * 'b * 'c -> valexpr
val to_triple : (valexpr -> 'a) -> (valexpr -> 'b) -> (valexpr -> 'c) -> valexpr -> 'a * 'b * 'c
val triple : 'a repr -> 'b repr -> 'c repr -> ('a * 'b * 'c) repr

val of_option : ('a -> valexpr) -> 'a option -> valexpr
val to_option : (valexpr -> 'a) -> valexpr -> 'a option
val option : 'a repr -> 'a option repr

val of_pattern : Pattern.constr_pattern -> valexpr
val to_pattern : valexpr -> Pattern.constr_pattern
val pattern : Pattern.constr_pattern repr

val of_evar : Evar.t -> valexpr
val to_evar : valexpr -> Evar.t
val evar : Evar.t repr

val of_sort : ESorts.t -> valexpr
val to_sort : valexpr -> ESorts.t
val sort : ESorts.t repr

val of_reduction : Redexpr.red_expr -> valexpr
val to_reduction : valexpr -> Redexpr.red_expr
val reduction : Redexpr.red_expr repr

val of_rewstrategy : Rewrite.strategy -> valexpr
val to_rewstrategy : valexpr -> Rewrite.strategy
val rewstrategy : Rewrite.strategy repr

val of_pp : Pp.t -> valexpr
val to_pp : valexpr -> Pp.t
val pp : Pp.t repr

val of_transparent_state : TransparentState.t -> valexpr
val to_transparent_state : valexpr -> TransparentState.t
val transparent_state : TransparentState.t repr

val of_pretype_flags : Pretyping.inference_flags -> valexpr
val to_pretype_flags : valexpr -> Pretyping.inference_flags
val pretype_flags : Pretyping.inference_flags repr

val of_expected_type : Pretyping.typing_constraint -> valexpr
val to_expected_type : valexpr -> Pretyping.typing_constraint
val expected_type : Pretyping.typing_constraint repr

type ind_data = (Names.Ind.t * Declarations.mutual_inductive_body)

val of_ind_data : ind_data -> valexpr
val to_ind_data : valexpr -> ind_data
val ind_data : ind_data repr

val of_inductive : inductive -> valexpr
val to_inductive : valexpr -> inductive
val inductive : inductive repr

val of_constant : Constant.t -> valexpr
val to_constant : valexpr -> Constant.t
val constant : Constant.t repr

val of_constructor : constructor -> valexpr
val to_constructor : valexpr -> constructor
val constructor : constructor repr

val of_projection : Projection.t -> valexpr
val to_projection : valexpr -> Projection.t
val projection : Projection.t repr

val of_qvar : Sorts.QVar.t -> valexpr
val to_qvar : valexpr -> Sorts.QVar.t
val qvar : Sorts.QVar.t repr

val of_case : Constr.case_info -> valexpr
val to_case : valexpr -> Constr.case_info
val case : Constr.case_info repr

type binder = (Name.t EConstr.binder_annot * types)

val of_binder : binder -> valexpr
val to_binder : valexpr -> binder
val binder : binder repr

val of_instance : EConstr.EInstance.t -> valexpr
val to_instance : valexpr -> EConstr.EInstance.t
val instance : EConstr.EInstance.t repr

val of_reference : GlobRef.t -> valexpr
val to_reference : valexpr -> GlobRef.t
val reference : GlobRef.t repr

val of_ext : 'a Val.tag -> 'a -> valexpr
val to_ext : 'a Val.tag -> valexpr -> 'a
val repr_ext : 'a Val.tag -> 'a repr

val of_open : KerName.t * valexpr array -> valexpr
val to_open : valexpr -> KerName.t * valexpr array
val open_ : (KerName.t * valexpr array) repr

val of_free : Nameops.Fresh.t -> valexpr
val to_free : valexpr -> Nameops.Fresh.t
val free : Nameops.Fresh.t repr

val of_uint63 : Uint63.t -> valexpr
val to_uint63 : valexpr -> Uint63.t
val uint63 : Uint63.t repr

val of_float : Float64.t -> valexpr
val to_float : valexpr -> Float64.t
val float : Float64.t repr

val of_pstring : Pstring.t -> valexpr
val to_pstring : valexpr -> Pstring.t
val pstring : Pstring.t repr

val valexpr : valexpr repr

(** Exception *)

exception LtacError of KerName.t * valexpr array
(** Ltac2-defined exceptions seen from OCaml side *)

quality98%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.