refactor(library/init): cmp_result => ordering

library/init/default.lean

@@ -9,6 +9,6 @@ import init.relation init.nat init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
 import init.monad init.fin init.list init.char init.string init.to_string init.timeit
-import init.unsigned
+import init.unsigned init.ordering
 import init.meta
 import init.wf init.wf_k

library/init/meta/cmp_result.lean

@@ -1,73 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.to_string init.prod
-
-inductive cmp_result :=
-| lt | eq | gt
-
-open cmp_result
-
-definition cmp_result.has_to_string [instance] : has_to_string cmp_result :=
-has_to_string.mk (λ s, match s with | lt := "lt" | eq := "eq" | gt := "gt" end)
-
-structure has_cmp [class] (A : Type) :=
-(cmp : A → A → cmp_result)
-
-definition nat.cmp (a b : nat) : cmp_result :=
-if a < b      then lt
-else if a = b then eq
-else               gt
-
-definition nat_has_cmp [instance] : has_cmp nat :=
-has_cmp.mk nat.cmp
-
-section
-open prod
-
-variables {A B : Type} [has_cmp A] [has_cmp B]
-
-definition prod.cmp : A × B → A × B → cmp_result
-| (a₁, b₁) (a₂, b₂) :=
-   match has_cmp.cmp a₁ a₂ with
-   | lt := lt
-   | eq := has_cmp.cmp b₁ b₂
-   | gt := gt
-   end
-
-definition prod_has_cmp [instance] {A B : Type} [has_cmp A] [has_cmp B] : has_cmp (A × B) :=
-has_cmp.mk prod.cmp
-end
-
-section
-open sum
-
-variables {A B : Type} [has_cmp A] [has_cmp B]
-
-definition sum.cmp : sum A B → sum A B → cmp_result
-| (inl a₁) (inl a₂) := has_cmp.cmp a₁ a₂
-| (inr b₁) (inr b₂) := has_cmp.cmp b₁ b₂
-| (inl a₁) (inr b₂) := lt
-| (inr b₁) (inl a₂) := gt
-
-definition sum_has_cmp [instance] {A B : Type} [has_cmp A] [has_cmp B] : has_cmp (sum A B) :=
-has_cmp.mk sum.cmp
-end
-
-section
-open option
-
-variables {A : Type} [has_cmp A]
-
-definition option.cmp : option A → option A → cmp_result
-| (some a₁) (some a₂) := has_cmp.cmp a₁ a₂
-| (some a₁) none      := gt
-| none      (some a₂) := lt
-| none      none      := eq
-
-definition option_has_cmp [instance] {A : Type} [has_cmp A] : has_cmp (option A) :=
-has_cmp.mk option.cmp
-end

library/init/meta/expr.lean

@@ -39,10 +39,10 @@ has_to_string.mk expr.to_string
 
 meta_constant expr.lt : expr → expr → bool
 meta_constant expr.lex_lt : expr → expr → bool
-meta_definition expr.cmp (a b : expr) : cmp_result :=
-if expr.lt a b = bool.tt then cmp_result.lt
-else if a = b then cmp_result.eq
-else cmp_result.gt
+meta_definition expr.cmp (a b : expr) : ordering :=
+if expr.lt a b = bool.tt then ordering.lt
+else if a = b then ordering.eq
+else ordering.gt
 
 meta_constant expr.fold {A :Type} : expr → A → (expr → unsigned → A → A) → A
 

library/init/meta/level.lean

@@ -34,10 +34,10 @@ meta_constant level.instantiate : level → list (name × level) → list level
 meta_constant level.to_format : level → options → format
 meta_constant level.to_string : level → string
 
-meta_definition level.cmp (a b : level) : cmp_result :=
-if level.lt a b = bool.tt then cmp_result.lt
-else if a = b then cmp_result.eq
-else cmp_result.gt
+meta_definition level.cmp (a b : level) : ordering :=
+if level.lt a b = bool.tt then ordering.lt
+else if a = b then ordering.eq
+else ordering.gt
 
 meta_definition level.has_to_string [instance] : has_to_string level :=
 has_to_string.mk level.to_string
