diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egrammar.ml | 38 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 4 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 44 |
3 files changed, 53 insertions, 33 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 -> diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 44ac445d..3ed4d8a7 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 14657 2011-11-16 08:46:33Z herbelin $ *) +(* $Id: ppvernac.ml 15025 2012-03-09 14:27:07Z glondu $ *) open Pp open Names @@ -781,7 +781,7 @@ let rec pr_vernac = function (if i = 1 then mt() else int i ++ str ": ") ++ pr_raw_tactic tac ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt () - with UserError _|Stdpp.Exc_located _ -> mt()) + with UserError _|Compat.Exc_located _ -> mt()) | VernacSolveExistential (i,c) -> str"Existential " ++ int i ++ pr_lconstrarg c diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 0d7a9cfe..2fbe3f44 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: tacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: tacextend.ml4 15043 2012-03-18 13:57:01Z herbelin $ *) open Util open Genarg @@ -131,19 +131,27 @@ let make_one_printing_rule se (pt,e) = let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) -let rec contains_epsilon = function - | List0ArgType _ -> true - | List1ArgType t -> contains_epsilon t - | OptArgType _ -> true - | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2 - | ExtraArgType("hintbases") -> true - | _ -> false -let is_atomic = function - | GramTerminal s :: l when - List.for_all (function - GramTerminal _ -> false - | GramNonTerminal(_,t,_,_) -> contains_epsilon t) l - -> [s] +let rec contains_epsilon loc = function + | List0ArgType _ as t -> + <:expr< Genarg.in_gen $make_globwit loc t$ [] >> + | List1ArgType t' as t -> + <:expr< Genarg.in_gen $make_globwit loc t$ + [out_gen $make_globwit loc t'$ $contains_epsilon loc t'$] >> + | OptArgType _ as t -> + <:expr< Genarg.in_gen $make_globwit loc t$ None >> +(* | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2*) + | ExtraArgType("hintbases") as t -> + <:expr< Genarg.in_gen $make_globwit loc t$ (Some []) >> (* fragile *) + | _ -> raise Exit + +let is_atomic loc = function + | GramTerminal s :: l -> + (try + let l = List.map (function + GramTerminal _ -> raise Exit + | GramNonTerminal(_,t,_,_) -> contains_epsilon loc t) l + in [<:expr< ($str:s$, $mlexpr_of_list (fun x -> x) l$) >>] + with Exit -> []) | _ -> [] let declare_tactic loc s cl = @@ -163,8 +171,8 @@ let declare_tactic loc s cl = in let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in let atomic_tactics = - mlexpr_of_list mlexpr_of_string - (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in + mlexpr_of_list (fun x -> x) + (List.flatten (List.map (fun (al,_) -> is_atomic loc al) cl)) in <:str_item< declare open Pcoq; @@ -173,9 +181,9 @@ let declare_tactic loc s cl = try let _=Tacinterp.add_tactic $se$ (fun [ $list:make_clauses s cl$ ]) in List.iter - (fun s -> Tacinterp.add_primitive_tactic s + (fun (s,l) -> Tacinterp.add_primitive_tactic s (Tacexpr.TacAtom($default_loc$, - Tacexpr.TacExtend($default_loc$,s,[])))) + Tacexpr.TacExtend($default_loc$,$se$,l)))) $atomic_tactics$ with e -> Pp.pp (Cerrors.explain_exn e); Egrammar.extend_tactic_grammar $se$ $gl$; |