blob: 1d7223f13c42c013e06c8d8f1fb9cf4b423a7fb2 [file] [log] [blame]
// Copyright 2021 The Go Authors. All rights reserved.
// Use of this source code is governed by a BSD-style
// license that can be found in the LICENSE file.
package types2
// A term describes elementary type sets:
//
// βˆ…: (*term)(nil) == βˆ… // set of no types (empty set)
// 𝓀: &term{} == 𝓀 // set of all types (𝓀niverse)
// T: &term{false, T} == {T} // set of type T
// ~t: &term{true, t} == {t' | under(t') == t} // set of types with underlying type t
//
type term struct {
tilde bool // valid if typ != nil
typ Type
}
func (x *term) String() string {
switch {
case x == nil:
return "βˆ…"
case x.typ == nil:
return "𝓀"
case x.tilde:
return "~" + x.typ.String()
default:
return x.typ.String()
}
}
// equal reports whether x and y represent the same type set.
func (x *term) equal(y *term) bool {
// easy cases
switch {
case x == nil || y == nil:
return x == y
case x.typ == nil || y.typ == nil:
return x.typ == y.typ
}
// βˆ… βŠ‚ x, y βŠ‚ 𝓀
return x.tilde == y.tilde && Identical(x.typ, y.typ)
}
// union returns the union x βˆͺ y: zero, one, or two non-nil terms.
func (x *term) union(y *term) (_, _ *term) {
// easy cases
switch {
case x == nil && y == nil:
return nil, nil // βˆ… βˆͺ βˆ… == βˆ…
case x == nil:
return y, nil // βˆ… βˆͺ y == y
case y == nil:
return x, nil // x βˆͺ βˆ… == x
case x.typ == nil:
return x, nil // 𝓀 βˆͺ y == 𝓀
case y.typ == nil:
return y, nil // x βˆͺ 𝓀 == 𝓀
}
// βˆ… βŠ‚ x, y βŠ‚ 𝓀
if x.disjoint(y) {
return x, y // x βˆͺ y == (x, y) if x ∩ y == βˆ…
}
// x.typ == y.typ
// ~t βˆͺ ~t == ~t
// ~t βˆͺ T == ~t
// T βˆͺ ~t == ~t
// T βˆͺ T == T
if x.tilde || !y.tilde {
return x, nil
}
return y, nil
}
// intersect returns the intersection x ∩ y.
func (x *term) intersect(y *term) *term {
// easy cases
switch {
case x == nil || y == nil:
return nil // βˆ… ∩ y == βˆ… and ∩ βˆ… == βˆ…
case x.typ == nil:
return y // 𝓀 ∩ y == y
case y.typ == nil:
return x // x ∩ 𝓀 == x
}
// βˆ… βŠ‚ x, y βŠ‚ 𝓀
if x.disjoint(y) {
return nil // x ∩ y == βˆ… if x ∩ y == βˆ…
}
// x.typ == y.typ
// ~t ∩ ~t == ~t
// ~t ∩ T == T
// T ∩ ~t == T
// T ∩ T == T
if !x.tilde || y.tilde {
return x
}
return y
}
// includes reports whether t ∈ x.
func (x *term) includes(t Type) bool {
// easy cases
switch {
case x == nil:
return false // t ∈ βˆ… == false
case x.typ == nil:
return true // t ∈ 𝓀 == true
}
// βˆ… βŠ‚ x βŠ‚ 𝓀
u := t
if x.tilde {
u = under(u)
}
return Identical(x.typ, u)
}
// subsetOf reports whether x βŠ† y.
func (x *term) subsetOf(y *term) bool {
// easy cases
switch {
case x == nil:
return true // βˆ… βŠ† y == true
case y == nil:
return false // x βŠ† βˆ… == false since x != βˆ…
case y.typ == nil:
return true // x βŠ† 𝓀 == true
case x.typ == nil:
return false // 𝓀 βŠ† y == false since y != 𝓀
}
// βˆ… βŠ‚ x, y βŠ‚ 𝓀
if x.disjoint(y) {
return false // x βŠ† y == false if x ∩ y == βˆ…
}
// x.typ == y.typ
// ~t βŠ† ~t == true
// ~t βŠ† T == false
// T βŠ† ~t == true
// T βŠ† T == true
return !x.tilde || y.tilde
}
// disjoint reports whether x ∩ y == βˆ….
// x.typ and y.typ must not be nil.
func (x *term) disjoint(y *term) bool {
if debug && (x.typ == nil || y.typ == nil) {
panic("invalid argument(s)")
}
ux := x.typ
if y.tilde {
ux = under(ux)
}
uy := y.typ
if x.tilde {
uy = under(uy)
}
return !Identical(ux, uy)
}