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

2 files changed, 78 insertions, 2 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;