refactor(library): format concatentation as instance of has_append instead of has_add

library/init/meta/base_tactic.lean

@@ -106,7 +106,7 @@ end
 meta_definition decorate_ex (msg : format) (t : base_tactic S A) : base_tactic S A :=
 λ s, base_tactic_result.cases_on (t s)
   success
-  (λ e, !exception (λ u, msg + format.nest 2 (format.line + e u)))
+  (λ e, !exception (λ u, msg ++ format.nest 2 (format.line ++ e u)))
 
 inline meta_definition write (s' : S) : base_tactic S unit :=
 λ s, success () s'

library/init/meta/format.lean

@@ -29,8 +29,8 @@ meta_constant trace_fmt {A : Type} : format → (unit → A) → A
 meta_definition format.is_inhabited [instance] : inhabited format :=
 inhabited.mk format.space
 
-meta_definition format_has_add [instance] : has_add format :=
-has_add.mk format.compose
+meta_definition format_has_append [instance] : has_append format :=
+has_append.mk format.compose
 
 meta_definition format_has_to_string [instance] : has_to_string format :=
 has_to_string.mk (λ f, format.to_string f options.mk)
@@ -74,12 +74,12 @@ has_to_format.mk (λ c : char, format.of_string [c])
 
 meta_definition list.to_format_aux {A : Type} [has_to_format A] : bool → list A → format
 | _  []      := ""
-| tt (x::xs) := to_fmt x + list.to_format_aux ff xs
-| ff (x::xs) := "," + line + to_fmt x + list.to_format_aux ff xs
+| tt (x::xs) := to_fmt x ++ list.to_format_aux ff xs
+| ff (x::xs) := "," ++ line ++ to_fmt x ++ list.to_format_aux ff xs
 
 meta_definition list.to_format {A : Type} [has_to_format A] : list A → format
 | []      := "[]"
-| (x::xs) := "[" + group (nest 1 (list.to_format_aux tt (x::xs))) + "]"
+| (x::xs) := "[" ++ group (nest 1 (list.to_format_aux tt (x::xs))) ++ "]"
 
 meta_definition list.has_to_format [instance] {A : Type} [has_to_format A] : has_to_format (list A) :=
 has_to_format.mk list.to_format
@@ -95,23 +95,23 @@ has_to_format.mk (λ u, "star")
 meta_definition option.has_to_format [instance] {A : Type} [has_to_format A] : has_to_format (option A) :=
 has_to_format.mk (λ o, option.cases_on o
   "none"
-  (λ a, "(some " + nest 6 (to_fmt a) + ")"))
+  (λ a, "(some " ++ nest 6 (to_fmt a) ++ ")"))
 
 meta_definition sum.has_to_format [instance] {A B : Type} [has_to_format A] [has_to_format B] : has_to_format (sum A B) :=
 has_to_format.mk (λ s, sum.cases_on s
-  (λ a, "(inl " + nest 5 (to_fmt a) + ")")
-  (λ b, "(inr " + nest 5 (to_fmt b) + ")"))
+  (λ a, "(inl " ++ nest 5 (to_fmt a) ++ ")")
+  (λ b, "(inr " ++ nest 5 (to_fmt b) ++ ")"))
 
 open prod
 
 meta_definition prod.has_to_format [instance] {A B : Type} [has_to_format A] [has_to_format B] : has_to_format (prod A B) :=
-has_to_format.mk (λ p, group (nest 1 ("(" + to_fmt (pr1 p) + "," + line + to_fmt (pr2 p) + ")")))
+has_to_format.mk (λ p, group (nest 1 ("(" ++ to_fmt (pr1 p) ++ "," ++ line ++ to_fmt (pr2 p) ++ ")")))
 
 open sigma
 
 meta_definition sigma.has_to_format [instance] {A : Type} {B : A → Type} [has_to_format A] [s : ∀ x, has_to_format (B x)]
                                           : has_to_format (sigma B) :=
-has_to_format.mk (λ p, group (nest 1 ("⟨"  + to_fmt (pr1 p) + "," + line + to_fmt (pr2 p) + "⟩")))
+has_to_format.mk (λ p, group (nest 1 ("⟨"  ++ to_fmt (pr1 p) ++ "," ++ line ++ to_fmt (pr2 p) ++ "⟩")))
 
 open subtype
 
