From 411fa5c60c59336b9af25a3d8395a31015d1a78c Mon Sep 17 00:00:00 2001
From: Shuhei Kadowaki <aviatesk@gmail.com>
Date: Sat, 30 Oct 2021 15:22:42 +0900
Subject: [PATCH] more symbolism

---
 base/compiler/abstractinterpretation.jl |  8 ++++----
 base/compiler/typelattice.jl            | 24 ++++++++++++++++++++++--
 2 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index cd2d96a7da78f..61b01831f600c 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -345,9 +345,9 @@ function from_interconditional(@nospecialize(typ), (; fargs, argtypes)::ArgInfo,
             else
                 elsetype = tmeet(elsetype, widenconst(new_elsetype))
             end
-            if (slot > 0 || condval !== false) && !(old ⊑ vtype) # essentially vtype ⋤ old
+            if (slot > 0 || condval !== false) && vtype ⋤ old
                 slot = id
-            elseif (slot > 0 || condval !== true) && !(old ⊑ elsetype) # essentially elsetype ⋤ old
+            elseif (slot > 0 || condval !== true) && elsetype ⋤ old
                 slot = id
             else # reset: no new useful information for this slot
                 vtype = elsetype = Any
@@ -1606,7 +1606,7 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
                 at = widenconditional(abstract_eval_value(interp, e.args[i], vtypes, sv))
                 if !anyrefine
                     anyrefine = has_nontrivial_const_info(at) || # constant information
-                                at ⋤ fieldtype(t, i - 1)         # just a type-level information, but more precise than the declared type
+                                at ⊏ fieldtype(t, i - 1)         # just a type-level information, but more precise than the declared type
                 end
                 ats[i-1] = at
                 if at === Bottom
@@ -1809,7 +1809,7 @@ function widenreturn(@nospecialize(rt), @nospecialize(bestguess), nslots::Int, s
             if !anyrefine
                 # TODO: consider adding && const_prop_profitable(a) here?
                 anyrefine = has_const_info(a) ||
-                            a ⋤ fieldtype(rt.typ, i)
+                            a ⊏ fieldtype(rt.typ, i)
             end
             fields[i] = a
         end
diff --git a/base/compiler/typelattice.jl b/base/compiler/typelattice.jl
index b7ad974bbf537..1f55ceb94a062 100644
--- a/base/compiler/typelattice.jl
+++ b/base/compiler/typelattice.jl
@@ -140,7 +140,12 @@ function maybe_extract_const_bool(c::AnyConditional)
 end
 maybe_extract_const_bool(@nospecialize c) = nothing
 
-function ⊑(@nospecialize(a), @nospecialize(b))
+"""
+    a ⊑ b -> Bool
+
+The non-strict partial order over the type inference lattice.
+"""
+@nospecialize(a) ⊑ @nospecialize(b) = begin
     if isa(b, LimitedAccuracy)
         if !isa(a, LimitedAccuracy)
             return false
@@ -231,7 +236,22 @@ function ⊑(@nospecialize(a), @nospecialize(b))
         return a === b
     end
 end
-⋤(@nospecialize(a), @nospecialize(b)) = !⊑(b, a)
+
+"""
+    a ⊏ b -> Bool
+
+The strict partial order over the type inference lattice.
+This is defined as the irreflexive kernel of `⊑`.
+"""
+@nospecialize(a) ⊏ @nospecialize(b) = a ⊑ b && !⊑(b, a)
+
+"""
+    a ⋤ b -> Bool
+
+This order could be used as a slightly more efficient version of the strict order `⊏`,
+where we can safely assume `a ⊑ b` holds.
+"""
+@nospecialize(a) ⋤ @nospecialize(b) = !⊑(b, a)
 
 # Check if two lattice elements are partial order equivalent. This is basically
 # `a ⊑ b && b ⊑ a` but with extra performance optimizations.