From 93d0b93ed3cb06ec9e3a355d8d5896cf12655a91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Sat, 22 Apr 2023 09:53:11 +0200 Subject: [PATCH] Ltac2: warn on unused variables Close #18637 To be decided: - should we warn for variable names starting with `_`? (current code does) - should we split the warning like ocaml does (unused `let x := ...` treated differently from unused `x` next to used `y` in `match ... with (x,y) => ...` or unused `x` in `fun x => ...`) TODO: more precise locations, currently it's on the whole expression ie all of `let x := ... in ...` just `x` would be nicer. --- plugins/ltac2/tac2intern.ml | 30 ++++++++++++++++++++++++++++-- plugins/ltac2/tac2typing_env.ml | 26 +++++++++++++++++++++----- plugins/ltac2/tac2typing_env.mli | 2 ++ user-contrib/Ltac2/Array.v | 6 +++--- user-contrib/Ltac2/List.v | 12 ++++++------ user-contrib/Ltac2/Notations.v | 2 +- 6 files changed, 61 insertions(+), 17 deletions(-) diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml index 5c4457835eeb6..06e4b109170cf 100644 --- a/plugins/ltac2/tac2intern.ml +++ b/plugins/ltac2/tac2intern.ml @@ -1108,6 +1108,19 @@ let expand_notation ?loc el kn = assert (Id.Map.is_empty argtys); CAst.make ?loc @@ CTacGlb (prms, el, body, ty) +let warn_unused_variables = CWarnings.create ~name:"ltac2-unused-variable" + ~category:CWarnings.CoreCategories.ltac2 + Pp.(fun ids -> str "Unused variables:" ++ spc() ++ prlist_with_sep spc Id.print ids ++ str ".") + +let check_unused_variables ?loc env to_name bnd = + let unused = List.filter_map (fun bnd -> match to_name bnd with + | Anonymous -> None + | Name id -> if is_used_var id env then None else Some id) + bnd + in + if CList.is_empty unused then () + else warn_unused_variables ?loc unused + let rec intern_rec env tycon {loc;v=e} = let check et = check ?loc env tycon et in match e with @@ -1151,6 +1164,10 @@ let rec intern_rec env tycon {loc;v=e} = env, tycon) (env,tycon) nas tl in let (e, t) = intern_rec env tycon (exp e) in + let () = + (* TODO better loc? *) + check_unused_variables ?loc env (fun x -> x) nas + in let t = match tycon with | None -> List.fold_right (fun t accu -> GTypArrow (t, accu)) tl t | Some tycon -> tycon @@ -1201,7 +1218,7 @@ let rec intern_rec env tycon {loc;v=e} = times in this matching") in let ids = List.fold_left fold Id.Set.empty el in - if is_rec then intern_let_rec env el tycon e + if is_rec then intern_let_rec env loc el tycon e else intern_let env loc ids el tycon e | CTacSyn (el, kn) -> let v = expand_notation ?loc el kn in @@ -1379,10 +1396,11 @@ and intern_let env loc ids el tycon e = let (e, elp) = List.fold_left_map fold e el in let env = List.fold_left (fun accu (na, _, t) -> push_name na t accu) env elp in let (e, t) = intern_rec env tycon e in + let () = check_unused_variables ?loc env pi1 elp in let el = List.map (fun (na, e, _) -> na, e) elp in (GTacLet (false, el, e), t) -and intern_let_rec env el tycon e = +and intern_let_rec env loc el tycon e = let map env (pat, t, e) = let na = match pat.v with | CPatVar na -> na @@ -1443,6 +1461,10 @@ and intern_let_rec env el tycon e = in let el = List.map map el in let (e, t) = intern_rec env tycon e in + let () = + (* TODO better loc? *) + check_unused_variables ?loc env fst el + in (GTacLet (true, el, e), t) and intern_constructor env loc tycon kn args = match kn with @@ -1509,6 +1531,7 @@ and intern_case env loc e tycon pl = let patvars, pat = intern_pat env cpat et in let patenv = push_ids patvars env in let br = intern_rec_with_constraint patenv cbr rt in + let () = check_unused_variables ?loc patenv (fun (id,_) -> Name id) (Id.Map.bindings patvars) in pat, br) pl in @@ -1521,6 +1544,7 @@ type context = (Id.t * type_scheme) list let intern ~strict ctx e = let env = empty_env ~strict () in + (* XXX not doing check_unused_variables *) let fold accu (id, t) = push_name (Name id) (polymorphic t) accu in let env = List.fold_left fold env ctx in let (e, t) = intern_rec env None e in @@ -2037,6 +2061,7 @@ let () = let env = List.fold_left fold env ids in let loc = tac.loc in let (tac, t) = intern_rec env None tac in + let () = check_unused_variables ?loc env (fun x -> Name x) ids in let () = check_elt_unit loc env t in (ist, (ids, tac)) in @@ -2084,6 +2109,7 @@ let () = let ids, env = Id.Map.fold fold ntn_vars (Id.Set.empty, env) in let loc = tac.loc in let (tac, t) = intern_rec env None tac in + let () = check_unused_variables ?loc env (fun x -> Name x) (Id.Set.elements ids) in let () = check_elt_unit loc env t in (ist, (ids, tac)) in diff --git a/plugins/ltac2/tac2typing_env.ml b/plugins/ltac2/tac2typing_env.ml index 71bfbfc477f53..28ea321e01552 100644 --- a/plugins/ltac2/tac2typing_env.ml +++ b/plugins/ltac2/tac2typing_env.ml @@ -101,8 +101,12 @@ type mix_var = type mix_type_scheme = int * mix_var glb_typexpr +(* Changing the APIs enough to get which variables are used in random genargs seems very hard + so instead we use mutation to detect them *) +type used = { mutable used : bool } + type t = { - env_var : mix_type_scheme Id.Map.t; + env_var : (mix_type_scheme * used) Id.Map.t; (** Type schemes of bound variables *) env_cst : UF.elt glb_typexpr UF.t; (** Unification state *) @@ -135,7 +139,14 @@ let find_rec_var id env = Id.Map.find_opt id env.env_rec let mem_var id env = Id.Map.mem id env.env_var -let find_var id env = Id.Map.find id env.env_var +let find_var id env = + let t, used = Id.Map.find id env.env_var in + used.used <- true; + t + +let is_used_var id env = + let _, {used} = Id.Map.find id env.env_var in + used let bound_vars env = Id.Map.domain env.env_var @@ -196,10 +207,15 @@ let get_alias {CAst.loc;v=id} env = let push_name id t env = match id with | Anonymous -> env -| Name id -> { env with env_var = Id.Map.add id t env.env_var } +| Name id -> { env with env_var = Id.Map.add id (t, {used=false}) env.env_var } let push_ids ids env = - { env with env_var = Id.Map.union (fun _ x _ -> Some x) ids env.env_var } + let merge_fun _ fresh orig = match fresh, orig with + | None, None -> assert false + | Some x, _ -> Some (x, {used=false}) + | None, Some x -> Some x + in + { env with env_var = Id.Map.merge merge_fun ids env.env_var } let rec subst_type subst (t : 'a glb_typexpr) = match t with | GTypVar id -> subst id @@ -346,7 +362,7 @@ let fv_env env = | id, None -> UF.Map.add id () accu | _, Some t -> fv_type f t accu in - let fold_var id (_, t) accu = + let fold_var id ((_, t), _) accu = let fmix id accu = match id with | LVar _ -> accu | GVar id -> f id accu diff --git a/plugins/ltac2/tac2typing_env.mli b/plugins/ltac2/tac2typing_env.mli index 95ae367cedf31..7717ad0336bf6 100644 --- a/plugins/ltac2/tac2typing_env.mli +++ b/plugins/ltac2/tac2typing_env.mli @@ -48,6 +48,8 @@ val mem_var : Id.t -> t -> bool val find_var : Id.t -> t -> mix_type_scheme +val is_used_var : Id.t -> t -> bool + val bound_vars : t -> Id.Set.t val get_variable0 : (Id.t -> bool) -> tacref or_relid -> tacref Locus.or_var diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v index 2bf4f6d5c246a..eea85087e7874 100644 --- a/user-contrib/Ltac2/Array.v +++ b/user-contrib/Ltac2/Array.v @@ -75,8 +75,8 @@ Ltac2 init (l : int) (f : int->'a) := end. Ltac2 make_matrix (sx : int) (sy : int) (v : 'a) := - let init1 i := v in - let initr i := init sy init1 in + let init1 _ := v in + let initr _ := init sy init1 in init sx initr. Ltac2 copy a := lowlevel_sub a 0 (length a). @@ -175,7 +175,7 @@ Ltac2 of_list (ls : 'a list) := end in match ls with | [] => empty - | hd::tl => + | hd :: _ => let anew := make (list_length ls) hd in of_list_aux ls anew 0; anew diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v index 10b769206c7c7..d918894484a36 100644 --- a/user-contrib/Ltac2/List.v +++ b/user-contrib/Ltac2/List.v @@ -71,19 +71,19 @@ Ltac2 cons (x : 'a) (xs : 'a list) := Ltac2 hd_opt (ls : 'a list) := match ls with | [] => None - | x :: xs => Some x + | x :: _ => Some x end. Ltac2 hd (ls : 'a list) := match ls with | [] => Control.throw_invalid_argument "List.hd" - | x :: xs => x + | x :: _ => x end. Ltac2 tl (ls : 'a list) := match ls with | [] => [] - | x :: xs => xs + | _ :: xs => xs end. Ltac2 dest (xs : 'a list) : 'a * 'a list := @@ -332,7 +332,7 @@ Ltac2 rec for_all2_aux (on_length_mismatch : 'a list -> 'b list -> bool) f xs ys match xs with | [] => match ys with | [] => true - | y :: ys' => on_length_mismatch xs ys + | _ :: _ => on_length_mismatch xs ys end | x :: xs' => match ys with @@ -352,7 +352,7 @@ Ltac2 rec exist2 f xs ys := match xs with | [] => match ys with | [] => false - | y :: ys' => Control.throw_invalid_argument "List.exist2" + | _ :: _ => Control.throw_invalid_argument "List.exist2" end | x :: xs' => match ys with @@ -473,7 +473,7 @@ Ltac2 rec skipn (n : int) (ls : 'a list) := | false => match ls with | [] => Control.throw_out_of_bounds "List.skipn" - | x :: xs + | _ :: xs => skipn (Int.sub n 1) xs end end. diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v index b98f892627cb2..e661635198e7a 100644 --- a/user-contrib/Ltac2/Notations.v +++ b/user-contrib/Ltac2/Notations.v @@ -246,7 +246,7 @@ match cl with end. Ltac2 pose0 ev p := - enter_h ev (fun ev (na, p) => Std.pose na p) p. + enter_h ev (fun _ (na, p) => Std.pose na p) p. Ltac2 Notation "pose" p(thunk(pose)) := pose0 false p.