refactor(library/arith): replace Nat, Int, Real with simple variable decls instead of semantic attachments

This commit also fixes bugs in the Alias command.

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

src/frontends/lean/frontend.cpp

@@ -54,22 +54,6 @@ static void read_mark_implicit(environment const & env, io_state const &, deseri
 }
 static object_cell::register_deserializer_fn mark_implicit_ds("MarkImplicit", read_mark_implicit);
 
-class alias_command : public neutral_object_cell {
-    name m_name;
-    expr m_expr;
-public:
-    alias_command(name const & n, expr const & e):m_name(n), m_expr(e) {}
-    virtual ~alias_command() {}
-    virtual char const * keyword() const { return "Alias"; }
-    virtual void write(serializer & s) const { s << "Alias" << m_name << m_expr; }
-};
-static void read_alias(environment const & env, io_state const &, deserializer & d) {
-    name n = read_name(d);
-    expr e = read_expr(d);
-    add_alias(env, n, e);
-}
-static object_cell::register_deserializer_fn add_alias_ds("Alias", read_alias);
-
 static std::vector<bool> g_empty_vector;
 /**
    \brief Environment extension object for the Lean default frontend.
@@ -549,7 +533,7 @@ struct lean_extension : public environment_extension {
             m_inv_aliases[e] = list<name>(n, *l);
         else
             m_inv_aliases[e] = list<name>(n);
-        env->add_neutral_object(new alias_command(n, e));
+        env->add_neutral_object(new alias_declaration(n, e));
     }
 };
 

src/frontends/lean/notation.cpp

@@ -10,11 +10,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/frontend.h"
 
 namespace lean {
-void add_alias(environment const & env, name const & n, name const & m) {
-    object const & obj = env->get_object(n);
-    env->add_definition(m, obj.get_type(), mk_constant(n));
-}
-
 /**
    \brief Initialize builtin notation.
 */
@@ -28,6 +23,7 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
             if (kernel_only)
                 return;
 
+            add_alias(env, "ℕ", Nat);
             add_infixl(env, ios, "+", 65, mk_nat_add_fn());
             add_infixl(env, ios, "-", 65, mk_nat_sub_fn());
             add_prefix(env, ios, "-", 75, mk_nat_neg_fn());
@@ -40,6 +36,7 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
             add_infix(env, ios, ">", 50, mk_nat_gt_fn());
             add_mixfixc(env, ios, {"|", "|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function
 
+            add_alias(env, "ℤ", Int);
             add_infixl(env, ios, "+", 65, mk_int_add_fn());
             add_infixl(env, ios, "-", 65, mk_int_sub_fn());
             add_prefix(env, ios, "-", 75, mk_int_neg_fn());
@@ -55,6 +52,7 @@ void init_builtin_notation(environment const & env, io_state & ios, bool kernel_
             add_infix(env, ios, "<", 50, mk_int_lt_fn());
             add_infix(env, ios, ">", 50, mk_int_gt_fn());
 
+            add_alias(env, "ℝ", Real);
             add_infixl(env, ios, "+", 65, mk_real_add_fn());
             add_infixl(env, ios, "-", 65, mk_real_sub_fn());
             add_prefix(env, ios, "-", 75, mk_real_neg_fn());

src/frontends/lean/operator_info.cpp

@@ -218,4 +218,13 @@ io_state_stream const & operator<<(io_state_stream const & out, operator_info co
     out.get_stream() << mk_pair(pp(o), out.get_options());
     return out;
 }
+
+char const * alias_declaration::keyword() const { return "Alias"; }
+void alias_declaration::write(serializer & s) const { s << "Alias" << m_name << m_expr; }
+static void read_alias(environment const & env, io_state const &, deserializer & d) {
+    name n = read_name(d);
+    expr e = read_expr(d);
+    add_alias(env, n, e);
+}
+static object_cell::register_deserializer_fn add_alias_ds("Alias", read_alias);
 }

src/frontends/lean/operator_info.h

@@ -128,4 +128,16 @@ public:
     expr const & get_expr() const { return m_expr; }
     virtual void write(serializer & s) const;
 };
+
+class alias_declaration : public neutral_object_cell {
+    name m_name;
+    expr m_expr;
+public:
+    alias_declaration(name const & n, expr const & e):m_name(n), m_expr(e) {}
+    virtual ~alias_declaration() {}
+    virtual char const * keyword() const;
+    name const & get_alias_name() const { return m_name; }
+    expr const & get_expr() const { return m_expr; }
+    virtual void write(serializer & s) const;
+};
 }

