feat(init/meta/interactive): declare format! and sformat! macros and start putting them to use

library/data/hash_map.lean

@@ -716,7 +716,7 @@ section string
 variables [has_to_string α] [∀ a, has_to_string (β a)]
 open prod
 private def key_data_to_string (a : α) (b : β a) (first : bool) : string :=
-(if first then "" else ", ") ++ to_string a ++ " ← " ++ to_string b
+(if first then "" else ", ") ++ sformat!"{a} ← {b}"
 
 private def to_string (m : hash_map α β) : string :=
 "⟨" ++ (fst (fold m ("", tt) (λ p a b, (fst p ++ key_data_to_string a b (snd p), ff)))) ++ "⟩"

library/init/meta/converter.lean

@@ -38,7 +38,7 @@ match o₁, o₂ with
   env ← get_env,
   match env.trans_for r with
   | some trans := do pr ← mk_app trans [p₁, p₂], return $ some pr
-  | none       := fail $ "converter failed, relation '" ++ r.to_string ++ "' is not transitive"
+  | none       := fail format!"converter failed, relation '{r}' is not transitive"
   end
 end
 
@@ -120,7 +120,7 @@ private meta def mk_refl_proof (r : name) (e : expr) : tactic expr :=
 do env ← get_env,
    match (environment.refl_for env r) with
    | (some refl) := do pr ← mk_app refl [e], return pr
-   | none        := fail $ "converter failed, relation '" ++ r.to_string ++ "' is not reflexive"
+   | none        := fail format!"converter failed, relation '{r}' is not reflexive"
    end
 
 meta def to_tactic (c : conv unit) : name → expr → tactic (expr × expr) :=

library/init/meta/interactive_base.lean

@@ -132,3 +132,41 @@ meta def param_desc : expr → tactic format
   then return $ to_fmt "{ tactic }"
   else paren <$> pp e
 end interactive
+
+section macros
+open interaction_monad
+open interactive
+
+private meta def parse_format : string → string → parser pexpr
+| acc []            := pure ``(to_fmt %%(reflect acc))
+| acc ('\n'::s)     :=
+do f ← parse_format [] s,
+   pure ``(to_fmt %%(reflect acc) ++ format.line ++ %%f)
+| acc ('{'::'{'::s) := parse_format (acc ++ "{") s
+| acc ('{'::s) :=
+do (e, s) ← with_input (lean.parser.pexpr 0) s.reverse,
+   '}'::s ← pure s.reverse | fail "'}' expected",
+   f ← parse_format [] s,
+   pure ``(to_fmt %%(reflect acc) ++ to_fmt %%e ++ %%f)
+| acc (c::s) := parse_format (acc ++ [c]) s
+
+reserve prefix `format! `:100
+@[user_notation]
+meta def format_macro (_ : parse $ tk "format!") (s : string) : parser pexpr :=
+parse_format "" s.reverse
+
+private meta def parse_sformat : string → string → parser pexpr
+| acc []            := pure $ pexpr.of_expr (reflect acc)
+| acc ('{'::'{'::s) := parse_sformat (acc ++ "{") s
+| acc ('{'::s) :=
+do (e, s) ← with_input (lean.parser.pexpr 0) s.reverse,
+   '}'::s ← pure s.reverse | fail "'}' expected",
+   f ← parse_sformat [] s,
+   pure ``(to_string %%(reflect acc) ++ to_string %%e ++ %%f)
+| acc (c::s) := parse_sformat (acc ++ [c]) s
+
+reserve prefix `sformat! `:100
+@[user_notation]
+meta def sformat_macro (_ : parse $ tk "sformat!") (s : string) : parser pexpr :=
+parse_sformat "" s.reverse
+end macros

library/init/meta/match_tactic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.tactic init.function
+import init.meta.interactive_base init.function
 
 namespace tactic
 meta structure pattern :=
@@ -110,6 +110,6 @@ meta instance : has_to_tactic_format pattern :=
   uo ← pp p.uoutput,
   u ← pp p.nuvars,
   m ← pp p.nmvars,
