Résolution bug #1850 sur notations avec niveaux inconnus de

camlp4. Petit nettoyage en passant.


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

5 files changed, 65 insertions, 17 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 1793be413..74b275fab 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -111,23 +111,28 @@ let make_constr_prod_item univ assoc from forpat = function
       let eobj = symbol_of_production assoc from forpat nt in
       (eobj, ovar)
 
+let prepare_empty_levels entry (pos,p4assoc,name,reinit) =
+  grammar_extend entry pos reinit [(name, p4assoc, [])]
+
 let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) =
   let univ = get_univ "constr" in
   let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in
   let (symbs,ntl) = List.split pil in
+  let needed_levels = register_empty_levels forpat symbs in
+  List.iter (prepare_empty_levels entry) needed_levels;
   grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])]
 
 let extend_constr_notation (n,assoc,ntn,rule) =
   (* Add the notation in constr *)
   let mkact loc env = CNotation (loc,ntn,List.map snd env) in
-  let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in
-  let pos,p4assoc,name,reinit = find_position false keepassoc assoc level in
+  let (e,level) = get_constr_entry false (ETConstr (n,())) in
+  let pos,p4assoc,name,reinit = find_position false assoc level in
   extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit)
     (make_constr_action mkact) (false,rule);
   (* Add the notation in cases_pattern *)
   let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
-  let (e,level,keepassoc) = get_constr_entry true (ETConstr (n,())) in
-  let pos,p4assoc,name,reinit = find_position true keepassoc assoc level in
+  let (e,level) = get_constr_entry true (ETConstr (n,())) in
+  let pos,p4assoc,name,reinit = find_position true assoc level in
   extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit)
     (make_cases_pattern_action mkact) (true,rule)
 
@@ -265,7 +270,7 @@ let add_tactic_entry (key,lev,prods,tac) =
       let mkact s tac loc l = 
 	(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
       make_rule univ (mkact key tac) mkprod prods in
-  let _ = find_position true true None None (* to synchronise with remove *) in
+  synchronize_level_positions ();
   grammar_extend entry pos None [(None, None, List.rev [rules])]
 
 (**********************************************************************)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index b4bac06e8..3b32cfd47 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -188,7 +188,7 @@ GEXTEND Gram
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
           CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ]
-    | "8" LEFTA [ ]
+    | "8" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
 	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 01b309f3c..73db83636 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -541,7 +541,7 @@ let default_levels =
    90,Gramext.RightA,false;
    10,Gramext.RightA,false;
    9,Gramext.RightA,false;
-   8,Gramext.LeftA,true;
+   8,Gramext.RightA,true;
    1,Gramext.LeftA,false;
    0,Gramext.RightA,false]
 
@@ -580,23 +580,25 @@ let error_level_assoc p current expected =
      pr_assoc current ++ str " associative while it is now expected to be " ++
      pr_assoc expected ++ str " associative")
 
-let find_position forpat other assoc lev =
+let find_position_gen forpat ensure assoc lev =
   let ccurrent,pcurrent as current = List.hd !level_stack in
   match lev with
   | None ->
       level_stack := current :: !level_stack;
-      None, (if other then assoc else None), None, None
+      None, None, None, None
   | Some n ->
       let after = ref None in
       let init = ref None in
       let rec add_level q = function
         | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
         | (p,a,reinit)::l when p = n ->
