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 nterm = NotationPt.term
35 nterm option * (string * nterm) list * nterm option
37 type auto_params = nterm list option * (string*string) list
39 (* The additional a is for abstract *)
40 type 'term aauto_params = 'term list option * (string*string) list
42 type 'term just = [`Term of 'term | `Auto of 'term aauto_params]
45 | NApply of loc * nterm
46 | NSmartApply of loc * nterm
47 | NAssert of loc * ((string * [`Decl of nterm | `Def of nterm * nterm]) list * nterm) list
48 | NCases of loc * nterm * npattern
49 | NCase1 of loc * string
50 | NChange of loc * npattern * nterm
51 | NClear of loc * string list
52 | NConstructor of loc * int option * nterm list
54 (* | NDiscriminate of loc * nterm
55 | NSubst of loc * nterm *)
56 | NDestruct of loc * string list option * string list
57 | NElim of loc * nterm * npattern
58 | NGeneralize of loc * npattern
60 | NIntro of loc * string
61 | NIntros of loc * string list
62 | NInversion of loc * nterm * npattern
63 | NLApply of loc * nterm
64 | NLetIn of loc * npattern * nterm * string
65 | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern
66 | NRewrite of loc * direction * nterm * npattern
67 | NAuto of loc * auto_params
72 | NPos of loc * int list
73 | NPosbyname of loc * string
77 | NFocus of loc * int list
79 | NTry of loc * ntactic
81 | NRepeat of loc * ntactic
82 | NBlock of loc * ntactic list
83 (* Declarative langauge *)
84 (* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
85 | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *)
86 | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *)
87 | By_just_we_proved of loc * nterm just * nterm * string option * nterm option (* loc,
88 justification, conclusion, identifier, eqconcl *)
89 | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
90 identifier, equivnewcon *)
91 | Bydone of loc * nterm just
93 | ExistsElim of loc * nterm just * string * nterm * nterm * string
94 | AndElim of loc * nterm just * nterm * string * nterm * string
98 | NCheck of loc * nterm
99 | Screenshot of loc * string
100 | NAutoInteractive of loc * auto_params
103 (** To be increased each time the command type below changes, used for "safe"
107 (* composed magic: term + command magics. No need to change this value *)
108 let magic = magic + 10000 * NotationPt.magic
111 | Ident_alias of string * string (* identifier, uri *)
112 | Symbol_alias of string * int * string (* name, instance no, description *)
113 | Number_alias of int * string (* instance no, description *)
115 type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
118 | Include of loc * inclusion_mode * string (* _,buri,_,path *)
119 | UnificationHint of loc * nterm * int (* term, precedence *)
120 | NObj of loc * nterm NotationPt.obj * bool
121 | NDiscriminator of loc * nterm
122 | NInverter of loc * string * nterm * bool list option * nterm option
123 | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
124 | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
125 | NCoercion of loc * string * bool *
126 (nterm * nterm * (string * nterm) * nterm) option
128 (* ex lexicon commands *)
129 | Alias of loc * alias_spec
130 (** parameters, name, type, fields *)
131 | Notation of loc * direction option * nterm * Gramext.g_assoc *
133 (* direction, l1 pattern, associativity, precedence, l2 pattern *)
134 | Interpretation of loc *
135 string * (string * NotationPt.argument_pattern list) *
136 NotationPt.cic_appl_pattern
137 (* description (i.e. id), symbol, arg pattern, appl pattern *)
140 | NCommand of loc * command
141 | NMacro of loc * nmacro
142 | NTactic of loc * ntactic list
145 | Note of loc * string
149 | Executable of loc * code
150 | Comment of loc * comment
152 let description_of_alias =
155 | Symbol_alias (_,_,desc)
156 | Number_alias (_,desc) -> desc