+++ /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/
- *)
-
-module Ast = CicNotationPt
-
-type direction = [ `LeftToRight | `RightToLeft ]
-
-type loc = Ast.location
-
-type ('term, 'lazy_term, 'ident) pattern =
- 'lazy_term option * ('ident * 'term) list * 'term
-
-type ('term, 'ident) type_spec =
- | Ident of 'ident
- | Type of UriManager.uri * int
-
-type reduction =
- [ `Normalize
- | `Reduce
- | `Simpl
- | `Unfold of CicNotationPt.term option
- | `Whd ]
-
-type ('term, 'lazy_term, 'reduction, 'ident) tactic =
- | Absurd of loc * 'term
- | Apply of loc * 'term
- | Assumption of loc
- | Auto of loc * int option * int option * string option * string option
- (* depth, width, paramodulation, full *) (* ALB *)
- | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_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, 'ident) type_spec list * 'ident * 'ident list
- | 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 * 'lazy_term * ('term, 'lazy_term, 'ident) pattern
- | Fourier of loc
- | FwdSimpl of loc * string * 'ident list
- | Generalize of loc * ('term, 'lazy_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 * ('term, 'lazy_term, 'ident) pattern
- | Reflexivity of loc
- | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
- | Rewrite of loc * direction * 'term *
- ('term, 'lazy_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 * Ast.term) list *
- Ast.term inductive_type list
- (** parameters, list of loc * mutual inductive types *)
- | Theorem of thm_flavour * string * Ast.term * Ast.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 * Ast.term) list * string * Ast.term *
- (string * Ast.term) list
- (** left parameters, name, type, fields *)
-
-type metadata =
- | Dependency of string (* baseuri without trailing slash *)
- | Baseuri of string
-
-let compare_metadata = Pervasives.compare
-
-let eq_metadata = (=)
-
-(** To be increased each time the command type below changes, used for "safe"
- * marshalling *)
-let magic = 2
-
-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 * direction option * Ast.term * Gramext.g_assoc *
- int * Ast.term
- (* direction, l1 pattern, associativity, precedence, l2 pattern *)
- | Interpretation of loc *
- string * (string * Ast.argument_pattern list) *
- Ast.cic_appl_pattern
- (* description (i.e. id), symbol, arg pattern, appl pattern *)
-
- | Metadata of loc * metadata
-
- (* DEBUGGING *)
- | Dump of loc (* dump grammar on stdout *)
- (* DEBUGGING *)
- | Render of loc * UriManager.uri (* render library object *)
-
-(* composed magic: term + command magics. No need to change this value *)
-let magic = magic + 10000 * CicNotationPt.magic
-
-let reash_cmd_uris =
- let reash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
- function
- | Default (loc, name, uris) ->
- let uris = List.map reash_uri uris in
- Default (loc, name, uris)
- | Interpretation (loc, dsc, args, cic_appl_pattern) ->
- let rec aux =
- function
- | CicNotationPt.UriPattern uri ->
- CicNotationPt.UriPattern (reash_uri uri)
- | CicNotationPt.ApplPattern args ->
- CicNotationPt.ApplPattern (List.map aux args)
- | CicNotationPt.VarPattern _
- | CicNotationPt.ImplicitPattern as pat -> pat
- in
- let appl_pattern = aux cic_appl_pattern in
- Interpretation (loc, dsc, args, appl_pattern)
- | cmd -> cmd
-
-type ('term, 'lazy_term, 'reduction, 'ident) tactical =
- | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
- | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical
- | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
- | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- (* sequential composition *)
- | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical *
- ('term, 'lazy_term, 'reduction, 'ident) tactical list
- | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- (* try a sequence of loc * tactical until one succeeds, fail otherwise *)
- | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
- (* try a tactical and mask failures *)
- | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
-
- | Dot of loc
- | Semicolon of loc
- | Branch of loc
- | Shift of loc
- | Pos of loc * int
- | Merge of loc
- | Focus of loc * int list
- | Unfocus of loc
- | Skip of loc
-
-let is_punctuation =
- function
- | Dot _ | Semicolon _ | Branch _ | Shift _ | Merge _ | Pos _ -> true
- | _ -> false
-
-type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
- | Command of loc * ('term,'obj) command
- | Macro of loc * 'term macro
- | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
- * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *)
-
-type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
- | Note of loc * string
- | Code of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
-
-type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
- | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
- | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment
-
- (* statements meaningful for matitadep *)
-type dependency =
- | IncludeDep of string
- | BaseuriDep of string
- | UriDep of UriManager.uri
-
projects / helm.git / blobdiff