Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool

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

4 files changed, 37 insertions, 20 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 67eb2d379d..cb05a5c7d2 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -207,7 +207,7 @@ let prec_assoc = function
 
 let constr_tab =
   [| "constr0"; "constr1"; "constr2"; "constr3"; "lassoc_constr4";
-     "constr5"; "constr6"; "constr7"; "constr8"; "constr9"; "constr10";
+     "constr5"; "constr6"; "constr7"; "constr8"; "constr9"; "lconstr";
      "pattern" |]
   
 let constr_rule (n,p) =
@@ -237,8 +237,11 @@ let make_hunks symbols =
 	  UNP_BRK (n, 1) :: RO s :: l)
     symbols []
 
+let string_of_prec (n,p) =
+  (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")
+
 let string_of_symbol = function
-  | NonTerminal _ -> "_"
+  | NonTerminal (lp,_) -> "_:"^(string_of_prec lp)
   | Terminal s -> s
 
 let string_of_assoc = function
@@ -285,24 +288,29 @@ let strip s =
   let n = String.length s in
   if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
 
-let rec find_symbols c_first c_next c_last vars new_var = function
+let rec find_symbols c_first c_next c_last vars new_var varprecl = function
   | []    -> (vars, [])
   | x::sl when is_letter x.[0] ->
       let id = Names.id_of_string x in
       if List.mem_assoc id vars then
         error ("Variable "^x^" occurs more than once");
-      let prec = if sl = [] then c_last else c_first in
-      let (vars,l) = find_symbols c_next c_next c_last vars (new_var+1) sl in
+      let prec =
+        try (List.assoc x varprecl,E)
+        with Not_found -> if sl = [] then c_last else c_first in
+      let (vars,l) =
+        find_symbols c_next c_next c_last vars (new_var+1) varprecl sl in
       let meta = create_meta new_var in
       ((id,ope ("META",[num new_var]))::vars, NonTerminal (prec, meta) :: l)
   | "_"::sl ->
       warning "Found '_'";
       let prec = if sl = [] then c_last else c_first in
-      let (vars,l) = find_symbols c_next c_next c_last vars (new_var+1) sl in
+      let (vars,l) =
+        find_symbols c_next c_next c_last vars (new_var+1) varprecl sl in
       let meta = create_meta new_var in
       (vars, NonTerminal (prec, meta) :: l)
   | s :: sl ->
-      let (vars,l) = find_symbols c_next c_next c_last vars new_var sl in
+      let (vars,l) =
+        find_symbols c_next c_next c_last vars new_var varprecl sl in
       (vars, Terminal (strip s) :: l)
 
 let make_grammar_pattern symbols ntn =
@@ -365,10 +373,11 @@ let rec reify_meta_ast = function
 
 (* Distfix, Infix, Notations *)
 
-let add_notation assoc n df ast sc =
+let add_notation assoc n df ast varprecl sc =
   let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
   let (lp,rp) = prec_assoc assoc in
-  let (subst,symbols) = find_symbols (n,lp) (n,L) (n,rp) [] 1 (split df) in
+  let (subst,symbols) =
+    find_symbols (n,lp) (10,E) (n,rp) [] 1 varprecl (split df) in
   let notation = make_symbolic assoc n symbols in
   let rule_name = notation^"_"^scope^"_notation" in
   (* To globalize... *)
@@ -403,7 +412,7 @@ let add_distfix assoc n df astf sc =
   let (vars,l) = rename "x" [] 1 (split df) in
   let df = String.concat " " l in
   let ast = ope("APPLIST",astf::vars) in
-  add_notation assoc n df ast sc
+  add_notation assoc n df ast [] sc
 
 let add_infix assoc n inf qid sc =
   let pr = Astterm.globalize_qualid qid in
@@ -418,7 +427,7 @@ let add_infix assoc n inf qid sc =
   *)
   let metas = [inject_var "x"; inject_var "y"] in 
   let ast = ope("APPLIST",pr::metas) in
-  add_notation assoc n ("x "^(quote inf)^" y") ast sc
+  add_notation assoc n ("x "^(quote inf)^" y") ast [] sc
 
 (* Delimiters *)
 let load_delimiters _ (_,(_,_,scope,dlm)) =
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 07d1db0e3c..1b667918ad 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -9,7 +9,10 @@
 (*i $Id$ i*)
 
 (*i*)
+open Util
+open Libnames
 open Extend
+open Tacexpr
 open Vernacexpr
 open Symbols
 (*i*)
@@ -20,19 +23,20 @@ val add_syntax_obj : string -> syntax_entry_ast list -> unit
 
 val add_grammar_obj : string -> grammar_entry_ast list -> unit
 val add_token_obj : string -> unit
-val add_tactic_grammar :  (string * (string * grammar_production list) * Tacexpr.raw_tactic_expr) list -> unit
+val add_tactic_grammar :
+  (string * (string * grammar_production list) * raw_tactic_expr) list -> unit
 
 val add_infix :
-  Gramext.g_assoc option -> int -> string -> Libnames.qualid Util.located
+  Gramext.g_assoc option -> precedence -> string -> qualid located
     -> scope_name option -> unit
 val add_distfix :
-  Gramext.g_assoc option -> int -> string -> Coqast.t 
+  Gramext.g_assoc option -> precedence -> string -> Coqast.t 
     -> scope_name option -> unit
 val add_delimiters : scope_name -> delimiters -> unit
 
 val add_notation : 
-  Gramext.g_assoc option -> int -> string -> Coqast.t
-    -> scope_name option -> unit
+  Gramext.g_assoc option -> precedence -> string -> Coqast.t
+    -> (string * precedence) list -> scope_name option -> unit
 
 val print_grammar : string -> string -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b3825dd932..49aae75bb6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1038,7 +1038,7 @@ let interp c = match c with
   | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
   | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc
   | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc
-  | VernacNotation (assoc,n,inf,c,sc) -> vernac_notation assoc n inf c sc
+  | VernacNotation (assoc,n,inf,c,pl,sc) -> vernac_notation assoc n inf c pl sc
 
   (* Gallina *)
   | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index d2ad10bb6e..7ea61dd6e5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -165,6 +165,7 @@ type local_decl_expr =
   | AssumExpr of identifier * constr_ast
   | DefExpr of identifier * constr_ast * constr_ast option
 
+type precedence = int
 type grammar_entry_ast = 
   (loc * string) * Ast.entry_type option * 
     grammar_associativity * raw_grammar_rule list
@@ -188,11 +189,14 @@ type vernac_expr =
   | VernacDelimiters of scope_name * (string * string)
   | VernacArgumentsScope of qualid located * scope_name option list
   | VernacInfix of
-      grammar_associativity * int * string * qualid located * scope_name option
+      grammar_associativity * precedence * string * qualid located
+      * scope_name option
   | VernacDistfix of
-      grammar_associativity * int * string * qualid located * scope_name option
+      grammar_associativity * precedence * string * qualid located
+      * scope_name option
   | VernacNotation of
-      grammar_associativity * int * string * constr_ast * scope_name option
+      grammar_associativity * precedence * string * constr_ast
+      * (string * precedence) list * scope_name option
 
   (* Gallina *)
   | VernacDefinition of definition_kind * identifier * definition_expr *