From 3fefe947574d0133fcbf96eda17330e929b76f59 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 26 Mar 2018 18:38:47 +0200
Subject: [PATCH] refactor(library/init/core,library/init/unit): make `unit` an
 abbreviation of `punit.{0}`

---
 doc/changes.md                            |  3 +++
 library/init/core.lean                    | 13 ++++++-------
 library/init/data/basic.lean              |  2 +-
 library/init/data/punit.lean              | 22 ++++++++++++++++++++++
 library/init/data/unit.lean               | 22 ----------------------
 library/init/meta/has_reflect.lean        |  3 +--
 src/library/constants.cpp                 |  8 ++++----
 src/library/constants.h                   |  2 +-
 src/library/constants.txt                 |  2 +-
 src/library/inductive_compiler/mutual.cpp |  3 ++-
 tests/lean/run/check_constants.lean       |  2 +-
 tests/lean/user_command.lean.expected.out |  2 +-
 12 files changed, 43 insertions(+), 41 deletions(-)
 create mode 100644 library/init/data/punit.lean
 delete mode 100644 library/init/data/unit.lean

diff --git a/doc/changes.md b/doc/changes.md
index 9324165503..c1dfbeac0d 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -243,6 +243,8 @@ master branch (aka work in progress branch)
 
 * The monad laws have been separated into new type classes `is_lawful_{functor,applicative,monad}`.
 
+* `unit` is now an abbreviation of `punit.{0}`
+
 *API name changes*
 
 * `monad.has_monad_lift(_t)` ~> `has_monad_lift(_t)`
@@ -251,6 +253,7 @@ master branch (aka work in progress branch)
 * deleted `monad.monad_transformer`
 * deleted `monad.lift{n}`. Use `f <$> a1 <*> ... <*> an` instead of `monad.lift{n} f a1 ... an`.
 * merged `has_map` into `functor`
+* `unit_eq(_unit)` ~> `punit_eq(_punit)`
 
 v3.3.0 (14 September 2017)
 -------------
diff --git a/library/init/core.lean b/library/init/core.lean
index e7749e287b..d60640fa13 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -113,8 +113,12 @@ abbreviation id_rhs (α : Sort u) (a : α) : α := a
 inductive punit : Sort u
 | star : punit
 
-inductive unit : Type
-| star : unit
+/-- An abbreviation for `punit.{0}`, its most common instantiation.
+    This type should be preferred over `punit` where possible to avoid
+    unnecessary universe parameters. -/
+abbreviation unit : Type := punit
+
+@[pattern] abbreviation unit.star : unit := punit.star
 
 /--
 Gadget for defining thunks, thunk parameters have special treatment.
