feat(tactic/sanity_check): add #sanity_check command (#1318)

* create a file sanity_check

Currently it contains a tactic that detects unused arguments in declarations
In the future I want to add other cleaning tactics

* fix last tactic

* update comment

* checkpoint

* checkpoint

* rewrite sanity_check

* update sanity_check

* move results to appropriate files

* move some declarations

Some declarations in tactic.core made more sense in meta.expr
tactic.core now imports string.defs (which adds very little)
add documentation

* add entry to docs/tactic.md

* fix errors

* some extra documentation

* add test

* add doc to meta.expr

Author: fpvandoorn

docs/tactics.md

@@ -1053,3 +1053,9 @@ localized "attribute [simp] le_refl" in le
 ### rotate
 
 `rotate` moves the first goal to the back. `rotate n` will do this `n` times.
+
+### sanity_check
+
+The `#sanity_check` command checks for common mistakes in the current file or in all of mathlib, respectively.
+
+Currently this will check for unused arguments in declarations and whether a declaration is incorrectly marked as a def/lemma.

src/data/string/defs.lean

@@ -11,10 +11,15 @@ list.as_string ∘ f ∘ string.to_list
 def split_on (c : char) (s : string) : list string :=
 (s.to_list.split_on c).map list.as_string
 
+/-- Tests whether the first string is a prefix of the second string -/
 def is_prefix_of (x y : string) : bool :=
 x.to_list.is_prefix_of y.to_list
 
 def is_suffix_of (x y : string) : bool :=
 x.to_list.is_suffix_of y.to_list
 
+/-- Removes the first `n` elements from the string `s` -/
+def popn (s : string) (n : nat) : string :=
+(s.mk_iterator.nextn n).next_to_string
+
 end string

src/meta/expr.lean

@@ -2,58 +2,100 @@
 Copyright (c) 2019 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lewis
+-/
+
+/-!
+# Additional operations on expr and related types
+
+ This file defines basic operations on the types expr, name, declaration, level, environment.
 
-Additional non-tactic operations on expr and related types
+ This file is mostly for non-tactics. Tactics should generally be placed in `tactic.core`.
+
+ ## Tags
+ expr, name, declaration, level, environment, meta, metaprogramming, tactic
 -/
 
 namespace name
-
+/-- If `nm` is a simple name (having only one string component) starting with `_`, then `deinternalize_field nm` removes the underscore. Otherwise, it does nothing. -/
 meta def deinternalize_field : name → name
-| (name.mk_string s name.anonymous) :=
+| (mk_string s name.anonymous) :=
   let i := s.mk_iterator in
   if i.curr = '_' then i.next.next_to_string else s
 | n := n
 
+/-- `get_nth_prefix nm n` removes the last `n` components from `nm` -/
 meta def get_nth_prefix : name → ℕ → name
 | nm 0 := nm
 | nm (n + 1) := get_nth_prefix nm.get_prefix n
 
+/-- Auxilliary definition for `pop_nth_prefix` -/
 private meta def pop_nth_prefix_aux : name → ℕ → name × ℕ
 | anonymous n := (anonymous, 1)
 | nm n := let (pfx, height) := pop_nth_prefix_aux nm.get_prefix n in
           if height ≤ n then (anonymous, height + 1)
           else (nm.update_prefix pfx, height + 1)
 
--- Pops the top `n` prefixes from the given name.
+/-- Pops the top `n` prefixes from the given name. -/
 meta def pop_nth_prefix (nm : name) (n : ℕ) : name :=
 prod.fst $ pop_nth_prefix_aux nm n
 
+/-- Pop the prefix of a name -/
 meta def pop_prefix (n : name) : name :=
 pop_nth_prefix n 1
 
+/-- Auxilliary definition for `from_components` -/
 private def from_components_aux : name → list string → name
 | n [] := n
 | n (s :: rest) := from_components_aux (name.mk_string s n) rest
 
