Affinement encore

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

3 files changed, 55 insertions, 12 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 84b1aa0f0a..a7cfcc591e 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -50,6 +50,10 @@ let constr_level assoc = function
   | 8 -> assert (assoc <> Some Gramext.LeftA); "top"
   | n -> (string_of_int n)^(assoc_level (canonise_assoc assoc))
 
+let constr_prod_level = function
+  | 8 -> "top"
+  | n -> string_of_int n
+
 let numeric_levels =
   ref [8,Some Gramext.RightA; 1,Some Gramext.RightA; 0,Some Gramext.RightA]
 
@@ -67,7 +71,7 @@ let eq_assoc a b = match (canonise_assoc a, canonise_assoc b) with
 let find_position assoc = function
   | None -> None, Some (canonise_assoc assoc)
   | Some n ->
-      if n = 8 & assoc = Some Gramext.LeftA then 
+      if n = 8 & canonise_assoc assoc = Gramext.LeftA then 
 	error "Left associativity not allowed at level 8";
       let after = ref (8,Some Gramext.RightA) in
       let rec add_level q = function
@@ -176,7 +180,7 @@ let rec build_prod_item univ assoc = function
       match get_constr_production_entry assoc typ with
 	| (eobj,None) -> Gramext.Snterm (Gram.Entry.obj eobj)
 	| (eobj,Some lev) -> 
-	    Gramext.Snterml (Gram.Entry.obj eobj,constr_level assoc lev)
+	    Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev)
 
 let symbol_of_prod_item univ assoc = function
   | Term tok -> (Gramext.Stoken tok, None)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 04a31fa49d..ae3561c1f9 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -234,10 +234,25 @@ let gram_rule univ (name,pil,act) =
   let a = to_act_check_vars act_env act in
   { gr_name = name; gr_production = pilc; gr_action = a }
 
+let border = function
+  | NonTerm (ProdPrimitive (ETConstr(_,BorderProd (_,a))),_) :: _ -> a
+  | _ -> None
+
+let clever_assoc = function
+  | [g] when g.gr_production <> [] ->
+      (match border g.gr_production, border (List.rev g.gr_production) with
+	  Some RightA, Some LeftA -> Some NonA
+	| a, b when a=b -> a
+	| Some LeftA, Some RightA -> Some LeftA (* since LR *)
+	| _ -> None)
+  | _ -> None
+
 let gram_entry univ (nt, ass, rl) =
+  let l = List.map (gram_rule (univ,nt)) rl in
+  let ass = if ass = None then clever_assoc l else ass in
   { ge_name = nt;
     gl_assoc = ass;
-    gl_rules = List.map (gram_rule (univ,nt)) rl }
+    gl_rules = l }
 
 let interp_grammar_command univ ge entryl =
   { gc_univ = univ;
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a3f0dcc2a2..875c72b39a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -418,9 +418,11 @@ let make_pp_rule symbols typs =
 (* Syntax extenstion: common parsing/printing rules and no interpretation *)
 
 let cache_syntax_extension (_,(prec,ntn,gr,se)) =
-  Egrammar.extend_grammar (Egrammar.Notation gr);
-  if se<>None then
-    Symbols.declare_notation_printing_rule ntn (out_some se,fst prec)
+  if not (Symbols.exists_notation prec notation) then begin
+    Egrammar.extend_grammar (Egrammar.Notation gr);
+    if se<>None then
+      Symbols.declare_notation_printing_rule ntn (out_some se,fst prec)
+  end
 
 let subst_notation_grammar subst x = x
 
@@ -480,12 +482,30 @@ let set_entry_type etyps (x,typ) =
   let typ = try 
     match List.assoc x etyps, typ with
       | ETConstr (n,()), (_,BorderProd (left,_)) ->
-          ETConstr (n,BorderProd (left,None))
+	  (* We set an associativity telling not to change the level *)
+	  let assoc = if left then Gramext.LeftA else Gramext.RightA in
+          ETConstr (n,BorderProd (left,Some assoc))
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
       | (ETPattern | ETIdent | ETOther _ | ETReference as t), _ -> t
     with Not_found -> ETConstr typ
   in (x,typ)
 
+let collapse_assoc_left = function
+  | None | Some Gramext.LeftA -> Some Gramext.NonA
+  | a -> a
+
+let collapse_assoc_right = function
+  | Some Gramext.RightA -> Some Gramext.NonA
+  | a -> a
+
+let is_border = function
+  | (_,ETConstr(_,BorderProd _)) :: _ -> true
+  | _ -> false
+
+let adjust_associativity typs assoc =
+  let assoc = if is_border typs then assoc else collapse_assoc_left assoc in
+  if is_border (List.rev typs) then assoc else collapse_assoc_right assoc 
+
 let add_syntax_extension df modifiers =
   let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in
   let (typs,symbs) =
@@ -493,11 +513,11 @@ let add_syntax_extension df modifiers =
       (n,BorderProd(true,assoc)) (10,InternalProd) (n,BorderProd(false,assoc))
       [] (split df) in
   let typs = List.map (set_entry_type etyps) typs in
+  let assoc = adjust_associativity typs assoc in
   let (prec,notation) = make_symbolic assoc n symbs typs in
   let gram_rule = make_grammar_rule n assoc typs symbs notation in
   let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbs) in
-  if not (Symbols.exists_notation prec notation) then
-    Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule))
+  Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule))
 
 (**********************************************************************)
 (* Distfix, Infix, Notations *)
@@ -576,11 +596,11 @@ let add_notation_in_scope df a modifiers sc toks =
   let etyps = merge_entry_types etyps' etyps in
 *)
   let typs = List.map (set_entry_type etyps) typs in
+  let assoc = adjust_associativity typs assoc in
   (* Declare the parsing and printing rules if not already done *)
   let (prec,notation) = make_symbolic assoc n symbols typs in
   let gram_rule = make_grammar_rule n assoc typs symbols notation in
   let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbols) in
-  if not (Symbols.exists_notation prec notation) then
   Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule));
   let old_pp_rule =
     if onlyparse then None
@@ -620,7 +640,9 @@ let add_distfix assoc n df r sc =
   let (vars,l) = rename "x" [] 1 (split df) in
   let df = String.concat " " l in
   let a = mkAppC (mkRefC r, vars) in
-  let assoc = match assoc with None -> [] | Some a -> [SetAssoc a] in
+  let assoc = match assoc with
+    | None -> [SetAssoc Gramext.LeftA]
+    | Some a -> [SetAssoc a] in
   add_notation df a (SetLevel n :: assoc) sc
 
 let add_infix assoc n inf pr sc =
@@ -636,7 +658,9 @@ let add_infix assoc n inf pr sc =
   *)
   let metas = [inject_var "x"; inject_var "y"] in
   let a = mkAppC (mkRefC pr,metas) in
-  let assoc = match assoc with None -> [] | Some a -> [SetAssoc a] in
+  let assoc = match assoc with
+    | None -> [SetAssoc Gramext.LeftA]
+    | Some a -> [SetAssoc a] in
   add_notation ("x "^(quote inf)^" y") a (SetLevel n :: assoc) sc
 
 (* Delimiters *)