X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Facic_content%2FcicNotationPt.ml;fp=helm%2Focaml%2Facic_content%2FcicNotationPt.ml;h=a66aa5febb3aa86600fdf8320edb439fb98ed2d0;hp=0000000000000000000000000000000000000000;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953 diff --git a/helm/ocaml/acic_content/cicNotationPt.ml b/helm/ocaml/acic_content/cicNotationPt.ml new file mode 100644 index 000000000..a66aa5feb --- /dev/null +++ b/helm/ocaml/acic_content/cicNotationPt.ml @@ -0,0 +1,190 @@ +(* Copyright (C) 2005, 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/ + *) + +(* $Id$ *) + +(** CIC Notation Parse Tree *) + +type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] +type induction_kind = [ `Inductive | `CoInductive ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] +type fold_kind = [ `Left | `Right ] + +type location = Token.flocation +let fail floc msg = + let (x, y) = HExtlib.loc_of_floc floc in + failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) + +type href = UriManager.uri + +type child_pos = [ `Left | `Right | `Inner ] + +type term_attribute = + [ `Loc of location (* source file location *) + | `IdRef of string (* ACic pointer *) + | `Level of int * Gramext.g_assoc (* precedence, associativity *) + | `ChildPos of child_pos (* position of l1 pattern variables *) + | `XmlAttrs of (string option * string * string) list + (* list of XML attributes: namespace, name, value *) + | `Raw of string (* unparsed version *) + ] + +type literal = + [ `Symbol of string + | `Keyword of string + | `Number of string + ] + +type case_indtype = string * href option + +(** To be increased each time the term type below changes, used for "safe" + * marshalling *) +let magic = 1 + +type term = + (* CIC AST *) + + | AttributedTerm of term_attribute * term + + | Appl of term list + | Binder of binder_kind * capture_variable * term (* kind, name, body *) + | Case of term * case_indtype option * term option * + (case_pattern * term) list + (* what to match, inductive type, out type, list *) + | Cast of term * term + | LetIn of capture_variable * term * term (* name, body, where *) + | LetRec of induction_kind * (capture_variable * term * int) list * term + (* (name, body, decreasing argument) list, where *) + | Ident of string * subst list option + (* literal, substitutions. + * Some [] -> user has given an empty explicit substitution list + * None -> user has given no explicit substitution list *) + | Implicit + | Meta of int * meta_subst list + | Num of string * int (* literal, instance *) + | Sort of sort_kind + | Symbol of string * int (* canonical name, instance *) + + | UserInput (* place holder for user input, used by MatitaConsole, not to be + used elsewhere *) + | Uri of string * subst list option (* as Ident, for long names *) + + (* Syntax pattern extensions *) + + | Literal of literal + | Layout of layout_pattern + + | Magic of magic_term + | Variable of pattern_variable + + (* name, type. First component must be Ident or Variable (FreshVar _) *) +and capture_variable = term * term option + +and meta_subst = term option +and subst = string * term +and case_pattern = string * href option * capture_variable list + +and box_kind = H | V | HV | HOV +and box_spec = box_kind * bool * bool (* kind, spacing, indent *) + +and layout_pattern = + | Sub of term * term + | Sup of term * term + | Below of term * term + | Above of term * term + | Frac of term * term + | Over of term * term + | Atop of term * term +(* | array of term * literal option * literal option + |+ column separator, row separator +| *) + | Sqrt of term + | Root of term * term (* argument, index *) + | Break + | Box of box_spec * term list + | Group of term list + +and magic_term = + (* level 1 magics *) + | List0 of term * literal option (* pattern, separator *) + | List1 of term * literal option (* pattern, separator *) + | Opt of term + + (* level 2 magics *) + | Fold of fold_kind * term * string list * term + (* base case pattern, recursive case bound names, recursive case pattern *) + | Default of term * term (* "some" case pattern, "none" case pattern *) + | Fail + | If of term * term * term (* test, pattern if true, pattern if false *) + +and pattern_variable = + (* level 1 and 2 variables *) + | NumVar of string + | IdentVar of string + | TermVar of string + + (* level 1 variables *) + | Ascription of term * string + + (* level 2 variables *) + | FreshVar of string + +type argument_pattern = + | IdentArg of int * string (* eta-depth, name *) + +type cic_appl_pattern = + | UriPattern of UriManager.uri + | VarPattern of string + | ImplicitPattern + | ApplPattern of cic_appl_pattern list + + (** + * true means inductive, false coinductive *) +type 'term inductive_type = string * bool * 'term * (string * 'term) list + +type obj = + | Inductive of (string * term) list * term inductive_type list + (** parameters, list of loc * mutual inductive types *) + | Theorem of Cic.object_flavour * string * term * 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 * term) list * string * term * (string * term * bool) list + (** left parameters, name, type, fields *) + +(** {2 Standard precedences} *) + +let let_in_prec = 10 +let binder_prec = 20 +let apply_prec = 70 +let simple_prec = 90 + +let let_in_assoc = Gramext.NonA +let binder_assoc = Gramext.RightA +let apply_assoc = Gramext.LeftA +let simple_assoc = Gramext.NonA +