+/-- Build a name from components. For example `from_components ["foo","bar"]` becomes
+  ``` `foo.bar``` -/
 def from_components : list string → name :=
 from_components_aux name.anonymous
 
--- `name`s can contain numeral pieces, which are not legal names
--- when typed/passed directly to the parser. We turn an arbitrary
--- name into a legal identifier name.
+/-- `name`s can contain numeral pieces, which are not legal names
+  when typed/passed directly to the parser. We turn an arbitrary
+  name into a legal identifier name by turning the numbers to strings. -/
 meta def sanitize_name : name → name
 | name.anonymous := name.anonymous
 | (name.mk_string s p) := name.mk_string s $ sanitize_name p
 | (name.mk_numeral s p) := name.mk_string sformat!"n{s}" $ sanitize_name p
 
+/-- Append a string to the last component of a name -/
 def append_suffix : name → string → name
 | (mk_string s n) s' := mk_string (s ++ s') n
 | n _ := n
 
+/-- The first component of a name, turning a number to a string -/
+meta def head : name → string
+| (mk_string s anonymous) := s
+| (mk_string s p)         := head p
+| (mk_numeral n p)        := head p
+| anonymous               := "[anonymous]"
+
+/-- Tests whether the first component of a name is `"_private"` -/
+meta def is_private (n : name) : bool :=
+n.head = "_private"
+
+/-- Get the last component of a name, and convert it to a string. -/
+meta def last : name → string
+| (mk_string s _)  := s
+| (mk_numeral n _) := repr n
+| anonymous        := "[anonymous]"
+
+/-- Returns the number of characters used to print all the string components of a name,
+  including periods between name segments. Ignores numerical parts of a name. -/
+meta def length : name → ℕ
+| (mk_string s anonymous) := s.length
+| (mk_string s p)         := s.length + 1 + p.length
+| (mk_numeral n p)        := p.length
+| anonymous               := "[anonymous]".length
+
 end name
 
 namespace level
 
+/-- Tests whether a universe level is non-zero for all assignments of its variables -/
 meta def nonzero : level → bool
 | (succ _) := tt
 | (max l₁ l₂) := l₁.nonzero || l₂.nonzero
@@ -65,48 +107,56 @@ end level
 namespace expr
 open tactic
 
+/-- Turns an expression into a positive natural number, assuming it is only built up from
+  `has_one.one`, `bit0` and `bit1`. -/
 protected meta def to_pos_nat : expr → option ℕ
 | `(has_one.one _) := some 1
 | `(bit0 %%e) := bit0 <$> e.to_pos_nat
 | `(bit1 %%e) := bit1 <$> e.to_pos_nat
 | _           := none
 
+/-- Turns an expression into a natural number, assuming it is only built up from
+  `has_one.one`, `bit0`, `bit1` and `has_zero.zero`. -/
 protected meta def to_nat : expr → option ℕ
 | `(has_zero.zero _) := some 0
 | e                  := e.to_pos_nat
 
+/-- Turns an expression into a integer, assuming it is only built up from
+  `has_one.one`, `bit0`, `bit1`, `has_zero.zero` and a optionally a single `has_neg.neg` as head. -/
 protected meta def to_int : expr → option ℤ
 | `(has_neg.neg %%e) := do n ← e.to_nat, some (-n)
 | e                  := coe <$> e.to_nat
 
-meta def is_meta_var : expr → bool
+/-- Tests whether an expression is a meta-variable. -/
+meta def is_mvar : expr → bool
 | (mvar _ _ _) := tt
-| e            := ff
+| _            := ff
 
+/-- Tests whether an expression is a sort. -/
 meta def is_sort : expr → bool
 | (sort _) := tt
 | e         := ff
 
