From 9aa6ac62ecb1c0b88f4a6315bec2ce734dfeff7c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jun 2016 07:58:17 +0100 Subject: [PATCH] refactor(library): add has_append type class, string concatenation is now an instance of has_append instead of has_add --- library/data/list/perm.lean | 2 +- library/init/list.lean | 5 +- library/init/meta/base_tactic.lean | 2 +- library/init/meta/exceptional.lean | 2 +- library/init/meta/name.lean | 4 +- library/init/meta/rb_map.lean | 4 +- library/init/meta/relation_tactics.lean | 2 +- library/init/reserved_notation.lean | 51 ++++++++++--------- library/init/string.lean | 4 +- library/init/to_string.lean | 22 ++++---- .../lean/local_notation_bug.lean.expected.out | 2 +- tests/lean/run/arity1.lean | 2 +- tests/lean/run/eq15.lean | 12 ++--- tests/lean/run/eq16.lean | 12 ++--- tests/lean/run/eq6.lean | 12 ++--- tests/lean/run/meta_tac6.lean | 4 +- tests/lean/sec_notation2.lean | 6 +-- tests/lean/sec_notation2.lean.expected.out | 2 +- tests/lean/str1.lean.expected.out | 4 +- tests/lean/struct_class.lean.expected.out | 2 + 20 files changed, 81 insertions(+), 75 deletions(-) diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index d3fc973ca4..15774c677b 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -97,7 +97,7 @@ list.induction_on l (λ p, p) (λ x xs r p, skip x (r p)) -theorem perm_app [congr] {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (l₁++t₁) ~ (l₂++t₂) := +theorem perm_app {l₁ l₂ t₁ t₂ : list A} : l₁ ~ l₂ → t₁ ~ t₂ → (l₁++t₁) ~ (l₂++t₂) := assume p₁ p₂, trans (perm_app_left t₁ p₁) (perm_app_right l₂ p₂) theorem perm_app_cons (a : A) {h₁ h₂ t₁ t₂ : list A} : h₁ ~ h₂ → t₁ ~ t₂ → (h₁ ++ (a::t₁)) ~ (h₂ ++ (a::t₂)) := diff --git a/library/init/list.lean b/library/init/list.lean index 9cd8a9aecd..d779451007 100644 --- a/library/init/list.lean +++ b/library/init/list.lean @@ -36,8 +36,6 @@ definition append : list A → list A → list A | [] l := l | (h :: s) t := h :: (append s t) -notation l₁ ++ l₂ := append l₁ l₂ - definition length : list A → nat | [] := 0 | (a :: l) := length l + 1 @@ -54,3 +52,6 @@ definition tail : list A → list A | (a :: l) := l end list + +definition list_has_append [instance] {A : Type} : has_append (list A) := +has_append.mk list.append diff --git a/library/init/meta/base_tactic.lean b/library/init/meta/base_tactic.lean index 3fad7ab029..715e1aa408 100644 --- a/library/init/meta/base_tactic.lean +++ b/library/init/meta/base_tactic.lean @@ -22,7 +22,7 @@ variables [has_to_string A] protected meta_definition base_tactic_result.to_string : base_tactic_result S A → string | (success a s) := to_string a -| (exception A e s) := "Exception: " + to_string (e options.mk) +| (exception A e s) := "Exception: " ++ to_string (e options.mk) protected meta_definition base_tactic_result.has_to_string [instance] : has_to_string (base_tactic_result S A) := has_to_string.mk base_tactic_result.to_string diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean index 9b4ef8e136..046b62849a 100644 --- a/library/init/meta/exceptional.lean +++ b/library/init/meta/exceptional.lean @@ -20,7 +20,7 @@ variables [has_to_string A] protected meta_definition exceptional.to_string : exceptional A → string | (success a) := to_string a -| (exception A e) := "Exception: " + to_string (e options.mk) +| (exception A e) := "Exception: " ++ to_string (e options.mk) protected meta_definition exceptional.has_to_string [instance] : has_to_string (exceptional A) := has_to_string.mk exceptional.to_string diff --git a/library/init/meta/name.lean b/library/init/meta/name.lean index 84bf485645..48f2f80f78 100644 --- a/library/init/meta/name.lean +++ b/library/init/meta/name.lean @@ -37,8 +37,8 @@ definition name.to_string : name → string | anonymous := "[anonymous]" | (mk_string s anonymous) := s | (mk_numeral v anonymous) := to_string v -| (mk_string s n) := name.to_string n + "." + s -| (mk_numeral v n) := name.to_string n + "." + to_string v +| (mk_string s n) := name.to_string n ++ "." ++ s +| (mk_numeral v n) := name.to_string n ++ "." ++ to_string v definition name.has_to_string [instance] : has_to_string name := has_to_string.mk name.to_string diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean index 42fe6a7ba3..d0f0df0637 100644 --- a/library/init/meta/rb_map.lean +++ b/library/init/meta/rb_map.lean @@ -60,9 +60,9 @@ end section variables {key : Type} {data : Type} [has_to_string key] [has_to_string data] private meta_definition key_data_to_string (k : key) (d : data) (first : bool) : string := -(if first = tt then "" else ", ") + to_string k + " ← " + to_string d +(if first = tt then "" else ", ") ++ to_string k ++ " ← " ++ to_string d meta_definition rb_map_has_to_string [instance] : has_to_string (rb_map key data) := has_to_string.mk (λ m, - "⟨" + (pr₁ (fold m ("", tt) (λ k d p, (pr₁ p + key_data_to_string k d (pr₂ p), ff)))) + "⟩") + "⟨" ++ (pr₁ (fold m ("", tt) (λ k d p, (pr₁ p ++ key_data_to_string k d (pr₂ p), ff)))) ++ "⟩") end diff --git a/library/init/meta/relation_tactics.lean b/library/init/meta/relation_tactics.lean index 5205c74037..061e171fc9 100644 --- a/library/init/meta/relation_tactics.lean +++ b/library/init/meta/relation_tactics.lean @@ -15,7 +15,7 @@ do tgt ← target, r ← return $ get_app_fn tgt, match op_for env (const_name r) with | some refl := mk_const refl >>= apply - | none := fail (tac_name + " tactic failed, target is not a reflexive relation application") + | none := fail (tac_name ++ " tactic failed, target is not a reflexive relation application") end meta_definition reflexivity : tactic unit := diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 1ab4ab06b3..db739ae6bb 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -9,31 +9,33 @@ import init.datatypes notation `assume` binders `,` r:(scoped f, f) := r notation `take` binders `,` r:(scoped f, f) := r -structure has_zero [class] (A : Type) := (zero : A) -structure has_one [class] (A : Type) := (one : A) -structure has_add [class] (A : Type) := (add : A → A → A) -structure has_mul [class] (A : Type) := (mul : A → A → A) -structure has_inv [class] (A : Type) := (inv : A → A) -structure has_neg [class] (A : Type) := (neg : A → A) -structure has_sub [class] (A : Type) := (sub : A → A → A) -structure has_div [class] (A : Type) := (div : A → A → A) -structure has_dvd [class] (A : Type) := (dvd : A → A → Prop) -structure has_mod [class] (A : Type) := (mod : A → A → A) -structure has_le [class] (A : Type) := (le : A → A → Prop) -structure has_lt [class] (A : Type) := (lt : A → A → Prop) +structure has_zero [class] (A : Type) := (zero : A) +structure has_one [class] (A : Type) := (one : A) +structure has_add [class] (A : Type) := (add : A → A → A) +structure has_mul [class] (A : Type) := (mul : A → A → A) +structure has_inv [class] (A : Type) := (inv : A → A) +structure has_neg [class] (A : Type) := (neg : A → A) +structure has_sub [class] (A : Type) := (sub : A → A → A) +structure has_div [class] (A : Type) := (div : A → A → A) +structure has_dvd [class] (A : Type) := (dvd : A → A → Prop) +structure has_mod [class] (A : Type) := (mod : A → A → A) +structure has_le [class] (A : Type) := (le : A → A → Prop) +structure has_lt [class] (A : Type) := (lt : A → A → Prop) +structure has_append [class] (A : Type) := (append : A → A → A) -definition zero {A : Type} [s : has_zero A] : A := has_zero.zero A -definition one {A : Type} [s : has_one A] : A := has_one.one A -definition add {A : Type} [s : has_add A] : A → A → A := has_add.add -definition mul {A : Type} [s : has_mul A] : A → A → A := has_mul.mul -definition sub {A : Type} [s : has_sub A] : A → A → A := has_sub.sub -definition div {A : Type} [s : has_div A] : A → A → A := has_div.div -definition dvd {A : Type} [s : has_dvd A] : A → A → Prop := has_dvd.dvd -definition mod {A : Type} [s : has_mod A] : A → A → A := has_mod.mod -definition neg {A : Type} [s : has_neg A] : A → A := has_neg.neg -definition inv {A : Type} [s : has_inv A] : A → A := has_inv.inv -definition le {A : Type} [s : has_le A] : A → A → Prop := has_le.le -definition lt {A : Type} [s : has_lt A] : A → A → Prop := has_lt.lt +definition zero {A : Type} [has_zero A] : A := has_zero.zero A +definition one {A : Type} [has_one A] : A := has_one.one A +definition add {A : Type} [has_add A] : A → A → A := has_add.add +definition mul {A : Type} [has_mul A] : A → A → A := has_mul.mul +definition sub {A : Type} [has_sub A] : A → A → A := has_sub.sub +definition div {A : Type} [has_div A] : A → A → A := has_div.div +definition dvd {A : Type} [has_dvd A] : A → A → Prop := has_dvd.dvd +definition mod {A : Type} [has_mod A] : A → A → A := has_mod.mod +definition neg {A : Type} [has_neg A] : A → A := has_neg.neg +definition inv {A : Type} [has_inv A] : A → A := has_inv.inv +definition le {A : Type} [has_le A] : A → A → Prop := has_le.le +definition lt {A : Type} [has_lt A] : A → A → Prop := has_lt.lt +definition append {A : Type} [has_append A] : A → A → A := has_append.append definition ge [reducible] {A : Type} [s : has_le A] (a b : A) : Prop := le b a definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Prop := lt b a @@ -211,6 +213,7 @@ infix ≤ := le infix ≥ := ge infix < := lt infix > := gt +infix ++ := append notation [parsing_only] x ` +[`:65 A:0 `] `:0 y:65 := @add A _ x y notation [parsing_only] x ` -[`:65 A:0 `] `:0 y:65 := @sub A _ x y diff --git a/library/init/string.lean b/library/init/string.lean index a8872901bf..65549546e6 100644 --- a/library/init/string.lean +++ b/library/init/string.lean @@ -16,5 +16,5 @@ definition concat (a b : string) : string := list.append b a end string -definition string.has_add [instance] : has_add string := -has_add.mk string.concat +definition string.has_append [instance] : has_append string := +has_append.mk string.concat diff --git a/library/init/to_string.lean b/library/init/to_string.lean index 9f48e5a60c..4aa597fca4 100644 --- a/library/init/to_string.lean +++ b/library/init/to_string.lean @@ -19,12 +19,12 @@ has_to_string.mk (λ b, if p then "tt" else "ff") definition list.to_string_aux {A : Type} [has_to_string A] : bool → list A → string | _ [] := "" -| tt (x::xs) := to_string x + list.to_string_aux ff xs -| ff (x::xs) := ", " + to_string x + list.to_string_aux ff xs +| tt (x::xs) := to_string x ++ list.to_string_aux ff xs +| ff (x::xs) := ", " ++ to_string x ++ list.to_string_aux ff xs definition list.to_string {A : Type} [has_to_string A] : list A → string | [] := "[]" -| (x::xs) := "[" + list.to_string_aux tt (x::xs) + "]" +| (x::xs) := "[" ++ list.to_string_aux tt (x::xs) ++ "]" definition list.has_to_string [instance] {A : Type} [has_to_string A] : has_to_string (list A) := has_to_string.mk list.to_string @@ -33,17 +33,17 @@ definition unit.has_to_string [instance] : has_to_string unit := has_to_string.mk (λ u, "star") definition option.has_to_string [instance] {A : Type} [has_to_string A] : has_to_string (option A) := -has_to_string.mk (λ o, match o with | none := "none" | some a := "(some " + to_string a + ")" end) +has_to_string.mk (λ o, match o with | none := "none" | some a := "(some " ++ to_string a ++ ")" end) definition sum.has_to_string [instance] {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (sum A B) := -has_to_string.mk (λ s, match s with | inl a := "(inl " + to_string a + ")" | inr b := "(inr " + to_string b + ")" end) +has_to_string.mk (λ s, match s with | inl a := "(inl " ++ to_string a ++ ")" | inr b := "(inr " ++ to_string b ++ ")" end) definition prod.has_to_string [instance] {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (prod A B) := -has_to_string.mk (λ p, "(" + to_string (pr1 p) + ", " + to_string (pr2 p) + ")") +has_to_string.mk (λ p, "(" ++ to_string (pr1 p) ++ ", " ++ to_string (pr2 p) ++ ")") definition sigma.has_to_string [instance] {A : Type} {B : A → Type} [has_to_string A] [s : ∀ x, has_to_string (B x)] : has_to_string (sigma B) := -has_to_string.mk (λ p, "⟨" + to_string (pr1 p) + ", " + to_string (pr2 p) + "⟩") +has_to_string.mk (λ p, "⟨" ++ to_string (pr1 p) ++ ", " ++ to_string (pr2 p) ++ "⟩") definition subtype.has_to_string [instance] {A : Type} {P : A → Prop} [has_to_string A] : has_to_string (subtype P) := has_to_string.mk (λ s, to_string (elt_of s)) @@ -55,15 +55,15 @@ else if char.to_nat c = 34 then "\\\"" else c::nil definition char.has_to_sting [instance] : has_to_string char := -has_to_string.mk (λ c, "'" + char.quote_core c + "'") +has_to_string.mk (λ c, "'" ++ char.quote_core c ++ "'") definition string.quote_aux : string → string | [] := "" -| (x::xs) := string.quote_aux xs + char.quote_core x +| (x::xs) := string.quote_aux xs ++ char.quote_core x definition string.quote : string → string | [] := "\"\"" -| (x::xs) := "\"" + string.quote_aux (x::xs) + "\"" +| (x::xs) := "\"" ++ string.quote_aux (x::xs) ++ "\"" definition string.has_to_string [instance] : has_to_string string := has_to_string.mk string.quote @@ -71,7 +71,7 @@ has_to_string.mk string.quote /- Remark: the code generator replaces this definition with one that display natural numbers in decimal notation -/ definition nat.to_string : nat → string | 0 := "zero" -| (succ a) := "(succ " + nat.to_string a + ")" +| (succ a) := "(succ " ++ nat.to_string a ++ ")" definition nat.has_to_string [instance] : has_to_string nat := has_to_string.mk nat.to_string diff --git a/tests/lean/local_notation_bug.lean.expected.out b/tests/lean/local_notation_bug.lean.expected.out index f31ab4af0e..496eb7420b 100644 --- a/tests/lean/local_notation_bug.lean.expected.out +++ b/tests/lean/local_notation_bug.lean.expected.out @@ -8,7 +8,7 @@ expr ↣ _Fun : expr.app string ↣ name : mk_simple_name expr ↣ [fun-class] : expr.app 10 : ?M_1 -local_notation_bug.lean:22:8: error: invalid expression +local_notation_bug.lean:22:10: error: invalid expression expr ↣ _Fun : expr.app string ↣ name : mk_simple_name expr ↣ [fun-class] : expr.app diff --git a/tests/lean/run/arity1.lean b/tests/lean/run/arity1.lean index f39385f490..90d691d300 100644 --- a/tests/lean/run/arity1.lean +++ b/tests/lean/run/arity1.lean @@ -13,6 +13,6 @@ by do bla ← mk_const "bla", infer_type bla >>= trace, n ← get_arity bla, - trace ("n arity: " + to_string n), + trace ("n arity: " ++ to_string n), when (n ≠ 3) (fail "bla is expected to have arity 3"), constructor diff --git a/tests/lean/run/eq15.lean b/tests/lean/run/eq15.lean index 90198cb42c..66cc3a88bd 100644 --- a/tests/lean/run/eq15.lean +++ b/tests/lean/run/eq15.lean @@ -3,15 +3,15 @@ open list set_option pp.implicit true -definition append : Π {A : Type}, list A → list A → list A -| append nil l := l -| append (h :: t) l := h :: (append t l) +definition app : Π {A : Type}, list A → list A → list A +| app nil l := l +| app (h :: t) l := h :: (app t l) -theorem append_nil {A : Type} (l : list A) : append nil l = l := +theorem app_nil {A : Type} (l : list A) : app nil l = l := rfl -theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) := +theorem app_cons {A : Type} (h : A) (t l : list A) : app (h :: t) l = h :: (app t l) := rfl -example : append ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := +example : app ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := rfl diff --git a/tests/lean/run/eq16.lean b/tests/lean/run/eq16.lean index 03cff78698..a9988e11f5 100644 --- a/tests/lean/run/eq16.lean +++ b/tests/lean/run/eq16.lean @@ -4,15 +4,15 @@ open list variable {A : Type} set_option pp.implicit true -definition append : list A → list A → list A -| append nil l := l -| append (h :: t) l := h :: (append t l) +definition app : list A → list A → list A +| app nil l := l +| app (h :: t) l := h :: (app t l) -theorem append_nil (l : list A) : append nil l = l := +theorem app_nil (l : list A) : app nil l = l := rfl -theorem append_cons (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) := +theorem app_cons (h : A) (t l : list A) : app (h :: t) l = h :: (app t l) := rfl -example : append ((1:num) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := +example : app ((1:num) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := rfl diff --git a/tests/lean/run/eq6.lean b/tests/lean/run/eq6.lean index abef80185e..99058edd49 100644 --- a/tests/lean/run/eq6.lean +++ b/tests/lean/run/eq6.lean @@ -1,15 +1,15 @@ import data.list open list -definition append {A : Type} : list A → list A → list A -| append nil l := l -| append (h :: t) l := h :: (append t l) +definition appd {A : Type} : list A → list A → list A +| appd nil l := l +| appd (h :: t) l := h :: (appd t l) -theorem append_nil {A : Type} (l : list A) : append nil l = l := +theorem appd_nil {A : Type} (l : list A) : appd nil l = l := rfl -theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) := +theorem appd_cons {A : Type} (h : A) (t l : list A) : appd (h :: t) l = h :: (appd t l) := rfl -example : append ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := +example : appd ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := rfl diff --git a/tests/lean/run/meta_tac6.lean b/tests/lean/run/meta_tac6.lean index ee85eb1b9c..c4e3938d01 100644 --- a/tests/lean/run/meta_tac6.lean +++ b/tests/lean/run/meta_tac6.lean @@ -16,12 +16,12 @@ by do fmt₂ ← pp t, trace $ fmt₁ + to_fmt " : " + fmt₂), trace "----------", - trace $ "num: " + to_string n, + trace $ "num: " ++ to_string n, trace_state, get_local "H3" >>= clear, (do {get_local "H3", return ()} <|> trace "get_local failed"), trace_state, assumption, n : nat ← num_goals, - trace $ "num: " + to_string n, + trace $ "num: " ++ to_string n, return () diff --git a/tests/lean/sec_notation2.lean b/tests/lean/sec_notation2.lean index 8a3610a9b0..79e99753a2 100644 --- a/tests/lean/sec_notation2.lean +++ b/tests/lean/sec_notation2.lean @@ -11,16 +11,16 @@ section postfix `+.2`:100 := add2 - local postfix `++2`:100 := add2 + local postfix `**2`:100 := add2 eval 3 +.2 - example : 3 +.2 = 3 ++2 := rfl + example : 3 +.2 = 3 **2 := rfl end eval 3 +.2 - example : 3 +.2 = 3 ++2 := rfl -- error + example : 3 +.2 = 3 **2 := rfl -- error end diff --git a/tests/lean/sec_notation2.lean.expected.out b/tests/lean/sec_notation2.lean.expected.out index 4cf4a1a32d..806649a6dd 100644 --- a/tests/lean/sec_notation2.lean.expected.out +++ b/tests/lean/sec_notation2.lean.expected.out @@ -1,5 +1,5 @@ 5 5 -sec_notation2.lean:23:21: error: invalid expression +sec_notation2.lean:23:22: error: invalid expression 5 sec_notation2.lean:30:13: error: invalid expression diff --git a/tests/lean/str1.lean.expected.out b/tests/lean/str1.lean.expected.out index ca4695cdde..7cf25e7589 100644 --- a/tests/lean/str1.lean.expected.out +++ b/tests/lean/str1.lean.expected.out @@ -4,11 +4,11 @@ "AB" : list char "ABC" : list char "abcD" : list char -"abc" ++ "cde" : list char +append "abc" "cde" : list char str 67 (str 66 (str 65 empty)) : string str 68 (str 65 (str 66 (str 99 (str 98 (str 97 empty))))) : string 65 :: str 99 (str 98 (str 97 empty)) : list char [66, 65] : list char [67, 66, 65] : list char 68 :: str 99 (str 98 (str 97 empty)) : list char -str 99 (str 98 (str 97 empty)) ++ str 101 (str 100 (str 99 empty)) : list char +append (str 99 (str 98 (str 97 empty))) (str 101 (str 100 (str 99 empty))) : list char diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out index b8e7db57f9..72183f7757 100644 --- a/tests/lean/struct_class.lean.expected.out +++ b/tests/lean/struct_class.lean.expected.out @@ -1,6 +1,7 @@ decidable : Prop → Type₁ functor : (Type → Type) → Type has_add : Type → Type +has_append : Type → Type has_div : Type → Type has_dvd : Type → Type has_inv : Type → Type @@ -28,6 +29,7 @@ well_founded : Π {A}, (A → A → Prop) → Prop decidable : Prop → Type₁ functor : (Type → Type) → Type has_add : Type → Type +has_append : Type → Type has_div : Type → Type has_dvd : Type → Type has_inv : Type → Type