diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 4 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 71 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 10 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 70 |
4 files changed, 84 insertions, 71 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 312f0e9497..dd00bc19a5 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -201,10 +201,10 @@ let declare_tactic loc s c cl = match cl 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 ($dloc$, $se$, [])) >> in - let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in + let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { - let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in + let obj () = Tacenv.register_ltac False $name$ $body$ in try do { Tacenv.register_ml_tactic $se$ $tac$; Mltop.declare_cache_obj obj $plugin_name$; } diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 63aea6f432..9bef0d3bba 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -110,18 +110,6 @@ let register_atomic_ltac id tac = let interp_atomic_ltac id = Id.Map.find id !atomic_mactab -let is_primitive_ltac_ident id = - try - match Pcoq.parse_string Pcoq.Tactic.tactic id with - | Tacexpr.TacArg _ -> false - | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) - with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) - -let is_atomic_kn kn = - let (_,_,l) = repr_kn kn in - (Id.Map.mem (Label.to_id l) !atomic_mactab) - || (is_primitive_ltac_ident (Label.to_string l)) - (***************************************************************************) (* Tactic registration *) @@ -191,60 +179,11 @@ let inMD : bool * (tacdef_kind * glob_tactic_expr) -> obj = subst_function = subst_md; classify_function = classify_md} -(* Adds a definition for tactics in the table *) -let make_absolute_name ident repl = - let loc = loc_of_reference ident in - if repl then - let kn = - try Nametab.locate_tactic (snd (qualid_of_reference ident)) - with Not_found -> - Errors.user_err_loc (loc, "", - str "There is no Ltac named " ++ pr_reference ident ++ str ".") - in - UpdateTac kn - else - let id = Constrexpr_ops.coerce_reference_to_id ident in - let kn = Lib.make_kn id in - let () = if KNmap.mem kn !mactab then - Errors.user_err_loc (loc, "", - str "There is already an Ltac named " ++ pr_reference ident ++ str".") - in - let () = if is_atomic_kn kn then - msg_warning (str "The Ltac name " ++ pr_reference ident ++ - str " may be unusable because of a conflict with a notation.") - in - NewTac id - -let register_ltac local isrec tacl = - let map (ident, local, body) = - let name = make_absolute_name ident local in - (name, body) - in - let rfun = List.map map tacl in - let ltacrecvars = - let fold accu (op, _) = match op with - | UpdateTac _ -> accu - | NewTac id -> Id.Map.add id (Lib.make_kn id) accu - in - if isrec then List.fold_left fold Id.Map.empty rfun - else Id.Map.empty - in - let ist = { (Tacintern.make_empty_glob_sign ()) with Genintern.ltacrecvars; } in - let map (name, body) = - let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in - (name, body) - in - let defs = List.map map rfun in - let iter def = match def with - | NewTac id, _ -> - let _ = Lib.add_leaf id (inMD (local, def)) in - Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined") - | UpdateTac kn, _ -> - let _ = Lib.add_anonymous_leaf (inMD (local, def)) in - let name = Nametab.shortest_qualid_of_tactic kn in - Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined") - in - List.iter iter defs +let register_ltac local id tac = + ignore (Lib.add_leaf id (inMD (local, (NewTac id, tac)))) + +let redefine_ltac local kn tac = + Lib.add_anonymous_leaf (inMD (local, (UpdateTac kn, tac))) let () = Hook.set Tacintern.interp_ltac_hook interp_ltac; diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index c130ef9132..3bc8040d73 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -33,8 +33,14 @@ val register_atomic_ltac : Id.t -> glob_tactic_expr -> unit val interp_atomic_ltac : Id.t -> glob_tactic_expr (** Find a Coq built-in tactic by name. Raise [Not_found] if it is absent. *) -val register_ltac : - Vernacexpr.locality_flag -> bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit +val register_ltac : bool -> Id.t -> glob_tactic_expr -> unit +(** Register a new Ltac with the given name and body. If the boolean flag is set + to true, then this is a local definition. It also puts the Ltac name in the + nametab, so that it can be used unqualified. *) + +val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit +(** Replace a Ltac with the given name and body. If the boolean flag is set + to true, then this is a local redefinition. *) val interp_ltac : KerName.t -> glob_tactic_expr (** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4df08b6a17..4f6b2d5f7e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -887,9 +887,77 @@ let vernac_restore_state file = (************) (* Commands *) +type tacdef_kind = + | NewTac of Id.t + | UpdateTac of Nametab.ltac_constant + +let is_defined_tac kn = + try ignore (Tacenv.interp_ltac kn); true with Not_found -> false + +let make_absolute_name ident repl = + let loc = loc_of_reference ident in + if repl then + let kn = + try Nametab.locate_tactic (snd (qualid_of_reference ident)) + with Not_found -> + Errors.user_err_loc (loc, "", + str "There is no Ltac named " ++ pr_reference ident ++ str ".") + in + UpdateTac kn + else + let id = Constrexpr_ops.coerce_reference_to_id ident in + let kn = Lib.make_kn id in + let () = if is_defined_tac kn then + Errors.user_err_loc (loc, "", + str "There is already an Ltac named " ++ pr_reference ident ++ str".") + in + let is_primitive = + try + match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with + | Tacexpr.TacArg _ -> false + | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) + with e when Errors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) + in + let () = if is_primitive then + msg_warning (str "The Ltac name " ++ pr_reference ident ++ + str " may be unusable because of a conflict with a notation.") + in + NewTac id + +let register_ltac local isrec tacl = + let map (ident, repl, body) = + let name = make_absolute_name ident repl in + (name, body) + in + let rfun = List.map map tacl in + let ltacrecvars = + let fold accu (op, _) = match op with + | UpdateTac _ -> accu + | NewTac id -> Id.Map.add id (Lib.make_kn id) accu + in + if isrec then List.fold_left fold Id.Map.empty rfun + else Id.Map.empty + in + let ist = { (Tacintern.make_empty_glob_sign ()) with Genintern.ltacrecvars; } in + let map (name, body) = + let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in + (name, body) + in + let defs = List.map map rfun in + let iter (def, tac) = match def with + | NewTac id -> + Tacenv.register_ltac local id tac; + Flags.if_verbose msg_info (Nameops.pr_id id ++ str " is defined") + | UpdateTac kn -> + Tacenv.redefine_ltac local kn tac; + let name = Nametab.shortest_qualid_of_tactic kn in + Flags.if_verbose msg_info (Libnames.pr_qualid name ++ str " is redefined") + in + List.iter iter defs + let vernac_declare_tactic_definition locality (x,def) = let local = make_module_locality locality in - Tacenv.register_ltac local x def + register_ltac local x def let vernac_create_hintdb locality id b = let local = make_module_locality locality in |