-  return $ to_fmt "pattern.mk (" ++ t ++ ") " ++ uo ++ " " ++ mo ++ " " ++ u ++ " " ++ m ++ "" ⟩
+  return format!"pattern.mk ({t}) {uo} {mo} {u} {m}" ⟩
 
 end tactic

library/init/meta/mk_inhabited_instance.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 Helper tactic for showing that a type has decidable equality.
 -/
 prelude
+import init.meta.interactive_base
 import init.meta.contradiction_tactic init.meta.constructor_tactic
 import init.meta.injection_tactic init.meta.relation_tactics
 
@@ -41,10 +42,10 @@ do
   I      ← get_inhabited_type_name,
   env    ← get_env,
   let n  := length (constructors_of env I),
-  when (n = 0) (fail $ "mk_inhabited_instance failed, type '" ++ to_string I ++ "' does not have constructors"),
+  when (n = 0) (fail format!"mk_inhabited_instance failed, type '{I}' does not have constructors"),
   constructor,
   (try_constructors n n)
   <|>
-  (fail $ "mk_inhabited_instance failed, failed to build instance using all constructors of '" ++ to_string I ++ "'")
+  (fail format!"mk_inhabited_instance failed, failed to build instance using all constructors of '{I}'")
 
 end tactic

library/init/meta/smt/congruence_closure.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.tactic init.meta.set_get_option_tactics
+import init.meta.interactive_base init.meta.tactic init.meta.set_get_option_tactics
 
 structure cc_config :=
 /- If tt, congruence closure will treat implicit instance arguments as constants. -/
@@ -103,8 +103,7 @@ do intros, s ← cc_state.mk_using_hs_core cfg, t ← target, s ← s.internaliz
        dbg ← get_bool_option `trace.cc.failure ff,
        if dbg then do {
          ccf ← pp s,
-         msg ← return $ to_fmt "cc tactic failed, equivalence classes: " ++ format.line ++ ccf,
-         fail msg
+         fail format!"cc tactic failed, equivalence classes: \n{ccf}"
        } else do {
          fail "cc tactic failed"
        }

library/init/meta/smt/ematch.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.smt.congruence_closure
 import init.meta.attribute init.meta.simp_tactic
+import init.meta.interactive_base
 open tactic
 
 /- Heuristic instantiation lemma -/
@@ -44,7 +45,7 @@ let tac := s.fold (return format.nil)
       hpp ← h.pp,
       r   ← tac,
       if r.is_nil then return hpp
-      else return (r ++ to_fmt "," ++ format.line ++ hpp))
+      else return format!"{r},\n{hpp}")
 in do
   r ← tac,
   return $ format.cbrace (format.group r)
@@ -94,7 +95,7 @@ meta def mk_hinst_lemma_attrs_core (as_simp : bool) : list name → command
   (do type ← infer_type (expr.const n []),
       let expected := `(caching_user_attribute hinst_lemmas),
       (is_def_eq type expected
-       <|> fail ("failed to create hinst_lemma attribute '" ++ n.to_string ++ "', declaration already exists and has different type.")),
+       <|> fail format!"failed to create hinst_lemma attribute '{n}', declaration already exists and has different type."),
       mk_hinst_lemma_attrs_core ns)
 
 meta def merge_hinst_lemma_attrs (m : transparency) (as_simp : bool) : list name → hinst_lemmas → tactic hinst_lemmas

library/init/meta/smt/interactive.lean

@@ -135,7 +135,7 @@ smt_tactic.by_contradiction
 open tactic (resolve_name transparency to_expr)
 
 private meta def report_invalid_em_lemma {α : Type} (n : name) : smt_tactic α :=
-fail ("invalid ematch lemma '" ++ to_string n ++ "'")
+fail format!"invalid ematch lemma '{n}'"
 
 private meta def add_lemma_name (md : transparency) (lhs_lemma : bool) (n : name) (ref : pexpr) : smt_tactic unit :=
 do
@@ -169,7 +169,7 @@ private meta def add_eqn_lemmas_for_core (md : transparency) : list name → smt
   p ← resolve_name c,
   match p with
   | expr.const n _           := add_ematch_eqn_lemmas_for_core md n >> add_eqn_lemmas_for_core cs
