Décomposition automatique des règles d'analyse syntaxique pour les

notations contenant le motif "{ _ }": permet de réperer des
incohérences de précédence comme dans "A*{B}+{C}" en présence d'une
notation "_ * { _ }" (il était parsé associant à droite au lieu de à
gauche) et de supprimer les règles spécifiques de Notations pour
parser "B+{x:A|P}" etc.


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

7 files changed, 161 insertions, 84 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 28ab30c057..455b91e4da 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1074,15 +1074,43 @@ let same c d = try check_same_type c d; true with _ -> false
 let make_current_scopes (scopt,scopes) = 
   option_fold_right push_scope scopt scopes
 
+let has_curly_brackets ntn =
+  String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
+    String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
+    string_string_contains ntn " { _ } ")
+
+let expand_curly_brackets make_ntn ntn l =
+  let ntn' = ref ntn in
+  let rec expand_ntn =
+    function
+    | [] -> []
+    | a::l as l' ->
+        let a' = 
+          try
+            let i = string_index_from !ntn' 0 "{ _ }" in
+            ntn' := 
+              String.sub !ntn' 0 i ^ "_" ^ 
+              String.sub !ntn' (i+5) (String.length !ntn' -i-5);
+            make_ntn "{ _ }" [a]
+          with Not_found -> a in
+        a' :: expand_ntn l in
+  let l = expand_ntn l in
+  (* side effect *)
+  make_ntn !ntn' l
+
 let make_notation loc ntn l =
-  match ntn,l with
+  if has_curly_brackets ntn
+  then expand_curly_brackets (fun n l -> CNotation (loc,n,l)) ntn l
+  else match ntn,l with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
     | "- _", [CNumeral(_,Bignat.POS p)] ->
         CNotation (loc,ntn,[CNotation(loc,"( _ )",l)])
     | _ -> CNotation (loc,ntn,l)
 
 let make_pat_notation loc ntn l =
-  match ntn,l with
+  if has_curly_brackets ntn
+  then expand_curly_brackets (fun n l -> CPatNotation (loc,n,l)) ntn l
+  else match ntn,l with
     (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
     | "- _", [CPatNumeral(_,Bignat.POS p)] ->
         CPatNotation (loc,ntn,[CPatNotation(loc,"( _ )",l)])
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index de5659c38f..821e9a26a3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -160,6 +160,52 @@ let dump_notation_location =
     dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst loc) path df sc)
 
 (**********************************************************************)
