On n'autorise plus les niveaux doubles L/R en v8

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

4 files changed, 119 insertions, 99 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 6d1d317e6..4f583424e 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -37,90 +37,6 @@ let (grammar_state : all_grammar_command list ref) = ref []
 
 
 (**************************************************************************)
-let assoc_level = function
-  | Gramext.LeftA -> "L"
-  | _ -> ""
-
-let constr_level = function
-  | n,assoc -> (string_of_int n)^(assoc_level assoc)
-
-let default_levels_v7 =
-  [10,Gramext.RightA;
-   9,Gramext.RightA;
-   8,Gramext.RightA;
-   1,Gramext.RightA;
-   0,Gramext.RightA]
-
-let default_levels_v8 =
-  [200,Gramext.RightA;
-   100,Gramext.RightA;
-   80,Gramext.RightA;
-   10,Gramext.LeftA;
-   9,Gramext.RightA;
-   1,Gramext.LeftA;
-   0,Gramext.RightA]
-
-let level_stack = ref [default_levels_v7]
-
-(* At a same level, LeftA takes precedence over RightA and NoneA *)
-(* In case, several associativity exists for a level, we make two levels, *)
-(* first LeftA, then RightA and NoneA together *)
-exception Found of Gramext.g_assoc
-
-open Ppextend
-
-let admissible_assoc = function
-  | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false
-  | Gramext.RightA, Some Gramext.LeftA -> false
-  | _ -> true
-
-let create_assoc = function
-  | None -> Gramext.RightA
-  | Some a -> a
-
-let find_position other assoc lev =
-  let default =
-    if !Options.v7 then (10,Gramext.RightA) else (200,Gramext.RightA) in
-  let current = List.hd !level_stack in 
-  match lev with
-  | None ->
-      level_stack := current :: !level_stack;
-      None, (if other then assoc else None), None
-  | Some n ->
-      if !Options.v7 & n = 8 & assoc = Some Gramext.LeftA then 
-	error "Left associativity not allowed at level 8";
-      let after = ref default in
-      let rec add_level q = function
-        | (p,_ as pa)::l when p > n -> pa :: add_level pa l
-        | (p,a as pa)::l as l' when p = n ->
-	    if admissible_assoc (a,assoc) then raise (Found a);
-	    (* Maybe this was (p,Right) and p occurs a second time *)
-	    if a = Gramext.LeftA then
-	      match l with
-		| (p,a)::_ as l' when p = n -> raise (Found a)
-		| _ -> after := pa; pa::(n,create_assoc assoc)::l
-	    else
-	      (* This was not (p,LeftA) hence assoc is RightA *)
-	      (after := q; (n,create_assoc assoc)::l')
-	| l ->
-	    after := q; (n,create_assoc assoc)::l
-      in
-      try
-	(* Create the entry *)
-        let current = List.hd !level_stack in
-        level_stack := add_level default current :: !level_stack;
-	let assoc = create_assoc assoc in
-        Some (Gramext.After (constr_level !after)),
-	Some assoc, Some (constr_level (n,assoc))
-      with
-          Found a ->
-            level_stack := current :: !level_stack;
-	    (* Just inherit the existing associativity and name (None) *)
-	    Some (Gramext.Level (constr_level (n,a))), None, None
-
-let remove_levels n =
-  level_stack := list_skipn n !level_stack
-
 (* Interpretation of the right hand side of grammar rules *)
 
 (* When reporting errors, we add the name of the grammar rule that failed *)
@@ -458,8 +374,7 @@ let reset_extend_grammars_v8 () =
   tac_exts := [];
   vernac_exts := [];
   List.iter (fun (s,gl) -> extend_tactic_grammar s gl) te;
-  List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv;
-  level_stack := [default_levels_v8]
+  List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv
 
 
 (* Summary functions: the state of the lexer is included in that of the parser.
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 6fa833275..d11d982ff 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -177,11 +177,11 @@ GEXTEND Gram
     | "80" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
       | c1 = operconstr; "->"; c2 = operconstr    -> CArrow(loc,c1,c2) ]
-    | "10L" LEFTA
+    | "10" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
       | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
     | "9" [ ]
-    | "1L" LEFTA
+    | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
 	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
       | c=operconstr; ".("; "@"; f=global;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 1f462b615..8d1d189ba 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -525,6 +525,106 @@ let default_action_parser =
    translated in camlp4 into "constr" without level) or to another level
    (to be translated into "constr LEVEL n") *)
 
