diff options
| -rw-r--r-- | lib/util.ml | 10 | ||||
| -rw-r--r-- | lib/util.mli | 1 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 58 |
3 files changed, 45 insertions, 24 deletions
diff --git a/lib/util.ml b/lib/util.ml index c4229fd32..e6c76f7f3 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -699,7 +699,7 @@ let list_split_when p = split_when_loop [] (* [list_split_by p l] splits [l] into two lists [(l1,l2)] such that elements of - [l1] satisfy [p] and elements of [l2] do not *) + [l1] satisfy [p] and elements of [l2] do not; order is preserved *) let list_split_by p = let rec split_by_loop = function | [] -> ([],[]) @@ -858,6 +858,14 @@ let rec list_cartesians_filter op init ll = let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl +(* Factorize lists of pairs according to the left argument *) +let rec list_factorize_left = function + | (a,b)::l -> + let al,l' = list_split_by (fun (a',b) -> a=a') l in + (a,(b::List.map snd al)) :: list_factorize_left l' + | [] -> + [] + (* Arrays *) let array_compare item_cmp v1 v2 = diff --git a/lib/util.mli b/lib/util.mli index 868a76711..37d15792f 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -191,6 +191,7 @@ val list_cartesians_filter : ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b +val list_factorize_left : ('a * 'b) list -> ('a * 'b list) list (** {6 Arrays. } *) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index b7364efc1..73ef0d701 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -120,28 +120,40 @@ let make_one_printing_rule se (pt,e) = let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) -let possibly_empty_subentries loc s prods = - try - let l = List.map (function - | GramNonTerminal(_,(List0ArgType _|OptArgType _|ExtraArgType _ as t),_,_)-> - (* This possibly parses epsilon *) - let globwit = make_globwit loc t in - <:expr< match Genarg.default_empty_value $globwit$ with - [ None -> failwith "" - | Some v -> Genarg.in_gen $globwit$ v ] >> - | GramTerminal _ | GramNonTerminal(_,_,_,_) -> - (* This does not parse epsilon (this Exit is static time) *) - raise Exit) prods in - if has_extraarg prods then - [s, <:expr< try Some $mlexpr_of_list (fun x -> x) l$ - with Failure "" -> None >>] - else - [s, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>] - with Exit -> [] - -let possibly_atomic loc = function - | GramTerminal s :: l -> possibly_empty_subentries loc s l - | _ -> [] +let rec possibly_empty_subentries loc = function + | [] -> [] + | (s,prodsl) :: l -> + let rec aux = function + | [] -> (false,<:expr< None >>) + | prods :: rest -> + try + let l = List.map (function + | GramNonTerminal(_,(List0ArgType _| + OptArgType _| + ExtraArgType _ as t),_,_)-> + (* This possibly parses epsilon *) + let globwit = make_globwit loc t in + <:expr< match Genarg.default_empty_value $globwit$ with + [ None -> failwith "" + | Some v -> Genarg.in_gen $globwit$ v ] >> + | GramTerminal _ | GramNonTerminal(_,_,_,_) -> + (* This does not parse epsilon (this Exit is static time) *) + raise Exit) prods in + if has_extraarg prods then + (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ + with Failure "" -> $snd (aux rest)$ >>) + else + (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>) + with Exit -> aux rest in + let (nonempty,v) = aux prodsl in + if nonempty then (s,v) :: possibly_empty_subentries loc l + else possibly_empty_subentries loc l + +let possibly_atomic loc prods = + let l = list_map_filter (function + | GramTerminal s :: l, _ -> Some (s,l) + | _ -> None) prods in + possibly_empty_subentries loc (list_factorize_left l) let declare_tactic loc s cl = let se = mlexpr_of_string s in @@ -161,7 +173,7 @@ let declare_tactic loc s cl = let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in let atomic_tactics = mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x)) - (List.flatten (List.map (fun (al,_) -> possibly_atomic loc al) cl)) in + (possibly_atomic loc cl) in declare_str_items loc (hidden @ [ <:str_item< do { |