chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
8184d0fe52
commit
e28d13e0d4
288 changed files with 261 additions and 4463 deletions
|
|
@ -1,16 +0,0 @@
|
|||
/*
|
||||
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 <cstddef>
|
||||
|
||||
namespace lean {
|
||||
void init_thread_heap();
|
||||
void * alloc(size_t sz);
|
||||
void dealloc(void * o, size_t sz);
|
||||
void initialize_alloc();
|
||||
void finalize_alloc();
|
||||
}
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
/*
|
||||
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 <string>
|
||||
#include <lean/object.h>
|
||||
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();
|
||||
};
|
||||
}
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
/*
|
||||
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 <lean/object.h>
|
||||
namespace lean {
|
||||
object * curry(void * f, unsigned n, object ** as);
|
||||
}
|
||||
|
|
@ -1,81 +0,0 @@
|
|||
/*
|
||||
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 <functional>
|
||||
#include <vector>
|
||||
#include <unordered_map>
|
||||
#include <lean/object.h>
|
||||
|
||||
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<object*, object_offset, std::hash<object*>, std::equal_to<object*>> m_obj_table;
|
||||
std::unique_ptr<max_sharing_table> m_max_sharing_table;
|
||||
std::vector<object*> m_todo;
|
||||
std::vector<object_offset> m_tmp;
|
||||
void * m_begin;
|
||||
void * m_end;
|
||||
void * m_capacity;
|
||||
size_t capacity() const { return static_cast<char*>(m_capacity) - static_cast<char*>(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<char*>(m_end) - static_cast<char*>(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();
|
||||
};
|
||||
}
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
/*
|
||||
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
|
||||
|
|
@ -1,129 +0,0 @@
|
|||
/*
|
||||
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 <iostream>
|
||||
#include <typeinfo>
|
||||
#include <lean/exception.h>
|
||||
|
||||
#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<typename T> 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
|
||||
}
|
||||
|
|
@ -1,67 +0,0 @@
|
|||
/*
|
||||
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 <exception>
|
||||
#include <string>
|
||||
#include <memory>
|
||||
|
||||
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;
|
||||
};
|
||||
}
|
||||
|
|
@ -1,87 +0,0 @@
|
|||
/*
|
||||
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 <memory>
|
||||
#include <vector>
|
||||
#include <lean/thread.h>
|
||||
#include <lean/debug.h>
|
||||
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<typename T>
|
||||
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<std::unique_ptr<extension>> m_extensions;
|
||||
public:
|
||||
template<typename... Args>
|
||||
extensible_object(Args &&... args):T(std::forward<Args>(args)...) {}
|
||||
|
||||
typedef std::unique_ptr<extension> (*mk_extension)();
|
||||
|
||||
class extension_factory {
|
||||
std::vector<mk_extension> m_makers;
|
||||
mutex m_makers_mutex;
|
||||
public:
|
||||
unsigned register_extension(mk_extension mk) {
|
||||
lock_guard<mutex> lock(m_makers_mutex);
|
||||
unsigned r = m_makers.size();
|
||||
m_makers.push_back(mk);
|
||||
return r;
|
||||
}
|
||||
|
||||
std::unique_ptr<extension> mk(unsigned extid) {
|
||||
lock_guard<mutex> 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<extension> ext = get_extension_factory().mk(extid);
|
||||
ext->m_owner = this;
|
||||
m_extensions[extid].swap(ext);
|
||||
}
|
||||
return *(m_extensions[extid].get());
|
||||
}
|
||||
|
||||
template<typename Ext> Ext & get_extension(unsigned extid) {
|
||||
extension & ext = get_extension_core(extid);
|
||||
lean_assert(dynamic_cast<Ext*>(&ext) != nullptr);
|
||||
return static_cast<Ext&>(ext);
|
||||
}
|
||||
};
|
||||
template<typename T>
|
||||
typename extensible_object<T>::extension_factory *
|
||||
extensible_object<T>::g_extension_factory = nullptr;
|
||||
}
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
/*
|
||||
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<int> l(m_field, 1); // set the value of m_field to 1
|
||||
|
||||
} // restore original value of m_field
|
||||
|
||||
*/
|
||||
template<typename T>
|
||||
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;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
|
@ -1,91 +0,0 @@
|
|||
/*
|
||||
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 <lean/debug.h>
|
||||
#include <lean/int64.h>
|
||||
|
||||
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<size_t>(ptr);
|
||||
#else
|
||||
/* 64-bit version */
|
||||
size_t r = reinterpret_cast<size_t>(ptr);
|
||||
return hash(static_cast<unsigned>(r >> 32), static_cast<unsigned>(r));
|
||||
#endif
|
||||
}
|
||||
|
||||
template<typename H>
|
||||
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;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
/*
|
||||
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();
|
||||
}
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
/*
|
||||
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 <stdint.h>
|
||||
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
|
||||
}
|
||||
|
|
@ -1,106 +0,0 @@
|
|||
/*
|
||||
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 <utility>
|
||||
#include <lean/thread.h>
|
||||
#include <lean/stackinfo.h>
|
||||
#include <lean/exception.h>
|
||||
#include <lean/flet.h>
|
||||
|
||||
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<size_t> {
|
||||
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<size_t> {
|
||||
public:
|
||||
scope_max_heartbeat(size_t max);
|
||||
};
|
||||
|
||||
void check_heartbeat();
|
||||
|
||||
struct scoped_interrupt_flag : flet<atomic_bool *> {
|
||||
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<typename Function>
|
||||
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
|
||||
}
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
/*
|
||||
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 <string>
|
||||
#include <lean/object.h>
|
||||
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();
|
||||
}
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,27 +0,0 @@
|
|||
/*
|
||||
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 <cstdlib>
|
||||
|
||||
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
|
||||
}
|
||||
|
|
@ -1,224 +0,0 @@
|
|||
/*
|
||||
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 <lean/mpz.h>
|
||||
#include <lean/serializer.h>
|
||||
|
||||
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<unsigned long int>(v)); }
|
||||
mpq & operator=(int v) { return operator=(static_cast<long int>(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<typename T> 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<unsigned>(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<int>(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<unsigned int>(k)); else return operator-=(static_cast<unsigned int>(-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<unsigned int>(k)); else return operator+=(static_cast<unsigned int>(-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; }
|
||||
}
|
||||
|
|
@ -1,267 +0,0 @@
|
|||
/*
|
||||
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 <cstddef>
|
||||
#include <gmp.h>
|
||||
#include <string>
|
||||
#include <iostream>
|
||||
#include <limits>
|
||||
#include <lean/int64.h>
|
||||
#include <lean/debug.h>
|
||||
#include <lean/lean.h>
|
||||
|
||||
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<char*>(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<unsigned>(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<int>(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<unsigned>(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<unsigned>::max() ? *this += mpz(u) : *this += static_cast<unsigned>(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<unsigned>::max() ? *this -= mpz(u) : *this -= static_cast<unsigned>(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<unsigned>::max() ? *this *= mpz(u) : *this *= static_cast<unsigned>(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<unsigned>::max() ? *this /= mpz(u) : *this /= static_cast<unsigned>(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); }
|
||||
};
|
||||
}
|
||||
|
|
@ -1,501 +0,0 @@
|
|||
/*
|
||||
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 <string>
|
||||
#include <lean/lean.h>
|
||||
#include <lean/mpz.h>
|
||||
|
||||
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<void*>(fun), 1, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 2, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 3, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(fun), 4, num_fixed);
|
||||
}
|
||||
inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object *, object *), unsigned num_fixed) {
|
||||
return alloc_closure(reinterpret_cast<void*>(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<void*>(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<void*>(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<void*>(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<unsigned>(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();
|
||||
}
|
||||
|
|
@ -1,155 +0,0 @@
|
|||
/*
|
||||
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 <lean/lean.h>
|
||||
#include <lean/debug.h>
|
||||
|
||||
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<typename T>
|
||||
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<T>(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<T>(v));
|
||||
}
|
||||
template<typename... Args>
|
||||
explicit optional(Args&&... args):m_some(true) {
|
||||
new (&m_value) T(std::forward<Args>(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<typename... Args>
|
||||
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<T>(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<T>(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<typename T> optional<T> some(T const & t) { return optional<T>(t); }
|
||||
template<typename T> optional<T> some(T && t) { return optional<T>(std::forward<T>(t)); }
|
||||
|
||||
// The following macro creates a template specialization optional<P>, 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<P> 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> { \
|
||||
P m_value; \
|
||||
public: \
|
||||
optional():m_value(nullptr) {} \
|
||||
optional(optional const & other):m_value(other.m_value) {} \
|
||||
optional(optional && other):m_value(std::forward<P>(other.m_value)) {} \
|
||||
explicit optional(P const & v):m_value(v) {} \
|
||||
explicit optional(P && v):m_value(std::forward<P>(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<P>(other.m_value); return *this; } \
|
||||
optional& operator=(P const & other) { m_value = other; return *this; } \
|
||||
optional& operator=(P && other) { m_value = std::forward<P>(other); return *this; } \
|
||||
friend bool operator==(optional const & o1, optional const & o2) { \
|
||||
return static_cast<bool>(o1) == static_cast<bool>(o2) && (!o1 || o1.m_value == o2.m_value); \
|
||||
} \
|
||||
friend bool operator!=(optional const & o1, optional const & o2) { \
|
||||
return !operator==(o1, o2); \
|
||||
} \
|
||||
};
|
||||
}
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
/*
|
||||
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();
|
||||
}
|
||||
|
|
@ -1,142 +0,0 @@
|
|||
/*
|
||||
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 <vector>
|
||||
#include <iostream>
|
||||
#include <string>
|
||||
#include <sstream>
|
||||
#include <functional>
|
||||
#include <unordered_map>
|
||||
#include <cstring>
|
||||
#include <lean/object.h>
|
||||
#include <lean/optional.h>
|
||||
|
||||
namespace lean {
|
||||
class serializer {
|
||||
std::ostream & m_out;
|
||||
std::unordered_map<object*, unsigned, std::hash<object*>, std::equal_to<object*>> 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<object*> m_objs;
|
||||
optional<std::string> 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<std::string> const & fname):m_in(in), m_fname(fname) {}
|
||||
~deserializer();
|
||||
std::string read_string();
|
||||
unsigned read_unsigned() {
|
||||
unsigned r = static_cast<unsigned>(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<std::string> 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<typename T>
|
||||
serializer & write_optional(serializer & s, optional<T> const & a) {
|
||||
if (a)
|
||||
s << true << *a;
|
||||
else
|
||||
s << false;
|
||||
return s;
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
optional<T> read_optional(deserializer & d) {
|
||||
if (d.read_bool()) {
|
||||
T r;
|
||||
d >> r;
|
||||
return optional<T>(r);
|
||||
} else {
|
||||
return optional<T>();
|
||||
}
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
serializer & operator<<(serializer & s, optional<T> const & a) {
|
||||
return write_optional<T>(s, a);
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
deserializer & operator>>(deserializer & d, optional<T> & a) {
|
||||
a = read_optional<T>(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; }
|
||||
}
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
/*
|
||||
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 <sstream>
|
||||
#include <string>
|
||||
|
||||
namespace lean {
|
||||
/** \brief Wrapper for std::ostringstream */
|
||||
class sstream {
|
||||
std::ostringstream m_strm;
|
||||
public:
|
||||
std::string str() const { return m_strm.str(); }
|
||||
template<typename T> sstream & operator<<(T const & t) { m_strm << t; return *this; }
|
||||
};
|
||||
}
|
||||
|
|
@ -1,25 +0,0 @@
|
|||
/*
|
||||
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 <csignal>
|
||||
#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();
|
||||
}
|
||||
|
|
@ -1,31 +0,0 @@
|
|||
/*
|
||||
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 <cstdlib>
|
||||
|
||||
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
|
||||
}
|
||||
|
|
@ -1,249 +0,0 @@
|
|||
/*
|
||||
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 <iostream>
|
||||
#include <chrono>
|
||||
#include <functional>
|
||||
|
||||
#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 <thread>
|
||||
#include <mutex>
|
||||
#include <atomic>
|
||||
#include <condition_variable>
|
||||
#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<imp> m_imp;
|
||||
public:
|
||||
lthread(std::function<void(void)> 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 <utility>
|
||||
#include <cstdlib>
|
||||
#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<typename T>
|
||||
class atomic {
|
||||
T m_value;
|
||||
public:
|
||||
atomic(T const & v = T()):m_value(v) {}
|
||||
atomic(T && v):m_value(std::forward<T>(v)) {}
|
||||
atomic(atomic const & v):m_value(v.m_value) {}
|
||||
atomic(atomic && v):m_value(std::forward<T>(v.m_value)) {}
|
||||
atomic & operator=(T const & v) { m_value = v; return *this; }
|
||||
atomic & operator=(T && v) { m_value = std::forward<T>(v); return *this; }
|
||||
atomic & operator=(atomic const & v) { m_value = v.m_value; return *this; }
|
||||
atomic & operator=(atomic && v) { m_value = std::forward<T>(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<unsigned short> atomic_ushort;
|
||||
typedef atomic<unsigned char> atomic_uchar;
|
||||
typedef atomic<bool> atomic_bool;
|
||||
typedef atomic<unsigned> atomic_uint;
|
||||
class thread {
|
||||
public:
|
||||
thread() {}
|
||||
template<typename Function, typename... Args>
|
||||
thread(Function && fun, Args &&... args) {
|
||||
fun(std::forward<Args>(args)...);
|
||||
}
|
||||
typedef unsigned id;
|
||||
bool joinable() const { return true; }
|
||||
void join() {}
|
||||
};
|
||||
class lthread {
|
||||
public:
|
||||
lthread(std::function<void(void)> 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<typename Lock> void wait(Lock const &) {}
|
||||
template<typename Lock, typename F> void wait(Lock const &, F) {}
|
||||
template<typename Lock> void wait_for(Lock const &, chrono::milliseconds const &) {}
|
||||
void notify_all() {}
|
||||
void notify_one() {}
|
||||
};
|
||||
template<typename T> class lock_guard {
|
||||
public:
|
||||
lock_guard(T const &) {}
|
||||
~lock_guard() {}
|
||||
};
|
||||
template<typename T> 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<T*>(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<T*>(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<void()> 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();
|
||||
}
|
||||
|
|
@ -1,53 +0,0 @@
|
|||
/*
|
||||
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 <string>
|
||||
#include <lean/optional.h>
|
||||
#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<size_t> 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<uchar const *>(begin),
|
||||
reinterpret_cast<uchar const *>(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<unsigned> 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<unsigned> & 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);
|
||||
}
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init
|
||||
// Imports: Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.LeanInit Init.ShareCommon
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Coe
|
||||
// Imports: Init.HasCoe Init.Core
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control
|
||||
// Imports: Init.Control.Applicative Init.Control.Functor Init.Control.Alternative Init.Control.Monad Init.Control.Lift Init.Control.State Init.Control.Id Init.Control.Except Init.Control.Reader Init.Control.Option Init.Control.Conditional
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Alternative
|
||||
// Imports: Init.Core Init.Control.Applicative
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Applicative
|
||||
// Imports: Init.Control.Functor
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Conditional
|
||||
// Imports: Init.Control.Monad Init.Data.Option.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.EState
|
||||
// Imports: Init.Control.State Init.Control.Except
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Except
|
||||
// Imports: Init.Control.Alternative Init.Control.Lift Init.Data.ToString
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Functor
|
||||
// Imports: Init.Core
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Id
|
||||
// Imports: Init.Control.Lift
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Lift
|
||||
// Imports: Init.Control.Monad Init.Coe
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Monad
|
||||
// Imports: Init.Control.Applicative Init.Coe
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Option
|
||||
// Imports: Init.Control.Alternative Init.Control.Lift Init.Control.Except
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.Reader
|
||||
// Imports: Init.Control.Lift Init.Control.Id Init.Control.Alternative Init.Control.Except
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Control.State
|
||||
// Imports: Init.Control.Alternative Init.Control.Lift Init.Control.Id Init.Control.Except
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Core
|
||||
// Imports:
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data
|
||||
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.RBTree Init.Data.RBMap Init.Data.Option Init.Data.HashMap Init.Data.Random Init.Data.Queue Init.Data.Stack
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Array
|
||||
// Imports: Init.Data.Array.Basic Init.Data.Array.QSort Init.Data.Array.BinSearch
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Array.Basic
|
||||
// Imports: Init.Data.Nat.Basic Init.Data.Fin.Basic Init.Data.UInt Init.Data.Repr Init.Data.ToString Init.Control.Id Init.Util
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Array.BinSearch
|
||||
// Imports: Init.Data.Array.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Array.QSort
|
||||
// Imports: Init.Data.Array.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.AssocList
|
||||
// Imports: Init.Control.Id
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Basic
|
||||
// Imports: Init.Data.Nat.Basic Init.Data.Fin.Basic Init.Data.List.Basic Init.Data.Char.Basic Init.Data.String.Basic Init.Data.Option.Basic Init.Data.UInt Init.Data.Repr Init.Data.ToString Init.Data.String.Extra
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.ByteArray
|
||||
// Imports: Init.Data.ByteArray.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.ByteArray.Basic
|
||||
// Imports: Init.Data.Array.Basic Init.Data.UInt Init.Data.Option.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Char
|
||||
// Imports: Init.Data.Char.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Char.Basic
|
||||
// Imports: Init.Data.UInt
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.DList
|
||||
// Imports: Init.Data.List.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Fin
|
||||
// Imports: Init.Data.Fin.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Fin.Basic
|
||||
// Imports: Init.Data.Nat.Div Init.Data.Nat.Bitwise
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Float
|
||||
// Imports: Init.Core Init.Data.ToString
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.FloatArray
|
||||
// Imports: Init.Data.FloatArray.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.FloatArray.Basic
|
||||
// Imports: Init.Data.Array.Basic Init.Data.Float Init.Data.Option.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.HashMap
|
||||
// Imports: Init.Data.HashMap.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.HashMap.Basic
|
||||
// Imports: Init.Data.Array.Basic Init.Data.AssocList Init.Data.Option.Basic Init.Data.Hashable
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.HashSet
|
||||
// Imports: Init.Data.Array.Basic Init.Data.List.Control Init.Data.Option.Basic Init.Data.Hashable
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Hashable
|
||||
// Imports: Init.Data.UInt Init.Data.String
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Int
|
||||
// Imports: Init.Data.Int.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Int.Basic
|
||||
// Imports: Init.Data.Nat.Basic Init.Data.List Init.Data.Repr Init.Data.ToString
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.List
|
||||
// Imports: Init.Data.List.Basic Init.Data.List.BasicAux Init.Data.List.Instances Init.Data.List.Control
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.List.Basic
|
||||
// Imports: Init.Core Init.Data.Nat.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.List.BasicAux
|
||||
// Imports: Init.Data.List.Basic Init.Util
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.List.Control
|
||||
// Imports: Init.Control.Monad Init.Control.Alternative Init.Data.List.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.List.Instances
|
||||
// Imports: Init.Data.List.Basic Init.Control.Alternative Init.Control.Monad
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Nat
|
||||
// Imports: Init.Data.Nat.Basic Init.Data.Nat.Div Init.Data.Nat.Bitwise Init.Data.Nat.Control
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Nat.Basic
|
||||
// Imports: Init.Core
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Nat.Bitwise
|
||||
// Imports: Init.Data.Nat.Basic Init.Data.Nat.Div Init.Coe
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Nat.Control
|
||||
// Imports: Init.Control.Monad Init.Control.Alternative Init.Data.Nat.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Nat.Div
|
||||
// Imports: Init.WF Init.Data.Nat.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Option
|
||||
// Imports: Init.Data.Option.Basic Init.Data.Option.BasicAux Init.Data.Option.Instances
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Option.Basic
|
||||
// Imports: Init.Core Init.Control.Monad Init.Control.Alternative Init.Coe
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Option.BasicAux
|
||||
// Imports: Init.Data.Option.Basic Init.Util
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Option.Instances
|
||||
// Imports: Init.Data.Option.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.PersistentArray
|
||||
// Imports: Init.Data.PersistentArray.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.PersistentArray.Basic
|
||||
// Imports: Init.Control.Conditional Init.Data.Array
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.PersistentHashMap
|
||||
// Imports: Init.Data.PersistentHashMap.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.PersistentHashMap.Basic
|
||||
// Imports: Init.Data.Array Init.Data.Hashable
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.PersistentHashSet
|
||||
// Imports: Init.Data.PersistentHashMap
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Queue
|
||||
// Imports: Init.Data.Queue.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Queue.Basic
|
||||
// Imports: Init.Data.Array Init.Data.Int
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.RBMap
|
||||
// Imports: Init.Data.RBMap.Basic Init.Data.RBMap.BasicAux
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.RBMap.Basic
|
||||
// Imports: Init.Data.Repr Init.Data.Option.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.RBMap.BasicAux
|
||||
// Imports: Init.Data.RBMap.Basic Init.Util
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.RBTree
|
||||
// Imports: Init.Data.RBTree.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.RBTree.Basic
|
||||
// Imports: Init.Data.RBMap.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Random
|
||||
// Imports: Init.System.IO Init.Data.Int
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Repr
|
||||
// Imports: Init.Data.String.Basic Init.Data.UInt Init.Data.Nat.Div
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Stack
|
||||
// Imports: Init.Data.Stack.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.Stack.Basic
|
||||
// Imports: Init.Data.Array Init.Data.Int
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.String
|
||||
// Imports: Init.Data.String.Basic Init.Data.String.Extra
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.String.Basic
|
||||
// Imports: Init.Data.List.Basic Init.Data.Char.Basic Init.Data.Option.Basic
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.String.Extra
|
||||
// Imports: Init.Util
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
// Lean compiler output
|
||||
// Module: Init.Data.ToString
|
||||
// Imports: Init.Data.String.Basic Init.Data.UInt Init.Data.Nat.Div Init.Data.Repr
|
||||
#include <lean/runtime/lean.h>
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
|
|
|
|||
Some files were not shown because too many files have changed in this diff Show more
Loading…
Add table
Reference in a new issue