From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- interp/notation.mli | 170 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 170 insertions(+) create mode 100644 interp/notation.mli (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli new file mode 100644 index 00000000..32ec7a96 --- /dev/null +++ b/interp/notation.mli @@ -0,0 +1,170 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +(* Open scope *) + +val current_scopes : unit -> scopes +val open_close_scope : + (* locality *) bool * (* open *) bool * scope_name -> unit + +(* Extend a list of scopes *) +val empty_scope_stack : scopes +val push_scope : scope_name -> scopes -> scopes + +(* 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 *) + +(* 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 * string +type required_module = section_path * string list +type cases_pattern_status = bool (* true = use prim token in patterns *) + +type 'a prim_token_interpreter = + loc -> 'a -> rawconstr + +type 'a prim_token_uninterpreter = + rawconstr list * (rawconstr -> 'a option) * cases_pattern_status + +val declare_numeral_interpreter : scope_name -> required_module -> + bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit + +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 + given scope context*) + +val interp_prim_token : loc -> prim_token -> scope_name list -> + rawconstr * (notation_location * scope_name option) +val interp_prim_token_cases_pattern : loc -> prim_token -> name -> + scope_name list -> cases_pattern * (notation_location * scope_name option) + +(* 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 +val uninterp_prim_token_cases_pattern : + cases_pattern -> name * scope_name * prim_token + +val availability_of_prim_token : + scope_name -> scopes -> delimiters option option + +(*s Declare and interpret back and forth a notation *) + +(* Binds a notation in a given scope to an interpretation *) +type interp_rule = + | NotationRule of scope_name option * notation + | SynDefRule of kernel_name + +val declare_notation_interpretation : notation -> scope_name option -> + interpretation -> notation_location -> unit + +val declare_uninterpretation : interp_rule -> interpretation -> unit + +(* Return the interpretation bound to a notation *) +val interp_notation : loc -> notation -> scope_name list -> + interpretation * (notation_location * scope_name option) + +(* Return the possible notations for a given term *) +val uninterp_notations : rawconstr -> + (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 *) +val availability_of_notation : scope_name option * notation -> scopes -> + (scope_name option * delimiters option) option + +(*s 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 *) + +(*s** Miscellaneous *) + +(* 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 *) +val declare_arguments_scope: global_reference -> scope_name option list -> unit +val find_arguments_scope : global_reference -> scope_name option list + +val declare_class_scope : scope_name -> Classops.cl_typ -> unit +val declare_ref_arguments_scope : global_reference -> unit + +val compute_arguments_scope : Term.types -> scope_name option list + +(* Building notation key *) + +type symbol = + | Terminal of string + | NonTerminal of identifier + | SProdList of identifier * symbol list + | Break of int + +val make_notation_key : symbol list -> notation +val decompose_notation_key : notation -> symbol list + +(* Prints scopes (expect 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 -> std_ppcmds + +val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds + +(**********************************************************************) +(*s Printing rules for 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 *) -- cgit v1.2.3