max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/compiler/erase_irrelevant): eliminate cases_on for builtin types

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-23 14:58:38 -07:00
parent cbbae4b331
commit 3ee863da68
8 changed files with 209 additions and 339 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
library/init/data/int/basic.lean
View file

@ -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

194
src/library/compiler/erase_irrelevant.cpp
View file

@ -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<expr> & 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<expr> & 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<expr> & 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<expr> & 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<expr> & 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<unsigned> 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<expr> 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<expr> 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<unsigned> 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<expr> 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<expr> 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);
}
}

32
src/library/constants.cpp
View file

@ -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; }

8
src/library/constants.h
View file

@ -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();

8
src/library/constants.txt
View file

@ -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

142
src/library/vm/vm_int.cpp
View file

@ -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<vm_obj> & 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() {

137
src/library/vm/vm_nat.cpp
View file

@ -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() {

7
src/library/vm/vm_string.cpp
View file

@ -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<vm_obj> & 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() {