diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /intf/notation_term.ml | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'intf/notation_term.ml')
-rw-r--r-- | intf/notation_term.ml | 123 |
1 files changed, 0 insertions, 123 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml deleted file mode 100644 index af9d6918..00000000 --- a/intf/notation_term.ml +++ /dev/null @@ -1,123 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Globnames -open Misctypes -open Glob_term - -(** [notation_constr] *) - -(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic - extensions (i.e. notations). - No location since intended to be substituted at any place of a text. - Complex expressions such as fixpoints and cofixpoints are excluded, - as well as non global expressions such as existential variables. *) - -type notation_constr = - (** Part common to [glob_constr] and [cases_pattern] *) - | NRef of global_reference - | NVar of Id.t - | NApp of notation_constr * notation_constr list - | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool - (** Part only in [glob_constr] *) - | NLambda of Name.t * notation_constr * notation_constr - | NProd of Name.t * notation_constr * notation_constr - | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool - | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr - | NCases of Constr.case_style * notation_constr option * - (notation_constr * (Name.t * (inductive * Name.t list) option)) list * - (cases_pattern list * notation_constr) list - | NLetTuple of Name.t list * (Name.t * notation_constr option) * - notation_constr * notation_constr - | NIf of notation_constr * (Name.t * notation_constr option) * - notation_constr * notation_constr - | NRec of fix_kind * Id.t array * - (Name.t * notation_constr option * notation_constr) list array * - notation_constr array * notation_constr array - | NSort of glob_sort - | NCast of notation_constr * notation_constr cast_type - -(** Note concerning NList: first constr is iterator, second is terminator; - first id is where each argument of the list has to be substituted - in iterator and snd id is alternative name just for printing; - boolean is associativity *) - -(** Types concerning notations *) - -type scope_name = string - -type tmp_scope_name = scope_name - -type subscopes = tmp_scope_name option * scope_name list - -(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, - x carries the sequence of objects bound to the list x..y *) - -type notation_binder_source = - (* This accepts only pattern *) - (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) - | NtnParsedAsPattern of bool - (* This accepts only ident *) - | NtnParsedAsIdent - (* This accepts ident, or pattern, or both *) - | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind - -type notation_var_instance_type = - | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList - -(** Type of variables when interpreting a constr_expr as a notation_constr: - in a recursive pattern x..y, both x and y carry the individual type - of each element of the list x..y *) -type notation_var_internalization_type = - | NtnInternTypeAny | NtnInternTypeOnlyBinder - -(** This characterizes to what a notation is interpreted to *) -type interpretation = - (Id.t * (subscopes * notation_var_instance_type)) list * - notation_constr - -type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list - -type notation_interp_env = { - ninterp_var_type : notation_var_internalization_type Id.Map.t; - ninterp_rec_vars : Id.t Id.Map.t; -} - -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool * int - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list when true; additionally release - the p last items as if they were parsed autonomously *) - -(** Dealing with precedences *) - -type precedence = int -type parenRelation = L | E | Any | Prec of precedence -type tolerability = precedence * parenRelation - -type level = precedence * tolerability list * Extend.constr_entry_key list - -(** Grammar rules for a notation *) - -type one_notation_grammar = { - notgram_level : level; - notgram_assoc : Extend.gram_assoc option; - notgram_notation : Constrexpr.notation; - notgram_prods : grammar_constr_prod_item list list; -} - -type notation_grammar = { - notgram_onlyprinting : bool; - notgram_rules : one_notation_grammar list -} |