diff options
-rw-r--r-- | grammar/q_util.ml4 | 4 | ||||
-rw-r--r-- | parsing/pcoq.ml | 26 | ||||
-rw-r--r-- | parsing/pcoq.mli | 2 |
3 files changed, 18 insertions, 14 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 5b005186b..20c83dfaf 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -58,6 +58,6 @@ let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = functi | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> | Pcoq.Aself -> <:expr< Pcoq.Aself >> | Pcoq.Anext -> <:expr< Pcoq.Anext >> - | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >> | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >> - | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> + | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry ($str:u$, $str:s$) >> + | Pcoq.Aentryl ((u,s), l) -> <:expr< Pcoq.Aentryl ($str:u$, $str:s$) $mlexpr_of_int l$ >> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b1692e9e2..b244a021e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -76,8 +76,8 @@ type ('self, _) entry_key = | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key | Aself : ('self, 'self) entry_key | Anext : ('self, 'self) entry_key -| Atactic : int -> ('self, Tacexpr.raw_tactic_expr) entry_key | Aentry : (string * string) -> ('self, 'a) entry_key +| Aentryl : (string * string) * int -> ('self, 'a) entry_key type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name @@ -370,8 +370,8 @@ module Tactic = (* Main entries for ltac *) let tactic_arg = Gram.entry_create "tactic:tactic_arg" - let tactic_expr = Gram.entry_create "tactic:tactic_expr" - let binder_tactic = Gram.entry_create "tactic:binder_tactic" + let tactic_expr = make_gen_entry utactic (rawwit wit_tactic) "tactic_expr" + let binder_tactic = make_gen_entry utactic (rawwit wit_tactic) "binder_tactic" let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic" @@ -707,12 +707,12 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function Gram.action (fun _ l _ _loc -> l))] | Aself -> Symbols.sself | Anext -> Symbols.snext - | Atactic 5 -> Symbols.snterm (Gram.Entry.obj Tactic.binder_tactic) - | Atactic n -> - Symbols.snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n) | Aentry (u,s) -> let e = get_entry (get_univ u) s in Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e)) + | Aentryl ((u, s), n) -> + let e = get_entry (get_univ u) s in + Symbols.snterml (Gram.Entry.obj (object_of_typed_entry e), string_of_int n) let level_of_snterml e = int_of_string (Symbols.snterml_level e) @@ -740,6 +740,14 @@ let tactic_level s = let type_of_entry u s = type_of_typed_entry (get_entry u s) +let name_of_entry e = match String.split ':' (Gram.Entry.name e) with +| u :: s :: [] -> (u, s) +| _ -> assert false + +let atactic n = + if n = 5 then Aentry (name_of_entry Tactic.binder_tactic) + else Aentryl (name_of_entry Tactic.tactic_expr, n) + let rec interp_entry_name static up_level s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then @@ -777,7 +785,7 @@ let rec interp_entry_name static up_level s sep = let se = if check_lvl n then Aself else if check_lvl (n + 1) then Anext - else Atactic n + else atactic n in (Some t, se) | None -> @@ -794,10 +802,6 @@ let rec interp_entry_name static up_level s sep = | None -> ExtraArgType s in EntryName (t, se) -let name_of_entry e = match String.split ':' (Gram.Entry.name e) with -| u :: s :: [] -> (u, s) -| _ -> assert false - let list_entry_names () = let add_entry key (entry, _) accu = (key, entry) :: accu in let ans = Hashtbl.fold add_entry (snd uprim) [] in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d13ff548c..959c039d3 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -273,8 +273,8 @@ type ('self, _) entry_key = | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key | Aself : ('self, 'self) entry_key | Anext : ('self, 'self) entry_key -| Atactic : int -> ('self, raw_tactic_expr) entry_key | Aentry : (string * string) -> ('self, 'a) entry_key +| Aentryl : (string * string) * int -> ('self, 'a) entry_key val name_of_entry : 'a Gram.entry -> string * string |