From 8659ff43db85c43df644da6ac08509374aabcad4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 11 Nov 2009 10:55:32 +0000 Subject: Improving abbreviations/notations + backtrack of semantic change in r12439 - Deactivation of short names registration and printing for abbreviations to identical names, what avoids printing uselessly qualified names binding where the short name is in fact equivalent. - New treatment of abbreviations to names: don't insert any maximally inserted implicit arguments at all at the time of the abbreviation and use the regular internalization strategy to have them inserted at use time. - The previous modifications altogether make redirections of qualified names easier and avoid the semantic change of r12349 and hence allows to keep "Notation b := @a" as it was before, i.e. as a notation for the deactivation of the implicit arguments of a. - Took benefit of these changes and updated nil/cons/list/app redefinition in "List.v". - Fixed parsing/printing notation bugs (loop on partially applied abreviations for constructors in constrintern.ml + bad reverting of notations with holes that captured non anonymous variables in match_cases_pattern). - Add support for parsing/printing abbreviations to @-like constructors and for reverting printing for abbreviations to constructors applied to parameters only (function extern_symbol_pattern). - Minor error messages fixes and minor APIs cleaning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/syntax_def.ml | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) (limited to 'interp/syntax_def.ml') diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b0e27f04e..245ed0f50 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -38,15 +38,25 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) = add_syntax_constant kn pat; Nametab.push_syndef (Nametab.Until i) sp kn +let is_alias_of_already_visible_name sp = function + | _,ARef ref -> + let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in + dir = empty_dirpath && id = basename sp + | _ -> + false + let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = - Nametab.push_syndef (Nametab.Exactly i) sp kn; - if not onlyparse then - (* Redeclare it to be used as (short) name in case an other (distfix) - notation was declared inbetween *) - Notation.declare_uninterpretation (Notation.SynDefRule kn) pat + if not (is_alias_of_already_visible_name sp pat) then begin + Nametab.push_syndef (Nametab.Exactly i) sp kn; + if not onlyparse then + (* Redeclare it to be used as (short) name in case an other (distfix) + notation was declared inbetween *) + Notation.declare_uninterpretation (Notation.SynDefRule kn) pat + end let cache_syntax_constant d = - load_syntax_constant 1 d + load_syntax_constant 1 d; + open_syntax_constant 1 d let subst_syntax_constant (subst,(local,pat,onlyparse)) = (local,subst_interpretation subst pat,onlyparse) @@ -72,5 +82,5 @@ let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let search_syntactic_definition loc kn = +let search_syntactic_definition kn = out_pat (KNmap.find kn !syntax_table) -- cgit v1.2.3