From b16633a5dc044e5d95c73b4c912ec7232f9caf12 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 23 Oct 2017 14:27:04 +0200 Subject: Make most of TACTIC EXTEND macros runtime calls. Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros. --- grammar/tacextend.mlp | 142 ++++++++++------------------------------------- grammar/vernacextend.mlp | 16 +++++- 2 files changed, 44 insertions(+), 114 deletions(-) (limited to 'grammar') diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 6c072e36a..525be6432 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -13,15 +13,6 @@ open Q_util open Argextend -(** Quotation difference for match clauses *) - -let default_patt loc = - (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>) - -let make_fun loc cl = - let l = cl @ [default_patt loc] in - MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) - let plugin_name = <:expr< __coq_plugin_name >> let mlexpr_of_ident id = @@ -29,112 +20,33 @@ let mlexpr_of_ident id = let id = "$" ^ id in <:expr< Names.Id.of_string_soft $str:id$ >> -let rec make_patt = function - | [] -> <:patt< [] >> - | ExtNonTerminal (_, Some p) :: l -> - <:patt< [ $lid:p$ :: $make_patt l$ ] >> - | _::l -> make_patt l - -let rec make_let raw e = function - | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (g, Some p) :: l -> - let t = type_of_user_symbol g in - let loc = MLast.loc_of_expr e in - let e = make_let raw e l in - let v = - if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> - else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in - <:expr< let $lid:p$ = $v$ in $e$ >> - | _::l -> make_let raw e l - -let make_clause (pt,e) = - (make_patt pt, - ploc_vala None, - make_let false e pt) - -let make_fun_clauses loc s l = - let map c = make_fun loc [make_clause c] in - mlexpr_of_list map 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< Extend.TUlist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> | Uentry e -> - let arg = get_argt <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> | 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$>> - -let make_prod_item = function - | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> - | ExtNonTerminal (g, id) -> - <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option mlexpr_of_ident id$ ) ) >> - -let mlexpr_of_clause cl = - mlexpr_of_list (fun (a,_) -> mlexpr_of_list make_prod_item a) cl - -(** Special treatment of constr entries *) -let is_constr_gram = function -| ExtTerminal _ -> false -| ExtNonTerminal (Uentry "constr", _) -> true -| _ -> false - -let make_var = function - | ExtNonTerminal (_, p) -> p - | _ -> assert false - -let declare_tactic loc tacname ~level clause = match clause with -| [(ExtTerminal name) :: rem, tac] when List.for_all is_constr_gram rem -> - (** The extension is only made of a name followed by constr entries: we do not - add any grammar nor printing rule and add it as a true Ltac definition. *) - let patt = make_patt rem in - let vars = List.map make_var rem in - let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in - let entry = mlexpr_of_string tacname in - let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in - let name = mlexpr_of_string name in - let tac = match rem with - | [] -> - (** Special handling of tactics without arguments: such tactics do not do - a Proofview.Goal.nf_enter to compute their arguments. It matters for some - whole-prof tactics like [shelve_unifiable]. *) - <:expr< fun _ $lid:"ist"$ -> $tac$ >> - | _ -> - let f = make_fun loc [patt, ploc_vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in - <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> - in - (** Arguments are not passed directly to the ML tactic in the TacML node, - 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 - 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$ } >> - ] -| _ -> - (** Otherwise we add parsing and printing rules to generate a call to a - TacML tactic. *) - let entry = mlexpr_of_string tacname in - let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let gl = mlexpr_of_clause clause in - let level = mlexpr_of_int level in - let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in - 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$; } >> - ] + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> + +let rec mlexpr_of_clause = function +| [] -> <:expr< TyNil >> +| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> +| ExtNonTerminal(g,None) :: cl -> + <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >> +| ExtNonTerminal(g,Some id) :: cl -> + <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >> + +let rec binders_of_clause e = function +| [] -> <:expr< fun ist -> $e$ >> +| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl +| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >> +| _ :: cl -> binders_of_clause e cl open Pcaml @@ -146,13 +58,17 @@ EXTEND OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> let level = match level with Some i -> int_of_string i | None -> 0 in - declare_tactic loc s ~level l ] ] + let level = mlexpr_of_int level in + let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in + declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ] ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; - "->"; "["; e = Pcaml.expr; "]" -> (l,e) + "->"; "["; e = Pcaml.expr; "]" -> + <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >> ] ] ; + tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 24ee0042b..a2872d07f 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -12,7 +12,6 @@ open Q_util open Argextend -open Tacextend type rule = { r_head : string option; @@ -27,6 +26,21 @@ type rule = { (** Whether this entry is deprecated *) } +(** Quotation difference for match clauses *) + +let default_patt loc = + (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>) + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) + +let rec make_patt = function + | [] -> <:patt< [] >> + | ExtNonTerminal (_, Some p) :: l -> + <:patt< [ $lid:p$ :: $make_patt l$ ] >> + | _::l -> make_patt l + let rec make_let e = function | [] -> e | ExtNonTerminal (g, Some p) :: l -> -- cgit v1.2.3