From 350cf4d262d75eb3b474546e62bb74ea755ba2ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 May 2020 13:53:06 -0700 Subject: [PATCH] chore: copy runtime files to `include/lean` --- src/include/lean/alloc.h | 16 + src/include/lean/allocprof.h | 29 + src/include/lean/apply.h | 11 + src/include/lean/compact.h | 81 ++ src/include/lean/compiler_hints.h | 17 + src/include/lean/debug.h | 129 ++ src/include/lean/exception.h | 67 + src/include/lean/extensible_object.h | 87 ++ src/include/lean/flet.h | 33 + src/include/lean/hash.h | 91 ++ src/include/lean/init_module.h | 12 + src/include/lean/int64.h | 13 + src/include/lean/interrupt.h | 106 ++ src/include/lean/io.h | 17 + src/include/lean/lean.h | 1788 ++++++++++++++++++++++++++ src/include/lean/memory.h | 27 + src/include/lean/mpq.h | 224 ++++ src/include/lean/mpz.h | 267 ++++ src/include/lean/object.h | 501 ++++++++ src/include/lean/optional.h | 155 +++ src/include/lean/platform.h | 12 + src/include/lean/serializer.h | 142 ++ src/include/lean/sstream.h | 19 + src/include/lean/stack_overflow.h | 25 + src/include/lean/stackinfo.h | 31 + src/include/lean/thread.h | 249 ++++ src/include/lean/utf8.h | 53 + 27 files changed, 4202 insertions(+) create mode 100644 src/include/lean/alloc.h create mode 100644 src/include/lean/allocprof.h create mode 100644 src/include/lean/apply.h create mode 100644 src/include/lean/compact.h create mode 100644 src/include/lean/compiler_hints.h create mode 100644 src/include/lean/debug.h create mode 100644 src/include/lean/exception.h create mode 100644 src/include/lean/extensible_object.h create mode 100644 src/include/lean/flet.h create mode 100644 src/include/lean/hash.h create mode 100644 src/include/lean/init_module.h create mode 100644 src/include/lean/int64.h create mode 100644 src/include/lean/interrupt.h create mode 100644 src/include/lean/io.h create mode 100644 src/include/lean/lean.h create mode 100644 src/include/lean/memory.h create mode 100644 src/include/lean/mpq.h create mode 100644 src/include/lean/mpz.h create mode 100644 src/include/lean/object.h create mode 100644 src/include/lean/optional.h create mode 100644 src/include/lean/platform.h create mode 100644 src/include/lean/serializer.h create mode 100644 src/include/lean/sstream.h create mode 100644 src/include/lean/stack_overflow.h create mode 100644 src/include/lean/stackinfo.h create mode 100644 src/include/lean/thread.h create mode 100644 src/include/lean/utf8.h diff --git a/src/include/lean/alloc.h b/src/include/lean/alloc.h new file mode 100644 index 0000000000..75276dff44 --- /dev/null +++ b/src/include/lean/alloc.h @@ -0,0 +1,16 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include + +namespace lean { +void init_thread_heap(); +void * alloc(size_t sz); +void dealloc(void * o, size_t sz); +void initialize_alloc(); +void finalize_alloc(); +} diff --git a/src/include/lean/allocprof.h b/src/include/lean/allocprof.h new file mode 100644 index 0000000000..8746c29cf1 --- /dev/null +++ b/src/include/lean/allocprof.h @@ -0,0 +1,29 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +namespace lean { +/* Low tech runtime allocation profiler. + We need to compile Lean using RUNTIME_STATS=ON to use it. */ +class allocprof { + std::ostream & m_out; + std::string m_msg; +#ifdef LEAN_RUNTIME_STATS + uint64 m_num_ctor; + uint64 m_num_closure; + uint64 m_num_string; + uint64 m_num_array; + uint64 m_num_thunk; + uint64 m_num_task; + uint64 m_num_ext; +#endif +public: + allocprof(std::ostream & out, char const * msg); + ~allocprof(); +}; +} diff --git a/src/include/lean/apply.h b/src/include/lean/apply.h new file mode 100644 index 0000000000..059173a226 --- /dev/null +++ b/src/include/lean/apply.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +namespace lean { +object * curry(void * f, unsigned n, object ** as); +} diff --git a/src/include/lean/compact.h b/src/include/lean/compact.h new file mode 100644 index 0000000000..7effcac520 --- /dev/null +++ b/src/include/lean/compact.h @@ -0,0 +1,81 @@ +/* +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include +#include + +namespace lean { +typedef lean_object * object_offset; + +class object_compactor { + struct max_sharing_table; + friend struct max_sharing_hash; + friend struct max_sharing_eq; + std::unordered_map, std::equal_to> m_obj_table; + std::unique_ptr m_max_sharing_table; + std::vector m_todo; + std::vector m_tmp; + void * m_begin; + void * m_end; + void * m_capacity; + size_t capacity() const { return static_cast(m_capacity) - static_cast(m_begin); } + void save(object * o, object * new_o); + void save_max_sharing(object * o, object * new_o, size_t new_o_sz); + void * alloc(size_t sz); + object_offset to_offset(object * o); + void insert_terminator(object * o); + object * copy_object(object * o); + bool insert_constructor(object * o); + bool insert_array(object * o); + void insert_sarray(object * o); + void insert_string(object * o); + bool insert_thunk(object * o); + bool insert_task(object * o); + bool insert_ref(object * o); + void insert_mpz(object * o); +public: + object_compactor(); + object_compactor(object_compactor const &) = delete; + object_compactor(object_compactor &&) = delete; + ~object_compactor(); + object_compactor operator=(object_compactor const &) = delete; + object_compactor operator=(object_compactor &&) = delete; + void operator()(object * o); + size_t size() const { return static_cast(m_end) - static_cast(m_begin); } + void const * data() const { return m_begin; } +}; + +class compacted_region { + void * m_begin; + void * m_next; + void * m_end; + mpz_object * m_nested_mpzs; + void move(size_t d); + void move(object * o); + object * fix_object_ptr(object * o); + void fix_constructor(object * o); + void fix_array(object * o); + void fix_thunk(object * o); + void fix_ref(object * o); + void fix_mpz(object * o); +public: + /* Creates a compacted object region using the given region in memory. + This object takes ownership of the region. */ + compacted_region(size_t sz, void * data); + /* Creates a compacted object region using the object_compactor current state. + It creates a copy of the compacted region generated by the object compactor. */ + explicit compacted_region(object_compactor const & c); + compacted_region(compacted_region const &) = delete; + compacted_region(compacted_region &&) = delete; + ~compacted_region(); + compacted_region operator=(compacted_region const &) = delete; + compacted_region operator=(compacted_region &&) = delete; + object * read(); +}; +} diff --git a/src/include/lean/compiler_hints.h b/src/include/lean/compiler_hints.h new file mode 100644 index 0000000000..05e2539082 --- /dev/null +++ b/src/include/lean/compiler_hints.h @@ -0,0 +1,17 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Gabriel Ebner +*/ +#pragma once + +#if defined(__GNUC__) || defined(__clang__) +#define LEAN_UNLIKELY(x) (__builtin_expect((x), 0)) +#define LEAN_LIKELY(x) (__builtin_expect((x), 1)) +#define LEAN_ALWAYS_INLINE __attribute__((always_inline)) +#else +#define LEAN_UNLIKELY(x) (x) +#define LEAN_LIKELY(x) (x) +#define LEAN_ALWAYS_INLINE +#endif diff --git a/src/include/lean/debug.h b/src/include/lean/debug.h new file mode 100644 index 0000000000..711a249ed3 --- /dev/null +++ b/src/include/lean/debug.h @@ -0,0 +1,129 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include + +#ifndef __has_builtin +#define __has_builtin(x) 0 +#endif + +#ifdef LEAN_DEBUG +#define DEBUG_CODE(CODE) CODE +#else +#define DEBUG_CODE(CODE) +#endif + +#define lean_unreachable() { DEBUG_CODE({lean::notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); lean::invoke_debugger();}) throw lean::unreachable_reached(); } + +#ifdef LEAN_DEBUG +#define lean_verify(COND) if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); } +#else +#define lean_verify(COND) (COND) +#endif + +// LEAN_NARG(ARGS...) return the number of arguments. +// This is a hack based on the following stackoverflow post: +// http://stackoverflow.com/questions/11317474/macro-to-count-number-of-arguments +#define LEAN_COMMASEQ_N() 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0 +#define LEAN_RSEQ_N() 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0 +#define LEAN_ARG_N(_1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, N, ...) N +#define LEAN_EXPAND(x) x +#ifdef _MSC_VER +#define LEAN_AUGMENT(...) dummy, __VA_ARGS__ +#define LEAN_NARG_1(...) LEAN_EXPAND(LEAN_ARG_N(__VA_ARGS__, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0)) +#define LEAN_NARG(...) LEAN_NARG_1(LEAN_AUGMENT(__VA_ARGS__)) +#else +#define LEAN_NARG_(ARGS...) LEAN_ARG_N(ARGS) +#define LEAN_HASCOMMA(ARGS...) LEAN_NARG_(ARGS, LEAN_COMMASEQ_N()) +#define LEAN_COMMA() , +#define LEAN_NARG_HELPER3_01(N) 0 +#define LEAN_NARG_HELPER3_00(N) 1 +#define LEAN_NARG_HELPER3_11(N) N +#define LEAN_NARG_HELPER2(a, b, N) LEAN_NARG_HELPER3_ ## a ## b(N) +#define LEAN_NARG_HELPER1(a, b, N) LEAN_NARG_HELPER2(a, b, N) +#define LEAN_NARG(ARGS...) LEAN_NARG_HELPER1(LEAN_HASCOMMA(ARGS), LEAN_HASCOMMA(LEAN_COMMA ARGS ()), LEAN_NARG_(ARGS, LEAN_RSEQ_N())) +#endif + +// Hack for LEAN_DISPLAY(ARGS...) +// It works for at most 16 arguments. +#define LEAN_DISPLAY1_CORE(V) lean::debug::display_var(#V, V); +#define LEAN_DISPLAY2_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY1_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY3_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY2_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY4_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY3_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY5_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY4_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY6_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY5_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY7_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY6_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY8_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY7_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY9_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY8_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY10_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY9_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY11_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY10_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY12_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY11_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY13_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY12_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY14_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY13_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY15_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY14_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY16_CORE(V, ...) lean::debug::display_var(#V, V); LEAN_EXPAND(LEAN_DISPLAY15_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY0(...) +#define LEAN_DISPLAY1(ARG) std::cerr << "Argument\n"; LEAN_DISPLAY1_CORE(ARG) +#define LEAN_DISPLAY2(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY2_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY3(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY3_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY4(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY4_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY5(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY5_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY6(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY6_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY7(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY7_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY8(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY8_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY9(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY9_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY10(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY10_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY11(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY11_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY12(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY12_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY13(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY13_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY14(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY14_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY15(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY15_CORE(__VA_ARGS__)) +#define LEAN_DISPLAY16(...) std::cerr << "Arguments\n"; LEAN_EXPAND(LEAN_DISPLAY16_CORE(__VA_ARGS__)) +#define LEAN_JOIN0(A, B) A ## B +#define LEAN_JOIN(A, B) LEAN_JOIN0(A, B) +#define LEAN_DISPLAY(...) { LEAN_JOIN(LEAN_DISPLAY, LEAN_NARG(__VA_ARGS__))(__VA_ARGS__) } + +#define lean_assert(COND, ...) DEBUG_CODE({if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean::invoke_debugger(); }}) +#define lean_cond_assert(TAG, COND, ...) DEBUG_CODE({if (lean::is_debug_enabled(TAG) && LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean::invoke_debugger(); }}) +#define lean_always_assert(COND, ...) { if (LEAN_UNLIKELY(!(COND))) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); LEAN_DISPLAY(__VA_ARGS__); lean_unreachable(); } } + +#define lean_assert_eq(A, B) lean_assert(A == B, A, B) +#define lean_assert_ne(A, B) lean_assert(A != B, A, B) +#define lean_assert_gt(A, B) lean_assert(A > B, A, B) +#define lean_assert_lt(A, B) lean_assert(A < B, A, B) +#define lean_assert_ge(A, B) lean_assert(A >= B, A, B) +#define lean_assert_le(A, B) lean_assert(A <= B, A, B) + +namespace lean { +void initialize_debug(); +void finalize_debug(); +void notify_assertion_violation(char const * file_name, int line, char const * condition); +void enable_debug(char const * tag); +void disable_debug(char const * tag); +bool is_debug_enabled(char const * tag); +void invoke_debugger(); +bool has_violations(); +void enable_debug_dialog(bool flag); +// LCOV_EXCL_START +/** \brief Exception used to sign that unreachable code was reached */ +class unreachable_reached : public exception { +public: + unreachable_reached() {} + virtual ~unreachable_reached() noexcept {} + virtual char const * what() const noexcept { return "'unreachable' code was reached"; } +}; +namespace debug { +template void display_var(char const * name, T const & value) { + // commented typeid(value).name() since the name is mangled + std::cerr << name << /* " : " << typeid(value).name() << */ " := " + << std::boolalpha << value << std::noboolalpha + << std::endl; } +} +// LCOV_EXCL_STOP +} diff --git a/src/include/lean/exception.h b/src/include/lean/exception.h new file mode 100644 index 0000000000..ed4fb4fa3f --- /dev/null +++ b/src/include/lean/exception.h @@ -0,0 +1,67 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include + +namespace lean { +class sstream; +/** \brief Base class for all Lean exceptions */ +class throwable : public std::exception { +protected: + std::string m_msg; + throwable() {} +public: + throwable(char const * msg); + throwable(std::string const & msg); + throwable(sstream const & strm); + virtual ~throwable() noexcept; + virtual char const * what() const noexcept; +}; + +/** \brief Base class for all Lean "logical" exceptions, that is, exceptions not related + to resource constraints, and runtime errors */ +class exception : public throwable { +protected: + exception() {} +public: + exception(char const * msg):throwable(msg) {} + exception(std::string const & msg):throwable(msg) {} + exception(sstream const & strm):throwable(strm) {} +}; + +/** \brief Exception used to sign that a computation was interrupted */ +class interrupted { +public: + interrupted() {} + virtual ~interrupted() noexcept {} + virtual char const * what() const noexcept { return "interrupted"; } +}; + +class stack_space_exception : public throwable { + std::string m_msg; + stack_space_exception(std::string const & msg):m_msg(msg) {} +public: + stack_space_exception(char const * component_name); + virtual char const * what() const noexcept { return m_msg.c_str(); } +}; + +class memory_exception : public throwable { + std::string m_msg; + memory_exception(std::string const & msg):m_msg(msg) {} +public: + memory_exception(char const * component_name); + virtual char const * what() const noexcept { return m_msg.c_str(); } +}; + +class heartbeat_exception : public throwable { +public: + heartbeat_exception() {} + virtual char const * what() const noexcept; +}; +} diff --git a/src/include/lean/extensible_object.h b/src/include/lean/extensible_object.h new file mode 100644 index 0000000000..8ef7567e2a --- /dev/null +++ b/src/include/lean/extensible_object.h @@ -0,0 +1,87 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include +#include +namespace lean { +/* + TODO(Leo): remove this file after we finish converting the code to `object`. + This file is needed because we had custom serializers for name/level/expr. + After we implement them using `object`, we can use the `object` serializer. +*/ + +/** + \brief Template for creating objects that can be attached to "extensions". +*/ +template +class extensible_object : public T { +public: + class extension { + friend class extensible_object; + extensible_object * m_owner; + public: + extension():m_owner(nullptr) {} + virtual ~extension() {} + extensible_object & get_owner() { return *m_owner; } + }; +private: + std::vector> m_extensions; +public: + template + extensible_object(Args &&... args):T(std::forward(args)...) {} + + typedef std::unique_ptr (*mk_extension)(); + + class extension_factory { + std::vector m_makers; + mutex m_makers_mutex; + public: + unsigned register_extension(mk_extension mk) { + lock_guard lock(m_makers_mutex); + unsigned r = m_makers.size(); + m_makers.push_back(mk); + return r; + } + + std::unique_ptr mk(unsigned extid) { + lock_guard lock(m_makers_mutex); + return m_makers[extid](); + } + }; + + static extension_factory * g_extension_factory; + static void initialize() { g_extension_factory = new extension_factory(); } + static void finalize() { delete g_extension_factory; } + static extension_factory & get_extension_factory() { return *g_extension_factory; } + + static unsigned register_extension(mk_extension mk) { + return get_extension_factory().register_extension(mk); + } + + extension & get_extension_core(unsigned extid) { + if (extid >= m_extensions.size()) + m_extensions.resize(extid+1); + if (!m_extensions[extid]) { + std::unique_ptr ext = get_extension_factory().mk(extid); + ext->m_owner = this; + m_extensions[extid].swap(ext); + } + return *(m_extensions[extid].get()); + } + + template Ext & get_extension(unsigned extid) { + extension & ext = get_extension_core(extid); + lean_assert(dynamic_cast(&ext) != nullptr); + return static_cast(ext); + } +}; +template +typename extensible_object::extension_factory * +extensible_object::g_extension_factory = nullptr; +} diff --git a/src/include/lean/flet.h b/src/include/lean/flet.h new file mode 100644 index 0000000000..f73cd082d7 --- /dev/null +++ b/src/include/lean/flet.h @@ -0,0 +1,33 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +namespace lean { +/** + \brief Template for simulating "fluid-lets". + Example: + { + flet l(m_field, 1); // set the value of m_field to 1 + + } // restore original value of m_field + +*/ +template +class flet { + T & m_ref; + T m_old_value; +public: + flet(T & ref, T const & new_value): + m_ref(ref), + m_old_value(ref) { + m_ref = new_value; + } + ~flet() { + m_ref = m_old_value; + } +}; +} diff --git a/src/include/lean/hash.h b/src/include/lean/hash.h new file mode 100644 index 0000000000..1d4a996a2a --- /dev/null +++ b/src/include/lean/hash.h @@ -0,0 +1,91 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include + +namespace lean { + +void mix(unsigned & a, unsigned & b, unsigned & c); + +unsigned hash_str(size_t len, char const * str, unsigned init_value); + +inline unsigned hash(unsigned h1, unsigned h2) { + h2 -= h1; h2 ^= (h1 << 8); + h1 -= h2; h2 ^= (h1 << 16); + h2 -= h1; h2 ^= (h1 << 10); + return h2; +} + +inline uint64 hash(uint64 h1, uint64 h2) { + h2 -= h1; h2 ^= (h1 << 16); + h1 -= h2; h2 ^= (h1 << 32); + h2 -= h1; h2 ^= (h1 << 20); + return h2; +} + +inline unsigned hash_ptr(void const * ptr) { +#if UINTPTR_MAX == 0xffffffff + /* 32-bit version */ + return reinterpret_cast(ptr); +#else + /* 64-bit version */ + size_t r = reinterpret_cast(ptr); + return hash(static_cast(r >> 32), static_cast(r)); +#endif +} + +template +unsigned hash(unsigned n, H h, unsigned init_value = 31) { + unsigned a, b, c; + if (n == 0) + return init_value; + + a = b = 0x9e3779b9; + c = 11; + + switch (n) { + case 1: + a += init_value; + b = h(0); + mix(a, b, c); + return c; + case 2: + a += init_value; + b += h(0); + c += h(1); + mix(a, b, c); + return c; + case 3: + a += h(0); + b += h(1); + c += h(2); + mix(a, b, c); + a += init_value; + mix(a, b, c); + return c; + default: + while (n >= 3) { + n--; + a += h(n); + n--; + b += h(n); + n--; + c += h(n); + mix(a, b, c); + } + + a += init_value; + switch (n) { + case 2: b += h(1); /* fall-thru */ + case 1: c += h(0); + } + mix(a, b, c); + return c; + } +} +} diff --git a/src/include/lean/init_module.h b/src/include/lean/init_module.h new file mode 100644 index 0000000000..b28dfb4cd2 --- /dev/null +++ b/src/include/lean/init_module.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +namespace lean { +void initialize_runtime_module(); +void finalize_runtime_module(); +} diff --git a/src/include/lean/int64.h b/src/include/lean/int64.h new file mode 100644 index 0000000000..47f6ef33dc --- /dev/null +++ b/src/include/lean/int64.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +namespace lean { +typedef int64_t int64; +typedef uint64_t uint64; +static_assert(sizeof(int64) == 8, "unexpected int64 size"); // NOLINT +static_assert(sizeof(uint64) == 8, "unexpected uint64 size"); // NOLINT +} diff --git a/src/include/lean/interrupt.h b/src/include/lean/interrupt.h new file mode 100644 index 0000000000..89ca2d1f36 --- /dev/null +++ b/src/include/lean/interrupt.h @@ -0,0 +1,106 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include +#include +#include + +namespace lean { +/** \brief Increment thread local counter for approximating elapsed time. */ +void inc_heartbeat(); + +/** \brief Reset thread local counter for approximating elapsed time. */ +void reset_heartbeat(); + +/* Update the current heartbeat */ +class scope_heartbeat : flet { +public: + scope_heartbeat(size_t curr); +}; + +/** \brief Threshold on the number of hearbeats. check_system will throw + an exception if a thread exceeds the limit. The default is unlimited. + The limit is checked in the check_system API. + + This is a thread local value. The class lthread uses the + maximum of the parent thread. */ +void set_max_heartbeat(size_t max); +void set_max_heartbeat_thousands(unsigned max); +size_t get_max_heartbeat(); + +/* Update the thread local max heartbeat */ +class scope_max_heartbeat : flet { +public: + scope_max_heartbeat(size_t max); +}; + +void check_heartbeat(); + +struct scoped_interrupt_flag : flet { + scoped_interrupt_flag(atomic_bool *); // NOLINT +}; + +/** + \brief Throw an interrupted exception if the (interrupt) flag is set. +*/ +void check_interrupted(); + +/** + \brief Check system resources: stack, memory, hearbeat, interrupt flag. +*/ +void check_system(char const * component_name); + +constexpr unsigned g_small_sleep = 10; + +/** + \brief Put the current thread to sleep for \c ms milliseconds. + + \remark check_interrupted is invoked every \c step_ms milliseconds; +*/ +void sleep_for(unsigned ms, unsigned step_ms = g_small_sleep); +inline void sleep_for(chrono::milliseconds const & ms) { sleep_for(ms.count(), 10); } + +/** + \brief Thread that provides a method for setting its interrupt flag. +*/ +class interruptible_thread { +public: + template + interruptible_thread(Function && fun): + m_thread([&, fun]() { + save_stack_info(false); + scoped_interrupt_flag scope_int_flag(&m_flag); + fun(); + }) + {} + + /** + \brief Return true iff an interrupt request has been made to the current thread. + */ + bool interrupted() const; + /** + \brief Send a interrupt request to the current thread. Return + true iff the request has been successfully performed. + */ + void request_interrupt(); + + void join(); +private: + atomic_bool m_flag; + lthread m_thread; +}; + +#if !defined(LEAN_MULTI_THREAD) +inline void check_threadsafe() { + throw exception("Lean was compiled without support for multi-threading"); +} +#else +inline void check_threadsafe() {} +#endif +} diff --git a/src/include/lean/io.h b/src/include/lean/io.h new file mode 100644 index 0000000000..46103c78ef --- /dev/null +++ b/src/include/lean/io.h @@ -0,0 +1,17 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +namespace lean { +obj_res set_io_result(obj_arg a); +obj_res set_io_error(obj_arg e); +obj_res set_io_error(char const * msg); +obj_res set_io_error(std::string const & msg); +void initialize_io(); +void finalize_io(); +} diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h new file mode 100644 index 0000000000..9425f00ecb --- /dev/null +++ b/src/include/lean/lean.h @@ -0,0 +1,1788 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include +#include +#include +#include +#if !defined(__APPLE__) +#include +#endif + +#ifdef __cplusplus +#include +#define _Atomic(t) std::atomic +#define LEAN_USING_STD using namespace std; /* NOLINT */ +extern "C" { +#else +#include +#define LEAN_USING_STD +#endif +#include + +#define LEAN_CLOSURE_MAX_ARGS 16 +#define LEAN_OBJECT_SIZE_DELTA 8 +#define LEAN_MAX_SMALL_OBJECT_SIZE 512 + +#ifdef _MSC_VER +#define LEAN_ALLOCA(s) _alloca(s) +#else +#define LEAN_ALLOCA(s) alloca(s) +#endif + +#if defined(__GNUC__) || defined(__clang__) +#define LEAN_UNLIKELY(x) (__builtin_expect((x), 0)) +#define LEAN_LIKELY(x) (__builtin_expect((x), 1)) +#define LEAN_ALWAYS_INLINE __attribute__((always_inline)) +#else +#define LEAN_UNLIKELY(x) (x) +#define LEAN_LIKELY(x) (x) +#define LEAN_ALWAYS_INLINE +#endif + +#ifdef LEAN_RUNTIME_STATS +#define LEAN_RUNTIME_STAT_CODE(c) c +#else +#define LEAN_RUNTIME_STAT_CODE(c) +#endif + +#define LEAN_BYTE(Var, Index) *(((uint8_t*)&Var)+Index) + +#define LeanMaxCtorTag 244 +#define LeanClosure 245 +#define LeanArray 246 +#define LeanStructArray 247 +#define LeanScalarArray 248 +#define LeanString 249 +#define LeanMPZ 250 +#define LeanThunk 251 +#define LeanTask 252 +#define LeanRef 253 +#define LeanExternal 254 +#define LeanReserved 255 + +static inline bool lean_is_big_object_tag(uint8_t tag) { + return tag == LeanArray || tag == LeanStructArray || tag == LeanScalarArray || tag == LeanString; +} + +#define LEAN_CASSERT(predicate) LEAN_impl_CASSERT_LINE(predicate, __LINE__, __FILE__) + +#define LEAN_impl_PASTE(a, b) a##b +#define LEAN_impl_CASSERT_LINE(predicate, line, file) \ + typedef char LEAN_impl_PASTE(assertion_failed_##file##_, line)[2*!!(predicate)-1]; + +LEAN_CASSERT(sizeof(size_t) == sizeof(void*)); + +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) +/* Compressed headers are only supported in 64-bit machines */ +LEAN_CASSERT(sizeof(void*) == 8); +#endif + +/* Lean object header */ +typedef struct { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) + /* (high) 8-bits : tag + 8-bits : num fields for constructors, element size for scalar arrays + 1-bit : single-threaded + 1-bit : multi-threaded + 1-bit : persistent + (low) 45-bits : RC */ + size_t m_header; +#define LEAN_RC_NBITS 45 +#define LEAN_PERSISTENT_BIT 45 +#define LEAN_MT_BIT 46 +#define LEAN_ST_BIT 47 +#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + /* (high) 8-bits : tag + 8-bits : num fields for constructors, element size for scalar arrays + 8-bits : memory kind + 8-bits : + (low) 32-bits : RC */ + size_t m_header; +#define LEAN_RC_NBITS 32 +#define LEAN_ST_MEM_KIND 0 +#define LEAN_MT_MEM_KIND 1 +#define LEAN_PERSISTENT_MEM_KIND 2 +#define LEAN_OTHER_MEM_KIND 3 +#else + size_t m_rc; + uint8_t m_tag; + uint8_t m_mem_kind; + uint16_t m_other; /* num fields for constructors, element size for scalar arrays, etc. */ +#define LEAN_ST_MEM_KIND 0 +#define LEAN_MT_MEM_KIND 1 +#define LEAN_PERSISTENT_MEM_KIND 2 +#define LEAN_OTHER_MEM_KIND 3 +#endif +} lean_object; + +/* +In our runtime, a Lean function consume the reference counter (RC) of its argument or not. +We say this behavior is part of the "calling convention" for the function. We say an argument uses: + +1- "standard" calling convention if it consumes/decrements the RC. + In this calling convention each argument should be viewed as a resource that is consumed by the function. + This is roughly equivalent to `S && a` in C++, where `S` is a smart pointer, and `a` is the argument. + When this calling convention is used for an argument `x`, then it is safe to perform destructive updates to + `x` if its RC is 1. + +2- "borrowed" calling convention if it doesn't consume/decrement the RC, and it is the responsability of the caller + to decrement the RC. + This is roughly equivalent to `S const & a` in C++, where `S` is a smart pointer, and `a` is the argument. + +For returning objects, we also have two conventions + +1- "standard" result. The caller is responsible for consuming the RC of the result. + This is roughly equivalent to returning a smart point `S` by value in C++. + +2- "borrowed" result. The caller is not responsible for decreasing the RC. + This is roughly equivalent to returning a smart point reference `S const &` in C++. + +Functions stored in closures use the "standard" calling convention. +*/ + +/* The following typedef's are used to document the calling convention for the primitives. */ +typedef lean_object * lean_obj_arg; /* Standard object argument. */ +typedef lean_object * b_lean_obj_arg; /* Borrowed object argument. */ +typedef lean_object * u_lean_obj_arg; /* Unique (aka non shared) object argument. */ +typedef lean_object * lean_obj_res; /* Standard object result. */ +typedef lean_object * b_lean_obj_res; /* Borrowed object result. */ + +typedef struct { + lean_object m_header; + lean_object * m_objs[0]; +} lean_ctor_object; + +/* Array arrays */ +typedef struct { + lean_object m_header; + size_t m_size; + size_t m_capacity; + lean_object * m_data[0]; +} lean_array_object; + +/* Scalar arrays */ +typedef struct { + lean_object m_header; + size_t m_size; + size_t m_capacity; + uint8_t m_data[0]; +} lean_sarray_object; + +typedef struct { + lean_object m_header; + size_t m_size; /* byte length including '\0' terminator */ + size_t m_capacity; + size_t m_length; /* UTF8 length */ + char m_data[0]; +} lean_string_object; + +typedef struct { + lean_object m_header; + void * m_fun; + uint16_t m_arity; /* Number of arguments expected by m_fun. */ + uint16_t m_num_fixed; /* Number of arguments that have been already fixed. */ + lean_object * m_objs[0]; +} lean_closure_object; + +typedef struct { + lean_object m_header; + lean_object * m_value; +} lean_ref_object; + +typedef struct { + lean_object m_header; + _Atomic(lean_object *) m_value; + _Atomic(lean_object *) m_closure; +} lean_thunk_object; + +struct lean_task; + +/* Data required for executing a Lean task. It is released as soon as + the task terminates. */ +typedef struct { + lean_object * m_closure; + struct lean_task * m_head_dep; + struct lean_task * m_next_dep; + unsigned m_prio; + uint8_t m_interrupted; + uint8_t m_deleted; +} lean_task_imp; + +typedef struct lean_task { + lean_object m_header; + _Atomic(lean_object *) m_value; + lean_task_imp * m_imp; +} lean_task_object; + +typedef void (*lean_external_finalize_proc)(void *); +typedef void (*lean_external_foreach_proc)(void *, b_lean_obj_arg); + +typedef struct { + lean_external_finalize_proc m_finalize; + lean_external_foreach_proc m_foreach; +} lean_external_class; + +lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc); + +/* Object for wrapping external data. */ +typedef struct { + lean_object m_header; + lean_external_class * m_class; + void * m_data; +} lean_external_object; + +static inline bool lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) == 1; } +static inline lean_object * lean_box(size_t n) { return (lean_object*)(((size_t)(n) << 1) | 1); } +static inline size_t lean_unbox(lean_object * o) { return (size_t)(o) >> 1; } + +void lean_set_exit_on_panic(bool flag); +lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg); + +__attribute__((noreturn)) void lean_panic(char const * msg); +__attribute__((noreturn)) void lean_panic_out_of_memory(); +__attribute__((noreturn)) void lean_panic_unreachable(); +__attribute__((noreturn)) void lean_panic_rc_overflow(); + +static inline size_t lean_align(size_t v, size_t a) { + return (v / a)*a + a * (v % a != 0); +} + +static inline unsigned lean_get_slot_idx(unsigned sz) { + assert(sz > 0); + assert(lean_align(sz, LEAN_OBJECT_SIZE_DELTA) == sz); + return sz / LEAN_OBJECT_SIZE_DELTA - 1; +} + +void * lean_alloc_small(unsigned sz, unsigned slot_idx); +void lean_free_small(void * p); +unsigned lean_small_mem_size(void * p); + +static inline lean_object * lean_alloc_small_object(unsigned sz) { +#ifdef LEAN_SMALL_ALLOCATOR + sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA); + unsigned slot_idx = lean_get_slot_idx(sz); + assert(sz <= LEAN_MAX_SMALL_OBJECT_SIZE); + return (lean_object*)lean_alloc_small(sz, slot_idx); +#else + void * mem = malloc(sizeof(size_t) + sz); + if (mem == 0) lean_panic_out_of_memory(); + *(size_t*)mem = sz; + return (lean_object*)((size_t*)mem + 1); +#endif +} + +static inline lean_object * lean_alloc_ctor_memory(unsigned sz) { +#ifdef LEAN_SMALL_ALLOCATOR + unsigned sz1 = lean_align(sz, LEAN_OBJECT_SIZE_DELTA); + unsigned slot_idx = lean_get_slot_idx(sz1); + assert(sz1 <= LEAN_MAX_SMALL_OBJECT_SIZE); + lean_object* r = (lean_object*)lean_alloc_small(sz1, slot_idx); + if (sz1 > sz) { + /* Initialize last word. + In our runtime `lean_object_byte_size` is always + a multiple of the machine word size for constructors. + + By setting the last word to 0, we make sure the sharing + maximizer procedures at `maxsharing.cpp` and `compact.cpp` are + not affected by uninitialized data at the (sz1 - sz) last bytes. + Otherwise, we may mistakenly assume to structurally equal + objects are not identical because of this uninitialized memory. */ + size_t * end = (size_t*)(((char*)r) + sz1); + end[-1] = 0; + } + return r; +#else + return lean_alloc_small_object(sz); +#endif +} + +static inline unsigned lean_small_object_size(lean_object * o) { +#ifdef LEAN_SMALL_ALLOCATOR + return lean_small_mem_size(o); +#else + return *((size_t*)o - 1); +#endif +} + +static inline void lean_free_small_object(lean_object * o) { +#ifdef LEAN_SMALL_ALLOCATOR + lean_free_small(o); +#else + free((size_t*)o - 1); +#endif +} + +lean_object * lean_alloc_object(size_t sz); +void lean_free_object(lean_object * o); + +static inline uint8_t lean_ptr_tag(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + return LEAN_BYTE(o->m_header, 7); +#else + return o->m_tag; +#endif +} + +static inline unsigned lean_ptr_other(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + return LEAN_BYTE(o->m_header, 6); +#else + return o->m_other; +#endif +} + +/* The object size may be slightly bigger for constructor objects. + The runtime does not track the size of the scalar size area. + All constructor objects are "small", and allocated into pages. + We retrieve their size by accessing the page header. The size of + small objects is a multiple of LEAN_OBJECT_SIZE_DELTA */ +size_t lean_object_byte_size(lean_object * o); + +static inline bool lean_is_mt(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) + return ((o->m_header >> LEAN_MT_BIT) & 1) != 0; +#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + return LEAN_BYTE(o->m_header, 5) == LEAN_MT_MEM_KIND; +#else + return o->m_mem_kind == LEAN_MT_MEM_KIND; +#endif +} + +static inline bool lean_is_st(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) + return ((o->m_header >> LEAN_ST_BIT) & 1) != 0; +#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + return LEAN_BYTE(o->m_header, 5) == LEAN_ST_MEM_KIND; +#else + return o->m_mem_kind == LEAN_ST_MEM_KIND; +#endif +} + +static inline bool lean_is_persistent(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) + return ((o->m_header >> LEAN_PERSISTENT_BIT) & 1) != 0; +#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + return LEAN_BYTE(o->m_header, 5) == LEAN_PERSISTENT_MEM_KIND; +#else + return o->m_mem_kind == LEAN_PERSISTENT_MEM_KIND; +#endif +} + +static inline bool lean_has_rc(lean_object * o) { + return lean_is_st(o) || lean_is_mt(o); +} + +static inline _Atomic(size_t) * lean_get_rc_mt_addr(lean_object* o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + return (_Atomic(size_t)*)(&(o->m_header)); +#else + return (_Atomic(size_t)*)(&(o->m_rc)); +#endif +} + +static inline void lean_inc_ref(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) + if (LEAN_LIKELY(lean_is_st(o))) { + o->m_header++; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_relaxed); + } +#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + if (LEAN_LIKELY(lean_is_st(o))) { + o->m_header++; + #ifdef LEAN_CHECK_RC_OVERFLOW + if (LEAN_UNLIKELY(((uint32_t)o->m_header) == 0)) { + lean_panic_rc_overflow(); + } + #endif + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + #ifdef LEAN_CHECK_RC_OVERFLOW + uint32_t old_rc = (uint32_t) + #endif + atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_relaxed); + #ifdef LEAN_CHECK_RC_OVERFLOW + if (LEAN_UNLIKELY(old_rc + 1 == 0)) { + lean_panic_rc_overflow(); + } + #endif + } +#else + if (LEAN_LIKELY(lean_is_st(o))) { + o->m_rc++; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_relaxed); + } +#endif +} + +static inline void lean_inc_ref_n(lean_object * o, size_t n) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) + if (LEAN_LIKELY(lean_is_st(o))) { + o->m_header += n; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed); + } +#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + if (LEAN_LIKELY(lean_is_st(o))) { + o->m_header += n; + #ifdef LEAN_CHECK_RC_OVERFLOW + if (LEAN_UNLIKELY(((uint32_t)o->m_header) < n)) { + lean_panic_rc_overflow(); + } + #endif + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + #ifdef LEAN_CHECK_RC_OVERFLOW + uint32_t old_rc = (uint32_t) + #endif + atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed); + #ifdef LEAN_CHECK_RC_OVERFLOW + if (LEAN_UNLIKELY(old_rc + n < n)) { + lean_panic_rc_overflow(); + } + #endif + } +#else + if (LEAN_LIKELY(lean_is_st(o))) { + o->m_rc += n; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed); + } +#endif +} + +static inline bool lean_dec_ref_core(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + if (LEAN_LIKELY(lean_is_st(o))) { + o->m_header--; + return ((o->m_header) & ((1ull << LEAN_RC_NBITS) - 1)) == 0; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + return (atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_acq_rel) & ((1ull << LEAN_RC_NBITS) - 1)) == 1; + } else { + return false; + } +#else + if (LEAN_LIKELY(lean_is_st(o))) { + o->m_rc--; + return o->m_rc == 0; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + return atomic_fetch_sub_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_acq_rel) == 1; + } else { + return false; + } +#endif +} + +/* Generic Lean object delete operation. */ +void lean_del(lean_object * o); + +static inline void lean_dec_ref(lean_object * o) { if (lean_dec_ref_core(o)) lean_del(o); } +static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); } +static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o)) lean_inc_ref_n(o, n); } +static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); } + +/* Just free memory */ +void lean_dealloc(lean_object * o); + +static inline bool lean_is_ctor(lean_object * o) { return lean_ptr_tag(o) <= LeanMaxCtorTag; } +static inline bool lean_is_closure(lean_object * o) { return lean_ptr_tag(o) == LeanClosure; } +static inline bool lean_is_array(lean_object * o) { return lean_ptr_tag(o) == LeanArray; } +static inline bool lean_is_sarray(lean_object * o) { return lean_ptr_tag(o) == LeanScalarArray; } +static inline bool lean_is_string(lean_object * o) { return lean_ptr_tag(o) == LeanString; } +static inline bool lean_is_mpz(lean_object * o) { return lean_ptr_tag(o) == LeanMPZ; } +static inline bool lean_is_thunk(lean_object * o) { return lean_ptr_tag(o) == LeanThunk; } +static inline bool lean_is_task(lean_object * o) { return lean_ptr_tag(o) == LeanTask; } +static inline bool lean_is_external(lean_object * o) { return lean_ptr_tag(o) == LeanExternal; } +static inline bool lean_is_ref(lean_object * o) { return lean_ptr_tag(o) == LeanRef; } + +static inline unsigned lean_obj_tag(lean_object * o) { + if (lean_is_scalar(o)) return lean_unbox(o); else return lean_ptr_tag(o); +} + +static inline lean_ctor_object * lean_to_ctor(lean_object * o) { assert(lean_is_ctor(o)); return (lean_ctor_object*)(o); } +static inline lean_closure_object * lean_to_closure(lean_object * o) { assert(lean_is_closure(o)); return (lean_closure_object*)(o); } +static inline lean_array_object * lean_to_array(lean_object * o) { assert(lean_is_array(o)); return (lean_array_object*)(o); } +static inline lean_sarray_object * lean_to_sarray(lean_object * o) { assert(lean_is_sarray(o)); return (lean_sarray_object*)(o); } +static inline lean_string_object * lean_to_string(lean_object * o) { assert(lean_is_string(o)); return (lean_string_object*)(o); } +static inline lean_thunk_object * lean_to_thunk(lean_object * o) { assert(lean_is_thunk(o)); return (lean_thunk_object*)(o); } +static inline lean_task_object * lean_to_task(lean_object * o) { assert(lean_is_task(o)); return (lean_task_object*)(o); } +static inline lean_ref_object * lean_to_ref(lean_object * o) { assert(lean_is_ref(o)); return (lean_ref_object*)(o); } +static inline lean_external_object * lean_to_external(lean_object * o) { assert(lean_is_external(o)); return (lean_external_object*)(o); } + +static inline bool lean_is_exclusive(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + if (LEAN_LIKELY(lean_is_st(o))) { + return ((o->m_header) & ((1ull << LEAN_RC_NBITS) - 1)) == 1; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + return (atomic_load_explicit(lean_get_rc_mt_addr(o), memory_order_acquire) & ((1ull << LEAN_RC_NBITS) - 1)) == 1; + } else { + return false; + } +#else + if (LEAN_LIKELY(lean_is_st(o))) { + return o->m_rc == 1; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + return atomic_load_explicit(lean_get_rc_mt_addr(o), memory_order_acquire) == 1; + } else { + return false; + } +#endif +} + +static inline bool lean_is_shared(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + if (LEAN_LIKELY(lean_is_st(o))) { + return ((o->m_header) & ((1ull << LEAN_RC_NBITS) - 1)) > 1; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + return (atomic_load_explicit(lean_get_rc_mt_addr(o), memory_order_acquire) & ((1ull << LEAN_RC_NBITS) - 1)) > 1; + } else { + return false; + } +#else + if (LEAN_LIKELY(lean_is_st(o))) { + return o->m_rc > 1; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + return atomic_load_explicit(lean_get_rc_mt_addr(o), memory_order_acquire) > 1; + } else { + return false; + } +#endif +} + +static inline bool lean_nonzero_rc(lean_object * o) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + if (LEAN_LIKELY(lean_is_st(o))) { + return ((o->m_header) & ((1ull << LEAN_RC_NBITS) - 1)) > 0; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + return (atomic_load_explicit(lean_get_rc_mt_addr(o), memory_order_acquire) & ((1ull << LEAN_RC_NBITS) - 1)) > 0; + } else { + return false; + } +#else + if (LEAN_LIKELY(lean_is_st(o))) { + return o->m_rc > 0; + } else if (lean_is_mt(o)) { + LEAN_USING_STD; + return atomic_load_explicit(lean_get_rc_mt_addr(o), memory_order_acquire) > 0; + } else { + return false; + } +#endif +} + +void lean_mark_mt(lean_object * o); +void lean_mark_persistent(lean_object * o); + +static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) { +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) + o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | (1ull << LEAN_ST_BIT) | 1; +#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | ((size_t)LEAN_ST_MEM_KIND << 40) | 1; +#else + o->m_rc = 1; + o->m_tag = tag; + o->m_mem_kind = LEAN_ST_MEM_KIND; + o->m_other = other; +#endif +} + +/* Remark: we don't need a reference counter for objects that are not stored in the heap. + Thus, we use the area to store the object size for small objects. */ +static inline void lean_set_non_heap_header(lean_object * o, size_t sz, unsigned tag, unsigned other) { + assert(sz > 0); + assert(sz < (1ull << 45)); + assert(sz == 1 || !lean_is_big_object_tag(tag)); +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) + o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | sz; +#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + o->m_header = ((size_t)(tag) << 56) | ((size_t)(other) << 48) | ((size_t)LEAN_OTHER_MEM_KIND << 40) | sz; +#else + o->m_rc = sz; + o->m_tag = tag; + o->m_mem_kind = LEAN_OTHER_MEM_KIND; + o->m_other = other; +#endif +} + +/* `lean_set_non_heap_header` for (potentially) big objects such as arrays and strings. */ +static inline void lean_set_non_heap_header_for_big(lean_object * o, unsigned tag, unsigned other) { + lean_set_non_heap_header(o, 1, tag, other); +} + +/* Constructor objects */ + +static inline unsigned lean_ctor_num_objs(lean_object * o) { + assert(lean_is_ctor(o)); + return lean_ptr_other(o); +} + +static inline lean_object ** lean_ctor_obj_cptr(lean_object * o) { + assert(lean_is_ctor(o)); + return lean_to_ctor(o)->m_objs; +} + +static inline uint8_t * lean_ctor_scalar_cptr(lean_object * o) { + assert(lean_is_ctor(o)); + return (uint8_t*)(lean_ctor_obj_cptr(o) + lean_ctor_num_objs(o)); +} + +static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) { + assert(tag <= LeanMaxCtorTag && num_objs < 256 && scalar_sz < 1024); + lean_object * o = lean_alloc_ctor_memory(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz); + lean_set_st_header(o, tag, num_objs); + return o; +} + +static inline b_lean_obj_res lean_ctor_get(b_lean_obj_arg o, unsigned i) { + assert(i < lean_ctor_num_objs(o)); + return lean_ctor_obj_cptr(o)[i]; +} + +static inline void lean_ctor_set(b_lean_obj_arg o, unsigned i, lean_obj_arg v) { + assert(i < lean_ctor_num_objs(o)); + lean_ctor_obj_cptr(o)[i] = v; +} + +static inline void lean_ctor_set_tag(b_lean_obj_arg o, uint8_t new_tag) { + assert(new_tag <= LeanMaxCtorTag); +#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC) + LEAN_BYTE(o->m_header, 7) = new_tag; +#else + o->m_tag = new_tag; +#endif +} + +static inline void lean_ctor_release(b_lean_obj_arg o, unsigned i) { + assert(i < lean_ctor_num_objs(o)); + lean_object ** objs = lean_ctor_obj_cptr(o); + lean_dec(objs[i]); + objs[i] = lean_box(0); +} + +static inline size_t lean_ctor_get_usize(b_lean_obj_arg o, unsigned i) { + assert(i >= lean_ctor_num_objs(o)); + return *((size_t*)(lean_ctor_obj_cptr(o) + i)); +} + +static inline uint8_t lean_ctor_get_uint8(b_lean_obj_arg o, unsigned offset) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + return *((uint8_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); +} + +static inline uint16_t lean_ctor_get_uint16(b_lean_obj_arg o, unsigned offset) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + return *((uint16_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); +} + +static inline uint32_t lean_ctor_get_uint32(b_lean_obj_arg o, unsigned offset) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + return *((uint32_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); +} + +static inline uint64_t lean_ctor_get_uint64(b_lean_obj_arg o, unsigned offset) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + return *((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); +} + +static inline double lean_ctor_get_float(b_lean_obj_arg o, unsigned offset) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + return *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)); +} + +static inline void lean_ctor_set_usize(b_lean_obj_arg o, unsigned i, size_t v) { + assert(i >= lean_ctor_num_objs(o)); + *((size_t*)(lean_ctor_obj_cptr(o) + i)) = v; +} + +static inline void lean_ctor_set_uint8(b_lean_obj_arg o, unsigned offset, uint8_t v) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + *((uint8_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v; +} + +static inline void lean_ctor_set_uint16(b_lean_obj_arg o, unsigned offset, uint16_t v) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + *((uint16_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v; +} + +static inline void lean_ctor_set_uint32(b_lean_obj_arg o, unsigned offset, uint32_t v) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + *((uint32_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v; +} + +static inline void lean_ctor_set_uint64(b_lean_obj_arg o, unsigned offset, uint64_t v) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + *((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v; +} + +static inline void lean_ctor_set_float(b_lean_obj_arg o, unsigned offset, double v) { + assert(offset >= lean_ctor_num_objs(o) * sizeof(void*)); + *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v; +} + +/* Closures */ + +static inline void * lean_closure_fun(lean_object * o) { return lean_to_closure(o)->m_fun; } +static inline unsigned lean_closure_arity(lean_object * o) { return lean_to_closure(o)->m_arity; } +static inline unsigned lean_closure_num_fixed(lean_object * o) { return lean_to_closure(o)->m_num_fixed; } +static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lean_to_closure(o)->m_objs; } +static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) { + assert(arity > 0); + assert(num_fixed < arity); + lean_closure_object * o = (lean_closure_object*)lean_alloc_small_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed); + lean_set_st_header((lean_object*)o, LeanClosure, 0); + o->m_fun = fun; + o->m_arity = arity; + o->m_num_fixed = num_fixed; + return (lean_object*)o; +} +static inline b_lean_obj_res lean_closure_get(b_lean_obj_arg o, unsigned i) { + assert(i < lean_closure_num_fixed(o)); + return lean_to_closure(o)->m_objs[i]; +} +static inline void lean_closure_set(u_lean_obj_arg o, unsigned i, lean_obj_arg a) { + assert(i < lean_closure_num_fixed(o)); + lean_to_closure(o)->m_objs[i] = a; +} + +lean_object* lean_apply_1(lean_object* f, lean_object* a1); +lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2); +lean_object* lean_apply_3(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3); +lean_object* lean_apply_4(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4); +lean_object* lean_apply_5(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5); +lean_object* lean_apply_6(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6); +lean_object* lean_apply_7(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7); +lean_object* lean_apply_8(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8); +lean_object* lean_apply_9(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9); +lean_object* lean_apply_10(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10); +lean_object* lean_apply_11(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11); +lean_object* lean_apply_12(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12); +lean_object* lean_apply_13(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13); +lean_object* lean_apply_14(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14); +lean_object* lean_apply_15(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15); +lean_object* lean_apply_16(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15, lean_object* a16); +lean_object* lean_apply_n(lean_object* f, unsigned n, lean_object** args); +/* Pre: n > 16 */ +lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args); + +/* Fixpoint */ + +lean_obj_res lean_fixpoint(lean_obj_arg rec, lean_obj_arg a); +lean_obj_res lean_fixpoint2(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2); +lean_obj_res lean_fixpoint3(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3); +lean_obj_res lean_fixpoint4(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4); +lean_obj_res lean_fixpoint5(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5); +lean_obj_res lean_fixpoint6(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5, lean_obj_arg a6); + +/* Arrays of objects (low level API) */ +static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) { + lean_array_object * o = (lean_array_object*)lean_alloc_object(sizeof(lean_array_object) + sizeof(void*)*capacity); + lean_set_st_header((lean_object*)o, LeanArray, 0); + o->m_size = size; + o->m_capacity = capacity; + return (lean_object*)o; +} +static inline size_t lean_array_size(b_lean_obj_arg o) { return lean_to_array(o)->m_size; } +static inline size_t lean_array_capacity(b_lean_obj_arg o) { return lean_to_array(o)->m_capacity; } +static inline size_t lean_array_byte_size(lean_object * o) { + return sizeof(lean_array_object) + sizeof(void*)*lean_array_capacity(o); +} +static inline lean_object ** lean_array_cptr(lean_object * o) { return lean_to_array(o)->m_data; } +static inline void lean_array_set_size(u_lean_obj_arg o, size_t sz) { + assert(lean_is_array(o)); + assert(lean_is_exclusive(o)); + assert(sz <= lean_array_capacity(o)); + lean_to_array(o)->m_size = sz; +} +static inline b_lean_obj_res lean_array_get_core(b_lean_obj_arg o, size_t i) { + assert(i < lean_array_size(o)); + return lean_to_array(o)->m_data[i]; +} +static inline void lean_array_set_core(u_lean_obj_arg o, size_t i, lean_obj_arg v) { + /* Remark: we use this procedure to update non shared arrays in the heap, + and when copying objects to compact region at compact.cpp */ + assert(!lean_has_rc(o) || lean_is_exclusive(o)); + assert(i < lean_array_size(o)); + lean_to_array(o)->m_data[i] = v; +} +lean_object * lean_array_mk(lean_obj_arg sz, lean_obj_arg fn); +lean_object * lean_array_data(lean_obj_arg a, lean_obj_arg i); + +/* Arrays of objects (high level API) */ + +static inline lean_object * lean_array_sz(lean_obj_arg a) { + lean_object * r = lean_box(lean_array_size(a)); + lean_dec(a); + return r; +} + +static inline lean_object * lean_array_get_size(b_lean_obj_arg a) { + return lean_box(lean_array_size(a)); +} + +static inline lean_object * lean_mk_empty_array() { + return lean_alloc_array(0, 0); +} + +static inline lean_object * lean_mk_empty_array_with_capacity(b_lean_obj_arg capacity) { + if (!lean_is_scalar(capacity)) lean_panic_out_of_memory(); + return lean_alloc_array(0, lean_unbox(capacity)); +} + +static inline lean_object * lean_array_uget(b_lean_obj_arg a, size_t i) { + lean_object * r = lean_array_get_core(a, i); lean_inc(r); + return r; +} + +static inline lean_obj_res lean_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) { + return lean_array_uget(a, lean_unbox(i)); +} + +static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) { + if (lean_is_scalar(i)) { + size_t idx = lean_unbox(i); + if (idx < lean_array_size(a)) { + lean_dec(def_val); + return lean_array_uget(a, idx); + } else { + return def_val; + } + } else { + /* The index must be out of bounds because + i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1 + but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones. + In both cases, we would be out-of-memory. */ + return def_val; + } +} + +lean_obj_res lean_copy_expand_array(lean_obj_arg a, bool expand); + +static inline lean_obj_res lean_copy_array(lean_obj_arg a) { + return lean_copy_expand_array(a, false); +} + +static inline lean_obj_res lean_ensure_exclusive_array(lean_obj_arg a) { + if (lean_is_exclusive(a)) return a; + return lean_copy_array(a); +} + +static inline lean_object * lean_array_uset(lean_obj_arg a, size_t i, lean_obj_arg v) { + lean_object * r = lean_ensure_exclusive_array(a); + lean_object ** it = lean_array_cptr(r) + i; + lean_dec(*it); + *it = v; + return r; +} + +static inline lean_object * lean_array_fset(lean_obj_arg a, b_lean_obj_arg i, lean_obj_arg v) { + return lean_array_uset(a, lean_unbox(i), v); +} + +static inline lean_object * lean_array_set(lean_obj_arg a, b_lean_obj_arg i, lean_obj_arg v) { + if (lean_is_scalar(i)) { + size_t idx = lean_unbox(i); + if (idx < lean_array_size(a)) + return lean_array_uset(a, idx, v); + } + lean_dec(v); + return a; +} + +static inline lean_object * lean_array_pop(lean_obj_arg a) { + lean_object * r = lean_ensure_exclusive_array(a); + size_t sz = lean_to_array(r)->m_size; + lean_object ** last; + if (sz == 0) return r; + sz--; + last = lean_array_cptr(r) + sz; + lean_to_array(r)->m_size = sz; + lean_dec(*last); + return r; +} + +static inline lean_object * lean_array_uswap(lean_obj_arg a, size_t i, size_t j) { + lean_object * r = lean_ensure_exclusive_array(a); + lean_object ** it = lean_array_cptr(r); + lean_object * v1 = it[i]; + it[i] = it[j]; + it[j] = v1; + return r; +} + +static inline lean_object * lean_array_fswap(lean_obj_arg a, b_lean_obj_arg i, b_lean_obj_arg j) { + return lean_array_uswap(a, lean_unbox(i), lean_unbox(j)); +} + +static inline lean_object * lean_array_swap(lean_obj_arg a, b_lean_obj_arg i, b_lean_obj_arg j) { + if (!lean_is_scalar(i) || !lean_is_scalar(j)) return a; + size_t ui = lean_unbox(i); + size_t uj = lean_unbox(j); + size_t sz = lean_to_array(a)->m_size; + if (ui >= sz || uj >= sz) return a; + return lean_array_uswap(a, ui, uj); +} + +lean_object * lean_array_push(lean_obj_arg a, lean_obj_arg v); +lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v); + +/* Array of scalars */ + +static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) { + lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity); + lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size); + o->m_size = size; + o->m_capacity = capacity; + return (lean_object*)o; +} +static inline unsigned lean_sarray_elem_size(lean_object * o) { + assert(lean_is_sarray(o)); + return lean_ptr_other(o); +} +static inline size_t lean_sarray_capacity(lean_object * o) { return lean_to_sarray(o)->m_capacity; } +static inline size_t lean_sarray_byte_size(lean_object * o) { + return sizeof(lean_sarray_object) + lean_sarray_elem_size(o)*lean_sarray_capacity(o); +} +static inline size_t lean_sarray_size(b_lean_obj_arg o) { return lean_to_sarray(o)->m_size; } +static inline void lean_sarray_set_size(u_lean_obj_arg o, size_t sz) { + assert(lean_is_exclusive(o)); + assert(sz <= lean_sarray_capacity(o)); + lean_to_sarray(o)->m_size = sz; +} +static inline uint8_t* lean_sarray_cptr(lean_object * o) { return lean_to_sarray(o)->m_data; } + +/* Remark: expand sarray API after we add better support in the compiler */ + +/* ByteArray (special case of Array of Scalars) */ + +lean_obj_res lean_byte_array_mk(lean_obj_arg a); +lean_obj_res lean_byte_array_data(lean_obj_arg a); +lean_obj_res lean_copy_byte_array(lean_obj_arg a); + +static inline lean_obj_res lean_mk_empty_byte_array(b_lean_obj_arg capacity) { + if (!lean_is_scalar(capacity)) lean_panic_out_of_memory(); + return lean_alloc_sarray(1, 0, lean_unbox(capacity)); +} + +static inline lean_obj_res lean_byte_array_size(b_lean_obj_arg a) { + return lean_box(lean_sarray_size(a)); +} + +static inline uint8_t lean_byte_array_get(b_lean_obj_arg a, b_lean_obj_arg i) { + if (lean_is_scalar(i)) { + size_t idx = lean_unbox(i); + return idx < lean_sarray_size(a) ? lean_sarray_cptr(a)[idx] : 0; + } else { + /* The index must be out of bounds. Otherwise we would be out of memory. */ + return 0; + } +} + +lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b); + +static inline lean_obj_res lean_byte_array_set(lean_obj_arg a, b_lean_obj_arg i, uint8_t b) { + if (!lean_is_scalar(i)) { + return a; + } else { + size_t idx = lean_unbox(i); + if (idx >= lean_sarray_size(a)) { + return a; + } else { + lean_obj_res r; + if (lean_is_exclusive(a)) r = a; + else r = lean_copy_byte_array(a); + uint8_t * it = lean_sarray_cptr(r) + idx; + *it = b; + return r; + } + } +} + +/* FloatArray (special case of Array of Scalars) */ + +lean_obj_res lean_float_array_mk(lean_obj_arg a); +lean_obj_res lean_float_array_data(lean_obj_arg a); +lean_obj_res lean_copy_float_array(lean_obj_arg a); + +static inline lean_obj_res lean_mk_empty_float_array(b_lean_obj_arg capacity) { + if (!lean_is_scalar(capacity)) lean_panic_out_of_memory(); + return lean_alloc_sarray(sizeof(double), 0, lean_unbox(capacity)); // NOLINT +} + +static inline lean_obj_res lean_float_array_size(b_lean_obj_arg a) { + return lean_box(lean_sarray_size(a)); +} + +static inline double * lean_float_array_cptr(b_lean_obj_arg a) { + return (double*)(lean_sarray_cptr(a)); // NOLINT +} + +static inline double lean_float_array_get(b_lean_obj_arg a, b_lean_obj_arg i) { + if (lean_is_scalar(i)) { + size_t idx = lean_unbox(i); + return idx < lean_sarray_size(a) ? lean_float_array_cptr(a)[idx] : 0.0; + } else { + /* The index must be out of bounds. Otherwise we would be out of memory. */ + return 0.0; + } +} + +lean_obj_res lean_float_array_push(lean_obj_arg a, double d); + +static inline lean_obj_res lean_float_array_set(lean_obj_arg a, b_lean_obj_arg i, double d) { + if (!lean_is_scalar(i)) { + return a; + } else { + size_t idx = lean_unbox(i); + if (idx >= lean_sarray_size(a)) { + return a; + } else { + lean_obj_res r; + if (lean_is_exclusive(a)) r = a; + else r = lean_copy_float_array(a); + double * it = lean_float_array_cptr(r) + idx; + *it = d; + return r; + } + } +} + +static inline double lean_float_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) { + size_t idx = lean_unbox(i); + return lean_float_array_cptr(a)[idx]; +} + +static inline lean_obj_res lean_float_array_fset(lean_obj_arg a, b_lean_obj_arg i, double d) { + size_t idx = lean_unbox(i); + lean_obj_res r; + if (lean_is_exclusive(a)) r = a; + else r = lean_copy_float_array(a); + double * it = lean_float_array_cptr(r) + idx; + *it = d; + return r; +} + +/* Strings */ + +static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_t len) { + lean_string_object * o = (lean_string_object*)lean_alloc_object(sizeof(lean_string_object) + capacity); + lean_set_st_header((lean_object*)o, LeanString, 0); + o->m_size = size; + o->m_capacity = capacity; + o->m_length = len; + return (lean_object*)o; +} +static inline size_t lean_string_capacity(lean_object * o) { return lean_to_string(o)->m_capacity; } +static inline size_t lean_string_byte_size(lean_object * o) { return sizeof(lean_string_object) + lean_string_capacity(o); } +/* instance : inhabited char := ⟨'A'⟩ */ +static inline uint32_t lean_char_default_value() { return 'A'; } +lean_obj_res lean_mk_string(char const * s); +static inline char const * lean_string_cstr(b_lean_obj_arg o) { + assert(lean_is_string(o)); + return lean_to_string(o)->m_data; +} +static inline size_t lean_string_size(b_lean_obj_arg o) { return lean_to_string(o)->m_size; } +static inline size_t lean_string_len(b_lean_obj_arg o) { return lean_to_string(o)->m_length; } +lean_obj_res lean_string_push(lean_obj_arg s, uint32_t c); +lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2); +static inline lean_obj_res lean_string_length(b_lean_obj_arg s) { return lean_box(lean_string_len(s)); } +lean_obj_res lean_string_mk(lean_obj_arg cs); +lean_obj_res lean_string_data(lean_obj_arg s); +uint32_t lean_string_utf8_get(b_lean_obj_arg s, b_lean_obj_arg i); +lean_obj_res lean_string_utf8_next(b_lean_obj_arg s, b_lean_obj_arg i); +lean_obj_res lean_string_utf8_prev(b_lean_obj_arg s, b_lean_obj_arg i); +lean_obj_res lean_string_utf8_set(lean_obj_arg s, b_lean_obj_arg i, uint32_t c); +static inline uint8_t lean_string_utf8_at_end(b_lean_obj_arg s, b_lean_obj_arg i) { + return !lean_is_scalar(i) || lean_unbox(i) >= lean_string_size(s) - 1; +} +lean_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e); +static inline lean_obj_res lean_string_utf8_byte_size(b_lean_obj_arg s) { return lean_box(lean_string_size(s) - 1); } +static inline bool lean_string_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) { + return s1 == s2 || + (lean_string_size(s1) == lean_string_size(s2) && memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0); +} +static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, s2); } +bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2); +static inline uint8_t lean_string_dec_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_eq(s1, s2); } +static inline uint8_t lean_string_dec_lt(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_lt(s1, s2); } +size_t lean_string_hash(b_lean_obj_arg); + +/* Thunks */ + +static inline lean_obj_res lean_mk_thunk(lean_obj_arg c) { + lean_thunk_object * o = (lean_thunk_object*)lean_alloc_small_object(sizeof(lean_thunk_object)); + lean_set_st_header((lean_object*)o, LeanThunk, 0); + o->m_value = (lean_object*)0; + o->m_closure = c; + return (lean_object*)o; +} + +/* Thunk.pure : A -> Thunk A */ +static inline lean_obj_res lean_thunk_pure(lean_obj_arg v) { + lean_thunk_object * o = (lean_thunk_object*)lean_alloc_small_object(sizeof(lean_thunk_object)); + lean_set_st_header((lean_object*)o, LeanThunk, 0); + o->m_value = v; + o->m_closure = (lean_object*)0; + return (lean_object*)o; +} + +lean_object * lean_thunk_get_core(lean_object * t); + +static inline b_lean_obj_res lean_thunk_get(b_lean_obj_arg t) { + lean_object * r = lean_to_thunk(t)->m_value; + if (r) return r; + return lean_thunk_get_core(t); +} + +/* Primitive for implementing the IR instruction for Thunk.get : Thunk A -> A */ +static inline lean_obj_res lean_thunk_get_own(b_lean_obj_arg t) { + lean_object * r = lean_thunk_get(t); + lean_inc(r); + return r; +} + +lean_obj_res lean_thunk_map(lean_obj_arg f, lean_obj_arg t); +lean_obj_res lean_thunk_bind(lean_obj_arg x, lean_obj_arg f); + +/* Tasks */ + +void lean_init_task_manager(); +void lean_init_task_manager_using(unsigned num_workers); + +lean_obj_res lean_mk_task_with_prio(lean_obj_arg c, unsigned prio); +/* Convert a closure `Unit -> A` into a `Task A` */ +static inline lean_obj_res lean_mk_task(lean_obj_arg c) { return lean_mk_task_with_prio(c, 0); } +/* Convert a value `a : A` into `Task A` */ +lean_obj_res lean_task_pure(lean_obj_arg a); +lean_obj_res lean_task_bind_with_prio(lean_obj_arg x, lean_obj_arg f, unsigned prio); +/* Task.bind (x : Task A) (f : A -> Task B) : Task B */ +static inline lean_obj_res lean_task_bind(lean_obj_arg x, lean_obj_arg f) { return lean_task_bind_with_prio(x, f, 0); } +lean_obj_res lean_task_map_with_prio(lean_obj_arg f, lean_obj_arg t, unsigned prio); +/* Task.map (f : A -> B) (t : Task A) : Task B */ +static inline lean_obj_res lean_task_map(lean_obj_arg f, lean_obj_arg t) { return lean_task_map_with_prio(f, t, 0); } +/* Task.get (t : Task A) : A */ +b_lean_obj_res lean_task_get(b_lean_obj_arg t); + +/* primitive for implementing `IO.checkInterrupt : IO bool` */ +bool lean_io_check_interrupt_core(); +/* primitive for implementing `IO.requestInterrupt : Task a -> IO Unit` */ +void lean_io_request_interrupt_core(b_lean_obj_arg t); +/* primitive for implementing `IO.hasFinished : Task a -> IO Unit` */ +bool lean_io_has_finished_core(b_lean_obj_arg t); +/* primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a) */ +b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list); + +/* External objects */ + +static inline lean_object * lean_alloc_external(lean_external_class * cls, void * data) { + lean_external_object * o = (lean_external_object*)lean_alloc_small_object(sizeof(lean_external_object)); + lean_set_st_header((lean_object*)o, LeanExternal, 0); + o->m_class = cls; + o->m_data = data; + return (lean_object*)o; +} + +static inline lean_external_class * lean_get_external_class(lean_object * o) { + return lean_to_external(o)->m_class; +} + +static inline void * lean_get_external_data(lean_object * o) { + return lean_to_external(o)->m_data; +} + +/* Natural numbers */ + +#define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1) + +lean_object * lean_nat_big_succ(lean_object * a); +lean_object * lean_nat_big_add(lean_object * a1, lean_object * a2); +lean_object * lean_nat_big_sub(lean_object * a1, lean_object * a2); +lean_object * lean_nat_big_mul(lean_object * a1, lean_object * a2); +lean_object * lean_nat_overflow_mul(size_t a1, size_t a2); +lean_object * lean_nat_big_div(lean_object * a1, lean_object * a2); +lean_object * lean_nat_big_mod(lean_object * a1, lean_object * a2); +bool lean_nat_big_eq(lean_object * a1, lean_object * a2); +bool lean_nat_big_le(lean_object * a1, lean_object * a2); +bool lean_nat_big_lt(lean_object * a1, lean_object * a2); +lean_object * lean_nat_big_land(lean_object * a1, lean_object * a2); +lean_object * lean_nat_big_lor(lean_object * a1, lean_object * a2); +lean_object * lean_nat_big_xor(lean_object * a1, lean_object * a2); + +lean_obj_res lean_cstr_to_nat(char const * n); +lean_obj_res lean_big_usize_to_nat(size_t n); +lean_obj_res lean_big_uint64_to_nat(uint64_t n); +static inline lean_obj_res lean_usize_to_nat(size_t n) { + if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT)) + return lean_box(n); + else + return lean_big_usize_to_nat(n); +} +static inline lean_obj_res lean_unsigned_to_nat(unsigned n) { + return lean_usize_to_nat(n); +} +static inline lean_obj_res lean_uint64_to_nat(uint64_t n) { + if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT)) + return lean_box(n); + else + return lean_big_uint64_to_nat(n); +} + +static inline lean_obj_res lean_nat_succ(b_lean_obj_arg a) { + if (LEAN_LIKELY(lean_is_scalar(a))) + return lean_usize_to_nat(lean_unbox(a) + 1); + else + return lean_nat_big_succ(a); +} + +static inline lean_obj_res lean_nat_add(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) + return lean_usize_to_nat(lean_unbox(a1) + lean_unbox(a2)); + else + return lean_nat_big_add(a1, a2); +} + +static inline lean_obj_res lean_nat_sub(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + size_t n1 = lean_unbox(a1); + size_t n2 = lean_unbox(a2); + if (n1 < n2) + return lean_box(0); + else + return lean_box(n1 - n2); + } else { + return lean_nat_big_sub(a1, a2); + } +} + +static inline lean_obj_res lean_nat_mul(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + size_t n1 = lean_unbox(a1); + if (n1 == 0) + return a1; + size_t n2 = lean_unbox(a2); + size_t r = n1*n2; + if (r <= LEAN_MAX_SMALL_NAT && r / n1 == n2) + return lean_box(r); + else + return lean_nat_overflow_mul(n1, n2); + } else { + return lean_nat_big_mul(a1, a2); + } +} + +static inline lean_obj_res lean_nat_div(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + size_t n1 = lean_unbox(a1); + size_t n2 = lean_unbox(a2); + if (n2 == 0) + return lean_box(0); + else + return lean_box(n1 / n2); + } else { + return lean_nat_big_div(a1, a2); + } +} + +static inline lean_obj_res lean_nat_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + size_t n1 = lean_unbox(a1); + size_t n2 = lean_unbox(a2); + if (n2 == 0) + return lean_box(0); + else + return lean_box(n1 % n2); + } else { + return lean_nat_big_mod(a1, a2); + } +} + +static inline bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return a1 == a2; + } else { + return lean_nat_big_eq(a1, a2); + } +} + +static inline uint8_t lean_nat_dec_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) { + return lean_nat_eq(a1, a2); +} + +static inline bool lean_nat_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) { + return !lean_nat_eq(a1, a2); +} + +static inline bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return a1 <= a2; + } else { + return lean_nat_big_le(a1, a2); + } +} + +static inline uint8_t lean_nat_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) { + return lean_nat_le(a1, a2); +} + +static inline bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return a1 < a2; + } else { + return lean_nat_big_lt(a1, a2); + } +} + +static inline uint8_t lean_nat_dec_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) { + return lean_nat_lt(a1, a2); +} + +static inline lean_obj_res lean_nat_land(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return (lean_object*)((size_t)(a1) & (size_t)(a2)); + } else { + return lean_nat_big_land(a1, a2); + } +} + +static inline lean_obj_res lean_nat_lor(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return (lean_object*)((size_t)(a1) | (size_t)(a2)); + } else { + return lean_nat_big_lor(a1, a2); + } +} + +static inline lean_obj_res lean_nat_lxor(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return lean_box(lean_unbox(a1) ^ lean_unbox(a2)); + } else { + return lean_nat_big_xor(a1, a2); + } +} + +lean_obj_res lean_nat_pow(b_lean_obj_arg a1, b_lean_obj_arg a2); + +/* Integers */ + +#define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? INT_MAX : (1 << 30)) +#define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? INT_MIN : -(1 << 30)) +lean_object * lean_int_big_neg(lean_object * a); +lean_object * lean_int_big_add(lean_object * a1, lean_object * a2); +lean_object * lean_int_big_sub(lean_object * a1, lean_object * a2); +lean_object * lean_int_big_mul(lean_object * a1, lean_object * a2); +lean_object * lean_int_big_div(lean_object * a1, lean_object * a2); +lean_object * lean_int_big_mod(lean_object * a1, lean_object * a2); +bool lean_int_big_eq(lean_object * a1, lean_object * a2); +bool lean_int_big_le(lean_object * a1, lean_object * a2); +bool lean_int_big_lt(lean_object * a1, lean_object * a2); +bool lean_int_big_nonneg(lean_object * a); + +lean_object * lean_cstr_to_int(char const * n); +lean_object * lean_big_int_to_int(int n); +lean_object * lean_big_size_t_to_int(size_t n); +lean_object * lean_big_int64_to_int(int64_t n); + +static inline lean_obj_res lean_int_to_int(int n) { + if (sizeof(void*) == 8) + return lean_box((unsigned)(n)); + else if (LEAN_MIN_SMALL_INT <= n && n <= LEAN_MAX_SMALL_INT) + return lean_box((unsigned)(n)); + else + return lean_big_int_to_int(n); +} + +static inline lean_obj_res lean_int64_to_int(int64_t n) { + if (LEAN_LIKELY(LEAN_MIN_SMALL_INT <= n && n <= LEAN_MAX_SMALL_INT)) + return lean_box((unsigned)((int)n)); /* NOLINT */ + else + return lean_big_int64_to_int(n); +} + +static inline int64_t lean_scalar_to_int64(b_lean_obj_arg a) { + assert(lean_is_scalar(a)); + if (sizeof(void*) == 8) + return (int)((unsigned)lean_unbox(a)); /* NOLINT */ + else + return ((int)((size_t)a)) >> 1; /* NOLINT */ +} + +static inline int lean_scalar_to_int(b_lean_obj_arg a) { + assert(lean_is_scalar(a)); + if (sizeof(void*) == 8) + return (int)((unsigned)lean_unbox(a)); /* NOLINT */ + else + return ((int)((size_t)a)) >> 1; /* NOLINT */ +} + +static inline lean_obj_res lean_nat_to_int(lean_obj_arg a) { + if (lean_is_scalar(a)) { + size_t v = lean_unbox(a); + if (v <= LEAN_MAX_SMALL_INT) + return a; + else + return lean_big_size_t_to_int(v); + } else { + return a; + } +} + +static inline lean_obj_res lean_int_neg(b_lean_obj_arg a) { + if (LEAN_LIKELY(lean_is_scalar(a))) { + return lean_int64_to_int(-lean_scalar_to_int64(a)); + } else { + return lean_int_big_neg(a); + } +} + +static inline lean_obj_res lean_int_neg_succ_of_nat(lean_obj_arg a) { + lean_obj_res s = lean_nat_succ(a); lean_dec(a); + lean_obj_res i = lean_nat_to_int(s); lean_dec(s); + lean_obj_res r = lean_int_neg(i); lean_dec(i); + return r; +} + +static inline lean_obj_res lean_int_add(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return lean_int64_to_int(lean_scalar_to_int64(a1) + lean_scalar_to_int64(a2)); + } else { + return lean_int_big_add(a1, a2); + } +} + +static inline lean_obj_res lean_int_sub(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return lean_int64_to_int(lean_scalar_to_int64(a1) - lean_scalar_to_int64(a2)); + } else { + return lean_int_big_sub(a1, a2); + } +} + +static inline lean_obj_res lean_int_mul(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return lean_int64_to_int(lean_scalar_to_int64(a1) * lean_scalar_to_int64(a2)); + } else { + return lean_int_big_mul(a1, a2); + } +} + +static inline lean_obj_res lean_int_div(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + int v1 = lean_scalar_to_int(a1); + int v2 = lean_scalar_to_int(a2); + if (v2 == 0) + return lean_box(0); + else + return lean_int_to_int(v1 / v2); + } else { + return lean_int_big_div(a1, a2); + } +} + +static inline lean_obj_res lean_int_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + int v1 = lean_scalar_to_int(a1); + int v2 = lean_scalar_to_int(a2); + if (v2 == 0) + return lean_box(0); + else + return lean_int_to_int(v1 % v2); + } else { + return lean_int_big_mod(a1, a2); + } +} + +static inline bool lean_int_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return a1 == a2; + } else { + return lean_int_big_eq(a1, a2); + } +} + +static inline bool lean_int_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) { + return !lean_int_eq(a1, a2); +} + +static inline bool lean_int_le(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return lean_scalar_to_int(a1) <= lean_scalar_to_int(a2); + } else { + return lean_int_big_le(a1, a2); + } +} + +static inline bool lean_int_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) { + return lean_scalar_to_int(a1) < lean_scalar_to_int(a2); + } else { + return lean_int_big_lt(a1, a2); + } +} + +lean_obj_res lean_big_int_to_nat(lean_obj_arg a); +static inline lean_obj_res lean_int_to_nat(lean_obj_arg a) { + assert(!lean_int_lt(a, lean_box(0))); + if (lean_is_scalar(a)) { + return a; + } else { + return lean_big_int_to_nat(a); + } +} + +static inline lean_obj_res lean_nat_abs(b_lean_obj_arg i) { + if (lean_int_lt(i, lean_box(0))) { + return lean_int_to_nat(lean_int_neg(i)); + } else { + lean_inc(i); + return lean_int_to_nat(i); + } +} + +static inline uint8_t lean_int_dec_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) { return lean_int_eq(a1, a2); } + +static inline uint8_t lean_int_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) { return lean_int_le(a1, a2); } + +static inline uint8_t lean_int_dec_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) { return lean_int_lt(a1, a2); } + +static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) { + if (LEAN_LIKELY(lean_is_scalar(a))) + return lean_scalar_to_int(a) >= 0; + else + return lean_int_big_nonneg(a); +} + + +/* UInt8 */ + +uint8_t lean_uint8_of_big_nat(b_lean_obj_arg a); +static inline uint8_t lean_uint8_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint8_t)(lean_unbox(a)) : lean_uint8_of_big_nat(a); } +static inline lean_obj_res lean_uint8_to_nat(uint8_t a) { return lean_usize_to_nat((size_t)a); } +static inline uint8_t lean_uint8_add(uint8_t a1, uint8_t a2) { return a1+a2; } +static inline uint8_t lean_uint8_sub(uint8_t a1, uint8_t a2) { return a1-a2; } +static inline uint8_t lean_uint8_mul(uint8_t a1, uint8_t a2) { return a1*a2; } +static inline uint8_t lean_uint8_div(uint8_t a1, uint8_t a2) { return a2 == 0 ? 0 : a1/a2; } +static inline uint8_t lean_uint8_mod(uint8_t a1, uint8_t a2) { return a2 == 0 ? 0 : a1%a2; } +static inline uint8_t lean_uint8_modn(uint8_t a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a2))) { + unsigned n2 = lean_unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else { + return a1; + } +} +static inline uint8_t lean_uint8_dec_eq(uint8_t a1, uint8_t a2) { return a1 == a2; } +static inline uint8_t lean_uint8_dec_lt(uint8_t a1, uint8_t a2) { return a1 < a2; } +static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a2; } + +/* UInt16 */ + +uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a); +static inline uint16_t lean_uint16_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (int16_t)(lean_unbox(a)) : lean_uint16_of_big_nat(a); } +static inline lean_obj_res lean_uint16_to_nat(uint16_t a) { return lean_usize_to_nat((size_t)a); } +static inline uint16_t lean_uint16_add(uint16_t a1, uint16_t a2) { return a1+a2; } +static inline uint16_t lean_uint16_sub(uint16_t a1, uint16_t a2) { return a1-a2; } +static inline uint16_t lean_uint16_mul(uint16_t a1, uint16_t a2) { return a1*a2; } +static inline uint16_t lean_uint16_div(uint16_t a1, uint16_t a2) { return a2 == 0 ? 0 : a1/a2; } +static inline uint16_t lean_uint16_mod(uint16_t a1, uint16_t a2) { return a2 == 0 ? 0 : a1%a2; } +static inline uint16_t lean_uint16_modn(uint16_t a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a2))) { + unsigned n2 = lean_unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else { + return a1; + } +} +static inline uint8_t lean_uint16_dec_eq(uint16_t a1, uint16_t a2) { return a1 == a2; } +static inline uint8_t lean_uint16_dec_lt(uint16_t a1, uint16_t a2) { return a1 < a2; } +static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <= a2; } + +/* UInt32 */ + +uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a); +static inline uint32_t lean_uint32_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint32_t)(lean_unbox(a)) : lean_uint32_of_big_nat(a); } +static inline lean_obj_res lean_uint32_to_nat(uint32_t a) { return lean_usize_to_nat((size_t)a); } +static inline uint32_t lean_uint32_add(uint32_t a1, uint32_t a2) { return a1+a2; } +static inline uint32_t lean_uint32_sub(uint32_t a1, uint32_t a2) { return a1-a2; } +static inline uint32_t lean_uint32_mul(uint32_t a1, uint32_t a2) { return a1*a2; } +static inline uint32_t lean_uint32_div(uint32_t a1, uint32_t a2) { return a2 == 0 ? 0 : a1/a2; } +static inline uint32_t lean_uint32_mod(uint32_t a1, uint32_t a2) { return a2 == 0 ? 0 : a1%a2; } +uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2); +static inline uint32_t lean_uint32_modn(uint32_t a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a2))) { + size_t n2 = lean_unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else if (sizeof(void*) == 4) { + /* 32-bit */ + return lean_uint32_big_modn(a1, a2); + } else { + /* 64-bit */ + return a1; + } +} +static inline uint8_t lean_uint32_dec_eq(uint32_t a1, uint32_t a2) { return a1 == a2; } +static inline uint8_t lean_uint32_dec_lt(uint32_t a1, uint32_t a2) { return a1 < a2; } +static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <= a2; } + +/* UInt64 */ + +uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a); +static inline uint64_t lean_uint64_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint64_t)(lean_unbox(a)) : lean_uint64_of_big_nat(a); } +static inline uint64_t lean_uint64_add(uint64_t a1, uint64_t a2) { return a1+a2; } +static inline uint64_t lean_uint64_sub(uint64_t a1, uint64_t a2) { return a1-a2; } +static inline uint64_t lean_uint64_mul(uint64_t a1, uint64_t a2) { return a1*a2; } +static inline uint64_t lean_uint64_div(uint64_t a1, uint64_t a2) { return a2 == 0 ? 0 : a1/a2; } +static inline uint64_t lean_uint64_mod(uint64_t a1, uint64_t a2) { return a2 == 0 ? 0 : a1%a2; } +uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2); +static inline uint64_t lean_uint64_modn(uint64_t a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a2))) { + size_t n2 = lean_unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else { + return lean_uint64_big_modn(a1, a2); + } +} +static inline uint8_t lean_uint64_dec_eq(uint64_t a1, uint64_t a2) { return a1 == a2; } +static inline uint8_t lean_uint64_dec_lt(uint64_t a1, uint64_t a2) { return a1 < a2; } +static inline uint8_t lean_uint64_dec_le(uint64_t a1, uint64_t a2) { return a1 <= a2; } + +/* USize */ + +size_t lean_usize_of_big_nat(b_lean_obj_arg a); +static inline size_t lean_usize_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? lean_unbox(a) : lean_usize_of_big_nat(a); } +static inline size_t lean_usize_add(size_t a1, size_t a2) { return a1+a2; } +static inline size_t lean_usize_sub(size_t a1, size_t a2) { return a1-a2; } +static inline size_t lean_usize_mul(size_t a1, size_t a2) { return a1*a2; } +static inline size_t lean_usize_div(size_t a1, size_t a2) { return a2 == 0 ? 0 : a1/a2; } +static inline size_t lean_usize_mod(size_t a1, size_t a2) { return a2 == 0 ? 0 : a1%a2; } +size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2); +static inline size_t lean_usize_modn(size_t a1, b_lean_obj_arg a2) { + if (LEAN_LIKELY(lean_is_scalar(a2))) { + size_t n2 = lean_unbox(a2); + return n2 == 0 ? 0 : a1 % n2; + } else { + return lean_usize_big_modn(a1, a2); + } +} +static inline uint8_t lean_usize_dec_eq(size_t a1, size_t a2) { return a1 == a2; } +static inline uint8_t lean_usize_dec_lt(size_t a1, size_t a2) { return a1 < a2; } +static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2; } +size_t lean_usize_mix_hash(size_t a1, size_t a2); + +/* Float */ + +double lean_float_of_nat(b_lean_obj_arg a); +lean_obj_res lean_float_to_string(double a); + +/* Boxing primitives */ + +static inline lean_obj_res lean_box_uint32(uint32_t v) { + if (sizeof(void*) == 4) { + /* 32-bit implementation */ + lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(uint32_t)); + lean_ctor_set_uint32(r, 0, v); + return r; + } else { + /* 64-bit implementation */ + return lean_box(v); + } +} + +static inline unsigned lean_unbox_uint32(b_lean_obj_arg o) { + if (sizeof(void*) == 4) { + /* 32-bit implementation */ + return lean_ctor_get_uint32(o, 0); + } else { + /* 64-bit implementation */ + return lean_unbox(o); + } +} + +static inline lean_obj_res lean_box_uint64(uint64_t v) { + lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(uint64_t)); + lean_ctor_set_uint64(r, 0, v); + return r; +} + +static inline uint64_t lean_unbox_uint64(b_lean_obj_arg o) { + return lean_ctor_get_uint64(o, 0); +} + +static inline lean_obj_res lean_box_usize(size_t v) { + lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(size_t)); + lean_ctor_set_usize(r, 0, v); + return r; +} + +static inline size_t lean_unbox_usize(b_lean_obj_arg o) { + return lean_ctor_get_usize(o, 0); +} + +static inline lean_obj_res lean_box_float(double v) { + lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(double)); // NOLINT + lean_ctor_set_float(r, 0, v); + return r; +} + +static inline double lean_unbox_float(b_lean_obj_arg o) { + return lean_ctor_get_float(o, 0); +} + +/* Debugging helper functions */ + +lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn); +lean_object * lean_dbg_sleep(uint32_t ms, lean_obj_arg fn); +lean_object * lean_dbg_trace_if_shared(lean_obj_arg s, lean_obj_arg a); + +/* IO Helper functions */ + +static inline lean_obj_res lean_io_mk_world() { return lean_box(0); } +static inline bool lean_io_result_is_ok(b_lean_obj_arg r) { return lean_ptr_tag(r) == 0; } +static inline bool lean_io_result_is_error(b_lean_obj_arg r) { return lean_ptr_tag(r) == 1; } +static inline b_lean_obj_res lean_io_result_get_value(b_lean_obj_arg r) { assert(lean_io_result_is_ok(r)); return lean_ctor_get(r, 0); } +static inline b_lean_obj_res lean_io_result_get_error(b_lean_obj_arg r) { assert(lean_io_result_is_error(r)); return lean_ctor_get(r, 0); } +void lean_io_result_show_error(b_lean_obj_arg r); +void lean_io_mark_end_initialization(); +static inline lean_obj_res lean_mk_io_result(lean_obj_arg a) { + lean_object * r = lean_alloc_ctor(0, 2, 0); + lean_ctor_set(r, 0, a); + lean_ctor_set(r, 1, lean_box(0)); + return r; +} +static inline lean_obj_res lean_mk_io_error(lean_obj_arg e) { + lean_object * r = lean_alloc_ctor(1, 2, 0); + lean_ctor_set(r, 0, e); + lean_ctor_set(r, 1, lean_box(0)); + return r; +} + +/* IO Ref primitives */ +lean_obj_res lean_io_mk_ref(lean_obj_arg, lean_obj_arg); +lean_obj_res lean_io_ref_get(b_lean_obj_arg, lean_obj_arg); +lean_obj_res lean_io_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg); +lean_obj_res lean_io_ref_reset(b_lean_obj_arg, lean_obj_arg); +lean_obj_res lean_io_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg); + +/* pointer address unsafe primitive */ +static inline size_t lean_ptr_addr(b_lean_obj_arg a) { return (size_t)a; } + +#ifdef __cplusplus +} +#endif diff --git a/src/include/lean/memory.h b/src/include/lean/memory.h new file mode 100644 index 0000000000..ff55f9bf69 --- /dev/null +++ b/src/include/lean/memory.h @@ -0,0 +1,27 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include + +namespace lean { +/** \brief Set maximum amount of memory in bytes */ +void set_max_memory(size_t max); +/** \brief Set maximum amount of memory in megabytes */ +void set_max_memory_megabyte(unsigned max); +void check_memory(char const * component_name); +size_t get_allocated_memory(); + +#ifdef LEAN_TRACK_CUSTOM_ALLOCATORS +/* We use report_memory_deallocated to track memory released by custom allocators such + as memory_pool. */ +void report_memory_deallocated(size_t s); +size_t get_memory_deallocated(); +#define lean_report_memory_deallocated(s) report_memory_deallocated(s) +#else +#define lean_report_memory_deallocated(s) +#endif +} diff --git a/src/include/lean/mpq.h b/src/include/lean/mpq.h new file mode 100644 index 0000000000..d8dc590080 --- /dev/null +++ b/src/include/lean/mpq.h @@ -0,0 +1,224 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include + +namespace lean { +/** + \brief Wrapper for GMP rationals +*/ +class mpq { + friend class mpfp; + mpq_t m_val; + static mpz_t const & zval(mpz const & v) { return v.m_val; } + static mpz_t & zval(mpz & v) { return v.m_val; } +public: + friend void swap(mpq & a, mpq & b) { mpq_swap(a.m_val, b.m_val); } + friend void swap_numerator(mpq & a, mpz & b) { mpz_swap(mpq_numref(a.m_val), zval(b)); mpq_canonicalize(a.m_val); } + friend void swap_denominator(mpq & a, mpz & b) { mpz_swap(mpq_denref(a.m_val), zval(b)); mpq_canonicalize(a.m_val); } + + mpq & operator=(mpz const & v) { mpq_set_z(m_val, v.m_val); return *this; } + mpq & operator=(mpq const & v) { mpq_set(m_val, v.m_val); return *this; } + mpq & operator=(mpq && v) { swap(*this, v); return *this; } + mpq & operator=(char const * v) { mpq_set_str(m_val, v, 10); return *this; } + mpq & operator=(unsigned long int v) { mpq_set_ui(m_val, v, 1u); return *this; } + mpq & operator=(long int v) { mpq_set_si(m_val, v, 1); return *this; } + mpq & operator=(unsigned int v) { return operator=(static_cast(v)); } + mpq & operator=(int v) { return operator=(static_cast(v)); } + mpq & operator=(double v) { mpq_set_d(m_val, v); return *this; } + + mpq() { mpq_init(m_val); } + mpq(mpq const & v):mpq() { operator=(v); } + mpq(mpq && s):mpq() { mpq_swap(m_val, s.m_val); } + template explicit mpq(T const & v):mpq() { operator=(v); } + mpq(unsigned long int n, unsigned long int d):mpq() { mpq_set_ui(m_val, n, d); mpq_canonicalize(m_val); } + mpq(long int n, long int d):mpq() { mpq_set_si(m_val, n, d); mpq_canonicalize(m_val); } + mpq(unsigned int n, unsigned int d):mpq() { mpq_set_ui(m_val, n, d); mpq_canonicalize(m_val); } + mpq(int n, int d):mpq() { mpq_set_si(m_val, n, d); mpq_canonicalize(m_val); } + ~mpq() { mpq_clear(m_val); } + + unsigned hash() const { return static_cast(mpz_get_si(mpq_numref(m_val))); } + + int sgn() const { return mpq_sgn(m_val); } + friend int sgn(mpq const & a) { return a.sgn(); } + bool is_pos() const { return sgn() > 0; } + bool is_neg() const { return sgn() < 0; } + bool is_zero() const { return sgn() == 0; } + bool is_nonpos() const { return !is_pos(); } + bool is_nonneg() const { return !is_neg(); } + + void neg() { mpq_neg(m_val, m_val); } + friend mpq neg(mpq a) { a.neg(); return a; } + + void abs() { mpq_abs(m_val, m_val); } + friend mpq abs(mpq a) { a.abs(); return a; } + + void inv() { mpq_inv(m_val, m_val); } + friend mpq inv(mpq a) { a.inv(); return a; } + + double get_double() const { return mpq_get_d(m_val); } + + bool is_integer() const { return mpz_cmp_ui(mpq_denref(m_val), 1u) == 0; } + + friend int cmp(mpq const & a, mpq const & b) { return mpq_cmp(a.m_val, b.m_val); } + friend int cmp(mpq const & a, mpz const & b); + friend int cmp(mpq const & a, unsigned b) { return mpq_cmp_ui(a.m_val, b, 1); } + friend int cmp(mpq const & a, int b) { return mpq_cmp_si(a.m_val, b, 1); } + friend int cmp(mpq const & a, double b) { return static_cast(a.get_double() - b); } + + friend bool operator<(mpq const & a, mpq const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpq const & a, mpz const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpq const & a, unsigned b) { return cmp(a, b) < 0; } + friend bool operator<(mpq const & a, int b) { return cmp(a, b) < 0; } + friend bool operator<(mpq const & a, double b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, mpq const & b) { return cmp(b, a) > 0; } + friend bool operator<(unsigned a, mpq const & b) { return cmp(b, a) > 0; } + friend bool operator<(int a, mpq const & b) { return cmp(b, a) > 0; } + friend bool operator<(double a, mpq const & b) { return cmp(b, a) > 0; } + + friend bool operator>(mpq const & a, mpq const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpq const & a, mpz const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpq const & a, unsigned b) { return cmp(a, b) > 0; } + friend bool operator>(mpq const & a, int b) { return cmp(a, b) > 0; } + friend bool operator>(mpq const & a, double b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, mpq const & b) { return cmp(b, a) < 0; } + friend bool operator>(unsigned a, mpq const & b) { return cmp(b, a) < 0; } + friend bool operator>(int a, mpq const & b) { return cmp(b, a) < 0; } + friend bool operator>(double a, mpq const & b) { return cmp(b, a) < 0; } + + friend bool operator<=(mpq const & a, mpq const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpq const & a, mpz const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpq const & a, unsigned b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpq const & a, int b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpq const & a, double b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, mpq const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(unsigned a, mpq const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(int a, mpq const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(double a, mpq const & b) { return cmp(b, a) >= 0; } + + friend bool operator>=(mpq const & a, mpq const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpq const & a, mpz const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpq const & a, unsigned b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpq const & a, int b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpq const & a, double b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, mpq const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(unsigned a, mpq const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(int a, mpq const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(double a, mpq const & b) { return cmp(b, a) <= 0; } + + friend bool operator==(mpq const & a, mpq const & b) { return mpq_equal(a.m_val, b.m_val) != 0; } + friend bool operator==(mpq const & a, mpz const & b) { return a.is_integer() && mpz_cmp(mpq_numref(a.m_val), zval(b)) == 0; } + friend bool operator==(mpq const & a, unsigned int b) { return a.is_integer() && mpz_cmp_ui(mpq_numref(a.m_val), b) == 0; } + friend bool operator==(mpq const & a, int b) { return a.is_integer() && mpz_cmp_si(mpq_numref(a.m_val), b) == 0; } + friend bool operator==(mpz const & a, mpq const & b) { return operator==(b, a); } + friend bool operator==(unsigned int a, mpq const & b) { return operator==(b, a); } + friend bool operator==(int a, mpq const & b) { return operator==(b, a); } + + friend bool operator!=(mpq const & a, mpq const & b) { return !operator==(a, b); } + friend bool operator!=(mpq const & a, mpz const & b) { return !operator==(a, b); } + friend bool operator!=(mpq const & a, unsigned int b) { return !operator==(a, b); } + friend bool operator!=(mpq const & a, int b) { return !operator==(a, b); } + friend bool operator!=(mpz const & a, mpq const & b) { return !operator==(a, b); } + friend bool operator!=(unsigned int a, mpq const & b) { return !operator==(a, b); } + friend bool operator!=(int a, mpq const & b) { return !operator==(a, b); } + + mpq & operator+=(mpq const & o) { mpq_add(m_val, m_val, o.m_val); return *this; } + mpq & operator+=(mpz const & o) { mpz_addmul(mpq_numref(m_val), mpq_denref(m_val), o.m_val); mpq_canonicalize(m_val); return *this; } + mpq & operator+=(unsigned int k) { mpz_addmul_ui(mpq_numref(m_val), mpq_denref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator+=(int k) { if (k >= 0) return operator+=(static_cast(k)); else return operator-=(static_cast(-k)); } + + mpq & operator-=(mpq const & o) { mpq_sub(m_val, m_val, o.m_val); return *this; } + mpq & operator-=(mpz const & o) { mpz_submul(mpq_numref(m_val), mpq_denref(m_val), o.m_val); mpq_canonicalize(m_val); return *this; } + mpq & operator-=(unsigned int k) { mpz_submul_ui(mpq_numref(m_val), mpq_denref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator-=(int k) { if (k >= 0) return operator-=(static_cast(k)); else return operator+=(static_cast(-k)); } + + mpq & operator*=(mpq const & o) { mpq_mul(m_val, m_val, o.m_val); return *this; } + mpq & operator*=(mpz const & o) { mpz_mul(mpq_numref(m_val), mpq_numref(m_val), o.m_val); mpq_canonicalize(m_val); return *this; } + mpq & operator*=(unsigned int k) { mpz_mul_ui(mpq_numref(m_val), mpq_numref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator*=(int k) { mpz_mul_si(mpq_numref(m_val), mpq_numref(m_val), k); mpq_canonicalize(m_val); return *this; } + + mpq & operator/=(mpq const & o) { mpq_div(m_val, m_val, o.m_val); return *this; } + mpq & operator/=(mpz const & o) { mpz_mul(mpq_denref(m_val), mpq_denref(m_val), o.m_val); mpq_canonicalize(m_val); return *this; } + mpq & operator/=(unsigned int k) { mpz_mul_ui(mpq_denref(m_val), mpq_denref(m_val), k); mpq_canonicalize(m_val); return *this; } + mpq & operator/=(int k) { mpz_mul_si(mpq_denref(m_val), mpq_denref(m_val), k); mpq_canonicalize(m_val); return *this; } + + friend mpq operator+(mpq a, mpq const & b) { return a += b; } + friend mpq operator+(mpq a, mpz const & b) { return a += b; } + friend mpq operator+(mpq a, unsigned b) { return a += b; } + friend mpq operator+(mpq a, int b) { return a += b; } + friend mpq operator+(mpz const & a, mpq b) { return b += a; } + friend mpq operator+(unsigned a, mpq b) { return b += a; } + friend mpq operator+(int a, mpq b) { return b += a; } + + friend mpq operator-(mpq a, mpq const & b) { return a -= b; } + friend mpq operator-(mpq a, mpz const & b) { return a -= b; } + friend mpq operator-(mpq a, unsigned b) { return a -= b; } + friend mpq operator-(mpq a, int b) { return a -= b; } + friend mpq operator-(mpz const & a, mpq b) { b.neg(); return b += a; } + friend mpq operator-(unsigned a, mpq b) { b.neg(); return b += a; } + friend mpq operator-(int a, mpq b) { b.neg(); return b += a; } + + friend mpq operator*(mpq a, mpq const & b) { return a *= b; } + friend mpq operator*(mpq a, mpz const & b) { return a *= b; } + friend mpq operator*(mpq a, unsigned b) { return a *= b; } + friend mpq operator*(mpq a, int b) { return a *= b; } + friend mpq operator*(mpz const & a, mpq b) { return b *= a; } + friend mpq operator*(unsigned a, mpq b) { return b *= a; } + friend mpq operator*(int a, mpq b) { return b *= a; } + + friend mpq operator/(mpq a, mpq const & b) { return a /= b; } + friend mpq operator/(mpq a, mpz const & b) { return a /= b; } + friend mpq operator/(mpq a, unsigned b) { return a /= b; } + friend mpq operator/(mpq a, int b) { return a /= b; } + friend mpq operator/(mpz const & a, mpq b) { b.inv(); return b *= a; } + friend mpq operator/(unsigned a, mpq b) { b.inv(); return b *= a; } + friend mpq operator/(int a, mpq b) { b.inv(); return b *= a; } + + mpq & operator++() { return operator+=(1); } + mpq operator++(int) { mpq r(*this); ++(*this); return r; } + + mpq & operator--() { return operator-=(1); } + mpq operator--(int) { mpq r(*this); --(*this); return r; } + + mpq operator-() const { mpq t = *this; t.neg(); return t; } + + // a <- numerator(b) + friend void numerator(mpz & a, mpq const & b) { mpz_set(zval(a), mpq_numref(b.m_val)); } + // a <- denominator(b) + friend void denominator(mpz & a, mpq const & b) { mpz_set(zval(a), mpq_denref(b.m_val)); } + + mpz get_numerator() const { mpz r; numerator(r, *this); return r; } + mpz get_denominator() const { mpz r; denominator(r, *this); return r; } + + void floor(); + friend mpz floor(mpq const & a); + + void ceil(); + friend mpz ceil(mpq const & a); + + friend void power(mpq & a, mpq const & b, unsigned k); + friend void _power(mpq & a, mpq const & b, unsigned k) { power(a, b, k); } + friend mpq pow(mpq a, unsigned k) { power(a, a, k); return a; } + + friend std::ostream & operator<<(std::ostream & out, mpq const & v); + + friend void display_decimal(std::ostream & out, mpq const & a, unsigned prec); + + class decimal { + mpq const & m_val; + unsigned m_prec; + public: + decimal(mpq const & val, unsigned prec = 10):m_val(val), m_prec(prec) {} + friend std::ostream & operator<<(std::ostream & out, decimal const & d) { display_decimal(out, d.m_val, d.m_prec); return out; } + }; +}; + +serializer & operator<<(serializer & s, mpq const & n); +mpq read_mpq(deserializer & d); +inline deserializer & operator>>(deserializer & d, mpq & n) { n = read_mpq(d); return d; } +} diff --git a/src/include/lean/mpz.h b/src/include/lean/mpz.h new file mode 100644 index 0000000000..b650834c9d --- /dev/null +++ b/src/include/lean/mpz.h @@ -0,0 +1,267 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include +#include +#include +#include +#include +#include + +namespace lean { + +class mpq; +/** \brief Wrapper for GMP integers */ +class mpz { + friend class mpq; + friend class mpfp; + mpz_t m_val; + mpz(__mpz_struct const * v) { mpz_init_set(m_val, v); } +public: + mpz() { mpz_init(m_val); } + explicit mpz(char const * v) { mpz_init_set_str(m_val, const_cast(v), 10); } + explicit mpz(unsigned int v) { mpz_init_set_ui(m_val, v); } + explicit mpz(int v) { mpz_init_set_si(m_val, v); } + explicit mpz(uint64 v); + explicit mpz(int64 v); + static mpz of_size_t(size_t v) { + if (sizeof(size_t) == sizeof(uint64)) // NOLINT + return mpz((uint64) v); // NOLINT + else + return mpz((unsigned) v); // NOLINT + } + mpz(mpz const & s) { mpz_init_set(m_val, s.m_val); } + mpz(mpz && s):mpz() { mpz_swap(m_val, s.m_val); } + ~mpz() { mpz_clear(m_val); } + + friend void swap(mpz & a, mpz & b) { mpz_swap(a.m_val, b.m_val); } + + unsigned hash() const { return static_cast(mpz_get_si(m_val)); } + + int sgn() const { return mpz_sgn(m_val); } + friend int sgn(mpz const & a) { return a.sgn(); } + bool is_pos() const { return sgn() > 0; } + bool is_neg() const { return sgn() < 0; } + bool is_zero() const { return sgn() == 0; } + bool is_nonpos() const { return !is_pos(); } + bool is_nonneg() const { return !is_neg(); } + + void neg() { mpz_neg(m_val, m_val); } + friend mpz neg(mpz a) { a.neg(); return a; } + + void abs() { mpz_abs(m_val, m_val); } + friend mpz abs(mpz a) { a.abs(); return a; } + + bool even() const { return mpz_even_p(m_val) != 0; } + bool odd() const { return !even(); } + + bool is_int() const { return mpz_fits_sint_p(m_val) != 0; } + bool is_unsigned_int() const { return mpz_fits_uint_p(m_val) != 0; } + bool is_long_int() const { return mpz_fits_slong_p(m_val) != 0; } + bool is_unsigned_long_int() const { return mpz_fits_ulong_p(m_val) != 0; } + bool is_size_t() const { + // GMP only features `fits` functions up to `unsigned long`, which is smaller than `size_t` on Windows. + // So we directly count the number of mpz words instead. + static_assert(sizeof(size_t) == sizeof(mp_limb_t), "GMP word size should be equal to system word size"); + return is_nonneg() && mpz_size(m_val) <= 1; + } + + long int get_long_int() const { lean_assert(is_long_int()); return mpz_get_si(m_val); } + int get_int() const { lean_assert(is_int()); return static_cast(get_long_int()); } + unsigned long int get_unsigned_long_int() const { lean_assert(is_unsigned_long_int()); return mpz_get_ui(m_val); } + unsigned int get_unsigned_int() const { lean_assert(is_unsigned_int()); return static_cast(get_unsigned_long_int()); } + size_t get_size_t() const; + double get_double() const { return mpz_get_d(m_val); } + + mpz & operator=(mpz const & v) { mpz_set(m_val, v.m_val); return *this; } + mpz & operator=(mpz && v) { swap(*this, v); return *this; } + mpz & operator=(char const * v) { mpz_set_str(m_val, v, 10); return *this; } + mpz & operator=(unsigned int v) { mpz_set_ui(m_val, v); return *this; } + mpz & operator=(int v) { mpz_set_si(m_val, v); return *this; } + + friend int cmp(mpz const & a, mpz const & b) { return mpz_cmp(a.m_val, b.m_val); } + friend int cmp(mpz const & a, unsigned b) { return mpz_cmp_ui(a.m_val, b); } + friend int cmp(mpz const & a, unsigned long b) { return mpz_cmp_ui(a.m_val, b); } + friend int cmp(mpz const & a, int b) { return mpz_cmp_si(a.m_val, b); } + + friend bool operator<(mpz const & a, mpz const & b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, unsigned b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, unsigned long b) { return cmp(a, b) < 0; } + friend bool operator<(mpz const & a, int b) { return cmp(a, b) < 0; } + friend bool operator<(unsigned a, mpz const & b) { return cmp(b, a) > 0; } + friend bool operator<(int a, mpz const & b) { return cmp(b, a) > 0; } + + friend bool operator>(mpz const & a, mpz const & b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, unsigned b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, unsigned long b) { return cmp(a, b) > 0; } + friend bool operator>(mpz const & a, int b) { return cmp(a, b) > 0; } + friend bool operator>(unsigned a, mpz const & b) { return cmp(b, a) < 0; } + friend bool operator>(int a, mpz const & b) { return cmp(b, a) < 0; } + + friend bool operator<=(mpz const & a, mpz const & b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, unsigned b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, unsigned long b) { return cmp(a, b) <= 0; } + friend bool operator<=(mpz const & a, int b) { return cmp(a, b) <= 0; } + friend bool operator<=(unsigned a, mpz const & b) { return cmp(b, a) >= 0; } + friend bool operator<=(int a, mpz const & b) { return cmp(b, a) >= 0; } + + friend bool operator>=(mpz const & a, mpz const & b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, unsigned b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, unsigned long b) { return cmp(a, b) >= 0; } + friend bool operator>=(mpz const & a, int b) { return cmp(a, b) >= 0; } + friend bool operator>=(unsigned a, mpz const & b) { return cmp(b, a) <= 0; } + friend bool operator>=(int a, mpz const & b) { return cmp(b, a) <= 0; } + + friend bool operator==(mpz const & a, mpz const & b) { return cmp(a, b) == 0; } + friend bool operator==(mpz const & a, unsigned b) { return cmp(a, b) == 0; } + friend bool operator==(mpz const & a, unsigned long b) { return cmp(a, b) == 0; } + friend bool operator==(mpz const & a, int b) { return cmp(a, b) == 0; } + friend bool operator==(unsigned a, mpz const & b) { return cmp(b, a) == 0; } + friend bool operator==(int a, mpz const & b) { return cmp(b, a) == 0; } + + friend bool operator!=(mpz const & a, mpz const & b) { return cmp(a, b) != 0; } + friend bool operator!=(mpz const & a, unsigned b) { return cmp(a, b) != 0; } + friend bool operator!=(mpz const & a, unsigned long b) { return cmp(a, b) != 0; } + friend bool operator!=(mpz const & a, int b) { return cmp(a, b) != 0; } + friend bool operator!=(unsigned a, mpz const & b) { return cmp(b, a) != 0; } + friend bool operator!=(int a, mpz const & b) { return cmp(b, a) != 0; } + + mpz & operator+=(mpz const & o) { mpz_add(m_val, m_val, o.m_val); return *this; } + mpz & operator+=(unsigned u) { mpz_add_ui(m_val, m_val, u); return *this; } + mpz & operator+=(uint64 u) { return u > std::numeric_limits::max() ? *this += mpz(u) : *this += static_cast(u); } + mpz & operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, -u); return *this; } + + mpz & operator-=(mpz const & o) { mpz_sub(m_val, m_val, o.m_val); return *this; } + mpz & operator-=(unsigned u) { mpz_sub_ui(m_val, m_val, u); return *this; } + mpz & operator-=(uint64 u) { return u > std::numeric_limits::max() ? *this -= mpz(u) : *this -= static_cast(u); } + mpz & operator-=(int u) { if (u >= 0) mpz_sub_ui(m_val, m_val, u); else mpz_add_ui(m_val, m_val, -u); return *this; } + + mpz & operator*=(mpz const & o) { mpz_mul(m_val, m_val, o.m_val); return *this; } + mpz & operator*=(unsigned u) { mpz_mul_ui(m_val, m_val, u); return *this; } + mpz & operator*=(uint64 u) { return u > std::numeric_limits::max() ? *this *= mpz(u) : *this *= static_cast(u); } + mpz & operator*=(int u) { mpz_mul_si(m_val, m_val, u); return *this; } + + mpz & operator/=(mpz const & o) { mpz_tdiv_q(m_val, m_val, o.m_val); return *this; } + mpz & operator/=(unsigned u) { mpz_tdiv_q_ui(m_val, m_val, u); return *this; } + mpz & operator/=(uint64 u) { return u > std::numeric_limits::max() ? *this /= mpz(u) : *this /= static_cast(u); } + mpz & operator/=(int u) { return operator/=(mpz(u)); } // TODO(Leo): improve + + friend mpz rem(mpz const & a, mpz const & b) { mpz r; mpz_tdiv_r(r.m_val, a.m_val, b.m_val); return r; } + mpz & operator%=(mpz const & o) { mpz r(*this % o); mpz_swap(m_val, r.m_val); return *this; } + mpz pow(unsigned int exp) const { mpz r; mpz_pow_ui(r.m_val, m_val, exp); return r; } + + friend mpz operator+(mpz a, mpz const & b) { return a += b; } + friend mpz operator+(mpz a, unsigned b) { return a += b; } + friend mpz operator+(mpz a, uint64 b) { return a += b; } + friend mpz operator+(mpz a, int b) { return a += b; } + friend mpz operator+(unsigned a, mpz b) { return b += a; } + friend mpz operator+(uint64 a, mpz b) { return b += a; } + friend mpz operator+(int a, mpz b) { return b += a; } + + friend mpz operator-(mpz a, mpz const & b) { return a -= b; } + friend mpz operator-(mpz a, unsigned b) { return a -= b; } + friend mpz operator-(mpz a, uint64 b) { return a -= b; } + friend mpz operator-(mpz a, int b) { return a -= b; } + friend mpz operator-(unsigned a, mpz b) { b.neg(); return b += a; } + friend mpz operator-(uint64 a, mpz b) { b.neg(); return b += a; } + friend mpz operator-(int a, mpz b) { b.neg(); return b += a; } + + friend mpz operator*(mpz a, mpz const & b) { return a *= b; } + friend mpz operator*(mpz a, unsigned b) { return a *= b; } + friend mpz operator*(mpz a, uint64 b) { return a *= b; } + friend mpz operator*(mpz a, int b) { return a *= b; } + friend mpz operator*(unsigned a, mpz b) { return b *= a; } + friend mpz operator*(uint64 a, mpz b) { return b *= a; } + friend mpz operator*(int a, mpz b) { return b *= a; } + + friend mpz operator/(mpz a, mpz const & b) { return a /= b; } + friend mpz operator/(mpz a, unsigned b) { return a /= b; } + friend mpz operator/(mpz a, uint64 b) { return a /= b; } + friend mpz operator/(mpz a, int b) { return a /= b; } + friend mpz operator/(unsigned a, mpz const & b) { mpz r(a); return r /= b; } + friend mpz operator/(uint64 a, mpz const & b) { mpz r(a); return r /= b; } + friend mpz operator/(int a, mpz const & b) { mpz r(a); return r /= b; } + + friend mpz operator%(mpz const & a, mpz const & b); + + mpz & operator++() { return operator+=(1); } + mpz operator++(int) { mpz r(*this); ++(*this); return r; } + + mpz & operator--() { return operator-=(1); } + mpz operator--(int) { mpz r(*this); --(*this); return r; } + + mpz & operator&=(mpz const & o) { mpz_and(m_val, m_val, o.m_val); return *this; } + mpz & operator|=(mpz const & o) { mpz_ior(m_val, m_val, o.m_val); return *this; } + mpz & operator^=(mpz const & o) { mpz_xor(m_val, m_val, o.m_val); return *this; } + void comp() { mpz_com(m_val, m_val); } + + friend mpz operator&(mpz a, mpz const & b) { return a &= b; } + friend mpz operator|(mpz a, mpz const & b) { return a |= b; } + friend mpz operator^(mpz a, mpz const & b) { return a ^= b; } + friend mpz operator~(mpz a) { a.comp(); return a; } + + bool test_bit(size_t bit) const { return mpz_tstbit(m_val, bit) != 0; } + + // this <- this + a*b + void addmul(mpz const & a, mpz const & b) { mpz_addmul(m_val, a.m_val, b.m_val); } + // this <- this - a*b + void submul(mpz const & a, mpz const & b) { mpz_submul(m_val, a.m_val, b.m_val); } + + // a <- b * 2^k + friend void mul2k(mpz & a, mpz const & b, unsigned k) { mpz_mul_2exp(a.m_val, b.m_val, k); } + // a <- b / 2^k + friend void div2k(mpz & a, mpz const & b, unsigned k) { mpz_tdiv_q_2exp(a.m_val, b.m_val, k); } + // a <- b % 2^k + friend void mod2k(mpz & a, mpz const & b, unsigned k) { mpz_tdiv_r_2exp(a.m_val, b.m_val, k); } + + /** + \brief Return the position of the most significant bit. + Return 0 if the number is negative + */ + unsigned log2() const; + + /** + \brief log2(-n) + Return 0 if the number is nonegative + */ + unsigned mlog2() const; + + bool perfect_square() const { return mpz_perfect_square_p(m_val); } + + bool is_power_of_two() const { return is_pos() && mpz_popcount(m_val) == 1; } + bool is_power_of_two(unsigned & shift) const; + /** + \brief Return largest k s.t. n is a multiple of 2^k + */ + unsigned power_of_two_multiple() const { return mpz_scan1(m_val, 0); } + + friend void power(mpz & a, mpz const & b, unsigned k) { mpz_pow_ui(a.m_val, b.m_val, k); } + friend void _power(mpz & a, mpz const & b, unsigned k) { power(a, b, k); } + friend mpz pow(mpz a, unsigned k) { power(a, a, k); return a; } + + friend void rootrem(mpz & root, mpz & rem, mpz const & a, unsigned k) { mpz_rootrem(root.m_val, rem.m_val, a.m_val, k); } + // root <- a^{1/k}, return true iff the result is an integer + friend bool root(mpz & root, mpz const & a, unsigned k); + friend mpz root(mpz const & a, unsigned k) { mpz r; root(r, a, k); return r; } + + friend void gcd(mpz & g, mpz const & a, mpz const & b) { mpz_gcd(g.m_val, a.m_val, b.m_val); } + friend mpz gcd(mpz const & a, mpz const & b) { mpz r; gcd(r, a, b); return r; } + friend void gcdext(mpz & g, mpz & s, mpz & t, mpz const & a, mpz const & b) { mpz_gcdext(g.m_val, s.m_val, t.m_val, a.m_val, b.m_val); } + friend void lcm(mpz & l, mpz const & a, mpz const & b) { mpz_lcm(l.m_val, a.m_val, b.m_val); } + friend mpz lcm(mpz const & a, mpz const & b) { mpz l; lcm(l, a, b); return l; } + + friend std::ostream & operator<<(std::ostream & out, mpz const & v); + + std::string to_string() const; +}; + +struct mpz_cmp_fn { + int operator()(mpz const & v1, mpz const & v2) const { return cmp(v1, v2); } +}; +} diff --git a/src/include/lean/object.h b/src/include/lean/object.h new file mode 100644 index 0000000000..04dd5df94c --- /dev/null +++ b/src/include/lean/object.h @@ -0,0 +1,501 @@ +/* +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include + +namespace lean { +typedef uint8_t uint8; +typedef uint16_t uint16; +typedef uint32_t uint32; +typedef uint64_t uint64; +typedef size_t usize; + +typedef lean_object object; +typedef object * obj_arg; +typedef object * b_obj_arg; +typedef object * u_obj_arg; +typedef object * obj_res; +typedef object * b_obj_res; + +struct mpz_object { + lean_object m_header; + mpz m_value; + mpz_object() {} + explicit mpz_object(mpz const & m):m_value(m) {} +}; + +typedef lean_external_class external_object_class; +typedef lean_external_finalize_proc external_object_finalize_proc; +typedef lean_external_foreach_proc external_object_foreach_proc; + +inline external_object_class * register_external_object_class(external_object_finalize_proc p1, external_object_foreach_proc p2) { + return lean_register_external_class(p1, p2); +} + +inline bool is_scalar(object * o) { return lean_is_scalar(o); } +inline object * box(size_t n) { return lean_box(n); } +inline size_t unbox(object * o) { return lean_unbox(o); } + +inline bool is_mt_heap_obj(object * o) { return lean_is_mt(o); } +inline bool is_st_heap_obj(object * o) { return lean_is_st(o); } +inline bool is_heap_obj(object * o) { return is_st_heap_obj(o) || is_mt_heap_obj(o); } +inline void mark_mt(object * o) { lean_mark_mt(o); } +inline bool is_shared(object * o) { return lean_is_shared(o); } +inline bool is_exclusive(object * o) { return lean_is_exclusive(o); } +inline void inc_ref(object * o) { lean_inc_ref(o); } +inline void inc_ref(object * o, size_t n) { lean_inc_ref_n(o, n); } +inline bool dec_ref_core(object * o) { return lean_dec_ref_core(o); } +inline void dec_ref(object * o) { lean_dec_ref(o); } +inline void inc(object * o) { lean_inc(o); } +inline void inc(object * o, size_t n) { lean_inc_n(o, n); } +inline void dec(object * o) { lean_dec(o); } +inline void free_heap_obj(object * o) { lean_free_object(o); } + +inline bool is_cnstr(object * o) { return lean_is_ctor(o); } +inline bool is_closure(object * o) { return lean_is_closure(o); } +inline bool is_array(object * o) { return lean_is_array(o); } +inline bool is_sarray(object * o) { return lean_is_sarray(o); } +inline bool is_string(object * o) { return lean_is_string(o); } +inline bool is_mpz(object * o) { return lean_is_mpz(o); } +inline bool is_thunk(object * o) { return lean_is_thunk(o); } +inline bool is_task(object * o) { return lean_is_task(o); } +inline bool is_external(object * o) { return lean_is_external(o); } +inline bool is_ref(object * o) { return lean_is_ref(o); } + +inline void mark_persistent(object * o) { return lean_mark_persistent(o); } + +inline unsigned obj_tag(b_obj_arg o) { return lean_obj_tag(o); } + +// ======================================= +// Constructors + +inline unsigned cnstr_num_objs(object * o) { return lean_ctor_num_objs(o); } +inline object ** cnstr_obj_cptr(object * o) { return lean_ctor_obj_cptr(o); } +inline uint8 * cnstr_scalar_cptr(object * o) { return lean_ctor_scalar_cptr(o); } +inline obj_res alloc_cnstr(unsigned tag, unsigned num_objs, unsigned scalar_sz) { return lean_alloc_ctor(tag, num_objs, scalar_sz); } +inline unsigned cnstr_tag(b_obj_arg o) { lean_assert(is_cnstr(o)); return lean_ptr_tag(o); } +inline void cnstr_set_tag(b_obj_arg o, unsigned tag) { lean_ctor_set_tag(o, tag); } +inline b_obj_res cnstr_get(b_obj_arg o, unsigned i) { return lean_ctor_get(o, i); } +inline void cnstr_set(u_obj_arg o, unsigned i, obj_arg v) { lean_ctor_set(o, i, v); } +inline void cnstr_release(u_obj_arg o, unsigned i) { lean_ctor_release(o, i); } +inline usize cnstr_get_usize(b_obj_arg o, unsigned i) { return lean_ctor_get_usize(o, i); } +inline void cnstr_set_usize(b_obj_arg o, unsigned i, usize v) { lean_ctor_set_usize(o, i, v); } +inline uint8 cnstr_get_uint8(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint8(o, offset); } +inline uint16 cnstr_get_uint16(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint16(o, offset); } +inline uint32 cnstr_get_uint32(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint32(o, offset); } +inline uint64 cnstr_get_uint64(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint64(o, offset); } +inline double cnstr_get_float(b_obj_arg o, unsigned offset) { return lean_ctor_get_float(o, offset); } +inline void cnstr_set_uint8(b_obj_arg o, unsigned offset, uint8 v) { lean_ctor_set_uint8(o, offset, v); } +inline void cnstr_set_uint16(b_obj_arg o, unsigned offset, uint16 v) { lean_ctor_set_uint16(o, offset, v); } +inline void cnstr_set_uint32(b_obj_arg o, unsigned offset, uint32 v) { lean_ctor_set_uint32(o, offset, v); } +inline void cnstr_set_uint64(b_obj_arg o, unsigned offset, uint64 v) { lean_ctor_set_uint64(o, offset, v); } +inline void cnstr_set_float(b_obj_arg o, unsigned offset, double v) { lean_ctor_set_float(o, offset, v); } + +// ======================================= +// Closures + +void free_closure_obj(object * o); +inline void * closure_fun(object * o) { return lean_closure_fun(o); } +inline unsigned closure_arity(object * o) { return lean_closure_arity(o); } +inline unsigned closure_num_fixed(object * o) { return lean_closure_num_fixed(o); } +inline object ** closure_arg_cptr(object * o) { return lean_closure_arg_cptr(o); } +inline obj_res alloc_closure(void * fun, unsigned arity, unsigned num_fixed) { return lean_alloc_closure(fun, arity, num_fixed); } +inline b_obj_res closure_get(b_obj_arg o, unsigned i) { return lean_closure_get(o, i); } +inline void closure_set(u_obj_arg o, unsigned i, obj_arg a) { lean_closure_set(o, i, a); } +inline obj_res alloc_closure(object*(*fun)(object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 1, num_fixed); +} +inline obj_res alloc_closure(object*(*fun)(object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 2, num_fixed); +} +inline obj_res alloc_closure(object*(*fun)(object *, object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 3, num_fixed); +} +inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 4, num_fixed); +} +inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 5, num_fixed); +} +inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 6, num_fixed); +} +inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *, object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 7, num_fixed); +} +inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *, object *, object *, object *), unsigned num_fixed) { + return alloc_closure(reinterpret_cast(fun), 8, num_fixed); +} +inline object* apply_1(object* f, object* a1) { return lean_apply_1(f, a1); } +inline object* apply_2(object* f, object* a1, object* a2) { return lean_apply_2(f, a1, a2); } +inline object* apply_3(object* f, object* a1, object* a2, object* a3) { return lean_apply_3(f, a1, a2, a3); } +inline object* apply_4(object* f, object* a1, object* a2, object* a3, object* a4) { return lean_apply_4(f, a1, a2, a3, a4); } +inline object* apply_5(object* f, object* a1, object* a2, object* a3, object* a4, object* a5) { + return lean_apply_5(f, a1, a2, a3, a4, a5); +} +inline object* apply_6(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6) { + return lean_apply_6(f, a1, a2, a3, a4, a5, a6); +} +inline object* apply_7(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7) { + return lean_apply_7(f, a1, a2, a3, a4, a5, a6, a7); +} +inline object* apply_8(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8) { + return lean_apply_8(f, a1, a2, a3, a4, a5, a6, a7, a8); +} +inline object* apply_9(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8, object* a9) { + return lean_apply_9(f, a1, a2, a3, a4, a5, a6, a7, a8, a9); +} +inline object* apply_10(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8, object* a9, object* a10) { + return lean_apply_10(f, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10); +} +inline object* apply_11(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8, object* a9, object* a10, object* a11) { + return lean_apply_11(f, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11); +} +inline object* apply_12(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8, object* a9, object* a10, object* a11, object* a12) { + return lean_apply_12(f, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12); +} +inline object* apply_13(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8, object* a9, object* a10, object* a11, object* a12, object* a13) { + return lean_apply_13(f, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13); +} +inline object* apply_14(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8, object* a9, object* a10, object* a11, object* a12, object* a13, object* a14) { + return lean_apply_14(f, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14); +} +inline object* apply_15(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8, object* a9, object* a10, object* a11, object* a12, object* a13, object* a14, object* a15) { + return lean_apply_15(f, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15); +} +inline object* apply_16(object* f, object* a1, object* a2, object* a3, object* a4, object* a5, object* a6, object* a7, object* a8, object* a9, object* a10, object* a11, object* a12, object* a13, object* a14, object* a15, object* a16) { + return lean_apply_16(f, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16); +} +inline object* apply_n(object* f, unsigned n, object** args) { return lean_apply_n(f, n, args); } +// pre: n > 16 +inline object* apply_m(object* f, unsigned n, object** args) { return lean_apply_m(f, n, args); } + +// ======================================= +// Fixpoint + +inline obj_res fixpoint(obj_arg rec, obj_arg a) { return lean_fixpoint(rec, a); } +inline obj_res fixpoint2(obj_arg rec, obj_arg a1, obj_arg a2) { return lean_fixpoint2(rec, a1, a2); } +inline obj_res fixpoint3(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3) { return lean_fixpoint3(rec, a1, a2, a3); } +inline obj_res fixpoint4(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) { return lean_fixpoint4(rec, a1, a2, a3, a4); } +inline obj_res fixpoint5(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) { + return lean_fixpoint5(rec, a1, a2, a3, a4, a5); +} +inline obj_res fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) { + return lean_fixpoint6(rec, a1, a2, a3, a4, a5, a6); +} + +// ======================================= +// MPZ + +object * alloc_mpz(mpz const &); +inline mpz_object * to_mpz(object * o) { lean_assert(is_mpz(o)); return (mpz_object*)o; } + +// ======================================= +// Array of objects + +inline size_t array_capacity(object * o) { return lean_array_capacity(o); } +inline object ** array_cptr(object * o) { return lean_array_cptr(o); } +inline obj_res alloc_array(size_t size, size_t capacity) { return lean_alloc_array(size, capacity); } +object * array_mk_empty(); +inline size_t array_size(b_obj_arg o) { return lean_array_size(o); } +inline void array_set_size(u_obj_arg o, size_t sz) { lean_array_set_size(o, sz); } +inline b_obj_res array_get(b_obj_arg o, size_t i) { return lean_array_get_core(o, i); } +inline void array_set(u_obj_arg o, size_t i, obj_arg v) { lean_array_set_core(o, i, v); } +inline object * array_sz(obj_arg a) { return lean_array_sz(a); } +inline object * array_get_size(b_obj_arg a) { return lean_array_get_size(a); } +inline object * mk_empty_array() { return lean_mk_empty_array(); } +inline object * mk_empty_array(b_obj_arg capacity) { return lean_mk_empty_array_with_capacity(capacity); } +inline object * array_uget(b_obj_arg a, usize i) { return lean_array_uget(a, i); } +inline obj_res array_fget(b_obj_arg a, b_obj_arg i) { return lean_array_fget(a, i); } +inline object * array_get(obj_arg def_val, b_obj_arg a, b_obj_arg i) { return lean_array_get(def_val, a, i); } +inline obj_res copy_array(obj_arg a, bool expand = false) { return lean_copy_expand_array(a, expand); } +inline object * array_uset(obj_arg a, usize i, obj_arg v) { return lean_array_uset(a, i, v); } +inline object * array_fset(obj_arg a, b_obj_arg i, obj_arg v) { return lean_array_fset(a, i, v); } +inline object * array_set(obj_arg a, b_obj_arg i, obj_arg v) { return lean_array_set(a, i, v); } +inline object * array_pop(obj_arg a) { return lean_array_pop(a); } +inline object * array_uswap(obj_arg a, usize i, usize j) { return lean_array_uswap(a, i, j); } +inline object * array_fswap(obj_arg a, b_obj_arg i, b_obj_arg j) { return lean_array_fswap(a, i, j); } +inline object * array_swap(obj_arg a, b_obj_arg i, b_obj_arg j) { return lean_array_swap(a, i, j); } +inline object * array_push(obj_arg a, obj_arg v) { return lean_array_push(a, v); } +inline object * mk_array(obj_arg n, obj_arg v) { return lean_mk_array(n, v); } + +// ======================================= +// Array of scalars + +inline obj_res alloc_sarray(unsigned elem_size, size_t size, size_t capacity) { return lean_alloc_sarray(elem_size, size, capacity); } +inline size_t sarray_size(b_obj_arg o) { return lean_sarray_size(o); } +inline void sarray_set_size(u_obj_arg o, size_t sz) { lean_sarray_set_size(o, sz); } +inline unsigned sarray_elem_size(object * o) { return lean_sarray_elem_size(o); } +inline size_t sarray_capacity(object * o) { return lean_sarray_capacity(o); } +inline uint8 * sarray_cptr(object * o) { return lean_sarray_cptr(o); } + +// ======================================= +// ByteArray + +inline obj_res byte_array_mk(obj_arg a) { return lean_byte_array_mk(a); } +inline obj_res byte_array_data(obj_arg a) { return lean_byte_array_data(a); } +inline obj_res copy_byte_array(obj_arg a) { return lean_copy_byte_array(a); } +inline obj_res mk_empty_byte_array(b_obj_arg capacity) { return lean_mk_empty_byte_array(capacity); } +inline obj_res byte_array_size(b_obj_arg a) { return lean_byte_array_size(a); } +inline uint8 byte_array_get(b_obj_arg a, b_obj_arg i) { return lean_byte_array_get(a, i); } +inline obj_res byte_array_push(obj_arg a, uint8 b) { return lean_byte_array_push(a, b); } +inline obj_res byte_array_set(obj_arg a, b_obj_arg i, uint8 b) { return lean_byte_array_set(a, i, b); } + +// ======================================= +// String + +inline size_t string_capacity(object * o) { return lean_string_capacity(o); } +inline uint32 char_default_value() { return lean_char_default_value(); } +inline obj_res alloc_string(size_t size, size_t capacity, size_t len) { return lean_alloc_string(size, capacity, len); } +inline obj_res mk_string(char const * s) { return lean_mk_string(s); } +obj_res mk_string(std::string const & s); +std::string string_to_std(b_obj_arg o); +inline char const * string_cstr(b_obj_arg o) { return lean_string_cstr(o); } +inline size_t string_size(b_obj_arg o) { return lean_string_size(o); } +inline size_t string_len(b_obj_arg o) { return lean_string_len(o); } +inline obj_res string_push(obj_arg s, uint32 c) { return lean_string_push(s, c); } +inline obj_res string_append(obj_arg s1, b_obj_arg s2) { return lean_string_append(s1, s2); } +inline obj_res string_length(b_obj_arg s) { return lean_string_length(s); } +inline obj_res string_mk(obj_arg cs) { return lean_string_mk(cs); } +inline obj_res string_data(obj_arg s) { return lean_string_data(s); } +inline uint32 string_utf8_get(b_obj_arg s, b_obj_arg i) { return lean_string_utf8_get(s, i); } +inline obj_res string_utf8_next(b_obj_arg s, b_obj_arg i) { return lean_string_utf8_next(s, i); } +inline obj_res string_utf8_prev(b_obj_arg s, b_obj_arg i) { return lean_string_utf8_prev(s, i); } +inline obj_res string_utf8_set(obj_arg s, b_obj_arg i, uint32 c) { return lean_string_utf8_set(s, i, c); } +inline uint8 string_utf8_at_end(b_obj_arg s, b_obj_arg i) { return lean_string_utf8_at_end(s, i); } +inline obj_res string_utf8_extract(b_obj_arg s, b_obj_arg b, b_obj_arg e) { return lean_string_utf8_extract(s, b, e); } +inline obj_res string_utf8_byte_size(b_lean_obj_arg s) { return lean_string_utf8_byte_size(s); } +inline bool string_eq(b_obj_arg s1, b_obj_arg s2) { return lean_string_eq(s1, s2); } +bool string_eq(b_obj_arg s1, char const * s2); +inline bool string_ne(b_obj_arg s1, b_obj_arg s2) { return lean_string_ne(s1, s2); } +inline bool string_lt(b_obj_arg s1, b_obj_arg s2) { return lean_string_lt(s1, s2); } +inline uint8 string_dec_eq(b_obj_arg s1, b_obj_arg s2) { return string_eq(s1, s2); } +inline uint8 string_dec_lt(b_obj_arg s1, b_obj_arg s2) { return string_lt(s1, s2); } +inline usize string_hash(b_obj_arg s) { return lean_string_hash(s); } + +// ======================================= +// Thunks + +inline obj_res mk_thunk(obj_arg c) { return lean_mk_thunk(c); } +inline obj_res thunk_pure(obj_arg v) { return lean_thunk_pure(v); } +inline b_obj_res thunk_get(b_obj_arg t) { return lean_thunk_get(t); } +inline obj_res thunk_get_own(b_obj_arg t) { return lean_thunk_get_own(t); } +inline obj_res thunk_map(obj_arg f, obj_arg t) { return lean_thunk_map(f, t); } +inline obj_res thunk_bind(obj_arg x, obj_arg f) { return lean_thunk_bind(x, f); } + +// ======================================= +// Tasks + +/* If num_workers == 0, then tasks primitives will just create thunks. + It must not be used if task objects have already been created. */ +class scoped_task_manager { +public: + scoped_task_manager(unsigned num_workers); + ~scoped_task_manager(); +}; + +inline obj_res mk_task(obj_arg c, unsigned prio = 0) { return lean_mk_task_with_prio(c, prio); } +inline obj_res task_pure(obj_arg a) { return lean_task_pure(a); } +inline obj_res task_bind(obj_arg x, obj_arg f, unsigned prio = 0) { return lean_task_bind_with_prio(x, f, prio); } +inline obj_res task_map(obj_arg f, obj_arg t, unsigned prio = 0) { return lean_task_map_with_prio(f, t, prio); } +inline b_obj_res task_get(b_obj_arg t) { return lean_task_get(t); } + +/* primitive for implementing `io.check_interrupt : io bool` */ +inline bool io_check_interrupt_core() { return lean_io_check_interrupt_core(); } +/* primitive for implementing `io.request_interrupt : task A -> io unit` */ +inline void io_request_interrupt_core(b_obj_arg t) { return lean_io_request_interrupt_core(t); } +/* primitive for implementing `io.has_finished : task A -> io unit` */ +inline bool io_has_finished_core(b_obj_arg t) { return lean_io_has_finished_core(t); } +/* primitive for implementing `io.wait_any : list (task A) -> io (task A) */ +inline b_obj_res io_wait_any_core(b_obj_arg task_list) { return lean_io_wait_any_core(task_list); } + +// ======================================= +// External + +inline object * alloc_external(external_object_class * cls, void * data) { return lean_alloc_external(cls, data); } +inline external_object_class * external_class(object * o) { return lean_get_external_class(o); } +inline void * external_data(object * o) { return lean_get_external_data(o); } + +// ======================================= +// Option + +inline obj_res mk_option_none() { return box(0); } +inline obj_res mk_option_some(obj_arg v) { obj_res r = alloc_cnstr(1, 1, 0); cnstr_set(r, 0, v); return r; } + +// ======================================= +// Natural numbers + +inline mpz const & mpz_value(b_obj_arg o) { return ((mpz_object*)o)->m_value; } +object * mpz_to_nat_core(mpz const & m); +inline object * mk_nat_obj_core(mpz const & m) { return mpz_to_nat_core(m); } +inline obj_res mk_nat_obj(mpz const & m) { + if (m.is_size_t() && m.get_size_t() <= LEAN_MAX_SMALL_NAT) + return box(m.get_size_t()); + else + return mk_nat_obj_core(m); +} +inline obj_res usize_to_nat(usize n) { return lean_usize_to_nat(n); } +inline obj_res mk_nat_obj(unsigned n) { return lean_unsigned_to_nat(n); } +inline obj_res uint64_to_nat(uint64 n) { return lean_uint64_to_nat(n); } +inline obj_res nat_succ(b_obj_arg a) { return lean_nat_succ(a); } +inline obj_res nat_add(b_obj_arg a1, b_obj_arg a2) { return lean_nat_add(a1, a2); } +inline obj_res nat_sub(b_obj_arg a1, b_obj_arg a2) { return lean_nat_sub(a1, a2); } +inline obj_res nat_mul(b_obj_arg a1, b_obj_arg a2) { return lean_nat_mul(a1, a2); } +inline obj_res nat_div(b_obj_arg a1, b_obj_arg a2) { return lean_nat_div(a1, a2); } +inline obj_res nat_mod(b_obj_arg a1, b_obj_arg a2) { return lean_nat_mod(a1, a2); } +inline bool nat_eq(b_obj_arg a1, b_obj_arg a2) { return lean_nat_eq(a1, a2); } +inline uint8 nat_dec_eq(b_obj_arg a1, b_obj_arg a2) { return lean_nat_dec_eq(a1, a2); } +inline bool nat_ne(b_obj_arg a1, b_obj_arg a2) { return lean_nat_ne(a1, a2); } +inline bool nat_le(b_obj_arg a1, b_obj_arg a2) { return lean_nat_le(a1, a2); } +inline uint8 nat_dec_le(b_obj_arg a1, b_obj_arg a2) { return lean_nat_dec_le(a1, a2); } +inline bool nat_lt(b_obj_arg a1, b_obj_arg a2) { return lean_nat_lt(a1, a2); } +inline uint8 nat_dec_lt(b_obj_arg a1, b_obj_arg a2) { return lean_nat_dec_lt(a1, a2); } +inline obj_res nat_land(b_obj_arg a1, b_obj_arg a2) { return lean_nat_land(a1, a2); } +inline obj_res nat_lor(b_obj_arg a1, b_obj_arg a2) { return lean_nat_lor(a1, a2); } +inline obj_res nat_lxor(b_obj_arg a1, b_obj_arg a2) { return lean_nat_lxor(a1, a2); } + +// ======================================= +// Integers +object * mk_int_obj_core(mpz const & m); +inline obj_res mk_int_obj(mpz const & m) { + if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT) + return mk_int_obj_core(m); + else + return box(static_cast(m.get_int())); +} +inline obj_res mk_int_obj(int n) { return lean_int_to_int(n); } +inline obj_res mk_int_obj(int64 n) { return lean_int64_to_int(n); } +inline obj_res nat2int(obj_arg a) { return lean_nat_to_int(a); } +inline obj_res int_neg(b_obj_arg a) { return lean_int_neg(a); } +inline obj_res int_neg_succ_of_nat(obj_arg a) { return lean_int_neg_succ_of_nat(a); } +inline obj_res int_add(b_obj_arg a1, b_obj_arg a2) { return lean_int_add(a1, a2); } +inline obj_res int_sub(b_obj_arg a1, b_obj_arg a2) { return lean_int_sub(a1, a2); } +inline obj_res int_mul(b_obj_arg a1, b_obj_arg a2) { return lean_int_mul(a1, a2); } +inline obj_res int_div(b_obj_arg a1, b_obj_arg a2) { return lean_int_div(a1, a2); } +inline obj_res int_mod(b_obj_arg a1, b_obj_arg a2) { return lean_int_mod(a1, a2); } +inline bool int_eq(b_obj_arg a1, b_obj_arg a2) { return lean_int_eq(a1, a2); } +inline bool int_ne(b_obj_arg a1, b_obj_arg a2) { return lean_int_ne(a1, a2); } +inline bool int_le(b_obj_arg a1, b_obj_arg a2) { return lean_int_le(a1, a2); } +inline bool int_lt(b_obj_arg a1, b_obj_arg a2) { return lean_int_lt(a1, a2); } +inline obj_res nat_abs(b_obj_arg i) { return lean_nat_abs(i); } +inline uint8 int_dec_eq(b_obj_arg a1, b_obj_arg a2) { return lean_int_dec_eq(a1, a2); } +inline uint8 int_dec_le(b_obj_arg a1, b_obj_arg a2) { return lean_int_dec_le(a1, a2); } +inline uint8 int_dec_lt(b_obj_arg a1, b_obj_arg a2) { return lean_int_dec_lt(a1, a2); } +inline uint8 int_dec_nonneg(b_obj_arg a) { return lean_int_dec_nonneg(a); } + +// ======================================= +// Boxing + +inline obj_res box_uint32(unsigned v) { return lean_box_uint32(v); } +inline unsigned unbox_uint32(b_obj_arg o) { return lean_unbox_uint32(o); } +inline obj_res box_uint64(unsigned long long v) { return lean_box_uint64(v); } +inline unsigned long long unbox_uint64(b_obj_arg o) { return lean_unbox_uint64(o); } +inline obj_res box_float(double v) { return lean_box_float(v); } +inline double unbox_float(b_obj_arg o) { return lean_unbox_float(o); } +inline obj_res box_size_t(size_t v) { return lean_box_usize(v); } +inline size_t unbox_size_t(b_obj_arg o) { return lean_unbox_usize(o); } + +// ======================================= +// uint8 +inline uint8 uint8_of_nat(b_obj_arg a) { return lean_uint8_of_nat(a); } +inline obj_res uint8_to_nat(uint8 a) { return lean_uint8_to_nat(a); } +inline uint8 uint8_add(uint8 a1, uint8 a2) { return lean_uint8_add(a1, a2); } +inline uint8 uint8_sub(uint8 a1, uint8 a2) { return lean_uint8_sub(a1, a2); } +inline uint8 uint8_mul(uint8 a1, uint8 a2) { return lean_uint8_mul(a1, a2); } +inline uint8 uint8_div(uint8 a1, uint8 a2) { return lean_uint8_div(a1, a2); } +inline uint8 uint8_mod(uint8 a1, uint8 a2) { return lean_uint8_mod(a1, a2); } +inline uint8 uint8_modn(uint8 a1, b_obj_arg a2) { return lean_uint8_modn(a1, a2); } +inline uint8 uint8_dec_eq(uint8 a1, uint8 a2) { return lean_uint8_dec_eq(a1, a2); } +inline uint8 uint8_dec_lt(uint8 a1, uint8 a2) { return lean_uint8_dec_lt(a1, a2); } +inline uint8 uint8_dec_le(uint8 a1, uint8 a2) { return lean_uint8_dec_le(a1, a2); } + +// ======================================= +// uint16 +inline uint16 uint16_of_nat(b_obj_arg a) { return lean_uint16_of_nat(a); } +inline obj_res uint16_to_nat(uint16 a) { return lean_uint16_to_nat(a); } +inline uint16 uint16_add(uint16 a1, uint16 a2) { return lean_uint16_add(a1, a2); } +inline uint16 uint16_sub(uint16 a1, uint16 a2) { return lean_uint16_sub(a1, a2); } +inline uint16 uint16_mul(uint16 a1, uint16 a2) { return lean_uint16_mul(a1, a2); } +inline uint16 uint16_div(uint16 a1, uint16 a2) { return lean_uint16_div(a1, a2); } +inline uint16 uint16_mod(uint16 a1, uint16 a2) { return lean_uint16_mod(a1, a2); } +inline uint16 uint16_modn(uint16 a1, b_obj_arg a2) { return lean_uint16_modn(a1, a2); } +inline uint16 uint16_dec_eq(uint16 a1, uint16 a2) { return lean_uint16_dec_eq(a1, a2); } +inline uint16 uint16_dec_lt(uint16 a1, uint16 a2) { return lean_uint16_dec_lt(a1, a2); } +inline uint16 uint16_dec_le(uint16 a1, uint16 a2) { return lean_uint16_dec_le(a1, a2); } + +// ======================================= +// uint32 +inline uint32 uint32_of_nat(b_obj_arg a) { return lean_uint32_of_nat(a); } +inline obj_res uint32_to_nat(uint32 a) { return lean_uint32_to_nat(a); } +inline uint32 uint32_add(uint32 a1, uint32 a2) { return lean_uint32_add(a1, a2); } +inline uint32 uint32_sub(uint32 a1, uint32 a2) { return lean_uint32_sub(a1, a2); } +inline uint32 uint32_mul(uint32 a1, uint32 a2) { return lean_uint32_mul(a1, a2); } +inline uint32 uint32_div(uint32 a1, uint32 a2) { return lean_uint32_div(a1, a2); } +inline uint32 uint32_mod(uint32 a1, uint32 a2) { return lean_uint32_mod(a1, a2); } +inline uint32 uint32_modn(uint32 a1, b_obj_arg a2) { return lean_uint32_modn(a1, a2); } +inline uint32 uint32_dec_eq(uint32 a1, uint32 a2) { return lean_uint32_dec_eq(a1, a2); } +inline uint32 uint32_dec_lt(uint32 a1, uint32 a2) { return lean_uint32_dec_lt(a1, a2); } +inline uint32 uint32_dec_le(uint32 a1, uint32 a2) { return lean_uint32_dec_le(a1, a2); } + +// ======================================= +// uint64 +inline uint64 uint64_of_nat(b_obj_arg a) { return lean_uint64_of_nat(a); } +inline uint64 uint64_add(uint64 a1, uint64 a2) { return lean_uint64_add(a1, a2); } +inline uint64 uint64_sub(uint64 a1, uint64 a2) { return lean_uint64_sub(a1, a2); } +inline uint64 uint64_mul(uint64 a1, uint64 a2) { return lean_uint64_mul(a1, a2); } +inline uint64 uint64_div(uint64 a1, uint64 a2) { return lean_uint64_div(a1, a2); } +inline uint64 uint64_mod(uint64 a1, uint64 a2) { return lean_uint64_mod(a1, a2); } +inline uint64 uint64_modn(uint64 a1, b_obj_arg a2) { return lean_uint64_modn(a1, a2); } +inline uint64 uint64_dec_eq(uint64 a1, uint64 a2) { return lean_uint64_dec_eq(a1, a2); } +inline uint64 uint64_dec_lt(uint64 a1, uint64 a2) { return lean_uint64_dec_lt(a1, a2); } +inline uint64 uint64_dec_le(uint64 a1, uint64 a2) { return lean_uint64_dec_le(a1, a2); } + +// ======================================= +// usize +inline usize usize_of_nat(b_obj_arg a) { return lean_usize_of_nat(a); } +inline usize usize_add(usize a1, usize a2) { return lean_usize_add(a1, a2); } +inline usize usize_sub(usize a1, usize a2) { return lean_usize_sub(a1, a2); } +inline usize usize_mul(usize a1, usize a2) { return lean_usize_mul(a1, a2); } +inline usize usize_div(usize a1, usize a2) { return lean_usize_div(a1, a2); } +inline usize usize_mod(usize a1, usize a2) { return lean_usize_mod(a1, a2); } +inline usize usize_modn(usize a1, b_obj_arg a2) { return lean_usize_modn(a1, a2); } +inline usize usize_dec_eq(usize a1, usize a2) { return lean_usize_dec_eq(a1, a2); } +inline usize usize_dec_lt(usize a1, usize a2) { return lean_usize_dec_lt(a1, a2); } +inline usize usize_dec_le(usize a1, usize a2) { return lean_usize_dec_le(a1, a2); } +inline usize usize_mix_hash(usize a1, usize a2) { return lean_usize_mix_hash(a1, a2); } + +// ======================================= +// debugging helper functions +inline object * dbg_trace(obj_arg s, obj_arg fn) { return lean_dbg_trace(s, fn); } +inline object * dbg_sleep(uint32 ms, obj_arg fn) { return lean_dbg_sleep(ms, fn); } +inline object * dbg_trace_if_shared(obj_arg s, obj_arg a) { return lean_dbg_trace_if_shared(s, a); } + +// ======================================= +// IO helper functions +inline obj_res io_mk_world() { return lean_io_mk_world(); } +inline bool io_result_is_ok(b_obj_arg r) { return lean_io_result_is_ok(r); } +inline bool io_result_is_error(b_obj_arg r) { return lean_io_result_is_error(r); } +inline b_obj_res io_result_get_value(b_obj_arg r) { return lean_io_result_get_value(r); } +inline b_obj_res io_result_get_error(b_obj_arg r) { return lean_io_result_get_error(r); } +inline void io_result_show_error(b_obj_arg r) { return lean_io_result_show_error(r); } +inline void io_mark_end_initialization() { return lean_io_mark_end_initialization(); } + +// ======================================= +// IO ref primitives +inline obj_res io_mk_ref(obj_arg v, obj_arg w) { return lean_io_mk_ref(v, w); } +inline obj_res io_ref_get(b_obj_arg r, obj_arg w) { return lean_io_ref_get(r, w); } +inline obj_res io_ref_set(b_obj_arg r, obj_arg v, obj_arg w) { return lean_io_ref_set(r, v, w); } +inline obj_res io_ref_reset(b_obj_arg r, obj_arg w) { return lean_io_ref_reset(r, w); } +inline obj_res io_ref_swap(b_obj_arg r, obj_arg v, obj_arg w) { return lean_io_ref_swap(r, v, w); } + +// ======================================= +// Module initialization/finalization +void initialize_object(); +void finalize_object(); +} diff --git a/src/include/lean/optional.h b/src/include/lean/optional.h new file mode 100644 index 0000000000..9c1ba11727 --- /dev/null +++ b/src/include/lean/optional.h @@ -0,0 +1,155 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include + +namespace lean { +/** + \brief Simple optional template. This is a naive replacement for C++14 optional. + We will delete it as soon optional is supported in g++ and clang++. +*/ +template +class optional { + bool m_some; + union { + T m_value; + }; +public: + optional():m_some(false) {} + optional(optional & other):m_some(other.m_some) { + if (m_some) + new (&m_value) T(other.m_value); + } + optional(optional const & other):m_some(other.m_some) { + if (m_some) + new (&m_value) T(other.m_value); + } + optional(optional && other):m_some(other.m_some) { + if (other.m_some) + new (&m_value) T(std::forward(other.m_value)); + } + explicit optional(T const & v):m_some(true) { + new (&m_value) T(v); + } + explicit optional(T && v):m_some(true) { + new (&m_value) T(std::forward(v)); + } + template + explicit optional(Args&&... args):m_some(true) { + new (&m_value) T(std::forward(args)...); + } + ~optional() { + if (m_some) + m_value.~T(); + } + + explicit operator bool() const { return m_some; } + T const * operator->() const { lean_assert(m_some); return &m_value; } + T * operator->() { lean_assert(m_some); return &m_value; } + T const & operator*() const { lean_assert(m_some); return m_value; } + T & operator*() { lean_assert(m_some); return m_value; } + T const & value() const { lean_assert(m_some); return m_value; } + T & value() { lean_assert(m_some); return m_value; } + + T const & value_or(T const & default_value) const { + return m_some ? m_value : default_value; + } + + template + void emplace(Args&&... args) { + if (m_some) + m_value.~T(); + m_some = true; + new (&m_value) T(args...); + } + + optional& operator=(optional const & other) { + if (this == &other) + return *this; + if (m_some) + m_value.~T(); + m_some = other.m_some; + if (m_some) + new (&m_value) T(other.m_value); + return *this; + } + optional& operator=(optional && other) { + lean_assert(this != &other); + if (m_some) + m_value.~T(); + m_some = other.m_some; + if (m_some) + new (&m_value) T(std::forward(other.m_value)); + return *this; + } + optional& operator=(T const & other) { + if (m_some) + m_value.~T(); + m_some = true; + new (&m_value) T(other); + return *this; + } + optional& operator=(T && other) { + if (m_some) + m_value.~T(); + m_some = true; + new (&m_value) T(std::forward(other)); + return *this; + } + + friend bool operator==(optional const & o1, optional const & o2) { + if (o1.m_some != o2.m_some) + return false; + else + return !o1.m_some || o1.m_value == o2.m_value; + } + + friend bool operator!=(optional const & o1, optional const & o2) { + return !operator==(o1, o2); + } +}; + +template optional some(T const & t) { return optional(t); } +template optional some(T && t) { return optional(std::forward(t)); } + +// The following macro creates a template specialization optional

, where P +// is an intrusive smart pointer that does not let "customers" point to nullptr. +// That is, if a customer have 'P x', then x is not a pointer to nullptr. +// Requirements: +// - P must declare optional

as a friend. +// - P must handle the nullptr case even if it does not let "customers" point to nullptr +// - P must have a field m_ptr a pointer to the actual value. +#define SPECIALIZE_OPTIONAL_FOR_SMART_PTR(P) \ +template<> class optional

{ \ + P m_value; \ +public: \ + optional():m_value(nullptr) {} \ + optional(optional const & other):m_value(other.m_value) {} \ + optional(optional && other):m_value(std::forward

(other.m_value)) {} \ + explicit optional(P const & v):m_value(v) {} \ + explicit optional(P && v):m_value(std::forward

(v)) {} \ + \ + explicit operator bool() const { return m_value.m_ptr != nullptr; } \ + P const * operator->() const { lean_assert(m_value.m_ptr); return &m_value; } \ + P * operator->() { lean_assert(m_value.m_ptr); return &m_value; } \ + P const & operator*() const { lean_assert(m_value.m_ptr); return m_value; } \ + P & operator*() { lean_assert(m_value.m_ptr); return m_value; } \ + P const & value() const { lean_assert(m_value.m_ptr); return m_value; } \ + P & value() { lean_assert(m_value.m_ptr); return m_value; } \ + optional & operator=(optional const & other) { m_value = other.m_value; return *this; } \ + optional& operator=(optional && other) { m_value = std::forward

(other.m_value); return *this; } \ + optional& operator=(P const & other) { m_value = other; return *this; } \ + optional& operator=(P && other) { m_value = std::forward

(other); return *this; } \ + friend bool operator==(optional const & o1, optional const & o2) { \ + return static_cast(o1) == static_cast(o2) && (!o1 || o1.m_value == o2.m_value); \ + } \ + friend bool operator!=(optional const & o1, optional const & o2) { \ + return !operator==(o1, o2); \ + } \ +}; +} diff --git a/src/include/lean/platform.h b/src/include/lean/platform.h new file mode 100644 index 0000000000..9ce2488ab9 --- /dev/null +++ b/src/include/lean/platform.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +namespace lean { +void initialize_platform(); +void finalize_platform(); +} diff --git a/src/include/lean/serializer.h b/src/include/lean/serializer.h new file mode 100644 index 0000000000..345ef6eced --- /dev/null +++ b/src/include/lean/serializer.h @@ -0,0 +1,142 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace lean { +class serializer { + std::ostream & m_out; + std::unordered_map, std::equal_to> m_obj_table; + void write_constructor(object * o); + void write_closure(object * o); + void write_thunk(object * o); + void write_task(object * o); + void write_array(object * o); + void write_scalar_array(object * o); + void write_string_object(object * o); + void write_external(object * o); +public: + serializer(std::ostream & out):m_out(out) {} + ~serializer(); + void write_string(char const * str) { m_out.write(str, strlen(str) + 1); } + void write_string(std::string const & str) { write_string(str.c_str()); } + void write_unsigned_short(unsigned short i); + void write_unsigned(unsigned i); + void write_uint64(uint64 i); + void write_size_t(size_t i); + void write_int(int i); + void write_char(char c) { m_out.put(c); } + void write_bool(bool b) { m_out.put(b ? 1 : 0); } + void write_double(double b); + void write_mpz(mpz const & m); + void write_object(object * o); + void write_blob(std::string const &); +}; + +inline serializer & operator<<(serializer & s, char const * str) { s.write_string(str); return s; } +inline serializer & operator<<(serializer & s, std::string const & str) { s.write_string(str); return s; } +inline serializer & operator<<(serializer & s, unsigned i) { s.write_unsigned(i); return s; } +inline serializer & operator<<(serializer & s, uint64 i) { s.write_uint64(i); return s; } +inline serializer & operator<<(serializer & s, int i) { s.write_int(i); return s; } +inline serializer & operator<<(serializer & s, char c) { s.write_char(c); return s; } +inline serializer & operator<<(serializer & s, bool b) { s.write_bool(b); return s; } +inline serializer & operator<<(serializer & s, double b) { s.write_double(b); return s; } +inline serializer & operator<<(serializer & s, object * o) { s.write_object(o); return s; } + +class deserializer { + std::istream & m_in; + std::vector m_objs; + optional m_fname; + unsigned read_unsigned_ext(); + object * read_constructor(); + object * read_closure(); + object * read_thunk(); + object * read_task(); + object * read_array(); + object * read_scalar_array(); + object * read_string_object(); + object * read_external(); +public: + deserializer(std::istream & in):m_in(in) {} + deserializer(std::istream & in, optional const & fname):m_in(in), m_fname(fname) {} + ~deserializer(); + std::string read_string(); + unsigned read_unsigned() { + unsigned r = static_cast(m_in.get()); + return r < 255 ? r : read_unsigned_ext(); + } + uint64 read_uint64(); + size_t read_size_t(); + int read_int() { return read_unsigned(); } + char read_char() { return m_in.get(); } + bool read_bool() { return m_in.get() != 0; } + unsigned short read_unsigned_short(); + double read_double(); + mpz read_mpz(); + std::string read_blob(); + object * read_object(); + optional get_fname() const { return m_fname; } +}; + +inline deserializer & operator>>(deserializer & d, std::string & str) { str = d.read_string(); return d; } +inline deserializer & operator>>(deserializer & d, unsigned & i) { i = d.read_unsigned(); return d; } +inline deserializer & operator>>(deserializer & d, uint64 & i) { i = d.read_uint64(); return d; } +inline deserializer & operator>>(deserializer & d, int & i) { i = d.read_int(); return d; } +inline deserializer & operator>>(deserializer & d, char & c) { c = d.read_char(); return d; } +inline deserializer & operator>>(deserializer & d, bool & b) { b = d.read_bool(); return d; } +inline deserializer & operator>>(deserializer & d, double & b) { b = d.read_double(); return d; } + +class corrupted_stream_exception : public exception { +public: + corrupted_stream_exception(); +}; + +void initialize_serializer(); +void finalize_serializer(); + +template +serializer & write_optional(serializer & s, optional const & a) { + if (a) + s << true << *a; + else + s << false; + return s; +} + +template +optional read_optional(deserializer & d) { + if (d.read_bool()) { + T r; + d >> r; + return optional(r); + } else { + return optional(); + } +} + +template +serializer & operator<<(serializer & s, optional const & a) { + return write_optional(s, a); +} + +template +deserializer & operator>>(deserializer & d, optional & a) { + a = read_optional(d); + return d; +} + +inline serializer & operator<<(serializer & s, mpz const & n) { s.write_mpz(n); return s; } +inline deserializer & operator>>(deserializer & d, mpz & n) { n = d.read_mpz(); return d; } +} diff --git a/src/include/lean/sstream.h b/src/include/lean/sstream.h new file mode 100644 index 0000000000..6d5c6a6cc5 --- /dev/null +++ b/src/include/lean/sstream.h @@ -0,0 +1,19 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include + +namespace lean { +/** \brief Wrapper for std::ostringstream */ +class sstream { + std::ostringstream m_strm; +public: + std::string str() const { return m_strm.str(); } + template sstream & operator<<(T const & t) { m_strm << t; return *this; } +}; +} diff --git a/src/include/lean/stack_overflow.h b/src/include/lean/stack_overflow.h new file mode 100644 index 0000000000..1d09d6a80e --- /dev/null +++ b/src/include/lean/stack_overflow.h @@ -0,0 +1,25 @@ +/* +Copyright (c) 2020 Sebastian Ullrich. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sebastian Ullrich +*/ +#pragma once +#ifndef LEAN_WINDOWS +#include +#endif + +namespace lean { +class stack_guard { +#ifndef LEAN_WINDOWS + // We need a separate signal stack since we can't use the overflowed stack + stack_t m_signal_stack; +#endif +public: + stack_guard(); + ~stack_guard(); +}; + +void initialize_stack_overflow(); +void finalize_stack_overflow(); +} diff --git a/src/include/lean/stackinfo.h b/src/include/lean/stackinfo.h new file mode 100644 index 0000000000..8469406bcc --- /dev/null +++ b/src/include/lean/stackinfo.h @@ -0,0 +1,31 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include + +namespace lean { +#if defined(LEAN_USE_SPLIT_STACK) +// If we are using split stacks, we don't need to check anything +inline void check_stack(char const * ) { } +inline size_t get_stack_size(bool ) { return 8192*1024; } +inline void save_stack_info(bool = true) {} +inline size_t get_used_stack_size() { return 0; } +inline size_t get_available_stack_size() { return 8192*1024; } +#else +size_t get_stack_size(bool main); +void save_stack_info(bool main = true); +size_t get_used_stack_size(); +size_t get_available_stack_size(); +/** + \brief Throw an exception if the amount of available stack space is low. + + \remark The optional argument \c component_name is used to inform the + user which module is the potential offender. +*/ +void check_stack(char const * component_name); +#endif +} diff --git a/src/include/lean/thread.h b/src/include/lean/thread.h new file mode 100644 index 0000000000..cc1b14ec00 --- /dev/null +++ b/src/include/lean/thread.h @@ -0,0 +1,249 @@ +/* +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include + +#ifndef LEAN_STACK_BUFFER_SPACE +#define LEAN_STACK_BUFFER_SPACE 128*1024 // 128 Kb +#endif + +namespace lean { +namespace chrono = std::chrono; +}; + +#if defined(LEAN_MULTI_THREAD) +#include +#include +#include +#include +#define LEAN_THREAD_LOCAL thread_local + +namespace lean { +using std::thread; +using std::mutex; +using std::recursive_mutex; +using std::atomic; +using std::atomic_bool; +using std::atomic_ushort; +using std::atomic_uint; +using std::atomic_uchar; +using std::condition_variable; +using std::lock_guard; +using std::unique_lock; +using std::atomic_load; +using std::atomic_load_explicit; +using std::atomic_fetch_add_explicit; +using std::atomic_fetch_sub_explicit; +using std::memory_order_relaxed; +using std::memory_order_release; +using std::memory_order_acquire; +using std::memory_order_acq_rel; +using std::memory_order_seq_cst; +using std::atomic_thread_fence; +namespace this_thread = std::this_thread; +inline unsigned hardware_concurrency() { return std::thread::hardware_concurrency(); } +/** Simple thread class that allows us to set the thread stack size. + We implement it using pthreads on OSX/Linux and WinThreads on Windows. */ +class lthread { + static size_t m_thread_stack_size; + struct imp; + std::unique_ptr m_imp; +public: + lthread(std::function const & p); + ~lthread(); + void join(); + static void set_thread_stack_size(size_t sz); + static size_t get_thread_stack_size(); +}; +} + +#else +// NO MULTI THREADING SUPPORT +#include +#include +#define LEAN_THREAD_LOCAL +namespace lean { +constexpr int memory_order_relaxed = 0; +constexpr int memory_order_release = 0; +constexpr int memory_order_acquire = 0; +constexpr int memory_order_acq_rel = 0; +constexpr int memory_order_seq_cst = 0; +inline void atomic_thread_fence(int ) {} +template +class atomic { + T m_value; +public: + atomic(T const & v = T()):m_value(v) {} + atomic(T && v):m_value(std::forward(v)) {} + atomic(atomic const & v):m_value(v.m_value) {} + atomic(atomic && v):m_value(std::forward(v.m_value)) {} + atomic & operator=(T const & v) { m_value = v; return *this; } + atomic & operator=(T && v) { m_value = std::forward(v); return *this; } + atomic & operator=(atomic const & v) { m_value = v.m_value; return *this; } + atomic & operator=(atomic && v) { m_value = std::forward(v.m_value); return *this; } + operator T() const { return m_value; } + void store(T const & v) { m_value = v; } + T load() const { return m_value; } + atomic & operator|=(T const & v) { m_value |= v; return *this; } + atomic & operator+=(T const & v) { m_value += v; return *this; } + atomic & operator-=(T const & v) { m_value -= v; return *this; } + atomic & operator++() { ++m_value; return *this; } + atomic operator++(int ) { atomic tmp(*this); ++m_value; return tmp; } + atomic & operator--() { --m_value; return *this; } + atomic operator--(int ) { atomic tmp(*this); --m_value; return tmp; } + friend T atomic_load(atomic const * a) { return a->m_value; } + friend T atomic_load_explicit(atomic const * a, int) { return a->m_value; } + friend T atomic_fetch_add_explicit(atomic * a, T const & v, int ) { T r(a->m_value); a->m_value += v; return r; } + friend T atomic_fetch_sub_explicit(atomic * a, T const & v, int ) { T r(a->m_value); a->m_value -= v; return r; } + T exchange(T desired) { T old = m_value; m_value = desired; return old; } + bool compare_exchange_strong(T & expected, T desired) { + if (m_value == expected) { + m_value = desired; + return true; + } else { + expected = m_value; + return false; + } + } +}; +typedef atomic atomic_ushort; +typedef atomic atomic_uchar; +typedef atomic atomic_bool; +typedef atomic atomic_uint; +class thread { +public: + thread() {} + template + thread(Function && fun, Args &&... args) { + fun(std::forward(args)...); + } + typedef unsigned id; + bool joinable() const { return true; } + void join() {} +}; +class lthread { +public: + lthread(std::function const & p) { p(); } + ~lthread() {} + void join() {} + static void set_thread_stack_size(size_t) {} + static size_t get_thread_stack_size() { return 0; } +}; +class this_thread { +public: + static void sleep_for(chrono::milliseconds const &) {} + static thread::id get_id() { return 0; } + static void yield() {} +}; +class mutex { +public: + void lock() {} + void unlock() {} +}; +class recursive_mutex { +public: + void lock() {} + void unlock() {} +}; +class condition_variable { +public: + template void wait(Lock const &) {} + template void wait(Lock const &, F) {} + template void wait_for(Lock const &, chrono::milliseconds const &) {} + void notify_all() {} + void notify_one() {} +}; +template class lock_guard { +public: + lock_guard(T const &) {} + ~lock_guard() {} +}; +template class unique_lock { +public: + unique_lock(T const &) {} + ~unique_lock() {} + void lock() {} + void unlock() {} +}; +inline unsigned hardware_concurrency() { return 1; } +} +#endif + +#ifdef _MSC_VER +#define LEAN_THREAD_PTR(T, V) static __declspec(thread) T * V = nullptr +#define LEAN_THREAD_EXTERN_PTR(T, V) extern __declspec(thread) T * V +#define LEAN_THREAD_GLOBAL_PTR(T, V) __declspec(thread) T * V = nullptr +#define LEAN_THREAD_VALUE(T, V, VAL) static __declspec(thread) T V = VAL +#else +#define LEAN_THREAD_PTR(T, V) static __thread T * V = nullptr +#define LEAN_THREAD_EXTERN_PTR(T, V) extern __thread T * V +#define LEAN_THREAD_GLOBAL_PTR(T, V) __thread T * V = nullptr +#define LEAN_THREAD_VALUE(T, V, VAL) static __thread T V = VAL +#endif + +#define MK_THREAD_LOCAL_GET(T, GETTER_NAME, DEF_VALUE) \ +LEAN_THREAD_PTR(T, GETTER_NAME ## _tlocal); \ +static void finalize_ ## GETTER_NAME(void * p) { \ + delete reinterpret_cast(p); \ + GETTER_NAME ## _tlocal = nullptr; \ +} \ +static T & GETTER_NAME() { \ + if (!GETTER_NAME ## _tlocal) { \ + GETTER_NAME ## _tlocal = new T(DEF_VALUE); \ + register_thread_finalizer(finalize_ ## GETTER_NAME, GETTER_NAME ## _tlocal); \ + } \ + return *(GETTER_NAME ## _tlocal); \ +} + +#define MK_THREAD_LOCAL_GET_DEF(T, GETTER_NAME) \ +LEAN_THREAD_PTR(T, GETTER_NAME ## _tlocal); \ +static void finalize_ ## GETTER_NAME(void * p) { \ + delete reinterpret_cast(p); \ + GETTER_NAME ## _tlocal = nullptr; \ +} \ +static T & GETTER_NAME() { \ + if (!GETTER_NAME ## _tlocal) { \ + GETTER_NAME ## _tlocal = new T(); \ + register_thread_finalizer(finalize_ ## GETTER_NAME, GETTER_NAME ## _tlocal); \ + } \ + return *(GETTER_NAME ## _tlocal); \ +} + +namespace lean { +void initialize_thread(); +void finalize_thread(); + +typedef void (*thread_finalizer)(void *); // NOLINT +void register_post_thread_finalizer(thread_finalizer fn, void * p); +void register_thread_finalizer(thread_finalizer fn, void * p); +void run_thread_finalizers(); +void run_post_thread_finalizers(); +void delete_thread_finalizer_manager(); + +bool in_thread_finalization(); + +/** + \brief Add \c fn to the list of functions used to reset thread local storage. + + This function must only be invoked during initialization. + + We use these functions to reset thread local storage that + contains cached data that may not be valid anymore. + + \see reset_thread_local */ +void register_thread_local_reset_fn(std::function fn); + +/** + \brief Reset thread local storage that contains cached + data that may not be valid anymore. + + We invoke this function before processing a command + and before executing a task. */ +void reset_thread_local(); +} diff --git a/src/include/lean/utf8.h b/src/include/lean/utf8.h new file mode 100644 index 0000000000..05797e992e --- /dev/null +++ b/src/include/lean/utf8.h @@ -0,0 +1,53 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include "util/buffer.h" + +namespace lean { +using uchar = unsigned char; + +bool is_utf8_next(unsigned char c); +unsigned get_utf8_size(unsigned char c); +/* Return the length of the null terminated string encoded using UTF8 */ +size_t utf8_strlen(char const * str); +/* Return the length of the string `str` encoded using UTF8. + `str` may contain null characters. */ +size_t utf8_strlen(std::string const & str); +/* Return the length of the string `str` encoded using UTF8. + `str` may contain null characters. */ +size_t utf8_strlen(char const * str, size_t sz); +optional utf8_char_pos(char const * str, size_t char_idx); +char const * get_utf8_last_char(char const * str); +std::string utf8_trim(std::string const & s); +unsigned utf8_to_unicode(uchar const * begin, uchar const * end); +inline unsigned utf8_to_unicode(char const * begin, char const * end) { + return utf8_to_unicode(reinterpret_cast(begin), + reinterpret_cast(end)); +} + +/* If `c` is the first byte of an utf-8 encoded unicode scalar value, + then return `some(n)` where `n` is the number of bytes needed to encode + the unicode scalar value. Otherwise, return `none` */ +optional get_utf8_first_byte_opt(unsigned char c); + +/* "Read" next unicode character starting at position i in a string using UTF-8 encoding. + Return the unicode character and update i. */ +unsigned next_utf8(std::string const & str, size_t & i); +unsigned next_utf8(char const * str, size_t size, size_t & i); + +/* Decode a UTF-8 encoded string `str` into unicode scalar values */ +void utf8_decode(std::string const & str, buffer & out); + +/* Push a unicode scalar value into a utf-8 encoded string */ +void push_unicode_scalar(std::string & s, unsigned code); + +/* Store unicode scalar value at `d`, `d` must point to memory with enough space to stroe `c`. + Return the number of bytes consumed. */ +unsigned push_unicode_scalar(char * d, unsigned code); +}