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 type just = [`Term of nterm | `Auto of auto_params]
42 | NApply of loc * nterm
43 | NSmartApply of loc * nterm
44 | NAssert of loc * ((string * [`Decl of nterm | `Def of nterm * nterm]) list * nterm) list
45 | NCases of loc * nterm * npattern
46 | NCase1 of loc * string
47 | NChange of loc * npattern * nterm
48 | NClear of loc * string list
49 | NConstructor of loc * int option * nterm list
51 (* | NDiscriminate of loc * nterm
52 | NSubst of loc * nterm *)
53 | NDestruct of loc * string list option * string list
54 | NElim of loc * nterm * npattern
55 | NGeneralize of loc * npattern
57 | NIntro of loc * string
58 | NIntros of loc * string list
59 | NInversion of loc * nterm * npattern
60 | NLApply of loc * nterm
61 | NLetIn of loc * npattern * nterm * string
62 | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern
63 | NRewrite of loc * direction * nterm * npattern
64 | NAuto of loc * auto_params
69 | NPos of loc * int list
70 | NPosbyname of loc * string
74 | NFocus of loc * int list
76 | NTry of loc * ntactic
78 | NRepeat of loc * ntactic
79 | NBlock of loc * ntactic list
80 (* Declarative langauge *)
81 (* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
82 | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *)
83 | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *)
84 | By_just_we_proved of loc * just * nterm * string option * nterm option (* loc,
85 justification, conclusion, identifier, eqconcl *)
86 | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
87 identifier, equivnewcon *)
88 | BetaRewritingStep of loc * nterm
89 | Bydone of loc * just
90 | ExistsElim of loc * just * string * nterm * nterm * string
91 | AndElim of loc * just * nterm * string * nterm * string
94 loc * (string option * nterm) option * nterm *
95 [ `Term of nterm | `Auto of auto_params
96 | `Proof | `SolveWith of nterm ] *
100 loc * nterm * [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*)
105 | Thesisbecomes of loc * nterm * nterm option
106 | We_proceed_by_induction_on of loc * nterm * nterm
107 | We_proceed_by_cases_on of loc * nterm * nterm
108 | Byinduction of loc * nterm * string
109 | Case of loc * string * (string * nterm) list
110 (* This is a debug tactic to print the stack to stdout, can be safely removed *)
114 | NCheck of loc * nterm
115 | Screenshot of loc * string
116 | NAutoInteractive of loc * auto_params
119 (** To be increased each time the command type below changes, used for "safe"
123 (* composed magic: term + command magics. No need to change this value *)
124 let magic = magic + 10000 * NotationPt.magic
127 | Ident_alias of string * string (* identifier, uri *)
128 | Symbol_alias of string * int * string (* name, instance no, description *)
129 | Number_alias of int * string (* instance no, description *)
131 type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
134 | Include of loc * inclusion_mode * string (* _,buri,_,path *)
135 | UnificationHint of loc * nterm * int (* term, precedence *)
136 | NObj of loc * nterm NotationPt.obj * bool
137 | NDiscriminator of loc * nterm
138 | NInverter of loc * string * nterm * bool list option * nterm option
139 | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
140 | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
141 | NCoercion of loc * string * bool *
142 (nterm * nterm * (string * nterm) * nterm) option
144 (* ex lexicon commands *)
145 | Alias of loc * alias_spec
146 (** parameters, name, type, fields *)
147 | Notation of loc * direction option * nterm * Gramext.g_assoc *
149 (* direction, l1 pattern, associativity, precedence, l2 pattern *)
150 | Interpretation of loc *
151 string * (string * NotationPt.argument_pattern list) *
152 NotationPt.cic_appl_pattern
153 (* description (i.e. id), symbol, arg pattern, appl pattern *)
156 | NCommand of loc * command
157 | NMacro of loc * nmacro
158 | NTactic of loc * ntactic list
161 | Note of loc * string
165 | Executable of loc * code
166 | Comment of loc * comment
168 let description_of_alias =
171 | Symbol_alias (_,_,desc)
172 | Number_alias (_,desc) -> desc