@@ -119,7 +119,7 @@ meta_definition subtype.has_to_format [instance] {A : Type} {P : A → Prop} [ha
 has_to_format.mk (λ s, to_fmt (elt_of s))
 
 meta_definition format.bracket : string → string → format → format
-| o c f := to_fmt o + nest (length o) f + to_fmt c
+| o c f := to_fmt o ++ nest (length o) f ++ to_fmt c
 
 meta_definition format.paren (f : format) : format :=
 format.bracket "(" ")" f
@@ -132,4 +132,4 @@ format.bracket "[" "]" f
 
 meta_definition format.dcbrace (f : format) : format :=
 -- TODO(Leo): backet uses length, but ⦃ is unicode, we need a function that computes the utf8 size of a string
-to_fmt "⦃" + nest 1 f + to_fmt "⦄"
+to_fmt "⦃" ++ nest 1 f ++ to_fmt "⦄"

library/init/meta/fun_info.lean

@@ -41,25 +41,25 @@ structure param_info :=
 open format list decidable
 
 private meta_definition ppfield {A : Type} [has_to_format A] (fname : string) (v : A) : format :=
-group $ fname + space + ":=" + space + nest (length fname + 4) (to_fmt v)
+group $ fname ++ space ++ ":=" ++ space ++ nest (length fname + 4) (to_fmt v)
 
 private meta_definition concat_fields (f₁ f₂ : format) : format :=
 if       is_nil f₁ = tt then f₂
 else if  is_nil f₂ = tt then f₁
-else f₁ + "," + line + f₂
+else f₁ ++ "," ++ line ++ f₂
 
-local infix `++`:65 := concat_fields
+local infix `+++`:65 := concat_fields
 
 meta_definition param_info.to_format : param_info → format
 | (param_info.mk s i ii p s d ds) :=
 group ∘ cbrace $
-  when s "specialized" ++
-  when i  "implicit" ++
-  when ii "inst_implicit" ++
-  when p  "prop" ++
-  when s  "subsingleton" ++
-  when d  "has_fwd_deps" ++
-  when (to_bool (length ds > 0)) ("back_deps := " + to_fmt ds)
+  when s "specialized" +++
+  when i  "implicit" +++
+  when ii "inst_implicit" +++
+  when p  "prop" +++
+  when s  "subsingleton" +++
+  when d  "has_fwd_deps" +++
+  when (to_bool (length ds > 0)) ("back_deps := " ++ to_fmt ds)
 
 meta_definition param_info.has_to_format [instance] : has_to_format param_info :=
 has_to_format.mk param_info.to_format

library/init/meta/rb_map.lean

@@ -50,11 +50,11 @@ section
 open format
 variables {key : Type} {data : Type} [has_to_format key] [has_to_format data]
 private meta_definition format_key_data (k : key) (d : data) (first : bool) : format :=
-(if first = tt then to_fmt "" else to_fmt "," + line) + to_fmt k + space + "←" + space + to_fmt d
+(if first = tt then to_fmt "" else to_fmt "," ++ line) ++ to_fmt k ++ space ++ "←" ++ space ++ to_fmt d
 
 meta_definition rb_map_has_to_format [instance] : has_to_format (rb_map key data) :=
 has_to_format.mk (λ m,
-  group ("⟨" + nest 1 (pr₁ (fold m (to_fmt "", tt) (λ k d p, (pr₁ p + format_key_data k d (pr₂ p), ff)))) + "⟩"))
+  group ("⟨" ++ nest 1 (pr₁ (fold m (to_fmt "", tt) (λ k d p, (pr₁ p ++ format_key_data k d (pr₂ p), ff)))) ++ "⟩"))
 end
 
 section

tests/lean/run/meta_env1.lean

@@ -43,4 +43,4 @@ vm_eval do
    exceptional.success (declaration.type d₁, declaration.type d₂,
                         environment.is_recursor e₂ ("Two" <.> "rec"),
                         environment.constructors_of e₂ "Two",
-                        environment.fold e₂ (to_format "") (λ d r, r + format.line + to_fmt (declaration.to_name d)))
+                        environment.fold e₂ (to_format "") (λ d r, r ++ format.line ++ to_fmt (declaration.to_name d)))

tests/lean/run/meta_tac6.lean

@@ -14,7 +14,7 @@ by do
       do t ← infer_type e,
          fmt₁ ← pp e,
          fmt₂ ← pp t,
-         trace $ fmt₁ + to_fmt " : " + fmt₂),
+         trace $ fmt₁ ++ to_fmt " : " ++ fmt₂),
     trace "----------",
     trace $ "num: " ++ to_string n,
     trace_state,