(* 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 (** * 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