feat(command): Add #where command, dumping environment info

The command tells you your current namespace (wherever you write it),
the current `include`s, and the current `variables` which have been
used at least once.

tactic/basic.lean

@@ -13,6 +13,31 @@ meta def deinternalize_field : name → name
   if i.curr = '_' then i.next.next_to_string else s
 | n := n
 
+meta def get_nth_prefix : name → ℕ → name
+| nm 0 := nm
+| nm (n + 1) := get_nth_prefix nm.get_prefix n
+
+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.
+meta def pop_nth_prefix (nm : name) (n : ℕ) : name :=
+prod.fst $ pop_nth_prefix_aux nm n
+
+meta def pop_prefix (n : name) : name :=
+pop_nth_prefix n 1
+
+-- `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.
+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
+
 end name
 
 namespace name_set
@@ -159,13 +184,33 @@ end
 meta instance has_coe' {α} : has_coe (tactic α) (parser α) :=
 ⟨of_tactic'⟩
 
+meta def emit_command_here (str : string) : lean.parser string :=
+do (_, left) ← with_input command_like str,
+   return left
+
+-- Emit a source code string at the location being parsed.
+meta def emit_code_here : string → lean.parser unit
+| str := do left ← emit_command_here str,
+            if left.length = 0 then return ()
+            else emit_code_here left
+
 end lean.parser
 
 namespace tactic
 
 meta def eval_expr' (α : Type*) [_inst_1 : reflected α] (e : expr) : tactic α :=
 mk_app ``id [e] >>= eval_expr α
 
+-- `mk_fresh_name` returns identifiers starting with underscores,
+-- which are not legal when emitted by tactic programs. Turn the
+-- useful source of random names provided by `mk_fresh_name` into
+-- names which are usable by tactic programs.
+--
+-- The returned name has four components.
+meta def mk_user_fresh_name : tactic name :=
+do nm ← mk_fresh_name,
+   return $ `user__ ++ nm.pop_prefix.sanitize_name ++ `user__
+
 meta def is_simp_lemma : name → tactic bool :=
 succeeds ∘ tactic.has_attribute `simp
 

tactic/interactive.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro, Simon Hudon, Sebastien Gouezel, Scott Morrison
 import data.dlist data.dlist.basic data.prod category.basic
   tactic.basic tactic.rcases tactic.generalize_proofs
   tactic.split_ifs logic.basic tactic.ext tactic.tauto tactic.replacer
+  tactic.where
 
 open lean
 open lean.parser

tactic/where.lean

