internal/core/subsume: initial implementation
Change-Id: I3bc7e2e74d8bc16f282deec511f437d0f6ff53cc
Reviewed-on: https://cue-review.googlesource.com/c/cue/+/6621
Reviewed-by: CUE cueckoo <cueckoo@gmail.com>
Reviewed-by: Marcel van Lohuizen <mpvl@golang.org>
diff --git a/internal/core/adt/composite.go b/internal/core/adt/composite.go
index 3246c5d..d7c51ca 100644
--- a/internal/core/adt/composite.go
+++ b/internal/core/adt/composite.go
@@ -74,6 +74,11 @@
// status indicates the evaluation progress of this vertex.
status VertexStatus
+ // isData indicates that this Vertex is to be interepreted as data: pattern
+ // and additional constraints, as well as optional fields, should be
+ // ignored.
+ isData bool
+
// Value is the value associated with this vertex. For lists and structs
// this is a sentinel value indicating its kind.
Value Value
@@ -148,6 +153,39 @@
v.status = s
}
+// IsData reports whether v should be interpreted in data mode. In other words,
+// it tells whether optional field matching and non-regular fields, like
+// definitions and hidden fields, should be ignored.
+func (v *Vertex) IsData() bool {
+ return v.isData || len(v.Conjuncts) == 0
+}
+
+// ToDataSingle creates a new Vertex that represents just the regular fields
+// of this vertex. Arcs are left untouched.
+// It is used by cue.Eval to convert nodes to data on per-node basis.
+func (v *Vertex) ToDataSingle() *Vertex {
+ w := *v
+ w.isData = true
+ return &w
+}
+
+// ToDataAll returns a new v where v and all its descendents contain only
+// the regular fields.
+func (v *Vertex) ToDataAll() *Vertex {
+ arcs := make([]*Vertex, len(v.Arcs))
+ for i, a := range v.Arcs {
+ arcs[i] = a.ToDataAll()
+ }
+ w := *v
+ w.Arcs = arcs
+ w.isData = true
+ return &w
+}
+
+// func (v *Vertex) IsEvaluating() bool {
+// return v.Value == cycle
+// }
+
func (v *Vertex) IsErr() bool {
// if v.Status() > Evaluating {
if _, ok := v.Value.(*Bottom); ok {
@@ -228,8 +266,23 @@
// constraints, and additional constraints that match f and inserts them in
// arc. Use f is 0 to match all additional constraints only.
MatchAndInsert(c *OpContext, arc *Vertex)
+
+ // OptionalTypes returns a bit field with the type of optional constraints
+ // that are represented by this Acceptor.
+ OptionalTypes() OptionalType
}
+// OptionalType is a bit field of the type of optional constraints in use by an
+// Acceptor.
+type OptionalType int
+
+const (
+ HasField OptionalType = 1 << iota
+ HasPattern
+ HasAdditional
+ IsOpen
+)
+
func (v *Vertex) Kind() Kind {
// This is possible when evaluating comprehensions. It is potentially
// not known at this time what the type is.
@@ -239,6 +292,17 @@
return v.Value.Kind()
}
+func (v *Vertex) OptionalTypes() OptionalType {
+ switch {
+ case v.Closed != nil:
+ return v.Closed.OptionalTypes()
+ case v.IsList():
+ return 0
+ default:
+ return IsOpen
+ }
+}
+
func (v *Vertex) IsClosed(ctx *OpContext) bool {
switch x := v.Value.(type) {
case *ListMarker:
diff --git a/internal/core/debug/compact.go b/internal/core/debug/compact.go
index 722a480..b40ada5 100644
--- a/internal/core/debug/compact.go
+++ b/internal/core/debug/compact.go
@@ -34,7 +34,7 @@
func (w *compactPrinter) node(n adt.Node) {
switch x := n.(type) {
case *adt.Vertex:
- if x.Value == nil || (w.cfg.Raw && len(x.Conjuncts) > 0) {
+ if x.Value == nil || (w.cfg.Raw && !x.IsData()) {
for i, c := range x.Conjuncts {
if i > 0 {
w.string(" & ")
diff --git a/internal/core/eval/closed.go b/internal/core/eval/closed.go
index 10cee11..c909b43 100644
--- a/internal/core/eval/closed.go
+++ b/internal/core/eval/closed.go
@@ -97,6 +97,13 @@
}
}
+func (a *acceptor) OptionalTypes() (mask adt.OptionalType) {
+ for _, f := range a.fields {
+ mask |= f.OptionalTypes()
+ }
+ return mask
+}
+
// CloseDef defines how individual FieldSets (corresponding to conjuncts)
// combine to determine whether a field is contained in a closed set.
//
diff --git a/internal/core/eval/optionals.go b/internal/core/eval/optionals.go
index 1dbd376..8d77a57 100644
--- a/internal/core/eval/optionals.go
+++ b/internal/core/eval/optionals.go
@@ -37,6 +37,25 @@
isOpen bool // has a ...
}
+func (o *fieldSet) OptionalTypes() (mask adt.OptionalType) {
+ for _, f := range o.fields {
+ if len(f.optional) > 0 {
+ mask = adt.HasField
+ break
+ }
+ }
+ if o.bulk != nil {
+ mask |= adt.HasPattern
+ }
+ if o.additional != nil {
+ mask |= adt.HasAdditional
+ }
+ if o.isOpen {
+ mask |= adt.IsOpen
+ }
+ return mask
+}
+
type field struct {
label adt.Feature
optional []adt.Node
diff --git a/internal/core/subsume/structural.go b/internal/core/subsume/structural.go
new file mode 100644
index 0000000..16e7a0e
--- /dev/null
+++ b/internal/core/subsume/structural.go
@@ -0,0 +1,281 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+// TODO: structural subsumption has not yet been implemented.
+
+import "cuelang.org/go/internal/core/adt"
+
+func (s *subsumer) subsumes(gt, lt adt.Conjunct) bool {
+ if gt == lt {
+ return true
+ }
+
+ // First try evaluating at the value level.
+ x, _ := gt.Expr().(adt.Value)
+ y, _ := lt.Expr().(adt.Value)
+ if x == nil {
+ // Fall back to structural.
+ return s.structural(gt, lt)
+ }
+ if y == nil {
+ return false
+ }
+
+ return s.values(x, y)
+}
+
+func (s *subsumer) conjunct(gt, lt adt.Conjunct) bool {
+ return false
+}
+
+func (s *subsumer) c(env *adt.Environment, x adt.Expr) adt.Conjunct {
+ return adt.MakeConjunct(env, x)
+}
+
+func isBottomConjunct(c adt.Conjunct) bool {
+ b, _ := c.Expr().(*adt.Bottom)
+ return b != nil
+}
+
+func (s *subsumer) node(env *adt.Environment, up int32) *adt.Vertex {
+ for ; up != 0; up-- {
+ env = env.Up
+ }
+ return env.Vertex
+}
+
+func (s *subsumer) structural(a, b adt.Conjunct) bool {
+ if y, ok := b.Expr().(*adt.LetReference); ok {
+ return s.conjunct(a, s.c(b.Env, y.X))
+ }
+ if isBottomConjunct(b) {
+ return true
+ }
+
+ switch x := a.Expr().(type) {
+ case *adt.DisjunctionExpr:
+
+ case *adt.StructLit:
+ case *adt.ListLit:
+
+ case *adt.FieldReference:
+ if y, ok := b.Expr().(*adt.FieldReference); ok && x.Label == y.Label {
+ if s.node(a.Env, x.UpCount) == s.node(b.Env, y.UpCount) {
+ return true
+ }
+ }
+
+ case *adt.LabelReference:
+ if y, ok := b.Expr().(*adt.LabelReference); ok {
+ if s.node(a.Env, x.UpCount) == s.node(b.Env, y.UpCount) {
+ return true
+ }
+ }
+
+ case *adt.DynamicReference:
+ if y, ok := b.Expr().(*adt.FieldReference); ok {
+ if s.node(a.Env, x.UpCount) == s.node(b.Env, y.UpCount) {
+ return true
+ }
+ }
+
+ case *adt.ImportReference:
+ if y, ok := b.Expr().(*adt.ImportReference); ok &&
+ x.ImportPath == y.ImportPath {
+ return true
+ }
+
+ case *adt.LetReference:
+ return s.conjunct(s.c(a.Env, x.X), b)
+
+ case *adt.SelectorExpr:
+ if y, ok := a.Expr().(*adt.SelectorExpr); ok &&
+ x.Sel == y.Sel &&
+ s.conjunct(s.c(a.Env, x.X), s.c(b.Env, y.X)) {
+ return true
+ }
+
+ case *adt.IndexExpr:
+ if y, ok := b.Expr().(*adt.IndexExpr); ok &&
+ s.conjunct(s.c(a.Env, x.X), s.c(b.Env, y.X)) &&
+ s.conjunct(s.c(a.Env, x.Index), s.c(b.Env, y.Index)) {
+ return true
+ }
+
+ case *adt.SliceExpr:
+ if r, ok := b.Expr().(*adt.SliceExpr); ok &&
+ s.conjunct(s.c(a.Env, x.X), s.c(b.Env, r.X)) &&
+ s.conjunct(s.c(a.Env, x.Lo), s.c(b.Env, r.Lo)) &&
+ s.conjunct(s.c(a.Env, x.Hi), s.c(b.Env, r.Hi)) {
+ return true
+ }
+
+ case *adt.Interpolation:
+ switch y := b.Expr().(type) {
+ case *adt.String:
+ // Be conservative if not ground.
+ s.inexact = true
+
+ case *adt.Interpolation:
+ // structural equivalence
+ if len(x.Parts) != len(y.Parts) {
+ return false
+ }
+ for i, p := range x.Parts {
+ if !s.conjunct(s.c(a.Env, p), s.c(b.Env, y.Parts[i])) {
+ return false
+ }
+ }
+ return true
+ }
+
+ case *adt.BoundExpr:
+ if y, ok := b.Expr().(*adt.BoundExpr); ok && x.Op == y.Op {
+ return s.conjunct(s.c(a.Env, x.Expr), s.c(b.Env, y.Expr))
+ }
+
+ case *adt.UnaryExpr:
+ if y, ok := b.Expr().(*adt.UnaryExpr); ok && x.Op == y.Op {
+ return s.conjunct(s.c(a.Env, x.X), s.c(b.Env, y.X))
+ }
+
+ case *adt.BinaryExpr:
+ if y, ok := b.Expr().(*adt.BinaryExpr); ok && x.Op == y.Op {
+ return s.conjunct(s.c(a.Env, x.X), s.c(b.Env, y.X)) &&
+ s.conjunct(s.c(a.Env, x.Y), s.c(b.Env, y.Y))
+ }
+
+ case *adt.CallExpr:
+ if y, ok := b.Expr().(*adt.CallExpr); ok {
+ if len(x.Args) != len(y.Args) {
+ return false
+ }
+ for i, arg := range x.Args {
+ if !s.conjunct(s.c(a.Env, arg), s.c(b.Env, y.Args[i])) {
+ return false
+ }
+ }
+ return s.conjunct(s.c(a.Env, x.Fun), s.c(b.Env, y.Fun))
+ }
+ }
+ return false
+}
+
+func (s *subsumer) structLit(
+ ea *adt.Environment, sa *adt.StructLit,
+ eb *adt.Environment, sb *adt.StructLit) bool {
+
+ // Create index of instance fields.
+ ca := newCollatedDecls()
+ ca.collate(ea, sa)
+
+ if ca.yielders != nil || ca.dynamic != nil {
+ // TODO: we could do structural comparison of comprehensions
+ // in many cases. For instance, an if clause would subsume
+ // structurally if it subsumes any of the if clauses in sb.
+ s.inexact = true
+ return false
+ }
+
+ cb := newCollatedDecls()
+ cb.collate(eb, sb)
+
+ if ca.hasOptional && !s.IgnoreOptional {
+ // TODO: same argument here as for comprehensions. This could
+ // be made to work.
+ if ca.pattern != nil || ca.dynamic != nil {
+ s.inexact = true
+ return false
+ }
+
+ // for f, b := range cb.fields {
+ // if !b.required || f.IsDef() {
+ // continue
+ // }
+ // name := ctx.LabelStr(b.Label)
+ // arg := &stringLit{x.baseValue, name, nil}
+ // u, _ := x.optionals.constraint(ctx, arg)
+ // if u != nil && !s.subsumes(u, b.v) {
+ // return false
+ // }
+ // }
+
+ }
+
+ return false
+
+}
+
+// collatedDecls is used to compute the structural subsumption of two
+// struct literals.
+type collatedDecls struct {
+ fields map[adt.Feature]field
+ yielders []adt.Yielder
+ pattern []*adt.BulkOptionalField
+ dynamic []*adt.DynamicField
+ values []adt.Expr
+ additional []*adt.Ellipsis
+ isOpen bool
+ hasOptional bool
+}
+
+func newCollatedDecls() *collatedDecls {
+ return &collatedDecls{fields: map[adt.Feature]field{}}
+}
+
+type field struct {
+ required bool
+ conjuncts []adt.Conjunct
+}
+
+func (c *collatedDecls) collate(env *adt.Environment, s *adt.StructLit) {
+ for _, d := range s.Decls {
+ switch x := d.(type) {
+ case *adt.Field:
+ e := c.fields[x.Label]
+ e.required = true
+ e.conjuncts = append(e.conjuncts, adt.MakeConjunct(env, x))
+ c.fields[x.Label] = e
+
+ case *adt.OptionalField:
+ e := c.fields[x.Label]
+ e.conjuncts = append(e.conjuncts, adt.MakeConjunct(env, x))
+ c.fields[x.Label] = e
+ c.hasOptional = true
+
+ case *adt.BulkOptionalField:
+ c.pattern = append(c.pattern, x)
+ c.hasOptional = true
+
+ case *adt.DynamicField:
+ c.dynamic = append(c.dynamic, x)
+ c.hasOptional = true
+
+ case *adt.Ellipsis:
+ c.isOpen = true
+ c.additional = append(c.additional, x)
+
+ case *adt.ForClause:
+ c.yielders = append(c.yielders, x)
+
+ case *adt.IfClause:
+ c.yielders = append(c.yielders, x)
+
+ case *adt.LetClause:
+ case *adt.ValueClause:
+ }
+ }
+}
diff --git a/internal/core/subsume/structural_test.go b/internal/core/subsume/structural_test.go
new file mode 100644
index 0000000..b22ded7
--- /dev/null
+++ b/internal/core/subsume/structural_test.go
@@ -0,0 +1,495 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+ "regexp"
+ "strconv"
+ "strings"
+ "testing"
+
+ "cuelang.org/go/cue/parser"
+ "cuelang.org/go/internal/core/adt"
+ "cuelang.org/go/internal/core/compile"
+ "cuelang.org/go/internal/core/eval"
+ "cuelang.org/go/internal/core/runtime"
+)
+
+func TestStructural(t *testing.T) {
+ // TODO: all these tests should pass for structural subsumption.
+ t.Skip()
+
+ // Do not inline: the named struct is used as a marker in
+ // testdata/gen.go.
+ type subsumeTest struct {
+ // the result of b ⊑ a, where a and b are defined in "in"
+ subsumes bool
+ in string
+ // mode subsumeMode
+ }
+ testCases := []subsumeTest{
+ // Top subsumes everything
+ 0: {subsumes: true, in: `a: _, b: _ `},
+ 1: {subsumes: true, in: `a: _, b: null `},
+ 2: {subsumes: true, in: `a: _, b: int `},
+ 3: {subsumes: true, in: `a: _, b: 1 `},
+ 4: {subsumes: true, in: `a: _, b: float `},
+ 5: {subsumes: true, in: `a: _, b: "s" `},
+ 6: {subsumes: true, in: `a: _, b: {} `},
+ 7: {subsumes: true, in: `a: _, b: []`},
+ 8: {subsumes: true, in: `a: _, b: _|_ `},
+
+ // Nothing besides top subsumed top
+ 9: {subsumes: false, in: `a: null, b: _`},
+ 10: {subsumes: false, in: `a: int, b: _`},
+ 11: {subsumes: false, in: `a: 1, b: _`},
+ 12: {subsumes: false, in: `a: float, b: _`},
+ 13: {subsumes: false, in: `a: "s", b: _`},
+ 14: {subsumes: false, in: `a: {}, b: _`},
+ 15: {subsumes: false, in: `a: [], b: _`},
+ 16: {subsumes: false, in: `a: _|_ , b: _`},
+
+ // Bottom subsumes nothing except bottom itself.
+ 17: {subsumes: false, in: `a: _|_, b: null `},
+ 18: {subsumes: false, in: `a: _|_, b: int `},
+ 19: {subsumes: false, in: `a: _|_, b: 1 `},
+ 20: {subsumes: false, in: `a: _|_, b: float `},
+ 21: {subsumes: false, in: `a: _|_, b: "s" `},
+ 22: {subsumes: false, in: `a: _|_, b: {} `},
+ 23: {subsumes: false, in: `a: _|_, b: [] `},
+ 24: {subsumes: true, in: ` a: _|_, b: _|_ `},
+
+ // All values subsume bottom
+ 25: {subsumes: true, in: `a: null, b: _|_`},
+ 26: {subsumes: true, in: `a: int, b: _|_`},
+ 27: {subsumes: true, in: `a: 1, b: _|_`},
+ 28: {subsumes: true, in: `a: float, b: _|_`},
+ 29: {subsumes: true, in: `a: "s", b: _|_`},
+ 30: {subsumes: true, in: `a: {}, b: _|_`},
+ 31: {subsumes: true, in: `a: [], b: _|_`},
+ 32: {subsumes: true, in: `a: true, b: _|_`},
+ 33: {subsumes: true, in: `a: _|_, b: _|_`},
+
+ // null subsumes only null
+ 34: {subsumes: true, in: ` a: null, b: null `},
+ 35: {subsumes: false, in: `a: null, b: 1 `},
+ 36: {subsumes: false, in: `a: 1, b: null `},
+
+ 37: {subsumes: true, in: ` a: true, b: true `},
+ 38: {subsumes: false, in: `a: true, b: false `},
+
+ 39: {subsumes: true, in: ` a: "a", b: "a" `},
+ 40: {subsumes: false, in: `a: "a", b: "b" `},
+ 41: {subsumes: true, in: ` a: string, b: "a" `},
+ 42: {subsumes: false, in: `a: "a", b: string `},
+
+ // Number typing (TODO)
+ //
+ // In principle, an "int" cannot assume an untyped "1", as "1" may
+ // still by typed as a float. They are two different type aspects. When
+ // considering, keep in mind that:
+ // Key requirement: if A subsumes B, it must not be possible to
+ // specialize B further such that A does not subsume B. HOWEVER,
+ // The type conversion rules for conversion are INDEPENDENT of the
+ // rules for subsumption!
+ // Consider:
+ // - only having number, but allowing user-defined types.
+ // Subsumption would still work the same, but it may be somewhat
+ // less weird.
+ // - making 1 always an int and 1.0 always a float.
+ // - the int type would subsume any derived type from int.
+ // - arithmetic would allow implicit conversions, but maybe not for
+ // types.
+ //
+ // TODO: irrational numbers: allow untyped, but require explicit
+ // trunking when assigning to float.
+ //
+ // a: number; cue.IsInteger(a) && a > 0
+ // t: (x) -> number; cue.IsInteger(a) && a > 0
+ // type x number: cue.IsInteger(x) && x > 0
+ // x: typeOf(number); cue.IsInteger(x) && x > 0
+ 43: {subsumes: true, in: `a: 1, b: 1 `},
+ 44: {subsumes: true, in: `a: 1.0, b: 1.0 `},
+ 45: {subsumes: true, in: `a: 3.0, b: 3.0 `},
+ 46: {subsumes: false, in: `a: 1.0, b: 1 `},
+ 47: {subsumes: false, in: `a: 1, b: 1.0 `},
+ 48: {subsumes: false, in: `a: 3, b: 3.0`},
+ 49: {subsumes: true, in: `a: int, b: 1`},
+ 50: {subsumes: true, in: `a: int, b: int & 1`},
+ 51: {subsumes: true, in: `a: float, b: 1.0`},
+ 52: {subsumes: false, in: `a: float, b: 1`},
+ 53: {subsumes: false, in: `a: int, b: 1.0`},
+ 54: {subsumes: true, in: `a: int, b: int`},
+ 55: {subsumes: true, in: `a: number, b: int`},
+
+ // Structs
+ 64: {subsumes: true, in: `a: {}, b: {}`},
+ 65: {subsumes: true, in: `a: {}, b: {a: 1}`},
+ 66: {subsumes: true, in: `a: {a:1}, b: {a:1, b:1}`},
+ 67: {subsumes: true, in: `a: {s: { a:1} }, b: { s: { a:1, b:2 }}`},
+ 68: {subsumes: true, in: `a: {}, b: {}`},
+ // TODO: allow subsumption of unevaluated values?
+ // ref not yet evaluated and not structurally equivalent
+ 69: {subsumes: true, in: `a: {}, b: {} & c, c: {}`},
+
+ 70: {subsumes: false, in: `a: {a:1}, b: {}`},
+ 71: {subsumes: false, in: `a: {a:1, b:1}, b: {a:1}`},
+ 72: {subsumes: false, in: `a: {s: { a:1} }, b: { s: {}}`},
+
+ 84: {subsumes: true, in: `a: 1 | 2, b: 2 | 1`},
+ 85: {subsumes: true, in: `a: 1 | 2, b: 1 | 2`},
+
+ 86: {subsumes: true, in: `a: number, b: 2 | 1`},
+ 87: {subsumes: true, in: `a: number, b: 2 | 1`},
+ 88: {subsumes: false, in: `a: int, b: 1 | 2 | 3.1`},
+
+ 89: {subsumes: true, in: `a: float | number, b: 1 | 2 | 3.1`},
+
+ 90: {subsumes: false, in: `a: int, b: 1 | 2 | 3.1`},
+ 91: {subsumes: true, in: `a: 1 | 2, b: 1`},
+ 92: {subsumes: true, in: `a: 1 | 2, b: 2`},
+ 93: {subsumes: false, in: `a: 1 | 2, b: 3`},
+
+ // Structural
+ 94: {subsumes: false, in: `a: int + int, b: int`},
+ 95: {subsumes: true, in: `a: int + int, b: int + int`},
+ 96: {subsumes: true, in: `a: int + number, b: int + int`},
+ 97: {subsumes: true, in: `a: number + number, b: int + int`},
+ // TODO: allow subsumption of unevaluated values?
+ // TODO: may be false if we allow arithmetic on incomplete values.
+ 98: {subsumes: false, in: `a: int + int, b: int * int`},
+
+ // TODO: allow subsumption of unevaluated values?
+ // true because both evaluate to bottom
+ 99: {subsumes: true, in: `a: !int, b: !int`},
+ 100: {subsumes: true, in: `a: !number, b: !int`},
+ 101: {subsumes: true, in: `a: !int, b: !number`},
+
+ // TODO: allow subsumption of unevaluated values?
+ 102: {subsumes: false, in: `a: int + int, b: !number`},
+ // TODO: allow subsumption of unevaluated values?
+ 103: {subsumes: false, in: `a: !bool, b: bool`},
+ 104: {subsumes: true, in: `a: !bool, b: !bool`},
+
+ // Call
+ 113: {subsumes: true, in: `
+ a: fn()
+ b: fn()
+ fn: _`,
+ },
+ 114: {subsumes: false, in: `
+ a: fn(),
+ b: fn(1)
+ fn: _`,
+ },
+ 115: {subsumes: true, in: `
+ a: fn(2)
+ b: fn(2)
+ fn: _`,
+ },
+ 116: {subsumes: true, in: `
+ a: fn(number)
+ b: fn(2)
+ fn: _`,
+ },
+ 117: {subsumes: false, in: `
+ a: fn(2)
+ b: fn(number)
+ fn: _`,
+ },
+
+ // TODO: allow subsumption of unevaluated values?
+ // TODO: okay, but why false?
+ 121: {subsumes: false, in: `a: c + d, b: int, c: int, d: int`},
+ // TODO: allow subsumption of unevaluated values?
+ 122: {subsumes: true, in: `a: {}, b: c & {}, c: {}`},
+
+ // references
+ 123: {subsumes: true, in: `a: c, b: c, c: {}`},
+ // TODO: allow subsumption of unevaluated values?
+ 124: {subsumes: true, in: `a: c, b: d, c: {}, d: {}`},
+ 125: {subsumes: false, in: `a: c, b: d, c: {a:1}, d: {}`},
+ // TODO: allow subsumption of unevaluated values?
+ 126: {subsumes: true, in: `a: c, b: d, c: {a:1}, d: c & {b:1}`},
+ 127: {subsumes: false, in: `a: d, b: c, c: {a:1}, d: c & {b:1}`},
+ 128: {subsumes: false, in: `a: c.c, b: c, c: { d: number}`},
+
+ // type unification catches a reference error.
+ 129: {subsumes: false, in: `a: c, b: d, c: 1, d: 2`},
+
+ 130: {subsumes: true, in: ` a: [1][1], b: [1][1]`},
+ 131: {subsumes: true, in: ` a: [1][number], b: [1][1]`},
+ 132: {subsumes: true, in: ` a: [number][1], b: [1][1]`},
+ 133: {subsumes: true, in: ` a: [number][number], b: [1][1]`},
+ 134: {subsumes: false, in: ` a: [1][0], b: [1][number]`},
+ 135: {subsumes: false, in: ` a: [1][0], b: [number][0]`},
+ 136: {subsumes: true, in: ` a: [number][number], b: [1][number]`},
+ 137: {subsumes: true, in: ` a: [number][number], b: [number][1]`},
+ // purely structural:
+ 138: {subsumes: false, in: ` a: [number][number], b: number`},
+
+ // interpolations
+ 139: {subsumes: true, in: ` a: "\(d)", b: "\(d)", d: _`},
+ // TODO: allow subsumption of unevaluated values?
+ 140: {subsumes: true, in: ` a: "\(d)", b: "\(e)", d: _, e: _`},
+
+ 141: {subsumes: true, in: ` a: "\(string)", b: "\("foo")"`},
+ // TODO: allow subsumption of unevaluated values?
+ 142: {subsumes: true, in: ` a: "\(string)", b: "\(d)", d: "foo"`},
+ 143: {subsumes: true, in: ` a: "\("foo")", b: "\("foo")"`},
+ 144: {subsumes: false, in: ` a: "\("foo")", b: "\(1) \(2)"`},
+
+ 145: {subsumes: false, in: ` a: "s \(d) e", b: "s a e", d: _`},
+ 146: {subsumes: false, in: ` a: "s \(d)m\(d) e", b: "s a e", d: _`},
+
+ // 147: {subsumes: true, in: ` a: 7080, b: *7080 | int`, mode: subChoose},
+
+ // Defaults
+ 150: {subsumes: false, in: `a: number | *1, b: number | *2`},
+ 151: {subsumes: true, in: `a: number | *2, b: number | *2`},
+ 152: {subsumes: true, in: `a: int | *float, b: int | *2.0`},
+ 153: {subsumes: false, in: `a: int | *2, b: int | *2.0`},
+ 154: {subsumes: true, in: `a: number | *2 | *3, b: number | *2`},
+ 155: {subsumes: true, in: `a: number, b: number | *2`},
+
+ // Bounds
+ 170: {subsumes: true, in: `a: >=2, b: >=2`},
+ 171: {subsumes: true, in: `a: >=1, b: >=2`},
+ 172: {subsumes: true, in: `a: >0, b: >=2`},
+ 173: {subsumes: true, in: `a: >1, b: >1`},
+ 174: {subsumes: true, in: `a: >=1, b: >1`},
+ 175: {subsumes: false, in: `a: >1, b: >=1`},
+ 176: {subsumes: true, in: `a: >=1, b: >=1`},
+ 177: {subsumes: true, in: `a: <1, b: <1`},
+ 178: {subsumes: true, in: `a: <=1, b: <1`},
+ 179: {subsumes: false, in: `a: <1, b: <=1`},
+ 180: {subsumes: true, in: `a: <=1, b: <=1`},
+
+ 181: {subsumes: true, in: `a: !=1, b: !=1`},
+ 182: {subsumes: false, in: `a: !=1, b: !=2`},
+
+ 183: {subsumes: false, in: `a: !=1, b: <=1`},
+ 184: {subsumes: true, in: `a: !=1, b: <1`},
+ 185: {subsumes: false, in: `a: !=1, b: >=1`},
+ 186: {subsumes: true, in: `a: !=1, b: <1`},
+
+ 187: {subsumes: true, in: `a: !=1, b: <=0`},
+ 188: {subsumes: true, in: `a: !=1, b: >=2`},
+ 189: {subsumes: true, in: `a: !=1, b: >1`},
+
+ 195: {subsumes: false, in: `a: >=2, b: !=2`},
+ 196: {subsumes: false, in: `a: >2, b: !=2`},
+ 197: {subsumes: false, in: `a: <2, b: !=2`},
+ 198: {subsumes: false, in: `a: <=2, b: !=2`},
+
+ 200: {subsumes: true, in: `a: =~"foo", b: =~"foo"`},
+ 201: {subsumes: false, in: `a: =~"foo", b: =~"bar"`},
+ 202: {subsumes: false, in: `a: =~"foo1", b: =~"foo"`},
+
+ 203: {subsumes: true, in: `a: !~"foo", b: !~"foo"`},
+ 204: {subsumes: false, in: `a: !~"foo", b: !~"bar"`},
+ 205: {subsumes: false, in: `a: !~"foo", b: !~"foo1"`},
+
+ // The following is could be true, but we will not go down the rabbit
+ // hold of trying to prove subsumption of regular expressions.
+ 210: {subsumes: false, in: `a: =~"foo", b: =~"foo1"`},
+ 211: {subsumes: false, in: `a: !~"foo1", b: !~"foo"`},
+
+ 220: {subsumes: true, in: `a: <5, b: 4`},
+ 221: {subsumes: false, in: `a: <5, b: 5`},
+ 222: {subsumes: true, in: `a: <=5, b: 5`},
+ 223: {subsumes: false, in: `a: <=5.0, b: 5.00000001`},
+ 224: {subsumes: true, in: `a: >5, b: 6`},
+ 225: {subsumes: false, in: `a: >5, b: 5`},
+ 226: {subsumes: true, in: `a: >=5, b: 5`},
+ 227: {subsumes: false, in: `a: >=5, b: 4`},
+ 228: {subsumes: true, in: `a: !=5, b: 6`},
+ 229: {subsumes: false, in: `a: !=5, b: 5`},
+ 230: {subsumes: false, in: `a: !=5.0, b: 5.0`},
+ 231: {subsumes: false, in: `a: !=5.0, b: 5`},
+
+ 250: {subsumes: true, in: `a: =~ #"^\d{3}$"#, b: "123"`},
+ 251: {subsumes: false, in: `a: =~ #"^\d{3}$"#, b: "1234"`},
+ 252: {subsumes: true, in: `a: !~ #"^\d{3}$"#, b: "1234"`},
+ 253: {subsumes: false, in: `a: !~ #"^\d{3}$"#, b: "123"`},
+
+ // Conjunctions
+ 300: {subsumes: true, in: `a: >0, b: >=2 & <=100`},
+ 301: {subsumes: false, in: `a: >0, b: >=0 & <=100`},
+
+ 310: {subsumes: true, in: `a: >=0 & <=100, b: 10`},
+ 311: {subsumes: true, in: `a: >=0 & <=100, b: >=0 & <=100`},
+ 312: {subsumes: false, in: `a: !=2 & !=4, b: >3`},
+ 313: {subsumes: true, in: `a: !=2 & !=4, b: >5`},
+
+ 314: {subsumes: false, in: `a: >=0 & <=100, b: >=0 & <=150`},
+ 315: {subsumes: true, in: `a: >=0 & <=150, b: >=0 & <=100`},
+
+ // Disjunctions
+ 330: {subsumes: true, in: `a: >5, b: >10 | 8`},
+ 331: {subsumes: false, in: `a: >8, b: >10 | 8`},
+
+ // Optional fields
+ // Optional fields defined constraints on fields that are not yet
+ // defined. So even if such a field is not part of the output, it
+ // influences the lattice structure.
+ // For a given A and B, where A and B unify and where A has an optional
+ // field that is not defined in B, the addition of an incompatible
+ // value of that field in B can cause A and B to no longer unify.
+ //
+ 400: {subsumes: false, in: `a: {foo: 1}, b: {}`},
+ 401: {subsumes: false, in: `a: {foo?: 1}, b: {}`},
+ 402: {subsumes: true, in: `a: {}, b: {foo: 1}`},
+ 403: {subsumes: true, in: `a: {}, b: {foo?: 1}`},
+
+ 404: {subsumes: true, in: `a: {foo: 1}, b: {foo: 1}`},
+ 405: {subsumes: true, in: `a: {foo?: 1}, b: {foo: 1}`},
+ 406: {subsumes: true, in: `a: {foo?: 1}, b: {foo?: 1}`},
+ 407: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`},
+
+ 408: {subsumes: false, in: `a: {foo: 1}, b: {foo: 2}`},
+ 409: {subsumes: false, in: `a: {foo?: 1}, b: {foo: 2}`},
+ 410: {subsumes: false, in: `a: {foo?: 1}, b: {foo?: 2}`},
+ 411: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 2}`},
+
+ 412: {subsumes: true, in: `a: {foo: number}, b: {foo: 2}`},
+ 413: {subsumes: true, in: `a: {foo?: number}, b: {foo: 2}`},
+ 414: {subsumes: true, in: `a: {foo?: number}, b: {foo?: 2}`},
+ 415: {subsumes: false, in: `a: {foo: number}, b: {foo?: 2}`},
+
+ 416: {subsumes: false, in: `a: {foo: 1}, b: {foo: number}`},
+ 417: {subsumes: false, in: `a: {foo?: 1}, b: {foo: number}`},
+ 418: {subsumes: false, in: `a: {foo?: 1}, b: {foo?: number}`},
+ 419: {subsumes: false, in: `a: {foo: 1}, b: {foo?: number}`},
+
+ // The one exception of the rule: there is no value of foo that can be
+ // added to b which would cause the unification of a and b to fail.
+ // So an optional field with a value of top is equivalent to not
+ // defining one at all.
+ 420: {subsumes: true, in: `a: {foo?: _}, b: {}`},
+
+ 430: {subsumes: false, in: `a: {[_]: 4}, b: {[_]: int}`},
+ // TODO: handle optionals.
+ 431: {subsumes: false, in: `a: {[_]: int}, b: {[_]: 2}`},
+
+ // 440: {subsumes: true, in: `a: {foo?: 1}, b: {}`, mode: subNoOptional},
+ // 441: {subsumes: true, in: `a: {}, b: {foo?: 1}`, mode: subNoOptional},
+ // 442: {subsumes: true, in: `a: {foo?: 1}, b: {foo: 1}`, mode: subNoOptional},
+ // 443: {subsumes: true, in: `a: {foo?: 1}, b: {foo?: 1}`, mode: subNoOptional},
+ // 444: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subNoOptional},
+ // 445: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subNoOptional},
+ // 446: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subNoOptional},
+ // 447: {subsumes: true, in: `a: {}, b: close({})`, mode: subNoOptional},
+ // 448: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subNoOptional},
+
+ // Lists
+ 506: {subsumes: true, in: `a: [], b: [] `},
+ 507: {subsumes: true, in: `a: [1], b: [1] `},
+ 508: {subsumes: false, in: `a: [1], b: [2] `},
+ 509: {subsumes: false, in: `a: [1], b: [2, 3] `},
+ 510: {subsumes: true, in: `a: [{b: string}], b: [{b: "foo"}] `},
+ 511: {subsumes: true, in: `a: [...{b: string}], b: [{b: "foo"}] `},
+ 512: {subsumes: false, in: `a: [{b: "foo"}], b: [{b: string}] `},
+ 513: {subsumes: false, in: `a: [{b: string}], b: [{b: "foo"}, ...{b: "foo"}] `},
+ 520: {subsumes: false, in: `a: [_, int, ...], b: [int, string, ...string] `},
+
+ // Closed structs.
+ 600: {subsumes: false, in: `a: close({}), b: {a: 1}`},
+ 601: {subsumes: false, in: `a: close({a: 1}), b: {a: 1}`},
+ 602: {subsumes: false, in: `a: close({a: 1, b: 1}), b: {a: 1}`},
+ 603: {subsumes: false, in: `a: {a: 1}, b: close({})`},
+ 604: {subsumes: true, in: `a: {a: 1}, b: close({a: 1})`},
+ 605: {subsumes: true, in: `a: {a: 1}, b: close({a: 1, b: 1})`},
+ 606: {subsumes: true, in: `a: close({b?: 1}), b: close({b: 1})`},
+ 607: {subsumes: false, in: `a: close({b: 1}), b: close({b?: 1})`},
+ 608: {subsumes: true, in: `a: {}, b: close({})`},
+ 609: {subsumes: true, in: `a: {}, b: close({foo?: 1})`},
+ 610: {subsumes: true, in: `a: {foo?:1}, b: close({})`},
+
+ // Definitions are not regular fields.
+ 630: {subsumes: false, in: `a: {#a: 1}, b: {a: 1}`},
+ 631: {subsumes: false, in: `a: {a: 1}, b: {#a: 1}`},
+
+ // // Subsuming final values.
+ // 700: {subsumes: true, in: `a: {[string]: 1}, b: {foo: 1}`, mode: subFinal},
+ // 701: {subsumes: true, in: `a: {[string]: int}, b: {foo: 1}`, mode: subFinal},
+ // 702: {subsumes: true, in: `a: {["foo"]: int}, b: {foo: 1}`, mode: subFinal},
+ // 703: {subsumes: false, in: `a: close({["foo"]: 1}), b: {bar: 1}`, mode: subFinal},
+ // 704: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subFinal},
+ // 705: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subFinal},
+ // 706: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subFinal},
+ // 707: {subsumes: true, in: `a: {}, b: close({})`, mode: subFinal},
+ // 708: {subsumes: false, in: `a: {[string]: 1}, b: {foo: 2}`, mode: subFinal},
+ // 709: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subFinal},
+ // 710: {subsumes: false, in: `a: {foo: [...string]}, b: {}`, mode: subFinal},
+
+ // // Schema values
+ // 800: {subsumes: true, in: `a: close({}), b: {foo: 1}`, mode: subSchema},
+ // // TODO(eval): FIX
+ // // 801: {subsumes: true, in: `a: {[string]: int}, b: {foo: 1}`, mode: subSchema},
+ // 804: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subSchema},
+ // 805: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subSchema},
+ // 806: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subSchema},
+ // 807: {subsumes: true, in: `a: {}, b: close({})`, mode: subSchema},
+ // 808: {subsumes: false, in: `a: {[string]: 1}, b: {foo: 2}`, mode: subSchema},
+ // 809: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subSchema},
+ }
+
+ re := regexp.MustCompile(`a: (.*).*b: ([^\n]*)`)
+ for i, tc := range testCases {
+ if tc.in == "" {
+ continue
+ }
+ m := re.FindStringSubmatch(strings.Join(strings.Split(tc.in, "\n"), ""))
+ const cutset = "\n ,"
+ key := strings.Trim(m[1], cutset) + " ⊑ " + strings.Trim(m[2], cutset)
+
+ r := runtime.New()
+
+ t.Run(strconv.Itoa(i)+"/"+key, func(t *testing.T) {
+
+ file, err := parser.ParseFile("subsume", tc.in)
+ if err != nil {
+ t.Fatal(err)
+ }
+
+ root, errs := compile.Files(nil, r, file)
+ if errs != nil {
+ t.Fatal(errs)
+ }
+
+ ctx := eval.NewContext(r, root)
+ root.Finalize(ctx)
+
+ // Use low-level lookup to avoid evaluation.
+ var a, b adt.Value
+ for _, arc := range root.Arcs {
+ switch arc.Label {
+ case ctx.StringLabel("a"):
+ a = arc
+ case ctx.StringLabel("b"):
+ b = arc
+ }
+ }
+
+ err = Value(ctx, a, b)
+ got := err == nil
+
+ if got != tc.subsumes {
+ t.Errorf("got %v; want %v (%v vs %v)", got, tc.subsumes, a.Kind(), b.Kind())
+ }
+ })
+ }
+}
diff --git a/internal/core/subsume/subsume.go b/internal/core/subsume/subsume.go
new file mode 100644
index 0000000..9ce210a
--- /dev/null
+++ b/internal/core/subsume/subsume.go
@@ -0,0 +1,127 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// Package subsume defines various subsumption relations.
+package subsume
+
+import (
+ "cuelang.org/go/cue/errors"
+ "cuelang.org/go/internal"
+ "cuelang.org/go/internal/core/adt"
+)
+
+// Profile configures the type of subsumption. One should typically use one
+// of the preconfigured profiles.
+type Profile struct {
+ // Final indicates subsumption should only consider fields that are relevant
+ // to data mode, and ignore definitions, hidden fields, pattern constraints
+ // and additional constraints.
+ Final bool
+
+ // Defaults indicate that default values should be used for the subsumed
+ // value.
+ Defaults bool
+
+ // Ignore optional fields.
+ IgnoreOptional bool
+
+ // IgnoreClosedness ignores closedness of structs and is used for comparing
+ // APIs.
+ IgnoreClosedness bool
+}
+
+var CUE = Profile{}
+
+// Final checks subsumption interpreting the subsumed value as data.
+var Final = Profile{
+ Final: true,
+ Defaults: true,
+}
+
+// FinalOpen exists as an artifact of the old API. One should probably not use
+// this.
+var FinalOpen = Profile{
+ Final: true,
+ Defaults: true,
+ IgnoreClosedness: true,
+}
+
+// API is subsumption used for APIs.
+var API = Profile{
+ IgnoreClosedness: true,
+}
+
+// Value subsumes two values based on their logical (evaluated) values.
+func Value(ctx *adt.OpContext, a, b adt.Value) errors.Error {
+ return CUE.Value(ctx, a, b)
+}
+
+func (p *Profile) Value(ctx *adt.OpContext, a, b adt.Value) errors.Error {
+ s := subsumer{ctx: ctx, Profile: *p}
+ if !s.values(a, b) {
+ return s.getError()
+ }
+ return s.errs
+}
+
+// Check reports whether b is an instance of a.
+func (p *Profile) Check(ctx *adt.OpContext, a, b adt.Value) bool {
+ s := subsumer{ctx: ctx, Profile: *p}
+ return s.values(a, b)
+}
+
+func isBottom(x adt.Node) bool {
+ b, _ := x.(*adt.Bottom)
+ return b != nil
+}
+
+type subsumer struct {
+ ctx *adt.OpContext
+ errs errors.Error
+
+ Profile
+
+ inexact bool // If true, the result could be a false negative.
+ missing adt.Feature
+ gt adt.Value
+ lt adt.Value
+}
+
+func (s *subsumer) errf(msg string, args ...interface{}) {
+ b := s.ctx.NewErrf(msg, args...)
+ s.errs = errors.Append(s.errs, b.Err)
+}
+
+func (s *subsumer) getError() (err errors.Error) {
+ c := s.ctx
+ // src := binSrc(token.NoPos, opUnify, gt, lt)
+ if s.gt != nil && s.lt != nil {
+ // src := binSrc(token.NoPos, opUnify, s.gt, s.lt)
+ if s.missing != 0 {
+ s.errf("missing field %q", s.missing.SelectorString(c))
+ } else if b, ok := adt.BinOp(c, adt.AndOp, s.gt, s.lt).(*adt.Bottom); !ok {
+ s.errf("value not an instance")
+ } else {
+ s.errs = errors.Append(s.errs, b.Err)
+ }
+ }
+ if s.errs == nil {
+ s.errf("value not an instance")
+ }
+ err = s.errs
+ if s.inexact {
+ err = internal.DecorateError(internal.ErrInexact, err)
+ }
+ return err
+}
diff --git a/internal/core/subsume/subsume_test.go b/internal/core/subsume/subsume_test.go
new file mode 100644
index 0000000..757c901
--- /dev/null
+++ b/internal/core/subsume/subsume_test.go
@@ -0,0 +1,61 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+ "testing"
+
+ "cuelang.org/go/cue/parser"
+ "cuelang.org/go/internal/core/adt"
+ "cuelang.org/go/internal/core/compile"
+ "cuelang.org/go/internal/core/eval"
+ "cuelang.org/go/internal/core/runtime"
+)
+
+// For debugging purposes, do not remove.
+func TestX(t *testing.T) {
+ t.Skip()
+
+ r := runtime.New()
+ ctx := eval.NewContext(r, nil)
+
+ const gt = `a: *1 | int`
+ const lt = `a: (*1 | int) & 1`
+
+ a := parse(t, ctx, gt)
+ b := parse(t, ctx, lt)
+
+ p := Profile{Defaults: true}
+ err := p.Check(ctx, a, b)
+ t.Error(err)
+}
+
+func parse(t *testing.T, ctx *adt.OpContext, str string) *adt.Vertex {
+ t.Helper()
+
+ file, err := parser.ParseFile("subsume", str)
+ if err != nil {
+ t.Fatal(err)
+ }
+
+ root, errs := compile.Files(nil, ctx, file)
+ if errs != nil {
+ t.Fatal(errs)
+ }
+
+ root.Finalize(ctx)
+
+ return root
+}
diff --git a/internal/core/subsume/value.go b/internal/core/subsume/value.go
new file mode 100644
index 0000000..c6e691f
--- /dev/null
+++ b/internal/core/subsume/value.go
@@ -0,0 +1,298 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+ "bytes"
+
+ "cuelang.org/go/cue/errors"
+ "cuelang.org/go/internal/core/adt"
+)
+
+func (s *subsumer) values(a, b adt.Value) (result bool) {
+ defer func() {
+ if !result && s.gt == nil && s.lt == nil {
+ s.gt = a
+ s.lt = b
+ }
+ }()
+
+ if a == b {
+ return true
+ }
+
+ if s.Defaults {
+ a = adt.Default(a)
+ b = adt.Default(b)
+ }
+
+ switch b := b.(type) {
+ case *adt.Bottom:
+ // If the value is incomplete, the error is not final. So either check
+ // structural equivalence or return an error.
+ return !b.IsIncomplete()
+
+ case *adt.Vertex:
+ if a, ok := a.(*adt.Vertex); ok {
+ return s.vertices(a, b)
+ }
+ // Safe to ignore arcs of w.
+ return s.values(a, b.Value)
+
+ case *adt.Conjunction:
+ if _, ok := a.(*adt.Conjunction); ok {
+ break
+ }
+ for _, y := range b.Values {
+ if s.values(a, y) {
+ return true
+ }
+ }
+ return false
+
+ case *adt.Disjunction:
+ if _, ok := a.(*adt.Disjunction); ok {
+ break
+ }
+
+ for _, y := range b.Values {
+ if !s.values(a, y) {
+ return false
+ }
+ }
+ return true
+
+ case *adt.NodeLink:
+ // Do not descend into NodeLinks to avoid processing cycles.
+ // TODO: this would work better if all equal nodes shared the same
+ // node link.
+ return deref(a) == deref(b)
+ }
+
+ switch x := a.(type) {
+ case *adt.Top:
+ return true
+
+ case *adt.Bottom:
+ // isBottom(b) was already tested above.
+ return false
+
+ case *adt.BasicType:
+ k := b.Kind()
+ return x.K&k == k
+
+ case *adt.BoundValue:
+ return s.bound(x, b)
+
+ case *adt.Builtin:
+ return x == b
+
+ case *adt.BuiltinValidator:
+ if y := s.ctx.Validate(x, b); y != nil {
+ s.errs = errors.Append(s.errs, y.Err)
+ return false
+ }
+ return true
+
+ case *adt.Null:
+ return b.Kind() == adt.NullKind
+
+ case *adt.Bool:
+ y, ok := b.(*adt.Bool)
+ return ok && x.B == y.B
+
+ case *adt.Num:
+ y, ok := b.(*adt.Num)
+ return ok && x.K&y.K == y.K && test(s.ctx, x, adt.EqualOp, x, y)
+
+ case *adt.String:
+ y, ok := b.(*adt.String)
+ return ok && x.Str == y.Str
+
+ case *adt.Bytes:
+ y, ok := b.(*adt.Bytes)
+ return ok && bytes.Equal(x.B, y.B)
+
+ case *adt.Vertex:
+ y, ok := b.(*adt.Vertex)
+ if !ok {
+ // // Under what conditions can we cast to the value?
+ if len(x.Arcs) == 0 && x.Value != nil {
+ return s.values(x.Value, b)
+ }
+ return false
+ }
+ return s.vertices(x, y)
+
+ case *adt.Conjunction:
+ if y, ok := b.(*adt.Conjunction); ok {
+ // A Conjunction subsumes another Conjunction if for all values a in
+ // x there is a value b in y such that a subsumes b.
+ //
+ // This assumes overlapping ranges in disjunctions are merged.If
+ // this is not the case, subsumes will return a false negative,
+ // which is allowed.
+ outerC:
+ for _, a := range x.Values {
+ for _, b := range y.Values {
+ if s.values(a, b) {
+ continue outerC
+ }
+ }
+ // TODO: should this be marked as inexact?
+ return false
+ }
+ return true
+ }
+ subsumed := true
+ for _, a := range x.Values {
+ subsumed = subsumed && s.values(a, b)
+ }
+ return subsumed
+
+ case *adt.Disjunction:
+ // A Disjunction subsumes another Disjunction if all values of y are
+ // subsumed by any of the values of x, and default values in y are
+ // subsumed by the default values of x.
+ //
+ // This assumes that overlapping ranges in x are merged. If this is not
+ // the case, subsumes will return a false negative, which is allowed.
+ if y, ok := b.(*adt.Disjunction); ok {
+ // at least one value in x should subsume each value in d.
+ outerD:
+ for i, b := range y.Values {
+ bDefault := i < y.NumDefaults
+ // v is subsumed if any value in x subsumes v.
+ for j, a := range x.Values {
+ aDefault := j < x.NumDefaults
+ if (aDefault || !bDefault) && s.values(a, b) {
+ continue outerD
+ }
+ }
+ return false
+ }
+ return true
+ }
+ // b is subsumed if any value in x subsumes b.
+ for _, a := range x.Values {
+ if s.values(a, b) {
+ return true
+ }
+ }
+ // TODO: should this be marked as inexact?
+ return false
+
+ case *adt.NodeLink:
+ return deref(x) == deref(b)
+ }
+ return false
+}
+
+func deref(v adt.Expr) *adt.Vertex {
+ switch x := v.(type) {
+ case *adt.Vertex:
+ return x
+ case *adt.NodeLink:
+ return x.Node
+ }
+ return nil
+}
+
+func (s *subsumer) bound(x *adt.BoundValue, v adt.Value) bool {
+ ctx := s.ctx
+ if isBottom(v) {
+ return true
+ }
+
+ switch y := v.(type) {
+ case *adt.BoundValue:
+ if !adt.IsConcrete(y.Value) {
+ return false
+ }
+
+ kx := x.Kind()
+ ky := y.Kind()
+ if (kx&ky)&^kx != 0 {
+ return false
+ }
+ // x subsumes y if
+ // x: >= a, y: >= b ==> a <= b
+ // x: >= a, y: > b ==> a <= b
+ // x: > a, y: > b ==> a <= b
+ // x: > a, y: >= b ==> a < b
+ //
+ // x: <= a, y: <= b ==> a >= b
+ //
+ // x: != a, y: != b ==> a != b
+ //
+ // false if types or op direction doesn't match
+
+ xv := x.Value
+ yv := y.Value
+ switch x.Op {
+ case adt.GreaterThanOp:
+ if y.Op == adt.GreaterEqualOp {
+ return test(ctx, x, adt.LessThanOp, xv, yv)
+ }
+ fallthrough
+ case adt.GreaterEqualOp:
+ if y.Op == adt.GreaterThanOp || y.Op == adt.GreaterEqualOp {
+ return test(ctx, x, adt.LessEqualOp, xv, yv)
+ }
+ case adt.LessThanOp:
+ if y.Op == adt.LessEqualOp {
+ return test(ctx, x, adt.GreaterThanOp, xv, yv)
+ }
+ fallthrough
+ case adt.LessEqualOp:
+ if y.Op == adt.LessThanOp || y.Op == adt.LessEqualOp {
+ return test(ctx, x, adt.GreaterEqualOp, xv, yv)
+ }
+ case adt.NotEqualOp:
+ switch y.Op {
+ case adt.NotEqualOp:
+ return test(ctx, x, adt.EqualOp, xv, yv)
+ case adt.GreaterEqualOp:
+ return test(ctx, x, adt.LessThanOp, xv, yv)
+ case adt.GreaterThanOp:
+ return test(ctx, x, adt.LessEqualOp, xv, yv)
+ case adt.LessThanOp:
+ return test(ctx, x, adt.GreaterEqualOp, xv, yv)
+ case adt.LessEqualOp:
+ return test(ctx, x, adt.GreaterThanOp, xv, yv)
+ }
+
+ case adt.MatchOp, adt.NotMatchOp:
+ // these are just approximations
+ if y.Op == x.Op {
+ return test(ctx, x, adt.EqualOp, xv, yv)
+ }
+
+ default:
+ // adt.NotEqualOp already handled above.
+ panic("cue: undefined bound mode")
+ }
+
+ case *adt.Num, *adt.String, *adt.Bool:
+ return test(ctx, x, x.Op, y, x.Value)
+ }
+ return false
+}
+
+func test(ctx *adt.OpContext, src adt.Node, op adt.Op, gt, lt adt.Value) bool {
+ x := adt.BinOp(ctx, op, gt, lt)
+ b, ok := x.(*adt.Bool)
+ return ok && b.B
+}
diff --git a/internal/core/subsume/value_test.go b/internal/core/subsume/value_test.go
new file mode 100644
index 0000000..80869c4
--- /dev/null
+++ b/internal/core/subsume/value_test.go
@@ -0,0 +1,427 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+ "regexp"
+ "strconv"
+ "strings"
+ "testing"
+
+ "cuelang.org/go/cue/parser"
+ "cuelang.org/go/internal/core/adt"
+ "cuelang.org/go/internal/core/compile"
+ "cuelang.org/go/internal/core/eval"
+ "cuelang.org/go/internal/core/runtime"
+)
+
+const (
+ subNone = iota
+ subFinal
+ subNoOptional
+ subSchema
+)
+
+func TestValues(t *testing.T) {
+ // Do not inline: the named struct is used as a marker in
+ // testdata/gen.go.
+ type subsumeTest struct {
+ // the result of b ⊑ a, where a and b are defined in "in"
+ subsumes bool
+ in string
+ mode int
+ }
+ testCases := []subsumeTest{
+ // Top subsumes everything
+ 0: {subsumes: true, in: `a: _, b: _ `},
+ 1: {subsumes: true, in: `a: _, b: null `},
+ 2: {subsumes: true, in: `a: _, b: int `},
+ 3: {subsumes: true, in: `a: _, b: 1 `},
+ 4: {subsumes: true, in: `a: _, b: float `},
+ 5: {subsumes: true, in: `a: _, b: "s" `},
+ 6: {subsumes: true, in: `a: _, b: {} `},
+ 7: {subsumes: true, in: `a: _, b: []`},
+ 8: {subsumes: true, in: `a: _, b: _|_ `},
+
+ // Nothing besides top subsumed top
+ 9: {subsumes: false, in: `a: null, b: _`},
+ 10: {subsumes: false, in: `a: int, b: _`},
+ 11: {subsumes: false, in: `a: 1, b: _`},
+ 12: {subsumes: false, in: `a: float, b: _`},
+ 13: {subsumes: false, in: `a: "s", b: _`},
+ 14: {subsumes: false, in: `a: {}, b: _`},
+ 15: {subsumes: false, in: `a: [], b: _`},
+ 16: {subsumes: false, in: `a: _|_ , b: _`},
+
+ // Bottom subsumes nothing except bottom itself.
+ 17: {subsumes: false, in: `a: _|_, b: null `},
+ 18: {subsumes: false, in: `a: _|_, b: int `},
+ 19: {subsumes: false, in: `a: _|_, b: 1 `},
+ 20: {subsumes: false, in: `a: _|_, b: float `},
+ 21: {subsumes: false, in: `a: _|_, b: "s" `},
+ 22: {subsumes: false, in: `a: _|_, b: {} `},
+ 23: {subsumes: false, in: `a: _|_, b: [] `},
+ 24: {subsumes: true, in: ` a: _|_, b: _|_ `},
+
+ // All values subsume bottom
+ 25: {subsumes: true, in: `a: null, b: _|_`},
+ 26: {subsumes: true, in: `a: int, b: _|_`},
+ 27: {subsumes: true, in: `a: 1, b: _|_`},
+ 28: {subsumes: true, in: `a: float, b: _|_`},
+ 29: {subsumes: true, in: `a: "s", b: _|_`},
+ 30: {subsumes: true, in: `a: {}, b: _|_`},
+ 31: {subsumes: true, in: `a: [], b: _|_`},
+ 32: {subsumes: true, in: `a: true, b: _|_`},
+ 33: {subsumes: true, in: `a: _|_, b: _|_`},
+
+ // null subsumes only null
+ 34: {subsumes: true, in: ` a: null, b: null `},
+ 35: {subsumes: false, in: `a: null, b: 1 `},
+ 36: {subsumes: false, in: `a: 1, b: null `},
+
+ 37: {subsumes: true, in: ` a: true, b: true `},
+ 38: {subsumes: false, in: `a: true, b: false `},
+
+ 39: {subsumes: true, in: ` a: "a", b: "a" `},
+ 40: {subsumes: false, in: `a: "a", b: "b" `},
+ 41: {subsumes: true, in: ` a: string, b: "a" `},
+ 42: {subsumes: false, in: `a: "a", b: string `},
+
+ // Number typing (TODO)
+ //
+ // In principle, an "int" cannot assume an untyped "1", as "1" may
+ // still by typed as a float. They are two different type aspects. When
+ // considering, keep in mind that:
+ // Key requirement: if A subsumes B, it must not be possible to
+ // specialize B further such that A does not subsume B. HOWEVER,
+ // The type conversion rules for conversion are INDEPENDENT of the
+ // rules for subsumption!
+ // Consider:
+ // - only having number, but allowing user-defined types.
+ // Subsumption would still work the same, but it may be somewhat
+ // less weird.
+ // - making 1 always an int and 1.0 always a float.
+ // - the int type would subsume any derived type from int.
+ // - arithmetic would allow implicit conversions, but maybe not for
+ // types.
+ //
+ // TODO: irrational numbers: allow untyped, but require explicit
+ // trunking when assigning to float.
+ //
+ // a: number; cue.IsInteger(a) && a > 0
+ // t: (x) -> number; cue.IsInteger(a) && a > 0
+ // type x number: cue.IsInteger(x) && x > 0
+ // x: typeOf(number); cue.IsInteger(x) && x > 0
+ 43: {subsumes: true, in: `a: 1, b: 1 `},
+ 44: {subsumes: true, in: `a: 1.0, b: 1.0 `},
+ 45: {subsumes: true, in: `a: 3.0, b: 3.0 `},
+ 46: {subsumes: false, in: `a: 1.0, b: 1 `},
+ 47: {subsumes: false, in: `a: 1, b: 1.0 `},
+ 48: {subsumes: false, in: `a: 3, b: 3.0`},
+ 49: {subsumes: true, in: `a: int, b: 1`},
+ 50: {subsumes: true, in: `a: int, b: int & 1`},
+ 51: {subsumes: true, in: `a: float, b: 1.0`},
+ 52: {subsumes: false, in: `a: float, b: 1`},
+ 53: {subsumes: false, in: `a: int, b: 1.0`},
+ 54: {subsumes: true, in: `a: int, b: int`},
+ 55: {subsumes: true, in: `a: number, b: int`},
+
+ // Structs
+ 64: {subsumes: true, in: `a: {}, b: {}`},
+ 65: {subsumes: true, in: `a: {}, b: {a: 1}`},
+ 66: {subsumes: true, in: `a: {a:1}, b: {a:1, b:1}`},
+ 67: {subsumes: true, in: `a: {s: { a:1} }, b: { s: { a:1, b:2 }}`},
+ 68: {subsumes: true, in: `a: {}, b: {}`},
+ // TODO: allow subsumption of unevaluated values?
+ // ref not yet evaluated and not structurally equivalent
+ 69: {subsumes: true, in: `a: {}, b: {} & c, c: {}`},
+
+ 70: {subsumes: false, in: `a: {a:1}, b: {}`},
+ 71: {subsumes: false, in: `a: {a:1, b:1}, b: {a:1}`},
+ 72: {subsumes: false, in: `a: {s: { a:1} }, b: { s: {}}`},
+
+ 84: {subsumes: true, in: `a: 1 | 2, b: 2 | 1`},
+ 85: {subsumes: true, in: `a: 1 | 2, b: 1 | 2`},
+
+ 86: {subsumes: true, in: `a: number, b: 2 | 1`},
+ 87: {subsumes: true, in: `a: number, b: 2 | 1`},
+ 88: {subsumes: false, in: `a: int, b: 1 | 2 | 3.1`},
+
+ 89: {subsumes: true, in: `a: float | number, b: 1 | 2 | 3.1`},
+
+ 90: {subsumes: false, in: `a: int, b: 1 | 2 | 3.1`},
+ 91: {subsumes: true, in: `a: 1 | 2, b: 1`},
+ 92: {subsumes: true, in: `a: 1 | 2, b: 2`},
+ 93: {subsumes: false, in: `a: 1 | 2, b: 3`},
+
+ // 147: {subsumes: true, in: ` a: 7080, b: *7080 | int`, mode: subChoose},
+
+ // Defaults
+ 150: {subsumes: false, in: `a: number | *1, b: number | *2`},
+ 151: {subsumes: true, in: `a: number | *2, b: number | *2`},
+ 152: {subsumes: true, in: `a: int | *float, b: int | *2.0`},
+ 153: {subsumes: false, in: `a: int | *2, b: int | *2.0`},
+ 154: {subsumes: true, in: `a: number | *2 | *3, b: number | *2`},
+ 155: {subsumes: true, in: `a: number, b: number | *2`},
+
+ // Bounds
+ 170: {subsumes: true, in: `a: >=2, b: >=2`},
+ 171: {subsumes: true, in: `a: >=1, b: >=2`},
+ 172: {subsumes: true, in: `a: >0, b: >=2`},
+ 173: {subsumes: true, in: `a: >1, b: >1`},
+ 174: {subsumes: true, in: `a: >=1, b: >1`},
+ 175: {subsumes: false, in: `a: >1, b: >=1`},
+ 176: {subsumes: true, in: `a: >=1, b: >=1`},
+ 177: {subsumes: true, in: `a: <1, b: <1`},
+ 178: {subsumes: true, in: `a: <=1, b: <1`},
+ 179: {subsumes: false, in: `a: <1, b: <=1`},
+ 180: {subsumes: true, in: `a: <=1, b: <=1`},
+
+ 181: {subsumes: true, in: `a: !=1, b: !=1`},
+ 182: {subsumes: false, in: `a: !=1, b: !=2`},
+
+ 183: {subsumes: false, in: `a: !=1, b: <=1`},
+ 184: {subsumes: true, in: `a: !=1, b: <1`},
+ 185: {subsumes: false, in: `a: !=1, b: >=1`},
+ 186: {subsumes: true, in: `a: !=1, b: <1`},
+
+ 187: {subsumes: true, in: `a: !=1, b: <=0`},
+ 188: {subsumes: true, in: `a: !=1, b: >=2`},
+ 189: {subsumes: true, in: `a: !=1, b: >1`},
+
+ 195: {subsumes: false, in: `a: >=2, b: !=2`},
+ 196: {subsumes: false, in: `a: >2, b: !=2`},
+ 197: {subsumes: false, in: `a: <2, b: !=2`},
+ 198: {subsumes: false, in: `a: <=2, b: !=2`},
+
+ 200: {subsumes: true, in: `a: =~"foo", b: =~"foo"`},
+ 201: {subsumes: false, in: `a: =~"foo", b: =~"bar"`},
+ 202: {subsumes: false, in: `a: =~"foo1", b: =~"foo"`},
+
+ 203: {subsumes: true, in: `a: !~"foo", b: !~"foo"`},
+ 204: {subsumes: false, in: `a: !~"foo", b: !~"bar"`},
+ 205: {subsumes: false, in: `a: !~"foo", b: !~"foo1"`},
+
+ // The following is could be true, but we will not go down the rabbit
+ // hold of trying to prove subsumption of regular expressions.
+ 210: {subsumes: false, in: `a: =~"foo", b: =~"foo1"`},
+ 211: {subsumes: false, in: `a: !~"foo1", b: !~"foo"`},
+
+ 220: {subsumes: true, in: `a: <5, b: 4`},
+ 221: {subsumes: false, in: `a: <5, b: 5`},
+ 222: {subsumes: true, in: `a: <=5, b: 5`},
+ 223: {subsumes: false, in: `a: <=5.0, b: 5.00000001`},
+ 224: {subsumes: true, in: `a: >5, b: 6`},
+ 225: {subsumes: false, in: `a: >5, b: 5`},
+ 226: {subsumes: true, in: `a: >=5, b: 5`},
+ 227: {subsumes: false, in: `a: >=5, b: 4`},
+ 228: {subsumes: true, in: `a: !=5, b: 6`},
+ 229: {subsumes: false, in: `a: !=5, b: 5`},
+ 230: {subsumes: false, in: `a: !=5.0, b: 5.0`},
+ 231: {subsumes: false, in: `a: !=5.0, b: 5`},
+
+ 250: {subsumes: true, in: `a: =~ #"^\d{3}$"#, b: "123"`},
+ 251: {subsumes: false, in: `a: =~ #"^\d{3}$"#, b: "1234"`},
+ 252: {subsumes: true, in: `a: !~ #"^\d{3}$"#, b: "1234"`},
+ 253: {subsumes: false, in: `a: !~ #"^\d{3}$"#, b: "123"`},
+
+ // Conjunctions
+ 300: {subsumes: true, in: `a: >0, b: >=2 & <=100`},
+ 301: {subsumes: false, in: `a: >0, b: >=0 & <=100`},
+
+ 310: {subsumes: true, in: `a: >=0 & <=100, b: 10`},
+ 311: {subsumes: true, in: `a: >=0 & <=100, b: >=0 & <=100`},
+ 312: {subsumes: false, in: `a: !=2 & !=4, b: >3`},
+ 313: {subsumes: true, in: `a: !=2 & !=4, b: >5`},
+
+ 314: {subsumes: false, in: `a: >=0 & <=100, b: >=0 & <=150`},
+ 315: {subsumes: true, in: `a: >=0 & <=150, b: >=0 & <=100`},
+
+ // Disjunctions
+ 330: {subsumes: true, in: `a: >5, b: >10 | 8`},
+ 331: {subsumes: false, in: `a: >8, b: >10 | 8`},
+
+ // Optional fields
+ // Optional fields defined constraints on fields that are not yet
+ // defined. So even if such a field is not part of the output, it
+ // influences the lattice structure.
+ // For a given A and B, where A and B unify and where A has an optional
+ // field that is not defined in B, the addition of an incompatible
+ // value of that field in B can cause A and B to no longer unify.
+ //
+ 400: {subsumes: false, in: `a: {foo: 1}, b: {}`},
+ 401: {subsumes: false, in: `a: {foo?: 1}, b: {}`},
+ 402: {subsumes: true, in: `a: {}, b: {foo: 1}`},
+ 403: {subsumes: true, in: `a: {}, b: {foo?: 1}`},
+
+ 404: {subsumes: true, in: `a: {foo: 1}, b: {foo: 1}`},
+ 405: {subsumes: true, in: `a: {foo?: 1}, b: {foo: 1}`},
+ 406: {subsumes: true, in: `a: {foo?: 1}, b: {foo?: 1}`},
+ 407: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`},
+
+ 408: {subsumes: false, in: `a: {foo: 1}, b: {foo: 2}`},
+ 409: {subsumes: false, in: `a: {foo?: 1}, b: {foo: 2}`},
+ 410: {subsumes: false, in: `a: {foo?: 1}, b: {foo?: 2}`},
+ 411: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 2}`},
+
+ 412: {subsumes: true, in: `a: {foo: number}, b: {foo: 2}`},
+ 413: {subsumes: true, in: `a: {foo?: number}, b: {foo: 2}`},
+ 414: {subsumes: true, in: `a: {foo?: number}, b: {foo?: 2}`},
+ 415: {subsumes: false, in: `a: {foo: number}, b: {foo?: 2}`},
+
+ 416: {subsumes: false, in: `a: {foo: 1}, b: {foo: number}`},
+ 417: {subsumes: false, in: `a: {foo?: 1}, b: {foo: number}`},
+ 418: {subsumes: false, in: `a: {foo?: 1}, b: {foo?: number}`},
+ 419: {subsumes: false, in: `a: {foo: 1}, b: {foo?: number}`},
+
+ // The one exception of the rule: there is no value of foo that can be
+ // added to b which would cause the unification of a and b to fail.
+ // So an optional field with a value of top is equivalent to not
+ // defining one at all.
+ 420: {subsumes: true, in: `a: {foo?: _}, b: {}`},
+
+ 430: {subsumes: false, in: `a: {[_]: 4}, b: {[_]: int}`},
+ // TODO: handle optionals.
+ 431: {subsumes: false, in: `a: {[_]: int}, b: {[_]: 2}`},
+
+ // TODO: the subNoOptional mode used to be used by the equality check.
+ // Now this has its own implementation it is no longer necessary. Keep
+ // around for now in case we still need the more permissive equality
+ // check that can be created by using subsumption.
+ //
+ // 440: {subsumes: true, in: `a: {foo?: 1}, b: {}`, mode: subNoOptional},
+ // 441: {subsumes: true, in: `a: {}, b: {foo?: 1}`, mode: subNoOptional},
+ // 442: {subsumes: true, in: `a: {foo?: 1}, b: {foo: 1}`, mode: subNoOptional},
+ // 443: {subsumes: true, in: `a: {foo?: 1}, b: {foo?: 1}`, mode: subNoOptional},
+ // 444: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subNoOptional},
+ // 445: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subNoOptional},
+ // 446: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subNoOptional},
+ // 447: {subsumes: true, in: `a: {}, b: close({})`, mode: subNoOptional},
+ // 448: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subNoOptional},
+
+ // Lists
+ 506: {subsumes: true, in: `a: [], b: [] `},
+ 507: {subsumes: true, in: `a: [1], b: [1] `},
+ 508: {subsumes: false, in: `a: [1], b: [2] `},
+ 509: {subsumes: false, in: `a: [1], b: [2, 3] `},
+ 510: {subsumes: true, in: `a: [{b: string}], b: [{b: "foo"}] `},
+ 511: {subsumes: true, in: `a: [...{b: string}], b: [{b: "foo"}] `},
+ 512: {subsumes: false, in: `a: [{b: "foo"}], b: [{b: string}] `},
+ 513: {subsumes: false, in: `a: [{b: string}], b: [{b: "foo"}, ...{b: "foo"}] `},
+ 520: {subsumes: false, in: `a: [_, int, ...], b: [int, string, ...string] `},
+
+ // Closed structs.
+ 600: {subsumes: false, in: `a: close({}), b: {a: 1}`},
+ 601: {subsumes: false, in: `a: close({a: 1}), b: {a: 1}`},
+ 602: {subsumes: false, in: `a: close({a: 1, b: 1}), b: {a: 1}`},
+ 603: {subsumes: false, in: `a: {a: 1}, b: close({})`},
+ 604: {subsumes: true, in: `a: {a: 1}, b: close({a: 1})`},
+ 605: {subsumes: true, in: `a: {a: 1}, b: close({a: 1, b: 1})`},
+ 606: {subsumes: true, in: `a: close({b?: 1}), b: close({b: 1})`},
+ 607: {subsumes: false, in: `a: close({b: 1}), b: close({b?: 1})`},
+ 608: {subsumes: true, in: `a: {}, b: close({})`},
+ 609: {subsumes: true, in: `a: {}, b: close({foo?: 1})`},
+ 610: {subsumes: true, in: `a: {foo?:1}, b: close({})`},
+
+ // New in new evaluator.
+ 611: {subsumes: false, in: `a: close({foo?:1}), b: close({bar?: 1})`},
+ 612: {subsumes: true, in: `a: {foo?:1}, b: close({bar?: 1})`},
+ 613: {subsumes: true, in: `a: {foo?:1}, b: close({bar: 1})`},
+
+ // Definitions are not regular fields.
+ 630: {subsumes: false, in: `a: {#a: 1}, b: {a: 1}`},
+ 631: {subsumes: false, in: `a: {a: 1}, b: {#a: 1}`},
+
+ // Subsuming final values.
+ 700: {subsumes: true, in: `a: {[string]: 1}, b: {foo: 1}`, mode: subFinal},
+ 701: {subsumes: true, in: `a: {[string]: int}, b: {foo: 1}`, mode: subFinal},
+ 702: {subsumes: true, in: `a: {["foo"]: int}, b: {foo: 1}`, mode: subFinal},
+ 703: {subsumes: false, in: `a: close({["foo"]: 1}), b: {bar: 1}`, mode: subFinal},
+ 704: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subFinal},
+ 705: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subFinal},
+ 706: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subFinal},
+ 707: {subsumes: true, in: `a: {}, b: close({})`, mode: subFinal},
+ 708: {subsumes: false, in: `a: {[string]: 1}, b: {foo: 2}`, mode: subFinal},
+ 709: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subFinal},
+ 710: {subsumes: false, in: `a: {foo: [...string]}, b: {}`, mode: subFinal},
+
+ // Schema values
+ 800: {subsumes: true, in: `a: close({}), b: {foo: 1}`, mode: subSchema},
+ // TODO(eval): FIX
+ // 801: {subsumes: true, in: `a: {[string]: int}, b: {foo: 1}`, mode: subSchema},
+ 804: {subsumes: false, in: `a: {foo: 1}, b: {foo?: 1}`, mode: subSchema},
+ 805: {subsumes: true, in: `a: close({}), b: {foo?: 1}`, mode: subSchema},
+ 806: {subsumes: true, in: `a: close({}), b: close({foo?: 1})`, mode: subSchema},
+ 807: {subsumes: true, in: `a: {}, b: close({})`, mode: subSchema},
+ 808: {subsumes: false, in: `a: {[string]: 1}, b: {foo: 2}`, mode: subSchema},
+ 809: {subsumes: true, in: `a: {}, b: close({foo?: 1})`, mode: subSchema},
+ }
+
+ re := regexp.MustCompile(`a: (.*).*b: ([^\n]*)`)
+ for i, tc := range testCases {
+ if tc.in == "" {
+ continue
+ }
+ m := re.FindStringSubmatch(strings.Join(strings.Split(tc.in, "\n"), ""))
+ const cutset = "\n ,"
+ key := strings.Trim(m[1], cutset) + " ⊑ " + strings.Trim(m[2], cutset)
+
+ r := runtime.New()
+
+ t.Run(strconv.Itoa(i)+"/"+key, func(t *testing.T) {
+
+ file, err := parser.ParseFile("subsume", tc.in)
+ if err != nil {
+ t.Fatal(err)
+ }
+
+ root, errs := compile.Files(nil, r, file)
+ if errs != nil {
+ t.Fatal(errs)
+ }
+
+ ctx := eval.NewContext(r, root)
+ root.Finalize(ctx)
+
+ // Use low-level lookup to avoid evaluation.
+ var a, b adt.Value
+ for _, arc := range root.Arcs {
+ switch arc.Label {
+ case ctx.StringLabel("a"):
+ a = arc
+ case ctx.StringLabel("b"):
+ b = arc
+ }
+ }
+
+ switch tc.mode {
+ case subNone:
+ err = Value(ctx, a, b)
+ case subSchema:
+ err = API.Value(ctx, a, b)
+ // TODO: see comments above.
+ // case subNoOptional:
+ // err = IgnoreOptional.Value(ctx, a, b)
+ case subFinal:
+ err = Final.Value(ctx, a, b)
+ }
+ got := err == nil
+
+ if got != tc.subsumes {
+ t.Errorf("got %v; want %v (%v vs %v)", got, tc.subsumes, a.Kind(), b.Kind())
+ }
+ })
+ }
+}
diff --git a/internal/core/subsume/vertex.go b/internal/core/subsume/vertex.go
new file mode 100644
index 0000000..6ece49e
--- /dev/null
+++ b/internal/core/subsume/vertex.go
@@ -0,0 +1,256 @@
+// Copyright 2020 CUE Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package subsume
+
+import (
+ "cuelang.org/go/internal/core/adt"
+ "cuelang.org/go/internal/core/export"
+)
+
+// Notes:
+// - Can optional fields of y can always be ignored here? Maybe not in the
+// schema case.
+// - Definitions of y can be ignored in data mode.
+//
+// TODO(perf): use merge sort where possible.
+func (s *subsumer) vertices(x, y *adt.Vertex) bool {
+ if x == y {
+ return true
+ }
+
+ if s.Defaults {
+ x = x.Default()
+ y = y.Default()
+ }
+
+ if b, _ := y.Value.(*adt.Bottom); b != nil {
+ // If the value is incomplete, the error is not final. So either check
+ // structural equivalence or return an error.
+ return !b.IsIncomplete()
+ }
+
+ ctx := s.ctx
+
+ final := y.IsData() || s.Final
+
+ switch v := x.Value.(type) {
+ case *adt.Bottom:
+ return false
+
+ case *adt.ListMarker:
+ if !y.IsList() {
+ s.errf("list does not subsume %s (type %s)", ctx.Str(y), y.Kind())
+ return false
+ }
+ if !s.listVertices(x, y) {
+ return false
+ }
+ // TODO: allow other arcs alongside list arc.
+ return true
+
+ case *adt.StructMarker:
+ _, ok := y.Value.(*adt.StructMarker)
+ if !ok {
+ return false
+ }
+
+ default:
+ if !s.values(v, y.Value) {
+ return false
+ }
+
+ // Embedded scalars could still have arcs.
+ if final {
+ return true
+ }
+ }
+
+ xClosed := x.IsClosed(ctx) && !s.IgnoreClosedness
+ yClosed := y.IsClosed(ctx) && !s.IgnoreClosedness
+
+ if xClosed && !yClosed && !final {
+ return false
+ }
+
+ types := x.OptionalTypes()
+ if !final && !s.IgnoreOptional && types&(adt.HasPattern|adt.HasAdditional) != 0 {
+ // TODO: there are many cases where pattern constraints can be checked.
+ s.inexact = true
+ return false
+ }
+
+ // All arcs in x must exist in y and its values must subsume.
+ xFeatures := export.VertexFeatures(x)
+ for _, f := range xFeatures {
+ if s.Final && !f.IsRegular() {
+ continue
+ }
+
+ a := x.Lookup(f)
+ aOpt := false
+ if a == nil {
+ // x.f is optional
+ if s.IgnoreOptional {
+ continue
+ }
+
+ a = &adt.Vertex{Label: f}
+ x.MatchAndInsert(ctx, a)
+ a.Finalize(ctx)
+
+ // If field a is optional and has value top, neither the
+ // omission of the field nor the field defined with any value
+ // may cause unification to fail.
+ if a.Kind() == adt.TopKind {
+ continue
+ }
+
+ aOpt = true
+ }
+
+ b := y.Lookup(f)
+ if b == nil {
+ // y.f is optional
+ if !aOpt {
+ s.errf("required field %s is optional in subsumed value",
+ f.SelectorString(ctx))
+ return false
+ }
+
+ // If f is undefined for y and if y is closed, the field is
+ // implicitly defined as _|_ and thus subsumed. Technically, this is
+ // even true if a is not optional, but in that case it means that y
+ // is invalid, so return false regardless
+ if !y.Accept(ctx, f) || y.IsData() || s.Final {
+ continue
+ }
+
+ b = &adt.Vertex{Label: f}
+ y.MatchAndInsert(ctx, b)
+ b.Finalize(ctx)
+ }
+
+ if s.values(a, b) {
+ continue
+ }
+
+ s.missing = f
+ s.gt = a
+ s.lt = y
+
+ s.errf("field %s not not present in %s",
+ f.SelectorString(ctx), ctx.Str(y))
+ return false
+ }
+
+ if xClosed && !yClosed && !s.Final {
+ s.errf("closed struct does not subsume open struct")
+ return false
+ }
+
+ yFeatures := export.VertexFeatures(y)
+outer:
+ for _, f := range yFeatures {
+ if s.Final && !f.IsRegular() {
+ continue
+ }
+
+ for _, g := range xFeatures {
+ if g == f {
+ // already validated
+ continue outer
+ }
+ }
+
+ b := y.Lookup(f)
+ if b == nil {
+ if s.IgnoreOptional || s.Final {
+ continue
+ }
+
+ b = &adt.Vertex{Label: f}
+ y.MatchAndInsert(ctx, b)
+ }
+
+ if !x.Accept(ctx, f) {
+ if s.Profile.IgnoreClosedness {
+ continue
+ }
+ s.errf("field %s not allowed in closed struct",
+ f.SelectorString(ctx))
+ return false
+ }
+
+ a := &adt.Vertex{Label: f}
+ x.MatchAndInsert(ctx, a)
+ if len(a.Conjuncts) == 0 {
+ // It is accepted and has no further constraints, so all good.
+ continue
+ }
+
+ a.Finalize(ctx)
+ b.Finalize(ctx)
+
+ if !s.vertices(a, b) {
+ return false
+ }
+ }
+
+ return true
+}
+
+func (s *subsumer) listVertices(x, y *adt.Vertex) bool {
+ ctx := s.ctx
+
+ if !y.IsData() && x.IsClosed(ctx) && !y.IsClosed(ctx) {
+ return false
+ }
+
+ xElems := x.Elems()
+ yElems := y.Elems()
+
+ switch {
+ case len(xElems) == len(yElems):
+ case len(xElems) > len(yElems):
+ return false
+ case x.IsClosed(ctx):
+ return false
+ default:
+ a := &adt.Vertex{Label: adt.InvalidLabel}
+ x.MatchAndInsert(ctx, a)
+ a.Finalize(ctx)
+
+ // x must be open
+ for _, b := range yElems[len(xElems):] {
+ if !s.vertices(a, b) {
+ return false
+ }
+ }
+
+ if !y.IsClosed(ctx) {
+ b := &adt.Vertex{Label: adt.InvalidLabel}
+ y.MatchAndInsert(ctx, b)
+ b.Finalize(ctx)
+ }
+ }
+
+ for i, a := range xElems {
+ if !s.vertices(a, yElems[i]) {
+ return false
+ }
+ }
+
+ return true
+}
