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

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/where.lean

@@ -0,0 +1,92 @@
+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} : unit := ()"
+   | some v := sformat!"def {n} : unit := let {v} := {v} in ()"
+   end,
+   nfull ← resolve_constant n,
+   return (nfull, n.components.length)
+
+meta def get_namespace : name × ℕ → name
+| (nfull, l) := nfull.get_nth_prefix l
+
+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_binders : expr → list (name × binder_info × expr)
+| (expr.pi n bi t b) := (n, bi, t) :: strip_binders b
+| _ := []
+
+meta def get_includes (flag : name) : tactic (list (name × binder_info × expr)) :=
+strip_binders <$> (mk_const flag >>= infer_type)
+
+meta def binder_brackets : binder_info → string × string
+| binder_info.implicit        := ("{", "}")
+| binder_info.strict_implicit := ("{", "}")
+| binder_info.inst_implicit   := ("[", "]")
+| _                           := ("(", ")")
+
+meta def format_binder : name × binder_info × expr → tactic string
+| (n, bi, e) := do let (l, r) := binder_brackets bi,
+                   e ← pp e,
+                   return sformat!"{l}{n} : {e}{r}"
+
+meta def format_variable_list (l : list (name × binder_info × expr)) : tactic string :=
+string.intercalate " " <$> l.mmap format_binder
+
+meta def trace_includes (flag : name) : lean.parser unit :=
+do l ← get_includes flag,
+   str ← format_variable_list l,
+   if l.length = 0 then skip
+   else trace format!"includes:  {str}"
+
+meta def get_all_in_namespace (ns : name) : tactic (list name) :=
+do e ← get_env,
+   return $ e.fold [] $ λ d l,
+     if ns.is_prefix_of 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 × binder_info × expr)) :=
+do l ← get_all_in_namespace ns,
+   l ← l.mmap (λ n, do
+     t ← mk_const n >>= infer_type, return $ strip_binders t),
+   return $ erase_duplicates l.join
+
+meta def is_variable_name : name × binder_info × expr → lean.parser bool
+| (n, bi, e) := (mk_flag n >> return tt) <|> return ff
+
+meta def trace_variables (ns : name) : lean.parser unit :=
+do l ← fetch_potential_variable_names ns,
+   l ← l.mfilter is_variable_name,
+   str ← format_variable_list l,
+   if l.length = 0 then skip
+   else trace format!"variables: {str}"
+
+meta def trace_where : lean.parser unit :=
+do (f, n) ← mk_flag,
+   let ns := get_namespace (f, n),
+   trace_namespace ns,
+   trace_includes f,
+   trace_variables 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