+let assoc_level = function
+  | Some Gramext.LeftA when !Options.v7 -> "L"
+  | _ -> ""
+
+let constr_level = function
+  | n,assoc -> (string_of_int n)^(assoc_level assoc)
+
+let constr_level2 = function
+  | n,assoc -> (string_of_int n)^(assoc_level (Some assoc))
+
+let default_levels_v7 =
+  [10,Gramext.RightA;
+   9,Gramext.RightA;
+   8,Gramext.RightA;
+   1,Gramext.RightA;
+   0,Gramext.RightA]
+
+let default_levels_v8 =
+  [200,Gramext.RightA;
+   100,Gramext.RightA;
+   80,Gramext.RightA;
+   10,Gramext.LeftA;
+   9,Gramext.RightA;
+   1,Gramext.LeftA;
+   0,Gramext.RightA]
+
+let level_stack = 
+  ref [if !Options.v7 then default_levels_v7 else default_levels_v8]
+
+(* At a same level, LeftA takes precedence over RightA and NoneA *)
+(* In case, several associativity exists for a level, we make two levels, *)
+(* first LeftA, then RightA and NoneA together *)
+exception Found of Gramext.g_assoc
+
+open Ppextend
+
+let admissible_assoc = function
+  | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false
+  | Gramext.RightA, Some Gramext.LeftA -> false
+  | _ -> true
+
+let create_assoc = function
+  | None -> Gramext.RightA
+  | Some a -> a
+
+let error_level_assoc p current expected =
+  let pr_assoc = function
+    | Gramext.LeftA -> str "left"
+    | Gramext.RightA -> str "right" 
+    | Gramext.NonA -> str "non" in
+  errorlabstrm ""
+    (str "Level " ++ int p ++ str " is already declared " ++
+     pr_assoc current ++ str " associative while it is now expected to be " ++
+     pr_assoc expected ++ str " associative")
+
+let find_position other assoc lev =
+  let default =
+    if !Options.v7 then (10,Gramext.RightA) else (200,Gramext.RightA) in
+  let current = List.hd !level_stack in 
+  match lev with
+  | None ->
+      level_stack := current :: !level_stack;
+      None, (if other then assoc else None), None
+  | Some n ->
+      if !Options.v7 & n = 8 & assoc = Some Gramext.LeftA then 
+	error "Left associativity not allowed at level 8";
+      let after = ref default in
+      let rec add_level q = function
+        | (p,_ as pa)::l when p > n -> pa :: add_level pa l
+        | (p,a as pa)::l as l' when p = n ->
+	    if admissible_assoc (a,assoc) then raise (Found a);
+	    (* No duplication of levels in v8 *)
+	    if not !Options.v7 then error_level_assoc p a (out_some assoc);
+	    (* Maybe this was (p,Left) and p occurs a second time *)
+	    if a = Gramext.LeftA then
+	      match l with
+		| (p,a)::_ as l' when p = n -> raise (Found a)
+		| _ -> after := pa; pa::(n,create_assoc assoc)::l
+	    else
+	      (* This was not (p,LeftA) hence assoc is RightA *)
+	      (after := q; (n,create_assoc assoc)::l')
+	| l ->
+	    after := q; (n,create_assoc assoc)::l
+      in
+      try
+	(* Create the entry *)
+        let current = List.hd !level_stack in
+        level_stack := add_level default current :: !level_stack;
+	let assoc = create_assoc assoc in
+        Some (Gramext.After (constr_level2 !after)),
+	Some assoc, Some (constr_level2 (n,assoc))
+      with
+          Found a ->
+            level_stack := current :: !level_stack;
+	    (* Just inherit the existing associativity and name (None) *)
+	    Some (Gramext.Level (constr_level2 (n,a))), None, None
+
+let remove_levels n =
+  level_stack := list_skipn n !level_stack
+
 (* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
 let camlp4_assoc = function
   | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA 
@@ -636,18 +736,15 @@ let get_constr_production_entry ass from en =
 *)
     | _ -> compute_entry false (adjust_level ass from) en
 
-let assoc_level = function
-  | Some Gramext.LeftA -> "L"
-  | _ -> ""
-
-let constr_level = function
-  | n,assoc -> (string_of_int n)^(assoc_level assoc)
-
 let constr_prod_level assoc cur lev =
-  if cur then constr_level (lev,assoc) else
-  match lev with
-  | 4 when !Options.v7 -> "4L"
-  | n -> string_of_int n
+  if !Options.v7 then
+    if cur then constr_level (lev,assoc) else
+      match lev with
+	| 4 when !Options.v7 -> "4L"
+	| n -> string_of_int n
+  else
+    (* No duplication L/R of levels in v8 *)
+    constr_level (lev,assoc)
 
 let is_self from e =
   match from, e with
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1c7a1932f..33fe8f1d1 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -177,3 +177,11 @@ module Vernac_ :
   end
 
 val reset_all_grammars : unit -> unit
+
+(* Registering/resetting the level of an entry *)
+
+val find_position : 
+  bool -> Gramext.g_assoc option -> int option ->
+    Gramext.position option * Gramext.g_assoc option * string option
+
+val remove_levels : int -> unit