diff options
| -rw-r--r-- | grammar/argextend.ml4 | 62 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 62 | ||||
| -rw-r--r-- | grammar/q_util.mli | 6 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 48 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 13 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 6 |
6 files changed, 102 insertions, 95 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index cb006186a..d976ee019 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -12,6 +12,7 @@ open Genarg open Q_util open Egramml open Compat +open Extend open Pcoq let loc = CompatLoc.ghost @@ -42,37 +43,33 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> let has_extraarg l = let check = function - | ExtNonTerminal(EntryName (t, _), _) -> - begin match Genarg.unquote t with - | ExtraArgType _ -> true - | _ -> false - end + | ExtNonTerminal(ExtraArgType _, _, _) -> true | _ -> false in List.exists check l -let rec is_possibly_empty : type s a. (s, a) entry_key -> bool = function -| Aopt _ -> true -| Alist0 _ -> true -| Alist0sep _ -> true -| Amodifiers _ -> true -| Alist1 t -> is_possibly_empty t -| Alist1sep (t, _) -> is_possibly_empty t +let rec is_possibly_empty = function +| Uopt _ -> true +| Ulist0 _ -> true +| Ulist0sep _ -> true +| Umodifiers _ -> true +| Ulist1 t -> is_possibly_empty t +| Ulist1sep (t, _) -> is_possibly_empty t | _ -> false -let rec get_empty_entry : type s a. (s, a) entry_key -> _ = function -| Aopt _ -> <:expr< None >> -| Alist0 _ -> <:expr< [] >> -| Alist0sep _ -> <:expr< [] >> -| Amodifiers _ -> <:expr< [] >> -| Alist1 t -> <:expr< [$get_empty_entry t$] >> -| Alist1sep (t, _) -> <:expr< [$get_empty_entry t$] >> +let rec get_empty_entry = function +| Uopt _ -> <:expr< None >> +| Ulist0 _ -> <:expr< [] >> +| Ulist0sep _ -> <:expr< [] >> +| Umodifiers _ -> <:expr< [] >> +| Ulist1 t -> <:expr< [$get_empty_entry t$] >> +| Ulist1sep (t, _) -> <:expr< [$get_empty_entry t$] >> | _ -> assert false let statically_known_possibly_empty s (prods,_) = List.for_all (function - | ExtNonTerminal(EntryName (t, e), _) -> - begin match Genarg.unquote t with + | ExtNonTerminal(t, e, _) -> + begin match t with | ExtraArgType s' -> (* For ExtraArg we don't know (we'll have to test dynamically) *) (* unless it is a recursive call *) @@ -91,10 +88,10 @@ let possibly_empty_subentries loc (prods,act) = in let rec aux = function | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >> - | ExtNonTerminal(EntryName (_, e), id) :: tl when is_possibly_empty e -> + | ExtNonTerminal(_, e, id) :: tl when is_possibly_empty e -> bind_name id (get_empty_entry e) (aux tl) - | ExtNonTerminal(EntryName (t, _), id) :: tl -> - let t = match Genarg.unquote t with + | ExtNonTerminal(t, _, id) :: tl -> + let t = match t with | ExtraArgType _ as t -> t | _ -> assert false in @@ -132,8 +129,7 @@ let make_possibly_empty_subentries loc s cl = let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (EntryName (t, _), p) :: tl -> - let t = Genarg.unquote t in + | ExtNonTerminal (t, _, p) :: tl -> let p = Names.Id.to_string p in <:expr< (fun $lid:p$ -> @@ -145,7 +141,7 @@ let make_act loc act pil = let make_prod_item = function | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >> - | ExtNonTerminal (EntryName (_, g), _) -> mlexpr_of_prod_entry_key g + | ExtNonTerminal (_, g, _) -> mlexpr_of_prod_entry_key g let rec make_prod = function | [] -> <:expr< Extend.Stop >> @@ -303,8 +299,8 @@ EXTEND | e = argtype; LIDENT "option" -> OptArgType e ] | "0" [ e = LIDENT -> - let EntryName (t, _) = interp_entry_name false TgAny e "" in - Genarg.unquote t + let e = parse_user_entry e "" in + type_of_user_symbol e | "("; e = argtype; ")" -> e ] ] ; argrule: @@ -312,11 +308,11 @@ EXTEND ; genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let entry = interp_entry_name false TgAny e "" in - ExtNonTerminal (entry, Names.Id.of_string s) + let e = parse_user_entry e "" in + ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let entry = interp_entry_name false TgAny e sep in - ExtNonTerminal (entry, Names.Id.of_string s) + let e = parse_user_entry e sep in + ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then Lexer.add_keyword s; diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 4c1f25941..af9de2df2 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -8,11 +8,12 @@ (* This file defines standard combinators to build ml expressions *) +open Extend open Compat type extend_token = | ExtTerminal of string -| ExtNonTerminal of unit Pcoq.entry_name * Names.Id.t +| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * Names.Id.t let mlexpr_of_list f l = List.fold_right @@ -66,23 +67,44 @@ let mlexpr_of_token = function | Tok.BULLET s -> <:expr< Tok.BULLET $mlexpr_of_string s$ >> | Tok.EOI -> <:expr< Tok.EOI >> -let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = function - | Pcoq.Atoken t -> <:expr< Pcoq.Atoken $mlexpr_of_token t$ >> - | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> - | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Pcoq.Alist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >> - | Pcoq.Alist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Pcoq.Aopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> - | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Pcoq.Aself -> <:expr< Pcoq.Aself >> - | Pcoq.Anext -> <:expr< Pcoq.Anext >> - | Pcoq.Aentry e -> - begin match Entry.repr e with - | Entry.Dynamic s -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >> - | Entry.Static (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >> - end - | Pcoq.Aentryl (e, l) -> - begin match Entry.repr e with - | Entry.Dynamic s -> <:expr< Pcoq.Aentryl (Pcoq.name_of_entry $lid:s$) >> - | Entry.Static (u, s) -> <:expr< Pcoq.Aentryl (Entry.unsafe_of_name ($str:u$, $str:s$)) $mlexpr_of_int l$ >> +let repr_entry e = + let entry u = + let _ = Pcoq.get_entry u e in + Some (Entry.univ_name u, e) + in + try entry Pcoq.uprim with Not_found -> + try entry Pcoq.uconstr with Not_found -> + try entry Pcoq.utactic with Not_found -> None + +let rec mlexpr_of_prod_entry_key = function + | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> + | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> + | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >> + | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> + | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> + | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> + | Extend.Uentry e -> + begin match repr_entry e with + | None -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >> + | Some (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >> end + | Extend.Uentryl (e, l) -> + (** Keep in sync with Pcoq! *) + assert (CString.equal e "tactic"); + if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> + else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> + +let type_entry u e = + let Pcoq.TypedEntry (t, _) = Pcoq.get_entry u e in + Genarg.unquote t + +let rec type_of_user_symbol = function +| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s -> + Genarg.ListArgType (type_of_user_symbol s) +| Uopt s -> + Genarg.OptArgType (type_of_user_symbol s) +| Uentry e | Uentryl (e, _) -> + try type_entry Pcoq.uprim e with Not_found -> + try type_entry Pcoq.uconstr e with Not_found -> + try type_entry Pcoq.utactic e with Not_found -> + Genarg.ExtraArgType e diff --git a/grammar/q_util.mli b/grammar/q_util.mli index d9359de1e..81ad42266 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -10,7 +10,7 @@ open Compat (* necessary for camlp4 *) type extend_token = | ExtTerminal of string -| ExtNonTerminal of unit Pcoq.entry_name * Names.Id.t +| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * Names.Id.t val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr @@ -34,4 +34,6 @@ val mlexpr_of_string : string -> MLast.expr val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr -val mlexpr_of_prod_entry_key : ('self, 'a) Pcoq.entry_key -> MLast.expr +val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr + +val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index a870722fd..7ae9baf72 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -27,24 +27,23 @@ let plugin_name = <:expr< __coq_plugin_name >> let rec make_patt = function | [] -> <:patt< [] >> - | ExtNonTerminal (_, p) :: l -> + | ExtNonTerminal (_, _, p) :: l -> let p = Names.Id.to_string p in <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l let rec make_when loc = function | [] -> <:expr< True >> - | ExtNonTerminal (EntryName (t, _), p) :: l -> + | ExtNonTerminal (t, _, p) :: l -> let p = Names.Id.to_string p in let l = make_when loc l in - let t = mlexpr_of_argtype loc (Genarg.unquote t) in + let t = mlexpr_of_argtype loc t in <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >> | _::l -> make_when loc l let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (EntryName (t, _), p) :: l -> - let t = Genarg.unquote t in + | ExtNonTerminal (t, _, p) :: l -> let p = Names.Id.to_string p in let loc = MLast.loc_of_expr e in let e = make_let raw e l in @@ -56,7 +55,7 @@ let rec make_let raw e = function let rec extract_signature = function | [] -> [] - | ExtNonTerminal (EntryName (t, _), _) :: l -> Genarg.unquote t :: extract_signature l + | ExtNonTerminal (t, _, _) :: l -> t :: extract_signature l | _::l -> extract_signature l @@ -78,18 +77,9 @@ let make_fun_clauses loc s l = let map c = Compat.make_fun loc [make_clause c] in mlexpr_of_list map l -let rec make_args = function - | [] -> <:expr< [] >> - | ExtNonTerminal (EntryName (t, _), p) :: l -> - let t = Genarg.unquote t in - let p = Names.Id.to_string p in - <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >> - | _::l -> make_args l - let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> - | ExtNonTerminal (EntryName (nt, g), id) -> - let nt = Genarg.unquote nt in + | ExtNonTerminal (nt, g, id) -> <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ $mlexpr_of_prod_entry_key g$ >> @@ -98,9 +88,8 @@ let mlexpr_of_clause cl = let rec make_tags loc = function | [] -> <:expr< [] >> - | ExtNonTerminal (EntryName (t, _), p) :: l -> + | ExtNonTerminal (t, _, p) :: l -> let l = make_tags loc l in - let t = Genarg.unquote t in let t = mlexpr_of_argtype loc t in <:expr< [ $t$ :: $l$ ] >> | _::l -> make_tags loc l @@ -115,8 +104,7 @@ let make_one_printing_rule (pt,_,e) = let make_printing_rule r = mlexpr_of_list make_one_printing_rule r let make_empty_check = function -| ExtNonTerminal (EntryName (t, e), _)-> - let t = Genarg.unquote t in +| ExtNonTerminal (t, e, _)-> let is_extra = match t with ExtraArgType _ -> true | _ -> false in if is_possibly_empty e || is_extra then (* This possibly parses epsilon *) @@ -153,17 +141,11 @@ let rec possibly_atomic loc = function (** Special treatment of constr entries *) let is_constr_gram = function | ExtTerminal _ -> false -| ExtNonTerminal (EntryName (_, e), _) -> - match e with - | Aentry e -> - begin match Entry.repr e with - | Entry.Static ("constr", "constr") -> true - | _ -> false - end - | _ -> false +| ExtNonTerminal (_, Extend.Uentry "constr", _) -> true +| _ -> false let make_var = function - | ExtNonTerminal (_, p) -> Some p + | ExtNonTerminal (_, _, p) -> Some p | _ -> assert false let declare_tactic loc s c cl = match cl with @@ -253,11 +235,11 @@ EXTEND ; tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let entry = interp_entry_name false TgAny e "" in - ExtNonTerminal (entry, Names.Id.of_string s) + let e = parse_user_entry e "" in + ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let entry = interp_entry_name false TgAny e sep in - ExtNonTerminal (entry, Names.Id.of_string s) + let e = parse_user_entry e sep in + ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) | s = STRING -> if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal."); ExtTerminal s diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 8de59e5cd..9d78c104e 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -34,8 +34,7 @@ type rule = { let rec make_let e = function | [] -> e - | ExtNonTerminal (EntryName (t, _), p) :: l -> - let t = Genarg.unquote t in + | ExtNonTerminal (t, _, p) :: l -> let p = Names.Id.to_string p in let loc = MLast.loc_of_expr e in let e = make_let e l in @@ -50,7 +49,7 @@ let make_clause { r_patt = pt; r_branch = e; } = (* To avoid warnings *) let mk_ignore c pt = let names = CList.map_filter (function - | ExtNonTerminal (_, p) -> Some (Names.Id.to_string p) + | ExtNonTerminal (_, _, p) -> Some (Names.Id.to_string p) | _ -> None) pt in let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in let names = List.fold_left fold <:expr< () >> names in @@ -181,11 +180,11 @@ EXTEND ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let entry = interp_entry_name false TgAny e "" in - ExtNonTerminal (entry, Names.Id.of_string s) + let e = parse_user_entry e "" in + ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let entry = interp_entry_name false TgAny e sep in - ExtNonTerminal (entry, Names.Id.of_string s) + let e = parse_user_entry e sep in + ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) | s = STRING -> ExtTerminal s ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 592c87919..aa2e092ad 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -153,11 +153,15 @@ type gram_universe = Entry.universe val get_univ : string -> gram_universe +type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry + val uprim : gram_universe val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe +val get_entry : gram_universe -> string -> typed_entry + val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.entry @@ -282,6 +286,8 @@ type _ target = TgAny : 's target | TgTactic : int -> raw_tactic_expr target val interp_entry_name : bool (** true to fail on unknown entry *) -> 's target -> string -> string -> 's entry_name +val parse_user_entry : string -> string -> user_symbol + (** Recover the list of all known tactic notation entries. *) val list_entry_names : unit -> (string * argument_type) list |