src/frontends/lean/parser.cpp

@@ -1199,6 +1199,8 @@ class parser::imp {
             return save(mk_app(left, save(mk_var(m_num_local_decls - it->second - 1), p)), p2);
         } else if (m_expr_macros && m_expr_macros->find(id) != m_expr_macros->end()) {
             return save(mk_app(left, parse_expr_macro(id, p)), p2);
+        } else if (auto alias = get_alias(m_env, id)) {
+            return save(mk_app(left, save(*alias, p)), p2);
         } else {
             operator_info op = find_led(m_env, id);
             if (op) {

src/frontends/lean/pp.cpp

@@ -162,8 +162,12 @@ bool is_coercion_decl(object const & obj) {
     return dynamic_cast<coercion_declaration const *>(obj.cell());
 }
 
+bool is_alias_decl(object const & obj) {
+    return dynamic_cast<alias_declaration const *>(obj.cell());
+}
+
 bool supported_by_pp(object const & obj) {
-    return obj.kind() != object_kind::Neutral || is_notation_decl(obj) || is_coercion_decl(obj);
+    return obj.kind() != object_kind::Neutral || is_notation_decl(obj) || is_coercion_decl(obj) || is_alias_decl(obj);
 }
 
 /** \brief Functional object for pretty printing expressions */
@@ -1363,6 +1367,13 @@ class pp_formatter_cell : public formatter_cell {
         return group(format{highlight_command(format(n.keyword())), nest(indent, format({line(), pp(c, opts)}))});
     }
 
+    format pp_alias_decl(object const & obj, options const & opts) {
+        alias_declaration const & alias_decl = *static_cast<alias_declaration const *>(obj.cell());
+        name const & n = alias_decl.get_alias_name();
+        expr const & d = alias_decl.get_expr();
+        format d_fmt   = is_constant(d) ? format(const_name(d)) : pp(d, opts);
+        return format{highlight_command(format(alias_decl.keyword())), space(), ::lean::pp(n), space(), colon(), space(), d_fmt};
+    }
 public:
     pp_formatter_cell(ro_environment const & env):
         m_env(env) {
@@ -1405,6 +1416,8 @@ public:
                 return pp_notation_decl(obj, opts);
             } else if (is_coercion_decl(obj)) {
                 return pp_coercion_decl(obj, opts);
+            } else if (is_alias_decl(obj)) {
+                return pp_alias_decl(obj, opts);
             } else {
                 // If the object is not notation or coercion
                 // declaration, then the object was created in

src/library/arith/int.cpp

@@ -7,24 +7,15 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
+#include "kernel/value.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/int.h"
 #include "library/arith/nat.h"
-#include "library/arith/num_type.h"
 
 namespace lean {
-/**
-   \brief Semantic attachment for Int type.
-*/
-class int_type_value : public num_type_value {
-public:
-    int_type_value():num_type_value("Int", "\u2124") /* ℤ */ {}
-    virtual void write(serializer & s) const { s << "Int"; }
-};
-expr const Int = mk_value(*(new int_type_value()));
-expr mk_int_type() { return Int; }
-expr read_int(deserializer & ) { return Int; }
-static register_deserializer_fn if_ds("Int", read_int);
+MK_CONSTANT(Int, "Int");
+expr const Int = mk_Int();
+expr mk_int_type() { return mk_Int(); }
 
 class int_value_value : public value {
     mpz m_val;
@@ -174,7 +165,7 @@ void import_int(environment const & env) {
             expr x    = Const("x");
             expr y    = Const("y");
 
-            env->add_builtin(Int);
+            env->add_var(Int_name, Type());
             env->add_builtin_set(iVal(0));
             env->add_builtin(mk_int_add_fn());
             env->add_builtin(mk_int_mul_fn());

src/library/arith/nat.cpp

@@ -7,23 +7,14 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
+#include "kernel/value.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/nat.h"
-#include "library/arith/num_type.h"
 
 namespace lean {
-/**
-   \brief Semantic attachment for Nat type
-*/
-class nat_type_value : public num_type_value {
-public:
-    nat_type_value():num_type_value("Nat", "\u2115") /* ℕ */ {}
-    virtual void write(serializer & s) const { s << "Nat"; }
-};
-expr const Nat = mk_value(*(new nat_type_value()));
-expr mk_nat_type() { return Nat; }
-expr read_nat(deserializer & ) { return Nat; }
-static register_deserializer_fn if_ds("Nat", read_nat);
+MK_CONSTANT(Nat, "Nat");
+expr const Nat = mk_Nat();
+expr mk_nat_type() { return mk_Nat(); }
 
 class nat_value_value : public value {
     mpz m_val;
@@ -129,8 +120,7 @@ void import_nat(environment const & env) {
             expr nn_b = Nat >> (Nat >> Bool);
             expr x    = Const("x");
             expr y    = Const("y");
-
-            env->add_builtin(Nat);
+            env->add_var(Nat_name, Type());
             env->add_builtin_set(nVal(0));
             env->add_builtin(mk_nat_add_fn());
             env->add_builtin(mk_nat_mul_fn());

src/library/arith/num_type.h

@@ -1,20 +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 "kernel/expr.h"
-#include "kernel/value.h"
-
-namespace lean {
-/** \brief Base class for numeric types */
-class num_type_value : public type_value {
-    name m_unicode;
-public:
-    num_type_value(name const & n, name const & u):type_value(n), m_unicode(u) {}
-    virtual ~num_type_value() {}
-    virtual name get_unicode_name() const { return m_unicode; }
-};
-}

src/library/arith/real.cpp

@@ -7,22 +7,16 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
+#include "kernel/value.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/real.h"
 #include "library/arith/int.h"
 #include "library/arith/nat.h"
-#include "library/arith/num_type.h"
 
 namespace lean {
-class real_type_value : public num_type_value {
-public:
-    real_type_value():num_type_value("Real", "\u211D") /* ℝ */ {}
-    virtual void write(serializer & s) const { s << "Real"; }
-};
-expr const Real = mk_value(*(new real_type_value()));
-expr mk_real_type() { return Real; }
-expr read_real(deserializer & ) { return Real; }
-static register_deserializer_fn if_ds("Real", read_real);
+MK_CONSTANT(Real, "Real");
+expr const Real = mk_Real();
+expr mk_real_type() { return mk_Real(); }
 
 /**
    \brief Semantic attachment for "Real" values.
@@ -159,7 +153,7 @@ void import_real(environment const & env) {
             expr x    = Const("x");
             expr y    = Const("y");
 
-            env->add_builtin(Real);
+            env->add_var(Real_name, Type());
             env->add_builtin_set(rVal(0));
             env->add_builtin(mk_real_add_fn());
             env->add_builtin(mk_real_mul_fn());

tests/lean/alias2.lean

@@ -1,3 +1,4 @@
+Push
   Variable Natural : Type.
   Alias ℕℕ : Natural.
   Variable x : Natural.
@@ -7,8 +8,9 @@ Show Environment 1.
   SetOption pp::unicode true.
   Show Environment 1.
   Alias NN : Natural.
-Show Environment 1.
+  Show Environment 2.
   Alias ℕℕℕ : Natural.
-Show Environment 1.
+  Show Environment 3.
   SetOption pp::unicode false.
-Show Environment 1.
+  Show Environment 3.
+Pop

tests/lean/alias2.lean.expected.out

@@ -8,6 +8,11 @@ Variable x : Natural
   Set: pp::unicode
 Variable x : ℕℕ
 Variable x : NN
+Alias NN : Natural
 Variable x : ℕℕℕ
+Alias NN : Natural
+Alias ℕℕℕ : Natural
   Set: pp::unicode
 Variable x : NN
+Alias NN : Natural
+Alias ℕℕℕ : Natural

tests/lean/loop2.lean.expected.out

@@ -1,4 +1,4 @@
   Set: pp::colors
   Set: pp::unicode
-Variable x : Int
+Variable x : ℤ
 done

tests/lean/lua13.lean

@@ -9,5 +9,5 @@ Variable f : Int -> Int -> Int
  print(b)
  assert(not b:closed())
  local env = get_environment()
- assert(d == env:find_object("Int"):get_value())
+ assert(env:find_object("Int"):get_name() == name("Int"))
 **)

tests/lean/lua14.lean

@@ -9,7 +9,7 @@ Variable f : Int -> Int -> Int
  print(b)
  assert(not b:closed())
  local env = get_environment()
- assert(d == env:find_object("Int"):get_value())
+ assert(env:find_object("Int"):get_name() == name("Int"))
  parse_lean_cmds([[
     Eval 10 + 20
     Check x + y
@@ -19,4 +19,3 @@ Variable f : Int -> Int -> Int
 **)
 
 Check g (f x 10)
-