refactor(kernel): remove normalizer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
a55c3c617d
commit
a39a5b4195
4 changed files with 0 additions and 494 deletions
|
|
@ -1,244 +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 <algorithm>
|
||||
#include <limits>
|
||||
#include "util/list.h"
|
||||
#include "util/flet.h"
|
||||
#include "util/freset.h"
|
||||
#include "util/buffer.h"
|
||||
#include "util/interrupt.h"
|
||||
#include "util/sexpr/options.h"
|
||||
#include "kernel/normalizer.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "kernel/expr_maps.h"
|
||||
#include "kernel/free_vars.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "kernel/replace_fn.h"
|
||||
#include "kernel/kernel_exception.h"
|
||||
|
||||
#ifndef LEAN_KERNEL_NORMALIZER_MAX_DEPTH
|
||||
#define LEAN_KERNEL_NORMALIZER_MAX_DEPTH std::numeric_limits<unsigned>::max()
|
||||
#endif
|
||||
|
||||
namespace lean {
|
||||
static name g_kernel_normalizer_max_depth {"kernel", "normalizer", "max_depth"};
|
||||
RegisterUnsignedOption(g_kernel_normalizer_max_depth, LEAN_KERNEL_NORMALIZER_MAX_DEPTH, "(kernel) maximum recursion depth for expression normalizer");
|
||||
unsigned get_normalizer_max_depth(options const & opts) {
|
||||
return opts.get_unsigned(g_kernel_normalizer_max_depth, LEAN_KERNEL_NORMALIZER_MAX_DEPTH);
|
||||
}
|
||||
|
||||
typedef list<expr> value_stack;
|
||||
value_stack extend(value_stack const & s, expr const & v) {
|
||||
lean_assert(!is_lambda(v) && !is_pi(v) && !is_metavar(v) && !is_let(v));
|
||||
return cons(v, s);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Internal value used to store closures.
|
||||
This is a transient value that is only used during normalization.
|
||||
*/
|
||||
class closure : public macro {
|
||||
expr m_expr;
|
||||
value_stack m_stack;
|
||||
public:
|
||||
closure(expr const & e, value_stack const & s):m_expr(e), m_stack(s) {}
|
||||
virtual ~closure() {}
|
||||
virtual expr get_type(buffer<expr> const & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
|
||||
virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
|
||||
virtual expr expand1(buffer<expr> const & ) const { lean_unreachable(); }
|
||||
virtual expr expand(buffer<expr> const & ) const { lean_unreachable(); }
|
||||
virtual name get_name() const { return name("Closure"); }
|
||||
virtual void display(std::ostream & out) const {
|
||||
out << "(Closure " << m_expr << " [";
|
||||
bool first = true;
|
||||
for (auto v : m_stack) {
|
||||
if (first) first = false; else out << " ";
|
||||
out << v;
|
||||
}
|
||||
out << "])";
|
||||
}
|
||||
expr const & get_expr() const { return m_expr; }
|
||||
value_stack const & get_stack() const { return m_stack; }
|
||||
virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return false; } // NOLINT
|
||||
};
|
||||
|
||||
expr mk_closure(expr const & e, value_stack const & s) { return mk_macro(new closure(e, s)); }
|
||||
bool is_closure(expr const & e) { return is_macro(e) && dynamic_cast<closure const *>(&to_macro(e)) != nullptr; }
|
||||
closure const & to_closure(expr const & e) { lean_assert(is_closure(e)); return static_cast<closure const &>(to_macro(e)); }
|
||||
|
||||
/** \brief Expression normalizer. */
|
||||
class normalizer::imp {
|
||||
typedef expr_map<expr> cache;
|
||||
|
||||
ro_environment::weak_ref m_env;
|
||||
cache m_cache;
|
||||
unsigned m_max_depth;
|
||||
unsigned m_depth;
|
||||
|
||||
ro_environment env() const { return ro_environment(m_env); }
|
||||
|
||||
expr lookup(value_stack const & s, unsigned i) {
|
||||
unsigned j = i;
|
||||
value_stack const * it1 = &s;
|
||||
while (*it1) {
|
||||
if (j == 0)
|
||||
return head(*it1);
|
||||
--j;
|
||||
it1 = &tail(*it1);
|
||||
}
|
||||
throw kernel_exception(env(), "normalizer failure, unexpected occurrence of free variable");
|
||||
}
|
||||
|
||||
/** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */
|
||||
expr reify(expr const & v, unsigned k) {
|
||||
return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) -> optional<expr> {
|
||||
lean_assert(offset == 0);
|
||||
lean_assert(!is_lambda(e) && !is_pi(e) && !is_let(e));
|
||||
if (is_var(e)) {
|
||||
// de Bruijn level --> de Bruijn index
|
||||
return some_expr(mk_var(k - var_idx(e) - 1));
|
||||
} else if (is_closure(e)) {
|
||||
return some_expr(reify_closure(to_closure(e), k));
|
||||
} else {
|
||||
return none_expr();
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
/** \brief Convert the closure \c c into an expression in a context that contains \c k binders. */
|
||||
expr reify_closure(closure const & c, unsigned k) {
|
||||
expr const & e = c.get_expr();
|
||||
value_stack const & s = c.get_stack();
|
||||
lean_assert(is_binder(e));
|
||||
freset<cache> reset(m_cache);
|
||||
expr new_d = reify(normalize(binder_domain(e), s, k), k);
|
||||
m_cache.clear(); // make sure we do not reuse cached values from the previous call
|
||||
expr new_b = reify(normalize(binder_body(e), extend(s, mk_var(k)), k+1), k+1);
|
||||
return update_binder(e, new_d, new_b);
|
||||
}
|
||||
|
||||
/** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */
|
||||
expr normalize(expr const & a, value_stack const & s, unsigned k) {
|
||||
flet<unsigned> l(m_depth, m_depth+1);
|
||||
check_system("normalizer");
|
||||
if (m_depth > m_max_depth)
|
||||
throw kernel_exception(env(), "normalizer maximum recursion depth exceeded");
|
||||
bool shared = false;
|
||||
if (is_shared(a)) {
|
||||
shared = true;
|
||||
auto it = m_cache.find(a);
|
||||
if (it != m_cache.end())
|
||||
return it->second;
|
||||
}
|
||||
|
||||
expr r;
|
||||
switch (a.kind()) {
|
||||
case expr_kind::Pi: case expr_kind::Lambda:
|
||||
r = mk_closure(a, s);
|
||||
break;
|
||||
case expr_kind::Var:
|
||||
r = lookup(s, var_idx(a));
|
||||
break;
|
||||
case expr_kind::Constant: {
|
||||
optional<object> obj = env()->find_object(const_name(a));
|
||||
if (should_unfold(obj)) {
|
||||
// TODO(Leo): instantiate level parameters
|
||||
freset<cache> reset(m_cache);
|
||||
r = normalize(obj->get_value(), value_stack(), 0);
|
||||
} else {
|
||||
r = a;
|
||||
}
|
||||
break;
|
||||
}
|
||||
case expr_kind::Sort: case expr_kind::Macro: case expr_kind::Local: case expr_kind::Meta:
|
||||
r = a;
|
||||
break;
|
||||
case expr_kind::App: {
|
||||
buffer<expr> new_args;
|
||||
expr const * it = &a;
|
||||
while (is_app(*it)) {
|
||||
new_args.push_back(normalize(app_arg(*it), s, k));
|
||||
it = &app_fn(*it);
|
||||
}
|
||||
expr f = normalize(*it, s, k);
|
||||
unsigned i = 0;
|
||||
unsigned n = new_args.size();
|
||||
while (true) {
|
||||
if (is_closure(f) && is_lambda(to_closure(f).get_expr())) {
|
||||
// beta reduction
|
||||
expr fv = to_closure(f).get_expr();
|
||||
value_stack new_s = to_closure(f).get_stack();
|
||||
while (is_lambda(fv) && i < n) {
|
||||
new_s = extend(new_s, new_args[n - i - 1]);
|
||||
i++;
|
||||
fv = binder_body(fv);
|
||||
}
|
||||
{
|
||||
freset<cache> reset(m_cache);
|
||||
f = normalize(fv, new_s, k);
|
||||
}
|
||||
if (i == n) {
|
||||
r = f;
|
||||
break;
|
||||
}
|
||||
} else {
|
||||
if (is_macro(f) && !is_closure(f)) {
|
||||
buffer<expr> reified_args;
|
||||
unsigned i = new_args.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
reified_args.push_back(reify(new_args[i], k));
|
||||
}
|
||||
r = to_macro(f).expand(reified_args);
|
||||
} else {
|
||||
new_args.push_back(f);
|
||||
std::reverse(new_args.begin(), new_args.end());
|
||||
r = mk_app(new_args);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
case expr_kind::Let: {
|
||||
expr v = normalize(let_value(a), s, k);
|
||||
{
|
||||
freset<cache> reset(m_cache);
|
||||
r = normalize(let_body(a), extend(s, v), k);
|
||||
}
|
||||
break;
|
||||
}}
|
||||
if (shared) {
|
||||
m_cache[a] = r;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
public:
|
||||
imp(ro_environment const & env, unsigned max_depth):
|
||||
m_env(env) {
|
||||
m_max_depth = max_depth;
|
||||
m_depth = 0;
|
||||
}
|
||||
|
||||
expr operator()(expr const & e) {
|
||||
unsigned k = 0;
|
||||
return reify(normalize(e, value_stack(), k), k);
|
||||
}
|
||||
|
||||
void clear() { m_cache.clear(); }
|
||||
};
|
||||
|
||||
normalizer::normalizer(ro_environment const & env, unsigned max_depth):m_ptr(new imp(env, max_depth)) {}
|
||||
normalizer::normalizer(ro_environment const & env):normalizer(env, std::numeric_limits<unsigned>::max()) {}
|
||||
normalizer::normalizer(ro_environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {}
|
||||
normalizer::~normalizer() {}
|
||||
expr normalizer::operator()(expr const & e) { return (*m_ptr)(e); }
|
||||
void normalizer::clear() { m_ptr->clear(); }
|
||||
expr normalize(expr const & e, ro_environment const & env) { return normalizer(env)(e); }
|
||||
}
|
||||
|
|
@ -1,30 +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 "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
class ro_environment;
|
||||
class options;
|
||||
/** \brief Functional object for normalizing expressions */
|
||||
class normalizer {
|
||||
class imp;
|
||||
std::unique_ptr<imp> m_ptr;
|
||||
public:
|
||||
normalizer(ro_environment const & env);
|
||||
normalizer(ro_environment const & env, unsigned max_depth);
|
||||
normalizer(ro_environment const & env, options const & opts);
|
||||
~normalizer();
|
||||
|
||||
expr operator()(expr const & e);
|
||||
void clear();
|
||||
};
|
||||
|
||||
/** \brief Normalize \c e using the environment \c env and context \c ctx */
|
||||
expr normalize(expr const & e, ro_environment const & env);
|
||||
}
|
||||
|
|
@ -10,9 +10,6 @@ add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr)
|
|||
add_executable(max_sharing max_sharing.cpp)
|
||||
target_link_libraries(max_sharing ${EXTRA_LIBS})
|
||||
add_test(max_sharing ${CMAKE_CURRENT_BINARY_DIR}/max_sharing)
|
||||
# add_executable(normalizer normalizer.cpp)
|
||||
# target_link_libraries(normalizer ${EXTRA_LIBS})
|
||||
# add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer)
|
||||
# add_executable(threads threads.cpp)
|
||||
# target_link_libraries(threads ${EXTRA_LIBS})
|
||||
# add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads)
|
||||
|
|
|
|||
|
|
@ -1,217 +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 <algorithm>
|
||||
#include "util/thread.h"
|
||||
#include "util/test.h"
|
||||
#include "util/trace.h"
|
||||
#include "util/exception.h"
|
||||
#include "util/interrupt.h"
|
||||
#include "kernel/normalizer.h"
|
||||
#include "kernel/expr_sets.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "kernel/kernel_exception.h"
|
||||
#include "kernel/free_vars.h"
|
||||
using namespace lean;
|
||||
|
||||
expr normalize(expr const & e) {
|
||||
environment env;
|
||||
return normalize(e, env);
|
||||
}
|
||||
|
||||
static void eval(expr const & e, environment & env) { std::cout << e << " --> " << normalize(e, env) << "\n"; }
|
||||
static expr t() { return Const("t"); }
|
||||
static expr lam(expr const & e) { return mk_lambda("_", t(), e); }
|
||||
static expr lam(expr const & t, expr const & e) { return mk_lambda("_", t, e); }
|
||||
static expr v(unsigned i) { return Var(i); }
|
||||
static expr zero() {
|
||||
// fun (t : T) (s : t -> t) (z : t) z
|
||||
return lam(t(), lam(mk_arrow(v(0), v(0)), lam(v(1), v(0))));
|
||||
}
|
||||
static expr one() {
|
||||
// fun (t : T) (s : t -> t) s
|
||||
return lam(t(), lam(mk_arrow(v(0), v(0)), v(0)));
|
||||
}
|
||||
static expr num() { return Const("num"); }
|
||||
static expr plus() {
|
||||
// fun (m n : numeral) (A : Type 0) (f : A -> A) (x : A) => m A f (n A f x).
|
||||
expr x = v(0), f = v(1), A = v(2), n = v(3), m = v(4);
|
||||
expr body = m(A, f, n(A, f, x));
|
||||
return lam(num(), lam(num(), lam(t(), lam(mk_arrow(v(0), v(0)), lam(v(1), body)))));
|
||||
}
|
||||
static expr two() { return mk_app({plus(), one(), one()}); }
|
||||
static expr three() { return mk_app({plus(), two(), one()}); }
|
||||
static expr four() { return mk_app({plus(), two(), two()}); }
|
||||
static expr times() {
|
||||
// fun (m n : numeral) (A : Type 0) (f : A -> A) (x : A) => m A (n A f) x.
|
||||
expr x = v(0), f = v(1), A = v(2), n = v(3), m = v(4);
|
||||
expr body = m(A, n(A, f), x);
|
||||
return lam(num(), lam(num(), lam(t(), lam(mk_arrow(v(0), v(0)), lam(v(1), body)))));
|
||||
}
|
||||
static expr power() {
|
||||
// fun (m n : numeral) (A : Type 0) => m (A -> A) (n A).
|
||||
expr A = v(0), n = v(1), m = v(2);
|
||||
expr body = n(mk_arrow(A, A), m(A));
|
||||
return lam(num(), lam(num(), lam(mk_arrow(v(0), v(0)), body)));
|
||||
}
|
||||
|
||||
unsigned count_core(expr const & a, expr_set & s) {
|
||||
if (s.find(a) != s.end())
|
||||
return 0;
|
||||
s.insert(a);
|
||||
switch (a.kind()) {
|
||||
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort:
|
||||
case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro:
|
||||
return 1;
|
||||
case expr_kind::App:
|
||||
return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1;
|
||||
case expr_kind::Lambda: case expr_kind::Pi:
|
||||
return count_core(binder_domain(a), s) + count_core(binder_body(a), s) + 1;
|
||||
case expr_kind::Let:
|
||||
return count_core(let_value(a), s) + count_core(let_body(a), s) + 1;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
unsigned count(expr const & a) {
|
||||
expr_set s;
|
||||
return count_core(a, s);
|
||||
}
|
||||
|
||||
static void tst_church_numbers() {
|
||||
environment env;
|
||||
env->add_var("t", Type);
|
||||
env->add_var("N", Type);
|
||||
env->add_var("z", Const("N"));
|
||||
env->add_var("s", Const("N"));
|
||||
expr N = Const("N");
|
||||
expr z = Const("z");
|
||||
expr s = Const("s");
|
||||
std::cout << normalize(mk_app(zero(), N, s, z), env) << "\n";
|
||||
std::cout << normalize(mk_app(one(), N, s, z), env) << "\n";
|
||||
std::cout << normalize(mk_app(two(), N, s, z), env) << "\n";
|
||||
std::cout << normalize(mk_app(four(), N, s, z), env) << "\n";
|
||||
std::cout << count(normalize(mk_app(four(), N, s, z), env)) << "\n";
|
||||
lean_assert_eq(count(normalize(mk_app(four(), N, s, z), env)), 15);
|
||||
std::cout << normalize(mk_app(mk_app(times(), four(), four()), N, s, z), env) << "\n";
|
||||
std::cout << normalize(mk_app(mk_app(power(), two(), four()), N, s, z), env) << "\n";
|
||||
lean_assert_eq(count(normalize(mk_app(mk_app(power(), two(), four()), N, s, z), env)), 51);
|
||||
std::cout << normalize(mk_app(mk_app(times(), two(), mk_app(power(), two(), four())), N, s, z), env) << "\n";
|
||||
std::cout << normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env) << "\n";
|
||||
std::cout << count(normalize(mk_app(mk_app(times(), two(), mk_app(power(), two(), four())), N, s, z), env)) << "\n";
|
||||
std::cout << count(normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env)) << "\n";
|
||||
lean_assert_eq(count(normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env)), 195);
|
||||
expr big = normalize(mk_app(mk_app(power(), two(), mk_app(power(), two(), three())), N, s, z), env);
|
||||
std::cout << count(big) << "\n";
|
||||
lean_assert_eq(count(big), 771);
|
||||
expr three = mk_app(plus(), two(), one());
|
||||
lean_assert_eq(count(normalize(mk_app(mk_app(power(), three, three), N, s, z), env)), 84);
|
||||
// expr big2 = normalize(mk_app(mk_app(power(), two(), mk_app(times(), mk_app(plus(), four(), one()), four())), N, s, z), env);
|
||||
// std::cout << count(big2) << "\n";
|
||||
std::cout << normalize(lam(lam(mk_app(mk_app(times(), four(), four()), N, Var(0), z))), env) << "\n";
|
||||
}
|
||||
|
||||
static void tst1() {
|
||||
environment env;
|
||||
env->add_var("t", Type);
|
||||
expr t = Type;
|
||||
env->add_var("f", mk_arrow(t, t));
|
||||
expr f = Const("f");
|
||||
env->add_var("a", t);
|
||||
expr a = Const("a");
|
||||
env->add_var("b", t);
|
||||
expr b = Const("b");
|
||||
expr x = Var(0);
|
||||
expr y = Var(1);
|
||||
eval(mk_app(mk_lambda("x", t, x), a), env);
|
||||
eval(mk_app(mk_lambda("x", t, x), a, b), env);
|
||||
eval(mk_lambda("x", t, f(x)), env);
|
||||
eval(mk_lambda("y", t, mk_lambda("x", t, f(y, x))), env);
|
||||
eval(mk_app(mk_lambda("x", t,
|
||||
mk_app(mk_lambda("f", t,
|
||||
mk_app(Var(0), b)),
|
||||
mk_lambda("g", t, f(Var(1))))),
|
||||
a), env);
|
||||
expr l01 = lam(v(0)(v(1)));
|
||||
expr l12 = lam(lam(v(1)(v(2))));
|
||||
eval(lam(l12(l01)), env);
|
||||
lean_assert(normalize(lam(l12(l01)), env) == lam(lam(v(1)(v(1)))));
|
||||
}
|
||||
|
||||
static void tst2() {
|
||||
environment env;
|
||||
env->add_var("b", Type);
|
||||
expr t1 = mk_let("a", Type, Const("b"), mk_lambda("c", Type, Var(1)(Var(0))));
|
||||
std::cout << t1 << " --> " << normalize(t1, env) << "\n";
|
||||
lean_assert(normalize(t1, env) == mk_lambda("c", Type, Const("b")(Var(0))));
|
||||
}
|
||||
|
||||
static expr mk_big(unsigned depth) {
|
||||
if (depth == 0)
|
||||
return Const("a");
|
||||
else
|
||||
return Const("f")(mk_big(depth - 1), mk_big(depth - 1));
|
||||
}
|
||||
|
||||
static void tst3() {
|
||||
#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD)
|
||||
expr t = mk_big(18);
|
||||
environment env;
|
||||
env->add_var("f", Bool >> (Bool >> Bool));
|
||||
env->add_var("a", Bool);
|
||||
normalizer proc(env);
|
||||
chrono::milliseconds dura(50);
|
||||
interruptible_thread thread([&]() {
|
||||
try {
|
||||
proc(t);
|
||||
// Remark: if the following code is reached, we
|
||||
// should decrease dura.
|
||||
lean_unreachable();
|
||||
} catch (interrupted & it) {
|
||||
std::cout << "interrupted\n";
|
||||
}
|
||||
});
|
||||
this_thread::sleep_for(dura);
|
||||
thread.request_interrupt();
|
||||
thread.join();
|
||||
#endif
|
||||
}
|
||||
|
||||
static void tst4() {
|
||||
environment env;
|
||||
expr x = Const("x");
|
||||
expr t = Fun({x, Type}, mk_app(x, x));
|
||||
expr omega = mk_app(t, t);
|
||||
normalizer proc(env, 512);
|
||||
try {
|
||||
proc(omega);
|
||||
} catch (kernel_exception & ex) {
|
||||
std::cout << ex.what() << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
static void tst5() {
|
||||
environment env;
|
||||
expr f = Const("f");
|
||||
env->add_var("f", Type >> (Type >> Type));
|
||||
expr x = Const("x");
|
||||
expr v = Const("v");
|
||||
expr F = Fun({x, Type}, Let(v, Type, Bool, f(x, v)));
|
||||
expr N = normalizer(env)(F);
|
||||
std::cout << F << " ==> " << N << "\n";
|
||||
lean_assert_eq(N, Fun({x, Type}, f(x, Bool)));
|
||||
}
|
||||
|
||||
int main() {
|
||||
save_stack_info();
|
||||
tst_church_numbers();
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
tst4();
|
||||
tst5();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
Loading…
Reference in a new issue