+/-- Returns a list of all local constants in an expression (without duplicates). -/
 meta def list_local_consts (e : expr) : list expr :=
 e.fold [] (λ e' _ es, if e'.is_local_constant then insert e' es else es)
 
+/-- Returns a name_set of all constants in an expression. -/
 meta def list_constant (e : expr) : name_set :=
 e.fold mk_name_set (λ e' _ es, if e'.is_constant then es.insert e'.const_name else es)
 
+/-- Returns a list of all meta-variables in an expression (without duplicates). -/
 meta def list_meta_vars (e : expr) : list expr :=
-e.fold [] (λ e' _ es, if e'.is_meta_var then insert e' es else es)
+e.fold [] (λ e' _ es, if e'.is_mvar then insert e' es else es)
 
+/-- Returns a name_set of all constants in an expression starting with a certain prefix. -/
 meta def list_names_with_prefix (pre : name) (e : expr) : name_set :=
 e.fold mk_name_set $ λ e' _ l,
   match e' with
   | expr.const n _ := if n.get_prefix = pre then l.insert n else l
   | _ := l
   end
 
-meta def is_mvar : expr → bool
-| (mvar _ _ _) := tt
-| _            := ff
-
 /--
  is_num_eq n1 n2 returns true if n1 and n2 are both numerals with the same numeral structure,
  ignoring differences in type and type class arguments.
@@ -120,35 +170,57 @@ meta def is_num_eq : expr → expr → bool
 | `(%%a/%%a') `(%%b/%%b') :=  a.is_num_eq b
 | _ _ := ff
 
+/-- Simplifies the expression `t` with the specified options.
+  The result is `(new_e, pr)` with the new expression `new_e` and a proof
+  `pr : e = new_e`. -/
 meta def simp (t : expr)
   (cfg : simp_config := {}) (discharger : tactic unit := failed)
   (no_defaults := ff) (attr_names : list name := []) (hs : list simp_arg_type := []) :
   tactic (expr × expr) :=
 do (s, to_unfold) ← mk_simp_set no_defaults attr_names hs,
    simplify s to_unfold t cfg `eq discharger
 
+/-- Definitionally simplifies the expression `t` with the specified options.
+  The result is the simplified expression. -/
 meta def dsimp (t : expr)
   (cfg : dsimp_config := {})
   (no_defaults := ff) (attr_names : list name := []) (hs : list simp_arg_type := []) :
   tactic expr :=
 do (s, to_unfold) ← mk_simp_set no_defaults attr_names hs,
    s.dsimplify to_unfold t cfg
 
-end expr
+/-- Auxilliary definition for `expr.pi_arity` -/
+meta def pi_arity_aux : ℕ → expr → ℕ
+| n (pi _ _ _ b) := pi_arity_aux (n + 1) b
+| n e            := n
+
+/-- The arity of a pi-type. Does not perform any reduction of the expression.
+  In one application this was ~30 times quicker than `tactic.get_pi_arity`. -/
+meta def pi_arity : expr → ℕ :=
+pi_arity_aux 0
 
+end expr
 
 namespace environment
 
+/-- Tests whether a name is declared in the current file. Fixes an error in `in_current_file`
+  which returns `tt` for the four names `quot, quot.mk, quot.lift, quot.ind` -/
 meta def in_current_file' (env : environment) (n : name) : bool :=
 env.in_current_file n && (n ∉ [``quot, ``quot.mk, ``quot.lift, ``quot.ind])
 
+/-- Tests whether `n` is an inductive type with one constructor without indices.
+  If so, returns the number of paramaters and the name of the constructor.
+  Otherwise, returns `none`. -/
 meta def is_structure_like (env : environment) (n : name) : option (nat × name) :=
 do guardb (env.is_inductive n),
   d ← (env.get n).to_option,
   [intro] ← pure (env.constructors_of n) | none,
   guard (env.inductive_num_indices n = 0),
   some (env.inductive_num_params n, intro)
 
+/-- Tests whether `n` is a structure.
+  It will first test whether `n` is structure-like and then test that the first projection is
+  defined in the environment and is a projection. -/
 meta def is_structure (env : environment) (n : name) : bool :=
 option.is_some $ do
   (nparams, intro) ← env.is_structure_like n,
@@ -158,4 +230,57 @@ option.is_some $ do
     (some di.type) | none,
   env.is_projection (n ++ x.deinternalize_field)
 
+/-- For all declarations `d` where `f d = some x` this adds `x` to the returned list.  -/
+meta def decl_filter_map {α : Type} (e : environment) (f : declaration → option α) : list α :=
+  e.fold [] $ λ d l, match f d with
+                     | some r := r :: l
+                     | none := l
+                     end
+
+/-- Maps `f` to all declarations in the environment. -/
+meta def decl_map {α : Type} (e : environment) (f : declaration → α) : list α :=
+  e.decl_filter_map $ λ d, some (f d)
+
+/-- Lists all declarations in the environment -/
+meta def get_decls (e : environment) : list declaration :=
+  e.decl_map id
+
+/-- Lists all trusted (non-meta) declarations in the environment -/
+meta def get_trusted_decls (e : environment) : list declaration :=
+  e.decl_filter_map (λ d, if d.is_trusted then some d else none)
+
+/-- Lists the name of all declarations in the environment -/
+meta def get_decl_names (e : environment) : list name :=
+  e.decl_map declaration.to_name
+
+/-- Fold a monad over all declarations in the environment. -/
+meta def mfold {α : Type} {m : Type → Type} [monad m] (e : environment) (x : α)
+  (fn : declaration → α → m α) : m α :=
+e.fold (return x) (λ d t, t >>= fn d)
+
 end environment
+
+namespace declaration
+
+open tactic
+/-- Checks whether the declaration is declared in the current file.
+  This is a simple wrapper around `environment.in_current_file'` -/
+meta def in_current_file (d : declaration) : tactic bool :=
+do e ← get_env, return $ e.in_current_file' d.to_name
+
+/-- Checks whether a declaration is a theorem -/
+meta def is_theorem : declaration → bool
+| (thm _ _ _ _) := tt
+| _             := ff
+
+/-- Checks whether a declaration is a constant -/
+meta def is_constant : declaration → bool
+| (cnst _ _ _ _) := tt
+| _              := ff
+
+/-- Checks whether a declaration is a axiom -/
+meta def is_axiom : declaration → bool
+| (ax _ _ _) := tt
+| _          := ff
+
+end declaration

src/tactic/core.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek
 -/
-import data.dlist.basic category.basic meta.expr meta.rb_map tactic.cache
+import data.dlist.basic category.basic meta.expr meta.rb_map data.string.defs
 
 namespace expr
 open tactic
@@ -83,50 +83,6 @@ meta def emit_code_here : string → lean.parser unit
 
 end lean.parser
 
-namespace name
-
-meta def head : name → string
-| (mk_string s anonymous) := s
-| (mk_string s p)         := head p
-| (mk_numeral n p)        := head p
-| anonymous               := "[anonymous]"
-
-meta def is_private (n : name) : bool :=
-n.head = "_private"
-
-meta def last : name → string
-| (mk_string s _)  := s
-| (mk_numeral n _) := repr n
-| anonymous        := "[anonymous]"
-
-meta def length : name → ℕ
-| (mk_string s anonymous) := s.length
-| (mk_string s p)         := s.length + 1 + p.length
-| (mk_numeral n p)        := p.length
-| anonymous               := "[anonymous]".length
-
-end name
-
-namespace environment
-meta def decl_filter_map {α : Type} (e : environment) (f : declaration → option α) : list α :=
-  e.fold [] $ λ d l, match f d with
-                     | some r := r :: l
-                     | none := l
-                     end
-
-meta def decl_map {α : Type} (e : environment) (f : declaration → α) : list α :=
-  e.decl_filter_map $ λ d, some (f d)
-
-meta def get_decls (e : environment) : list declaration :=
-  e.decl_map id
-
-meta def get_trusted_decls (e : environment) : list declaration :=
-  e.decl_filter_map (λ d, if d.is_trusted then some d else none)
-
-meta def get_decl_names (e : environment) : list name :=
-  e.decl_map declaration.to_name
-end environment
-
 namespace format
 
 meta def intercalate (x : format) : list format → format :=
@@ -1153,5 +1109,24 @@ meta def trace_macro (_ : parse $ tk "trace!") (s : string) : parser pexpr :=
 do e ← pformat_macro () s,
    pure ``((%%e : pformat) >>= trace)
 
+/-- A hackish way to get the `src` directory of mathlib. -/
+meta def get_mathlib_dir : tactic string :=
+do e ← get_env,
+  s ← e.decl_olean `tactic.reset_instance_cache,
+  return $ s.popn_back 17
+
+/-- Checks whether `ml` is a prefix of the file where `n` is declared.
+  If you want to run `is_in_mathlib` many times, you should use this tactic instead,
+  since it is expensive to execute get_mathlib_dir many times. -/
+meta def is_in_mathlib_aux (ml : string) (n : name) : tactic bool :=
+do e ← get_env, return $ ml.is_prefix_of $ (e.decl_olean n).get_or_else ""
+
+/-- Checks whether a declaration with the given name is declared in mathlib.
+  If you want to run this tactic many times, you should use `is_in_mathlib_aux` instead,
+  since it is expensive to execute get_mathlib_dir many times. -/
+meta def is_in_mathlib (n : name) : tactic bool :=
+do ml ← get_mathlib_dir, is_in_mathlib_aux ml n
+
+
 end tactic
 open tactic