]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/grafite/grafiteAst.ml
More exceptions pretty-printed.
[helm.git] / helm / software / components / grafite / grafiteAst.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 type direction = [ `LeftToRight | `RightToLeft ]
29
30 type loc = Token.flocation
31
32 type ('term, 'lazy_term, 'ident) pattern =
33   'lazy_term option * ('ident * 'term) list * 'term option
34
35 type 'lazy_term reduction =
36   [ `Normalize
37   | `Reduce
38   | `Simpl
39   | `Unfold of 'lazy_term option
40   | `Whd ]
41
42 type 'ident intros_spec = int option * 'ident option list
43
44 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
45   (* Higher order tactics (i.e. tacticals) *)
46   | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic
47   | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
48   | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
49       (* sequential composition *)
50   | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic *
51       ('term, 'lazy_term, 'reduction, 'ident) tactic list
52   | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
53       (* try a sequence of loc * tactic until one succeeds, fail otherwise *)
54   | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
55       (* try a tactic and mask failures *)
56   | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
57   | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
58   (* Real tactics *)
59   | Absurd of loc * 'term
60   | Apply of loc * 'term
61   | ApplyS of loc * 'term * (string * string) list
62   | Assumption of loc
63   | AutoBatch of loc * (string * string) list
64   | Cases of loc * 'term * 'ident intros_spec
65   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
66   | Clear of loc * 'ident list
67   | ClearBody of loc * 'ident
68   | Constructor of loc * int
69   | Contradiction of loc
70   | Cut of loc * 'ident option * 'term
71   | Decompose of loc * 'ident option list
72   | Demodulate of loc
73   | Destruct of loc * 'term
74   | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern *
75             'ident intros_spec
76   | ElimType of loc * 'term * 'term option * 'ident intros_spec
77   | Exact of loc * 'term
78   | Exists of loc
79   | Fail of loc
80   | Fold of loc * 'reduction * 'lazy_term * ('term, 'lazy_term, 'ident) pattern
81   | Fourier of loc
82   | FwdSimpl of loc * string * 'ident option list
83   | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option
84   | IdTac of loc
85   | Intros of loc * 'ident intros_spec
86   | Inversion of loc * 'term
87   | LApply of loc * bool * int option * 'term list * 'term * 'ident option
88   | Left of loc
89   | LetIn of loc * 'term * 'ident
90   | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern 
91   | Reflexivity of loc
92   | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
93   | Rewrite of loc * direction * 'term *
94       ('term, 'lazy_term, 'ident) pattern * 'ident option list
95   | Right of loc
96   | Ring of loc
97   | Split of loc
98   | Subst of loc
99   | Symmetry of loc
100   | Transitivity of loc * 'term
101   (* Costruttori Aggiunti *)
102   | Assume of loc * 'ident * 'term
103   | Suppose of loc * 'term *'ident * 'term option
104   | By_term_we_proved of loc *'term option * 'term * 'ident option * 'term option
105   | We_need_to_prove of loc * 'term * 'ident option * 'term option
106   | Bydone of loc * 'term option 
107   | We_proceed_by_induction_on of loc * 'term * 'term
108   | We_proceed_by_cases_on of loc * 'term * 'term
109   | Byinduction of loc * 'term * 'ident
110   | Thesisbecomes of loc * 'term
111   | Case of loc * string * (string * 'term) list 
112   | ExistsElim of loc * 'term option * 'ident * 'term * 'ident * 'lazy_term
113   | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
114   | RewritingStep of
115      loc * (string option * 'term) option * 'term  *
116       [ `Term of 'term | `Auto of (string * string) list ] *
117       bool (* last step*)
118   
119 type search_kind = [ `Locate | `Hint | `Match | `Elim ]
120
121 type print_kind = [ `Env | `Coer ]
122
123 type presentation_style = Declarative
124                         | Procedural of int option
125
126 type 'term macro = 
127   (* Whelp's stuff *)
128   | WHint of loc * 'term 
129   | WMatch of loc * 'term 
130   | WInstance of loc * 'term 
131   | WLocate of loc * string
132   | WElim of loc * 'term
133   (* real macros *)
134   | Check of loc * 'term 
135   | Hint of loc
136   | AutoInteractive of loc * (string * string) list
137   | Inline of loc * presentation_style * string * string 
138      (* URI or base-uri, name prefix *) 
139
140 (** To be increased each time the command type below changes, used for "safe"
141  * marshalling *)
142 let magic = 11
143
144 type ('term,'obj) command =
145   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
146   | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *)
147   | Default of loc * string * UriManager.uri list
148   | Drop of loc
149   | Include of loc * string
150   | Obj of loc * 'obj
151   | Relation of
152      loc * string * 'term * 'term * 'term option * 'term option * 'term option
153   | Set of loc * string * string
154   | Print of loc * string
155   | Qed of loc
156
157 type ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical =
158   | Dot of loc
159   | Semicolon of loc
160   | Branch of loc
161   | Shift of loc
162   | Pos of loc * int list
163   | Wildcard of loc
164   | Merge of loc
165
166 type ('term,'lazy_term,'reduction,'ident) non_punctuation_tactical =
167   | Focus of loc * int list
168   | Unfocus of loc
169   | Skip of loc
170
171 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
172   | Command of loc * ('term, 'obj) command
173   | Macro of loc * 'term macro 
174   | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option
175       * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical
176   | NonPunctuationTactical of loc
177       * ('term, 'lazy_term, 'reduction, 'ident) non_punctuation_tactical
178       * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical
179              
180 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
181   | Note of loc * string
182   | Code of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
183              
184 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
185   | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
186   | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment