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 (* loc, identifier, type *)
83 | Suppose of loc * nterm * string (* loc, assumption, identifier *)
84 | By_just_we_proved of loc * just * nterm * string option (* loc, justification, conclusion, identifier *)
85 | We_need_to_prove of loc * nterm * string option (* loc, newconclusion, identifier *)
86 | BetaRewritingStep of loc * nterm
87 | Bydone of loc * just
88 | ExistsElim of loc * just * string * nterm * nterm * string
89 | AndElim of loc * just * nterm * string * nterm * string
91 loc * nterm * [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*)
96 | Thesisbecomes of loc * nterm
97 | We_proceed_by_induction_on of loc * nterm * nterm
98 | We_proceed_by_cases_on of loc * nterm * nterm
99 | Byinduction of loc * nterm * string
100 | Case of loc * string * (string * nterm) list
101 (* This is a debug tactic to print the stack to stdout, can be safely removed *)
105 | NCheck of loc * nterm
106 | Screenshot of loc * string
107 | NAutoInteractive of loc * auto_params
110 (** To be increased each time the command type below changes, used for "safe"
114 (* composed magic: term + command magics. No need to change this value *)
115 let magic = magic + 10000 * NotationPt.magic
118 | Ident_alias of string * string (* identifier, uri *)
119 | Symbol_alias of string * int * string (* name, instance no, description *)
120 | Number_alias of int * string (* instance no, description *)
122 type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
125 | Include of loc * inclusion_mode * string (* _,buri,_,path *)
126 | UnificationHint of loc * nterm * int (* term, precedence *)
127 | NObj of loc * nterm NotationPt.obj * bool
128 | NDiscriminator of loc * nterm
129 | NInverter of loc * string * nterm * bool list option * nterm option
130 | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
131 | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
132 | NCoercion of loc * string * bool *
133 (nterm * nterm * (string * nterm) * nterm) option
135 (* ex lexicon commands *)
136 | Alias of loc * alias_spec
137 (** parameters, name, type, fields *)
138 | Notation of loc * direction option * nterm * Gramext.g_assoc *
140 (* direction, l1 pattern, associativity, precedence, l2 pattern *)
141 | Interpretation of loc *
142 string * (string * NotationPt.argument_pattern list) *
143 NotationPt.cic_appl_pattern
144 (* description (i.e. id), symbol, arg pattern, appl pattern *)
147 | NCommand of loc * command
148 | NMacro of loc * nmacro
149 | NTactic of loc * ntactic list
152 | Note of loc * string
156 | Executable of loc * code
157 | Comment of loc * comment
159 let description_of_alias =
162 | Symbol_alias (_,_,desc)
163 | Number_alias (_,desc) -> desc