@@ -0,0 +1,226 @@
+import tactic.basic
+
+open lean.parser tactic
+
+namespace where
+
+meta def mk_flag (let_var : option name := none) : lean.parser (name × ℕ) :=
+do n ← mk_user_fresh_name,
+   emit_code_here $ match let_var with
+   | none   := sformat!"def {n} := ()"
+   | some v := sformat!"def {n} := let {v} := {v} in ()"
+   end,
+   nfull ← resolve_constant n,
+   return (nfull, n.components.length)
+
+meta def get_namespace_core : name × ℕ → name
+| (nfull, l) := nfull.get_nth_prefix l
+
+meta def resolve_var : list name → ℕ → expr
+| [] _ := default expr
+| (n :: rest) 0 := expr.const n []
+| (v :: rest) (n + 1) := resolve_var rest n
+
+meta def resolve_vars_aux : list name → expr → expr
+| head (expr.var n) := resolve_var head n
+| head (expr.app f a) := expr.app (resolve_vars_aux head f) (resolve_vars_aux head a)
+| head (expr.macro m e) := expr.macro m $ e.map (resolve_vars_aux head)
+| head (expr.mvar n m e) := expr.mvar n m $ resolve_vars_aux head e
+| head (expr.pi n bi t v) :=
+  expr.pi n bi (resolve_vars_aux head t) (resolve_vars_aux (n :: head) v)
+| head (expr.lam n bi t v) :=
+  expr.lam n bi (resolve_vars_aux head t) (resolve_vars_aux (n :: head) v)
+| head e := e
+
+meta def resolve_vars : expr → expr :=
+resolve_vars_aux []
+
+meta def strip_pi_binders_aux : expr → list (name × binder_info × expr)
+| (expr.pi n bi t b) := (n, bi, t) :: strip_pi_binders_aux b
+| _ := []
+
+meta def strip_pi_binders : expr → list (name × binder_info × expr) :=
+strip_pi_binders_aux ∘ resolve_vars
+
+meta def get_def_variables (n : name) : tactic (list (name × binder_info × expr)) :=
+(strip_pi_binders ∘ declaration.type) <$> get_decl n
+
+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
+| binder_info.default := 3
+| binder_info.inst_implicit := 4
+| binder_info.aux_decl := 5
+
+meta def binder_less_important (u v : binder_info) : bool :=
+(binder_priority u) < (binder_priority v)
+
+meta def is_in_namespace_nonsynthetic (ns n : name) : bool :=
+ns.is_prefix_of n ∧ ¬(ns.append `user__).is_prefix_of n
+
+meta def get_all_in_namespace (ns : name) : tactic (list name) :=
+do e ← get_env,
+   return $ e.fold [] $ λ d l,
+     if is_in_namespace_nonsynthetic ns d.to_name then d.to_name :: l else l
+
+meta def erase_duplicates {α : Type} [decidable_eq α] : list α → list α
+| [] := []
+| (x :: t) := (x :: erase_duplicates (t.filter $ λ a, a ≠ x))
+
+meta def fetch_potential_variable_names (ns : name) : tactic (list name) :=
+do l ← get_all_in_namespace ns,
+   l ← l.mmap get_def_variables,
+   return $ erase_duplicates $ l.join.map prod.fst
+
+-- Note: we don't call `list.find` and other sorting functions in order
+-- that this file can be imported in places like `data.nat.basic` without
+-- cyclic import hell.
+meta def find_var (n' : name) : list (name × binder_info × expr) → option (name × binder_info × expr)
+| [] := none
+| ((n, bi, e) :: rest) := if n = n' then some (n, bi, e) else find_var rest
+
+meta def is_variable_name (n : name) : lean.parser (option (name × binder_info × expr)) :=
+(do (f, _) ← mk_flag n,
+    l ← get_def_variables f,
+    return $ find_var n l
+) <|> return none
+
+meta def get_variables_core (ns : name) : lean.parser (list (name × binder_info × expr)) :=
+do l ← fetch_potential_variable_names ns,
+   list.filter_map id <$> l.mmap is_variable_name
+
+meta def select_for_which {α β γ : Type} (p : α → β × γ) [decidable_eq β] (b' : β) : list α → list γ × list α
+| [] := ([], [])
+| (a :: rest) :=
+  let (cs, others) := select_for_which rest, (b, c) := p a in
+  if b = b' then (c :: cs, others) else (cs, a :: others)
+
+private meta def collect_by_aux {α β γ : Type} (p : α → β × γ) [decidable_eq β] : list β → list α → list (β × list γ)
+| [] [] := []
+| [] _ := undefined_core "didn't find every key entry!"
+| (b :: rest) as := let (cs, as) := select_for_which p b as in (b, cs) :: collect_by_aux rest as
+
+meta def collect_by {α β γ : Type} (l : list α) (p : α → β × γ) [decidable_eq β] : list (β × list γ) :=
+collect_by_aux p (erase_duplicates $ l.map $ prod.fst ∘ p) l
+
+meta def inflate {α β γ : Type} : list (α × list (β × γ)) → list (α × β × γ)
+| [] := []
+| ((a, l) :: rest) := (l.map $ λ e, (a, e.1, e.2)) ++ inflate rest
+
+private meta def get_least {α : Type} (p : α → α → bool) : α → list α → list α → α × list α
+| c others [] := (c, others)
+| c others (a :: rest) :=
+  if p c a then get_least c (a :: others) rest
+  else get_least a (c :: others) rest
+
+meta def order_by {α : Type} (p : α → α → bool) : list α → list α
+| [] := []
+| (a :: rest) := let (m, others) := get_least p a [] rest in m :: order_by others
+
+meta def sort_variable_list (l : list (name × binder_info × expr)) : list (expr × binder_info × list name) :=
+let l := collect_by l $ λ v, (v.2.2, (v.1, v.2.1)) in
+let l := l.map $ λ el, (el.1, collect_by el.2 $ λ v, (v.2, v.1)) in
+(inflate l).qsort (λ v u, binder_less_important v.2.1 u.2.1)
+
+meta def collect_implicit_names : list name → list string × list string
+| [] := ([], [])
+| (n :: ns) :=
+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 ← pp e,
+                    let (ns, ins) := collect_implicit_names ns,
+                    let ns := " ".intercalate $ ns.map to_string,
+                    let ns := if ns.length = 0 then [] else [sformat!"{l}{ns} : {e}{r}"],
+                    let ins := ins.map $ λ _, sformat!"{l}{e}{r}",
+                    return $ " ".intercalate $ ns ++ ins
+
+meta def compile_variable_list (l : list (name × binder_info × expr)) : tactic string :=
+" ".intercalate <$> (sort_variable_list l).mmap format_variable
+
+meta def trace_namespace (ns : name) : lean.parser unit :=
+do let str := match ns with
+   | name.anonymous := "[root namespace]"
+   | ns := to_string ns
+   end,
+   trace format!"namespace {str}"
+
+meta def strip_namespace (ns n : name) : name :=
+n.replace_prefix ns name.anonymous
+
+meta def get_opens (ns : name) : tactic (list name) :=
+do opens ← erase_duplicates <$> open_namespaces,
+   return $ (opens.erase ns).map $ strip_namespace ns
+
+meta def trace_opens (ns : name) : tactic unit :=
+do l ← get_opens ns,
+   let str := " ".intercalate $ l.map to_string,
+   if l.empty then skip
+   else trace format!"open {str}"
+
+meta def trace_variables (ns : name) : lean.parser unit :=
+do l ← get_variables_core ns,
+   str ← compile_variable_list l,
+   if l.empty then skip
+   else trace format!"variables {str}"
+
+meta def trace_includes (f : name) : tactic unit :=
+do l ← get_includes_core f,
+   let str := " ".intercalate $ l.map $ λ n, to_string n.1,
+   if l.empty then skip
+   else trace format!"include {str}"
+
+meta def trace_nl : ℕ → tactic unit
+| 0 := skip
+| (n + 1) := trace "" >> trace_nl n
+
+meta def trace_end (ns : name) : tactic unit :=
+trace format!"end {ns}"
+
+meta def trace_where : lean.parser unit :=
+do (f, n) ← mk_flag,
+   let ns := get_namespace_core (f, n),
+   trace_namespace ns,
+   trace_nl 1,
+   trace_opens ns,
+   trace_variables ns,
+   trace_includes f,
+   trace_nl 3,
+   trace_end ns
+
+open interactive
+
+reserve prefix `#where`:max
+
+@[user_command]
+meta def where_cmd (_ : decl_meta_info) (_ : parse $ tk "#where") : lean.parser unit := trace_where
+
+end where
+
+namespace lean.parser
+
+open where
+
+meta def get_namespace : lean.parser name :=
+get_namespace_core <$> mk_flag
+
+meta def get_includes : lean.parser (list (name × binder_info × expr)) :=
+do (f, _) ← mk_flag,
+   get_includes_core f
+
+meta def get_variables : lean.parser (list (name × binder_info × expr)) :=
+do (f, _) ← mk_flag,
+   get_variables_core f
+
+end lean.parser