@@ -45,8 +45,8 @@ has_to_string.mk level.to_string
 meta_definition level.has_to_format [instance] : has_to_format level :=
 has_to_format.mk (λ l, level.to_format l options.mk)
 
-meta_definition level.has_to_cmp [instance] : has_cmp level :=
-has_cmp.mk level.cmp
+meta_definition level.has_to_cmp [instance] : has_ordering level :=
+has_ordering.mk level.cmp
 
 meta_definition level.of_nat : nat → level
 | 0            := level.zero

library/init/meta/name.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.cmp_result
+import init.ordering
 
 /- Reflect a C++ name object. The VM replaces it with the C++ implementation. -/
 inductive name :=
@@ -41,10 +41,10 @@ has_to_string.mk name.to_string
 /- TODO(Leo): provide a definition in Lean. -/
 meta_constant name.has_decidable_eq : decidable_eq name
 /- Both cmp and lex_cmp are total orders, but lex_cmp implements a lexicographical order. -/
-meta_constant name.cmp : name → name → cmp_result
-meta_constant name.lex_cmp : name → name → cmp_result
+meta_constant name.cmp : name → name → ordering
+meta_constant name.lex_cmp : name → name → ordering
 
 attribute [instance] name.has_decidable_eq
 
-meta_definition name_has_cmp [instance] : has_cmp name :=
-has_cmp.mk name.cmp
+meta_definition name_has_ordering [instance] : has_ordering name :=
+has_ordering.mk name.cmp

library/init/meta/rb_map.lean

@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.cmp_result init.meta.name init.meta.format
+import init.ordering init.meta.name init.meta.format
 
 meta_constant rb_map.{l₁ l₂} : Type.{l₁} → Type.{l₂} → Type.{max l₁ l₂ 1}
 
 namespace rb_map
-meta_constant mk_core {key : Type} (data : Type)        : (key → key → cmp_result) → rb_map key data
+meta_constant mk_core {key : Type} (data : Type)        : (key → key → ordering) → rb_map key data
 meta_constant size {key : Type} {data : Type}           : rb_map key data → nat
 meta_constant insert {key : Type} {data : Type}         : rb_map key data → key → data → rb_map key data
 meta_constant erase  {key : Type} {data : Type}         : rb_map key data → key → rb_map key data
@@ -19,11 +19,11 @@ meta_constant min {key : Type} {data : Type}            : rb_map key data → op
 meta_constant max {key : Type} {data : Type}            : rb_map key data → option data
 meta_constant fold {key : Type} {data : Type} {A :Type} : rb_map key data → A → (key → data → A → A) → A
 
-inline meta_definition mk (key : Type) [has_cmp key] (data : Type) : rb_map key data :=
-mk_core data has_cmp.cmp
+inline meta_definition mk (key : Type) [has_ordering key] (data : Type) : rb_map key data :=
+mk_core data has_ordering.cmp
 
 open list
-meta_definition of_list {key : Type} {data : Type} [has_cmp key] : list (key × data) → rb_map key data
+meta_definition of_list {key : Type} {data : Type} [has_ordering key] : list (key × data) → rb_map key data
 | []           := mk key data
 | ((k, v)::ls) := insert (of_list ls) k v
 