-  | _                        := fail $ "'" ++ to_string c ++ "' is not a constant"
+  | _                        := fail format!"'{c}' is not a constant"
   end
 
 meta def add_eqn_lemmas_for (ids : parse ident*) : smt_tactic unit :=

library/init/meta/smt/rsimp.lean

@@ -31,7 +31,7 @@ private meta def to_hinst_lemmas (m : transparency) (ex : name_set) : list name
 meta def mk_hinst_lemma_attr_from_simp_attr (attr_decl_name attr_name : name) (simp_attr_name : name) (ex_attr_name : name) : command :=
 do let t := `(caching_user_attribute hinst_lemmas),
    let v := `({name     := attr_name,
-                 descr    := "hinst_lemma attribute derived from '" ++ to_string simp_attr_name ++ "'",
+                 descr    := sformat!"hinst_lemma attribute derived from '{simp_attr_name}'",
                  mk_cache := λ ns,
                  let aux := simp_attr_name in
                  let ex_attr := ex_attr_name in

library/init/meta/transfer.lean

@@ -48,7 +48,7 @@ meta instance has_to_tactic_format_rel_data : has_to_tactic_format rel_data :=
   R ← pp r.relation,
   α ← pp r.in_type,
   β ← pp r.out_type,
-  return $ to_fmt "(" ++ R ++ ": rel (" ++ α ++ ") (" ++ β ++ "))" ⟩
+  return format!"({R}: rel ({α}) ({β}))" ⟩
 
 private meta structure rule_data :=
 (pr      : expr)
@@ -68,7 +68,7 @@ meta instance has_to_tactic_format_rule_data : has_to_tactic_format rule_data :=
   ma ← pp r.args,
   pat ← pp r.pat.target,
   out ← pp r.out,
-  return $ to_fmt "{ ⟨" ++ pat ++ "⟩ pr: " ++ pr ++ " → " ++ out ++ ", " ++ up ++ " " ++ mp ++ " " ++ ua ++ " " ++ ma ++ " }" ⟩
+  return format!"{{ ⟨{pat}⟩ pr: {pr} → {out}, {up} {mp} {ua} {ma} }" ⟩
 
 private meta def get_lift_fun : expr → tactic (list rel_data × expr)
 | e :=
@@ -150,9 +150,9 @@ meta def compute_transfer : list rule_data → list expr → expr → tactic (ex
     -- Argument has function type
     (args, r) ← get_lift_fun (i d.relation),
     ((a_vars, b_vars), (R_vars, bnds)) ← monad.for (enum args) (λ⟨n, arg⟩, do
-      a ← mk_local_def (("a" ++ to_string n) : string) arg.in_type,
-      b ← mk_local_def (("b" ++ to_string n) : string) arg.out_type,
-      R ← mk_local_def (("R" ++ to_string n) : string) (arg.relation a b),
+      a ← mk_local_def sformat!"a{n}" arg.in_type,
+      b ← mk_local_def sformat!"b{n}" arg.out_type,
+      R ← mk_local_def sformat!"R{n}" (arg.relation a b),
       return ((a, b), (R, [a, b, R]))) >>= (return ∘ prod.map unzip unzip ∘ unzip),
     rds'      ← monad.for R_vars (analyse_rule []),
 

library/tools/debugger/util.lean

@@ -47,16 +47,16 @@ do {
   d      ← vm.get_decl fn,
   some p ← return (vm_decl.pos d) | failure,
   file   ← get_file fn,
-  return (file ++ ":" ++ p.line.to_string ++ ":" ++ p.column.to_string)
+  return sformat!"{file}:{p.line}:{p.column}"
 }
 <|>
 return "<position not available>"
 
 meta def show_fn (header : string) (fn : name) (frame : nat) : vm unit :=
 do pos ← pos_info fn,
-   vm.put_str ("[" ++ frame.to_string ++ "] " ++ header),
+   vm.put_str sformat!"[{frame}] {header}",
    if header = "" then return () else vm.put_str " ",
-   vm.put_str (fn.to_string ++ " at " ++ pos ++ "\n")
+   vm.put_str sformat!"{fn} at {pos}\n"
 
 meta def show_curr_fn (header : string) : vm unit :=
 do fn ← vm.curr_fn,
@@ -105,7 +105,7 @@ meta def show_vars_core : nat → nat → nat → vm unit
   else do
     (n, type) ← vm.stack_obj_info i,
     type_str  ← type_to_string type i,
-    vm.put_str $ "#" ++ c.to_string ++ " " ++ n.to_string ++ " : " ++ type_str ++ "\n",
+    vm.put_str sformat!"#{c} {n} : {type_str}\n",
     show_vars_core (c+1) (i+1) e
 
 meta def show_vars (frame : nat) : vm unit :=

tests/lean/user_notation.lean

@@ -10,24 +10,6 @@ meta def unquote_macro (_ : parse $ tk "unquote!") (e : parse lean.parser.pexpr)
 
 #eval unquote! ``(1 + 1)
 
-private meta def parse_format : string → string → parser pexpr
-| acc []            := pure $ pexpr.of_expr (reflect acc)
-| acc ('{'::'{'::s) := parse_format (acc ++ "{") s
-| acc ('{'::s) :=
-do (e, s) ← with_input (lean.parser.pexpr 0) s.reverse,
-   '}'::s ← pure s.reverse | fail "'}' expected",
-   f ← parse_format [] s,
-   pure ``(to_fmt %%(reflect acc) ++ to_fmt %%(e) ++ %%f)
-| acc (c::s) := parse_format (acc ++ [c]) s
-
-reserve prefix `format! `:100
-@[user_notation]
-meta def format_macro (_ : parse $ tk "format!") (s : string) : parser pexpr :=
-parse_format "" s.reverse
-
-#eval let a := "bla" in format! "({to_fmt a ++ format! \"{a}\"} {42})"
--- #eval format! "{} {}" "a" "bla" -- TODO: delayed abstractions issue
-
 reserve infix ` +⋯+ `:65
 @[user_notation]
 meta def upto_notation (e₁ : parse lean.parser.pexpr) (_ : parse $ tk "+⋯+") (n₂ : ℕ) : parser pexpr :=

tests/lean/user_notation.lean.expected.out

@@ -1,12 +1,12 @@
 2
-abc
-0 + (bit1 [nat_value_macro] + [nat_value_macro]) + (bit1 [nat_value_macro] + bit1 [nat_value_macro]) +
-                (bit1 [nat_value_macro] + bit0 (bit1 [nat_value_macro])) +
-              (bit1 [nat_value_macro] + bit1 (bit1 [nat_value_macro])) +
-            (bit1 [nat_value_macro] + bit0 (bit0 (bit1 [nat_value_macro]))) +
-          (bit1 [nat_value_macro] + bit1 (bit0 (bit1 [nat_value_macro]))) +
-        (bit1 [nat_value_macro] + bit0 (bit1 (bit1 [nat_value_macro]))) +
-      (bit1 [nat_value_macro] + bit1 (bit1 (bit1 [nat_value_macro]))) +
-    (bit1 [nat_value_macro] + bit0 (bit0 (bit0 (bit1 [nat_value_macro])))) +
-  (bit1 [nat_value_macro] + bit1 (bit0 (bit0 (bit1 [nat_value_macro])))) :
-  ℕ
+0 + (1 + 0) + (1 + 1) + (1 + 2) + (1 + 3) + (1 + 4) + (1 + 5) + (1 + 6) + (1 + 7) + (1 + 8) + (1 + 9) : ℕ
+user_notation.lean:21:0: error: invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` parameter, optionally preceded by `interactive.parse lean.parser.[pq]expr` parameter
+user_notation.lean:22:9: error: don't know how to synthesize placeholder
+context:
+e₁ : parse lean.parser.pexpr
+⊢ Sort ?
+user_notation.lean:24:0: error: invalid user-defined notation, must return type `lean.parser p`
+user_notation.lean:25:9: error: don't know how to synthesize placeholder
+context:
+e₁ : parse (tk "(")
+⊢ Sort ?