typeterm.go

     1  // Copyright 2021 The Go Authors. All rights reserved.
     2  // Use of this source code is governed by a BSD-style
     3  // license that can be found in the LICENSE file.
     4  
     5  package types2
     6  
     7  // A term describes elementary type sets:
     8  //
     9  //	 ∅:  (*term)(nil)     == ∅                      // set of no types (empty set)
    10  //	 𝓤:  &term{}          == 𝓤                      // set of all types (𝓤niverse)
    11  //	 T:  &term{false, T}  == {T}                    // set of type T
    12  //	~t:  &term{true, t}   == {t' | under(t') == t}  // set of types with underlying type t
    13  type term struct {
    14  	tilde bool // valid if typ != nil
    15  	typ   Type
    16  }
    17  
    18  func (x *term) String() string {
    19  	switch {
    20  	case x == nil:
    21  		return "∅"
    22  	case x.typ == nil:
    23  		return "𝓤"
    24  	case x.tilde:
    25  		return "~" + x.typ.String()
    26  	default:
    27  		return x.typ.String()
    28  	}
    29  }
    30  
    31  // equal reports whether x and y represent the same type set.
    32  func (x *term) equal(y *term) bool {
    33  	// easy cases
    34  	switch {
    35  	case x == nil || y == nil:
    36  		return x == y
    37  	case x.typ == nil || y.typ == nil:
    38  		return x.typ == y.typ
    39  	}
    40  	// ∅ ⊂ x, y ⊂ 𝓤
    41  
    42  	return x.tilde == y.tilde && Identical(x.typ, y.typ)
    43  }
    44  
    45  // union returns the union x ∪ y: zero, one, or two non-nil terms.
    46  func (x *term) union(y *term) (_, _ *term) {
    47  	// easy cases
    48  	switch {
    49  	case x == nil && y == nil:
    50  		return nil, nil // ∅ ∪ ∅ == ∅
    51  	case x == nil:
    52  		return y, nil // ∅ ∪ y == y
    53  	case y == nil:
    54  		return x, nil // x ∪ ∅ == x
    55  	case x.typ == nil:
    56  		return x, nil // 𝓤 ∪ y == 𝓤
    57  	case y.typ == nil:
    58  		return y, nil // x ∪ 𝓤 == 𝓤
    59  	}
    60  	// ∅ ⊂ x, y ⊂ 𝓤
    61  
    62  	if x.disjoint(y) {
    63  		return x, y // x ∪ y == (x, y) if x ∩ y == ∅
    64  	}
    65  	// x.typ == y.typ
    66  
    67  	// ~t ∪ ~t == ~t
    68  	// ~t ∪  T == ~t
    69  	//  T ∪ ~t == ~t
    70  	//  T ∪  T ==  T
    71  	if x.tilde || !y.tilde {
    72  		return x, nil
    73  	}
    74  	return y, nil
    75  }
    76  
    77  // intersect returns the intersection x ∩ y.
    78  func (x *term) intersect(y *term) *term {
    79  	// easy cases
    80  	switch {
    81  	case x == nil || y == nil:
    82  		return nil // ∅ ∩ y == ∅ and ∩ ∅ == ∅
    83  	case x.typ == nil:
    84  		return y // 𝓤 ∩ y == y
    85  	case y.typ == nil:
    86  		return x // x ∩ 𝓤 == x
    87  	}
    88  	// ∅ ⊂ x, y ⊂ 𝓤
    89  
    90  	if x.disjoint(y) {
    91  		return nil // x ∩ y == ∅ if x ∩ y == ∅
    92  	}
    93  	// x.typ == y.typ
    94  
    95  	// ~t ∩ ~t == ~t
    96  	// ~t ∩  T ==  T
    97  	//  T ∩ ~t ==  T
    98  	//  T ∩  T ==  T
    99  	if !x.tilde || y.tilde {
   100  		return x
   101  	}
   102  	return y
   103  }
   104  
   105  // includes reports whether t ∈ x.
   106  func (x *term) includes(t Type) bool {
   107  	// easy cases
   108  	switch {
   109  	case x == nil:
   110  		return false // t ∈ ∅ == false
   111  	case x.typ == nil:
   112  		return true // t ∈ 𝓤 == true
   113  	}
   114  	// ∅ ⊂ x ⊂ 𝓤
   115  
   116  	u := t
   117  	if x.tilde {
   118  		u = under(u)
   119  	}
   120  	return Identical(x.typ, u)
   121  }
   122  
   123  // subsetOf reports whether x ⊆ y.
   124  func (x *term) subsetOf(y *term) bool {
   125  	// easy cases
   126  	switch {
   127  	case x == nil:
   128  		return true // ∅ ⊆ y == true
   129  	case y == nil:
   130  		return false // x ⊆ ∅ == false since x != ∅
   131  	case y.typ == nil:
   132  		return true // x ⊆ 𝓤 == true
   133  	case x.typ == nil:
   134  		return false // 𝓤 ⊆ y == false since y != 𝓤
   135  	}
   136  	// ∅ ⊂ x, y ⊂ 𝓤
   137  
   138  	if x.disjoint(y) {
   139  		return false // x ⊆ y == false if x ∩ y == ∅
   140  	}
   141  	// x.typ == y.typ
   142  
   143  	// ~t ⊆ ~t == true
   144  	// ~t ⊆ T == false
   145  	//  T ⊆ ~t == true
   146  	//  T ⊆  T == true
   147  	return !x.tilde || y.tilde
   148  }
   149  
   150  // disjoint reports whether x ∩ y == ∅.
   151  // x.typ and y.typ must not be nil.
   152  func (x *term) disjoint(y *term) bool {
   153  	if debug && (x.typ == nil || y.typ == nil) {
   154  		panic("invalid argument(s)")
   155  	}
   156  	ux := x.typ
   157  	if y.tilde {
   158  		ux = under(ux)
   159  	}
   160  	uy := y.typ
   161  	if x.tilde {
   162  		uy = under(uy)
   163  	}
   164  	return !Identical(ux, uy)
   165  }
   166
View as plain text