1 files changed, 137 insertions, 0 deletions
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
new file mode 100644
index 00000000..bd44bdbe
--- /dev/null
+++ b/plugins/ltac/tacinterp.mli
@@ -0,0 +1,137 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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 Tactic_debug
+open EConstr
+open Tacexpr
+open Genarg
+open Redexpr
+open Misctypes
+
+val ltac_trace_info : ltac_trace Exninfo.t
+
+module Value :
+sig
+  type t = Geninterp.Val.t
+  val of_constr : constr -> t
+  val to_constr : t -> constr option
+  val of_int : int -> t
+  val to_int : t -> int option
+  val to_list : t -> t list option
+  val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
+  val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
+end
+
+(** Values for interpretation *)
+type value = Value.t
+
+module TacStore : Store.S with
+  type t = Geninterp.TacStore.t
+  and type 'a field = 'a Geninterp.TacStore.field
+
+(** Signature for interpretation: val\_interp and interpretation functions *)
+type interp_sign = Geninterp.interp_sign = {
+  lfun : value Id.Map.t;
+  extra : TacStore.t }
+
+val f_avoid_ids : Id.Set.t TacStore.field
+val f_debug : debug_info TacStore.field
+
+val extract_ltac_constr_values : interp_sign -> Environ.env ->
+  Ltac_pretype.constr_under_binders Id.Map.t
+(** Given an interpretation signature, extract all values which are coercible to
+    a [constr]. *)
+
+(** Sets the debugger mode *)
+val set_debug : debug_info -> unit
+
+(** Gives the state of debug *)
+val get_debug : unit -> debug_info
+
+val type_uconstr :
+  ?flags:Pretyping.inference_flags ->
+  ?expected_type:Pretyping.typing_constraint ->
+  Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> constr Tactypes.delayed_open
+
+(** Adds an interpretation function for extra generic arguments *)
+
+val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t
+
+(** Interprets any expression *)
+val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tactic) -> unit Proofview.tactic
+
+(** Interprets an expression that evaluates to a constr *)
+val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
+
+(** Interprets redexp arguments *)
+val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
+
+(** Interprets tactic expressions *)
+
+val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
+  lident -> Id.t
+
+val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map ->
+  ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr ->
+  Ltac_pretype.closed_glob_constr
+
+val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map ->
+  glob_constr_and_expr -> Ltac_pretype.closed_glob_constr
+
+val interp_constr_gen : Pretyping.typing_constraint -> interp_sign ->
+  Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr
+
+val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
+  glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
+
+val interp_open_constr : ?expected_type:Pretyping.typing_constraint ->
+  ?flags:Pretyping.inference_flags ->
+  interp_sign -> Environ.env -> Evd.evar_map ->
+  glob_constr_and_expr -> Evd.evar_map * EConstr.constr
+
+val interp_open_constr_with_classes : ?expected_type:Pretyping.typing_constraint ->
+  interp_sign -> Environ.env -> Evd.evar_map ->
+  glob_constr_and_expr -> Evd.evar_map * EConstr.constr
+
+val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
+  glob_constr_and_expr with_bindings -> Evd.evar_map * EConstr.constr with_bindings
+
+(** Initial call for interpretation *)
+
+val eval_tactic : glob_tactic_expr -> unit Proofview.tactic
+
+val eval_tactic_ist : interp_sign -> glob_tactic_expr -> unit Proofview.tactic
+(** Same as [eval_tactic], but with the provided [interp_sign]. *)
+
+val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic
+
+(** Globalization + interpretation *)
+
+val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
+                 debug_info -> raw_tactic_expr -> unit Proofview.tactic
+
+val interp : raw_tactic_expr -> unit Proofview.tactic
+
+(** Hides interpretation for pretty-print *)
+
+val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic
+
+(** Internals that can be useful for syntax extensions. *)
+
+val interp_ltac_var : (value -> 'a) -> interp_sign ->
+  (Environ.env * Evd.evar_map) option -> lident -> 'a
+
+val interp_int : interp_sign -> lident -> int
+
+val interp_int_or_var : interp_sign -> int or_var -> int
+
+val default_ist : unit -> Geninterp.interp_sign
+(** Empty ist with debug set on the current value. *)