this repo has no description
internal/core/adt: fix conjunction semantics for opened embeddings
When a conjunction is opened with `...` (e.g. `(#C1 & #C2)...`
or `#C...` where `#C: #C1 & #C2`), the conjunction operands
should still mutually constrain each other, while allowing
extra fields in the enclosing struct.
Add `ConjunctOpened` flag to `CloseInfo` to track conjunction
operands that are opened. In `hasEvidenceForOne`, use a
pre-scan to determine if a field is "known" to the
conjunction (has conjuncts from within the embedding scope).
If so, reject it when no operand accepts it. If not, the
field is external and should be allowed.
This fixes the case where `__closeAll` wraps an outer struct
containing a nested field with an opened conjunction
embedding.
Signed-off-by: Marcel van Lohuizen <mpvl@gmail.com>
Change-Id: Ic3f8b271da138017c756ca5e84d727d29b849766
Reviewed-on: https://cue.gerrithub.io/c/cue-lang/cue/+/1236311
Unity-Result: CUE porcuepine <cue.porcuepine@gmail.com>
Reviewed-by: Daniel Martí <mvdan@mvdan.cc>
TryBot-Result: CUEcueckoo <cueckoo@cuelang.org>
+162
-68
+13
internal/core/adt/closed.go
+13
internal/core/adt/closed.go
···
180
180
// This conjunct was opened by the ... postfix operator.
181
181
Opened bool
182
182
183
+
// ConjunctOpened indicates that this conjunct is an operand of a
184
+
// conjunction that was opened with ... (e.g. (#A & #B)...). The operand
185
+
// itself is NOT opened (its close group stays active for mutual constraint
186
+
// checking), but closeOuter is suppressed so that extra fields in the
187
+
// enclosing struct are still allowed.
188
+
//
189
+
// TODO: consolidate with Opened. Since (#A & {})... is equivalent to
190
+
// #A..., ConjunctOpened could replace Opened entirely: for single
191
+
// references the pre-scan in hasEvidenceForOne produces the same result
192
+
// as ignoring the resolver. This would require creating an embedding
193
+
// scope for single opened references (not just conjunctions).
194
+
ConjunctOpened bool
195
+
183
196
CycleInfo
184
197
}
185
198
+22
-4
internal/core/adt/conjunct.go
+22
-4
internal/core/adt/conjunct.go
···
97
97
// NOTE: do not unshare: a conjunction could still allow structure
98
98
// sharing, such as in the case of `ref & ref`.
99
99
if x.Op == AndOp {
100
-
n.scheduleConjunct(MakeConjunct(env, x.X, id), id)
101
-
n.scheduleConjunct(MakeConjunct(env, x.Y, id), id)
100
+
// For (A & B)..., mark operands as ConjunctOpened instead of
101
+
// Opened. This keeps each operand's close group active (for
102
+
// mutual constraint checking between A and B) while still
103
+
// suppressing closeOuter (so extra fields like d in
104
+
// __closeAll({(#C1 & #C2)..., d: int}) are allowed).
105
+
//
106
+
// In ExplicitOpen mode, injectEmbedNode is a no-op, so no
107
+
// embedding scope is created for the conjunction. We re-inject
108
+
// it here so the evidence mechanism can distinguish between
109
+
// fields from within the conjunction vs extra fields in the
110
+
// enclosing struct.
111
+
inner := id
112
+
if inner.Opened {
113
+
inner.Opened = false
114
+
inner.ConjunctOpened = true
115
+
inner.FromEmbed = true
116
+
inner = n.newReq(x, inner, defEmbedding)
117
+
}
118
+
n.scheduleConjunct(MakeConjunct(env, x.X, inner), inner)
119
+
n.scheduleConjunct(MakeConjunct(env, x.Y, inner), inner)
102
120
return
103
121
}
104
122
···
348
366
closeInfo.enclosingEmbed != 0 {
349
367
closeInfo.FromDef = false
350
368
}
351
-
if c.CloseInfo.Opened {
369
+
if c.CloseInfo.Opened || c.CloseInfo.ConjunctOpened {
352
370
n.setEmbedClosedness(arc)
353
371
}
354
372
···
373
391
// once.
374
392
switch isDef, _ := IsDef(c.Expr()); {
375
393
case isDef || arc.Label.IsDef() || closeInfo.TopDef:
376
-
if c.CloseInfo.Opened {
394
+
if c.CloseInfo.Opened || c.CloseInfo.ConjunctOpened {
377
395
// Definitions are always recursively closed, even if arc
378
396
// doesn't have ClosedRecursive set yet at this point.
379
397
n.embedClosedness = embedRecursivelyClosed
+4
-1
internal/core/adt/tasks.go
+4
-1
internal/core/adt/tasks.go
+42
-14
internal/core/adt/typocheck.go
+42
-14
internal/core/adt/typocheck.go
···
246
246
247
247
// isRecursive indicates this is recursively closed.
248
248
isRecursive bool
249
+
250
+
// conjunctOpened indicates this resolver is from an opened conjunction
251
+
// operand ((A & B)...). It must not use the parent==0 shortcut in
252
+
// hasEvidenceForOne, so that mutual constraints between conjunction
253
+
// operands are enforced.
254
+
conjunctOpened bool
249
255
}
250
256
251
257
type conjunctFlags uint8
···
345
351
}
346
352
347
353
// This can only be true when not using the @experiment(explicitopen).
348
-
closeOuter := id.FromDef && id.FromEmbed && !id.Opened
354
+
closeOuter := id.FromDef && id.FromEmbed && !id.Opened && !id.ConjunctOpened
349
355
350
356
if closeOuter && !forceIgnore {
351
357
// Walk up the parent chain of the outer structs to "activate" them.
···
415
421
dstID = next
416
422
417
423
n.reqDefIDs = append(n.reqDefIDs, refInfo{
418
-
v: v,
419
-
id: dstID,
420
-
parent: id.outerID,
421
-
ignore: ignore,
422
-
kind: defReference,
423
-
embed: id.enclosingEmbed,
424
-
isRecursive: v.ClosedRecursive,
424
+
v: v,
425
+
id: dstID,
426
+
parent: id.outerID,
427
+
ignore: ignore,
428
+
kind: defReference,
429
+
embed: id.enclosingEmbed,
430
+
isRecursive: v.ClosedRecursive,
431
+
conjunctOpened: id.ConjunctOpened,
425
432
})
426
433
}
427
434
srcID := id.defID
···
633
640
a.removed = true
634
641
}
635
642
}
643
+
636
644
// TODO(perf): somehow prevent error generation of recursive structures,
637
645
// or at least make it cheap. Right now if this field is a typo, likely
638
646
// all descendents will be regarded as typos.
···
703
711
return false
704
712
}
705
713
714
+
// For conjunctOpened resolvers with no parent: determine if the
715
+
// field has any conjuncts from within the conjunction's embedding
716
+
// scope. If not, the field is external to the conjunction and
717
+
// should be allowed (the ... opened it). If yes, the field is
718
+
// "known" to the conjunction, and the first check above already
719
+
// determined there's no direct evidence, so reject it.
720
+
if a.conjunctOpened && a.parent == 0 {
721
+
for _, c := range conjuncts {
722
+
if n.containsDefID(embedScope.id, c.embed) {
723
+
return false
724
+
}
725
+
}
726
+
return true
727
+
}
728
+
706
729
outerScope, ok := all.lookupSet(a.parent)
707
730
708
731
outer:
···
877
900
// we still need to track the group memberships for embeddings or enclosing
878
901
// structs.
879
902
removed bool
903
+
904
+
// conjunctOpened indicates this requirement is from an opened conjunction
905
+
// operand. See [refInfo.conjunctOpened].
906
+
conjunctOpened bool
880
907
}
881
908
882
909
// mergeCloseInfo merges the conjunctInfo of nw that is missing from nv into nv.
···
973
1000
}
974
1001
975
1002
a = append(a, reqSet{
976
-
id: y.id,
977
-
parent: y.parent,
978
-
once: once,
979
-
ignored: y.ignore,
980
-
embed: y.embed,
981
-
kind: y.kind,
1003
+
id: y.id,
1004
+
parent: y.parent,
1005
+
once: once,
1006
+
ignored: y.ignore,
1007
+
embed: y.embed,
1008
+
kind: y.kind,
1009
+
conjunctOpened: y.conjunctOpened,
982
1010
})
983
1011
984
1012
if y.parent != 0 && !y.ignore {
+80
-48
tools/fix/testdata/explicitopen_expr.txtar
+80
-48
tools/fix/testdata/explicitopen_expr.txtar
···
73
73
t2: v & {b: 1} @test(err, code=eval)
74
74
}
75
75
76
-
#C1: {a?: int, c: int}
77
-
#C2: {b?: int, c: int}
78
76
conjunctComplex: {
77
+
#C1: {a?: int, c: int}
78
+
#C2: {b?: int, c: int}
79
79
v: {
80
80
#C1 & #C2
81
81
d: int
82
82
}
83
-
// TODO:
84
-
// The new semantics is more permissive here:
85
-
// t1: v & {a: 1} @test(err, code=eval)
86
-
// t2: v & {b: 1} @test(err, code=eval)
83
+
t1: v & {a: 1} @test(err, code=eval)
84
+
t2: v & {b: 1} @test(err, code=eval)
85
+
t3: v & {c: 1} @test(eq, { c: 1, d: int })
86
+
t4: v & {d: 1} @test(eq, { d: 1, c: int })
87
+
t5: v & {e: 1} @test(err, code=eval)
87
88
88
-
t3: v & {c: 1} @test(eq, {
89
-
c: 1
89
+
#C: #C1 & #C2
90
+
vb: {
91
+
#C
90
92
d: int
91
-
a?: _|_
92
-
b?: _|_
93
-
})
94
-
t4: v & {d: 1} @test(eq, {
95
-
d: 1
96
-
a?: _|_
97
-
c: int
98
-
b?: _|_
99
-
})
100
-
t5: v & {e: 1} @test(err, code=eval)
93
+
}
94
+
tb1: vb & {a: 1} @test(err, code=eval)
95
+
tb2: vb & {b: 1} @test(err, code=eval)
96
+
tb3: vb & {c: 1} @test(eq, { c: 1, d: int })
97
+
tb5: vb & {e: 1} @test(err, code=eval)
101
98
}
102
99
103
100
···
182
179
[eval] conjunct.t2.b: field not allowed:
183
180
./in.cue:59:11
184
181
[eval] conjunctComplex.v.a: field not allowed:
185
-
./in.cue:62:7
182
+
./in.cue:63:8
186
183
[eval] conjunctComplex.v.b: field not allowed:
187
-
./in.cue:63:7
184
+
./in.cue:64:8
185
+
[eval] conjunctComplex.t1.a: field not allowed:
186
+
./in.cue:63:8
187
+
./in.cue:69:11
188
+
[eval] conjunctComplex.t1.b: field not allowed:
189
+
./in.cue:64:8
190
+
[eval] conjunctComplex.t2.b: field not allowed:
191
+
./in.cue:64:8
192
+
./in.cue:70:11
193
+
[eval] conjunctComplex.t2.a: field not allowed:
194
+
./in.cue:63:8
188
195
[eval] conjunctComplex.t3.a: field not allowed:
189
-
./in.cue:62:7
196
+
./in.cue:63:8
190
197
[eval] conjunctComplex.t3.b: field not allowed:
191
-
./in.cue:63:7
198
+
./in.cue:64:8
192
199
[eval] conjunctComplex.t4.a: field not allowed:
193
-
./in.cue:62:7
200
+
./in.cue:63:8
194
201
[eval] conjunctComplex.t4.b: field not allowed:
195
-
./in.cue:63:7
202
+
./in.cue:64:8
196
203
[eval] conjunctComplex.t5.e: field not allowed:
197
-
./in.cue:86:11
204
+
./in.cue:73:11
198
205
[eval] conjunctComplex.t5.a: field not allowed:
199
-
./in.cue:62:7
206
+
./in.cue:63:8
200
207
[eval] conjunctComplex.t5.b: field not allowed:
201
-
./in.cue:63:7
208
+
./in.cue:64:8
209
+
[eval] conjunctComplex.#C.a: field not allowed:
210
+
./in.cue:63:8
211
+
[eval] conjunctComplex.#C.b: field not allowed:
212
+
./in.cue:64:8
213
+
[eval] conjunctComplex.vb.a: field not allowed:
214
+
./in.cue:63:8
215
+
[eval] conjunctComplex.vb.b: field not allowed:
216
+
./in.cue:64:8
217
+
[eval] conjunctComplex.tb1.a: field not allowed:
218
+
./in.cue:63:8
219
+
./in.cue:80:13
220
+
[eval] conjunctComplex.tb1.b: field not allowed:
221
+
./in.cue:64:8
222
+
[eval] conjunctComplex.tb2.b: field not allowed:
223
+
./in.cue:64:8
224
+
./in.cue:81:13
225
+
[eval] conjunctComplex.tb2.a: field not allowed:
226
+
./in.cue:63:8
227
+
[eval] conjunctComplex.tb3.a: field not allowed:
228
+
./in.cue:63:8
229
+
[eval] conjunctComplex.tb3.b: field not allowed:
230
+
./in.cue:64:8
231
+
[eval] conjunctComplex.tb5.e: field not allowed:
232
+
./in.cue:83:13
233
+
[eval] conjunctComplex.tb5.a: field not allowed:
234
+
./in.cue:63:8
235
+
[eval] conjunctComplex.tb5.b: field not allowed:
236
+
./in.cue:64:8
202
237
[eval] embeddedCloseField.t3.c: field not allowed:
203
-
./in.cue:115:11
238
+
./in.cue:112:11
204
239
[eval] andField.v.c: field not allowed:
205
-
./in.cue:138:15
240
+
./in.cue:135:15
206
241
[eval] andField.t1.c: field not allowed:
207
-
./in.cue:138:15
242
+
./in.cue:135:15
208
243
[eval] andField.t2.c: field not allowed:
209
-
./in.cue:138:15
244
+
./in.cue:135:15
210
245
-- out/fixmod --
211
246
--- cue.mod/module.cue
212
247
module: "builtins.test"
···
271
306
t2: v & {b: 1} @test(err, code=eval)
272
307
}
273
308
274
-
#C1: {a?: int, c: int}
275
-
#C2: {b?: int, c: int}
276
309
conjunctComplex: {
310
+
#C1: {a?: int, c: int}
311
+
#C2: {b?: int, c: int}
277
312
v: __closeAll({
278
313
(#C1 & #C2)...
279
314
d: int
280
315
})
281
-
// TODO:
282
-
// The new semantics is more permissive here:
283
-
// t1: v & {a: 1} @test(err, code=eval)
284
-
// t2: v & {b: 1} @test(err, code=eval)
316
+
t1: v & {a: 1} @test(err, code=eval)
317
+
t2: v & {b: 1} @test(err, code=eval)
318
+
t3: v & {c: 1} @test(eq, { c: 1, d: int })
319
+
t4: v & {d: 1} @test(eq, { d: 1, c: int })
320
+
t5: v & {e: 1} @test(err, code=eval)
285
321
286
-
t3: v & {c: 1} @test(eq, {
287
-
c: 1
322
+
#C: #C1 & #C2
323
+
vb: __closeAll({
324
+
#C...
288
325
d: int
289
-
a?: _|_
290
-
b?: _|_
291
326
})
292
-
t4: v & {d: 1} @test(eq, {
293
-
d: 1
294
-
a?: _|_
295
-
c: int
296
-
b?: _|_
297
-
})
298
-
t5: v & {e: 1} @test(err, code=eval)
327
+
tb1: vb & {a: 1} @test(err, code=eval)
328
+
tb2: vb & {b: 1} @test(err, code=eval)
329
+
tb3: vb & {c: 1} @test(eq, { c: 1, d: int })
330
+
tb5: vb & {e: 1} @test(err, code=eval)
299
331
}
300
332
301
333
// Disjunct → single embed, simplified.