diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 34 | ||||
| -rw-r--r-- | tactics/coretactics.ml4 | 68 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 20 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 5 |
4 files changed, 71 insertions, 56 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 5a65fe93a3..3afbc8138e 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -10,6 +10,7 @@ open Util open Pp +open Names open Genarg open Q_util open Q_coqast @@ -56,6 +57,8 @@ let rec extract_signature = function | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l | _::l -> extract_signature l + + let check_unicity s l = let l' = List.map (fun (l,_,_) -> extract_signature l) l in if not (Util.List.distinct l') then @@ -159,20 +162,39 @@ let possibly_atomic loc prods = in possibly_empty_subentries loc (List.factorize_left String.equal l) +(** Special treatment of constr entries *) +let is_constr_gram = function +| GramTerminal _ -> false +| GramNonTerminal (_, _, e, _) -> + match e with + | Aentry ("constr", "constr") -> true + | _ -> false + +let make_vars len = + (** We choose names unlikely to be written by a human, even though that + does not matter at all. *) + List.init len (fun i -> Some (Id.of_string (Printf.sprintf "_%i" i))) + let declare_tactic loc s c cl = match cl with -| [[GramTerminal name], _, tac] -> - (** The extension is only made of a name: we do not add any grammar nor - printing rule and add it as a true Ltac definition. *) +| [(GramTerminal 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 = make_vars (List.length rem) in + let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in let se = mlexpr_of_string s in let name = mlexpr_of_string name in - let tac = <:expr< fun _ $lid:"ist"$ -> $tac$ >> in - let body = <:expr< Tacexpr.TacAtom ($dloc$, Tacexpr.TacExtend($dloc$, $se$, [])) >> in + let tac = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in + (** Arguments are not passed directly to the ML tactic in the TacExtend 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.TacAtom ($dloc$, Tacexpr.TacExtend($dloc$, $se$, []))) >> in let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in declare_str_items loc [ <:str_item< do { let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in try do { - Tacenv.register_ml_tactic $se$ $tac$; + Tacenv.register_ml_tactic $se$ (Tacinterp.lift_constr_tac_to_ml_tac $vars$ $tac$); Mltop.declare_cache_obj obj __coq_plugin_name; } with [ e when Errors.noncritical e -> Pp.msg_warning diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 2434d3f453..d3b9dd1325 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -23,58 +23,26 @@ TACTIC EXTEND assumption [ "assumption" ] -> [ Tactics.assumption ] END -let make_vars len = - List.init len (fun i -> Id.of_string (Printf.sprintf "_%i" i)) - -let dummy_id = Id.of_string "_" - -(** Add a tactic that only uses constrs arguments. Such tactics actually do - not need to define grammar rules, because tactic arguments are already - parsed as constrs. So we add them manually. *) -(** TODO: do this automagically in TACTIC EXTEND and use it in this file *) -let add_constr_tactic name len tac = - let vars = make_vars len in - (** We pass the arguments through the environment rather than through the - tactic, to overcome the way tactics arguments are interpreted. *) - let tac _ ist = Proofview.Goal.raw_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let map id = - let c = Id.Map.find id ist.lfun in - try Taccoerce.coerce_to_closed_constr env c - with Taccoerce.CannotCoerceTo ty -> - error_ltac_variable Loc.ghost dummy_id (Some env) c ty - in - let args = List.map map vars in - tac args ist - end in - let () = Tacenv.register_ml_tactic name tac in - let ref = Libnames.Ident (Loc.ghost, Id.of_string name) in - let args = List.map (fun id -> Some id) vars in - let body = TacExtend (Loc.ghost, name, []) in - let body = TacFun (args, TacAtom (Loc.ghost, body)) in - let obj () = Tacenv.register_ltac false false [ref, false, body] in - Mltop.declare_cache_obj obj "coretactics" - -let () = - let tac args _ = match args with [c] _ -> Tactics.cut c | _ -> assert false in - add_constr_tactic "cut" 1 tac +TACTIC EXTEND cut + [ "cut" constr(c) ] -> [ Tactics.cut c ] +END -let () = - let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.exact_no_check c) | _ -> assert false in - add_constr_tactic "exact_no_check" 1 tac +TACTIC EXTEND exact_no_check + [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ] +END -let () = - let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.vm_cast_no_check c) | _ -> assert false in - add_constr_tactic "vm_cast_no_check" 1 tac +TACTIC EXTEND vm_cast_no_check + [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ] +END -let () = - let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.case_type c) | _ -> assert false in - add_constr_tactic "casetype" 1 tac +TACTIC EXTEND casetype + [ "casetype" constr(c) ] -> [ Proofview.V82.tactic (Tactics.case_type c) ] +END -let () = - let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.elim_type c) | _ -> assert false in - add_constr_tactic "elimtype" 1 tac +TACTIC EXTEND elimtype + [ "elimtype" constr(c) ] -> [ Proofview.V82.tactic (Tactics.elim_type c) ] +END -let () = - let tac args _ = match args with [c] -> Tactics.cut_and_apply c | _ -> assert false in - add_constr_tactic "lapply" 1 tac +TACTIC EXTEND lapply + [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ] +END diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4333c5696d..a992c52ce1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2109,3 +2109,23 @@ let _ = Hook.set Auto.extern_interp let lfun = Id.Map.map (fun c -> Value.of_constr c) l in let ist = { (default_ist ()) with lfun; } in interp_tactic ist) + +(** Used in tactic extension **) + +let dummy_id = Id.of_string "_" + +let lift_constr_tac_to_ml_tac vars tac = + let tac _ ist = Proofview.Goal.raw_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let map = function + | None -> None + | Some id -> + let c = Id.Map.find id ist.lfun in + try Some (coerce_to_closed_constr env c) + with CannotCoerceTo ty -> + error_ltac_variable Loc.ghost dummy_id (Some env) c ty + in + let args = List.map_filter map vars in + tac args ist + end in + tac diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 090fb1ccab..71721427a7 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -113,3 +113,8 @@ val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> Id.t val interp_int : interp_sign -> Id.t Loc.located -> int val error_ltac_variable : Loc.t -> Id.t -> Environ.env option -> value -> string -> 'a + +(** Transforms a constr-expecting tactic into a tactic finding its arguments in + the Ltac environment according to the given names. *) +val lift_constr_tac_to_ml_tac : Id.t option list -> + (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic |