blob: 2d448e832b262a00e86af3ec035992c6253b0fb7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
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 error_ltac_variable : ?loc:Loc.t -> Id.t ->
(Environ.env * Evd.evar_map) option -> value -> string -> 'a
(** Transforms a constr-expecting tactic into a tactic finding its arguments in
the Ltac environment according to the given names. *)
val lift_constr_tac_to_ml_tac : Name.t list ->
(constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic
val default_ist : unit -> Geninterp.interp_sign
(** Empty ist with debug set on the current value. *)
|
