feat(frontends/lean): parse numerals as expressions of type 'num.num'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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

library/standard/standard.lean

@@ -1 +1,2 @@
-import logic tactic
+import logic tactic num
+

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() {

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<bool>          m_has_num;
 
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);

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})

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<mpz> to_num(expr const & e) {
+    try {
+        return optional<mpz>(to_num_core(e));
+    } catch (...) {
+        return optional<mpz>();
+    }
+}
+}

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<mpz> to_num(expr const & e);
+}

tests/lean/run/num.lean

@@ -0,0 +1,6 @@
+import num
+check 14
+check 0
+check 3
+check 2
+check 4