+(* Contracting "{ _ }" in notations *)
+
+let rec wildcards ntn n =
+  if n = String.length ntn then []
+  else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l
+and spaces ntn n =
+  if n = String.length ntn then []
+  else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
+
+let expand_notation_string ntn n =
+  let pos = List.nth (wildcards ntn 0) n in
+  let hd = if pos = 0 then "" else String.sub ntn 0 pos in
+  let tl = 
+    if pos = String.length ntn then "" 
+    else String.sub ntn (pos+1) (String.length ntn - pos -1) in
+  hd ^ "{ _ }" ^ tl
+
+(* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
+(* Remark: expansion of squash at definition is done in metasyntax.ml *)
+let contract_notation ntn l =
+  let ntn' = ref ntn in
+  let rec contract_squash n = function
+    | [] -> []
+    | CNotation (_,"{ _ }",[a]) :: l -> 
+        ntn' := expand_notation_string !ntn' n;
+        contract_squash n (a::l)
+    | a :: l ->
+        a::contract_squash (n+1) l in
+  let l = contract_squash 0 l in
+  (* side effect; don't inline *)
+  !ntn',l
+
+let contract_pat_notation ntn l =
+  let ntn' = ref ntn in
+  let rec contract_squash n = function
+    | [] -> []
+    | CPatNotation (_,"{ _ }",[a]) :: l -> 
+        ntn' := expand_notation_string !ntn' n;
+        contract_squash n (a::l)
+    | a :: l ->
+        a::contract_squash (n+1) l in
+  let l = contract_squash 0 l in
+  (* side effect; don't inline *)
+  !ntn',l
+
+(**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
 let make_current_scope (scopt,scopes) = option_cons scopt scopes
@@ -454,6 +500,7 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function
   | CPatNotation (_,"( _ )",[a]) ->
       intern_cases_pattern scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
+      let ntn,args = contract_pat_notation ntn args in
       let scopes = option_cons tmp_scope scopes in
       let ((ids,c),df) = Symbols.interp_notation ntn scopes in
       if !dump then dump_notation_location (patntn_loc loc args ntn) ntn df;
@@ -677,6 +724,7 @@ let internalise sigma env allow_soapp lvar c =
         Symbols.interp_numeral loc (Bignat.NEG p) scopes
     | CNotation (_,"( _ )",[a]) -> intern env a
     | CNotation (loc,ntn,args) ->
+        let ntn,args = contract_notation ntn args in
 	let scopes = option_cons tmp_scope scopes in
 	let ((ids,c),df) = Symbols.interp_notation ntn scopes in
         if !dump then dump_notation_location (ntn_loc loc args ntn) ntn df;
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 3568991918..92e1a818b5 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -61,28 +61,15 @@ Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 )" (at level 0).
 Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 )" (at level 0).
 Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 )" (at level 0).
 
-(** Notations for sum-types *)
-
-(* Home-made factorization at level 4 to parse B+{x:A|P} without parentheses *)
-
-Reserved Notation "B + { x : A | P }"
-(at level 50, x at level 99, left associativity, only parsing).
-
-Reserved Notation "B + { x : A | P & Q }"
-(at level 50, x at level 99, left associativity, only parsing).
+(** Notation "{ x }" is reserved and has a special status as component
+    of other notations; it is at level 0 to factor with {x:A|P} etc *)
 
-Reserved Notation "B + { x : A & P }"
-(at level 50, x at level 99, left associativity, only parsing).
+Reserved Notation "{ x }" (at level 0, x at level 99).
 
-Reserved Notation "B + { x : A & P & Q }"
-(at level 50, x at level 99, left associativity, only parsing).
-
-(* At level 1 to factor with {x:A|P} etc *)
-
-Reserved Notation "{ A }  + { B }" (at level 0, A at level 99).
+(** Notations for sum-types *)
 
-Reserved Notation "A + { B }"
-(at level 50, B at level 99, left associativity).
+Reserved Notation "{ A } + { B }" (at level 50, left associativity).
+Reserved Notation "A + { B }" (at level 50, left associativity).
 
 (** Notations for sigma-types or subsets *)
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index eb775505f6..4d145fbdda 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -111,17 +111,6 @@ Inductive sumor (A:Set) (B:Prop) : Set :=
   | inright : B -> A + {B} 
  where "A + { B }" := (sumor A B) : type_scope.
 
-(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
-
-Notation "B + { x : A | P }" := (B + sig (fun x:A => P)) 
-  (only parsing) : type_scope.
-Notation "B + { x : A | P & Q }" := (B + sig2 (fun x:A => P) (fun x:A => Q))
-  (only parsing) : type_scope.
-Notation "B + { x : A & P }" := (B + sigS (fun x:A => P)) 
-  (only parsing) : type_scope.
-Notation "B + { x : A & P & Q }" := (B + sigS2 (fun x:A => P) (fun x:A => Q))
-  (only parsing) : type_scope.
-
 (** Choice *)
 
 Section Choice_lemmas.
diff --git a/theories7/Init/Notations.v b/theories7/Init/Notations.v
index 3cdb8e6ce4..2e9e1692d3 100644
--- a/theories7/Init/Notations.v
+++ b/theories7/Init/Notations.v
@@ -69,33 +69,19 @@ Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 )" (at level 0).
 Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 )" (at level 0).
 Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 )" (at level 0).
 
-(** Notations for sum-types *)
-
-(* Home-made factorization at level 4 to parse B+{x:A|P} without parentheses *)
-
-Uninterpreted Notation "B + { x : A | P }"
-  (at level 4, left associativity, only parsing)
-  V8only (at level 50, x at level 99, left associativity, only parsing).
-
-Uninterpreted Notation "B + { x : A | P & Q }"
-  (at level 4, left associativity, only parsing)
-  V8only (at level 50, x at level 99, left associativity, only parsing).
+(** Notation "{ x }" is reserved and has a special status as component
+    of other notations; it is at level 1 to factor with {x:A|P} etc *)
 
-Uninterpreted Notation "B + { x : A & P }"
-  (at level 4, left associativity, only parsing)
-  V8only (at level 50, x at level 99, left associativity, only parsing).
-
-Uninterpreted Notation "B + { x : A & P & Q }"
-  (at level 4, left associativity, only parsing)
-  V8only (at level 50, x at level 99, left associativity, only parsing).
+Uninterpreted Notation "{ x }" (at level 1)
+  V8only (at level 0, x at level 99).
 
