diff options
| author | ppedrot | 2013-07-05 01:49:27 +0000 |
|---|---|---|
| committer | ppedrot | 2013-07-05 01:49:27 +0000 |
| commit | a778b72e3ebfbe784fbe55ee5e124ba3f66cfb10 (patch) | |
| tree | 45ccc4afcf8edc5aed09d76b45c826a1e779af66 /grammar | |
| parent | 556c2ce6f1b09d09484cc83f6ada213496add45b (diff) | |
Expurgating the useless difference between List0 and List1 at the
level of generic arguments. This only matters at parsing time.
TODO: the current status is not satisfactory enough, as rule
emptyness is still decided w.r.t. generic arguments. This should be
done on a grammar entry basis instead.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 32 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 3 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 38 |
3 files changed, 43 insertions, 30 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index dfcaa4e84c..d8f615a98f 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -12,6 +12,7 @@ open Genarg open Q_util open Egramml open Compat +open Pcoq let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> @@ -42,8 +43,7 @@ let rec make_wit loc = function | OpenConstrArgType b -> <:expr< Constrarg.wit_open_constr_gen $mlexpr_of_bool b$ >> | ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >> | BindingsArgType -> <:expr< Constrarg.wit_bindings >> - | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> - | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >> + | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> @@ -56,16 +56,26 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> let has_extraarg = List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false) +let rec is_possibly_empty = function +| Aopt _ | Alist0 _ | Alist0sep _ | Amodifiers _ -> true +| Alist1 t | Alist1sep (t, _) -> is_possibly_empty t +| _ -> false + +let rec get_empty_entry = function +| Aopt _ -> <:expr< None >> +| Alist0 _ | Alist0sep _ | Amodifiers _ -> <:expr< [] >> +| Alist1 t | Alist1sep (t, _) -> <:expr< [$get_empty_entry t$] >> +| _ -> assert false + let statically_known_possibly_empty s (prods,_) = List.for_all (function | GramNonTerminal(_,ExtraArgType s',_,_) -> (* For ExtraArg we don't know (we'll have to test dynamically) *) (* unless it is a recursive call *) s <> s' - | GramNonTerminal(_,(OptArgType _|List0ArgType _),_,_) -> - (* Opt and List0 parses the empty string *) - true - | _ -> + | GramNonTerminal(_,_,e,_) -> + is_possibly_empty e + | GramTerminal _ -> (* This consumes a token for sure *) false) prods @@ -76,10 +86,8 @@ let possibly_empty_subentries loc (prods,act) = let s = Names.Id.to_string id in <:expr< let $lid:s$ = $v$ in $e$ >> in let rec aux = function | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >> - | GramNonTerminal(_,OptArgType _,_,p) :: tl -> - bind_name p <:expr< None >> (aux tl) - | GramNonTerminal(_,List0ArgType _,_,p) :: tl -> - bind_name p <:expr< [] >> (aux tl) + | GramNonTerminal(_,_,e,p) :: tl when is_possibly_empty e -> + bind_name p (get_empty_entry e) (aux tl) | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl -> (* We check at runtime if extraarg s parses "epsilon" *) let s = match p with None -> "_" | Some id -> Names.Id.to_string id in @@ -93,7 +101,7 @@ let possibly_empty_subentries loc (prods,act) = (* declares loc because some code can refer to it; *) (* ensures loc is used to avoid "unused variable" warning *) (true, <:expr< try Some $aux prods$ - with [ e when Errors.noncritical e -> None ] >>) + with [ Exit -> None ] >>) else (* Static optimisation *) (false, aux prods) @@ -262,7 +270,7 @@ EXTEND [ "2" [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ] | "1" - [ e = argtype; LIDENT "list" -> List0ArgType e + [ e = argtype; LIDENT "list" -> ListArgType e | e = argtype; LIDENT "option" -> OptArgType e ] | "0" [ e = LIDENT -> fst (interp_entry_name false None e "") diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index acb6c8347a..9e8ff8b645 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -214,8 +214,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.SortArgType -> <:expr< Genarg.SortArgType >> | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> - | Genarg.List0ArgType t -> <:expr< Genarg.List0ArgType $mlexpr_of_argtype loc t$ >> - | Genarg.List1ArgType t -> <:expr< Genarg.List1ArgType $mlexpr_of_argtype loc t$ >> + | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >> | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >> | Genarg.PairArgType (t1,t2) -> let t1 = mlexpr_of_argtype loc t1 in diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index d494a92d88..6e241cf879 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -111,6 +111,26 @@ let make_one_printing_rule se (pt,e) = let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) +let make_empty_check = function +| GramNonTerminal(_, t, e, _)-> + let is_extra = match t with ExtraArgType _ -> true | _ -> false in + if is_possibly_empty e || is_extra then + (* This possibly parses epsilon *) + let wit = make_wit loc t in + let rawwit = make_rawwit loc t in + <:expr< + match Genarg.default_empty_value $wit$ with + [ None -> raise Exit + | Some v -> + Tacintern.intern_genarg Tacintern.fully_empty_glob_sign + (Genarg.in_gen $rawwit$ v) ] >> + else + (* This does not parse epsilon (this Exit is static time) *) + raise Exit +| GramTerminal _ -> + (* Idem *) + raise Exit + let rec possibly_empty_subentries loc = function | [] -> [] | (s,prodsl) :: l -> @@ -118,24 +138,10 @@ let rec possibly_empty_subentries loc = function | [] -> (false,<:expr< None >>) | prods :: rest -> try - let l = List.map (function - | GramNonTerminal(_,(List0ArgType _| - OptArgType _| - ExtraArgType _ as t),_,_)-> - (* This possibly parses epsilon *) - let wit = make_wit loc t in - let rawwit = make_rawwit loc t in - <:expr< match Genarg.default_empty_value $wit$ with - [ None -> failwith "" - | Some v -> - Tacintern.intern_genarg Tacintern.fully_empty_glob_sign - (Genarg.in_gen $rawwit$ v) ] >> - | GramTerminal _ | GramNonTerminal(_,_,_,_) -> - (* This does not parse epsilon (this Exit is static time) *) - raise Exit) prods in + let l = List.map make_empty_check prods in if has_extraarg prods then (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ - with [ Failure "" -> $snd (aux rest)$ ] >>) + with [ Exit -> $snd (aux rest)$ ] >>) else (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>) with Exit -> aux rest in |
