X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPt.ml;h=8dbfea7992019a4e69a894cda12cec357b55d666;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=609fb9d2f24a08f362c2276afa16f8fa2f673737;hpb=9c9e979d4c45cf3b1ee01688b2c36fe49190ce98;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 609fb9d2f..8dbfea799 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -29,10 +29,11 @@ type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of +CicUniv.universe | `NType of string |`NCProp of string] type fold_kind = [ `Left | `Right ] -type location = Token.flocation +type location = Stdpp.location 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) @@ -44,8 +45,7 @@ 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 *) + | `Level of int | `XmlAttrs of (string option * string * string) list (* list of XML attributes: namespace, name, value *) | `Raw of string (* unparsed version *) @@ -59,9 +59,11 @@ type literal = type case_indtype = string * href option +type 'term capture_variable = 'term * 'term option + (** To be increased each time the term type below changes, used for "safe" * marshalling *) -let magic = 1 +let magic = 6 type term = (* CIC AST *) @@ -69,14 +71,14 @@ type term = | AttributedTerm of term_attribute * term | Appl of term list - | Binder of binder_kind * capture_variable * term (* kind, name, body *) + | Binder of binder_kind * term 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 *) + | LetIn of term capture_variable * term * term (* name, body, where *) + | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term + (* (params, name, body, decreasing arg) list, where *) | Ident of string * subst list option (* literal, substitutions. * Some [] -> user has given an empty explicit substitution list @@ -90,6 +92,7 @@ type term = | 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 *) + | NRef of NReference.reference (* Syntax pattern extensions *) @@ -100,11 +103,12 @@ type 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 case_pattern = + Pattern of string * href option * term capture_variable list + | Wildcard and box_kind = H | V | HV | HOV and box_spec = box_kind * bool * bool (* kind, spacing, indent *) @@ -117,13 +121,17 @@ and layout_pattern = | Frac of term * term | Over of term * term | Atop of term * term + | InfRule of term * term * term (* | array of term * literal option * literal option |+ column separator, row separator +| *) + | Maction of term list | Sqrt of term | Root of term * term (* argument, index *) | Break | Box of box_spec * term list | Group of term list + | Mstyle of (string * string) list * term list + | Mpadded of (string * string) list * term list and magic_term = (* level 1 magics *) @@ -138,11 +146,13 @@ and magic_term = | Fail | If of term * term * term (* test, pattern if true, pattern if false *) +and term_level = Self of int | Level of int + and pattern_variable = (* level 1 and 2 variables *) | NumVar of string | IdentVar of string - | TermVar of string + | TermVar of string * term_level (* level 1 variables *) | Ascription of term * string @@ -155,6 +165,7 @@ type argument_pattern = type cic_appl_pattern = | UriPattern of UriManager.uri + | NRefPattern of NReference.reference | VarPattern of string | ImplicitPattern | ApplPattern of cic_appl_pattern list @@ -163,10 +174,10 @@ type cic_appl_pattern = * 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 +type 'term obj = + | Inductive of 'term capture_variable list * 'term inductive_type list (** parameters, list of loc * mutual inductive types *) - | Theorem of Cic.object_flavour * string * term * term option + | 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 @@ -174,7 +185,7 @@ type obj = * will be given in proof editing mode using the tactical language, * unless the flavour is an Axiom *) - | Record of (string * term) list * string * term * (string * term * bool) list + | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list (** left parameters, name, type, fields *) (** {2 Standard precedences} *) @@ -184,8 +195,3 @@ 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 -