-(* At level 1 to factor with {x:A|P} etc *)
+(** Notations for sum-types *)
 
-Uninterpreted Notation "{ A }  + { B }" (at level 1)
-  V8only (at level 0, A at level 99).
+Uninterpreted Notation "{ A }  + { B }" (at level 4, left associativity)
+  V8only (at level 50, left associativity).
 
 Uninterpreted Notation "A + { B }" (at level 4, left associativity)
-  V8only (at level 50, B at level 99, left associativity).
+  V8only (at level 50, left associativity).
 
 (** Notations for sigma-types or subsets *)
 
diff --git a/theories7/Init/Specif.v b/theories7/Init/Specif.v
index 2e49fab040..1255a5a284 100755
--- a/theories7/Init/Specif.v
+++ b/theories7/Init/Specif.v
@@ -108,17 +108,6 @@ Inductive sumor [A:Set;B:Prop] : Set
 
 where "A + { B }" := (sumor A B) : type_scope.
 
-(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
-
-Notation "B + { x : A | P }"     := B + (sig A [x:A]P)
-  (only parsing) : type_scope.
-Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q)
-  (only parsing) : type_scope.
-Notation "B + { x : A & P }"     := B + (sigS A [x:A]P)
-  (only parsing) : type_scope.
-Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q)
-  (only parsing) : type_scope.
-
 (** Choice *)
 
 Section Choice_lemmas.
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a50339c6e9..3d773a7da0 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -576,9 +576,6 @@ let string_of_assoc = function
   | Some(Gramext.LeftA) | None -> "LEFTA"
   | Some(Gramext.NonA) -> "NONA"
 
-let make_symbolic n symbols etyps =
-  ((n,List.map (assoc_of_type n) etyps), make_notation_key symbols)
-
 let is_not_small_constr = function
     ETConstr _ -> true
   | ETOther("constr","binder_constr") -> true
@@ -633,6 +630,14 @@ let recompute_assoc typs =
     | _, Some Gramext.RightA -> Some Gramext.RightA
     | _ -> None
 
+let rec expand_squash = function
+  | Term ("","{") :: NonTerm (ProdPrimitive (ETConstr _), n) :: Term ("","}")
+    :: l ->
+      NonTerm (ProdPrimitive (ETConstr (NextLevel,InternalProd)),n)
+      :: expand_squash l
+  | a :: l -> a :: expand_squash l
+  | [] -> []
+
 let make_grammar_rule n typs symbols ntn perm =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
@@ -858,6 +863,35 @@ let find_precedence lev etyps symbols =
       if lev = None then error "Cannot determine the level";
       out_some lev
 
