doc/ref/spec.md: change disjunction rule
Closes #577
This change aims to make default handling more intuitive and
easier to reason about, both for the implementation and user.
This also removes the O1 rule, which is inconsitent
with the above text and not reflecting the implementation
(defaults are always chosen when used as operand to
an operator other than & or |).
This change has the nice mathematical property that
combining terms in resolving disjunctions uses the
same commutative operation for determing default
status regardless of whether it concerns resolving
nested disjunctions or distributing a unification over
disjunctions.
It makes several cases more intuitive and simplifies
reasoning over the implementation.
Closes #625
Change-Id: Ie483b9f2bbfd17756590f74a141f6cec9628baed
Reviewed-on: https://cue-review.googlesource.com/c/cue/+/8001
Reviewed-by: Marcel van Lohuizen <mpvl@golang.org>
diff --git a/cue/testdata/basicrewrite/014_disjunctions.txtar b/cue/testdata/basicrewrite/014_disjunctions.txtar
index 2172cb7..a691403 100644
--- a/cue/testdata/basicrewrite/014_disjunctions.txtar
+++ b/cue/testdata/basicrewrite/014_disjunctions.txtar
@@ -14,8 +14,8 @@
o9: (2 | 3) & (1 | 2 | 3)
o10: (3 | 2) & (1 | *2 | 3)
-m1: (*1 | (*2 | 3)) & (>=2 & <=3)
-m2: (*1 | (*2 | 3)) & (2 | 3)
+m1: (1 | (*2 | 3)) & (>=2 & <=3)
+m2: (1 | (*2 | 3)) & (2 | 3)
m3: (*1 | *(*2 | 3)) & (2 | 3)
m4: (2 | 3) & (*2 | 3)
m5: (*2 | 3) & (2 | 3)
@@ -69,8 +69,8 @@
o8: ((1|2|3) & (3|2))
o9: ((2|3) & (1|2|3))
o10: ((3|2) & (1|*2|3))
- m1: ((*1|(*2|3)) & (>=2 & <=3))
- m2: ((*1|(*2|3)) & (2|3))
+ m1: ((1|(*2|3)) & (>=2 & <=3))
+ m2: ((1|(*2|3)) & (2|3))
m3: ((*1|*(*2|3)) & (2|3))
m4: ((2|3) & (*2|3))
m5: ((*2|3) & (2|3))
diff --git a/cue/testdata/choosedefault/002_associativity_of_defaults.txtar b/cue/testdata/choosedefault/002_associativity_of_defaults.txtar
index c452972..b27b9e7 100644
--- a/cue/testdata/choosedefault/002_associativity_of_defaults.txtar
+++ b/cue/testdata/choosedefault/002_associativity_of_defaults.txtar
@@ -41,11 +41,11 @@
(struct){
a: (string){ |(*(string){ "a" }, (string){ "b" }, (string){ "c" }) }
b: (string){ |(*(string){ "a" }, (string){ "b" }, (string){ "c" }) }
- c: (string){ |(*(string){ "a" }, *(string){ "b" }, (string){ "c" }) }
+ c: (string){ |(*(string){ "a" }, (string){ "b" }, (string){ "c" }) }
x: (string){ |(*(string){ "a" }, (string){ "b" }, (string){ "c" }) }
y: (string){ |(*(string){ "a" }, (string){ "b" }, (string){ "c" }) }
- s1: (int){ |(*(int){ 1 }, *(int){ 2 }, (int){ 3 }) }
- s2: (int){ |(*(int){ 1 }, *(int){ 2 }, (int){ 3 }) }
+ s1: (int){ |(*(int){ 1 }, (int){ 2 }, (int){ 3 }) }
+ s2: (int){ |(*(int){ 1 }, (int){ 2 }, (int){ 3 }) }
s3: (int){ |(*(int){ 1 }, (int){ 3 }) }
s4: (int){ |(*(int){ 1 }, (int){ 2 }) }
s5: (int){ |(*(int){ 1 }, *(int){ 2 }, (int){ 3 }) }
diff --git a/cue/testdata/disjunctions/defembed.txtar b/cue/testdata/disjunctions/defembed.txtar
index 5dcaf0d..e3caa11 100644
--- a/cue/testdata/disjunctions/defembed.txtar
+++ b/cue/testdata/disjunctions/defembed.txtar
@@ -4,8 +4,8 @@
-- in.cue --
x: {
// All of these resolve to *2 | 3
- m1: (*1 | (*2 | 3)) & (>=2 & <=3)
- m2: (*1 | (*2 | 3)) & (2 | 3)
+ m1: (1 | (*2 | 3)) & (>=2 & <=3)
+ m2: (1 | (*2 | 3)) & (2 | 3)
m3: (*1 | *(*2 | 3)) & (2 | 3)
}
y1: x & {
@@ -66,8 +66,8 @@
--- in.cue
{
x: {
- m1: ((*1|(*2|3)) & (>=2 & <=3))
- m2: ((*1|(*2|3)) & (2|3))
+ m1: ((1|(*2|3)) & (>=2 & <=3))
+ m2: ((1|(*2|3)) & (2|3))
m3: ((*1|*(*2|3)) & (2|3))
}
y1: (〈0;x〉 & {
diff --git a/doc/ref/spec.md b/doc/ref/spec.md
index 4419d03..395730b 100644
--- a/doc/ref/spec.md
+++ b/doc/ref/spec.md
@@ -697,69 +697,79 @@
#### Default values
-Any element of a disjunction can be marked as a default
-by prefixing it with an asterisk `*`.
+Any value `v` _may_ be associated with a default value `d`,
+where `d` must be in instance of `v` (`d ⊑ v`).
+
+Default values are introduced by means of disjunctions.
+Any element of a disjunction can be _marked_ as a default
+by prefixing it with an asterisk `*` ([a unary expression](#Operators)).
+Syntactically consecutive disjunctions are considered to be
+part of a single disjunction,
+whereby multiple disjuncts can be marked as default.
+A _marked disjunction_ is one where any of its terms are marked.
+So `a | b | *c | d` is a single marked disjunction of four terms,
+whereas `a | (b | *c | d)` is an unmarked disjunction of two terms,
+one of which is a marked disjunction of three terms.
+As explained below, distinguishing the nesting of disjunctions like this
+is only relevant when both an outer and nested disjunction are marked.
+
Intuitively, when an expression needs to be resolved for an operation other
-than unification or disjunctions,
+than unification or disjunction,
non-starred elements are dropped in favor of starred ones if the starred ones
do not resolve to bottom.
-More precisely, any value `v` may be associated with a default value `d`,
-denoted `(v, d)` (not CUE syntax),
-where `d` must be in instance of `v` (`d ⊑ v`).
-The rules for unifying and disjoining such values are as follows:
+To define the the unification and disjunction operation we use the notation
+`⟨v⟩` to denote a CUE value `v` that is not associated with a default
+and the notation `⟨v, d⟩` to denote a value `v` associated with a default
+value `d`.
+The rewrite rules for unifying such values are as follows:
```
-U1: (v1, d1) & v2 => (v1&v2, d1&v2)
-U2: (v1, d1) & (v2, d2) => (v1&v2, d1&d2)
-
-D1: (v1, d1) | v2 => (v1|v2, d1)
-D2: (v1, d1) | (v2, d2) => (v1|v2, d1|d2)
+U0: ⟨v1⟩ & ⟨v2⟩ => ⟨v1&v2⟩
+U1: ⟨v1, d1⟩ & ⟨v2⟩ => ⟨v1&v2, d1&v2⟩
+U2: ⟨v1, d1⟩ & ⟨v2, d2⟩ => ⟨v1&v2, d1&d2⟩
```
-Default values may be introduced within disjunctions
-by _marking_ terms of a disjunction with an asterisk `*`
-([a unary expression](#Operators)).
-The default value of a disjunction with marked terms is the disjunction
-of those marked terms, applying the following rules for marks:
-
+The rewrite rules for disjoining terms of unmarked disjunctions are
```
-M1: *v => (v, v)
-M2: *(v1, d1) => (v1, d1)
+D0: ⟨v1⟩ | ⟨v2⟩ => ⟨v1|v2⟩
+D1: ⟨v1, d1⟩ | ⟨v2⟩ => ⟨v1|v2, d1⟩
+D2: ⟨v1, d1⟩ | ⟨v2, d2⟩ => ⟨v1|v2, d1|d2⟩
```
-In general, any operation `f` in CUE involving default values proceeds along the
-following lines
+Terms of marked disjunctions are first rewritten according to the following
+rules:
```
-O1: f((v1, d1), ..., (vn, dn)) => (f(v1, ..., vn), f(d1, ..., dn))
+M0: ⟨v⟩ => ⟨v⟩ don't introduce defaults for unmarked term
+M1: *⟨v⟩ => ⟨v, v⟩ introduce identical default for marked term
+M2: *⟨v, d⟩ => ⟨v, d⟩ keep existing defaults for marked term
+M3: ⟨v, d⟩ => ⟨v⟩ strip existing defaults from unmarked term
```
-where, with the exception of disjunction, a value `v` without a default
-value is promoted to `(v, v)`.
+Note that for any marked disjunction `a`,
+the expressions `a|a`, `*a|a` and `*a|*a` all resolve to `a`.
```
Expression Value-default pair Rules applied
-*"tcp" | "udp" ("tcp"|"udp", "tcp") M1, D1
-string | *"foo" (string, "foo") M1, D1
+*"tcp" | "udp" ⟨"tcp"|"udp", "tcp"⟩ M1, D1
+string | *"foo" ⟨string, "foo"⟩ M1, D1
-*1 | 2 | 3 (1|2|3, 1) M1, D1
+*1 | 2 | 3 ⟨1|2|3, 1⟩ M1, D1
-(*1|2|3) | (1|*2|3) (1|2|3, 1|2) M1, D1, D2
-(*1|2|3) | *(1|*2|3) (1|2|3, 1|2) M1, D1, M2, D2
-(*1|2|3) | (1|*2|3)&2 (1|2|3, 1|2) M1, D1, U1, D2
+(*1|2|3) | (1|*2|3) ⟨1|2|3, 1|2⟩ M1, D1, D2
+(*1|2|3) | *(1|*2|3) ⟨1|2|3, 2⟩ M1, M2, M3, D1, D2
+(*1|2|3) | (1|*2|3)&2 ⟨1|2|3, 1|2⟩ M1, D1, U1, D2
-(*1|2) & (1|*2) (1|2, _|_) M1, D1, U2
-
-(*1|2) + (1|*2) ((1|2)+(1|2), 3) M1, D1, O1
+(*1|2) & (1|*2) ⟨1|2, _|_⟩ M1, D1, U2
```
The rules of subsumption for defaults can be derived from the above definitions
and are as follows.
```
-(v2, d2) ⊑ (v1, d1) if v2 ⊑ v1 and d2 ⊑ d1
-(v1, d1) ⊑ v if v1 ⊑ v
-v ⊑ (v1, d1) if v ⊑ d1
+⟨v2, d2⟩ ⊑ ⟨v1, d1⟩ if v2 ⊑ v1 and d2 ⊑ d1
+⟨v1, d1⟩ ⊑ ⟨v⟩ if v1 ⊑ v
+⟨v⟩ ⊑ ⟨v1, d1⟩ if v ⊑ d1
```
<!--
@@ -783,13 +793,13 @@
disjunction literals be normalized).
-->
-
```
Expression Resolves to
"tcp" | "udp" "tcp" | "udp"
*"tcp" | "udp" "tcp"
float | *1 1
*string | 1.0 string
+(*1|2) + (2|*3) 4
(*1|2|3) | (1|*2|3) 1|2
(*1|2|3) & (1|*2|3) 1|2|3 // default is _|_
@@ -807,8 +817,8 @@
{a: 1} | {b: 1} {a: 1} | {b: 1}
{a: 1} | *{b: 1} {b:1}
*{a: 1} | *{b: 1} {a: 1} | {b: 1}
-({a: 1} | {b: 1}) & {a:1} {a:1} // after eliminating {a:1,b:1} by normalization
-({a:1}|*{b:1}) & ({a:1}|*{b:1}) {b:1} // after eliminating {a:1,b:1} by normalization
+({a: 1} | {b: 1}) & {a:1} {a:1} | {a: 1, b: 1}
+({a:1}|*{b:1}) & ({a:1}|*{b:1}) {b:1}
```
diff --git a/internal/core/eval/disjunct.go b/internal/core/eval/disjunct.go
index d58aa93..0afb4ea 100644
--- a/internal/core/eval/disjunct.go
+++ b/internal/core/eval/disjunct.go
@@ -284,7 +284,7 @@
subMode = combineDefault(subMode, mode)
}
}
- defMode = combineSubDefault(defMode, subMode)
+ defMode = combineDefault(defMode, subMode)
n.defaultMode = combineDefault(n.defaultMode, defMode)
}
@@ -357,43 +357,6 @@
isDefault
)
-// combineSubDefault combines default modes where b is a subexpression in
-// a disjunctions.
-//
-// Default rules from spec:
-//
-// D1: (v1, d1) | v2 => (v1|v2, d1)
-// D2: (v1, d1) | (v2, d2) => (v1|v2, d1|d2)
-//
-// Spec:
-// M1: *v => (v, v)
-// M2: *(v1, d1) => (v1, d1)
-//
-func combineSubDefault(a, b defaultMode) defaultMode {
- switch {
- case a == maybeDefault && b == maybeDefault: // D1
- return maybeDefault
- case a == maybeDefault && b == notDefault: // D1
- return notDefault
- case a == maybeDefault && b == isDefault: // D1
- return isDefault
- case a == notDefault && b == maybeDefault: // D1
- return notDefault
- case a == notDefault && b == notDefault: // D2
- return notDefault
- case a == notDefault && b == isDefault: // D2
- return isDefault
- case a == isDefault && b == maybeDefault: // D1
- return isDefault
- case a == isDefault && b == notDefault: // M2
- return notDefault
- case a == isDefault && b == isDefault: // D2
- return isDefault
- default:
- panic("unreachable")
- }
-}
-
// combineDefaults combines default modes for unifying conjuncts.
//
// Default rules from spec:
