diff options
Diffstat (limited to 'grammar/tacextend.mlp')
| -rw-r--r-- | grammar/tacextend.mlp | 170 |
1 files changed, 170 insertions, 0 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp new file mode 100644 index 00000000..683a7e2f --- /dev/null +++ b/grammar/tacextend.mlp @@ -0,0 +1,170 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Implementation of the TACTIC EXTEND macro. *) + +open Q_util +open Argextend +open GramCompat + +let dloc = <:expr< Loc.ghost >> + +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$ >> + +let rec make_patt = function + | [] -> <:patt< [] >> + | ExtNonTerminal (_, 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, 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, + vala None, + make_let false e pt) + +let make_fun_clauses loc s l = + let map c = GramCompat.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$ >> +| Uentry e -> + let arg = get_argt <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> +| Uentryl (e, l) -> + assert (e = "tactic"); + let arg = get_argt <:expr< Constrarg.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 $default_loc$ $mlexpr_of_symbol g$ $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) -> Some p + | _ -> assert false + +let declare_tactic loc s c cl = match cl 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_option mlexpr_of_ident) vars in + let entry = mlexpr_of_string s 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 = GramCompat.make_fun loc [patt, 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 ($dloc$, $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 s in + let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in + let gl = mlexpr_of_clause cl in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in + declare_str_items loc + [ <:str_item< do { + Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); + Mltop.declare_cache_obj $obj$ $plugin_name$; } >> + ] + +open Pcaml +open PcamlSig (* necessary for camlp4 *) + +EXTEND + GLOBAL: str_item; + str_item: + [ [ "TACTIC"; "EXTEND"; s = tac_name; + c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ]; + OPT "|"; l = LIST1 tacrule SEP "|"; + "END" -> + declare_tactic loc s c l ] ] + ; + tacrule: + [ [ "["; l = LIST1 tacargs; "]"; + c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ]; + "->"; "["; e = Pcaml.expr; "]" -> + (match l with + | ExtNonTerminal _ :: _ -> + (* En attendant la syntaxe de tacticielles *) + failwith "Tactic syntax must start with an identifier" + | _ -> (l,c,e)) + ] ] + ; + tacargs: + [ [ e = LIDENT; "("; s = LIDENT; ")" -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, s) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let e = parse_user_entry e sep in + ExtNonTerminal (e, s) + | s = STRING -> + let () = if s = "" then failwith "Empty terminal." in + ExtTerminal s + ] ] + ; + tac_name: + [ [ s = LIDENT -> s + | s = UIDENT -> s + ] ] + ; + END |