diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /interp/notation.mli | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'interp/notation.mli')
-rw-r--r-- | interp/notation.mli | 95 |
1 files changed, 45 insertions, 50 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 33ffe7b4..f92ef94e 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,36 +1,31 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: notation.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Pp open Bigint open Names open Nametab open Libnames -open Rawterm +open Glob_term open Topconstr open Ppextend -(*i*) - -(**********************************************************************) -(* Scopes *) +(** Notations *) -(*s A scope is a set of interpreters for symbols + optional +(** {6 Scopes } *) +(** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) type level = precedence * tolerability list type delimiters = string type scope -type scopes (* = [scope_name list] *) +type scopes (** = [scope_name list] *) type local_scopes = tmp_scope_name option * scope_name list @@ -39,41 +34,43 @@ val declare_scope : scope_name -> unit val current_scopes : unit -> scopes -(* Check where a scope is opened or not in a scope list, or in +(** Check where a scope is opened or not in a scope list, or in * the current opened scopes *) val scope_is_open_in_scopes : scope_name -> scopes -> bool val scope_is_open : scope_name -> bool -(* Open scope *) +(** Open scope *) val open_close_scope : - (* locality *) bool * (* open *) bool * scope_name -> unit + (** locality *) bool * (* open *) bool * scope_name -> unit -(* Extend a list of scopes *) +(** Extend a list of scopes *) val empty_scope_stack : scopes val push_scope : scope_name -> scopes -> scopes -(* Declare delimiters for printing *) +val find_scope : scope_name -> scope + +(** Declare delimiters for printing *) val declare_delimiters : scope_name -> delimiters -> unit val find_delimiters_scope : loc -> delimiters -> scope_name -(*s Declare and uses back and forth an interpretation of primitive token *) +(** {6 Declare and uses back and forth an interpretation of primitive token } *) -(* A numeral interpreter is the pair of an interpreter for **integer** +(** A numeral interpreter is the pair of an interpreter for **integer** numbers in terms and an optional interpreter in pattern, if negative numbers are not supported, the interpreter must fail with an appropriate error message *) type notation_location = (dir_path * dir_path) * string type required_module = full_path * string list -type cases_pattern_status = bool (* true = use prim token in patterns *) +type cases_pattern_status = bool (** true = use prim token in patterns *) type 'a prim_token_interpreter = - loc -> 'a -> rawconstr + loc -> 'a -> glob_constr type 'a prim_token_uninterpreter = - rawconstr list * (rawconstr -> 'a option) * cases_pattern_status + glob_constr list * (glob_constr -> 'a option) * cases_pattern_status val declare_numeral_interpreter : scope_name -> required_module -> bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit @@ -81,28 +78,28 @@ val declare_numeral_interpreter : scope_name -> required_module -> val declare_string_interpreter : scope_name -> required_module -> string prim_token_interpreter -> string prim_token_uninterpreter -> unit -(* Return the [term]/[cases_pattern] bound to a primitive token in a +(** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) val interp_prim_token : loc -> prim_token -> local_scopes -> - rawconstr * (notation_location * scope_name option) + glob_constr * (notation_location * scope_name option) val interp_prim_token_cases_pattern : loc -> prim_token -> name -> local_scopes -> cases_pattern * (notation_location * scope_name option) -(* Return the primitive token associated to a [term]/[cases_pattern]; +(** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) val uninterp_prim_token : - rawconstr -> scope_name * prim_token + glob_constr -> scope_name * prim_token val uninterp_prim_token_cases_pattern : cases_pattern -> name * scope_name * prim_token val availability_of_prim_token : prim_token -> scope_name -> local_scopes -> delimiters option option -(*s Declare and interpret back and forth a notation *) +(** {6 Declare and interpret back and forth a notation } *) -(* Binds a notation in a given scope to an interpretation *) +(** Binds a notation in a given scope to an interpretation *) type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of kernel_name @@ -112,39 +109,39 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit -(* Return the interpretation bound to a notation *) +(** Return the interpretation bound to a notation *) val interp_notation : loc -> notation -> local_scopes -> interpretation * (notation_location * scope_name option) -(* Return the possible notations for a given term *) -val uninterp_notations : rawconstr -> +(** Return the possible notations for a given term *) +val uninterp_notations : glob_constr -> (interp_rule * interpretation * int option) list val uninterp_cases_pattern_notations : cases_pattern -> (interp_rule * interpretation * int option) list -(* Test if a notation is available in the scopes *) -(* context [scopes]; if available, the result is not None; the first *) -(* argument is itself not None if a delimiters is needed *) +(** Test if a notation is available in the scopes + context [scopes]; if available, the result is not None; the first + argument is itself not None if a delimiters is needed *) val availability_of_notation : scope_name option * notation -> local_scopes -> (scope_name option * delimiters option) option -(*s Declare and test the level of a (possibly uninterpreted) notation *) +(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) val declare_notation_level : notation -> level -> unit -val level_of_notation : notation -> level (* raise [Not_found] if no level *) +val level_of_notation : notation -> level (** raise [Not_found] if no level *) -(*s** Miscellaneous *) +(** {6 Miscellaneous} *) val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> notation -> delimiters option -> global_reference -(* Checks for already existing notations *) +(** Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> interpretation -> bool -(* Declares and looks for scopes associated to arguments of a global ref *) +(** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : - bool (* true=local *) -> global_reference -> scope_name option list -> unit + bool (** true=local *) -> global_reference -> scope_name option list -> unit val find_arguments_scope : global_reference -> scope_name option list @@ -153,7 +150,7 @@ val declare_ref_arguments_scope : global_reference -> unit val compute_arguments_scope : Term.types -> scope_name option list -(* Building notation key *) +(** Building notation key *) type symbol = | Terminal of string @@ -164,21 +161,19 @@ type symbol = val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list -(* Prints scopes (expects a pure aconstr printer) *) -val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds -val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds -val locate_notation : (rawconstr -> std_ppcmds) -> notation -> +(** Prints scopes (expects a pure aconstr printer) *) +val pr_scope : (glob_constr -> std_ppcmds) -> scope_name -> std_ppcmds +val pr_scopes : (glob_constr -> std_ppcmds) -> std_ppcmds +val locate_notation : (glob_constr -> std_ppcmds) -> notation -> scope_name option -> std_ppcmds -val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds +val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmds -(**********************************************************************) -(*s Printing rules for notations *) +(** {6 Printing rules for notations} *) -(* Declare and look for the printing rule for symbolic notations *) +(** Declare and look for the printing rule for symbolic notations *) type unparsing_rule = unparsing list * precedence val declare_notation_printing_rule : notation -> unparsing_rule -> unit val find_notation_printing_rule : notation -> unparsing_rule -(**********************************************************************) -(* Rem: printing rules for primitive token are canonical *) +(** Rem: printing rules for primitive token are canonical *) |