+let check_curly_brackets_notation_exists () =
+  try let _ = Symbols.level_of_notation "{ _ }" in ()
+  with Not_found -> 
+    error "Notations involving patterns of the form \"{ _ }\" are treated \n\
+specially and require that the notation \"{ _ }\" is already reserved"
+
+(* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
+let remove_curly_brackets l = 
+  let rec next = function
+    | Break _ :: l -> next l
+    | l -> l in
+  let rec aux deb = function
+  | [] -> []
+  | Terminal "{" as t1 :: l -> 
+      (match next l with
+        | NonTerminal _ as x :: l' as l0 ->
+            (match next l' with
+              | Terminal "}" as t2 :: l'' as l1 ->
+                  if l <> l0 or l' <> l1 then
+                    warning "Skipping spaces inside curly brackets";
+                  if deb & l'' = [] then [t1;x;t2] else begin
+                    check_curly_brackets_notation_exists ();
+                    x :: aux false l''
+                  end
+              | l1 -> t1 :: x :: aux false l1)
+        | l0 -> t1 :: aux false l0)
+  | x :: l -> x :: aux false l
+  in aux true l
+
 let compute_syntax_data forv7 (df,modifiers) =
   let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
   (* Notation defaults to NONA *)
@@ -865,6 +899,8 @@ let compute_syntax_data forv7 (df,modifiers) =
   let toks = split_notation_string df in
   let innerlevel = NumLevel (if forv7 then 10 else 200) in
   let (vars,symbols) = analyse_notation_tokens toks in
+  let symbols = remove_curly_brackets symbols in
+  let notation = make_notation_key symbols in
   check_rule_reversibility symbols;
   let n =
     if !Options.v7 then find_precedence_v7 n etyps symbols
@@ -877,24 +913,25 @@ let compute_syntax_data forv7 (df,modifiers) =
       symbols in
   (* To globalize... *)
   let typs = List.map (set_entry_type etyps) typs in
-  let (prec,notation) = make_symbolic n symbols typs in
-  ((onlyparse,vars,notation),prec,(n,typs,symbols,fmt),(Lib.library_dp(),df))
+  let ppdata = (n,typs,symbols,fmt) in
+  let prec = (n,List.map (assoc_of_type n) typs) in
+  ((onlyparse,vars,notation),prec,ppdata,(Lib.library_dp(),df))
 
 let add_syntax_extension local mv mv8 =
   let data8 = option_app (compute_syntax_data false) mv8 in
   let data = option_app (compute_syntax_data !Options.v7) mv in
   let prec,gram_rule = match data with
-    | None -> None, None
-    | Some ((_,_,notation),prec,(n,typs,symbols,_),_) -> 
-	Some prec, Some (make_grammar_rule n typs symbols notation None) in
+  | None -> None, None
+  | Some ((_,_,notation),prec,(n,typs,symbols,_),_) -> 
+      Some prec, Some (make_grammar_rule n typs symbols notation None) in
   match data, data8 with
-    | None, None -> (* Nothing to do: V8Notation while not translating *) () 
-    | _, Some d | Some d, None ->
-  let ((_,_,notation),ppprec,ppdata,_) = d in
-  let notation = match data with Some ((_,_,ntn),_,_,_) -> ntn | _ -> notation in
-  let pp_rule = make_pp_rule ppdata in
-  Lib.add_anonymous_leaf
-    (inSyntaxExtension (local,(prec,ppprec),notation,gram_rule,pp_rule))
+  | None, None -> (* Nothing to do: V8Notation while not translating *) () 
+  | _, Some d | Some d, None ->
+    let ((_,_,ntn),ppprec,ppdata,_) = d in
+    let ntn' = match data with Some ((_,_,ntn),_,_,_) -> ntn | _ -> ntn in
+    let pp_rule = make_pp_rule ppdata in
+    Lib.add_anonymous_leaf
+      (inSyntaxExtension (local,(prec,ppprec),ntn',gram_rule,pp_rule))
 	
 (**********************************************************************)
 (* Distfix, Infix, Symbols *)
@@ -977,6 +1014,18 @@ let mk_permut vars7 vars8 =
         (fun v8 subs -> list_index v8 vars7 - 1 :: subs)
         vars8 [])
 
+let contract_notation ntn =
+  let rec aux ntn i =
+    if i <= String.length ntn - 5 then
+      let ntn' =
+        if String.sub ntn i 5 = "{ _ }" then
+          String.sub ntn 0 i ^ "_" ^ 
+          String.sub ntn (i+5) (String.length ntn -i-5)
+        else ntn in
+      aux ntn' (i+1) 
+    else ntn in
+  aux ntn 0
+
 let add_notation_in_scope local df c mods omodv8 scope toks =
   let ((onlyparse,vars,notation),prec,(n,typs,symbols,_ as ppdata),df') =
     compute_syntax_data !Options.v7 (df,mods) in
@@ -997,8 +1046,9 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
     | _ -> 
 	(* means the rule already exists: recover it *)
 	try 
-	  let _, oldprec8 = Symbols.level_of_notation notation in
-	  let rule,_ = Symbols.find_notation_printing_rule notation in
+          let ntn = contract_notation notation in
+	  let _, oldprec8 = Symbols.level_of_notation ntn in
+	  let rule,_ = Symbols.find_notation_printing_rule ntn in
 	  notation,vars,oldprec8,rule
 	with Not_found -> error "No known parsing rule for this notation in V8"
   in
@@ -1025,7 +1075,7 @@ 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
+    let a,_ = Symbols.level_of_notation (contract_notation notation) in
     if a = None then raise Not_found
   with Not_found ->
     error "Parsing rule for this notation has to be previously declared"
@@ -1033,7 +1083,7 @@ let check_notation_existence notation =
 let build_old_pp_rule notation scope symbs (r,vars) =
   let prec = 
     try
-      let a,_ = Symbols.level_of_notation notation in
+      let a,_ = Symbols.level_of_notation (contract_notation notation) in
       if a = None then raise Not_found else out_some a
     with Not_found ->
       error "Parsing rule for this notation has to be previously declared" in