From 2bdcd093b357adb2185518dabbafd1a0b9279044 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 27 Mar 2012 07:41:19 +0200
Subject: Imported Upstream version 8.3.pl4

---
 parsing/egrammar.ml | 38 +++++++++++++++++++++++++-------------
 1 file changed, 25 insertions(+), 13 deletions(-)

(limited to 'parsing/egrammar.ml')

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index ba965a54..072b09fa 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: egrammar.ml 14779 2011-12-07 21:54:18Z herbelin $ *)
+(* $Id: egrammar.ml 15072 2012-03-20 17:36:33Z herbelin $ *)
 
 open Pp
 open Util
@@ -109,11 +109,14 @@ let make_constr_action
   in
   make ([],[],[]) (List.rev pil)
 
+let check_cases_pattern_env loc (env,envlist,hasbinders) =
+  if hasbinders then error_invalid_pattern_notation loc else (env,envlist)
+
 let make_cases_pattern_action
   (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
-  let rec make (env,envlist as fullenv) = function
+  let rec make (env,envlist,hasbinders as fullenv) = function
   | [] ->
-      Gramext.action (fun loc -> f loc fullenv)
+      Gramext.action (fun loc -> f loc (check_cases_pattern_env loc fullenv))
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
       (* parse a non-binding item *)
       Gramext.action (fun _ -> make fullenv tl)
@@ -121,28 +124,37 @@ let make_cases_pattern_action
       (* parse a binding non-terminal *)
     (match typ with
     | ETConstr _ -> (* pattern non-terminal *)
-        Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
+        Gramext.action (fun (v:cases_pattern_expr) ->
+          make (v::env, envlist, hasbinders) tl)
     | ETReference ->
         Gramext.action (fun (v:reference) ->
-	  make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
+	  make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl)
     | ETName ->
         Gramext.action (fun (na:name located) ->
-	  make (cases_pattern_expr_of_name na :: env, envlist) tl)
+	  make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
     | ETBigint ->
         Gramext.action (fun (v:Bigint.bigint) ->
-	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
+	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl)
     | ETConstrList (_,_) ->
         Gramext.action  (fun (vl:cases_pattern_expr list) ->
-	  make (env, vl :: envlist) tl)
-    | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
-	failwith "Unexpected entry of type cases pattern or other")
+	  make (env, vl :: envlist, hasbinders) tl)
+    | ETBinder _ | ETBinderList (true,_) ->
+	Gramext.action (fun (v:local_binder list) ->
+	  make (env, envlist, hasbinders) tl)
+    | ETBinderList (false,_) ->
+	Gramext.action (fun (v:local_binder list list) ->
+	  make (env, envlist, true) tl)
+    | (ETPattern | ETOther _) ->
+        anomaly "Unexpected entry of type cases pattern or other")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
       let heads,env = list_chop n env in
-      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
-      else make (env,heads::envlist) tl
+      if b then
+        make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl
+      else
+        make (env,heads::envlist,hasbinders) tl
   in
-  make ([],[]) (List.rev pil)
+  make ([],[],false) (List.rev pil)
 
 let rec make_constr_prod_item assoc from forpat = function
   | GramConstrTerminal tok :: l ->
-- 
cgit v1.2.3