diff options
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 38 |
1 files changed, 25 insertions, 13 deletions
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 -> |