library/init/ordering.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.to_string init.prod
+
+inductive ordering :=
+| lt | eq | gt
+
+open ordering
+
+definition ordering.has_to_string [instance] : has_to_string ordering :=
+has_to_string.mk (λ s, match s with | lt := "lt" | eq := "eq" | gt := "gt" end)
+
+structure has_ordering [class] (A : Type) :=
+(cmp : A → A → ordering)
+
+definition nat.cmp (a b : nat) : ordering :=
+if a < b      then lt
+else if a = b then eq
+else               gt
+
+definition nat_has_ordering [instance] : has_ordering nat :=
+has_ordering.mk nat.cmp
+
+section
+open prod
+
+variables {A B : Type} [has_ordering A] [has_ordering B]
+
+definition prod.cmp : A × B → A × B → ordering
+| (a₁, b₁) (a₂, b₂) :=
+   match has_ordering.cmp a₁ a₂ with
+   | lt := lt
+   | eq := has_ordering.cmp b₁ b₂
+   | gt := gt
+   end
+
+definition prod_has_ordering [instance] {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (A × B) :=
+has_ordering.mk prod.cmp
+end
+
+section
+open sum
+
+variables {A B : Type} [has_ordering A] [has_ordering B]
+
+definition sum.cmp : sum A B → sum A B → ordering
+| (inl a₁) (inl a₂) := has_ordering.cmp a₁ a₂
+| (inr b₁) (inr b₂) := has_ordering.cmp b₁ b₂
+| (inl a₁) (inr b₂) := lt
+| (inr b₁) (inl a₂) := gt
+
+definition sum_has_ordering [instance] {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (sum A B) :=
+has_ordering.mk sum.cmp
+end
+
+section
+open option
+
+variables {A : Type} [has_ordering A]
+
+definition option.cmp : option A → option A → ordering
+| (some a₁) (some a₂) := has_ordering.cmp a₁ a₂
+| (some a₁) none      := gt
+| none      (some a₂) := lt
+| none      none      := eq
+
+definition option_has_ordering [instance] {A : Type} [has_ordering A] : has_ordering (option A) :=
+has_ordering.mk option.cmp
+end

src/library/vm/vm_name.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_string.h"
-#include "library/vm/cmp_result.h"
+#include "library/vm/vm_ordering.h"
 
 namespace lean {
 struct vm_name : public vm_external {
@@ -77,11 +77,11 @@ vm_obj name_has_decidable_eq(vm_obj const & o1, vm_obj const & o2) {
 }
 
 vm_obj name_cmp(vm_obj const & o1, vm_obj const & o2) {
-    return int_to_cmp_result(quick_cmp(to_name(o1), to_name(o2)));
+    return int_to_ordering(quick_cmp(to_name(o1), to_name(o2)));
 }
 
 vm_obj name_lex_cmp(vm_obj const & o1, vm_obj const & o2) {
-    return int_to_cmp_result(cmp(to_name(o1), to_name(o2)));
+    return int_to_ordering(cmp(to_name(o1), to_name(o2)));
 }
 
 void initialize_vm_name() {

src/library/vm/vm_ordering.h

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 
 namespace lean {
-/* cmp_result inductive datatype is defined as
+/* ordering inductive datatype is defined as
 
       inductive cmp_result :=
       | lt | eq | gt
@@ -18,12 +18,12 @@ namespace lean {
      eq -> 0
      gt -> 1
 */
-inline int cmp_result_to_int(vm_obj const & o) {
+inline int ordering_to_int(vm_obj const & o) {
     return static_cast<int>(cidx(o)) - 1;
 }
 
-/* Convert an integer representing a comparison result into a cmp_result value */
-inline vm_obj int_to_cmp_result(int i) {
+/* Convert an integer into a ordering value */
+inline vm_obj int_to_ordering(int i) {
     if (i < 0) return mk_vm_simple(0);
     else if (i == 0) return mk_vm_simple(1);
     else return mk_vm_simple(2);

src/library/vm/vm_rb_map.cpp

@@ -9,13 +9,13 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "library/vm/vm_nat.h"
 #include "library/vm/vm_option.h"
-#include "library/vm/cmp_result.h"
+#include "library/vm/vm_ordering.h"
 
 namespace lean {
 struct vm_obj_cmp {
     vm_obj m_cmp;
     int operator()(vm_obj const & o1, vm_obj const & o2) const {
-        return cmp_result_to_int(invoke(m_cmp, o1, o2));
+        return ordering_to_int(invoke(m_cmp, o1, o2));
     }
     vm_obj_cmp() {}
     explicit vm_obj_cmp(vm_obj const & cmp):m_cmp(cmp) {}