From 4eefc41b6e286b2e9d9c605c3ea652da9f73decd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Jun 2017 16:45:18 -0700 Subject: [PATCH] refactor(*): wrap string in a structure We want to make sure string users do not depend on the string implementation. This is the first step. We need this refactoring *now* to make sure it will not be super painful to address issue #1175 --- leanpkg/leanpkg/main.lean | 14 ++-- leanpkg/leanpkg/resolve.lean | 4 +- leanpkg/leanpkg/toml.lean | 17 +++-- library/data/bitvec.lean | 2 +- library/data/buffer.lean | 6 +- library/data/buffer/parser.lean | 14 ++-- library/init/data/list/instances.lean | 2 +- library/init/data/string/basic.lean | 71 +++++++++++++++---- library/init/data/string/lemmas.lean | 16 ++--- library/init/data/to_string.lean | 12 ++-- library/init/meta/expr.lean | 7 ++ library/init/meta/format.lean | 2 +- library/init/meta/fun_info.lean | 2 +- library/init/meta/interactive_base.lean | 26 +++---- library/tools/debugger/util.lean | 34 ++++----- src/library/comp_val.cpp | 19 +++-- src/library/string.cpp | 17 +---- src/library/vm/vm_io.cpp | 1 + tests/lean/caching_user_attribute.lean | 2 +- .../caching_user_attribute.lean.expected.out | 14 ++-- tests/lean/char_lits.lean | 8 +-- tests/lean/run/1089.lean | 2 +- tests/lean/run/meta_env1.lean | 2 +- tests/lean/run/term_app2.lean | 10 +-- tests/lean/utf8.lean | 14 ++-- 25 files changed, 182 insertions(+), 136 deletions(-) diff --git a/leanpkg/leanpkg/main.lean b/leanpkg/leanpkg/main.lean index 252242371d..1d32ff52b4 100644 --- a/leanpkg/leanpkg/main.lean +++ b/leanpkg/leanpkg/main.lean @@ -32,7 +32,7 @@ return $ ev = 0 -- TODO(gabriel): io.env.get_current_directory def get_current_directory : io string := -do cwd ← io.cmd { cmd := "pwd" }, return (cwd.dropn 1) -- remove final newline +do cwd ← io.cmd { cmd := "pwd" }, return cwd.pop_back -- remove final newline def mk_path_file : ∀ (paths : list string), string | [] := "builtin_path\n" @@ -76,10 +76,8 @@ exec_cmd {cmd := "leanpkg", args := ["configure"], cwd := dir} def init (n : string) := init_pkg n "." -- TODO(gabriel): windows -def basename : ∀ (fn : string), string -| [] := [] -| (c :: rest) := - if c = '/' then [] else c :: basename rest +def basename (s : string) : string := +s.fold "" $ λ s c, if c = '/' then "" else s.str c def add_dep_to_manifest (dep : dependency) : io unit := do d ← read_manifest, @@ -87,10 +85,10 @@ let d' := { d with dependencies := d.dependencies.filter (λ old_dep, old_dep.na write_manifest d' def strip_dot_git (url : string) : string := -if url.taken 4 = ".git" then url.dropn 4 else url +if url.backn 4 = ".git" then url.popn_back 4 else url def looks_like_git_url (dep : string) : bool := -':' ∈ show list char, from dep +':' ∈ dep.to_list def absolutize_add_dep (dep : string) : io string := if looks_like_git_url dep then return dep @@ -104,7 +102,7 @@ else def git_head_revision (git_repo_dir : string) : io string := do rev ← io.cmd {cmd := "git", args := ["rev-parse", "HEAD"], cwd := git_repo_dir}, -return (rev.dropn 1) -- remove newline at end +return rev.pop_back -- remove newline at end def fixup_git_version (dir : string) : ∀ (src : source), io source | (source.git url _) := source.git url <$> git_head_revision dir diff --git a/leanpkg/leanpkg/resolve.lean b/leanpkg/leanpkg/resolve.lean index f21c2d72da..aca8a2a9a0 100644 --- a/leanpkg/leanpkg/resolve.lean +++ b/leanpkg/leanpkg/resolve.lean @@ -10,7 +10,7 @@ namespace leanpkg def assignment := hash_map string (λ _, string) -- TODO(gabriel): hash function for strings -def assignment.empty : assignment := mk_hash_map list.length +def assignment.empty : assignment := mk_hash_map string.length @[reducible] def solver := state_t assignment io instance {α : Type} : has_coe (io α) (solver α) := ⟨state_t.lift⟩ @@ -32,7 +32,7 @@ return $ ev = 0 -- TODO(gabriel): windows? def resolve_dir (abs_or_rel : string) (base : string) : string := -if abs_or_rel.reverse.head = '/' then +if abs_or_rel.front = '/' then abs_or_rel -- absolute else base ++ "/" ++ abs_or_rel diff --git a/leanpkg/leanpkg/toml.lean b/leanpkg/leanpkg/toml.lean index 9ee42cf988..f9f9b0c4ef 100644 --- a/leanpkg/leanpkg/toml.lean +++ b/leanpkg/leanpkg/toml.lean @@ -28,15 +28,15 @@ private def escapec : char → string | '\t' := "\\t" | '\n' := "\\n" | '\\' := "\\\\" -| c := [c] +| c := to_string c private def escape (s : string) : string := -list.bind s escapec +s.fold "" (λ s c, s ++ escapec c) private mutual def to_string_core, to_string_pairs with to_string_core : value → string | (value.str s) := "\"" ++ escape s ++ "\"" -| (value.nat n) := n.to_string +| (value.nat n) := to_string n | (value.bool tt) := "true" | (value.bool ff) := "false" | (value.table cs) := "{" ++ to_string_pairs cs ++ "}" @@ -76,7 +76,7 @@ ch '#' >> many' (sat (≠ '#')) >> optional (ch '\n') >> eps def Ws : parser unit := decorate_error "" $ -many' $ one_of' " \t\n" <|> Comment +many' $ one_of' " \t\n".to_list <|> Comment def tok (s : string) := str s >> Ws @@ -89,14 +89,13 @@ sat (λc, c ≠ '\"' ∧ c ≠ '\\' ∧ c.val > 0x1f) (str "\"" >> return '\"')) def BasicString : parser string := -str "\"" *> (list.reverse <$> many StringChar) <* str "\"" <* Ws +str "\"" *> (many_char StringChar) <* str "\"" <* Ws def String := BasicString def Nat : parser nat := -do l ← many1 (one_of "0123456789"), +do s ← many_char1 (one_of "0123456789".to_list), Ws, - let s : string := l.reverse, return s.to_nat def Boolean : parser bool := @@ -104,9 +103,9 @@ def Boolean : parser bool := (tok "false" >> return ff) def BareKey : parser string := do -cs ← many1 $ sat $ λ c, c.is_alpha ∨ c.is_digit ∨ c = '_' ∨ c = '-', +cs ← many_char1 $ sat $ λ c, c.is_alpha ∨ c.is_digit ∨ c = '_' ∨ c = '-', Ws, -return cs.reverse +return cs def Key := BareKey <|> BasicString diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean index 1d9ca29b4d..c9d34b0166 100644 --- a/library/data/bitvec.lean +++ b/library/data/bitvec.lean @@ -212,7 +212,7 @@ end conversion private def to_string {n : nat} : bitvec n → string | ⟨bs, p⟩ := - "0b" ++ (bs.reverse.map (λ b, if b then '1' else '0')) + "0b" ++ (bs.map (λ b : bool, if b then '1' else '0')).as_string instance (n : nat) : has_to_string (bitvec n) := ⟨to_string⟩ diff --git a/library/data/buffer.lean b/library/data/buffer.lean index 40b481575f..50726917fa 100644 --- a/library/data/buffer.lean +++ b/library/data/buffer.lean @@ -53,15 +53,15 @@ by cases b; unfold write write'; simp [array.write_eq_write'] def to_list (b : buffer α) : list α := b.to_array.to_list -protected def to_string (b : buffer α) : list α := -b.to_array.to_list.reverse +protected def to_string (b : buffer char) : string := +b.to_array.to_list.as_string def append_list {α : Type u} : buffer α → list α → buffer α | b [] := b | b (v::vs) := append_list (b.push_back v) vs def append_string (b : buffer char) (s : string) : buffer char := -b.append_list s.reverse +b.append_list s.to_list def append_array {α : Type u} {n : nat} (nz : n > 0) : buffer α → array α n → ∀ i : nat, i < n → buffer α | ⟨m, b⟩ a 0 _ := diff --git a/library/data/buffer/parser.lean b/library/data/buffer/parser.lean index f9b41eb156..06b9475d01 100644 --- a/library/data/buffer/parser.lean +++ b/library/data/buffer/parser.lean @@ -113,7 +113,7 @@ def eps : parser unit := return () /-- Matches the given character. -/ def ch (c : char) : parser unit := -decorate_error [c] $ sat (= c) >> eps +decorate_error c.to_string $ sat (= c) >> eps /-- Matches a whole char_buffer. Does not consume input in case of failure. -/ def char_buf (s : char_buffer) : parser unit := @@ -121,7 +121,7 @@ decorate_error s.to_string $ monad.for' s.to_list ch /-- Matches one out of a list of characters. -/ def one_of (cs : list char) : parser char := -decorate_errors (do c ← cs, return [c]) $ +decorate_errors (do c ← cs, return c.to_string) $ sat (∈ cs) def one_of' (cs : list char) : parser unit := @@ -129,7 +129,7 @@ one_of cs >> eps /-- Matches a string. Does not consume input in case of failure. -/ def str (s : string) : parser unit := -decorate_error s $ monad.for' s.reverse ch +decorate_error s $ monad.for' s.to_list ch /-- Number of remaining input characters. -/ def remaining : parser ℕ := @@ -148,6 +148,9 @@ def many_core (p : parser α) : ∀ (reps : ℕ), parser (list α) def many (p : parser α) : parser (list α) := λ input pos, many_core p (input.size - pos + 1) input pos +def many_char (p : parser char) : parser string := +list.as_string <$> many p + /-- Matches zero or more occurrences of `p`. -/ def many' (p : parser α) : parser unit := many p >> eps @@ -156,6 +159,9 @@ many p >> eps def many1 (p : parser α) : parser (list α) := list.cons <$> p <*> many p +def many_char1 (p : parser char) : parser string := +list.as_string <$> many1 p + /-- Matches one or more occurrences of `p`, separated by `sep`. -/ def sep_by1 (sep : parser unit) (p : parser α) : parser (list α) := list.cons <$> p <*> many (sep >> p) @@ -184,7 +190,7 @@ left_ctx.map make_monospaced ++ right_ctx.map make_monospaced ++ "\n".to_char_bu left_ctx.map (λ _, ' ') ++ "^\n".to_char_buffer ++ "\n".to_char_buffer ++ "expected: ".to_char_buffer - ++ string.to_char_buffer (list.intercalate " | " expected.to_list) + ++ string.to_char_buffer (" | ".intercalate expected.to_list) ++ "\n".to_char_buffer /-- Runs a parser on the given input. The parser needs to match the complete input. -/ diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean index 974236066c..08009b92c4 100644 --- a/library/init/data/list/instances.lean +++ b/library/init/data/list/instances.lean @@ -54,7 +54,7 @@ instance {α : Type u} [decidable_eq α] : decidable_eq (list α) := by tactic.mk_dec_eq_instance instance : decidable_eq string := -list.decidable_eq +by tactic.mk_dec_eq_instance namespace list diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 23717a37c6..3749f8c4d9 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -7,29 +7,71 @@ prelude import init.data.list.basic import init.data.char.basic -def string := list char +structure string := +(data : list char) + +def list.as_string (s : list char) : string := +⟨s.reverse⟩ namespace string -@[pattern] def empty : string := list.nil +def empty : string := +⟨list.nil⟩ instance : inhabited string := ⟨empty⟩ +def length : string → nat +| ⟨s⟩ := s.length + instance : has_sizeof string := -⟨list.sizeof⟩ +⟨string.length⟩ -@[pattern] def str : char → string → string := list.cons +def str : string → char → string +| ⟨s⟩ c := ⟨c::s⟩ -def concat (a b : string) : string := -list.append b a +def append : string → string → string +| ⟨a⟩ ⟨b⟩ := ⟨b ++ a⟩ + +def is_empty : string → bool +| ⟨[]⟩ := tt +| _ := ff instance : has_append string := -⟨string.concat⟩ +⟨string.append⟩ + +def to_list : string → list char +| ⟨s⟩ := s.reverse + +def pop_back : string → string +| ⟨s⟩ := ⟨s.tail⟩ + +def popn_back : string → nat → string +| ⟨s⟩ n := ⟨s.dropn n⟩ + +def intercalate (s : string) (ss : list string) : string := +(list.intercalate s.to_list (ss.map to_list)).as_string + +def fold {α} (a : α) (f : α → char → α) (s : string) : α := +s.to_list.foldl f a + +def front (s : string) : char := +s.to_list.head + +def back : string → char +| ⟨[]⟩ := default char +| ⟨c::cs⟩ := c + +def backn : string → nat → string +| ⟨s⟩ n := ⟨s.taken n⟩ + +def join (l : list string) : string := +l.foldl (λ r s, r ++ s) "" + end string -open list +open list string -private def utf8_length_aux : nat → nat → string → nat +private def utf8_length_aux : nat → nat → list char → nat | 0 r (c::s) := let n := char.to_nat c in if n < 0x80 then utf8_length_aux 0 (r+1) s @@ -42,8 +84,10 @@ private def utf8_length_aux : nat → nat → string → nat | (n+1) r (c::s) := utf8_length_aux n r s | n r [] := r -def utf8_length : string → nat -| s := utf8_length_aux 0 0 (reverse s) +def string.utf8_length : string → nat +| s := utf8_length_aux 0 0 s.to_list + +export string (utf8_length) private def to_nat_core : list char → nat → nat | [] r := r @@ -51,4 +95,7 @@ private def to_nat_core : list char → nat → nat to_nat_core cs (char.to_nat c - char.to_nat '0' + r*10) def string.to_nat (s : string) : nat := -to_nat_core s.reverse 0 +to_nat_core s.to_list 0 + +def char.to_string (c : char) : string := +str empty c diff --git a/library/init/data/string/lemmas.lean b/library/init/data/string/lemmas.lean index 5cac68a026..7fc873f890 100644 --- a/library/init/data/string/lemmas.lean +++ b/library/init/data/string/lemmas.lean @@ -7,15 +7,15 @@ prelude import init.meta namespace string -lemma empty_ne_str (c : char) (s : string) : empty ≠ str c s := -begin intro h, contradiction end +lemma empty_ne_str (c : char) (s : string) : empty ≠ str s c := +begin cases s, unfold str empty, intro h, injection h, contradiction end -lemma str_ne_empty (c : char) (s : string) : str c s ≠ empty := -begin intro h, contradiction end +lemma str_ne_empty (c : char) (s : string) : str s c ≠ empty := +begin cases s, unfold str empty, intro h, injection h, contradiction end -lemma str_ne_str_left {c₁ c₂ : char} (s₁ s₂ : string) : c₁ ≠ c₂ → str c₁ s₁ ≠ str c₂ s₂ := -begin intros h₁ h₂, unfold str at h₂, injection h₂, contradiction end +lemma str_ne_str_left {c₁ c₂ : char} (s₁ s₂ : string) : c₁ ≠ c₂ → str s₁ c₁ ≠ str s₂ c₂ := +begin cases s₁, cases s₂, intros h₁ h₂, unfold str at h₂, injection h₂, injection h, contradiction end -lemma str_ne_str_right (c₁ c₂ : char) {s₁ s₂ : string} : s₁ ≠ s₂ → str c₁ s₁ ≠ str c₂ s₂ := -begin intros h₁ h₂, unfold str at h₂, injection h₂, contradiction end +lemma str_ne_str_right (c₁ c₂ : char) {s₁ s₂ : string} : s₁ ≠ s₂ → str s₁ c₁ ≠ str s₂ c₂ := +begin cases s₁, cases s₂, intros h₁ h₂, unfold str at h₂, injection h₂, injection h, subst data, contradiction end end string diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean index 7f4766e873..ce41bb4484 100644 --- a/library/init/data/to_string.lean +++ b/library/init/data/to_string.lean @@ -82,18 +82,18 @@ else if c = '\t' then "\\t" else if c = '\\' then "\\\\" else if c = '\"' then "\\\"" else if char.to_nat c <= 31 then "\\x" ++ char_to_hex c -else [c] +else c.to_string instance : has_to_string char := ⟨λ c, "'" ++ char.quote_core c ++ "'"⟩ -def string.quote_aux : string → string +def string.quote_aux : list char → string | [] := "" -| (x::xs) := string.quote_aux xs ++ char.quote_core x +| (x::xs) := char.quote_core x ++ string.quote_aux xs -def string.quote : string → string -| [] := "\"\"" -| (x::xs) := "\"" ++ string.quote_aux (x::xs) ++ "\"" +def string.quote (s : string) : string := +if s.is_empty = tt then "\"\"" +else "\"" ++ string.quote_aux s.to_list ++ "\"" instance : has_to_string string := ⟨string.quote⟩ diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index b0543505e9..e430127953 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -344,6 +344,13 @@ meta def binding_body : expr → expr | (lam _ _ _ b) := b | e := e +meta def is_numeral : expr → bool +| `(@has_zero.zero %%α %%s) := tt +| `(@has_one.one %%α %%s) := tt +| `(@bit0 %%α %%s %%v) := is_numeral v +| `(@bit1 %%α %%s₁ %%s₂ %%v) := is_numeral v +| _ := ff + meta def imp (a b : expr) : expr := pi `_ binder_info.default a b diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean index 6511732d47..705372a4be 100644 --- a/library/init/meta/format.lean +++ b/library/init/meta/format.lean @@ -82,7 +82,7 @@ meta instance : has_to_format unsigned := ⟨λ n, to_fmt n.to_nat⟩ meta instance : has_to_format char := -⟨λ c : char, format.of_string [c]⟩ +⟨λ c : char, format.of_string c.to_string⟩ meta def list.to_format {α : Type u} [has_to_format α] : list α → format | [] := to_fmt "[]" diff --git a/library/init/meta/fun_info.lean b/library/init/meta/fun_info.lean index 27d3cacc56..fac4fbd911 100644 --- a/library/init/meta/fun_info.lean +++ b/library/init/meta/fun_info.lean @@ -16,7 +16,7 @@ structure param_info := open format list decidable private meta def ppfield {α : Type} [has_to_format α] (fname : string) (v : α) : format := -group $ to_fmt fname ++ space ++ to_fmt ":=" ++ space ++ nest (length fname + 4) (to_fmt v) +group $ to_fmt fname ++ space ++ to_fmt ":=" ++ space ++ nest (fname.utf8_length + 4) (to_fmt v) private meta def concat_fields (f₁ f₂ : format) : format := if is_nil f₁ then f₂ diff --git a/library/init/meta/interactive_base.lean b/library/init/meta/interactive_base.lean index 3b374f6b2f..22870fe506 100644 --- a/library/init/meta/interactive_base.lean +++ b/library/init/meta/interactive_base.lean @@ -146,36 +146,36 @@ section macros open interaction_monad open interactive -private meta def parse_format : string → string → parser pexpr +private meta def parse_format : string → list char → parser pexpr | acc [] := pure ``(to_fmt %%(reflect acc)) | acc ('\n'::s) := -do f ← parse_format [] 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, +do (e, s) ← with_input (lean.parser.pexpr 0) s.as_string, + '}'::s ← return s.to_list | fail "'}' expected", + f ← parse_format "" s, pure ``(to_fmt %%(reflect acc) ++ to_fmt %%e ++ %%f) -| acc (c::s) := parse_format (acc ++ [c]) s +| acc (c::s) := parse_format (acc ++ c.to_string) s reserve prefix `format! `:100 @[user_notation] meta def format_macro (_ : parse $ tk "format!") (s : string) : parser pexpr := -parse_format "" s.reverse +parse_format "" s.to_list -private meta def parse_sformat : string → string → parser pexpr +private meta def parse_sformat : string → list char → 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, +do (e, s) ← with_input (lean.parser.pexpr 0) s.as_string, + '}'::s ← return s.to_list | fail "'}' expected", + f ← parse_sformat "" s, pure ``(to_string %%(reflect acc) ++ to_string %%e ++ %%f) -| acc (c::s) := parse_sformat (acc ++ [c]) s +| acc (c::s) := parse_sformat (acc ++ c.to_string) s reserve prefix `sformat! `:100 @[user_notation] meta def sformat_macro (_ : parse $ tk "sformat!") (s : string) : parser pexpr := -parse_sformat "" s.reverse +parse_sformat "" s.to_list end macros diff --git a/library/tools/debugger/util.lean b/library/tools/debugger/util.lean index 12253eecf7..89d0ac32a2 100644 --- a/library/tools/debugger/util.lean +++ b/library/tools/debugger/util.lean @@ -7,31 +7,31 @@ namespace debugger def is_space (c : char) : bool := if c = ' ' ∨ c = char.of_nat 11 ∨ c = '\n' then tt else ff -def split_core : string → string → list string -| (c::cs) [] := - if is_space c then split_core cs [] else split_core cs [c] -| (c::cs) r := - if is_space c then r.reverse :: split_core cs [] else split_core cs (c::r) -| [] [] := [] -| [] r := [r.reverse] +private def split_core : list char → option string → list string +| (c::cs) none := + if is_space c then split_core cs none else split_core cs (some c.to_string) +| (c::cs) (some s) := + if is_space c then s :: split_core cs none else split_core cs (s.str c) +| [] none := [] +| [] (some s) := [s] def split (s : string) : list string := -(split_core s []).reverse +split_core s.to_list none -def to_qualified_name_core : string → string → name -| [] r := if r = "" then name.anonymous else mk_simple_name r.reverse -| (c::cs) r := - if is_space c then to_qualified_name_core cs r +def to_qualified_name_core : list char → name → string → name +| [] r s := if s.is_empty then r else r <.> s +| (c::cs) r s := + if is_space c then to_qualified_name_core cs r s else if c = '.' then - if r = "" then to_qualified_name_core cs [] - else name.mk_string r.reverse (to_qualified_name_core cs []) - else to_qualified_name_core cs (c::r) + if s.is_empty then to_qualified_name_core cs r "" + else to_qualified_name_core cs (r <.> s) "" + else to_qualified_name_core cs r (s.str c) def to_qualified_name (s : string) : name := -to_qualified_name_core s [] +to_qualified_name_core s.to_list name.anonymous "" def olean_to_lean (s : string) := -list.dropn 5 s ++ "lean" +s.popn_back 5 ++ "lean" meta def get_file (fn : name) : vm string := do { diff --git a/src/library/comp_val.cpp b/src/library/comp_val.cpp index a3ded9a5a2..3b5bc5d423 100644 --- a/src/library/comp_val.cpp +++ b/src/library/comp_val.cpp @@ -142,11 +142,10 @@ optional mk_char_val_ne_proof(expr const & a, expr const & b) { } /* Remark: this function assumes 'e' has type string */ -static bool is_string_str(expr const & e, expr & c, expr & s) { - if (is_app_of(e, get_string_str_name(), 2) || - is_app_of(e, get_list_cons_name(), 3)) { - c = app_arg(app_fn(e)); - s = app_arg(e); +static bool is_string_str(expr const & e, expr & s, expr & c) { + if (is_app_of(e, get_string_str_name(), 2)) { + s = app_arg(app_fn(e)); + c = app_arg(e); return true; } return false; @@ -154,9 +153,7 @@ static bool is_string_str(expr const & e, expr & c, expr & s) { /* Remark: this function assumes 'e' has type string */ static bool is_string_empty(expr const & e) { - return - is_constant(e, get_string_empty_name()) || - is_app_of(e, get_list_nil_name(), 1); + return is_constant(e, get_string_empty_name()); } optional mk_string_val_ne_proof(expr a, expr b) { @@ -166,8 +163,8 @@ optional mk_string_val_ne_proof(expr a, expr b) { b = *new_b; expr c_a, s_a; expr c_b, s_b; - if (is_string_str(a, c_a, s_a)) { - if (is_string_str(b, c_b, s_b)) { + if (is_string_str(a, s_a, c_a)) { + if (is_string_str(b, s_b, c_b)) { if (auto pr = mk_char_val_ne_proof(c_a, c_b)) { return some_expr(mk_app({mk_constant(get_string_str_ne_str_left_name()), c_a, c_b, s_a, s_b, *pr})); } else if (auto pr = mk_string_val_ne_proof(s_a, s_b)) { @@ -177,7 +174,7 @@ optional mk_string_val_ne_proof(expr a, expr b) { return some_expr(mk_app(mk_constant(get_string_str_ne_empty_name()), c_a, s_a)); } } else if (is_string_empty(a)) { - if (is_string_str(b, c_b, s_b)) { + if (is_string_str(b, s_b, c_b)) { return some_expr(mk_app(mk_constant(get_string_empty_ne_str_name()), c_b, s_b)); } } diff --git a/src/library/string.cpp b/src/library/string.cpp index 16d378802a..e491716206 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -24,9 +24,6 @@ static expr * g_string = nullptr; static expr * g_empty = nullptr; static expr * g_str = nullptr; static expr * g_fin_mk = nullptr; -static expr * g_list_char = nullptr; -static expr * g_list_cons = nullptr; -static expr * g_list_nil_char = nullptr; expr from_string_core(std::string const & s); @@ -125,9 +122,6 @@ void initialize_string() { g_empty = new expr(Const(get_string_empty_name())); g_str = new expr(Const(get_string_str_name())); g_fin_mk = new expr(Const(get_fin_mk_name())); - g_list_char = new expr(mk_app(mk_constant(get_list_name(), {mk_level_one()}), *g_char)); - g_list_cons = new expr(mk_constant(get_list_cons_name(), {mk_level_one()})); - g_list_nil_char = new expr(mk_app(mk_constant(get_list_nil_name(), {mk_level_one()}), *g_char)); register_macro_deserializer(*g_string_opcode, [](deserializer & d, unsigned num, expr const *) { if (num != 0) @@ -151,9 +145,6 @@ void finalize_string() { delete g_char; delete g_string_opcode; delete g_string_macro; - delete g_list_char; - delete g_list_cons; - delete g_list_nil_char; delete g_fin_mk; } @@ -162,7 +153,7 @@ expr from_string_core(std::string const & s) { for (unsigned i = 0; i < s.size(); i++) { expr n = to_nat_expr(mpz(static_cast(s[i]))); expr c = mk_app(*g_char_of_nat, n); - r = mk_app(*g_str, c, r); + r = mk_app(*g_str, r, c); } return r; } @@ -217,7 +208,7 @@ static bool append_char(expr const & e, std::string & r) { } bool to_string_core(expr const & e, std::string & r) { - if (e == *g_empty || e == *g_list_nil_char) { + if (e == *g_empty) { return true; } else if (is_string_macro(e)) { r = to_string_macro(e).get_value(); @@ -226,9 +217,7 @@ bool to_string_core(expr const & e, std::string & r) { buffer args; expr const & fn = get_app_args(e, args); if (fn == *g_str && args.size() == 2) { - return to_string_core(args[1], r) && append_char(args[0], r); - } else if (fn == *g_list_cons && args.size() == 3 && args[0] == *g_char) { - return to_string_core(args[2], r) && append_char(args[1], r); + return to_string_core(args[0], r) && append_char(args[1], r); } else { return false; } diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index f5199fdd27..be0918fb61 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -361,6 +361,7 @@ static vm_obj io_process_spawn(vm_obj const & process_obj, vm_obj const &) { if (cwd) proc.set_cwd(*cwd); auto ch = proc.spawn(); + return mk_io_result(to_obj(ch)); } diff --git a/tests/lean/caching_user_attribute.lean b/tests/lean/caching_user_attribute.lean index 663d65f9df..13f6af35f4 100644 --- a/tests/lean/caching_user_attribute.lean +++ b/tests/lean/caching_user_attribute.lean @@ -1,7 +1,7 @@ @[user_attribute] meta def foo_attr : caching_user_attribute string := { name := `foo, descr := "bar", - mk_cache := λ ns, return $ list.join ∘ list.map (list.append "\n" ∘ to_string) $ ns, + mk_cache := λ ns, return $ string.join (list.map (λ n, to_string n ++ "\n") ns), dependencies := [] } attribute [foo] eq.refl eq.mp diff --git a/tests/lean/caching_user_attribute.lean.expected.out b/tests/lean/caching_user_attribute.lean.expected.out index e07241d131..b09f771e61 100644 --- a/tests/lean/caching_user_attribute.lean.expected.out +++ b/tests/lean/caching_user_attribute.lean.expected.out @@ -1,18 +1,18 @@ [user_attributes_cache] no cached result for [foo] [user_attributes_cache] recomputing cache for [foo] -eq.refl eq.mp +eq.refl -eq.refl eq.mp +eq.refl [user_attributes_cache] cached result for [foo] has been found, but cache fingerprint does not match [user_attributes_cache] recomputing cache for [foo] -eq.refl -eq.mp eq.mpr - -eq.refl eq.mp -eq.mpr +eq.refl + +eq.mpr +eq.mp +eq.refl diff --git a/tests/lean/char_lits.lean b/tests/lean/char_lits.lean index 90d322b684..710326ab7c 100644 --- a/tests/lean/char_lits.lean +++ b/tests/lean/char_lits.lean @@ -6,7 +6,7 @@ open io #eval '\n' #eval '\\' variable [io.interface] -#eval put_str (list.cons '\\' "aaa") -#eval put_str ['\n'] -#eval put_str ['\n'] -#eval put_str (list.cons '\'' "aaa") +#eval put_str ("aaa".str '\\') +#eval put_str '\n'.to_string +#eval put_str '\n'.to_string +#eval put_str ("aaa".str '\'') diff --git a/tests/lean/run/1089.lean b/tests/lean/run/1089.lean index 18b00b9329..d48b1d4249 100644 --- a/tests/lean/run/1089.lean +++ b/tests/lean/run/1089.lean @@ -8,7 +8,7 @@ inductive token open token open option -def to_token : string → option token +def to_token : list char → option token | [] := none | (c :: cs) := let t : option token := match c with diff --git a/tests/lean/run/meta_env1.lean b/tests/lean/run/meta_env1.lean index c1ed2743a2..bb10a1abac 100644 --- a/tests/lean/run/meta_env1.lean +++ b/tests/lean/run/meta_env1.lean @@ -44,4 +44,4 @@ open name 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_fmt "") (λ d r, r ++ format.line ++ to_fmt (declaration.to_name d))) diff --git a/tests/lean/run/term_app2.lean b/tests/lean/run/term_app2.lean index f7117159f6..45922f8d09 100644 --- a/tests/lean/run/term_app2.lean +++ b/tests/lean/run/term_app2.lean @@ -46,8 +46,9 @@ def num_consts : term → nat | (term.app n ts) := ts.attach.foldl (λ r p, - have sizeof p.1 < 1 + (sizeof n + sizeof ts), from - nat.lt_one_add_of_lt (nat.lt_add_of_lt (list.sizeof_lt_sizeof_of_mem p.2)), + have sizeof p.1 < n.length + (1 + sizeof ts), from + calc sizeof p.1 < 1 + (n.length + sizeof ts) : nat.lt_one_add_of_lt (nat.lt_add_of_lt (list.sizeof_lt_sizeof_of_mem p.2)) + ... = n.length + (1 + sizeof ts) : by simp, r + num_consts p.1) 0 @@ -60,8 +61,9 @@ def num_consts' : term → nat | (term.app n ts) := ts.attach.foldl (λ r ⟨t, h⟩, - have sizeof t < 1 + (sizeof n + sizeof ts), from - nat.lt_one_add_of_lt (nat.lt_add_of_lt (list.sizeof_lt_sizeof_of_mem h)), + have sizeof t < n.length + (1 + sizeof ts), from + calc sizeof t < 1 + (n.length + sizeof ts) : nat.lt_one_add_of_lt (nat.lt_add_of_lt (list.sizeof_lt_sizeof_of_mem h)) + ... = n.length + (1 + sizeof ts) : by simp, r + num_consts' t) 0 diff --git a/tests/lean/utf8.lean b/tests/lean/utf8.lean index 8455ee9cac..5a6c7fbd5a 100644 --- a/tests/lean/utf8.lean +++ b/tests/lean/utf8.lean @@ -1,9 +1,9 @@ -open list +--open list -#eval length "α₁" -#eval length "α₁ → β₁" -#eval length "∀ α : nat → nat, α 0 ≥ 0" +#eval "α₁".length +#eval "α₁ → β₁".length +#eval "∀ α : nat → nat, α 0 ≥ 0".length #print "------------" -#eval utf8_length "α₁" -#eval utf8_length "α₁ → β₁" -#eval utf8_length "∀ α : nat → nat, α 0 ≥ 0" +#eval "α₁".utf8_length +#eval "α₁ → β₁".utf8_length +#eval "∀ α : nat → nat, α 0 ≥ 0".utf8_length