From 62d1cdcff944209b7490421c79bedd8b3a810b1f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 19 Sep 2019 17:50:24 +0200 Subject: [PATCH 1/5] chore(library/init/data/repr): fix `String.Iterator.HasRepr` --- library/init/data/repr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean index 2e76d01d9e24..aadcec323f60 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.lean @@ -129,7 +129,7 @@ instance : HasRepr Substring := ⟨fun s => String.quote s.toString ++ ".toSubstring"⟩ instance : HasRepr String.Iterator := -⟨fun it => it.remainingToString.quote ++ ".mkIterator"⟩ +⟨fun ⟨s, pos⟩ => "(String.Iterator.mk " ++ repr s ++ " " ++ repr pos ++ ")"⟩ instance (n : Nat) : HasRepr (Fin n) := ⟨fun f => repr (Fin.val f)⟩ From 61819bee6ddc1c3d1b4d66f82e9f47bf6a499230 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 19 Sep 2019 17:51:51 +0200 Subject: [PATCH 2/5] refactor(library/compiler/ir_interpreter): make `box_t/unbox_t` total --- src/library/compiler/ir_interpreter.cpp | 69 +++++++++---------------- 1 file changed, 23 insertions(+), 46 deletions(-) diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 2ba7549589be..7a2e2cd2ae13 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -195,19 +195,22 @@ union value { value(object * o): m_obj(o) {} }; -object * box_t(uint64 v, type t) { +object * box_t(value v, type t) { switch (t) { case type::Float: throw exception("floats are not supported yet"); - case type::UInt8: return box(v); - case type::UInt16: return box(v); - case type::UInt32: return box_uint32(v); - case type::UInt64: return box_uint64(v); - case type::USize: return box_size_t(v); - default: lean_unreachable(); + case type::UInt8: return box(v.m_num); + case type::UInt16: return box(v.m_num); + case type::UInt32: return box_uint32(v.m_num); + case type::UInt64: return box_uint64(v.m_num); + case type::USize: return box_size_t(v.m_num); + case type::Object: + case type::TObject: + case type::Irrelevant: + return v.m_obj; } } -uint64 unbox_t(object * o, type t) { +value unbox_t(object * o, type t) { switch (t) { case type::Float: throw exception("floats are not supported yet"); case type::UInt8: return unbox(o); @@ -215,7 +218,10 @@ uint64 unbox_t(object * o, type t) { case type::UInt32: return unbox_uint32(o); case type::UInt64: return unbox_uint64(o); case type::USize: return unbox_size_t(o); - default: lean_unreachable(); + case type::Object: + case type::TObject: + case type::Irrelevant: + return o; } } @@ -704,48 +710,19 @@ class interpreter { if (e.m_addr) { object ** args2 = static_cast(LEAN_ALLOCA(args.size() * sizeof(object *))); // NOLINT for (size_t i = 0; i < args.size(); i++) { - value v = eval_arg(args[i]); type t = param_type(decl_params(e.m_decl)[i]); - switch (t) { - case type::Float: - case type::UInt8: - case type::UInt16: - case type::UInt32: - case type::UInt64: - case type::USize: - args2[i] = box_t(v.m_num, t); - break; - case type::Object: - case type::TObject: - case type::Irrelevant: - args2[i] = v.m_obj; - if (e.m_boxed && param_borrow(decl_params(e.m_decl)[i])) { - // NOTE: If we chose the boxed version where the IR chose the unboxed one, we need to manually increment - // originally borrowed parameters because the wrapper will decrement these after the call. - // Basically the wrapper is more homogeneous (removing both unboxed and borrowed parameters) than we - // would need in this instance. - inc(args2[i]); - } - break; + args2[i] = box_t(eval_arg(args[i]), t); + if (e.m_boxed && param_borrow(decl_params(e.m_decl)[i])) { + // NOTE: If we chose the boxed version where the IR chose the unboxed one, we need to manually increment + // originally borrowed parameters because the wrapper will decrement these after the call. + // Basically the wrapper is more homogeneous (removing both unboxed and borrowed parameters) than we + // would need in this instance. + inc(args2[i]); } } push_frame(e.m_decl, old_size); object * o = curry(e.m_addr, args.size(), args2); - switch (decl_type(e.m_decl)) { - case type::Float: - case type::UInt8: - case type::UInt16: - case type::UInt32: - case type::UInt64: - case type::USize: - r = unbox_t(o, decl_type(e.m_decl)); - break; - case type::Object: - case type::TObject: - r = o; - break; - default: lean_unreachable(); - } + r = unbox_t(o, decl_type(e.m_decl)); } else { if (decl_tag(e.m_decl) == decl_kind::Extern) { throw exception(sstream() << "unexpected external declaration '" << fn << "'"); From 31c170117e508cc8bd12e5378ca5790f0bdaab30 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 19 Sep 2019 17:52:18 +0200 Subject: [PATCH 3/5] feat(frontends/lean/builtin_cmds,library/compiler/ir_interpreter): reimplement `#eval` --- src/frontends/lean/builtin_cmds.cpp | 58 ++++++++++ src/library/compiler/ir_interpreter.cpp | 135 +++++++++++++++--------- src/library/compiler/ir_interpreter.h | 2 + 3 files changed, 146 insertions(+), 49 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 447a12950ac9..b5ff53df60e7 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -40,6 +40,7 @@ Author: Leonardo de Moura #include "frontends/lean/parse_table.h" #include "frontends/lean/decl_attributes.h" #include "frontends/lean/typed_expr.h" +#include "library/compiler/ir_interpreter.h" namespace lean { environment section_cmd(parser & p) { @@ -315,6 +316,62 @@ environment hide_cmd(parser & p) { return new_env; } +static environment eval_cmd(parser & p) { + transient_cmd_scope cmd_scope(p); + auto pos = p.pos(); + expr e; names ls; + std::tie(e, ls) = parse_local_expr(p, "_eval", /* relaxed */ false); + if (has_synthetic_sorry(e)) + return p.env(); + + type_context_old tc(p.env(), transparency_mode::All); + auto type = tc.infer(e); + + bool has_eval = false; + + /* Check if resultant type has an instance of has_eval */ + try { + expr has_eval_type = mk_app(tc, "HasEval", type); + optional eval_instance = tc.mk_class_instance(has_eval_type); + if (eval_instance) { + /* Modify the 'program' to (has_eval.eval e) */ + e = mk_app(tc, {"HasEval", "eval"}, 3, type, *eval_instance, e); + type = tc.infer(e); + has_eval = true; + } + } catch (exception &) {} + + if (!has_eval) { + // NOTE: HasRepr implies HasEval + throw exception("result type does not have an instance of type class 'HasRepr' or 'HasEval'"); + } + + name fn_name = "_main"; + auto new_env = compile_expr(p.env(), p.get_options(), fn_name, ls, type, e, pos); + + auto out = p.mk_message(p.cmd_pos(), p.pos(), INFORMATION); + out.set_caption("eval result"); + scope_traces_as_messages scope_traces(p.get_stream_name(), p.cmd_pos()); + std::streambuf * saved_cout = std::cout.rdbuf(out.get_text_stream().get_stream().rdbuf()); + + // run `IO Unit` + object * args[] = { io_mk_world() }; + + if (p.profiling()) { + timeit timer(out.get_text_stream().get_stream(), "eval time"); + // NOTE: no need to free `()` + ir::run_boxed(new_env, fn_name, &args[0]); + } else { + ir::run_boxed(new_env, fn_name, &args[0]); + } + + std::cout.rdbuf(saved_cout); + out.report(); + return p.env(); +} + + + environment compact_tst_cmd(parser & p) { environment env = p.env(); unsigned num_copies = 0; @@ -410,6 +467,7 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("init_quot", "initialize `quot` type computational rules", init_quot_cmd)); add_cmd(r, cmd_info("import", "import module(s)", import_cmd)); add_cmd(r, cmd_info("hide", "hide aliases in the current scope", hide_cmd)); + add_cmd(r, cmd_info("#eval", "evaluate given expression using interpreter/precompiled code", eval_cmd)); register_decl_cmds(r); register_inductive_cmds(r); register_structure_cmd(r); diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 7a2e2cd2ae13..c89702987b11 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -737,55 +737,6 @@ class interpreter { pop_frame(r, decl_type(e.m_decl)); return r; } -public: - explicit interpreter(environment const & env) : m_env(env) { - lean_assert(g_interpreter == nullptr); - g_interpreter = this; - } - ~interpreter() { - for_each(m_constant_cache, [](name const &, constant_cache_entry const & e) { - if (!e.m_is_scalar) { - dec(e.m_val.m_obj); - } - }); - lean_assert(g_interpreter == this); - g_interpreter = nullptr; - } - - uint32 run_main(int argc, char * argv[]) { - decl d = get_fdecl("main"); - array_ref const & params = decl_params(d); - if (params.size() == 2) { // List String -> IO UInt32 - lean_object * in = lean_box(0); - int i = argc; - while (i > 0) { - i--; - lean_object * n = lean_alloc_ctor(1, 2, 0); - lean_ctor_set(n, 0, lean_mk_string(argv[i])); - lean_ctor_set(n, 1, in); - in = n; - } - m_arg_stack.push_back(in); - } else { // IO UInt32 - lean_assert(params.size() == 1); - } - object * w = io_mk_world(); - m_arg_stack.push_back(w); - push_frame(d, 0); - w = eval_body(decl_fun_body(d)).m_obj; - pop_frame(w, type::Object); - if (io_result_is_ok(w)) { - // NOTE: in an awesome hack, `IO Unit` works just as well because `pure 0` and `pure ()` use the same - // representation - int ret = unbox(io_result_get_value(w)); - dec_ref(w); - return ret; - } else { - io_result_show_error(w); - dec_ref(w); - return 1; - } - } // closure stub object * stub_m(object ** args) { @@ -852,8 +803,94 @@ class interpreter { default: return reinterpret_cast(stub_m_aux); } } +public: + explicit interpreter(environment const & env) : m_env(env) { + lean_assert(g_interpreter == nullptr); + g_interpreter = this; + } + ~interpreter() { + for_each(m_constant_cache, [](name const &, constant_cache_entry const & e) { + if (!e.m_is_scalar) { + dec(e.m_val.m_obj); + } + }); + lean_assert(g_interpreter == this); + g_interpreter = nullptr; + } + + object * call_boxed(name const & fn, object ** args) { + symbol_cache_entry e = lookup_symbol(fn); + unsigned n = decl_params(e.m_decl).size(); + object * r; + if (e.m_addr) { + push_frame(e.m_decl, 0); + // directly call boxed function, nothing more to do + r = curry(e.m_addr, n, args); + } else { + // equivalent code to boxed stubs generated by the compiler: unbox args, box result, decrement borrowed args + + if (decl_tag(e.m_decl) == decl_kind::Extern) { + throw exception(sstream() << "unexpected external declaration '" << fn << "'"); + } + // evaluate args in old stack frame + for (unsigned i = 0; i < n; i++) { + type t = param_type(decl_params(e.m_decl)[i]); + m_arg_stack.push_back(unbox_t(args[i], t)); + if (type_is_scalar(t)) { + dec(args[i]); + } + } + push_frame(e.m_decl, 0); + r = box_t(eval_body(decl_fun_body(e.m_decl)), decl_type(e.m_decl)); + for (size_t i = 0; i < n; i++) { + if (param_borrow(decl_params(e.m_decl)[i])) { + dec(args[i]); + } + } + } + pop_frame(r, decl_type(e.m_decl)); + return r; + } + + uint32 run_main(int argc, char * argv[]) { + decl d = get_fdecl("main"); + array_ref const & params = decl_params(d); + if (params.size() == 2) { // List String -> IO UInt32 + lean_object * in = lean_box(0); + int i = argc; + while (i > 0) { + i--; + lean_object * n = lean_alloc_ctor(1, 2, 0); + lean_ctor_set(n, 0, lean_mk_string(argv[i])); + lean_ctor_set(n, 1, in); + in = n; + } + m_arg_stack.push_back(in); + } else { // IO UInt32 + lean_assert(params.size() == 1); + } + object * w = io_mk_world(); + m_arg_stack.push_back(w); + push_frame(d, 0); + w = eval_body(decl_fun_body(d)).m_obj; + pop_frame(w, type::Object); + if (io_result_is_ok(w)) { + // NOTE: in an awesome hack, `IO Unit` works just as well because `pure 0` and `pure ()` use the same + // representation + int ret = unbox(io_result_get_value(w)); + dec_ref(w); + return ret; + } else { + io_result_show_error(w); + dec_ref(w); + return 1; + } + } }; +object * run_boxed(environment const & env, name const & fn, object ** args) { + return interpreter(env).call_boxed(fn, args); +} uint32 run_main(environment const & env, int argv, char * argc[]) { return interpreter(env).run_main(argv, argc); } diff --git a/src/library/compiler/ir_interpreter.h b/src/library/compiler/ir_interpreter.h index 93204ee415a3..331c5c797e45 100644 --- a/src/library/compiler/ir_interpreter.h +++ b/src/library/compiler/ir_interpreter.h @@ -10,6 +10,8 @@ Author: Sebastian Ullrich namespace lean { namespace ir { +/** \brief Run `n` using the "boxed" ABI, i.e. with all-owned parameters. */ +object * run_boxed(environment const & env, name const & fn, object ** args); uint32 run_main(environment const & env, int argv, char * argc[]); } void initialize_ir_interpreter(); From 8cb387e59959e8fd150973b131fb24464e939e2e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 19 Sep 2019 18:09:31 +0200 Subject: [PATCH 4/5] chore(tests/lean/extract): reactivate some `#eval` tests --- tests/lean/extract.lean | 69 ++++++++++++------------ tests/lean/extract.lean.expected.out | 13 ++++- tests/lean/repr_issue.lean | 2 - tests/lean/repr_issue.lean.expected.out | 3 +- tests/lean/run/array1.lean | 2 +- tests/lean/run/compiler_proj_bug.lean | 2 - tests/lean/string_imp.lean | 33 ++---------- tests/lean/string_imp.lean.expected.out | 16 +++++- tests/lean/string_imp2.lean | 29 +--------- tests/lean/string_imp2.lean.expected.out | 38 ++++++++++++- 10 files changed, 108 insertions(+), 99 deletions(-) diff --git a/tests/lean/extract.lean b/tests/lean/extract.lean index 5a09ef4e4f5f..30c4de76e9d3 100644 --- a/tests/lean/extract.lean +++ b/tests/lean/extract.lean @@ -1,80 +1,79 @@ -#exit -- Disabled until we implement new VM #eval "abc" /- some "a" -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator in - let it₂ := it₁.next in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator; + let it₂ := it₁.next; it₁.extract it₂ /- some "" -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator; it₁.extract it₁ /- none -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator in - let it₂ := it₁.next in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator; + let it₂ := it₁.next; it₂.extract it₁ /- some "abc" -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator in - let it₂ := it₁.next.next.next.prev.next in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator; + let it₂ := it₁.next.next.next.prev.next; it₁.extract it₂ /- some "bcde" -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator.next in - let it₂ := it₁.next.next.next.next in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator.next; + let it₂ := it₁.next.next.next.next; it₁.extract it₂ /- some "abcde" -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator in - let it₂ := it₁.next.next.next.next.next in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator; + let it₂ := it₁.next.next.next.next.next; it₁.extract it₂ /- some "ab" -/ #eval - let s₁ := "abcde" in - let s₂ := "abcde" in - let it₁ := s₁.mkIterator in - let it₂ := s₂.mkIterator.next.next in + let s₁ := "abcde"; + let s₂ := "abcde"; + let it₁ := s₁.mkIterator; + let it₂ := s₂.mkIterator.next.next; it₁.extract it₂ /- none -/ #eval - let s₁ := "abcde" in - let s₂ := "abhde" in - let it₁ := s₁.mkIterator in - let it₂ := s₂.mkIterator.next.next in + let s₁ := "abcde"; + let s₂ := "abhde"; + let it₁ := s₁.mkIterator; + let it₂ := s₂.mkIterator.next.next; it₁.extract it₂ /- none -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator in - let it₂ := it₁.next.setCurr 'a' in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator; + let it₂ := it₁.next.setCurr 'a'; it₁.extract it₂ /- some "a" -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator in - let it₂ := it₁.next.setCurr 'b' in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator; + let it₂ := it₁.next.setCurr 'b'; it₁.extract it₂ /- some "a" -/ #eval - let s₁ := "abcde" in - let it₁ := s₁.mkIterator in - let it₂ := (it₁.next.setCurr 'a').setCurr 'b' in + let s₁ := "abcde"; + let it₁ := s₁.mkIterator; + let it₂ := (it₁.next.setCurr 'a').setCurr 'b'; it₁.extract it₂ diff --git a/tests/lean/extract.lean.expected.out b/tests/lean/extract.lean.expected.out index 79697375bae0..c7329d7f1020 100644 --- a/tests/lean/extract.lean.expected.out +++ b/tests/lean/extract.lean.expected.out @@ -1 +1,12 @@ -extract.lean:1:0: warning: using 'exit' to interrupt Lean +"abc" +"a" +"" +"" +"abc" +"bcde" +"abcde" +"ab" +"" +"" +"a" +"a" diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean index 5651e61f14c7..29d2d32d377b 100644 --- a/tests/lean/repr_issue.lean +++ b/tests/lean/repr_issue.lean @@ -9,8 +9,6 @@ foo def ex₂ : ExceptT String (StateT (Array Nat) Id) Nat := foo -#exit - -- The following examples were producing an element of Type `id (Except String Nat)`. -- Type class resolution was failing to produce an instance for `HasRepr (id (Except String Nat))` because `id` is not transparent. #eval run ex₁ (mkArray 10 1000) diff --git a/tests/lean/repr_issue.lean.expected.out b/tests/lean/repr_issue.lean.expected.out index b267fa18dc11..1e7e4f8c8133 100644 --- a/tests/lean/repr_issue.lean.expected.out +++ b/tests/lean/repr_issue.lean.expected.out @@ -1 +1,2 @@ -repr_issue.lean:12:0: warning: using 'exit' to interrupt Lean +(ok 1000) +(ok 33) diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean index 652065af4487..41deab444526 100644 --- a/tests/lean/run/array1.lean +++ b/tests/lean/run/array1.lean @@ -14,7 +14,7 @@ a.foldl Nat.add 0 #exit #eval mkArray 4 1 -#eval Array.map (+10) v +#eval Array.map (fun x => x+10) v #eval f ⟨1, sorry⟩ #eval f ⟨9, sorry⟩ #eval (((mkArray 1 1).push 2).push 3).foldl 0 (+) diff --git a/tests/lean/run/compiler_proj_bug.lean b/tests/lean/run/compiler_proj_bug.lean index c23b8abb4e5f..788bd834fba6 100644 --- a/tests/lean/run/compiler_proj_bug.lean +++ b/tests/lean/run/compiler_proj_bug.lean @@ -4,6 +4,4 @@ structure S := def f (s : S) := s.b - s.a -#exit - #eval f {a := 5, b := 30, h := sorry } diff --git a/tests/lean/string_imp.lean b/tests/lean/string_imp.lean index 06e9b4d466ec..1b69c503d367 100644 --- a/tests/lean/string_imp.lean +++ b/tests/lean/string_imp.lean @@ -1,35 +1,12 @@ -#exit -- Disabled until we implement new VM - #eval ("abc" ++ "cde").length -#eval "abc".popBack -#eval "".popBack -#eval "abcd".popBack #eval ("abcd".mkIterator.nextn 2).remainingToString -#eval ("abcd".mkIterator.nextn 2).prevToString #eval ("abcd".mkIterator.nextn 10).remainingToString -#eval ("abcd".mkIterator.nextn 10).prevToString -#eval "foo.Lean".popnBack 5 -#eval "foo.Lean".backn 5 -#eval "αβγ".popBack #eval "αβ".length -#eval ("αβcc".mkIterator.next.insert "_foo_").toString -#eval ("αβcc".mkIterator.next.next.insert "_foo_").toString -#eval ("αβcc".mkIterator.next.next.prev.insert "_foo_").toString -#eval ("αβcc".mkIterator.remaining) -#eval ("αβcc".mkIterator.next.remaining) -#eval ("αβcc".mkIterator.next.insert "αbcβ").remaining -#eval (("αβcc".mkIterator.next.insert "αbcβ").remove 2).remaining -#eval (("αβcc".mkIterator.next.insert "αbcβ").remove 2).prev.remaining -#eval ("αβcc".mkIterator.next.toEnd).remaining -#eval "αβcc".mkIterator.offset -#eval "αβcc".mkIterator.next.offset -#eval "αβcc".mkIterator.next.next.offset -#eval ("αβcc".mkIterator.next.setCurr 'a').offset -#eval ("αβcc".mkIterator.next.insert "αbc").offset -#eval ("αβcc".mkIterator.next.insert "αbc").remaining -#eval ("αβcc".mkIterator.insert "αbc").offset -#eval ("αβcc".mkIterator.next.insert "αbcβ").offset -#eval "αβcd".mkIterator.toEnd.offset +#eval "αβcc".mkIterator.pos +#eval "αβcc".mkIterator.next.pos +#eval "αβcc".mkIterator.next.next.pos +#eval "αβcc".mkIterator.next.setCurr 'a' +#eval "αβcd".mkIterator.toEnd.pos #eval "ab\n\nfoo bla".lineColumn 0 #eval "ab\n\nfoo bla".lineColumn 1 #eval "ab\n\nfoo bla".lineColumn 2 diff --git a/tests/lean/string_imp.lean.expected.out b/tests/lean/string_imp.lean.expected.out index 22b72a4dd284..bf4bf5bcf27d 100644 --- a/tests/lean/string_imp.lean.expected.out +++ b/tests/lean/string_imp.lean.expected.out @@ -1 +1,15 @@ -string_imp.lean:1:0: warning: using 'exit' to interrupt Lean +6 +"cd" +"" +2 +0 +2 +4 +(String.Iterator.mk "αacc" 2) +6 +(3, 7) +(3, 7) +(3, 7) +(3, 7) +(3, 7) +(3, 7) diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean index 424dc14a49bc..722041021cf6 100644 --- a/tests/lean/string_imp2.lean +++ b/tests/lean/string_imp2.lean @@ -9,20 +9,6 @@ let it₁ := s.mkIterator; let it₂ := it₁.next; it₁.remainingToString ++ "-" ++ it₂.remainingToString - -#exit -- Disabled until we implement new VM - -def r (s : String) : String := -let it₁ := s.mkIterator.toEnd; -let it₂ := it₁.prev; -it₁.prevToString ++ "-" ++ it₂.prevToString - -def s (s : String) : String := -let it₁ := s.mkIterator.toEnd; -let it₂ := it₁.prev; -(it₁.insert "abc").toString ++ (it₂.insert "de").toString - - #eval "hello" ++ "hello" #eval f "hello" #eval (f "αβ").length @@ -51,8 +37,6 @@ let it₂ := it₁.prev; #eval "abc".mkIterator.remainingToString #eval ("a".push (Char.ofNat 0)) ++ "bb" #eval (("a".push (Char.ofNat 0)) ++ "αb").length -#eval r "abc" -#eval "abc".mkIterator.toEnd.prevToString #eval "".mkIterator.hasNext #eval "a".mkIterator.hasNext #eval "a".mkIterator.next.hasNext @@ -60,14 +44,5 @@ let it₂ := it₁.prev; #eval "a".mkIterator.next.hasPrev #eval "αβ".mkIterator.next.hasPrev #eval "αβ".mkIterator.next.prev.hasPrev -#eval ("αβ".mkIterator.toEnd.insert "abc").toString -#eval ("αβ".mkIterator.next.insert "abc").toString -#eval s "αβ" -#eval ("abcdef".mkIterator.next.remove 2).toString -#eval ("abcdef".mkIterator.next.next.remove 2).toString -#eval ("abcdef".mkIterator.next.remove 3).toString -#eval (("abcdef".mkIterator.next.next.next.remove 100).prev.setCurr 'a').toString -#eval ("abcdef".mkIterator.next.next.next.remove 100).hasNext -#eval ("abcdef".mkIterator.next.next.next.remove 100).prev.hasNext -#eval toBool $ "abc" = "abc" -#eval toBool $ "abc" = "abd" +#eval "abc" == "abc" +#eval "abc" == "abd" diff --git a/tests/lean/string_imp2.lean.expected.out b/tests/lean/string_imp2.lean.expected.out index 3a5dab16be66..0b0ec8edef1e 100644 --- a/tests/lean/string_imp2.lean.expected.out +++ b/tests/lean/string_imp2.lean.expected.out @@ -1 +1,37 @@ -string_imp2.lean:13:0: warning: using 'exit' to interrupt Lean +"hellohello" +"hello hello" +5 +['h', 'e', 'l', 'l', 'o'] +['α', 'β'] +[] +['α', 'β', 'γ'] +"αβγ" +"αβγ" +"αβγ" +2 +['α', 'β'] +"αβa" +"α α-" +'A' +"aβγ" +"abγ" +"abc" +"cbγ" +"0bc" +"01c" +"012" +"21c" +"λbc" +"abc-bc" +"abc" +"a\x00bb" +4 +false +true +false +false +true +true +false +true +false From f22c17e94b452db3dde3bee8029a459d9220f99a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 19 Sep 2019 18:11:44 +0200 Subject: [PATCH 5/5] chore(library/init/data/string/basic): remove broken `lineColumn` obsoleted by `FileMap` --- library/init/data/string/basic.lean | 11 ----------- tests/lean/string_imp.lean | 6 ------ tests/lean/string_imp.lean.expected.out | 6 ------ 3 files changed, 23 deletions(-) diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 287bce06ef34..358321006e70 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -257,17 +257,6 @@ def prevn : Iterator → Nat → Iterator | it, i+1 => prevn it.prev i end Iterator -private partial def lineColumnAux (s : String) : Pos → Nat × Nat → Nat × Nat -| i, r@(line, col) => - if atEnd s i then r - else - let c := s.get i; - if c = '\n' then lineColumnAux (s.next i) (line+1, 0) - else lineColumnAux (s.next i) (line, col+1) - -def lineColumn (s : String) (pos : Pos) : Nat × Nat := -lineColumnAux s 0 (1, 0) - partial def offsetOfPosAux (s : String) (pos : Pos) : Pos → Nat → Nat | i, offset => if i == pos || s.atEnd i then offset diff --git a/tests/lean/string_imp.lean b/tests/lean/string_imp.lean index 1b69c503d367..2d840ef5583d 100644 --- a/tests/lean/string_imp.lean +++ b/tests/lean/string_imp.lean @@ -7,9 +7,3 @@ #eval "αβcc".mkIterator.next.next.pos #eval "αβcc".mkIterator.next.setCurr 'a' #eval "αβcd".mkIterator.toEnd.pos -#eval "ab\n\nfoo bla".lineColumn 0 -#eval "ab\n\nfoo bla".lineColumn 1 -#eval "ab\n\nfoo bla".lineColumn 2 -#eval "ab\n\nfoo bla".lineColumn 3 -#eval "ab\n\nfoo bla".lineColumn 8 -#eval "ab\n\nfoo bla".lineColumn 100 diff --git a/tests/lean/string_imp.lean.expected.out b/tests/lean/string_imp.lean.expected.out index bf4bf5bcf27d..53ed150410e6 100644 --- a/tests/lean/string_imp.lean.expected.out +++ b/tests/lean/string_imp.lean.expected.out @@ -7,9 +7,3 @@ 4 (String.Iterator.mk "αacc" 2) 6 -(3, 7) -(3, 7) -(3, 7) -(3, 7) -(3, 7) -(3, 7)