← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to tactics/tacinterp.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
tactics/tacinterp.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: tacinterp.mli 12102 2009-04-24 10:48:11Z herbelin $ i*)
 
10
 
 
11
(*i*)
 
12
open Dyn
 
13
open Pp
 
14
open Util
 
15
open Names
 
16
open Proof_type
 
17
open Tacmach
 
18
open Tactic_debug
 
19
open Term
 
20
open Tacexpr
 
21
open Genarg
 
22
open Topconstr
 
23
open Mod_subst
 
24
open Redexpr
 
25
(*i*)
 
26
 
 
27
(* Values for interpretation *)
 
28
type value =
 
29
  | VRTactic of (goal list sigma * validation)
 
30
  | VFun of ltac_trace * (identifier*value) list * 
 
31
      identifier option list * glob_tactic_expr
 
32
  | VVoid
 
33
  | VInteger of int
 
34
  | VIntroPattern of intro_pattern_expr
 
35
  | VConstr of constr
 
36
  | VConstr_context of constr
 
37
  | VList of value list
 
38
  | VRec of (identifier*value) list ref * glob_tactic_expr
 
39
 
 
40
(* Signature for interpretation: val\_interp and interpretation functions *)
 
41
and interp_sign =
 
42
  { lfun : (identifier * value) list;
 
43
    avoid_ids : identifier list;
 
44
    debug : debug_info;
 
45
    trace : ltac_trace }
 
46
 
 
47
val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env -> 
 
48
  Pretyping.var_map * Pretyping.unbound_ltac_var_map
 
49
 
 
50
(* Transforms an id into a constr if possible *)
 
51
val constr_of_id : Environ.env -> identifier -> constr
 
52
 
 
53
(* To embed several objects in Coqast.t *)
 
54
val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t
 
55
val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)
 
56
  
 
57
val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
 
58
val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr
 
59
val valueIn : value -> raw_tactic_arg
 
60
val constrIn : constr -> constr_expr
 
61
 
 
62
(* Sets the debugger mode *)
 
63
val set_debug : debug_info -> unit
 
64
 
 
65
(* Gives the state of debug *)
 
66
val get_debug : unit -> debug_info
 
67
 
 
68
(* Adds a definition for tactics in the table *)
 
69
val add_tacdef :
 
70
  bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit
 
71
val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
72
 
 
73
(* Tactic extensions *)
 
74
val add_tactic :
 
75
  string -> (typed_generic_argument list -> tactic) -> unit
 
76
val overwriting_add_tactic :
 
77
  string -> (typed_generic_argument list -> tactic) -> unit
 
78
val lookup_tactic :
 
79
  string -> (typed_generic_argument list) -> tactic
 
80
 
 
81
(* Adds an interpretation function for extra generic arguments *)
 
82
type glob_sign = {
 
83
  ltacvars : identifier list * identifier list;
 
84
  ltacrecvars : (identifier * Nametab.ltac_constant) list;
 
85
  gsigma : Evd.evar_map;
 
86
  genv : Environ.env }
 
87
 
 
88
val add_interp_genarg :
 
89
  string ->
 
90
    (glob_sign -> raw_generic_argument -> glob_generic_argument) *
 
91
    (interp_sign -> goal sigma -> glob_generic_argument -> 
 
92
      typed_generic_argument) *
 
93
    (substitution -> glob_generic_argument -> glob_generic_argument)
 
94
    -> unit
 
95
 
 
96
val interp_genarg :
 
97
  interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument
 
98
 
 
99
val intern_genarg :
 
100
  glob_sign -> raw_generic_argument -> glob_generic_argument
 
101
 
 
102
val intern_tactic : 
 
103
  glob_sign -> raw_tactic_expr -> glob_tactic_expr
 
104
 
 
105
val intern_constr :
 
106
  glob_sign -> constr_expr -> rawconstr_and_expr
 
107
 
 
108
val intern_constr_with_bindings :
 
109
  glob_sign -> constr_expr * constr_expr Rawterm.bindings -> 
 
110
  rawconstr_and_expr * rawconstr_and_expr Rawterm.bindings
 
111
 
 
112
val intern_hyp :
 
113
  glob_sign -> identifier Util.located -> identifier Util.located
 
114
 
 
115
val subst_genarg :
 
116
  substitution -> glob_generic_argument -> glob_generic_argument
 
117
 
 
118
val subst_rawconstr_and_expr :
 
119
  substitution -> rawconstr_and_expr -> rawconstr_and_expr
 
120
 
 
121
(* Interprets any expression *)
 
122
val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value
 
123
 
 
124
(* Interprets an expression that evaluates to a constr *)
 
125
val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> 
 
126
  constr
 
127
 
 
128
(* Interprets redexp arguments *)
 
129
val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr
 
130
 
 
131
(* Interprets tactic expressions *)
 
132
val interp_tac_gen : (identifier * value) list -> identifier list ->
 
133
                 debug_info -> raw_tactic_expr -> tactic
 
134
 
 
135
val interp_hyp :  interp_sign -> goal sigma -> identifier located -> identifier
 
136
 
 
137
val interp_bindings : interp_sign -> goal sigma -> rawconstr_and_expr Rawterm.bindings -> 
 
138
  Evd.open_constr Rawterm.bindings
 
139
 
 
140
(* Initial call for interpretation *)
 
141
val glob_tactic : raw_tactic_expr -> glob_tactic_expr
 
142
 
 
143
val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
 
144
 
 
145
val eval_tactic : glob_tactic_expr -> tactic
 
146
 
 
147
val interp : raw_tactic_expr -> tactic
 
148
 
 
149
val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr
 
150
 
 
151
val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
 
152
 
 
153
(* Hides interpretation for pretty-print *)
 
154
 
 
155
val hide_interp : raw_tactic_expr -> tactic option -> tactic
 
156
 
 
157
(* Declare the default tactic to fill implicit arguments *)
 
158
val declare_implicit_tactic : tactic -> unit
 
159
 
 
160
(* Declare the xml printer *)
 
161
val declare_xml_printer : 
 
162
  (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit
 
163
 
 
164
(* printing *)
 
165
val print_ltac : Libnames.qualid -> std_ppcmds
 
166
 
 
167
(* Internals that can be useful for syntax extensions. *)
 
168
 
 
169
exception CannotCoerceTo of string
 
170
 
 
171
val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> identifier located -> 'a
 
172
 
 
173
val interp_int : interp_sign -> identifier located -> int
 
174
 
 
175
val error_ltac_variable : loc -> identifier -> Environ.env option -> value -> string -> 'a
 
176