feat(tactic/squeeze,hole): remove needless qualifications in names

src/meta/rb_map.lean

@@ -49,11 +49,11 @@ variables {m : Type → Type*} [monad m]
 open function
 
 meta def mfilter {key val} [has_lt key] [decidable_rel ((<) : key → key → Prop)]
-  (s : rb_map key val) (P : key → val → m bool) : m (rb_map.{0 0} key val) :=
+  (P : key → val → m bool) (s : rb_map key val) : m (rb_map.{0 0} key val) :=
 rb_map.of_list <$> s.to_list.mfilter (uncurry P)
 
 meta def mmap {key val val'} [has_lt key] [decidable_rel ((<) : key → key → Prop)]
-  (s : rb_map key val) (f : val → m val') : m (rb_map.{0 0} key val') :=
+  (f : val → m val') (s : rb_map key val) : m (rb_map.{0 0} key val') :=
 rb_map.of_list <$> s.to_list.mmap (λ ⟨a,b⟩, prod.mk a <$> f b)
 
 meta def scale {α β} [has_lt α] [decidable_rel ((<) : α → α → Prop)] [has_mul β] (b : β) (m : rb_map α β) : rb_map α β :=
@@ -77,14 +77,20 @@ end rb_map
 end native
 
 namespace name_set
-meta def filter (s : name_set) (P : name → bool) : name_set :=
+meta def filter (P : name → bool) (s : name_set) : name_set :=
 s.fold s (λ a m, if P a then m else m.erase a)
 
-meta def mfilter {m} [monad m] (s : name_set) (P : name → m bool) : m name_set :=
+meta def mfilter {m} [monad m] (P : name → m bool) (s : name_set) : m name_set :=
 s.fold (pure s) (λ a m,
   do x ← m,
      mcond (P a) (pure x) (pure $ x.erase a))
 
+meta def mmap {m} [monad m] (f : name → m name) (s : name_set) : m name_set :=
+s.fold (pure mk_name_set) (λ a m,
+  do x ← m,
+     b ← f a,
+     (pure $ x.insert b))
+
 meta def union (s t : name_set) : name_set :=
 s.fold t (λ a t, t.insert a)
 

src/tactic/basic.lean

@@ -121,6 +121,13 @@ 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 :=
+format.join ∘ list.intersperse x
+
+end format
+
 namespace tactic
 
 meta def eval_expr' (α : Type*) [_inst_1 : reflected α] (e : expr) : tactic α :=
@@ -641,10 +648,25 @@ instance : monad id :=
      env ← get_env,
      fs ← expanded_field_list cl,
      let fs := fs.map prod.snd,
-     let fs := list.intersperse (",\n  " : format) $ fs.map (λ fn, format!"{fn} := _"),
-     let out := format.to_string format!"{{ {format.join fs} }",
+     let fs := format.intercalate (",\n  " : format) $ fs.map (λ fn, format!"{fn} := _"),
+     let out := format.to_string format!"{{ {fs} }",
      return [(out,"")] }
 
+meta def strip_prefix' (n : name) : list string → name → tactic name
+| s name.anonymous := pure $ s.foldl (flip name.mk_string) name.anonymous
+| s (name.mk_string a p) :=
+  do let n' := s.foldl (flip name.mk_string) name.anonymous,
+     do { n'' ← tactic.resolve_constant n',
+          if n'' = n
+            then pure n'
+            else strip_prefix' (a :: s) p }
+     <|> strip_prefix' (a :: s) p
+| s (name.mk_numeral a p) := interaction_monad.failed
+
+meta def strip_prefix : name → tactic name
+| n@(name.mk_string a a_1) := strip_prefix' n [a] a_1
+| _ := interaction_monad.failed
+
 meta def is_default_local : expr → bool
 | (expr.local_const _ _ binder_info.default _) := tt
 | _ := ff
@@ -662,6 +684,7 @@ do let cl := t.get_app_fn.const_name,
                pure v' ),
           vs.mmap' $ λ v, get_local v >>= clear,
           let args := list.intersperse (" " : format) $ vs.map to_fmt,
+          f ← strip_prefix f,
           if args.empty
             then pure $ format!"| {f} := _\n"
             else pure format!"| ({f} {format.join args}) := _\n" }

src/tactic/squeeze.lean

@@ -69,7 +69,7 @@ do g ← main_goal,
    simp use_iota_eqn no_dflt hs attr_names locat cfg',
    g ← instantiate_mvars g,
    let vs := g.list_constant,
-   vs ← vs.mfilter (succeeds ∘ has_attribute `simp),
+   vs ← vs.mfilter (succeeds ∘ has_attribute `simp) >>= name_set.mmap strip_prefix,
    let use_iota_eqn := if use_iota_eqn.is_some then "!" else "",
    let attrs := if attr_names.empty then "" else string.join (list.intersperse " " (" with" :: attr_names.map to_string)),
    let loc := loc.to_string locat,
@@ -87,7 +87,7 @@ do g ← main_goal,
    simpa use_iota_eqn no_dflt hs attr_names tgt cfg',
    g ← instantiate_mvars g,
    let vs := g.list_constant,
-   vs ← vs.mfilter (succeeds ∘ has_attribute `simp),
+   vs ← vs.mfilter (succeeds ∘ has_attribute `simp) >>= name_set.mmap strip_prefix,
    let use_iota_eqn := if use_iota_eqn.is_some then "!" else "",
    let attrs := if attr_names.empty then "" else string.join (list.intersperse " " (" with" :: attr_names.map to_string)),
    let tgt' := tgt'.get_or_else "",