From 661940fd55a925a6f17f6025f5d15fc9f5647cf9 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 10 Oct 2016 10:59:22 +0200 Subject: Put all plugins behind an "API". --- grammar/argextend.mlp | 34 +++++++++++++++++----------------- grammar/q_util.mlp | 18 +++++++++--------- grammar/tacextend.mlp | 22 +++++++++++----------- grammar/vernacextend.mlp | 18 +++++++++--------- 4 files changed, 46 insertions(+), 46 deletions(-) (limited to 'grammar') diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 5068ba8a6..36b9d612a 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -46,17 +46,17 @@ let make_act loc act pil = make (List.rev pil) let make_prod_item = function - | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> + | ExtTerminal s -> <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $mlexpr_of_string s$) >> | ExtNonTerminal (g, _) -> let base s = <:expr< $lid:s$ >> in mlexpr_of_prod_entry_key base g let rec make_prod = function -| [] -> <:expr< Extend.Stop >> -| item :: prods -> <:expr< Extend.Next $make_prod prods$ $make_prod_item item$ >> +| [] -> <:expr< Grammar_API.Extend.Stop >> +| item :: prods -> <:expr< Grammar_API.Extend.Next $make_prod prods$ $make_prod_item item$ >> let make_rule loc (prods,act) = - <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> + <:expr< Grammar_API.Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> let is_ident x = function | <:expr< $lid:s$ >> -> (s : string) = x @@ -67,7 +67,7 @@ let make_extend loc s cl wit = match cl with (** Special handling of identity arguments by not redeclaring an entry *) <:str_item< value $lid:s$ = - let () = Pcoq.register_grammar $wit$ $lid:e$ in + let () = Grammar_API.Pcoq.register_grammar $wit$ $lid:e$ in $lid:e$ >> | _ -> @@ -75,8 +75,8 @@ let make_extend loc s cl wit = match cl with let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< value $lid:s$ = - let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in - let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in + let $lid:s$ = Grammar_API.Pcoq.create_generic_entry Grammar_API.Pcoq.utactic $se$ (Genarg.rawwit $wit$) in + let () = Grammar_API.Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in $lid:s$ >> let warning_redundant prefix s = @@ -127,7 +127,7 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = begin match globtyp with | None -> let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in - <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >> + <:expr< fun ist v -> API.Ftactic.return (API.Geninterp.Val.inject (API.Geninterp.val_tag $make_topwit loc typ$) v) >> | Some globtyp -> <:expr< fun ist x -> Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >> @@ -137,10 +137,10 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in <:expr< let f = $lid:f$ in - fun ist v -> Ftactic.nf_enter (fun gl -> - let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in - let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v) + fun ist v -> API.Ftactic.nf_enter (fun gl -> + let (sigma, v) = API.Tacmach.New.of_old (fun gl -> f ist gl v) gl in + let v = API.Geninterp.Val.inject (API.Geninterp.val_tag $make_topwit loc typ$) v in + API.Proofview.tclTHEN (API.Proofview.Unsafe.tclEVARS sigma) (API.Ftactic.return v) ) >> in let subst = match h with @@ -156,15 +156,15 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = | Some f -> <:expr< $lid:f$>> in let dyn = match typ with | None -> <:expr< None >> - | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >> + | Some typ -> <:expr< Some (API.Geninterp.val_tag $make_topwit loc typ$) >> in let wit = <:expr< $lid:"wit_"^s$ >> in declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>; - <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; - <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; - <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; - <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>; + <:str_item< Grammar_API.Genintern.register_intern0 $wit$ $glob$ >>; + <:str_item< Grammar_API.Genintern.register_subst0 $wit$ $subst$ >>; + <:str_item< API.Geninterp.register_interp0 $wit$ $interp$ >>; + <:str_item< API.Geninterp.register_val0 $wit$ $dyn$ >>; make_extend loc s cl wit; <:str_item< do { Pptactic.declare_extra_genarg_pprule diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 87262e1c8..7d309cf0d 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -60,20 +60,20 @@ let mlexpr_of_name f = function | None -> <:expr< Anonymous >> | Some e -> <:expr< Name $f e$ >> -let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> +let symbol_of_string s = <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $str:s$) >> let rec mlexpr_of_prod_entry_key f = function - | 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$ $symbol_of_string 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$ $symbol_of_string sep$ >> - | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Uentry e -> <:expr< Extend.Aentry $f e$ >> + | Ulist1 s -> <:expr< Grammar_API.Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Ulist1sep (s,sep) -> <:expr< Grammar_API.Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> + | Ulist0 s -> <:expr< Grammar_API.Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Ulist0sep (s,sep) -> <:expr< Grammar_API.Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> + | Uopt s -> <:expr< Grammar_API.Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Uentry e -> <:expr< Grammar_API.Extend.Aentry ($f e$) >> | Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (e = "tactic"); - if l = 5 then <:expr< Extend.Aentry (Pltac.binder_tactic) >> - else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> + if l = 5 then <:expr< Grammar_API.Extend.Aentry Pltac.binder_tactic >> + else <:expr< Grammar_API.Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 8e3dccf47..8f3f7a9de 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -25,7 +25,7 @@ let plugin_name = <:expr< __coq_plugin_name >> let mlexpr_of_ident id = (** Workaround for badly-designed generic arguments lacking a closure *) let id = "$" ^ id in - <:expr< Names.Id.of_string_soft $str:id$ >> + <:expr< API.Names.Id.of_string_soft $str:id$ >> let rec make_patt = function | [] -> <:patt< [] >> @@ -57,18 +57,18 @@ let make_fun_clauses loc s l = let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> +| Ulist1 s -> <:expr< Grammar_API.Extend.Ulist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Grammar_API.Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Grammar_API.Extend.Ulist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Grammar_API.Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Grammar_API.Extend.Uopt $mlexpr_of_symbol s$ >> | Uentry e -> let arg = get_argt <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> + <:expr< Grammar_API.Extend.Uentry (Genarg.ArgT.Any $arg$) >> | Uentryl (e, l) -> assert (e = "tactic"); let arg = get_argt <:expr< Tacarg.wit_tactic >> in - <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> + <:expr< Grammar_API.Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> let make_prod_item = function | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> @@ -113,12 +113,12 @@ let declare_tactic loc tacname ~level classification clause = match clause with the ML tactic retrieves its arguments in the [ist] environment instead. This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML (Loc.tag ( $ml$ , []))) >> in - let name = <:expr< Names.Id.of_string $name$ >> in + let name = <:expr< API.Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { let obj () = Tacenv.register_ltac True False $name$ $body$ in let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in - Mltop.declare_cache_obj obj $plugin_name$ } >> + API.Mltop.declare_cache_obj obj $plugin_name$ } >> ] | _ -> (** Otherwise we add parsing and printing rules to generate a call to a @@ -131,7 +131,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with declare_str_items loc [ <:str_item< do { Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$); - Mltop.declare_cache_obj $obj$ $plugin_name$; } >> + Grammar_API.Mltop.declare_cache_obj $obj$ $plugin_name$; } >> ] open Pcaml diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 798b46523..6f0e9b7cf 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -100,12 +100,12 @@ let make_fun_classifiers loc s c l = mlexpr_of_list (fun x -> x) cl let make_prod_item = function - | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | ExtTerminal s -> <:expr< Grammar_API.Egramml.GramTerminal $str:s$ >> | ExtNonTerminal (g, ido) -> let nt = type_of_user_symbol g in - let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in + let base s = <:expr< Grammar_API.Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in let typ = match ido with None -> None | Some _ -> Some nt in - <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ , + <:expr< Grammar_API.Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ , $mlexpr_of_prod_entry_key base g$ ) ) >> let mlexpr_of_clause cl = @@ -122,9 +122,9 @@ let declare_command loc s c nt cl = let classl = make_fun_classifiers loc s c cl in declare_str_items loc [ <:str_item< do { - CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; - CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$; - CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; + CList.iteri (fun i (depr, f) -> Grammar_API.Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; + CList.iteri (fun i f -> API.Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$; + CList.iteri (fun i r -> Grammar_API.Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; } >> ] open Pcaml @@ -143,16 +143,16 @@ EXTEND | "DECLARE"; "PLUGIN"; name = STRING -> declare_str_items loc [ <:str_item< value __coq_plugin_name = $str:name$ >>; - <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>; + <:str_item< value _ = Grammar_API.Mltop.add_known_module __coq_plugin_name >>; ] ] ] ; classification: [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> | "CLASSIFIED"; "AS"; "SIDEFF" -> - <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >> + <:expr< fun _ -> API.Vernac_classifier.classify_as_sideeff >> | "CLASSIFIED"; "AS"; "QUERY" -> - <:expr< fun _ -> Vernac_classifier.classify_as_query >> + <:expr< fun _ -> API.Vernac_classifier.classify_as_query >> ] ] ; deprecation: -- cgit v1.2.3