aboutsummaryrefslogtreecommitdiff
path: root/grammar
diff options
context:
space:
mode:
authorppedrot2013-07-05 01:49:27 +0000
committerppedrot2013-07-05 01:49:27 +0000
commita778b72e3ebfbe784fbe55ee5e124ba3f66cfb10 (patch)
tree45ccc4afcf8edc5aed09d76b45c826a1e779af66 /grammar
parent556c2ce6f1b09d09484cc83f6ada213496add45b (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.ml432
-rw-r--r--grammar/q_coqast.ml43
-rw-r--r--grammar/tacextend.ml438
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