feat(runtime/lean_obj): natural number support
This commit is contained in:
Leonardo de Moura
parent
2cf731c607
commit
8cb7511a91
9 changed files with 374 additions and 46 deletions
|
|
@ -184,33 +184,28 @@ match t with
|
|||
| type.object := emit_big_binop x y z big_op
|
||||
| _ := emit_infix x y z op
|
||||
|
||||
def emit_logical_arith (t : type) (x y z : var) (bool_op : string) (op : string) (big_op : option string) : extract_m unit :=
|
||||
def emit_logical_arith (t : type) (x y z : var) (bool_op : string) (op : string) (big_op : string) : extract_m unit :=
|
||||
match t with
|
||||
| type.bool := emit_infix x y z bool_op
|
||||
| type.object :=
|
||||
(match big_op with
|
||||
| some big_op := emit_big_binop x y z big_op
|
||||
| none := throw "ill-formed binary operator")
|
||||
| type.object := emit_big_binop x y z big_op
|
||||
| _ := emit_infix x y z op
|
||||
|
||||
def emit_assign_binop (x : var) (t : type) (op : assign_binop) (y z : var) : extract_m unit :=
|
||||
match op with
|
||||
| assign_binop.add := emit_arith t x y z "+" "lean::add"
|
||||
| assign_binop.sub := emit_arith t x y z "-" "lean::sub"
|
||||
| assign_binop.mul := emit_arith t x y z "*" "lean::mul"
|
||||
| assign_binop.div := emit_arith t x y z "/" "lean::div"
|
||||
| assign_binop.mod := emit_arith t x y z "%" "lean::mod"
|
||||
| assign_binop.add := emit_arith t x y z "+" "lean::nat_add"
|
||||
| assign_binop.sub := emit_arith t x y z "-" "lean::nat_sub"
|
||||
| assign_binop.mul := emit_arith t x y z "*" "lean::nat_mul"
|
||||
| assign_binop.div := emit_arith t x y z "/" "lean::nat_div"
|
||||
| assign_binop.mod := emit_arith t x y z "%" "lean::nat_mod"
|
||||
| assign_binop.shl := emit_infix x y z "<<"
|
||||
| assign_binop.shr := emit_infix x y z ">>"
|
||||
| assign_binop.and := emit_logical_arith t x y z "&&" "&" (some "lean::and")
|
||||
| assign_binop.or := emit_logical_arith t x y z "||" "|" (some "lean::or")
|
||||
| assign_binop.xor := emit_logical_arith t x y z "!=" "^" none
|
||||
| assign_binop.le := emit_arith t x y z "<=" "lean::le"
|
||||
| assign_binop.ge := emit_arith t x y z ">=" "lean::ge"
|
||||
| assign_binop.lt := emit_arith t x y z "<" "lean::lt"
|
||||
| assign_binop.gt := emit_arith t x y z ">" "lean::gt"
|
||||
| assign_binop.eq := emit_arith t x y z "==" "lean::eq"
|
||||
| assign_binop.ne := emit_arith t x y z "!=" "lean::ne"
|
||||
| assign_binop.and := emit_logical_arith t x y z "&&" "&" "lean::nat_land"
|
||||
| assign_binop.or := emit_logical_arith t x y z "||" "|" "lean::nat_lor"
|
||||
| assign_binop.xor := emit_logical_arith t x y z "!=" "^" "lean::nat_lxor"
|
||||
| assign_binop.le := emit_arith t x y z "<=" "lean::nat_le"
|
||||
| assign_binop.lt := emit_arith t x y z "<" "lean::nat_lt"
|
||||
| assign_binop.eq := emit_arith t x y z "==" "lean::nat_eq"
|
||||
| assign_binop.ne := emit_arith t x y z "!=" "lean::nat_ne"
|
||||
| assign_binop.array_read :=
|
||||
(match t with
|
||||
| type.object := emit_var x >> emit " = lean::array_obj" >> paren (emit_var y <+> emit_var z)
|
||||
|
|
@ -234,6 +229,7 @@ def assign_unop2cpp (t : type) : assign_unop → string
|
|||
| assign_unop.array_size := "lean::array_size"
|
||||
| assign_unop.sarray_size := "lean::sarray_size"
|
||||
| assign_unop.string_len := "lean::string_len"
|
||||
| assign_unop.succ := "lean::nat_succ"
|
||||
|
||||
def emit_assign_unop (x : var) (t : type) (op : assign_unop) (y : var) : extract_m unit :=
|
||||
emit_var x >> emit " = " >> emit (assign_unop2cpp t op) >> paren(emit_var y)
|
||||
|
|
@ -252,11 +248,10 @@ match l with
|
|||
| literal.float v := emit_var x >> emit " = " >> emit v
|
||||
| literal.num v :=
|
||||
match t with
|
||||
| type.object := do
|
||||
emit_var x >> emit " = lean::alloc_mpz(lean::mpz(",
|
||||
if v < uint32_sz then emit v >> emit "u"
|
||||
else emit "\"" >> emit v >> emit "\"",
|
||||
emit "))"
|
||||
| type.object :=
|
||||
emit_var x >> emit " = " >>
|
||||
if v < uint32_sz then emit "lean::mk_nat_obj" >> paren(emit v >> emit "u")
|
||||
else emit "lean::mk_mpz_core(lean::mpz(\"" >> emit v >> emit "\"))"
|
||||
| _ := emit_var x >> emit " = " >> emit v >> emit_num_suffix t
|
||||
|
||||
def unop2cpp : unop → string
|
||||
|
|
|
|||
|
|
@ -55,7 +55,8 @@ def assign_unop.to_format : assign_unop → format
|
|||
| assign_unop.cast := "cast"
|
||||
| assign_unop.array_copy := "array_copy" | assign_unop.sarray_copy := "sarray_copy"
|
||||
| assign_unop.array_size := "array_size" | assign_unop.sarray_size := "sarray_size"
|
||||
| assign_unop.string_len := "string_len"
|
||||
| assign_unop.string_len := "string_len" | assign_unop.succ := "succ"
|
||||
|
||||
|
||||
instance assign_unop.has_to_format : has_to_format assign_unop := ⟨assign_unop.to_format⟩
|
||||
instance assign_unop.has_to_string : has_to_string assign_unop := ⟨pretty ∘ to_fmt⟩
|
||||
|
|
@ -64,8 +65,7 @@ def assign_binop.to_format : assign_binop → format
|
|||
| assign_binop.add := "add" | assign_binop.sub := "sub" | assign_binop.mul := "mul" | assign_binop.div := "div"
|
||||
| assign_binop.mod := "mod" | assign_binop.shl := "shl" | assign_binop.shr := "shr"
|
||||
| assign_binop.and := "and" | assign_binop.or := "or" | assign_binop.xor := "xor" | assign_binop.le := "le"
|
||||
| assign_binop.ge := "ge" | assign_binop.lt := "lt" | assign_binop.gt := "gt" | assign_binop.eq := "eq"
|
||||
| assign_binop.ne := "ne"
|
||||
| assign_binop.lt := "lt" | assign_binop.eq := "eq" | assign_binop.ne := "ne"
|
||||
| assign_binop.array_read := "array_read"
|
||||
|
||||
instance assign_binop.has_to_format : has_to_format assign_binop := ⟨assign_binop.to_format⟩
|
||||
|
|
|
|||
|
|
@ -61,15 +61,18 @@ Remark: `sarray_copy` can be used to copy strings.
|
|||
- `x : usize := array_size y` stores the size of the array `y : object` into `x`.
|
||||
The behavior is unspecified if `y` is not an array of objects.
|
||||
|
||||
- `x : usize : sarray_size y` stores the size of the scalar array `y : object` into `x`.
|
||||
- `x : usize := sarray_size y` stores the size of the scalar array `y : object` into `x`.
|
||||
The behavior is unspecified if `y` is not an array of scalar values.
|
||||
|
||||
- `x : usize : string_len y` stores the length of the string `y : object` into `x`.
|
||||
- `x : usize := string_len y` stores the length of the string `y : object` into `x`.
|
||||
The length is the number of unicode scalar values.
|
||||
The behavior is unspecified if `y` is not a string. -/
|
||||
The behavior is unspecified if `y` is not a string.
|
||||
|
||||
- `x : object := succ y` natural number successor. -/
|
||||
inductive assign_unop
|
||||
| not | neg | is_scalar | is_shared | is_null | cast | box | unbox
|
||||
| array_copy | sarray_copy | array_size | sarray_size | string_len
|
||||
| succ
|
||||
|
||||
/-- Operators for instructions of the form `x : t := op y z`
|
||||
|
||||
|
|
@ -102,15 +105,9 @@ Remark: `t ≠ bool`, `t ≠ float`, `t ≠ double` and `t ≠ object`.
|
|||
- `x : bool := le y z`: less than or equal to. Remark: `t ≠ bool`.
|
||||
If `y` and `z` are `object`, then they must be big numbers.
|
||||
|
||||
- `x : bool := ge y z`: greater than or equal to. Remark: `t ≠ bool`.
|
||||
If `y` and `z` are `object`, then they must be big numbers.
|
||||
|
||||
- `x : bool := lt y z`: less than. Remark: `t ≠ bool`.
|
||||
If `y` and `z` are `object`, then they must be big numbers.
|
||||
|
||||
- `x : bool := gt y z`: greater than. Remark: `t ≠ bool`.
|
||||
If `y` and `z` are `object`, then they must be big numbers.
|
||||
|
||||
- `x : bool := eq y z`: equality test. If `y` and `z` are `object`, then they must be big numbers.
|
||||
|
||||
- `x : bool := ne y z`: disequality test. If `y` and `z` are `object`, then they must be big numbers.
|
||||
|
|
@ -119,7 +116,7 @@ If `y` and `z` are `object`, then they must be big numbers.
|
|||
If `a` is a scalar array, then `t ≠ object`. If `a` is an (non-scalar) array, then `t = object`. -/
|
||||
inductive assign_binop
|
||||
| add | sub | mul | div | mod | shl | shr | and | or | xor
|
||||
| le | ge | lt | gt | eq | ne
|
||||
| le | lt | eq | ne
|
||||
| array_read -- (scalar) array read
|
||||
|
||||
/-- Operators for instructions of the form `op x`
|
||||
|
|
|
|||
|
|
@ -46,6 +46,7 @@ def parse_assign_unop : parser assign_unop :=
|
|||
<|> (keyword "array_size" >> return assign_unop.array_size)
|
||||
<|> (keyword "sarray_size" >> return assign_unop.sarray_size)
|
||||
<|> (keyword "string_len" >> return assign_unop.string_len)
|
||||
<|> (keyword "succ" >> return assign_unop.succ)
|
||||
|
||||
def parse_assign_binop : parser assign_binop :=
|
||||
(keyword "add" >> return assign_binop.add)
|
||||
|
|
@ -59,9 +60,7 @@ def parse_assign_binop : parser assign_binop :=
|
|||
<|> (keyword "or" >> return assign_binop.or)
|
||||
<|> (keyword "xor" >> return assign_binop.xor)
|
||||
<|> (keyword "le" >> return assign_binop.le)
|
||||
<|> (keyword "ge" >> return assign_binop.ge)
|
||||
<|> (keyword "lt" >> return assign_binop.lt)
|
||||
<|> (keyword "gt" >> return assign_binop.gt)
|
||||
<|> (keyword "eq" >> return assign_binop.eq)
|
||||
<|> (keyword "ne" >> return assign_binop.ne)
|
||||
<|> (keyword "array_read" >> return assign_binop.array_read)
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ def reserved := [ "bool", "byte", "uint16", "uint32", "uint64",
|
|||
"apply", "cnstr", "set", "get", "sset", "sget", "array", "read",
|
||||
"write", "sarray", "sread", "swrite", "inc", "decs", "dec", "del",
|
||||
"phi", "ret", "case", "jmp", "decl", "tt", "ff", "def", "external",
|
||||
"defconst"]
|
||||
"defconst", "succ"]
|
||||
|
||||
def reserved_set : rbtree string (<) :=
|
||||
reserved.foldl rbtree.insert (mk_rbtree string (<))
|
||||
|
|
|
|||
|
|
@ -56,6 +56,7 @@ match op with
|
|||
| assign_unop.array_size := r = type.usize && t = type.object
|
||||
| assign_unop.sarray_size := r = type.usize && t = type.object
|
||||
| assign_unop.string_len := r = type.usize && t = type.object
|
||||
| assign_unop.succ := r = type.object && t = type.object
|
||||
|
||||
/-- Return `tt` iff the instruction `x : r := op y z` is type correct where `y z : t` -/
|
||||
def valid_assign_binop_types (op : assign_binop) (r : type) (t₁ t₂ : type) : bool :=
|
||||
|
|
@ -71,9 +72,7 @@ match op with
|
|||
| assign_binop.or := r = t₁ && r = t₂ && is_bitwise_ty r
|
||||
| assign_binop.xor := r = t₁ && r = t₂ && is_bitwise_ty r
|
||||
| assign_binop.le := r = type.bool && t₁ = t₂ && is_arith_ty t₁
|
||||
| assign_binop.ge := r = type.bool && t₁ = t₂ && is_arith_ty t₁
|
||||
| assign_binop.lt := r = type.bool && t₁ = t₂ && is_arith_ty t₁
|
||||
| assign_binop.gt := r = type.bool && t₁ = t₂ && is_arith_ty t₁
|
||||
| assign_binop.eq := r = type.bool && t₁ = t₂
|
||||
| assign_binop.ne := r = type.bool && t₁ = t₂
|
||||
| assign_binop.array_read := t₁ = type.object && t₂ = type.usize
|
||||
|
|
|
|||
|
|
@ -107,6 +107,8 @@ void del(lean_obj * o) {
|
|||
}
|
||||
}
|
||||
|
||||
/* Strings */
|
||||
|
||||
lean_obj * mk_string(char const * s) {
|
||||
size_t sz = strlen(s);
|
||||
size_t len = utf8_strlen(s);
|
||||
|
|
@ -121,6 +123,132 @@ lean_obj * mk_string(std::string const & s) {
|
|||
return mk_string(s.c_str());
|
||||
}
|
||||
|
||||
/* Natural numbers */
|
||||
|
||||
lean_obj * nat_big_add(lean_obj * a1, lean_obj * a2) {
|
||||
lean_assert(!is_scalar(a1) || !is_scalar(a2));
|
||||
if (is_scalar(a1))
|
||||
return mk_mpz_core(unbox(a1) + mpz_value(a2));
|
||||
else if (is_scalar(a2))
|
||||
return mk_mpz_core(mpz_value(a1) + unbox(a2));
|
||||
else
|
||||
return mk_mpz_core(mpz_value(a1) + mpz_value(a2));
|
||||
}
|
||||
|
||||
lean_obj * nat_big_sub(lean_obj * a1, lean_obj * a2) {
|
||||
lean_assert(!is_scalar(a1) || !is_scalar(a2));
|
||||
if (is_scalar(a1)) {
|
||||
lean_assert(unbox(a1) < mpz_value(a2));
|
||||
return box(0);
|
||||
} else if (is_scalar(a2)) {
|
||||
lean_assert(mpz_value(a1) > unbox(a2));
|
||||
return mk_mpz(mpz_value(a1) - unbox(a2));
|
||||
} else {
|
||||
if (mpz_value(a1) < mpz_value(a2))
|
||||
return box(0);
|
||||
else
|
||||
return mk_mpz(mpz_value(a1) - mpz_value(a2));
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_mul(lean_obj * a1, lean_obj * a2) {
|
||||
lean_assert(!is_scalar(a1) || !is_scalar(a2));
|
||||
if (is_scalar(a1))
|
||||
return mk_mpz_core(unbox(a1) * mpz_value(a2));
|
||||
else if (is_scalar(a2))
|
||||
return mk_mpz_core(mpz_value(a1) * unbox(a2));
|
||||
else
|
||||
return mk_mpz_core(mpz_value(a1) * mpz_value(a2));
|
||||
}
|
||||
|
||||
lean_obj * nat_big_div(lean_obj * a1, lean_obj * a2) {
|
||||
lean_assert(!is_scalar(a1) || !is_scalar(a2));
|
||||
if (is_scalar(a1)) {
|
||||
lean_assert(mpz_value(a2) != 0);
|
||||
lean_assert(unbox(a1) / mpz_value(a2) == 0);
|
||||
return box(0);
|
||||
} else if (is_scalar(a2)) {
|
||||
unsigned n2 = unbox(a2);
|
||||
return n2 == 0 ? a2 : mk_mpz(mpz_value(a1) / n2);
|
||||
} else {
|
||||
lean_assert(mpz_value(a2) != 0);
|
||||
return mk_mpz(mpz_value(a1) / mpz_value(a2));
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_mod(lean_obj * a1, lean_obj * a2) {
|
||||
lean_assert(!is_scalar(a1) || !is_scalar(a2));
|
||||
if (is_scalar(a1)) {
|
||||
lean_assert(mpz_value(a2) != 0);
|
||||
return a1;
|
||||
} else if (is_scalar(a2)) {
|
||||
unsigned n2 = unbox(a2);
|
||||
return n2 == 0 ? a2 : box((mpz_value(a1) % mpz(n2)).get_unsigned_int());
|
||||
} else {
|
||||
lean_assert(mpz_value(a2) != 0);
|
||||
return mk_mpz(mpz_value(a1) % mpz_value(a2));
|
||||
}
|
||||
}
|
||||
|
||||
bool nat_big_eq(lean_obj * a1, lean_obj * a2) {
|
||||
if (is_scalar(a1))
|
||||
return unbox(a1) == mpz_value(a2);
|
||||
else if (is_scalar(a2))
|
||||
return mpz_value(a1) == unbox(a2);
|
||||
else
|
||||
return mpz_value(a1) == mpz_value(a2);
|
||||
}
|
||||
|
||||
bool nat_big_le(lean_obj * a1, lean_obj * a2) {
|
||||
if (is_scalar(a1))
|
||||
return unbox(a1) <= mpz_value(a2);
|
||||
else if (is_scalar(a2))
|
||||
return mpz_value(a1) <= unbox(a2);
|
||||
else
|
||||
return mpz_value(a1) <= mpz_value(a2);
|
||||
}
|
||||
|
||||
bool nat_big_lt(lean_obj * a1, lean_obj * a2) {
|
||||
if (is_scalar(a1))
|
||||
return unbox(a1) < mpz_value(a2);
|
||||
else if (is_scalar(a2))
|
||||
return mpz_value(a1) < unbox(a2);
|
||||
else
|
||||
return mpz_value(a1) < mpz_value(a2);
|
||||
}
|
||||
|
||||
lean_obj * nat_big_land(lean_obj * a1, lean_obj * a2) {
|
||||
lean_assert(!is_scalar(a1) || !is_scalar(a2));
|
||||
if (is_scalar(a1))
|
||||
return mk_mpz(mpz(unbox(a1)) & mpz_value(a2));
|
||||
else if (is_scalar(a2))
|
||||
return mk_mpz(mpz_value(a1) & mpz(unbox(a2)));
|
||||
else
|
||||
return mk_mpz(mpz_value(a1) & mpz_value(a2));
|
||||
}
|
||||
|
||||
lean_obj * nat_big_lor(lean_obj * a1, lean_obj * a2) {
|
||||
lean_assert(!is_scalar(a1) || !is_scalar(a2));
|
||||
if (is_scalar(a1))
|
||||
return mk_mpz(mpz(unbox(a1)) | mpz_value(a2));
|
||||
else if (is_scalar(a2))
|
||||
return mk_mpz(mpz_value(a1) | mpz(unbox(a2)));
|
||||
else
|
||||
return mk_mpz(mpz_value(a1) | mpz_value(a2));
|
||||
}
|
||||
|
||||
lean_obj * nat_big_lxor(lean_obj * a1, lean_obj * a2) {
|
||||
lean_assert(!is_scalar(a1) || !is_scalar(a2));
|
||||
if (is_scalar(a1))
|
||||
return mk_mpz(mpz(unbox(a1)) ^ mpz_value(a2));
|
||||
else if (is_scalar(a2))
|
||||
return mk_mpz(mpz_value(a1) ^ mpz(unbox(a2)));
|
||||
else
|
||||
return mk_mpz(mpz_value(a1) ^ mpz_value(a2));
|
||||
}
|
||||
|
||||
/* Debugging helper functions */
|
||||
|
||||
void dbg_print_str(lean_obj * o) {
|
||||
lean_assert(is_string(o));
|
||||
std::cout << c_str(o) << "\n";
|
||||
|
|
|
|||
|
|
@ -6,7 +6,9 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#pragma once
|
||||
#include <string>
|
||||
#include "runtime/compiler_hints.h"
|
||||
#include "runtime/mpz.h"
|
||||
#include "runtime/int64.h"
|
||||
|
||||
namespace lean {
|
||||
enum class lean_obj_kind { Constructor, Closure, Array, ScalarArray, MPZ, External };
|
||||
|
|
@ -93,7 +95,7 @@ struct lean_external : public lean_obj {
|
|||
};
|
||||
|
||||
inline bool is_scalar(lean_obj * o) { return (reinterpret_cast<uintptr_t>(o) & 1) == 1; }
|
||||
inline lean_obj * box(unsigned n) { return reinterpret_cast<lean_obj*>(static_cast<uintptr_t>((n << 1) | 1)); }
|
||||
inline lean_obj * box(unsigned n) { return reinterpret_cast<lean_obj*>((static_cast<uintptr_t>(n) << 1) | 1); }
|
||||
inline unsigned unbox(lean_obj * o) { return reinterpret_cast<uintptr_t>(o) >> 1; }
|
||||
|
||||
/* Generic Lean object delete operation.
|
||||
|
|
@ -316,12 +318,188 @@ inline void set_closure_arg(lean_obj * o, unsigned i, lean_obj * a) {
|
|||
set_obj_data(o, sizeof(lean_closure) + sizeof(lean_obj*)*i, a); // NOLINT
|
||||
}
|
||||
|
||||
/* Constructors */
|
||||
|
||||
inline lean_obj * mk_mpz(mpz const & m) { return alloc_mpz(m); }
|
||||
/* String */
|
||||
|
||||
lean_obj * mk_string(char const * s);
|
||||
lean_obj * mk_string(std::string const & s);
|
||||
inline bool is_string(lean_obj * o) { return !is_scalar(o) && is_sarray(o) && sarray_elem_size(o) == 1; }
|
||||
inline char const * c_str(lean_obj * o) { lean_assert(is_string(o)); return sarray_cptr<char>(o) + sizeof(size_t); }
|
||||
|
||||
/* Natural numbers */
|
||||
|
||||
#define LEAN_MAX_SMALL_NAT (sizeof(void*) == 8 ? std::numeric_limits<unsigned>::max() : (std::numeric_limits<unsigned>::max() >> 1)) // NOLINT
|
||||
|
||||
inline lean_obj * mk_mpz_core(mpz const & m) {
|
||||
lean_assert(m > LEAN_MAX_SMALL_NAT);
|
||||
return alloc_mpz(m);
|
||||
}
|
||||
|
||||
inline lean_obj * mk_mpz(mpz const & m) {
|
||||
if (m > LEAN_MAX_SMALL_NAT)
|
||||
return mk_mpz_core(m);
|
||||
else
|
||||
return box(m.get_unsigned_int());
|
||||
}
|
||||
|
||||
inline lean_obj * mk_nat_obj(unsigned n) {
|
||||
if (sizeof(void*) == 8) { // NOLINT
|
||||
return box(n);
|
||||
} else if (n <= LEAN_MAX_SMALL_NAT) {
|
||||
return box(n);
|
||||
} else {
|
||||
return mk_mpz_core(mpz(n));
|
||||
}
|
||||
}
|
||||
|
||||
inline lean_obj * mk_nat_obj(uint64 n) {
|
||||
if (LEAN_LIKELY(n < LEAN_MAX_SMALL_NAT)) {
|
||||
return box(n);
|
||||
} else {
|
||||
return mk_mpz_core(mpz(n));
|
||||
}
|
||||
}
|
||||
|
||||
inline uint64 nat2uint64(lean_obj * a) {
|
||||
lean_assert(is_scalar(a));
|
||||
return unbox(a);
|
||||
}
|
||||
|
||||
inline lean_obj * nat_succ(lean_obj * a) {
|
||||
if (LEAN_LIKELY(is_scalar(a))) {
|
||||
return mk_nat_obj(nat2uint64(a) + 1);
|
||||
} else {
|
||||
return mk_mpz_core(mpz_value(a) + 1);
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_add(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline lean_obj * nat_add(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
return mk_nat_obj(nat2uint64(a1) + nat2uint64(a2));
|
||||
} else {
|
||||
return nat_big_add(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_sub(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline lean_obj * nat_sub(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
unsigned n1 = unbox(a1);
|
||||
unsigned n2 = unbox(a2);
|
||||
if (n1 < n2)
|
||||
return box(0);
|
||||
else
|
||||
return box(n1 - n2);
|
||||
} else {
|
||||
return nat_big_sub(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_mul(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline lean_obj * nat_mul(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
return mk_nat_obj(nat2uint64(a1) * nat2uint64(a2));
|
||||
} else {
|
||||
return nat_big_mul(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_div(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline lean_obj * nat_div(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
unsigned n1 = unbox(a1);
|
||||
unsigned n2 = unbox(a2);
|
||||
if (n2 == 0)
|
||||
return box(0);
|
||||
else
|
||||
return box(n1 / n2);
|
||||
} else {
|
||||
return nat_big_div(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_mod(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline lean_obj * nat_mod(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
unsigned n1 = unbox(a1);
|
||||
unsigned n2 = unbox(a2);
|
||||
if (n2 == 0)
|
||||
return box(0);
|
||||
else
|
||||
return box(n1 % n2);
|
||||
} else {
|
||||
return nat_big_mod(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
bool nat_big_eq(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline bool nat_eq(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
return a1 == a2;
|
||||
} else {
|
||||
return nat_big_eq(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
inline bool nat_ne(lean_obj * a1, lean_obj * a2) {
|
||||
return !nat_eq(a1, a2);
|
||||
}
|
||||
|
||||
bool nat_big_le(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline bool nat_le(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
return a1 <= a2;
|
||||
} else {
|
||||
return nat_big_le(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
bool nat_big_lt(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline bool nat_lt(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
return a1 < a2;
|
||||
} else {
|
||||
return nat_big_lt(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_land(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline lean_obj * nat_land(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
return reinterpret_cast<lean_obj*>(reinterpret_cast<uintptr_t>(a1) & reinterpret_cast<uintptr_t>(a2));
|
||||
} else {
|
||||
return nat_big_land(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_lor(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline lean_obj * nat_lor(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
return reinterpret_cast<lean_obj*>(reinterpret_cast<uintptr_t>(a1) | reinterpret_cast<uintptr_t>(a2));
|
||||
} else {
|
||||
return nat_big_lor(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
lean_obj * nat_big_xor(lean_obj * a1, lean_obj * a2);
|
||||
|
||||
inline lean_obj * nat_lxor(lean_obj * a1, lean_obj * a2) {
|
||||
if (LEAN_LIKELY(is_scalar(a1) && is_scalar(a2))) {
|
||||
return box(unbox(a1) ^ unbox(a2));
|
||||
} else {
|
||||
return nat_big_xor(a1, a2);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
|
|||
32
tests/ir/tst2.ir
Normal file
32
tests/ir/tst2.ir
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
[lean_dbg_print_str] external print_str (s : object)
|
||||
[lean_dbg_print_num] external print_num (s : object)
|
||||
|
||||
def print_bool (b : bool) :=
|
||||
entry:
|
||||
case b [false_lbl, true_lbl];
|
||||
true_lbl:
|
||||
s1 : object := "true";
|
||||
call print_str s1;
|
||||
ret;
|
||||
false_lbl:
|
||||
s2 : object := "false";
|
||||
call print_str s2;
|
||||
ret;
|
||||
|
||||
def main : int32 :=
|
||||
entry:
|
||||
n1 : object := 10;
|
||||
n2 : object := 20;
|
||||
n3 : object := add n1 n2;
|
||||
n4 : object := mul n3 n3;
|
||||
call print_num n4;
|
||||
c1 : bool := lt n4 n1;
|
||||
call print_bool c1;
|
||||
c2 : bool := le n4 n4;
|
||||
call print_bool c2;
|
||||
n5 : object := 100000000000000000;
|
||||
n6 : object := 200000000000000000;
|
||||
n7 : object := add n5 n6;
|
||||
call print_num n7;
|
||||
r : int32 := 0;
|
||||
ret r;
|
||||
Loading…
Add table
Reference in a new issue