From a559727d0a219db79d4230cccc2b4e73c8fc30c8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 18:20:51 +0100 Subject: EXTEND macros use their own internal representations. --- grammar/argextend.ml4 | 30 +++++++++++------------------- grammar/q_util.ml4 | 41 ++++++++++++++++++++++++++++------------- grammar/q_util.mli | 24 ++++++++++++++++++++---- grammar/tacextend.ml4 | 2 +- 4 files changed, 60 insertions(+), 37 deletions(-) (limited to 'grammar') diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index a38f57cdc..f9f3ee988 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -8,10 +8,8 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) -open Genarg open Q_util open Compat -open Extend let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> @@ -25,6 +23,10 @@ let rec make_wit loc = function <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> | ExtraArgType s -> mk_extraarg loc s +let is_self s = function +| ExtraArgType s' -> s = s' +| _ -> false + let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> @@ -79,30 +81,26 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = in let glob = match g with | None -> - begin match rawtyp with - | Genarg.ExtraArgType s' when s = s' -> + if is_self s rawtyp then <:expr< fun ist v -> (ist, v) >> - | _ -> + else <:expr< fun ist v -> let ans = out_gen $make_globwit loc rawtyp$ (Tacintern.intern_genarg ist (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in (ist, ans) >> - end | Some f -> <:expr< fun ist v -> (ist, $lid:f$ ist v) >> in let interp = match f with | None -> - begin match globtyp with - | Genarg.ExtraArgType s' when s = s' -> + if is_self s globtyp then <:expr< fun ist v -> Ftactic.return v >> - | _ -> + else <:expr< fun ist x -> Ftactic.bind (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x)) (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >> - end | Some f -> (** Compatibility layer, TODO: remove me *) <:expr< @@ -114,23 +112,17 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = >> in let subst = match h with | None -> - begin match globtyp with - | Genarg.ExtraArgType s' when s = s' -> + if is_self s globtyp then <:expr< fun s v -> v >> - | _ -> + else <:expr< fun s x -> out_gen $make_globwit loc globtyp$ (Tacsubst.subst_genarg s (Genarg.in_gen $make_globwit loc globtyp$ x)) >> - end | Some f -> <:expr< $lid:f$>> in let dyn = match typ with | `Uniform typ -> - let is_new = match typ with - | Genarg.ExtraArgType s' when s = s' -> true - | _ -> false - in - if is_new then <:expr< None >> + if is_self s typ then <:expr< None >> else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >> | `Specialized _ -> <:expr< None >> in diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 56deb61f3..682188732 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -8,12 +8,27 @@ (* This file defines standard combinators to build ml expressions *) -open Extend open Compat +type argument_type = +| ListArgType of argument_type +| OptArgType of argument_type +| PairArgType of argument_type * argument_type +| ExtraArgType of string + +type user_symbol = +| Ulist1 : user_symbol -> user_symbol +| Ulist1sep : user_symbol * string -> user_symbol +| Ulist0 : user_symbol -> user_symbol +| Ulist0sep : user_symbol * string -> user_symbol +| Uopt : user_symbol -> user_symbol +| Umodifiers : user_symbol -> user_symbol +| Uentry : string -> user_symbol +| Uentryl : string * int -> user_symbol + type extend_token = | ExtTerminal of string -| ExtNonTerminal of Extend.user_symbol * string +| ExtNonTerminal of user_symbol * string let mlexpr_of_list f l = List.fold_right @@ -48,14 +63,14 @@ let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> let rec mlexpr_of_prod_entry_key f = function - | Extend.Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Extend.Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> - | Extend.Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> - | Extend.Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> - | Extend.Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Extend.Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >> - | Extend.Uentry e -> <:expr< Extend.Aentry $f e$ >> - | Extend.Uentryl (e, l) -> + | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >> + | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >> + | Uentry e -> <:expr< Extend.Aentry $f e$ >> + | Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (e = "tactic"); if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> @@ -63,10 +78,10 @@ let rec mlexpr_of_prod_entry_key f = function let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s -> - Genarg.ListArgType (type_of_user_symbol s) + ListArgType (type_of_user_symbol s) | Uopt s -> - Genarg.OptArgType (type_of_user_symbol s) -| Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e + OptArgType (type_of_user_symbol s) +| Uentry e | Uentryl (e, _) -> ExtraArgType e let coincide s pat off = let len = String.length pat in diff --git a/grammar/q_util.mli b/grammar/q_util.mli index c84e9d140..7d4cc0200 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -8,9 +8,25 @@ open Compat (* necessary for camlp4 *) +type argument_type = +| ListArgType of argument_type +| OptArgType of argument_type +| PairArgType of argument_type * argument_type +| ExtraArgType of string + +type user_symbol = +| Ulist1 : user_symbol -> user_symbol +| Ulist1sep : user_symbol * string -> user_symbol +| Ulist0 : user_symbol -> user_symbol +| Ulist0sep : user_symbol * string -> user_symbol +| Uopt : user_symbol -> user_symbol +| Umodifiers : user_symbol -> user_symbol +| Uentry : string -> user_symbol +| Uentryl : string * int -> user_symbol + type extend_token = | ExtTerminal of string -| ExtNonTerminal of Extend.user_symbol * string +| ExtNonTerminal of user_symbol * string val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr @@ -28,8 +44,8 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr val mlexpr_of_ident : string -> MLast.expr -val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr +val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr -val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type +val type_of_user_symbol : user_symbol -> argument_type -val parse_user_entry : string -> string -> Extend.user_symbol +val parse_user_entry : string -> string -> user_symbol diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 51c382b3b..bbd3d8a62 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -68,7 +68,7 @@ let make_printing_rule r = mlexpr_of_list make_one_printing_rule r (** Special treatment of constr entries *) let is_constr_gram = function | ExtTerminal _ -> false -| ExtNonTerminal (Extend.Uentry "constr", _) -> true +| ExtNonTerminal (Uentry "constr", _) -> true | _ -> false let make_var = function -- cgit v1.2.3