From ea85f46dc0cc34db149c24bb2da8f3130e191fc1 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 11 Sep 2009 17:53:30 +0000 Subject: Generalized the possibility to refer to a global name by a notation string in most commands expecting a global name (e.g. 'Print "+"' for an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly surrounded by a scope delimiter). Support for such smart globals in VERNAC EXTEND to do. Added a file smartlocate.ml for high-level globalization functions. Mini-nettoyage metasyntax.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/coqlib.ml | 2 +- interp/genarg.ml | 6 ++++- interp/genarg.mli | 4 +++- interp/interp.mllib | 3 ++- interp/notation.ml | 7 +++--- interp/notation.mli | 3 ++- interp/smartlocate.ml | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++ interp/smartlocate.mli | 37 ++++++++++++++++++++++++++++++ interp/syntax_def.ml | 26 --------------------- interp/syntax_def.mli | 16 ------------- 10 files changed, 116 insertions(+), 50 deletions(-) create mode 100644 interp/smartlocate.ml create mode 100644 interp/smartlocate.mli (limited to 'interp') diff --git a/interp/coqlib.ml b/interp/coqlib.ml index d38ef592fc..6879dc9659 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -15,7 +15,7 @@ open Term open Libnames open Pattern open Nametab -open Syntax_def +open Smartlocate (************************************************************************) (* Generic functions to find Coq objects *) diff --git a/interp/genarg.ml b/interp/genarg.ml index 8724b0bfd6..c6dc12164e 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -47,7 +47,11 @@ type argument_type = type 'a and_short_name = 'a * identifier located option type 'a or_by_notation = | AN of 'a - | ByNotation of loc * string * Notation.delimiters option + | ByNotation of (loc * string * Notation.delimiters option) + +let loc_of_or_by_notation f = function + | AN c -> f c + | ByNotation (loc,s,_) -> loc type rawconstr_and_expr = rawconstr * constr_expr option type open_constr_expr = unit * constr_expr diff --git a/interp/genarg.mli b/interp/genarg.mli index 9072456c3e..e6747db171 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -21,7 +21,9 @@ type 'a and_short_name = 'a * identifier located option type 'a or_by_notation = | AN of 'a - | ByNotation of loc * string * Notation.delimiters option + | ByNotation of (loc * string * Notation.delimiters option) + +val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) (* in the environment by the effective calls to Intro, Inversion, etc *) diff --git a/interp/interp.mllib b/interp/interp.mllib index 234487bc9d..991cfac57b 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -4,7 +4,8 @@ Ppextend Notation Dumpglob Genarg -Syntax_def +Syntax_def +Smartlocate Reserve Impargs Implicit_quantifiers diff --git a/interp/notation.ml b/interp/notation.ml index 08936759dd..58c28149dd 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -536,7 +536,7 @@ let decompose_notation_key s = let tok = match String.sub s n (pos-n) with | "_" -> NonTerminal (id_of_string "_") - | s -> Terminal s in + | s -> Terminal (drop_simple_quotes s) in decomp_ntn (tok::dirs) (pos+1) in decomp_ntn [] 0 @@ -650,15 +650,16 @@ let interp_notation_as_global_reference loc test ntn sc = | [] -> error_notation_not_reference loc ntn | _ -> error_ambiguous_notation loc ntn -let locate_notation prraw ntn = +let locate_notation prraw ntn scope = let ntns = factorize_entries (browse_notation false ntn !scope_map) in + let scopes = Option.fold_right push_scope scope !scope_stack in if ntns = [] then str "Unknown notation" else t (str "Notation " ++ tab () ++ str "Scope " ++ tab () ++ fnl () ++ prlist (fun (ntn,l) -> - let scope = find_default ntn !scope_stack in + let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> hov 0 ( diff --git a/interp/notation.mli b/interp/notation.mli index 21d3ae1a08..57e0deb10a 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -167,7 +167,8 @@ 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 locate_notation : (rawconstr -> std_ppcmds) -> notation -> + scope_name option -> std_ppcmds val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml new file mode 100644 index 0000000000..07ae87fa08 --- /dev/null +++ b/interp/smartlocate.ml @@ -0,0 +1,62 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ref + | SynDef kn -> + match search_syntactic_definition dummy_loc kn with + | [],ARef ref -> ref + | _ -> raise Not_found + +let locate_global_with_alias (loc,qid) = + let ref = Nametab.locate_extended qid in + try global_of_extended_global ref + with Not_found -> + user_err_loc (loc,"",pr_qualid qid ++ + str " is bound to a notation that does not denote a reference") + +let global_inductive_with_alias r = + match locate_global_with_alias (qualid_of_reference r) with + | IndRef ind -> ind + | ref -> + user_err_loc (loc_of_reference r,"global_inductive", + pr_reference r ++ spc () ++ str "is not an inductive type") + +let global_with_alias r = + let (loc,qid as lqid) = qualid_of_reference r in + try locate_global_with_alias lqid + with Not_found -> Nametab.error_global_not_found_loc loc qid + +let smart_global = function + | AN r -> + global_with_alias r + | ByNotation (loc,ntn,sc) -> + Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc + +let smart_global_inductive = function + | AN r -> + global_inductive_with_alias r + | ByNotation (loc,ntn,sc) -> + destIndRef + (Notation.interp_notation_as_global_reference loc isIndRef ntn sc) diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli new file mode 100644 index 0000000000..682484f57f --- /dev/null +++ b/interp/smartlocate.mli @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* global_reference + +(* Extract a global_reference from a reference that can be an "alias" *) +val global_of_extended_global : extended_global_reference -> global_reference + +(* Locate a reference taking into account possible "alias" notations *) +val global_with_alias : reference -> global_reference + +(* The same for inductive types *) +val global_inductive_with_alias : reference -> inductive + +(* Locate a reference taking into account notations and "aliases" *) +val smart_global : reference or_by_notation -> global_reference + +(* The same for inductive types *) +val smart_global_inductive : reference or_by_notation -> inductive + diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 1619bad278..e58bb000a0 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -81,29 +81,3 @@ let declare_syntactic_definition local id onlyparse pat = let search_syntactic_definition loc kn = out_pat (KNmap.find kn !syntax_table) - -let global_of_extended_global = function - | TrueGlobal ref -> ref - | SynDef kn -> - match search_syntactic_definition dummy_loc kn with - | [],ARef ref -> ref - | _ -> raise Not_found - -let locate_global_with_alias (loc,qid) = - let ref = Nametab.locate_extended qid in - try global_of_extended_global ref - with Not_found -> - user_err_loc (loc,"",pr_qualid qid ++ - str " is bound to a notation that does not denote a reference") - -let global_inductive_with_alias r = - match locate_global_with_alias (qualid_of_reference r) with - | IndRef ind -> ind - | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type") - -let global_with_alias r = - let (loc,qid as lqid) = qualid_of_reference r in - try locate_global_with_alias lqid - with Not_found -> Nametab.error_global_not_found_loc loc qid diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index fb0c3c9f28..3ba78e91d9 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -25,19 +25,3 @@ val declare_syntactic_definition : bool -> identifier -> bool -> syndef_interpretation -> unit val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation - -(* [locate_global_with_alias] locates global reference possibly following - a notation if this notation has a role of aliasing; raise Not_found - if not bound in the global env; raise an error if bound to a - syntactic def that does not denote a reference *) - -val locate_global_with_alias : qualid located -> global_reference - -(* Extract a global_reference from a reference that can be an "alias" *) -val global_of_extended_global : extended_global_reference -> global_reference - -(* Locate a reference taking into account possible "alias" notations *) -val global_with_alias : reference -> global_reference - -(* The same for inductive types *) -val global_inductive_with_alias : reference -> inductive -- cgit v1.2.3