fix(frontends/lean/parser): add support for decimals

Decimal numbers are notation for rationals.
If rat.of_num is not available, then an error is generated.

closes #793

src/frontends/lean/parser.cpp

@@ -1438,9 +1438,24 @@ expr parser::parse_numeral_expr(bool user_notation) {
 }
 
 expr parser::parse_decimal_expr() {
-    // TODO(Leo)
-    next();  // to avoid loop
-    return expr();
+    auto p  = pos();
+    mpq val = get_num_val();
+    next();
+    if (!m_has_rat_of_num) {
+        m_has_rat_of_num = static_cast<bool>(m_env.find(get_rat_of_num_name()));
+    }
+    if (!*m_has_rat_of_num) {
+        throw parser_error("invalid decimal number, environment does not contain 'rat.of_num' "
+                           "(solution: use 'import data.rat')", p);
+    }
+    expr of_num = save_pos(mk_constant(get_rat_of_num_name()), p);
+    expr num    = mk_app(of_num, save_pos(copy(from_num(val.get_numerator())), p), p);
+    if (val.get_denominator() == 1) {
+        return num;
+    } else {
+        expr den    = mk_app(of_num, save_pos(copy(from_num(val.get_denominator())), p), p);
+        return mk_app({save_pos(mk_constant(get_rat_divide_name()), p), num, den}, p);
+    }
 }
 
 expr parser::parse_string_expr() {

src/frontends/lean/parser.h

@@ -119,6 +119,7 @@ class parser {
     undef_id_behavior       m_undef_id_behavior;
     optional<bool>          m_has_num;
     optional<bool>          m_has_string;
+    optional<bool>          m_has_rat_of_num;
     optional<bool>          m_has_tactic_decls;
     // We process theorems in parallel
     theorem_queue           m_theorem_queue;

src/library/constants.cpp

@@ -72,6 +72,8 @@ name const * g_prod_mk = nullptr;
 name const * g_prod_pr1 = nullptr;
 name const * g_prod_pr2 = nullptr;
 name const * g_propext = nullptr;
+name const * g_rat_divide = nullptr;
+name const * g_rat_of_num = nullptr;
 name const * g_sigma = nullptr;
 name const * g_sigma_mk = nullptr;
 name const * g_string = nullptr;
@@ -214,6 +216,8 @@ void initialize_constants() {
     g_prod_pr1 = new name{"prod", "pr1"};
     g_prod_pr2 = new name{"prod", "pr2"};
     g_propext = new name{"propext"};
+    g_rat_divide = new name{"rat", "divide"};
+    g_rat_of_num = new name{"rat", "of_num"};
     g_sigma = new name{"sigma"};
     g_sigma_mk = new name{"sigma", "mk"};
     g_string = new name{"string"};
@@ -357,6 +361,8 @@ void finalize_constants() {
     delete g_prod_pr1;
     delete g_prod_pr2;
     delete g_propext;
+    delete g_rat_divide;
+    delete g_rat_of_num;
     delete g_sigma;
     delete g_sigma_mk;
     delete g_string;
@@ -499,6 +505,8 @@ name const & get_prod_mk_name() { return *g_prod_mk; }
 name const & get_prod_pr1_name() { return *g_prod_pr1; }
 name const & get_prod_pr2_name() { return *g_prod_pr2; }
 name const & get_propext_name() { return *g_propext; }
+name const & get_rat_divide_name() { return *g_rat_divide; }
+name const & get_rat_of_num_name() { return *g_rat_of_num; }
 name const & get_sigma_name() { return *g_sigma; }
 name const & get_sigma_mk_name() { return *g_sigma_mk; }
 name const & get_string_name() { return *g_string; }

src/library/constants.h

@@ -74,6 +74,8 @@ name const & get_prod_mk_name();
 name const & get_prod_pr1_name();
 name const & get_prod_pr2_name();
 name const & get_propext_name();
+name const & get_rat_divide_name();
+name const & get_rat_of_num_name();
 name const & get_sigma_name();
 name const & get_sigma_mk_name();
 name const & get_string_name();

src/library/constants.txt

@@ -67,6 +67,8 @@ prod.mk
 prod.pr1
 prod.pr2
 propext
+rat.divide
+rat.of_num
 sigma
 sigma.mk
 string

tests/lean/793a.lean

@@ -0,0 +1,15 @@
+import data.rat
+
+check 4.0
+check 2.3
+check 1.00
+check 10.213
+
+open rat
+
+check -0.3
+check 10.213
+check 2.3
+check 1.0
+
+eval (λ v, 1.0) 2

tests/lean/793a.lean.expected.out

@@ -0,0 +1,9 @@
+rat.of_num 4 : ℚ
+rat.divide (rat.of_num 23) (rat.of_num 10) : ℚ
+rat.of_num 1 : ℚ
+rat.divide (rat.of_num 10213) (rat.of_num 1000) : ℚ
+-(3 / 10) : ℚ
+10213 / 1000 : ℚ
+23 / 10 : ℚ
+1 : ℚ
+quot.mk (prerat.mk (int.of_nat (nat.succ nat.zero)) (int.of_nat (nat.succ nat.zero)) (int.of_nat_succ_pos nat.zero))

tests/lean/793b.lean

@@ -0,0 +1 @@
+check 1.2

tests/lean/793b.lean.expected.out

@@ -0,0 +1 @@
+793b.lean:1:6: error: invalid decimal number, environment does not contain 'rat.of_num' (solution: use 'import data.rat')