@@ -491,11 +495,6 @@ protected def psigma.sizeof {α : Type u} {β : α → Type v} [has_sizeof α] [
 instance (α : Type u) (β : α → Type v) [has_sizeof α] [∀ a, has_sizeof (β a)] : has_sizeof (psigma β) :=
 ⟨psigma.sizeof⟩
 
-protected def unit.sizeof : unit → nat
-| u := 1
-
-instance : has_sizeof unit := ⟨unit.sizeof⟩
-
 protected def punit.sizeof : punit → nat
 | u := 1
 
diff --git a/library/init/data/basic.lean b/library/init/data/basic.lean
index fb480735f5..0e4dadf7b0 100644
--- a/library/init/data/basic.lean
+++ b/library/init/data/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.setoid init.data.quot init.data.bool.basic init.data.unit
+import init.data.setoid init.data.quot init.data.bool.basic init.data.punit
 import init.data.nat.basic init.data.prod init.data.sum.basic
 import init.data.sigma.basic init.data.subtype.basic
 import init.data.fin.basic init.data.list.basic init.data.char.basic
diff --git a/library/init/data/punit.lean b/library/init/data/punit.lean
new file mode 100644
index 0000000000..5f2b14435a
--- /dev/null
+++ b/library/init/data/punit.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.logic
+
+lemma punit_eq (a b : punit) : a = b :=
+punit.rec_on a (punit.rec_on b rfl)
+
+lemma punit_eq_punit (a : punit) : a = () :=
+punit_eq a ()
+
+instance : subsingleton punit :=
+subsingleton.intro punit_eq
+
+instance : inhabited punit :=
+⟨()⟩
+
+instance : decidable_eq punit :=
+λ a b, is_true (punit_eq a b)
diff --git a/library/init/data/unit.lean b/library/init/data/unit.lean
deleted file mode 100644
index de2d0132fc..0000000000
--- a/library/init/data/unit.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import init.logic
-
-lemma unit_eq (a b : unit) : a = b :=
-unit.rec_on a (unit.rec_on b rfl)
-
-lemma unit_eq_unit (a : unit) : a = () :=
-unit_eq a ()
-
-instance : subsingleton unit :=
-subsingleton.intro unit_eq
-
-instance : inhabited unit :=
-⟨()⟩
-
-instance : decidable_eq unit :=
-λ a b, is_true (unit_eq a b)
diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean
index 9fd5e0ef0d..e5189aee11 100644
--- a/library/init/meta/has_reflect.lean
+++ b/library/init/meta/has_reflect.lean
@@ -34,6 +34,5 @@ meta instance list.reflect {α : Type} [has_reflect α] [reflected α] : has_ref
 | []     := `([])
 | (h::t) := `(λ t, h :: t).subst (list.reflect t)
 
-meta instance unit.reflect : has_reflect unit
+meta instance punit.reflect : has_reflect punit
 | () := `(_)
-
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index d928dc3234..6033ef7420 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -286,6 +286,7 @@ name const * g_opt_param = nullptr;
 name const * g_or = nullptr;
 name const * g_out_param = nullptr;
 name const * g_punit = nullptr;
+name const * g_punit_cases_on = nullptr;
 name const * g_punit_star = nullptr;
 name const * g_prod_mk = nullptr;
 name const * g_pprod = nullptr;
@@ -343,7 +344,6 @@ name const * g_true_intro = nullptr;
 name const * g_unification_hint = nullptr;
 name const * g_unification_hint_mk = nullptr;
 name const * g_unit = nullptr;
-name const * g_unit_cases_on = nullptr;
 name const * g_unit_star = nullptr;
 name const * g_monad_from_pure_bind = nullptr;
 name const * g_user_attribute = nullptr;
@@ -643,6 +643,7 @@ void initialize_constants() {
     g_or = new name{"or"};
     g_out_param = new name{"out_param"};
     g_punit = new name{"punit"};
+    g_punit_cases_on = new name{"punit", "cases_on"};
     g_punit_star = new name{"punit", "star"};
     g_prod_mk = new name{"prod", "mk"};
     g_pprod = new name{"pprod"};
@@ -700,7 +701,6 @@ void initialize_constants() {
     g_unification_hint = new name{"unification_hint"};
     g_unification_hint_mk = new name{"unification_hint", "mk"};
     g_unit = new name{"unit"};
-    g_unit_cases_on = new name{"unit", "cases_on"};
     g_unit_star = new name{"unit", "star"};
     g_monad_from_pure_bind = new name{"monad_from_pure_bind"};
     g_user_attribute = new name{"user_attribute"};
@@ -1001,6 +1001,7 @@ void finalize_constants() {
     delete g_or;
     delete g_out_param;
     delete g_punit;
+    delete g_punit_cases_on;
     delete g_punit_star;
     delete g_prod_mk;
     delete g_pprod;
@@ -1058,7 +1059,6 @@ void finalize_constants() {
     delete g_unification_hint;
     delete g_unification_hint_mk;
     delete g_unit;
-    delete g_unit_cases_on;
     delete g_unit_star;
     delete g_monad_from_pure_bind;
     delete g_user_attribute;
@@ -1358,6 +1358,7 @@ name const & get_opt_param_name() { return *g_opt_param; }
 name const & get_or_name() { return *g_or; }
 name const & get_out_param_name() { return *g_out_param; }
 name const & get_punit_name() { return *g_punit; }
+name const & get_punit_cases_on_name() { return *g_punit_cases_on; }
 name const & get_punit_star_name() { return *g_punit_star; }
 name const & get_prod_mk_name() { return *g_prod_mk; }
 name const & get_pprod_name() { return *g_pprod; }
@@ -1415,7 +1416,6 @@ name const & get_true_intro_name() { return *g_true_intro; }
 name const & get_unification_hint_name() { return *g_unification_hint; }
 name const & get_unification_hint_mk_name() { return *g_unification_hint_mk; }
 name const & get_unit_name() { return *g_unit; }
-name const & get_unit_cases_on_name() { return *g_unit_cases_on; }
 name const & get_unit_star_name() { return *g_unit_star; }
 name const & get_monad_from_pure_bind_name() { return *g_monad_from_pure_bind; }
 name const & get_user_attribute_name() { return *g_user_attribute; }
diff --git a/src/library/constants.h b/src/library/constants.h
index c21744ab81..62f36ae1ee 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -288,6 +288,7 @@ name const & get_opt_param_name();
 name const & get_or_name();
 name const & get_out_param_name();
 name const & get_punit_name();
+name const & get_punit_cases_on_name();
 name const & get_punit_star_name();
 name const & get_prod_mk_name();
 name const & get_pprod_name();
@@ -345,7 +346,6 @@ name const & get_true_intro_name();
 name const & get_unification_hint_name();
 name const & get_unification_hint_mk_name();
 name const & get_unit_name();
-name const & get_unit_cases_on_name();
 name const & get_unit_star_name();
 name const & get_monad_from_pure_bind_name();
 name const & get_user_attribute_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index ba6657f852..2d981cb3dc 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -281,6 +281,7 @@ opt_param
 or
 out_param
 punit
+punit.cases_on
 punit.star
 prod.mk
 pprod
@@ -338,7 +339,6 @@ true.intro
 unification_hint
 unification_hint.mk
 unit
-unit.cases_on
 unit.star
 monad_from_pure_bind
 user_attribute
diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp
index 202c541651..c8b6e53b41 100644
--- a/src/library/inductive_compiler/mutual.cpp
+++ b/src/library/inductive_compiler/mutual.cpp
@@ -533,12 +533,13 @@ class add_mutual_inductive_decl_fn {
             expr x_u = mk_local_pp("x_u", mk_app(m_basic_decl.get_c_ind_params(0), mk_app(m_putters[ind_idx], mk_sigma(rev_unpacked_sigma_args, u))));
             expr unit_C = Fun(u, Pi(x_u, mk_sort(m_elim_level)));
             level motive_level = get_level(m_tctx, Pi(u, Pi(x_u, mk_sort(m_elim_level))));
+            level unit_level = mk_level_one();
             expr unit_major_premise = idx;
 
             expr x_star = mk_local_pp("x", mk_app(m_basic_decl.get_c_ind_params(0), mk_app(m_putters[ind_idx], mk_sigma(rev_unpacked_sigma_args, mk_constant(get_unit_star_name())))));
             expr unit_minor_premise = Fun(x_star, mk_app(mk_app(C, indices), x_star));
 
-            return mk_app(mk_constant(get_unit_cases_on_name(), {motive_level}), unit_C, unit_major_premise, unit_minor_premise);
+            return mk_app(mk_constant(get_punit_cases_on_name(), {motive_level, unit_level}), unit_C, unit_major_premise, unit_minor_premise);
         }
 
         expr A = binding_domain(ty);
diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean
index 011b447e13..10eec90e04 100644
--- a/tests/lean/run/check_constants.lean
+++ b/tests/lean/run/check_constants.lean
@@ -286,6 +286,7 @@ run_cmd script_check_id `opt_param
 run_cmd script_check_id `or
 run_cmd script_check_id `out_param
 run_cmd script_check_id `punit
+run_cmd script_check_id `punit.cases_on
 run_cmd script_check_id `punit.star
 run_cmd script_check_id `prod.mk
 run_cmd script_check_id `pprod
@@ -343,7 +344,6 @@ run_cmd script_check_id `true.intro
 run_cmd script_check_id `unification_hint
 run_cmd script_check_id `unification_hint.mk
 run_cmd script_check_id `unit
-run_cmd script_check_id `unit.cases_on
 run_cmd script_check_id `unit.star
 run_cmd script_check_id `monad_from_pure_bind
 run_cmd script_check_id `user_attribute
diff --git a/tests/lean/user_command.lean.expected.out b/tests/lean/user_command.lean.expected.out
index 3a794767ce..e8c9ed4b42 100644
--- a/tests/lean/user_command.lean.expected.out
+++ b/tests/lean/user_command.lean.expected.out
@@ -3,7 +3,7 @@ user_command.lean:14:0: error: unknown identifier 'foo'
 user_command.lean:12:50: error: function expected at
   ()
 term has type
-  unit
+  punit
 foo
 user_command.lean:23:8: error: command does not accept modifiers
 bar