-
Notifications
You must be signed in to change notification settings - Fork 7
/
Copy pathterm.go
71 lines (62 loc) · 1.52 KB
/
term.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
package modver
// This file duplicates logic from go/types that is sadly unexported.
import "go/types"
// termSubset reports whether x ⊆ y.
func (c *comparer) termSubset(x, y *types.Term) bool {
// easy cases
switch {
case x == nil:
return true // ∅ ⊆ y == true
case y == nil:
return false // x ⊆ ∅ == false since x != ∅
case y.Type() == nil:
return true // x ⊆ 𝓤 == true
case x.Type() == nil:
return false // 𝓤 ⊆ y == false since y != 𝓤
}
// ∅ ⊂ x, y ⊂ 𝓤
if c.termDisjoint(x, 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()
}
// termDisjoint reports whether x ∩ y == ∅.
// x.typ and y.typ must not be nil.
func (c *comparer) termDisjoint(x, y *types.Term) bool {
ux := x.Type()
if y.Tilde() {
ux = ux.Underlying()
}
uy := y.Type()
if x.Tilde() {
uy = uy.Underlying()
}
return !c.identical(ux, uy)
}
// termListSubset reports whether xl ⊆ yl.
func (c *comparer) termListSubset(xl, yl []*types.Term) bool {
if len(yl) == 0 {
return len(xl) == 0
}
// each term x of xl must be a subset of yl
for _, x := range xl {
if !c.termListSuperset(yl, x) {
return false // x is not a subset yl
}
}
return true
}
// termListSuperset reports whether y ⊆ xl.
func (c *comparer) termListSuperset(xl []*types.Term, y *types.Term) bool {
for _, x := range xl {
if c.termSubset(y, x) {
return true
}
}
return false
}