-	    if admissible_assoc (a,assoc) then
-              if reinit then (init := Some a; (p,a,false)::l) else raise Exit
+            if reinit then
+	      let a' = create_assoc assoc in (init := Some a'; (p,a',false)::l)
+	    else if admissible_assoc (a,assoc) then
+	      raise Exit
             else
 	      error_level_assoc p a (Option.get assoc)
-	| l -> after := q; (n,create_assoc assoc,false)::l
+	| l -> after := q; (n,create_assoc assoc,ensure)::l
       in
       try
 	let updated =
@@ -622,6 +624,25 @@ let find_position forpat other assoc lev =
 let remove_levels n =
   level_stack := list_skipn n !level_stack
 
+let rec list_mem_assoc_triple x = function
+  | [] -> false
+  | (a,b,c) :: l -> a = x or list_mem_assoc_triple x l
+
+let register_empty_levels forpat symbs =
+  map_succeed (function
+    | Gramext.Snterml (_,n) when
+	let levels = (if forpat then snd else fst) (List.hd !level_stack) in
+	not (list_mem_assoc_triple (int_of_string n) levels) ->
+	find_position_gen forpat true None (Some (int_of_string n))
+    | _ -> failwith "") symbs
+
+let find_position forpat assoc level =
+  find_position_gen forpat false assoc level
+
+(* Synchronise the stack of level updates *) 
+let synchronize_level_positions () =
+  let _ = find_position true None None in ()
+
 (* 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 
@@ -685,9 +706,10 @@ let compute_entry allow_create adjust forpat = function
 (* This computes the name of the level where to add a new rule *)
 let get_constr_entry forpat = function
   | ETConstr(200,()) when not forpat ->
-      weaken_entry Constr.binder_constr, None, false
+      weaken_entry Constr.binder_constr, None
   | e ->
-      compute_entry true (fun (n,()) -> Some n) forpat e
+      let (e,level,_) = compute_entry true (fun (n,()) -> Some n) forpat e in
+      (e, level)
 
 (* This computes the name to give to a production knowing the name and
    associativity of the level where it must be added *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 2525c430a..aaf4324e2 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -37,7 +37,7 @@ val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e
 val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
 
 val get_constr_entry :
-  bool -> constr_entry -> grammar_object Gram.Entry.e * int option * bool
+  bool -> constr_entry -> grammar_object Gram.Entry.e * int option
 
 val grammar_extend :
   grammar_object Gram.Entry.e -> Gramext.position option -> 
@@ -222,10 +222,17 @@ val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
 (* Registering/resetting the level of an entry *)
 
 val find_position : 
-  bool -> bool -> Gramext.g_assoc option -> int option ->
+  bool (* true if for creation in pattern entry; false if in constr entry *) ->
+  Gramext.g_assoc option -> int option ->
     Gramext.position option * Gramext.g_assoc option * string option * 
     (* for reinitialization: *) Gramext.g_assoc option
 
+val synchronize_level_positions : unit -> unit
+
+val register_empty_levels : bool -> Compat.token Gramext.g_symbol list ->
+    (Gramext.position option * Gramext.g_assoc option *
+     string option * Gramext.g_assoc option) list
+
 val remove_levels : int -> unit 
 
 val coerce_global_to_id : reference -> identifier
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index a9e2c59ab..facd55099 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -1,5 +1,5 @@
 (* Check that "where" clause behaves as if given independently of the  *)
-(* definition (variant of bug #113? submitted by Assia Mahboubi) *)
+(* definition (variant of bug #1132 submitted by Assia Mahboubi) *)
 
 Fixpoint plus1 (n m:nat) {struct n} : nat :=
    match n with
@@ -7,3 +7,17 @@ Fixpoint plus1 (n m:nat) {struct n} : nat :=
    | S p => S (p+m)
    end
  where "n + m" := (plus1 n m) : nat_scope.
+
+(* Check behaviour wrt yet empty levels (see Stephane's bug #1850) *)
+
+Parameter P : Type -> Type -> Type -> Type.
+Notation "e |= t --> v" := (P e t v)     (at level 100, t at level 54).
+Check (nat |= nat --> nat).
+
+(* Check that first non empty definition at an empty level can be of any 
+   associativity *)
+
+Definition marker := O.
+Notation "x +1" := (S x) (at level 8, left associativity).
+Reset marker.
+Notation "x +1" := (S x) (at level 8, right associativity).