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 | NEval of loc * npattern * [ `Whd of bool ]
60 | NGeneralize of loc * npattern
62 | NIntro of loc * string
63 | NLetIn of loc * npattern * CicNotationPt.term * string
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 presentation_style = Declarative
151 | Procedural of int option
153 type ('term,'lazy_term) macro =
155 | WHint of loc * 'term
156 | WMatch of loc * 'term
157 | WInstance of loc * 'term
158 | WLocate of loc * string
159 | WElim of loc * 'term
161 | Eval of loc * 'lazy_term reduction * 'term
162 | Check of loc * 'term
164 | AutoInteractive of loc * 'term auto_params
165 | Inline of loc * presentation_style * string * string * Cic.object_flavour option
166 (* URI or base-uri, name prefix, flavour *)
168 (** To be increased each time the command type below changes, used for "safe"
172 type ('term,'obj) command =
173 | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
174 | Select of loc * UriManager.uri
176 | Coercion of loc * 'term * bool (* add_obj *) *
177 int (* arity *) * int (* saturations *)
178 | PreferCoercion of loc * 'term
179 | UnificationHint of loc * 'term * int (* term, precedence *)
180 | Default of loc * string * UriManager.uri list
182 | Include of loc * string
185 loc * string * 'term * 'term * 'term option * 'term option * 'term option
186 | Set of loc * string * string
187 | Print of loc * string
189 | NObj of loc * CicNotationPt.term CicNotationPt.obj
191 type punctuation_tactical =
196 | Pos of loc * int list
200 type non_punctuation_tactical =
201 | Focus of loc * int list
205 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
206 | Command of loc * ('term, 'obj) command
207 | Macro of loc * ('term,'lazy_term) macro
208 | NTactic of loc * ntactic * punctuation_tactical
209 | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option
210 * punctuation_tactical
211 | NonPunctuationTactical of loc * non_punctuation_tactical
212 * punctuation_tactical
214 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
215 | Note of loc * string
216 | Code of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
218 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
219 | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
220 | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment