Ajout de Print Visibility

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4733 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 135 insertions, 21 deletions

diff --git a/interp/symbols.ml b/interp/symbols.ml
index e6247c65a3..cd0ac0aa13 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -58,8 +58,8 @@ let empty_scope = {
   delimiters = None
 }
 
-let default_scope = "core_scope"
-let type_scope = "type_scope"
+let default_scope = "" (* empty name, not available from outside *)
+let type_scope = "type_scope" (* special scope used for interpreting types *)
 
 let init_scope_map () =
   scope_map := Stringmap.add default_scope empty_scope !scope_map;
@@ -86,7 +86,7 @@ let check_scope sc = let _ = find_scope sc in ()
 type scope_elem = Scope of scope_name | SingleNotation of string
 type scopes = scope_elem list
 
-let scope_stack = ref [Scope default_scope; Scope type_scope]
+let scope_stack = ref []
 
 let current_scopes () = !scope_stack
 
@@ -468,8 +468,13 @@ let pr_notation_info prraw ntn c =
   str "\"" ++ str ntn ++ str "\" := " ++ prraw (rawconstr_of_aconstr () c)
 
 let pr_named_scope prraw scope sc =
-  str "Scope " ++ str scope ++ fnl ()
-  ++ pr_delimiters_info sc.delimiters ++ fnl ()
+ (if scope = default_scope then
+   match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
+     | 0 -> str "No lonely notation"
+     | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
+  else 
+    str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
+  ++ fnl ()
   ++ pr_scope_classes scope
   ++ Stringmap.fold
        (fun ntn ((_,r),df,_) strm ->
@@ -539,6 +544,55 @@ let locate_notation prraw ntn =
 	    ++ fnl ()))
 	l) ntns)
 
+let collect_notation_in_scope scope sc known =
+  assert (scope <> default_scope);
+  Stringmap.fold
+    (fun ntn ((_,r),df,_) (l,known as acc) ->
+      if List.mem ntn known then acc else ((df,r)::l,ntn::known))
+    sc.notations ([],known)
+
+let collect_notations stack =
+  fst (List.fold_left
+    (fun (all,knownntn as acc) -> function
+      | Scope scope ->
+	  if List.mem_assoc scope all then acc
+	  else
+	    let (l,knownntn) =
+	      collect_notation_in_scope scope (find_scope scope) knownntn in
+	    ((scope,l)::all,knownntn)
+      | SingleNotation ntn ->
+	  if List.mem ntn knownntn then (all,knownntn)
+	  else
+	    let ((_,r),df,_) =
+	      Stringmap.find ntn (find_scope default_scope).notations in
+	    let all' = match all with
+	      | (s,lonelyntn)::rest when s = default_scope ->
+		  (s,(df,r)::lonelyntn)::rest
+	      | _ -> 
+		  (default_scope,[df,r])::all in
+	    (all',ntn::knownntn))
+    ([],[]) stack)
+
+let pr_visible_in_scope prraw (scope,ntns) =
+  let strm =
+    List.fold_right
+      (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
+      ntns (mt ()) in
+  (if scope = default_scope then
+     str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt())
+   else 
+     str "Visible in scope " ++ str scope)
+  ++ fnl () ++ strm
+
+let pr_scope_stack prraw stack = 
+  List.fold_left
+    (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ())
+    (mt ()) (collect_notations stack)
+
+let pr_visibility prraw = function
+  | Some scope -> pr_scope_stack prraw (push_scope scope !scope_stack)
+  | None -> pr_scope_stack prraw !scope_stack
+
 (**********************************************************************)
 (* Mapping notations to concrete syntax *)
 
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 3ddb7d22ed..711e81cc27 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -32,9 +32,6 @@ type delimiters = string
 type scope
 type scopes (* = scope_name list*)
 
-(*
-val default_scope : scope_name
-*)
 val type_scope : scope_name
 val declare_scope : scope_name -> unit
 
@@ -136,6 +133,8 @@ 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 *)
 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 778aef105a..e4ce693c2e 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -195,7 +195,8 @@ GEXTEND Gram
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
       | IDENT "Scopes" -> PrintScopes
-      | IDENT "Scope"; s = IDENT -> PrintScope s ] ]
+      | IDENT "Scope"; s = IDENT -> PrintScope s
+      | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s ] ]
   ;
   locatable:
     [ [ qid = global -> LocateTerm qid
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 56edd95269..9ff07141c8 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -608,7 +608,8 @@ GEXTEND Gram
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
       | IDENT "Scopes" -> PrintScopes
-      | IDENT "Scope"; s = IDENT -> PrintScope s ] ]
+      | IDENT "Scope"; s = IDENT -> PrintScope s
+      | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index f1ceda650a..5960bbc049 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -752,13 +752,6 @@ let interp_infix_modifiers modl =
     error "explicit entry level or type unexpected in infix notation";
   (assoc,level,b,fmt)
 
-(* Notation defaults to NONA *)
-let interp_notation_modifiers modl =
-  let (assoc,n,t,b,format) = interp_modifiers modl in
-  let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
-  let n = match n with None -> 1 | Some n -> n in
-  (assoc,n,t,b,format)
-
 (* 2nd list of types has priority *)
 let rec merge_entry_types etyps' = function
   | [] -> etyps'
@@ -768,8 +761,6 @@ let rec merge_entry_types etyps' = function
 let set_entry_type etyps (x,typ) =
   let typ = try 
     match List.assoc x etyps, typ with
-      | _, (_,BorderProd (true,_)) ->
-	  error "The level of the leftmost non-terminal cannot be changed"
       | ETConstr (n,()), (_,BorderProd (left,_)) ->
           ETConstr (n,BorderProd (left,None))
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
@@ -777,11 +768,63 @@ let set_entry_type etyps (x,typ) =
     with Not_found -> ETConstr typ
   in (x,typ)
 
