From 3ee863da6857a77f1c956326a964b86a6ce461bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Oct 2018 14:58:38 -0700 Subject: [PATCH] feat(library/compiler/erase_irrelevant): eliminate `cases_on` for builtin types --- library/init/data/int/basic.lean | 20 +-- src/library/compiler/erase_irrelevant.cpp | 194 ++++++++++++++++------ src/library/constants.cpp | 32 ++++ src/library/constants.h | 8 + src/library/constants.txt | 8 + src/library/vm/vm_int.cpp | 142 ++-------------- src/library/vm/vm_nat.cpp | 137 --------------- src/library/vm/vm_string.cpp | 7 - 8 files changed, 209 insertions(+), 339 deletions(-) diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index 63ba66af19..c726f7c28b 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -15,6 +15,16 @@ inductive int : Type | of_nat : nat → int | neg_succ_of_nat : nat → int +notation `ℤ` := int + +instance : has_coe nat int := ⟨int.of_nat⟩ + +notation `-[1+ ` n `]` := int.neg_succ_of_nat n + +def int.nat_abs : int → nat +| (int.of_nat m) := m +| (int.neg_succ_of_nat m) := nat.succ m + instance : decidable_eq int := {dec_eq := λ a b, match a, b with | (int.of_nat a), (int.of_nat b) := @@ -26,12 +36,6 @@ instance : decidable_eq int := | (int.of_nat a), (int.neg_succ_of_nat b) := is_false (λ h, int.no_confusion h) | (int.neg_succ_of_nat a), (int.of_nat b) := is_false (λ h, int.no_confusion h)} -notation `ℤ` := int - -instance : has_coe nat int := ⟨int.of_nat⟩ - -notation `-[1+ ` n `]` := int.neg_succ_of_nat n - protected def int.repr : int → string | (int.of_nat n) := repr n | (int.neg_succ_of_nat n) := "-" ++ repr (succ n) @@ -84,10 +88,6 @@ m + -n instance : has_sub int := ⟨int.sub⟩ -def nat_abs : int → ℕ -| (of_nat m) := m -| -[1+ m] := succ m - def sign : int → int | (n+1:ℕ) := 1 | 0 := 0 diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index df8798dfd8..b2e9bedb15 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -220,65 +220,151 @@ class erase_irrelevant_fn { return visit_lambda_core(e, true); } + expr mk_simple_decl(expr const & e, expr const & e_type) { + name n = next_name(); + expr x = m_lctx.mk_local_decl(ngen(), n, e_type, e); + m_let_fvars.push_back(x); + m_let_entries.emplace_back(n, mk_runtime_type(e_type), e); + return x; + } + + static expr mk_list_char() { + return mk_app(mk_constant(get_list_name(), {mk_level_zero()}), mk_constant(get_char_name())); + } + + expr elim_string_cases(buffer & args) { + lean_assert(args.size() == 3); + expr major = visit(args[1]); + expr x = mk_simple_decl(mk_app(mk_constant(get_string_to_list_name()), major), mk_list_char()); + expr minor = args[2]; + minor = instantiate(binding_body(minor), x); + return visit(minor); + } + + expr elim_string_iterator_cases(buffer & args) { + lean_assert(args.size() == 3); + expr major = visit(args[1]); + expr fst = mk_simple_decl(mk_app(mk_constant(get_string_iterator_fst_name()), major), mk_list_char()); + expr snd = mk_simple_decl(mk_app(mk_constant(get_string_iterator_snd_name()), major), mk_list_char()); + expr minor = args[2]; + minor = instantiate(binding_body(minor), fst); + minor = instantiate(binding_body(minor), snd); + return visit(minor); + } + + expr elim_nat_cases(buffer & args) { + lean_assert(args.size() == 4); + expr major = visit(args[1]); + expr zero = mk_lit(literal(nat(0))); + expr one = mk_lit(literal(nat(1))); + expr nat_type = mk_constant(get_nat_name()); + expr eq = mk_app(mk_constant(get_eq_name(), {mk_level_one()}), nat_type, major, zero); + expr dec_eq = mk_app(mk_constant(get_nat_dec_eq_name()), major, zero); + expr dec_eq_type = mk_app(mk_constant(get_decidable_name(), {mk_level_one()}), eq); + expr c = mk_simple_decl(dec_eq, dec_eq_type); + expr minor_z = args[2]; + minor_z = visit_minor(mk_lambda(next_name(), eq, minor_z)); + expr minor_s = args[3]; + expr pred = mk_app(mk_constant(get_nat_sub_name()), major, one); + minor_s = ::lean::mk_let(next_name(), nat_type, pred, binding_body(minor_s)); + minor_s = visit_minor(mk_lambda(next_name(), mk_not(eq), minor_s)); + return mk_app(mk_constant(get_decidable_cases_on_name()), c, minor_s, minor_z); + } + + expr elim_int_cases(buffer & args) { + lean_assert(args.size() == 4); + expr major = visit(args[1]); + expr zero = mk_lit(literal(nat(0))); + expr int_type = mk_constant(get_int_name()); + expr nat_type = mk_constant(get_nat_name()); + expr izero = mk_simple_decl(mk_app(mk_constant(get_int_of_nat_name()), zero), int_type); + expr lt = mk_app(mk_constant(get_int_lt_name()), major, izero); + expr dec_lt = mk_app(mk_constant(get_int_decidable_lt_name()), major, izero); + expr dec_lt_type = mk_app(mk_constant(get_decidable_name(), {mk_level_one()}), lt); + expr c = mk_simple_decl(dec_lt, dec_lt_type); + expr abs = mk_app(mk_constant(get_int_nat_abs_name()), major); + expr minor_p = args[2]; + minor_p = ::lean::mk_let(next_name(), nat_type, abs, binding_body(minor_p)); + minor_p = visit_minor(mk_lambda(next_name(), mk_not(lt), minor_p)); + expr one = mk_lit(literal(nat(1))); + expr minor_n = args[3]; + minor_n = ::lean::mk_let(next_name(), nat_type, abs, + ::lean::mk_let(next_name(), nat_type, mk_app(mk_constant(get_nat_sub_name()), mk_bvar(0), one), + binding_body(minor_n))); + minor_n = visit_minor(mk_lambda(next_name(), lt, minor_n)); + return mk_app(mk_constant(get_decidable_cases_on_name()), c, minor_p, minor_n); + } + /* Remark: we only keep major and minor premises. */ expr visit_cases_on(expr const & c, buffer & args) { name const & I_name = const_name(c).get_prefix(); - unsigned minors_begin; unsigned minors_end; - std::tie(minors_begin, minors_end) = get_cases_on_minors_range(env(), const_name(c)); - if (!is_runtime_builtin_type(I_name) && minors_end == minors_begin + 1) { - expr major = args[minors_begin - 1]; - lean_assert(is_atom(major)); - expr minor = args[minors_begin]; - optional fidx = has_trivial_structure(const_name(c).get_prefix()); - /* - ``` - prod.cases_on M (\fun a b, t) - ``` - ==> - ``` - let a := M.0 in - let b := M.1 in - t - ``` - Remark: if `fidx` is not none, we use neutral element for irrelevant fields, - and major for the relevant one. - */ - unsigned i = 0; - buffer fields; - while (is_lambda(minor)) { - expr v = mk_proj(I_name, i, major); - expr t = infer_type(v); - name n = next_name(); - expr fvar = m_lctx.mk_local_decl(ngen(), n, t, v); - fields.push_back(fvar); - expr new_t; expr new_v; - if (fidx) { - if (*fidx == i) { - expr major_type = infer_type(major); - new_t = mk_runtime_type(major_type); - new_v = visit(major); - } else { - new_t = mk_enf_object_type(); - new_v = mk_enf_neutral(); - } - } else { - new_t = mk_runtime_type(t); - new_v = visit(v); - } - m_let_fvars.push_back(fvar); - m_let_entries.emplace_back(n, new_t, new_v); - i++; - minor = binding_body(minor); - } - expr r = instantiate_rev(minor, fields.size(), fields.data()); - return visit(r); + if (I_name == get_string_name()) { + return elim_string_cases(args); + } else if (I_name == get_string_iterator_name()) { + return elim_string_iterator_cases(args); + } else if (I_name == get_nat_name()) { + return elim_nat_cases(args); + } else if (I_name == get_int_name()) { + return elim_int_cases(args); } else { - buffer new_args; - new_args.push_back(visit(args[minors_begin - 1])); - for (unsigned i = minors_begin; i < minors_end; i++) { - new_args.push_back(visit_minor(args[i])); + unsigned minors_begin; unsigned minors_end; + std::tie(minors_begin, minors_end) = get_cases_on_minors_range(env(), const_name(c)); + + if (!is_runtime_builtin_type(I_name) && minors_end == minors_begin + 1) { + expr major = args[minors_begin - 1]; + lean_assert(is_atom(major)); + expr minor = args[minors_begin]; + optional fidx = has_trivial_structure(const_name(c).get_prefix()); + /* + ``` + prod.cases_on M (\fun a b, t) + ``` + ==> + ``` + let a := M.0 in + let b := M.1 in + t + ``` + Remark: if `fidx` is not none, we use neutral element for irrelevant fields, + and major for the relevant one. + */ + unsigned i = 0; + buffer fields; + while (is_lambda(minor)) { + expr v = mk_proj(I_name, i, major); + expr t = infer_type(v); + name n = next_name(); + expr fvar = m_lctx.mk_local_decl(ngen(), n, t, v); + fields.push_back(fvar); + expr new_t; expr new_v; + if (fidx) { + if (*fidx == i) { + expr major_type = infer_type(major); + new_t = mk_runtime_type(major_type); + new_v = visit(major); + } else { + new_t = mk_enf_object_type(); + new_v = mk_enf_neutral(); + } + } else { + new_t = mk_runtime_type(t); + new_v = visit(v); + } + m_let_fvars.push_back(fvar); + m_let_entries.emplace_back(n, new_t, new_v); + i++; + minor = binding_body(minor); + } + expr r = instantiate_rev(minor, fields.size(), fields.data()); + return visit(r); + } else { + buffer new_args; + new_args.push_back(visit(args[minors_begin - 1])); + for (unsigned i = minors_begin; i < minors_end; i++) { + new_args.push_back(visit_minor(args[i])); + } + return mk_app(c, new_args); } - return mk_app(c, new_args); } } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index e2d508d0ff..9675c49df0 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -39,6 +39,7 @@ name const * g_congr = nullptr; name const * g_congr_arg = nullptr; name const * g_congr_fun = nullptr; name const * g_decidable = nullptr; +name const * g_decidable_cases_on = nullptr; name const * g_decidable_to_bool = nullptr; name const * g_decidable_is_true = nullptr; name const * g_decidable_is_false = nullptr; @@ -124,6 +125,10 @@ name const * g_implies = nullptr; name const * g_implies_of_if_neg = nullptr; name const * g_implies_of_if_pos = nullptr; name const * g_int = nullptr; +name const * g_int_nat_abs = nullptr; +name const * g_int_lt = nullptr; +name const * g_int_decidable_lt = nullptr; +name const * g_int_of_nat = nullptr; name const * g_interactive_param_desc = nullptr; name const * g_interactive_parse = nullptr; name const * g_io_core = nullptr; @@ -231,8 +236,11 @@ name const * g_singleton = nullptr; name const * g_sizeof = nullptr; name const * g_sorry_ax = nullptr; name const * g_string = nullptr; +name const * g_string_to_list = nullptr; name const * g_string_empty = nullptr; name const * g_string_iterator = nullptr; +name const * g_string_iterator_fst = nullptr; +name const * g_string_iterator_snd = nullptr; name const * g_string_str = nullptr; name const * g_string_empty_ne_str = nullptr; name const * g_string_str_ne_empty = nullptr; @@ -312,6 +320,7 @@ void initialize_constants() { g_congr_arg = new name{"congr_arg"}; g_congr_fun = new name{"congr_fun"}; g_decidable = new name{"decidable"}; + g_decidable_cases_on = new name{"decidable", "cases_on"}; g_decidable_to_bool = new name{"decidable", "to_bool"}; g_decidable_is_true = new name{"decidable", "is_true"}; g_decidable_is_false = new name{"decidable", "is_false"}; @@ -397,6 +406,10 @@ void initialize_constants() { g_implies_of_if_neg = new name{"implies_of_if_neg"}; g_implies_of_if_pos = new name{"implies_of_if_pos"}; g_int = new name{"int"}; + g_int_nat_abs = new name{"int", "nat_abs"}; + g_int_lt = new name{"int", "lt"}; + g_int_decidable_lt = new name{"int", "decidable_lt"}; + g_int_of_nat = new name{"int", "of_nat"}; g_interactive_param_desc = new name{"interactive", "param_desc"}; g_interactive_parse = new name{"interactive", "parse"}; g_io_core = new name{"io_core"}; @@ -504,8 +517,11 @@ void initialize_constants() { g_sizeof = new name{"sizeof"}; g_sorry_ax = new name{"sorry_ax"}; g_string = new name{"string"}; + g_string_to_list = new name{"string", "to_list"}; g_string_empty = new name{"string", "empty"}; g_string_iterator = new name{"string", "iterator"}; + g_string_iterator_fst = new name{"string", "iterator", "fst"}; + g_string_iterator_snd = new name{"string", "iterator", "snd"}; g_string_str = new name{"string", "str"}; g_string_empty_ne_str = new name{"string", "empty_ne_str"}; g_string_str_ne_empty = new name{"string", "str_ne_empty"}; @@ -586,6 +602,7 @@ void finalize_constants() { delete g_congr_arg; delete g_congr_fun; delete g_decidable; + delete g_decidable_cases_on; delete g_decidable_to_bool; delete g_decidable_is_true; delete g_decidable_is_false; @@ -671,6 +688,10 @@ void finalize_constants() { delete g_implies_of_if_neg; delete g_implies_of_if_pos; delete g_int; + delete g_int_nat_abs; + delete g_int_lt; + delete g_int_decidable_lt; + delete g_int_of_nat; delete g_interactive_param_desc; delete g_interactive_parse; delete g_io_core; @@ -778,8 +799,11 @@ void finalize_constants() { delete g_sizeof; delete g_sorry_ax; delete g_string; + delete g_string_to_list; delete g_string_empty; delete g_string_iterator; + delete g_string_iterator_fst; + delete g_string_iterator_snd; delete g_string_str; delete g_string_empty_ne_str; delete g_string_str_ne_empty; @@ -859,6 +883,7 @@ name const & get_congr_name() { return *g_congr; } name const & get_congr_arg_name() { return *g_congr_arg; } name const & get_congr_fun_name() { return *g_congr_fun; } name const & get_decidable_name() { return *g_decidable; } +name const & get_decidable_cases_on_name() { return *g_decidable_cases_on; } name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; } name const & get_decidable_is_true_name() { return *g_decidable_is_true; } name const & get_decidable_is_false_name() { return *g_decidable_is_false; } @@ -944,6 +969,10 @@ name const & get_implies_name() { return *g_implies; } name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } name const & get_int_name() { return *g_int; } +name const & get_int_nat_abs_name() { return *g_int_nat_abs; } +name const & get_int_lt_name() { return *g_int_lt; } +name const & get_int_decidable_lt_name() { return *g_int_decidable_lt; } +name const & get_int_of_nat_name() { return *g_int_of_nat; } name const & get_interactive_param_desc_name() { return *g_interactive_param_desc; } name const & get_interactive_parse_name() { return *g_interactive_parse; } name const & get_io_core_name() { return *g_io_core; } @@ -1051,8 +1080,11 @@ name const & get_singleton_name() { return *g_singleton; } name const & get_sizeof_name() { return *g_sizeof; } name const & get_sorry_ax_name() { return *g_sorry_ax; } name const & get_string_name() { return *g_string; } +name const & get_string_to_list_name() { return *g_string_to_list; } name const & get_string_empty_name() { return *g_string_empty; } name const & get_string_iterator_name() { return *g_string_iterator; } +name const & get_string_iterator_fst_name() { return *g_string_iterator_fst; } +name const & get_string_iterator_snd_name() { return *g_string_iterator_snd; } name const & get_string_str_name() { return *g_string_str; } name const & get_string_empty_ne_str_name() { return *g_string_empty_ne_str; } name const & get_string_str_ne_empty_name() { return *g_string_str_ne_empty; } diff --git a/src/library/constants.h b/src/library/constants.h index 76faa43aa3..2ca6304616 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -41,6 +41,7 @@ name const & get_congr_name(); name const & get_congr_arg_name(); name const & get_congr_fun_name(); name const & get_decidable_name(); +name const & get_decidable_cases_on_name(); name const & get_decidable_to_bool_name(); name const & get_decidable_is_true_name(); name const & get_decidable_is_false_name(); @@ -126,6 +127,10 @@ name const & get_implies_name(); name const & get_implies_of_if_neg_name(); name const & get_implies_of_if_pos_name(); name const & get_int_name(); +name const & get_int_nat_abs_name(); +name const & get_int_lt_name(); +name const & get_int_decidable_lt_name(); +name const & get_int_of_nat_name(); name const & get_interactive_param_desc_name(); name const & get_interactive_parse_name(); name const & get_io_core_name(); @@ -233,8 +238,11 @@ name const & get_singleton_name(); name const & get_sizeof_name(); name const & get_sorry_ax_name(); name const & get_string_name(); +name const & get_string_to_list_name(); name const & get_string_empty_name(); name const & get_string_iterator_name(); +name const & get_string_iterator_fst_name(); +name const & get_string_iterator_snd_name(); name const & get_string_str_name(); name const & get_string_empty_ne_str_name(); name const & get_string_str_ne_empty_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index fd39143d49..19fa2a0102 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -34,6 +34,7 @@ congr congr_arg congr_fun decidable +decidable.cases_on decidable.to_bool decidable.is_true decidable.is_false @@ -119,6 +120,10 @@ implies implies_of_if_neg implies_of_if_pos int +int.nat_abs +int.lt +int.decidable_lt +int.of_nat interactive.param_desc interactive.parse io_core @@ -226,8 +231,11 @@ singleton sizeof sorry_ax string +string.to_list string.empty string.iterator +string.iterator.fst +string.iterator.snd string.str string.empty_ne_str string.str_ne_empty diff --git a/src/library/vm/vm_int.cpp b/src/library/vm/vm_int.cpp index 4b100a4eab..75e0561f19 100644 --- a/src/library/vm/vm_int.cpp +++ b/src/library/vm/vm_int.cpp @@ -156,91 +156,6 @@ vm_obj int_gcd(vm_obj const & a1, vm_obj const & a2) { return mk_vm_nat(r); } -vm_obj int_shiftl(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - int v1 = to_small_int(a1); - int v2 = to_small_int(a2); - - if (v1 >= 0) { - if (v2 >= 0) { - if (v2 <= 30 && v1 >> (30 - v2) == 0) // LEAN_VM_MAX_SMALL_INT = 1 >> 30 - return mk_vm_int(v1 << v2); - } else if (-v2 < 32) { - return mk_vm_int(v1 >> -v2); - } else { - return mk_vm_int(0); - } - } - } - mpz v1 = to_mpz1(a1); - if (auto v2 = try_to_int(a2)) { - if (*v2 >= 0) { - mul2k(v1, v1, *v2); - } else if (v1 < 0) { - div2k(v1, v1 + 1, -*v2); - v1--; - } else { - div2k(v1, v1, -*v2); - } - return mk_vm_int(v1); - } else { - throw exception("int.shiftl: second argument is larger than 2^31"); - } -} - -vm_obj int_land(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_int(to_small_int(a1) & to_small_int(a2)); - } else { - return mk_vm_int(to_mpz1(a1) & to_mpz2(a2)); - } -} - -vm_obj int_lor(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_int(to_small_int(a1) | to_small_int(a2)); - } else { - return mk_vm_int(to_mpz1(a1) | to_mpz2(a2)); - } -} - -vm_obj int_lxor(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_int(to_small_int(a1) ^ to_small_int(a2)); - } else { - return mk_vm_int(to_mpz1(a1) ^ to_mpz2(a2)); - } -} - -vm_obj int_lnot(vm_obj const & a) { - if (LEAN_LIKELY(is_simple(a))) { - return mk_vm_int(~to_small_int(a)); - } else { - return mk_vm_int(~to_mpz1(a)); - } -} - -vm_obj int_ldiff(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_int(to_small_int(a1) & ~to_small_int(a2)); - } else { - return mk_vm_int(to_mpz1(a1) & ~to_mpz2(a2)); - } -} - -vm_obj int_test_bit(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_bool((to_small_int(a1) & (1 << cidx(a2))) != 0); - } else { - mpz const & v1 = to_mpz1(a1); - mpz const & v2 = to_mpz2(a2); - if (v2.is_unsigned_long_int()) - return mk_vm_bool(v1.test_bit(v2.get_unsigned_long_int())); - else - return mk_vm_bool(false); - } -} - vm_obj int_decidable_eq(vm_obj const & a1, vm_obj const & a2) { if (is_simple(a1) && is_simple(a2)) { return mk_vm_bool(to_small_int(a1) == to_small_int(a2)); @@ -273,6 +188,16 @@ vm_obj int_neg(vm_obj const & a) { } } +vm_obj int_nat_abs(vm_obj const & a) { + if (is_simple(a)) { + int n = to_small_int(a); + return mk_vm_nat(n < 0 ? -n : n); + } else { + mpz z = to_mpz1(a); + return mk_vm_nat(z < 0 ? (0 - z) : z); + } +} + vm_obj int_of_nat(vm_obj const & a) { if (is_simple(a)) { return mk_vm_int(cidx(a)); @@ -289,41 +214,9 @@ vm_obj int_neg_succ_of_nat(vm_obj const & a) { } } - -void int_rec(vm_state &) { - /* recursors are implemented by the compiler */ - lean_unreachable(); -} - -void int_no_confusion(vm_state &) { - /* no_confusion is implemented by the compiler */ - lean_unreachable(); -} - -unsigned int_cases_on(vm_obj const & o, buffer & data) { - if (is_simple(o)) { - int v = to_small_int(o); - if (v >= 0) { - data.push_back(mk_vm_nat(v)); - return 0; - } else { - data.push_back(mk_vm_nat(-v - 1)); - return 1; - } - } else { - mpz const & v = to_mpz1(o); - if (v >= 0) { - data.push_back(mk_vm_nat(v)); - return 0; - } else { - data.push_back(mk_vm_nat(0 - v - 1)); - return 1; - } - } -} - void initialize_vm_int() { DECLARE_VM_BUILTIN(name({"int", "of_nat"}), int_of_nat); + DECLARE_VM_BUILTIN(name({"int", "nat_abs"}), int_nat_abs); DECLARE_VM_BUILTIN(name({"int", "neg_succ_of_nat"}), int_neg_succ_of_nat); DECLARE_VM_BUILTIN(name({"int", "add"}), int_add); DECLARE_VM_BUILTIN(name({"int", "mul"}), int_mul); @@ -334,19 +227,6 @@ void initialize_vm_int() { DECLARE_VM_BUILTIN(name({"int", "decidable_eq"}), int_decidable_eq); DECLARE_VM_BUILTIN(name({"int", "decidable_le"}), int_decidable_le); DECLARE_VM_BUILTIN(name({"int", "decidable_lt"}), int_decidable_lt); - DECLARE_VM_BUILTIN(name({"int", "shiftl"}), int_shiftl); - DECLARE_VM_BUILTIN(name({"int", "lor"}), int_lor); - DECLARE_VM_BUILTIN(name({"int", "land"}), int_land); - DECLARE_VM_BUILTIN(name({"int", "ldiff"}), int_ldiff); - DECLARE_VM_BUILTIN(name({"int", "lnot"}), int_lnot); - DECLARE_VM_BUILTIN(name({"int", "lxor"}), int_lxor); - DECLARE_VM_BUILTIN(name({"int", "test_bit"}), int_test_bit); - - DECLARE_VM_CASES_BUILTIN(name({"int", "cases_on"}), int_cases_on); - - declare_vm_builtin(name({"int", "rec_on"}), "int_rec", 4, int_rec); - declare_vm_builtin(name({"int", "no_confusion"}), "int_no_confusion", 5, int_no_confusion); - declare_vm_builtin(name({"int", "no_confusion_type"}), "int_no_confusion", 3, int_no_confusion); } void finalize_vm_int() { diff --git a/src/library/vm/vm_nat.cpp b/src/library/vm/vm_nat.cpp index 5b53e796fa..7ae0631a19 100644 --- a/src/library/vm/vm_nat.cpp +++ b/src/library/vm/vm_nat.cpp @@ -177,97 +177,6 @@ vm_obj nat_gcd(vm_obj const & a1, vm_obj const & a2) { return mk_vm_nat(r); } -vm_obj nat_shiftl(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - unsigned v1 = cidx(a1); - unsigned v2 = cidx(a2); - if (v2 <= 31 && v1 >> (31 - v2) == 0) // LEAN_VM_MAX_SMALL_NAT = 1 >> 31 - return mk_vm_nat(v1 << v2); - } - mpz v1 = to_mpz1(a1); - mul2k(v1, v1, to_unsigned(a2)); - return mk_vm_mpz(v1); -} - -vm_obj nat_shiftr(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - int v2 = cidx(a2); - return v2 < 32 ? mk_vm_nat(cidx(a1) >> v2) : mk_vm_simple(0); - } else { - mpz v1 = to_mpz1(a1); - div2k(v1, v1, to_unsigned(a2)); - return mk_vm_mpz(v1); - } -} - -vm_obj nat_div2(vm_obj const & a) { - if (LEAN_LIKELY(is_simple(a))) { - return mk_vm_nat(cidx(a) >> 1); - } else { - mpz v = to_mpz1(a); - div2k(v, v, 1); - return mk_vm_mpz(v); - } -} - -vm_obj nat_bodd(vm_obj const & a1) { - if (LEAN_LIKELY(is_simple(a1))) { - return mk_vm_bool((cidx(a1) & 1u) != 0); - } else { - mpz const & v1 = to_mpz1(a1); - return mk_vm_bool(v1.test_bit(0)); - } -} - -vm_obj nat_bodd_div2(vm_obj const & a) { - return mk_vm_pair(nat_bodd(a), nat_div2(a)); -} - -vm_obj nat_land(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_nat(cidx(a1) & cidx(a2)); - } else { - return mk_vm_mpz(to_mpz1(a1) & to_mpz2(a2)); - } -} - -vm_obj nat_lor(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_nat(cidx(a1) | cidx(a2)); - } else { - return mk_vm_mpz(to_mpz1(a1) | to_mpz2(a2)); - } -} - -vm_obj nat_lxor(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_nat(cidx(a1) ^ cidx(a2)); - } else { - return mk_vm_mpz(to_mpz1(a1) ^ to_mpz2(a2)); - } -} - -vm_obj nat_ldiff(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_nat(cidx(a1) & ~cidx(a2)); - } else { - return mk_vm_mpz(to_mpz1(a1) & ~to_mpz2(a2)); - } -} - -vm_obj nat_test_bit(vm_obj const & a1, vm_obj const & a2) { - if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { - return mk_vm_bool((cidx(a1) & (1u << cidx(a2))) != 0); - } else { - mpz const & v1 = to_mpz1(a1); - mpz const & v2 = to_mpz2(a2); - if (v2.is_unsigned_long_int()) - return mk_vm_bool(v1.test_bit(v2.get_unsigned_long_int())); - else - return mk_vm_bool(false); - } -} - vm_obj nat_decidable_eq(vm_obj const & a1, vm_obj const & a2) { if (LEAN_LIKELY(is_simple(a1) && is_simple(a2))) { return mk_vm_bool(cidx(a1) == cidx(a2)); @@ -292,16 +201,6 @@ vm_obj nat_decidable_lt(vm_obj const & a1, vm_obj const & a2) { } } -void nat_rec(vm_state &) { - /* recursors are implemented by the compiler */ - lean_unreachable(); -} - -void nat_no_confusion(vm_state &) { - /* no_confusion is implemented by the compiler */ - lean_unreachable(); -} - vm_obj nat_repr(vm_obj const & a) { std::ostringstream out; if (is_simple(a)) { @@ -312,26 +211,6 @@ vm_obj nat_repr(vm_obj const & a) { return to_obj(out.str()); } -vm_obj nat_repeat(vm_obj const &, vm_obj const & f, vm_obj const & n, vm_obj const & a) { - if (LEAN_LIKELY(is_simple(n))) { - unsigned _n = cidx(n); - vm_obj r = a; - for (unsigned i = 0; i < _n ; i++) { - r = invoke(f, mk_vm_simple(i), r); - } - return r; - } else { - mpz _n = to_mpz(n); - mpz i(0); - vm_obj r = a; - while (i < _n) { - r = invoke(f, mk_vm_nat(i), r); - i++; - } - return r; - } -} - vm_obj mix_hash(vm_obj const & u1, vm_obj const & u2) { return mk_vm_nat(hash(to_unsigned(u1), to_unsigned(u2))); } @@ -348,24 +227,8 @@ void initialize_vm_nat() { DECLARE_VM_BUILTIN(name({"nat", "decidable_le"}), nat_decidable_le); DECLARE_VM_BUILTIN(name({"nat", "decidable_lt"}), nat_decidable_lt); DECLARE_VM_BUILTIN(name({"nat", "repr"}), nat_repr); - DECLARE_VM_BUILTIN(name({"nat", "repeat"}), nat_repeat); - DECLARE_VM_BUILTIN(name({"nat", "bodd"}), nat_bodd); - DECLARE_VM_BUILTIN(name({"nat", "div2"}), nat_div2); - DECLARE_VM_BUILTIN(name({"nat", "bodd_div2"}), nat_bodd_div2); - DECLARE_VM_BUILTIN(name({"nat", "shiftl"}), nat_shiftl); - DECLARE_VM_BUILTIN(name({"nat", "shiftr"}), nat_shiftr); - DECLARE_VM_BUILTIN(name({"nat", "lor"}), nat_lor); - DECLARE_VM_BUILTIN(name({"nat", "land"}), nat_land); - DECLARE_VM_BUILTIN(name({"nat", "ldiff"}), nat_ldiff); - DECLARE_VM_BUILTIN(name({"nat", "lxor"}), nat_lxor); - DECLARE_VM_BUILTIN(name({"nat", "test_bit"}), nat_test_bit); DECLARE_VM_BUILTIN(name("mix_hash"), mix_hash); - - declare_vm_builtin(name({"nat", "cases_on"}), "nat_rec", 4, nat_rec); - declare_vm_builtin(name({"nat", "rec_on"}), "nat_rec", 4, nat_rec); - declare_vm_builtin(name({"nat", "no_confusion"}), "nat_no_confusion", 5, nat_no_confusion); - declare_vm_builtin(name({"nat", "no_confusion_type"}), "nat_no_confusion", 3, nat_no_confusion); } void finalize_vm_nat() { diff --git a/src/library/vm/vm_string.cpp b/src/library/vm/vm_string.cpp index a8dde91d92..b53ec2d848 100644 --- a/src/library/vm/vm_string.cpp +++ b/src/library/vm/vm_string.cpp @@ -116,11 +116,6 @@ vm_obj string_to_list(vm_obj const & s) { return string_to_list_core(to_vm_string(s).m_value); } -unsigned string_cases_on(vm_obj const & o, buffer & data) { - data.push_back(string_to_list(o)); - return 0; -} - vm_obj string_data(vm_obj const & s) { return string_to_list(s); } @@ -499,7 +494,6 @@ vm_obj string_hash(vm_obj const & s) { void initialize_vm_string() { DECLARE_VM_BUILTIN(name({"string", "mk"}), string_mk); DECLARE_VM_BUILTIN(name({"string", "data"}), string_data); - DECLARE_VM_CASES_BUILTIN(name({"string", "cases_on"}), string_cases_on); DECLARE_VM_BUILTIN(name({"string", "length"}), string_length); DECLARE_VM_BUILTIN(name({"string", "empty"}), string_empty); @@ -532,7 +526,6 @@ void initialize_vm_string() { DECLARE_VM_BUILTIN(name({"string", "iterator", "mk"}), string_iterator_mk); DECLARE_VM_BUILTIN(name({"string", "iterator", "fst"}), string_iterator_fst); DECLARE_VM_BUILTIN(name({"string", "iterator", "snd"}), string_iterator_snd); - DECLARE_VM_CASES_BUILTIN(name({"string", "iterator", "cases_on"}), string_iterator_cases_on); } void finalize_vm_string() {