--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+type direction = [ `LeftToRight | `RightToLeft ]
+type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
+
+type loc = CicNotationPt.location
+
+type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
+
+type ('term, 'ident) tactic =
+ | Absurd of loc * 'term
+ | Apply of loc * 'term
+ | Assumption of loc
+ | Auto of loc * int option * int option (* depth, width *)
+ | Change of loc * ('term,'ident) pattern * 'term
+ | Clear of loc * 'ident
+ | ClearBody of loc * 'ident
+ | Compare of loc * 'term
+ | Constructor of loc * int
+ | Contradiction of loc
+ | Cut of loc * 'ident option * 'term
+ | DecideEquality of loc
+ | Decompose of loc * 'term
+ | Discriminate of loc * 'term
+ | Elim of loc * 'term * 'term option * int option * 'ident list
+ | ElimType of loc * 'term * 'term option * int option * 'ident list
+ | Exact of loc * 'term
+ | Exists of loc
+ | Fail of loc
+ | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
+ | Fourier of loc
+ | FwdSimpl of loc * string * 'ident list
+ | Generalize of loc * ('term, 'ident) pattern * 'ident option
+ | Goal of loc * int (* change current goal, argument is goal number 1-based *)
+ | IdTac of loc
+ | Injection of loc * 'term
+ | Intros of loc * int option * 'ident list
+ | LApply of loc * int option * 'term list * 'term * 'ident option
+ | Left of loc
+ | LetIn of loc * 'term * 'ident
+ | Reduce of loc * reduction_kind * ('term, 'ident) pattern
+ | Reflexivity of loc
+ | Replace of loc * ('term, 'ident) pattern * 'term
+ | Rewrite of loc * direction * 'term * ('term, 'ident) pattern
+ | Right of loc
+ | Ring of loc
+ | Split of loc
+ | Symmetry of loc
+ | Transitivity of loc * 'term
+
+type thm_flavour = Cic.object_flavour
+
+ (** <name, inductive/coinductive, type, constructor list>
+ * true means inductive, false coinductive *)
+type 'term inductive_type = string * bool * 'term * (string * 'term) list
+
+type search_kind = [ `Locate | `Hint | `Match | `Elim ]
+
+type print_kind = [ `Env | `Coer ]
+
+type 'term macro =
+ (* Whelp's stuff *)
+ | WHint of loc * 'term
+ | WMatch of loc * 'term
+ | WInstance of loc * 'term
+ | WLocate of loc * string
+ | WElim of loc * 'term
+ (* real macros *)
+(* | Abort of loc *)
+ | Print of loc * string
+ | Check of loc * 'term
+ | Hint of loc
+ | Quit of loc
+(* | Redo of loc * int option
+ | Undo of loc * int option *)
+(* | Print of loc * print_kind *)
+ | Search_pat of loc * search_kind * string (* searches with string pattern *)
+ | Search_term of loc * search_kind * 'term (* searches with term pattern *)
+
+type alias_spec =
+ | Ident_alias of string * string (* identifier, uri *)
+ | Symbol_alias of string * int * string (* name, instance no, description *)
+ | Number_alias of int * string (* instance no, description *)
+
+type obj =
+ | Inductive of (string * CicNotationPt.term) list *
+ CicNotationPt.term inductive_type list
+ (** parameters, list of loc * mutual inductive types *)
+ | Theorem of thm_flavour * string * CicNotationPt.term * CicNotationPt.term option
+ (** flavour, name, type, body
+ * - name is absent when an unnamed theorem is being proved, tipically in
+ * interactive usage
+ * - body is present when its given along with the command, otherwise it
+ * will be given in proof editing mode using the tactical language
+ *)
+ | Record of
+ (string * CicNotationPt.term) list * string * CicNotationPt.term *
+ (string * CicNotationPt.term) list
+
+type argument_pattern =
+ | IdentArg of int * string (* eta-depth, name *)
+
+type cic_appl_pattern =
+ | UriPattern of UriManager.uri
+ | VarPattern of string
+ | ApplPattern of cic_appl_pattern list
+
+type ('term,'obj) command =
+ | Default of loc * string * UriManager.uri list
+ | Include of loc * string
+ | Set of loc * string * string
+ | Drop of loc
+ | Qed of loc
+ (** name.
+ * Name is needed when theorem was started without providing a name
+ *)
+ | Coercion of loc * 'term
+ | Alias of loc * alias_spec
+ (** parameters, name, type, fields *)
+ | Obj of loc * 'obj
+ | Notation of loc * 'term * Gramext.g_assoc option * int option * 'term
+ (* level 1 pattern, associativity, precedence, level 2 pattern *)
+ | Interpretation of loc * (string * argument_pattern list) * cic_appl_pattern
+
+ (* DEBUGGING *)
+ | Dump of loc (* dump grammar on stdout *)
+ (* DEBUGGING *)
+ | Render of loc * UriManager.uri (* render library object *)
+
+type ('term, 'ident) tactical =
+ | Tactic of loc * ('term, 'ident) tactic
+ | Do of loc * int * ('term, 'ident) tactical
+ | Repeat of loc * ('term, 'ident) tactical
+ | Seq of loc * ('term, 'ident) tactical list (* sequential composition *)
+ | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list
+ | First of loc * ('term, 'ident) tactical list
+ (* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
+ | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
+ | Solve of loc * ('term, 'ident) tactical list
+
+
+type ('term, 'obj, 'ident) code =
+ | Command of loc * ('term,'obj) command
+ | Macro of loc * 'term macro
+ | Tactical of loc * ('term, 'ident) tactical
+
+type ('term, 'obj, 'ident) comment =
+ | Note of loc * string
+ | Code of loc * ('term, 'obj, 'ident) code
+
+type ('term, 'obj, 'ident) statement =
+ | Executable of loc * ('term, 'obj, 'ident) code
+ | Comment of loc * ('term, 'obj, 'ident) comment
+
projects / helm.git / blobdiff