1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 type direction = [ `LeftToRight | `RightToLeft ]
30 type loc = Stdpp.location
32 type ('term, 'lazy_term, 'ident) pattern =
33 'lazy_term option * ('ident * 'term) list * 'term option
36 CicNotationPt.term option * (string * CicNotationPt.term) list * CicNotationPt.term option
38 type 'lazy_term reduction =
41 | `Unfold of 'lazy_term option
44 type 'ident intros_spec = int option * 'ident option list
46 type 'term auto_params = 'term list * (string*string) list
50 | `Auto of 'term auto_params ]
53 | NApply of loc * CicNotationPt.term
54 | NAssert of loc * ((string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term) list
55 | NCases of loc * CicNotationPt.term * npattern
56 | NCase1 of loc * string
57 | NChange of loc * npattern * CicNotationPt.term
58 | NElim of loc * CicNotationPt.term * npattern
59 | NGeneralize of loc * npattern
61 | NIntro of loc * string
62 | NLetIn of loc * npattern * CicNotationPt.term * string
63 | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern
64 | NRewrite of loc * direction * CicNotationPt.term * npattern
66 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
67 (* Higher order tactics (i.e. tacticals) *)
68 | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic
69 | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
70 | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
71 (* sequential composition *)
72 | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic *
73 ('term, 'lazy_term, 'reduction, 'ident) tactic list
74 | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
75 (* try a sequence of loc * tactic until one succeeds, fail otherwise *)
76 | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
77 (* try a tactic and mask failures *)
78 | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
79 | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
81 | Absurd of loc * 'term
82 | Apply of loc * 'term
83 | ApplyRule of loc * 'term
84 | ApplyP of loc * 'term (* apply for procedural reconstruction *)
85 | ApplyS of loc * 'term * 'term auto_params
87 | AutoBatch of loc * 'term auto_params
88 | Cases of loc * 'term * ('term, 'lazy_term, 'ident) pattern *
90 | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
91 | Clear of loc * 'ident list
92 | ClearBody of loc * 'ident
93 | Compose of loc * 'term * 'term option * int * 'ident intros_spec
94 | Constructor of loc * int
95 | Contradiction of loc
96 | Cut of loc * 'ident option * 'term
97 | Decompose of loc * 'ident option list
98 | Demodulate of loc * 'term auto_params
99 | Destruct of loc * 'term list option
100 | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern *
102 | ElimType of loc * 'term * 'term option * 'ident intros_spec
103 | Exact of loc * 'term
106 | Fold of loc * 'reduction * 'lazy_term * ('term, 'lazy_term, 'ident) pattern
108 | FwdSimpl of loc * string * 'ident option list
109 | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option
111 | Intros of loc * 'ident intros_spec
112 | Inversion of loc * 'term
113 | LApply of loc * bool * int option * 'term list * 'term * 'ident option
115 | LetIn of loc * 'term * 'ident
116 | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern
118 | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
119 | Rewrite of loc * direction * 'term *
120 ('term, 'lazy_term, 'ident) pattern * 'ident option list
125 | Transitivity of loc * 'term
126 (* Declarative language *)
127 | Assume of loc * 'ident * 'term
128 | Suppose of loc * 'term *'ident * 'term option
129 | By_just_we_proved of loc * 'term just *
130 'term * 'ident option * 'term option
131 | We_need_to_prove of loc * 'term * 'ident option * 'term option
132 | Bydone of loc * 'term just
133 | We_proceed_by_induction_on of loc * 'term * 'term
134 | We_proceed_by_cases_on of loc * 'term * 'term
135 | Byinduction of loc * 'term * 'ident
136 | Thesisbecomes of loc * 'term
137 | Case of loc * string * (string * 'term) list
138 | ExistsElim of loc * 'term just * 'ident * 'term * 'ident * 'lazy_term
139 | AndElim of loc * 'term just * 'ident * 'term * 'ident * 'term
141 loc * (string option * 'term) option * 'term *
142 [ `Term of 'term | `Auto of 'term auto_params
143 | `Proof | `SolveWith of 'term ] *
146 type search_kind = [ `Locate | `Hint | `Match | `Elim ]
148 type print_kind = [ `Env | `Coer ]
150 type inline_param = IPPrefix of string
151 | IPAs of Cic.object_flavour
157 type ('term,'lazy_term) macro =
159 | WHint of loc * 'term
160 | WMatch of loc * 'term
161 | WInstance of loc * 'term
162 | WLocate of loc * string
163 | WElim of loc * 'term
165 | Eval of loc * 'lazy_term reduction * 'term
166 | Check of loc * 'term
168 | AutoInteractive of loc * 'term auto_params
169 | Inline of loc * string * inline_param list
170 (* URI or base-uri, parameters *)
172 (** To be increased each time the command type below changes, used for "safe"
176 type ('term,'obj) command =
177 | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
178 | Select of loc * UriManager.uri
180 | Coercion of loc * 'term * bool (* add_obj *) *
181 int (* arity *) * int (* saturations *)
182 | PreferCoercion of loc * 'term
183 | Inverter of loc * string * 'term * bool list
184 | UnificationHint of loc * 'term * int (* term, precedence *)
185 | Default of loc * string * UriManager.uri list
187 | Include of loc * string
190 loc * string * 'term * 'term * 'term option * 'term option * 'term option
191 | Set of loc * string * string
192 | Print of loc * string
194 | NObj of loc * CicNotationPt.term CicNotationPt.obj
195 | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
198 type punctuation_tactical =
203 | Pos of loc * int list
207 type non_punctuation_tactical =
208 | Focus of loc * int list
212 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
213 | Command of loc * ('term, 'obj) command
214 | Macro of loc * ('term,'lazy_term) macro
215 | NTactic of loc * ntactic * punctuation_tactical
216 | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option
217 * punctuation_tactical
218 | NonPunctuationTactical of loc * non_punctuation_tactical
219 * punctuation_tactical
220 | NNonPunctuationTactical of loc * non_punctuation_tactical
221 * punctuation_tactical
223 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
224 | Note of loc * string
225 | Code of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
227 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
228 | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
229 | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment