feat(sanity_check): improve sanity_check

src/data/list/defs.lean

@@ -395,7 +395,7 @@ variable {R}
 instance decidable_chain [decidable_rel R] (a : α) (l : list α) : decidable (chain R a l) :=
 by induction l generalizing a; simp only [chain.nil, chain_cons]; resetI; apply_instance
 
-instance decidable_chain' [decidable_rel R] (a : α) (l : list α) : decidable (chain' R l) :=
+instance decidable_chain' [decidable_rel R] (l : list α) : decidable (chain' R l) :=
 by cases l; dunfold chain'; apply_instance
 
 end chain

src/meta/expr.lean

@@ -15,6 +15,19 @@ Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lew
  expr, name, declaration, level, environment, meta, metaprogramming, tactic
 -/
 
+namespace binder_info
+
+instance : inhabited binder_info := ⟨ binder_info.default ⟩
+
+/-- The brackets corresponding to a given binder_info. -/
+def brackets : binder_info → string × string
+| binder_info.implicit        := ("{", "}")
+| binder_info.strict_implicit := ("{{", "}}")
+| binder_info.inst_implicit   := ("[", "]")
+| _                           := ("(", ")")
+
+end binder_info
+
 namespace name
 
 /-- Find the largest prefix `n` of a `name` such that `f n ≠ none`, then replace this prefix
@@ -305,4 +318,37 @@ meta def is_axiom : declaration → bool
 | (ax _ _ _) := tt
 | _          := ff
 
+/-- Checks whether a declaration is automatically generated in the environment -/
+meta def is_auto_generated (e : environment) (d : declaration) : bool :=
+e.is_constructor d.to_name ∨
+(e.is_projection d.to_name).is_some ∨
+(e.is_constructor d.to_name.get_prefix ∧
+  d.to_name.last ∈ ["inj", "inj_eq", "sizeof_spec", "inj_arrow"]) ∨
+(e.is_inductive d.to_name.get_prefix ∧
+  d.to_name.last ∈ ["below", "binduction_on", "brec_on", "cases_on", "dcases_on", "drec_on", "drec",
+  "rec", "rec_on", "no_confusion", "no_confusion_type", "sizeof", "ibelow", "has_sizeof_inst"])
+
 end declaration
+
+/-- The type of binders containing a name, the binding info and the binding type -/
+@[derive decidable_eq]
+meta structure binder :=
+  (name : name)
+  (info : binder_info)
+  (type : expr)
+
+namespace binder
+/-- Turn a binder into a string. Uses expr.to_string for the type. -/
+protected meta def to_string (b : binder) : string :=
+let (l, r) := b.info.brackets in
+l ++ b.name.to_string ++ " : " ++ b.type.to_string ++ r
+
+open tactic
+meta instance : inhabited binder := ⟨⟨default _, default _, default _⟩⟩
+meta instance : has_to_string binder := ⟨ binder.to_string ⟩
+meta instance : has_to_format binder := ⟨ λ b, b.to_string ⟩
+meta instance : has_to_tactic_format binder :=
+⟨ λ b, let (l, r) := b.info.brackets in
+  (λ e, l ++ b.name.to_string ++ " : " ++ e ++ r) <$> pp b.type ⟩
+
+end binder

src/tactic/core.lean

@@ -105,8 +105,18 @@ meta def mk_user_fresh_name : tactic name :=
 do nm ← mk_fresh_name,
    return $ `user__ ++ nm.pop_prefix.sanitize_name ++ `user__
 