+let check_rule_reversibility l = 
+  if List.for_all (function NonTerminal _ -> true | _ -> false) l then
+    error "A notation must include at least one symbol"
+
+let find_precedence_v7 lev etyps symbols =
+  (match symbols with
+    | NonTerminal x :: _ ->
+	(try match List.assoc x etyps with
+	  | ETConstr _ ->
+	      error "The level of the leftmost non-terminal cannot be changed"
+	  | _ -> ()
+	with Not_found -> ())
+    | _ -> ());
+  if lev = None then 1 else out_some lev
+
+let find_precedence lev etyps symbols =
+  match symbols with
+  | NonTerminal x :: _ ->
+      (try match List.assoc x etyps with
+	| ETConstr _ ->
+	    error "The level of the leftmost non-terminal cannot be changed"
+	| ETIdent | ETBigint | ETReference -> 
+	    if lev = None then 
+	      Options.if_verbose msgnl (str "Setting notation at level 0")
+	    else
+	    if lev <> Some 0 then
+	      error "A notation starting with an atomic expression must be at level 0";
+	    0
+	| ETPattern | ETOther _ -> (* Give a default ? *)
+	    if lev = None then
+	      error "Need an explicit level"
+	    else out_some lev
+      with Not_found -> 
+	if lev = None then
+	  error "A left-recursive notation must have an explicit level"
+	else out_some lev)
+  | Terminal _ ::l when
+      (match list_last symbols with Terminal _ -> true |_ -> false)
+      -> 
+      if lev = None then
+	(Options.if_verbose msgnl (str "Setting notation at level 0"); 0)
+      else out_some lev
+  | _ ->
+      if lev = None then error "Cannot determine the level";
+      out_some lev
+
 let compute_syntax_data forv7 (df,modifiers) =
-  let (assoc,n,etyps,onlyparse,fmt) = interp_notation_modifiers modifiers in
+  let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
+  (* Notation defaults to NONA *)
+  let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
   let toks = split df in
   let innerlevel = NumLevel (if forv7 then 10 else 200) in
   let (vars,symbols) = analyse_tokens toks in
+  check_rule_reversibility symbols;
+  let n =
+    if !Options.v7 then find_precedence_v7 n etyps symbols
+    else find_precedence n etyps symbols in
   let typs =
     find_symbols
       (NumLevel n,BorderProd(true,assoc))
@@ -924,6 +967,13 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
 
 let level_rule (n,p) = if p = E then n else max (n-1) 0
 
+let check_notation_existence notation =
+  try
+    let a,_ = Symbols.level_of_notation notation in
+    if a = None then raise Not_found
+  with Not_found ->
+    error "Parsing rule for this notation has to be previously declared"
+
 let build_old_pp_rule notation scope symbs (r,vars) =
   let prec = 
     try
@@ -940,12 +990,15 @@ let add_notation_interpretation_core local symbs for_old df a scope onlyparse
   onlypp =
   let notation = make_anon_notation symbs in
   let old_pp_rule = 
-    option_app (build_old_pp_rule notation scope symbs) for_old in
+    if !Options.v7 then 
+      option_app (build_old_pp_rule notation scope symbs) for_old
+    else None in
   Lib.add_anonymous_leaf
     (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp,df))
 
 let add_notation_interpretation df names c sc =
   let (vars,symbs) = analyse_tokens (split df) in
+  check_notation_existence (make_anon_notation symbs);
   let a = interp_aconstr names vars c in
   let a_for_old = interp_rawconstr_with_implicits (Global.env()) vars names c 
   in
@@ -1017,6 +1070,7 @@ let add_notation local c dfmod mv8 sc =
 	      else
 	        (* Declare only interpretation *)
 		let (vars,symbs) = analyse_tokens toks in
+		check_notation_existence (make_anon_notation symbs);
 		let onlyparse = modifiers = [SetOnlyParsing] in
 		let a = interp_aconstr [] vars c in
 		let a_for_old = interp_global_rawconstr_with_vars vars c in
@@ -1098,6 +1152,7 @@ let add_infix local (inf,modl) pr mv8 sc =
     (* de ne déclarer que l'interprétation *)
     (* Declare only interpretation *)
     let (vars,symbs) = analyse_tokens toks in
+    check_notation_existence (make_anon_notation symbs);
     let a' = interp_aconstr [] vars a in
     let a_for_old = interp_global_rawconstr_with_vars vars a in
     let for_old = Some (a_for_old,vars) in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 82318340cc..c5cbb206f3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -867,6 +867,8 @@ let vernac_print = function
       pp (Symbols.pr_scopes (Constrextern.without_symbols pr_rawterm))
   | PrintScope s ->
       pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s)
+  | PrintVisibility s ->
+      pp (Symbols.pr_visibility (Constrextern.without_symbols pr_rawterm) s)
   | PrintAbout qid -> msgnl (print_about qid)
 
 let global_module r =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 06dae38155..042845dc6d 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -53,6 +53,7 @@ type printable =
   | PrintHintDb
   | PrintScopes
   | PrintScope of string
+  | PrintVisibility of string option
   | PrintAbout of reference
 
 type search_about_item =
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 3eaaeb0ead..ff8f236764 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1014,6 +1014,7 @@ let rec pr_vernac = function
 	| PrintInspect n -> str"Inspect" ++ spc() ++ int n
 	| PrintScopes -> str"Print Scopes"
 	| PrintScope s -> str"Print Scope" ++ spc() ++ str s 
+	| PrintVisibility s -> str"Print Visibility" ++ pr_opt str s 
 	| PrintAbout qid -> str"About" ++ spc()  ++ pr_reference qid
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern