From 0198dfc7c595fd21c247c069ab30dc59f5ddeedc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Jul 2014 08:08:35 -0700 Subject: [PATCH] feat(frontends/lean): parse numerals as expressions of type 'num.num' Signed-off-by: Leonardo de Moura --- library/standard/num.lean | 17 +++++++ library/standard/standard.lean | 3 +- src/frontends/lean/parser.cpp | 13 ++++-- src/frontends/lean/parser.h | 1 + src/library/CMakeLists.txt | 2 +- src/library/num.cpp | 81 ++++++++++++++++++++++++++++++++++ src/library/num.h | 39 ++++++++++++++++ tests/lean/run/num.lean | 6 +++ 8 files changed, 157 insertions(+), 5 deletions(-) create mode 100644 library/standard/num.lean create mode 100644 src/library/num.cpp create mode 100644 src/library/num.h create mode 100644 tests/lean/run/num.lean diff --git a/library/standard/num.lean b/library/standard/num.lean new file mode 100644 index 000000000..6dc1d5cb3 --- /dev/null +++ b/library/standard/num.lean @@ -0,0 +1,17 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura +namespace num +-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. +-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))). +-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc). +inductive pos_num : Type := +| one : pos_num +| bit1 : pos_num → pos_num +| bit0 : pos_num → pos_num + +inductive num : Type := +| zero : num +| pos : pos_num → num + +end \ No newline at end of file diff --git a/library/standard/standard.lean b/library/standard/standard.lean index 9359410ee..af2dd2d21 100644 --- a/library/standard/standard.lean +++ b/library/standard/standard.lean @@ -1 +1,2 @@ -import logic tactic +import logic tactic num + diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 79992cadd..c2f54290a 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -25,6 +25,7 @@ Author: Leonardo de Moura #include "library/deep_copy.h" #include "library/module.h" #include "library/scoped_ext.h" +#include "library/num.h" #include "library/error_handling/error_handling.h" #include "frontends/lean/parser.h" #include "frontends/lean/parser_bindings.h" @@ -846,9 +847,15 @@ expr parser::parse_id() { } expr parser::parse_numeral_expr() { - // TODO(Leo) - next(); // to avoid loop - return expr(); + auto p = pos(); + mpz n = get_num_val().get_numerator(); + next(); + if (!m_has_num) + m_has_num = has_num_decls(m_env); + if (!*m_has_num) + throw parser_error("numeral cannot be encoded as expression, environment does not contain the type 'num' " + "(solution: use 'import num')", p); + return from_num(n); } expr parser::parse_decimal_expr() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 66f5c1406..ba702f014 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -64,6 +64,7 @@ class parser { // When the following flag is true, it creates a constant. // This flag is when we are trying to parse mutually recursive declarations. bool m_no_undef_id_error; + optional m_has_num; void display_error_pos(unsigned line, unsigned pos); void display_error_pos(pos_info p); diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 1371a0d42..79e004bd3 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -4,7 +4,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp normalize.cpp shared_environment.cpp module.cpp coercion.cpp private.cpp placeholder.cpp aliases.cpp level_names.cpp update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp - unifier.cpp explicit.cpp) + unifier.cpp explicit.cpp num.cpp) # hop_match.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/num.cpp b/src/library/num.cpp new file mode 100644 index 000000000..44352aa16 --- /dev/null +++ b/src/library/num.cpp @@ -0,0 +1,81 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/type_checker.h" +#include "library/num.h" + +namespace lean { +static expr g_num(Const({"num", "num"})); +static expr g_pos_num(Const({"num", "pos_num"})); +static expr g_zero(Const({"num", "zero"})); +static expr g_pos(Const({"num", "pos"})); +static expr g_one(Const({"num", "one"})); +static expr g_bit0(Const({"num", "bit0"})); +static expr g_bit1(Const({"num", "bit1"})); + +bool has_num_decls(environment const & env) { + try { + type_checker tc(env); + return + tc.infer(g_zero) == g_num && + tc.infer(g_pos) == mk_arrow(g_pos_num, g_num) && + tc.infer(g_one) == g_pos_num && + tc.infer(g_bit0) == mk_arrow(g_pos_num, g_pos_num) && + tc.infer(g_bit1) == mk_arrow(g_pos_num, g_pos_num); + } catch (...) { + return false; + } +} + +expr from_pos_num(mpz const & n) { + lean_assert(n > 0); + if (n == 1) + return g_one; + if (n % mpz(2) == 1) + return mk_app(g_bit1, from_pos_num(n / 2)); + else + return mk_app(g_bit0, from_pos_num(n / 2)); +} + +expr from_num(mpz const & n) { + expr r; + lean_assert(n >= 0); + if (n == 0) + r = g_zero; + else + r = mk_app(g_pos, from_pos_num(n)); + lean_assert(*to_num(r) == n); + return r; +} + +mpz to_pos_num_core(expr const & e) { + if (e == g_one) + return mpz(1); + else if (app_fn(e) == g_bit0) + return 2 * to_pos_num_core(app_arg(e)); + else if (app_fn(e) == g_bit1) + return 2 * to_pos_num_core(app_arg(e)) + 1; + else + throw exception("expression does not represent a numeral"); +} + +mpz to_num_core(expr const & e) { + if (e == g_zero) + return mpz(0); + else if (app_fn(e) == g_pos) + return to_pos_num_core(app_arg(e)); + else + throw exception("expression does not represent a numeral"); +} + +optional to_num(expr const & e) { + try { + return optional(to_num_core(e)); + } catch (...) { + return optional(); + } +} +} diff --git a/src/library/num.h b/src/library/num.h new file mode 100644 index 000000000..6d0809272 --- /dev/null +++ b/src/library/num.h @@ -0,0 +1,39 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/numerics/mpz.h" +#include "kernel/environment.h" + +namespace lean { +/** + \brief Return true iff the environment \c env contains the following declarations + in the namespace 'num' + one : pos_num + bit0 : pos_num -> pos_num + bit1 : pos_num -> pos_num + zero : num + pos : pos_num -> num +*/ +bool has_num_decls(environment const & env); + +/** + \brief Return an expression that encodes the given numeral in binary using + the declarations one, bit0, bit1, zero, pos. + + \see has_num_decls + + \pre n >= 0 + \post *to_num(from_num(n)) == n +*/ +expr from_num(mpz const & n); + +/** + \brief If the given expression encodes a numeral, then convert it back to mpz numeral. + + \see from_num +*/ +optional to_num(expr const & e); +} diff --git a/tests/lean/run/num.lean b/tests/lean/run/num.lean new file mode 100644 index 000000000..663bca263 --- /dev/null +++ b/tests/lean/run/num.lean @@ -0,0 +1,6 @@ +import num +check 14 +check 0 +check 3 +check 2 +check 4 \ No newline at end of file