diff options
| author | Pierre-Marie Pédrot | 2016-03-17 15:10:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-17 15:10:57 +0100 |
| commit | e3e8a4065047e254f5f5c2747227db75f01b7bed (patch) | |
| tree | c7505db28eee92bc1855b6ee0cf275381b4aa106 /parsing | |
| parent | 22c1e7c3f1d86902b1abf2d887e0e9bf93ddb60d (diff) | |
| parent | 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 (diff) | |
Removing the default value mechanism for generic arguments.
There was a complicated dedicated code in grammar/ to decide whether a generic argument
parsed the empty string. We now only rely on a dynamic decision. This should not affect
efficiency, as it is only made once by declaration of ML tactics.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 7 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
2 files changed, 9 insertions, 0 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index cf65262c4a..52437e3867 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -853,3 +853,10 @@ let list_entry_names () = let ans = Hashtbl.fold add_entry (get_utable uprim) [] in let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in Hashtbl.fold add_entry (get_utable utactic) ans + +let epsilon_value f e = + let r = Rule (Next (Stop, e), fun x _ -> f x) in + let ext = of_coq_extend_statement (None, [None, None, [r]]) in + let entry = G.entry_create "epsilon" in + let () = maybe_uncurry (Gram.extend entry) ext in + try Some (parse_string entry "") with _ -> None diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index b26c3044bd..7e0c89fd12 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -272,6 +272,8 @@ val symbol_of_constr_prod_entry_key : gram_assoc option -> val name_of_entry : 'a Gram.entry -> 'a Entry.t +val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option + (** Binding general entry keys to symbols *) type 's entry_name = EntryName : |