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