From e6127d1f65a761a27c80b81c0f1bc5fca2b74af8 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Thu, 16 Feb 2017 10:24:15 -0500 Subject: [cleanup] Change Id.t option to Name.t in TacFun --- dev/doc/changes.txt | 3 +++ grammar/q_util.mli | 2 ++ grammar/q_util.mlp | 4 ++++ grammar/tacextend.mlp | 2 +- ltac/g_auto.ml4 | 1 + ltac/g_class.ml4 | 1 + ltac/g_eqdecide.ml4 | 1 + ltac/g_ltac.ml4 | 9 +++++---- ltac/pptactic.ml | 4 +--- ltac/tacentries.ml | 5 +---- ltac/tacexpr.mli | 2 +- ltac/tacintern.ml | 6 ++---- ltac/tacinterp.ml | 10 +++++----- ltac/tacinterp.mli | 2 +- ltac/tauto.ml | 2 +- plugins/nsatz/g_nsatz.ml4 | 2 ++ plugins/setoid_ring/newring.ml | 12 ++++++------ plugins/ssrmatching/ssrmatching.ml4 | 2 +- 18 files changed, 39 insertions(+), 31 deletions(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f54f3fcc8..2a083b360 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -40,6 +40,9 @@ important things: - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes +The TacFun tactic expression constructor now takes a `Name.t list` for the +variable list rather than an `Id.t option list`. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For diff --git a/grammar/q_util.mli b/grammar/q_util.mli index a5e36e47b..37ec1d56a 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -41,6 +41,8 @@ val mlexpr_of_string : string -> MLast.expr val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr +val mlexpr_of_name : ('a -> MLast.expr) -> 'a option -> MLast.expr + val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr val type_of_user_symbol : user_symbol -> argument_type diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 919ca3ad7..0dd096ef7 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -58,6 +58,10 @@ let mlexpr_of_option f = function | None -> <:expr< None >> | Some e -> <:expr< Some $f e$ >> +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 rec mlexpr_of_prod_entry_key f = function diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index fe864ed40..8605dda3a 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -88,7 +88,7 @@ let declare_tactic loc s c cl = match cl with 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 vars = mlexpr_of_list (mlexpr_of_name 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 diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index a37cf306e..f32548cd3 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -16,6 +16,7 @@ open Pcoq.Constr open Pltac open Hints open Tacexpr +open Names DECLARE PLUGIN "g_auto" diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index a28132a4b..ca9537c82 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -13,6 +13,7 @@ open Class_tactics open Pltac open Stdarg open Tacarg +open Names DECLARE PLUGIN "g_class" diff --git a/ltac/g_eqdecide.ml4 b/ltac/g_eqdecide.ml4 index 905653281..679aa1127 100644 --- a/ltac/g_eqdecide.ml4 +++ b/ltac/g_eqdecide.ml4 @@ -15,6 +15,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Eqdecide +open Names DECLARE PLUGIN "g_eqdecide" diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 54229bb2a..aab568746 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -17,6 +17,7 @@ open Misctypes open Genarg open Genredexpr open Tok (* necessary for camlp4 *) +open Names open Pcoq open Pcoq.Constr @@ -226,8 +227,8 @@ GEXTEND Gram | "multimatch" -> General ] ] ; input_fun: - [ [ "_" -> None - | l = ident -> Some l ] ] + [ [ "_" -> Anonymous + | l = ident -> Name l ] ] ; let_clause: [ [ id = identref; ":="; te = tactic_expr -> @@ -499,8 +500,8 @@ let pr_tacdef_body tacdef_body = | Tacexpr.TacFun (idl,b) -> idl,b | _ -> [], body in id ++ - prlist (function None -> str " _" - | Some id -> spc () ++ Nameops.pr_id id) idl + prlist (function Anonymous -> str " _" + | Name id -> spc () ++ Nameops.pr_id id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ Pptactic.pr_raw_tactic body diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml index fccee6e40..6f4ef37b4 100644 --- a/ltac/pptactic.ml +++ b/ltac/pptactic.ml @@ -574,9 +574,7 @@ module Make str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - let pr_funvar = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id + let pr_funvar n = spc () ++ pr_name n let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 2e2b55be7..75edf150e 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -504,10 +504,7 @@ let print_ltacs () = | Tacexpr.TacFun (l, t) -> (l, t) | _ -> ([], body) in - let pr_ltac_fun_arg = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id - in + let pr_ltac_fun_arg n = spc () ++ pr_name n in hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) diff --git a/ltac/tacexpr.mli b/ltac/tacexpr.mli index 9c25a1645..e23992a80 100644 --- a/ltac/tacexpr.mli +++ b/ltac/tacexpr.mli @@ -282,7 +282,7 @@ constraint 'a = < > and 'a gen_tactic_fun_ast = - Id.t option list * 'a gen_tactic_expr + Name.t list * 'a gen_tactic_expr constraint 'a = < term:'t; diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 763e0dc22..3292c8353 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -646,7 +646,7 @@ and intern_tactic_or_tacarg ist = intern_tactic false ist and intern_pure_tactic ist = intern_tactic true ist and intern_tactic_fun ist (var,body) = - let lfun = List.fold_left opt_cons ist.ltacvars var in + let lfun = List.fold_left name_cons ist.ltacvars var in (var,intern_tactic_or_tacarg { ist with ltacvars = lfun } body) and intern_tacarg strict onlytac ist = function @@ -722,9 +722,7 @@ let split_ltac_fun = function | TacFun (l,t) -> (l,t) | t -> ([],t) -let pr_ltac_fun_arg = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id +let pr_ltac_fun_arg n = spc () ++ pr_name n let print_ltac id = try diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 32bcdfb6a..adc393d2c 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -120,7 +120,7 @@ let combine_appl appl1 appl2 = (* Values for interpretation *) type tacvalue = | VFun of appl*ltac_trace * value Id.Map.t * - Id.t option list * glob_tactic_expr + Name.t list * glob_tactic_expr | VRec of value Id.Map.t ref * glob_tactic_expr let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = @@ -1087,8 +1087,8 @@ let head_with_value (lvar,lval) = | ([],[]) -> (lacc,[],[]) | (vr::tvr,ve::tve) -> (match vr with - | None -> head_with_value_rec lacc (tvr,tve) - | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) + | Anonymous -> head_with_value_rec lacc (tvr,tve) + | Name v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) | (vr,[]) -> (lacc,vr,[]) | ([],ve) -> (lacc,[],ve) in @@ -2119,8 +2119,8 @@ let lift_constr_tac_to_ml_tac vars tac = let env = Proofview.Goal.env gl in let sigma = project gl in let map = function - | None -> None - | Some id -> + | Anonymous -> None + | Name id -> let c = Id.Map.find id ist.lfun in try Some (coerce_to_closed_constr env c) with CannotCoerceTo ty -> diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 6f64981ef..adbd1d32b 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -115,7 +115,7 @@ val error_ltac_variable : Loc.t -> Id.t -> (** 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 -> +val lift_constr_tac_to_ml_tac : Name.t list -> (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic val default_ist : unit -> Geninterp.interp_sign diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 756958c2f..fb05fd7d0 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -259,7 +259,7 @@ let with_flags flags _ ist = let register_tauto_tactic tac name0 args = let ids = List.map (fun id -> Id.of_string id) args in - let ids = List.map (fun id -> Some id) ids in + let ids = List.map (fun id -> Name id) ids in let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in let entry = { mltac_name = name; mltac_index = 0 } in let () = Tacenv.register_ml_tactic name [| tac |] in diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 5f906a8da..fda7c0fa8 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -10,6 +10,8 @@ DECLARE PLUGIN "nsatz_plugin" (*i camlp4deps: "grammar/grammar.cma" i*) +open Names + DECLARE PLUGIN "nsatz_plugin" TACTIC EXTEND nsatz_compute diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 657efe175..d1f3bd6d3 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -122,7 +122,7 @@ let closed_term_ast l = mltac_index = 0; } in let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in - TacFun([Some(Id.of_string"t")], + TacFun([Name(Id.of_string"t")], TacML(Loc.ghost,tacname, [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])) @@ -205,7 +205,7 @@ let exec_tactic env evd n f args = let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in - let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in + let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in (** Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in @@ -722,8 +722,8 @@ let ltac_ring_structure e = let pow_tac = tacarg e.ring_pow_tac in let lemma1 = carg e.ring_lemma1 in let lemma2 = carg e.ring_lemma2 in - let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in - let posttac = tacarg (TacFun([None],e.ring_post_tac)) in + let pretac = tacarg (TacFun([Anonymous],e.ring_pre_tac)) in + let posttac = tacarg (TacFun([Anonymous],e.ring_post_tac)) in [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] @@ -994,8 +994,8 @@ let ltac_field_structure e = let field_simpl_eq_ok = carg e.field_simpl_eq_ok in let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in let cond_ok = carg e.field_cond in - let pretac = tacarg (TacFun([None],e.field_pre_tac)) in - let posttac = tacarg (TacFun([None],e.field_post_tac)) in + let pretac = tacarg (TacFun([Anonymous],e.field_pre_tac)) in + let posttac = tacarg (TacFun([Anonymous],e.field_post_tac)) in [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index fc988a2c5..ea14bc00a 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1411,7 +1411,7 @@ let () = let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = - TacFun ([Some (Id.of_string "pattern")], + TacFun ([Name (Id.of_string "pattern")], TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in let obj () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in -- cgit v1.2.3