+
+/-- Checks whether n' has attribute n. -/
+meta def has_attribute' : name → name → tactic bool | n n' :=
+succeeds (has_attribute n n')
+
+/-- Checks whether the name is a simp lemma -/
 meta def is_simp_lemma : name → tactic bool :=
-succeeds ∘ tactic.has_attribute `simp
+has_attribute' `simp
+
+/-- Checks whether the name is an instance. -/
+meta def is_instance : name → tactic bool :=
+has_attribute' `instance
 
 meta def local_decls : tactic (name_map declaration) :=
 do e ← tactic.get_env,
@@ -315,6 +325,20 @@ whnf type >>= get_expl_pi_arity_aux
 meta def get_expl_arity (fn : expr) : tactic nat :=
 infer_type fn >>= get_expl_pi_arity
 
+/-- Auxilliary defintion for `get_pi_binders`. -/
+meta def get_pi_binders_aux : list binder → expr → tactic (list binder × expr)
+| es (expr.pi n bi d b) :=
+  do m ← mk_fresh_name,
+     let l := expr.local_const m n bi d,
+     let new_b := expr.instantiate_var b l,
+     get_pi_binders_aux (⟨n, bi, d⟩::es) new_b
+| es e                  := return (es, e)
+
+/-- Get the binders and target of a pi-type. Instantiates bound variables by
+  local constants. -/
+meta def get_pi_binders : expr → tactic (list binder × expr) | e :=
+do (es, e) ← get_pi_binders_aux [] e, return (es.reverse, e)
+
 /-- variation on `assert` where a (possibly incomplete)
     proof of the assertion is provided as a parameter.
 

src/tactic/sanity_check.lean

@@ -29,7 +29,7 @@ meta def fold_over_with_cond {α} (tac : declaration → tactic (option α)) :
   tactic (list (declaration × α)) :=
 do e ← get_env,
    e.mfold [] $ λ d ds,
-     if name.is_internal d.to_name then return ds else
+     if d.to_name.is_internal || d.is_auto_generated e then return ds else
      do o ← tac d,
      if h : o.is_some then return $ (d, option.get h)::ds else return ds
 
@@ -38,21 +38,21 @@ meta def fold_over_with_cond_sorted {α} (tac : declaration → tactic (option 
   tactic (list (string × list (declaration × α))) :=
 do e ← get_env,
    ds ← fold_over_with_cond tac,
-   let ds₂ := rb_lmap.of_list (ds.map (λ x, ((e.decl_olean x.1.to_name).get_or_else "", x))),
+   let ds₂ := rb_lmap.of_list (ds.map (λ x, ((e.decl_olean x.1.to_name).iget, x))),
    return $ ds₂.to_list
 
 /-- Make the output of `fold_over_with_cond` printable, in the following form:
-      #print <name> -- <elt of α> -/
+      #print <name> <open multiline comment> <elt of α> <close multiline comment> -/
 meta def print_decls {α} [has_to_format α] (ds : list (declaration × α)) : format :=
 ds.foldl
-  (λ f x, f ++ format.line ++ to_fmt "#print " ++ to_fmt x.1.to_name ++ " -- " ++ to_fmt x.2)
+  (λ f x, f ++ "\n" ++ to_fmt "#print " ++ to_fmt x.1.to_name ++ " /- " ++ to_fmt x.2 ++ " -/")
   format.nil
 
 /-- Make the output of `fold_over_with_cond_sorted` printable, with the file path + name inserted.-/
 meta def print_decls_sorted {α} [has_to_format α] (ds : list (string × list (declaration × α))) :
   format :=
 ds.foldl
-  (λ f x, f ++ format.line ++ format.line ++ to_fmt "-- " ++ to_fmt x.1 ++ print_decls x.2)
+  (λ f x, f ++ "\n" ++ "\n" ++ to_fmt "-- " ++ to_fmt x.1 ++ print_decls x.2)
   format.nil
 
 /- Print all (non-internal) declarations where tac return `some x`-/
@@ -76,83 +76,118 @@ do ml ← get_mathlib_dir,
    return $ print_decls_sorted $ f.map (λ x, ⟨x.1.popn ml.length, x.2⟩)
 
 /-- Auxilliary definition for `check_unused_arguments_aux` -/
-meta def check_unused_arguments_aux : list ℕ → ℕ → ℕ → expr → list ℕ
-:= λ l n n_max e,
+meta def check_unused_arguments_aux : list ℕ → ℕ → ℕ → expr → list ℕ | l n n_max e :=
 if n > n_max then l else
-if ¬is_lambda e then
-  if e = const `true.intro [] ∨ e = const `trivial [] then [] else l -- don't return if the target is true
-else
+if ¬is_lambda e ∧ ¬is_pi e then l else
   let b := e.binding_body in
   let l' := if b.has_var_idx 0 then l else n :: l in check_unused_arguments_aux l' (n+1) n_max b
 
 /-- Check which arguments of a declaration are not used.
   Prints a list of natural numbers corresponding to which arguments are not used (e.g.
     this outputs [1, 4] if the first and fourth arguments are unused).
-  We return [] if the body of `e` is `true.intro` or `trivial`,
-    to filter many automatically generated declarations.
-  We don't print arguments that are larger than the arity of the type of the declaration. -/
+  Checks both the type and the value of `d` for whether the argument is used
+  (in rare cases an argument is used in the type but not in the value).
+  We return [] if the declaration was automatically generated.
+  We print arguments that are larger than the arity of the type of the declaration
+  (without unfolding definitions). -/
 meta def check_unused_arguments (d : declaration) : option (list ℕ) :=
-let l := check_unused_arguments_aux [] 1 (d.type.pi_arity) d.value in
-if l = [] then none else l.reverse
-
-/-- Get all declarations with unused arguments -/
+let l := check_unused_arguments_aux [] 1 d.type.pi_arity d.value in
+if l = [] then none else
+let l2 := check_unused_arguments_aux [] 1 d.type.pi_arity d.type in
+(l.filter $ λ n, n ∈ l2).reverse
+
+/- Check for unused arguments, and print them with their position, variable name, type and whether
+  the argument is a duplicate.
+  See also `check_unused_arguments`.
+  This tactic additionally filters out all unused arguments of type `parse _` -/
+meta def prettify_unused_arguments (d : declaration) : tactic (option format) :=
+do
+  let ns := check_unused_arguments d,
+  if ¬ ns.is_some then return none else do
+  let ns := ns.iget,
+  (ds, _) ← get_pi_binders d.type,
+  let ns := ns.map (λ n, (n, (ds.nth $ n - 1).iget)),
+  let ns := ns.filter (λ x, x.2.type.get_app_fn ≠ const `interactive.parse []),
+  if ns = [] then return none else do
+  ds' ← ds.mmap pp,
+  ns ← ns.mmap (λ ⟨n, b⟩, (λ s, to_fmt "argument " ++ to_fmt n ++ ": " ++ s ++
+    (if ds.countp (λ b', b.type = b'.type) ≥ 2 then " (duplicate)" else "")) <$> pp b),
+  return $ some $ ns.to_string_aux tt
+
+/-- Print all declarations with unused arguments -/
 meta def get_all_unused_args : tactic unit :=
-print_all_decls (return ∘ check_unused_arguments) >>= trace
+print_all_decls prettify_unused_arguments >>= trace
 
-/-- Get all declarations in mathlib with unused arguments -/
+/-- Print all declarations in mathlib with unused arguments -/
 meta def get_all_unused_args_mathlib : tactic unit :=
-print_decls_mathlib (return ∘ check_unused_arguments) >>= trace
+print_decls_mathlib prettify_unused_arguments >>= trace
 
-/-- Get all declarations in current file with unused arguments. -/
+/-- Print all declarations in current file with unused arguments. -/
 meta def get_all_unused_args_current_file : tactic unit :=
-print_decls_current_file (return ∘ check_unused_arguments) >>= trace
+print_decls_current_file prettify_unused_arguments >>= trace
 
 /-- Checks whether the correct declaration constructor (definition of theorem) by comparing it
-  to its sort. This will automatically remove all instances and automatically generated
-  definitions -/
+  to its sort. Instances will not be printed -/
 meta def incorrect_def_lemma (d : declaration) : tactic (option string) :=
 do
   e ← get_env,
   expr.sort n ← infer_type d.type,
-  if d.is_constant ∨ d.is_axiom ∨ (e.is_projection d.to_name).is_some ∨
-    (d.is_definition : bool) = (n ≠ level.zero : bool) ∨
-    (d.to_name.last ∈ ["inj","inj_eq","sizeof_spec"] ∧
-      e.is_constructor d.to_name.get_prefix) ∨
-    (d.to_name.last ∈ ["dcases_on","drec_on","drec","cases_on","rec_on","binduction_on"] ∧
-      e.is_inductive d.to_name.get_prefix)
+  let is_def : Prop := d.is_definition,
+  if d.is_constant ∨ d.is_axiom ∨ is_def ↔ (n ≠ level.zero)
     then return none
-    else (option.is_some <$> try_core (has_attribute `instance d.to_name)) >>=
-    λ b, return $ if b then none
+    else is_instance d.to_name >>= λ b, return $
+    if b then none
     else if (d.is_definition : bool) then "is a def, should be a lemma/theorem"
     else "is a lemma/theorem, should be a def"
 
-/-- Get all declarations in mathlib incorrectly marked as def/lemma -/
+/-- Print all declarations in mathlib incorrectly marked as def/lemma -/
 meta def incorrect_def_lemma_mathlib : tactic unit :=
-print_decls_mathlib (return ∘ check_unused_arguments) >>= trace
+print_decls_mathlib prettify_unused_arguments >>= trace
+
+/-- Checks whether a declaration has a namespace twice consecutively in its name -/
+meta def dup_namespace (d : declaration) : tactic (option string) :=
+return $ let nm := d.to_name.components in if nm.chain' (≠) then none
+  else let s := (nm.find $ λ n, nm.count n ≥ 2).iget.to_string in
+  some $ "The namespace " ++ s ++ " is duplicated in the name"
+
+
+/-- Return the message printed by `#sanity_check`. -/
+meta def sanity_check : tactic format :=
+do
+  let s := to_fmt "/- Note: This command is still in development. -/\n\n",
+  f ← print_decls_current_file prettify_unused_arguments,
+  let s := s ++ if f.is_nil then "/- OK: No unused arguments in the current file. -/\n\n"
+  else to_fmt "/- Unused arguments in the current file: -/" ++ f ++ "\n\n",
+  f ← print_decls_current_file incorrect_def_lemma,
+  let s := s ++ if f.is_nil then "/- OK: All declarations correctly marked as def/lemma -/\n\n"
+  else to_fmt "/- Declarations incorrectly marked as def/lemma: -/" ++ f ++ "\n\n",
+  f ← print_decls_current_file dup_namespace,
+  let s := s ++ if f.is_nil then "/- OK: No declarations have a duplicate namespace -/\n\n"
+  else to_fmt "/- Declarations with a namespace duplicated: -/" ++ f ++ "\n\n",
+  return s
 
 /-- The command `#sanity_check` at the bottom of a file will warn you about some common mistakes
   in that file. -/
 @[user_command] meta def sanity_check_cmd (_ : parse $ tk "#sanity_check") : parser unit :=
-do
-  trace "/- Note: This command is still in development. -/\n",
-  f ← print_decls_current_file (return ∘ check_unused_arguments),
-  if f.is_nil then trace "/- OK: No unused arguments in the current file. -/"
-  else trace (to_fmt "/- Unused arguments in the current file: -/" ++ f ++ format.line),
-  f ← print_decls_current_file incorrect_def_lemma,
-  if f.is_nil then trace "/-OK: All declarations correctly marked as def/lemma -/"
-  else trace (to_fmt "/- Declarations incorrectly marked as def/lemma: -/" ++ f ++ format.line),
-  skip
+do s ← sanity_check, trace s
 
 /-- The command `#sanity_check_mathlib` checks all of mathlib for certain mistakes. -/
 @[user_command] meta def sanity_check_mathlib_cmd (_ : parse $ tk "#sanity_check_mathlib") :
   parser unit :=
 do
   trace "/- Note: This command is still in development. -/\n",
-  f ← print_decls_mathlib (return ∘ check_unused_arguments),
-  trace (to_fmt "/- UNUSED ARGUMENTS: -/" ++ f ++ format.line),
+  f ← print_decls_mathlib prettify_unused_arguments,
+  trace (to_fmt "/- UNUSED ARGUMENTS: -/" ++ f ++ "\n"),
   f ← print_decls_mathlib incorrect_def_lemma,
-  trace (to_fmt "/- INCORRECT DEF/LEMMA: -/" ++ f ++ format.line),
+  trace (to_fmt "/- INCORRECT DEF/LEMMA: -/" ++ f ++ "\n"),
+  f ← print_decls_mathlib dup_namespace,
+  trace (to_fmt "/- DUPLICATED NAMESPACES IN NAME: -/" ++ f ++ "\n"),
   skip
 
+@[hole_command] meta def sanity_check_hole_cmd : hole_command :=
+{ name := "Sanity Check",
+  descr := "Sanity check: Find mistakes in current file.",
+  action := λ es, do s ← sanity_check, return [(s.to_string,"")] }
+
 -- #sanity_check
 -- #sanity_check_mathlib

src/tactic/where.lean

@@ -53,12 +53,6 @@ meta def get_def_variables (n : name) : tactic (list (name × binder_info × exp
 meta def get_includes_core (flag : name) : tactic (list (name × binder_info × expr)) :=
 get_def_variables flag
 
-meta def binder_brackets : binder_info → string × string
-| binder_info.implicit        := ("{", "}")
-| binder_info.strict_implicit := ("{", "}")
-| binder_info.inst_implicit   := ("[", "]")
-| _                           := ("(", ")")
-
 meta def binder_priority : binder_info → ℕ
 | binder_info.implicit := 1
 | binder_info.strict_implicit := 2
@@ -126,7 +120,7 @@ let n := to_string n, (ns, ins) := collect_implicit_names ns in
 if n.front = '_' then (ns, n :: ins) else (n :: ns, ins)
 
 meta def format_variable : expr × binder_info × list name → tactic string
-| (e, bi, ns) := do let (l, r) := binder_brackets bi,
+| (e, bi, ns) := do let (l, r) := bi.brackets,
                     e ← pp e,
                     let (ns, ins) := collect_implicit_names ns,
                     let ns := " ".intercalate $ ns.map to_string,

test/sanity_check.lean

@@ -22,3 +22,5 @@ run_cmd do
   let e2 : list (name × _) := e.map $ λ x, ⟨x.1.to_name, x.2⟩,
   guard $ ∃(x ∈ e2), (x : name × _).1 = `foo2,
   guard $ ∃(x ∈ e2), (x : name × _).1 = `foo3
+
+-- #sanity_check_mathlib