diff --git a/dag/std/types.dag b/dag/std/types.dag index 4049749310d..5a3939b4689 100644 --- a/dag/std/types.dag +++ b/dag/std/types.dag @@ -104,6 +104,24 @@ type Bytes type Char = Int where unicode_scalar, brand("Char") type List = FreeMonoid +// ONE SPELLING, TWO CARRIERS -- the open half of the collection-realization fork, stated where the +// fusion is authored rather than where it surfaces. `Set` names a predicate here and a finite +// enumeration at every realization: `extdeps.languages.rust.types` gives `PointwisePower` the +// inhabitant `BTreeSet<{0}>`, so a declaration position lowers to `im::OrdSet` while a record +// literal `Set { member: .. }` lowers to the algebra struct, and the two meet as a rustc refusal +// wherever one compiled closure holds both. Measured at +// `docs/probes/t3_collection_realization_2026-08-22.md`. +// +// The PREDICATE half is closed: every corpus site that constructs by characteristic function or +// reads `.member` now names `std.algebra` `PointwisePower` directly, so no `Set { member: .. }` +// literal survives in `src/v2`. What is NOT closed is this alias -- `Set` still resolves to the +// predicate carrier, so the literal is still writable and nothing refuses a new one. Making it +// unwritable is a retarget of this row onto the finite carrier, and it is deliberately not taken +// here: it is a `std` authority change whose only verification is a whole-corpus compile, and the +// Map half of the same fork (`Map { lookup: .. }`, 145 literals) is untouched and would have to +// move with it. NEXT-RUNG TRIGGER: the Map-side decomposition landing, after which both rows +// retarget in one motion. Until then the class sits at MITIGATABLE (DESIGN 4b) -- the invalid +// state is writable and only review sees it. type Set = PointwisePower type Map = PartialFunction diff --git a/docs/probes/set_carrier_decomposition_2026-08-23.md b/docs/probes/set_carrier_decomposition_2026-08-23.md new file mode 100644 index 00000000000..2ee3c434346 --- /dev/null +++ b/docs/probes/set_carrier_decomposition_2026-08-23.md @@ -0,0 +1,143 @@ +# The predicate half of the Set/Map carrier fork, decomposed (2026-08-23) + +**Work item:** `node://adhoc-66adece2-31f`. **Session:** `silent-gull-867`. +Measurement this rests on and does not restate: +[`t3_collection_realization_2026-08-22.md`](t3_collection_realization_2026-08-22.md) (the E0308 half) +and [`board_2026-08-23/README.md`](board_2026-08-23/README.md) (the retained log this brief's 27 +blocks were partitioned from). + +## The 27 blocks, at `.dag` grain + +Subject `src/v2/compiler/03_ingest.dag`, ref `98b18cdc81e`, board `CARGO_ERROR_TOTAL=330`. The brief +names 27 blocks in two shapes; both are the same fork read from two positions. + +| shape | code | blocks | what rustc saw | +|---|---|---:|---| +| the algebra name leaks as a Rust type | `E0560` | 17 | `struct Rc> has no field named member` (8) · `struct Rc> has no field named lookup` (9) | +| the carrier's own field read off the realized type | `E0609` | 10 | `no field member on type Rc>` | + +Both come from `std.types` naming one spelling for two carriers. A **type** position takes the +`container_template_alias_rows` hop on to the target inhabitant row and lowers `Set` to +`im::OrdSet`; a **record-literal** position takes the `container_template_algebra` hop and stops +at the modeled algebra struct, `Rc>`. Where one compiled closure holds both, the +two meet as a refusal. + +## What this change does + +Every corpus site that **constructs by characteristic function** or **reads `.member`** now names +`std.algebra` `PointwisePower` directly, under its own authority, instead of borrowing `Set`. The +populations were read individually, not sampled: + +| | count | +|---|---:| +| `Set { member: … }` literals in `src/v2` before | 37 | +| — of them, characteristic functions | 37 | +| — of them, finite enumerations mis-spelled | 0 | +| `Set { … }` literals in `src/v2` after | 0 | +| `.member(` call sites re-pointed | 26 | +| `Set<…>` declarations re-typed to `PointwisePower<…>` | 128 occurrences across 20 files | + +Nothing in the finite-`Set` population moved: `std.graph` `visited`, `std.authorization_profile` +`EnumeratedAudience.members`, `std.occurrence_binding_candidates`, `std.syllogism`, +`gunbc.package_delivery`, and the `dag/`-rooted emit templates keep `Set` and keep the `OrdSet` +realization, because every one of them is fed by `empty_set` / `set_insert` and read by +`set_contains` — the finite surface, never `member`. + +This closes the 18 blocks of the 27 that are Set-shaped (8 `E0560` + all 10 `E0609`). The 9 +remaining are `Map { lookup: … }`, and they are **not** closed here — see below. + +## What is deliberately left open, and why + +1. **The Map half.** `Map` needs no retarget — `PartialFunction`'s template roster already *is* the + finite map surface — but its 145 corpus literals do need re-authoring onto the construction route + `std.primitives` already declares (`empty_map_contract`, `map_insert_contract`; the second is + bound in `v2.std.collection` `map_insert_host_binding` and then not used, the function writing a + closure chain instead). 97 of those 145 are `lookup: ` delegates whose key list has to + be read out of the delegate body one at a time. That is a lane, not a rider on this one. +2. **The alias itself.** `std.types` still reads `type Set = PointwisePower`, so + `Set { member: … }` is still *writable* — nothing refuses a new one. Making it unwritable is a + retarget of that row onto the finite carrier, which is a `std` authority change whose only + verification is a whole-corpus compile, and which has to move together with the Map row. The + obligation is recorded on the declaration itself (`dag/std/types.dag`, the annotation above + `type Set`), with the next-rung trigger named there: the Map-side decomposition landing. Until + then the class sits at **mitigatable** (DESIGN §4b) and only review sees a regression. + +So the honest statement of the rung: this change removes the fork's instances on the Set side and +does not yet make the Set side's invalid state unwritable. + +## Controls + +- **The re-typed population is exactly the predicate population.** Two independent instruments + agree: a grep for `Set {` literals (37, each read) and a grep for `.member(` consumers (26, each + read). No site was found that constructs a `Set` literal and then enumerates it, and no finite- + surface call (`set_contains` / `set_insert` / `empty_set`) appears in any re-typed declaration's + module against a re-typed value. +- **The rewrite could not touch string data or prose.** The edit was applied outside double-quoted + spans and outside `//` annotation lines; the two `"Set"` string literals in + `v2.extdeps.languages.rust` (`target_collection_set_carrier` rows) are unchanged, and the two + prose blocks that cite the grounding (`v2.std.grammar`'s sync-token note and + `v2.compiler.02_parse`'s convergence-measure note) were updated by hand, not by the rewrite. +- **Not verified here:** the emitted-Rust block count. Re-measuring the board requires the probe + dispatch, and this change is landed against the `.dag` acceptance path (`gunbc compile --entry + src/v2/compiler/03_ingest.dag`) rather than against a re-run of `curated_cargo_probe_one.sh`. The + claim "18 of 27 close" is derived from the site-to-literal correspondence above, and is a + prediction about the next board, not a measurement of one. + +## Addendum — the Map lane is not the shape the scoping doc predicted (full read, 2026-08-23) + +`decomposition_scope.md` classified the 97 `lookup: ` delegates from a **sample** and +flagged that row as "the one number here that a full read could move." It moves. Read +mechanically over every delegate body in `src/v2` + `dag`: + +| classification | count | test | +|---|---:|---| +| finite — branches on the key | **6** | the delegate body contains ` ==` or `match ` | +| finite one level down | **3** | a callee receiving the key does | +| **open — no key comparison anywhere in two levels** | **78** | computes a fact from the key unconditionally | + +92 delegate names, 87 bodies resolved. The sample that produced the "if-chain over a fixed key list" +reading landed on `v2.program` `program_facts_lookup`, which is one of the 6. + +The overwhelming majority are shaped like + +``` +fn bind_facts_lookup(key: Node) -> Optional { + optional_present(value: claim_inferred_facts_from_nodes(resolved: key, ..)) +} +``` + +— a **total function of the key**, not a table. So most of the Map population is a genuine partial +function rather than a finite table, and 145 re-authorings into finite maps is the wrong lane. + +**But it is NOT the symmetric move, and an earlier revision of this addendum said it was.** That +revision read "they should name `PartialFunction` under its own authority, exactly the move this +change made on the Set side." Corrected here rather than left standing, because it is the premise a +reader would plan the Map lane against. `PointwisePower` is **one** template row (`member`), which is +why an open characteristic function inhabits it completely and the Set change is clean. +`PartialFunction` is **thirteen** (`get map_get lookup map_insert map_merge map_has map_contains_key +map_keys map_values with contains length count`) — it bundles a partial function with a finite map, +and an open delegate cannot answer `map_keys`, `map_values` or `count` at all. + +The asymmetry is visible in the model's own profile rosters, and it is the Map side that is missing a +carrier, not the Set side that has a spare: + +| concept | Set side | Map side | +|---|---|---| +| open / characteristic | `PointwisePower` — 1 template | **missing** | +| finite / enumerable | `BooleanAlgebra` collection — 13 templates | `PartialFunction` — 13 templates | + +Inhabitance measured, not argued: **0 of the 145** `Map { … }` literals in `src/v2` + `dag` supply any +field beyond `lookup`. The other twelve rows are promises the entire existing population already +fails to keep. So the Map lane's first move is a **decomposition** of `PartialFunction` — the partial +function keeps its real meaning (`lookup: fn(K) -> V?`, mirroring the single-slot +`v2.std.collection` `TotalMap { lookup: fn(K) -> V }` already in tree, so this is the totality +axis on an existing pair rather than a minted name) and the finite map takes its own name — not a +retype. That is a `std` authority change of the same class as the alias row deferred above, so it +moves in its own PR verified by whole-corpus compile, and **both** alias retargets can ride it. + +**What this does and does not establish.** The classifier is a text predicate over the body and one +level of callees, so it is a *lower bound on openness*: a delegate could still be finite through a +deeper helper. The 9 finite ones are confirmed by reading them; the 78 are "no key comparison found +within two levels", and the classification converged rather than drifted (going from one level to +two moved 3 of 81), which is evidence it is near-stable but not a proof. The remaining 5 unresolved +names are declared here rather than absorbed into either column. diff --git a/src/v2/compiler/02_parse.dag b/src/v2/compiler/02_parse.dag index f2b78590cfe..28b0aa445a4 100644 --- a/src/v2/compiler/02_parse.dag +++ b/src/v2/compiler/02_parse.dag @@ -87,7 +87,7 @@ import v2.std.provenance { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, list_at_optional, map_get, @@ -277,7 +277,7 @@ type ParseTableRealization { memo_hits: Int memo_misses: Int memo_lookup_calls: Int - nullable_set: Set + nullable_set: PointwisePower first_rows: Map> productions_by_name: Map } @@ -634,7 +634,7 @@ fn parse_table_empty() -> ParseTable { memo_hits: 0, memo_misses: 0, memo_lookup_calls: 0, - nullable_set: Set { member: fn(_) { false } }, + nullable_set: PointwisePower { member: fn(_) { false } }, first_rows: empty_map(), productions_by_name: empty_map() } @@ -1166,13 +1166,13 @@ fn parse_nonterminal_memoized_core( } } -fn set_symbol_insert(s: Set, item: Symbol) -> Set { - Set { +fn set_symbol_insert(s: PointwisePower, item: Symbol) -> PointwisePower { + PointwisePower { member: fn(sym) { sym == item || s.member(sym) } } } -fn expr_is_nullable_given_set(expr: GrammarExpr, nullable_set: Set) -> Bool { +fn expr_is_nullable_given_set(expr: GrammarExpr, nullable_set: PointwisePower) -> Bool { fold_grammar_expr( expr: expr, algebra: GrammarExprFold { @@ -1186,7 +1186,7 @@ fn expr_is_nullable_given_set(expr: GrammarExpr, nullable_set: Set) -> B ) } -fn compute_nullable_step(ns: Set, p: GrammarProduction) -> Set { +fn compute_nullable_step(ns: PointwisePower, p: GrammarProduction) -> PointwisePower { if expr_is_nullable_given_set(expr: p.expression, nullable_set: ns) { set_symbol_insert(s: ns, item: p.name) } else { @@ -1196,7 +1196,7 @@ fn compute_nullable_step(ns: Set, p: GrammarProduction) -> Set { // ONE ROUND of the nullable fixpoint: every production gets a chance to join the set given what // the set already holds. -fn compute_nullable_round(root: GrammarRoot, ns: Set) -> Set { +fn compute_nullable_round(root: GrammarRoot, ns: PointwisePower) -> PointwisePower { fold_list( xs: root.productions, empty: ns, @@ -1206,13 +1206,13 @@ fn compute_nullable_round(root: GrammarRoot, ns: Set) -> Set { ) } -// THE CONVERGENCE MEASURE. `Set` is a `PointwisePower` — a characteristic function — so two sets -// cannot be compared directly, and the fixpoint cannot stop by testing `next == previous`. It can +// THE CONVERGENCE MEASURE. The carrier is a `PointwisePower` — a characteristic function — so two +// sets cannot be compared directly, and the fixpoint cannot stop by testing `next == previous`. It can // stop on a MONOTONE MEASURE instead: `compute_nullable_step` only ever inserts, so the number of // productions the set admits rises until the round adds nothing, and equal counts across a round // mean equal sets. Counting over `root.productions` is exact here because that is the only // population `compute_nullable_step` can insert from. -fn nullable_member_count(root: GrammarRoot, ns: Set) -> Int { +fn nullable_member_count(root: GrammarRoot, ns: PointwisePower) -> Int { fold_list( xs: root.productions, empty: 0, @@ -1232,10 +1232,10 @@ fn nullable_member_count(root: GrammarRoot, ns: Set) -> Int { // a round adds nothing, so the RESULT is identical and only the redundant rounds are gone. fn compute_nullable_fixpoint( root: GrammarRoot, - ns: Set, + ns: PointwisePower, seen_count: Int, fuel: Int -) -> Set { +) -> PointwisePower { if fuel == 0 { ns } else { @@ -1249,10 +1249,10 @@ fn compute_nullable_fixpoint( } } -fn compute_nullable_set(root: GrammarRoot) -> Set { +fn compute_nullable_set(root: GrammarRoot) -> PointwisePower { compute_nullable_fixpoint( root: root, - ns: Set { member: fn(_) { false } }, + ns: PointwisePower { member: fn(_) { false } }, seen_count: 0, fuel: length(xs: root.productions) ) @@ -1264,7 +1264,7 @@ type GrammarExprFirstFold { } type GrammarFirstAnalysis { - nullable_set: Set + nullable_set: PointwisePower first_rows: Map> } @@ -1314,7 +1314,7 @@ fn expr_first_fold_terminal(token_class: Symbol) -> GrammarExprFirstFold { fn expr_first_fold_nonterminal( name: Symbol, - nullable_set: Set, + nullable_set: PointwisePower, first_rows: Map> ) -> GrammarExprFirstFold { GrammarExprFirstFold { @@ -1350,7 +1350,7 @@ fn expr_first_fold_repeat(element: GrammarExprFirstFold) -> GrammarExprFirstFold fn expr_first_fold( expr: GrammarExpr, - nullable_set: Set, + nullable_set: PointwisePower, first_rows: Map> ) -> GrammarExprFirstFold { fold_grammar_expr( @@ -1371,7 +1371,7 @@ fn expr_first_fold( fn compute_production_first_row_terminals( rows: Map>, p: GrammarProduction, - nullable_set: Set + nullable_set: PointwisePower ) -> List { expr_first_fold( expr: p.expression, @@ -1382,7 +1382,7 @@ fn compute_production_first_row_terminals( fn compute_production_first_rows_round( root: GrammarRoot, - nullable_set: Set, + nullable_set: PointwisePower, rows: Map> ) -> Map> { fold_list( @@ -1419,7 +1419,7 @@ fn production_first_rows_total(root: GrammarRoot, rows: Map fn compute_production_first_rows_fixpoint( root: GrammarRoot, - nullable_set: Set, + nullable_set: PointwisePower, rows: Map>, seen_total: Int, fuel: Int @@ -1445,7 +1445,7 @@ fn compute_production_first_rows_fixpoint( fn compute_production_first_rows( root: GrammarRoot, - nullable_set: Set + nullable_set: PointwisePower ) -> Map> { compute_production_first_rows_fixpoint( root: root, @@ -1489,7 +1489,7 @@ fn append_choice_ambiguity_row( fn collect_choice_ambiguities_in_expr( expr: GrammarExpr, production: Symbol, - nullable_set: Set, + nullable_set: PointwisePower, first_rows: Map>, acc: List ) -> List { @@ -1554,7 +1554,7 @@ fn collect_choice_ambiguities_in_expr( fn compute_grammar_first_analysis_given( root: GrammarRoot, - nullable_set: Set + nullable_set: PointwisePower ) -> GrammarFirstAnalysis { GrammarFirstAnalysis { nullable_set: nullable_set, @@ -1656,7 +1656,7 @@ fn expr_corner_fold_terminal(_: Symbol) -> GrammarExprCornerFold { GrammarExprCornerFold { corners: std.algebra.Empty, nullable: false } } -fn expr_corner_fold_nonterminal(name: Symbol, nullable_set: Set) -> GrammarExprCornerFold { +fn expr_corner_fold_nonterminal(name: Symbol, nullable_set: PointwisePower) -> GrammarExprCornerFold { GrammarExprCornerFold { corners: Cons { head: name, tail: std.algebra.Empty }, nullable: nullable_set.member(name) @@ -1699,7 +1699,7 @@ fn expr_corner_fold_repeat(element_fold: GrammarExprCornerFold) -> GrammarExprCo GrammarExprCornerFold { corners: element_fold.corners, nullable: true } } -fn expr_corner_nullable_fold(expr: GrammarExpr, nullable_set: Set) -> GrammarExprCornerFold { +fn expr_corner_nullable_fold(expr: GrammarExpr, nullable_set: PointwisePower) -> GrammarExprCornerFold { fold_grammar_expr( expr: expr, algebra: GrammarExprFold { @@ -1713,7 +1713,7 @@ fn expr_corner_nullable_fold(expr: GrammarExpr, nullable_set: Set) -> Gr ) } -fn expr_direct_left_corner_list(expr: GrammarExpr, nullable_set: Set) -> List { +fn expr_direct_left_corner_list(expr: GrammarExpr, nullable_set: PointwisePower) -> List { expr_corner_nullable_fold(expr: expr, nullable_set: nullable_set).corners } @@ -1744,7 +1744,7 @@ fn left_corner_list_union(left: List, right: List) -> List) -> Map> { +fn left_corner_direct_rows(root: GrammarRoot, nullable_set: PointwisePower) -> Map> { fold_list( xs: root.productions, empty: empty_map(), @@ -1825,7 +1825,7 @@ fn left_corner_fixpoint( } } -fn left_corner_rows(root: GrammarRoot, nullable_set: Set) -> Map> { +fn left_corner_rows(root: GrammarRoot, nullable_set: PointwisePower) -> Map> { let seeded = left_corner_direct_rows(root: root, nullable_set: nullable_set) left_corner_fixpoint( root: root, @@ -1838,7 +1838,7 @@ fn left_corner_rows(root: GrammarRoot, nullable_set: Set) -> Map) -> Bool { +fn grammar_has_left_recursion_given(root: GrammarRoot, nullable_set: PointwisePower) -> Bool { let rows = left_corner_rows(root: root, nullable_set: nullable_set) any( xs: root.productions, diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index 5c162468d25..9ab1d59e60a 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -16,7 +16,7 @@ import std.algebra { Cons, Empty, FreeMonoid } import v2.std.algebra { length, list_snoc_item } import v2.std.collection { Map, - Set, + PointwisePower, empty_map, map_get, map_insert @@ -87,7 +87,7 @@ type ResolvedTree = Node type Namespace { bindings: Map - canonical_symbols: Set + canonical_symbols: PointwisePower symbol_index: SymbolIndex module_qn: QualifiedName } @@ -128,8 +128,8 @@ fn empty_namespace() -> Namespace { } } -fn empty_canonical_symbol_set() -> Set { - Set { +fn empty_canonical_symbol_set() -> PointwisePower { + PointwisePower { member: fn(_) { false } diff --git a/src/v2/extdeps/languages/cpp.dag b/src/v2/extdeps/languages/cpp.dag index 96cef0f9310..063147f0a58 100644 --- a/src/v2/extdeps/languages/cpp.dag +++ b/src/v2/extdeps/languages/cpp.dag @@ -39,7 +39,7 @@ import v2.std.compilers.target_model { TargetModel, target_model_emit_transforms import v2.std.logic { Bool, bool_boolean_algebra } import std.algebra { Empty } import v2.std.algebra { BooleanAlgebra, boolean_algebra_node, commutative_semiring_node, fold_list, list_append, list_snoc_item, ordered_ring_node } -import v2.std.collection { Absent, List, Map, Present, Set, empty_map, map_insert } +import v2.std.collection { Absent, List, Map, PointwisePower, Present, empty_map, map_insert } import v2.std.model_core { AlgebraInhabitanceDecl, EffectSemanticsDecl, @@ -584,8 +584,8 @@ fn cpp_catalog_surface_symbol(sym: Symbol, target_profile: Node) -> Bool { cpp_bool_catalog_surface_symbol(sym: sym) } -fn cpp_language_model_canonical_symbols(target_profile: Node) -> Set { - Set { +fn cpp_language_model_canonical_symbols(target_profile: Node) -> PointwisePower { + PointwisePower { member: fn(sym) { cpp_catalog_surface_symbol(sym: sym, target_profile: target_profile) } diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index f8f603e05bd..76e6cef94fb 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -5,7 +5,7 @@ import v2.std.language_model { LanguageModel } import v2.std.host_transport { target_emit_host_runtime_row_unconfigured, TargetEmitHostRuntimeRow } import v2.std.collection { List, - Set, + PointwisePower, Map, empty_map, list_at_optional, @@ -3371,8 +3371,8 @@ fn dag_grammar() -> ParseGrammar { ModeledGrammar { root: dag_grammar_root() } } -fn dag_language_model_surface_prelude_atoms() -> Set { - Set { +fn dag_language_model_surface_prelude_atoms() -> PointwisePower { + PointwisePower { member: fn(sym) { sym == ^dag_c3_surface_sugar_service || sym == ^dag_c3_surface_sugar_fn || @@ -3383,8 +3383,8 @@ fn dag_language_model_surface_prelude_atoms() -> Set { } } -fn dag_language_model_empty_canonical_symbol_set() -> Set { - Set { +fn dag_language_model_empty_canonical_symbol_set() -> PointwisePower { + PointwisePower { member: fn(_) { false } @@ -3406,8 +3406,8 @@ fn dag_language_model_binding_canonical(sym: Symbol) -> Bool { || sym == ^dag_loop_measure_sym } -fn dag_canonical_symbols() -> Set { - Set { +fn dag_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { dag_language_model_surface_prelude_atoms().member(sym) || grammar_carries_symbol(grammar: dag_grammar(), sym: sym) || @@ -3446,7 +3446,7 @@ fn dag_language_model_surface_empty_prelude() -> LanguageModel { } } -fn dag_language_model_canonical_symbols(lm: LanguageModel) -> Set { +fn dag_language_model_canonical_symbols(lm: LanguageModel) -> PointwisePower { lm.canonical_symbols } diff --git a/src/v2/extdeps/languages/ecmascript.dag b/src/v2/extdeps/languages/ecmascript.dag index 02e00e624c1..59710250f57 100644 --- a/src/v2/extdeps/languages/ecmascript.dag +++ b/src/v2/extdeps/languages/ecmascript.dag @@ -57,7 +57,7 @@ import v2.std.compilers.lexing { import v2.std.compilers.target_model { ProducedDeclUnwired, ConcreteSyntaxToken, FixedToken, BoundToken, concrete_syntax_token_class, concrete_syntax_token_to_node } import v2.std.compilers.target_model { TargetModel, target_model_emit_transforms_empty } -import v2.std.collection { List, Map, Set, empty_map, map_insert } +import v2.std.collection { List, Map, PointwisePower, empty_map, map_insert } import v2.std.model_core { AlgebraInhabitanceDecl, EffectSemanticsDecl, @@ -1315,8 +1315,8 @@ fn ecmascript_catalog_surface_symbol(sym: Symbol) -> Bool { ecmascript_singleton_catalog_surface_symbol(sym: sym) } -fn ecmascript_language_model_canonical_symbols() -> Set { - Set { +fn ecmascript_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { ecmascript_catalog_surface_symbol(sym: sym) || ecmascript_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/go.dag b/src/v2/extdeps/languages/go.dag index 660a5020c80..b5c9abb5c25 100644 --- a/src/v2/extdeps/languages/go.dag +++ b/src/v2/extdeps/languages/go.dag @@ -41,7 +41,7 @@ import v2.std.compilers.lexing { TriviaRule, lex_rule_set_token_class_member } -import v2.std.collection { Absent, List, Map, Present, Set, empty_map, map_insert, optional_absent } +import v2.std.collection { Absent, List, Map, PointwisePower, Present, empty_map, map_insert, optional_absent } import v2.std.model_core { AlgebraInhabitanceDecl, EffectSemanticsDecl, @@ -2137,8 +2137,8 @@ fn go_catalog_surface_symbol(sym: Symbol) -> Bool { go_string_catalog_surface_symbol(sym: sym) } -fn go_language_model_canonical_symbols() -> Set { - Set { +fn go_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { go_catalog_surface_symbol(sym: sym) || go_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/java.dag b/src/v2/extdeps/languages/java.dag index 855d820d050..5a33a634d3b 100644 --- a/src/v2/extdeps/languages/java.dag +++ b/src/v2/extdeps/languages/java.dag @@ -46,7 +46,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -1490,8 +1490,8 @@ fn java_grammar() -> ParseGrammar { ModeledGrammar { root: java_grammar_root() } } -fn java_canonical_symbols() -> Set { - Set { +fn java_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { java_catalog_surface_symbol(sym: sym) || sym == ^java_surface_spelling_void || @@ -1588,8 +1588,8 @@ fn java_method_add_lex_token_symbol(sym: Symbol) -> Bool { sym == ^java_token_semicolon } -fn java_language_model_canonical_symbols() -> Set { - Set { +fn java_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { java_catalog_surface_symbol(sym: sym) || sym == ^java_surface_spelling_void || diff --git a/src/v2/extdeps/languages/kotlin.dag b/src/v2/extdeps/languages/kotlin.dag index cfa1a45cec9..9e1062c2979 100644 --- a/src/v2/extdeps/languages/kotlin.dag +++ b/src/v2/extdeps/languages/kotlin.dag @@ -55,7 +55,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -2530,8 +2530,8 @@ fn kotlin_lex_token_symbol(sym: Symbol) -> Bool { ) } -fn kotlin_language_model_canonical_symbols() -> Set { - Set { +fn kotlin_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { kotlin_catalog_surface_symbol(sym: sym) || kotlin_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 1955dcd139f..77d6423f950 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -35,7 +35,7 @@ import v2.std.compilers.lexing { TokenRule, lex_rule_set_token_class_member } -import v2.std.collection { Absent, List, Map, Optional, Present, Set } +import v2.std.collection { Absent, List, Map, Optional, PointwisePower, Present } import v2.std.logic { Bool, bool_boolean_algebra } import extdeps.languages.lean.overflow { lean_upstream_fixed_width_overflow_returns_rule } import std.algebra { Cons, Empty } @@ -872,8 +872,8 @@ fn lean_ingest_grammar_probe() -> GrammarSchemaProbeBinding { data lean_ingest_grammar_probe_authority: GrammarSchemaProbeBinding = lean_ingest_grammar_probe() -fn lean_language_model_canonical_symbols() -> Set { - Set { +fn lean_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { lean_catalog_surface_symbol(sym: sym) || lean_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/python.dag b/src/v2/extdeps/languages/python.dag index 39d278968c4..dd044a82c5a 100644 --- a/src/v2/extdeps/languages/python.dag +++ b/src/v2/extdeps/languages/python.dag @@ -54,7 +54,7 @@ import v2.std.compilers.lexing { import v2.std.compilers.target_model { ProducedDeclUnwired, ConcreteSyntaxToken, FixedToken, BoundToken, concrete_syntax_token_class, concrete_syntax_token_to_node } import v2.std.compilers.target_model { TargetModel, target_model_emit_transforms_empty } -import v2.std.collection { List, Map, Set, empty_map, map_insert } +import v2.std.collection { List, Map, PointwisePower, empty_map, map_insert } import v2.std.host_transport { EmitHostRuntimeRow, HostRuntimeRowPresent, @@ -1530,8 +1530,8 @@ fn python_catalog_surface_symbol(sym: Symbol) -> Bool { python_singleton_catalog_surface_symbol(sym: sym) } -fn python_language_model_canonical_symbols() -> Set { - Set { +fn python_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { python_catalog_surface_symbol(sym: sym) || python_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index 7c3249de27e..c5356d38c3f 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -88,7 +88,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, list_at_optional, map_insert, @@ -1765,15 +1765,15 @@ fn rust_hash_set_supplemental_generic_bound_contracts() -> Map + requirements: PointwisePower authority: ExternalAuthority coverage: RustSupplementalGenericBoundContractCoverageDisposition } fn rust_hash_set_eq_hash_supplemental_generic_bound_requirements( representation_parameter: Symbol -) -> Set { - Set { +) -> PointwisePower { + PointwisePower { member: fn(requirement) { fold_list( xs: [ @@ -3078,8 +3078,8 @@ fn rust_fn_add_lex_token_symbol(sym: Symbol) -> Bool { lex_rule_set_token_class_member(rules: rust_fn_add_lex_rules(), token_class: sym) } -fn rust_language_model_canonical_symbols() -> Set { - Set { +fn rust_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { rust_catalog_surface_symbol(sym: sym) || rust_fn_add_lex_token_symbol(sym: sym) || @@ -4365,8 +4365,8 @@ fn rust_grammar() -> ParseGrammar { ModeledGrammar { root: rust_grammar_root() } } -fn rust_canonical_symbols() -> Set { - Set { +fn rust_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { rust_catalog_surface_symbol(sym: sym) || lex_rule_set_token_class_member(rules: rust_lex_rules(), token_class: sym) || diff --git a/src/v2/extdeps/languages/swift.dag b/src/v2/extdeps/languages/swift.dag index 23e2afe780d..5af6f790f0b 100644 --- a/src/v2/extdeps/languages/swift.dag +++ b/src/v2/extdeps/languages/swift.dag @@ -56,7 +56,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -1817,8 +1817,8 @@ fn swift_catalog_surface_symbol(sym: Symbol) -> Bool { swift_nonnumeric_catalog_surface_symbol(sym: sym) } -fn swift_language_model_canonical_symbols() -> Set { - Set { +fn swift_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { swift_catalog_surface_symbol(sym: sym) || swift_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/typescript.dag b/src/v2/extdeps/languages/typescript.dag index fda08b6041c..5f3e3c17f57 100644 --- a/src/v2/extdeps/languages/typescript.dag +++ b/src/v2/extdeps/languages/typescript.dag @@ -54,7 +54,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -2146,8 +2146,8 @@ fn ts_catalog_surface_symbol(sym: Symbol) -> Bool { ) } -fn ts_language_model_canonical_symbols() -> Set { - Set { +fn ts_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { ts_catalog_surface_symbol(sym: sym) || ts_fn_add_lex_token_symbol(sym: sym) || @@ -3099,8 +3099,8 @@ fn ts_grammar() -> ParseGrammar { ModeledGrammar { root: ts_grammar_root() } } -fn ts_grammar_canonical_symbols() -> Set { - Set { +fn ts_grammar_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { ts_catalog_surface_symbol(sym: sym) || ts_lex_token_symbol(sym: sym) || @@ -3645,8 +3645,8 @@ fn ts_model_core() -> ModelCore { } } -fn ts_canonical_symbols() -> Set { - Set { +fn ts_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { ts_grammar_canonical_symbols().member(sym: sym) || sym == ^ts_surface_spelling_string diff --git a/src/v2/extdeps/languages/wasm.dag b/src/v2/extdeps/languages/wasm.dag index b749c8471a0..0d35daa1239 100644 --- a/src/v2/extdeps/languages/wasm.dag +++ b/src/v2/extdeps/languages/wasm.dag @@ -52,7 +52,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -1552,8 +1552,8 @@ fn wasm_catalog_surface_symbol(sym: Symbol) -> Bool { wasm_float_catalog_surface_symbol(sym: sym) } -fn wasm_language_model_canonical_symbols() -> Set { - Set { +fn wasm_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { wasm_catalog_surface_symbol(sym: sym) || wasm_lex_token_symbol(sym: sym) || diff --git a/src/v2/lens/subsumption.dag b/src/v2/lens/subsumption.dag index a15a327e3b2..2a02e0d1419 100644 --- a/src/v2/lens/subsumption.dag +++ b/src/v2/lens/subsumption.dag @@ -18,12 +18,12 @@ type SubsumptionVerification type DissolutionSubsumption { root_fix: DiffId - subsumed_fixes: Set + subsumed_fixes: PointwisePower verification: SubsumptionVerification } -fn affected_set_irt1_subsumed_fixes_value() -> Set { - Set { +fn affected_set_irt1_subsumed_fixes_value() -> PointwisePower { + PointwisePower { member: fn(d) { d.id == ^affected_set_boundary_receipt_leaf_fix || d.id == ^affected_set_dimension_receipt_leaf_fix || @@ -35,7 +35,7 @@ fn affected_set_irt1_subsumed_fixes_value() -> Set { } } -data affected_set_irt1_subsumed_fixes: Set = affected_set_irt1_subsumed_fixes_value() +data affected_set_irt1_subsumed_fixes: PointwisePower = affected_set_irt1_subsumed_fixes_value() data affected_set_irt1_subsumption: DissolutionSubsumption = { root_fix: DiffId { id: ^affected_set_irt1_frontier_root_fix }, @@ -45,8 +45,8 @@ data affected_set_irt1_subsumption: DissolutionSubsumption = { } } -fn rust_language_model_emit_subsumed_fixes_value() -> Set { - Set { +fn rust_language_model_emit_subsumed_fixes_value() -> PointwisePower { + PointwisePower { member: fn(d) { d.id == ^emit_rust_template_leaf_fix || d.id == ^emit_rust_name_dispatch_leaf_fix @@ -54,7 +54,7 @@ fn rust_language_model_emit_subsumed_fixes_value() -> Set { } } -data rust_language_model_emit_subsumed_fixes: Set = rust_language_model_emit_subsumed_fixes_value() +data rust_language_model_emit_subsumed_fixes: PointwisePower = rust_language_model_emit_subsumed_fixes_value() data rust_language_model_emit_subsumption: DissolutionSubsumption = { root_fix: DiffId { id: ^rust_language_model_emit_root_fix }, diff --git a/src/v2/std/collection.dag b/src/v2/std/collection.dag index edd6d90e62d..e7b48d72334 100644 --- a/src/v2/std/collection.dag +++ b/src/v2/std/collection.dag @@ -1,6 +1,6 @@ module v2.std.collection -import std.algebra { FreeMonoid } +import std.algebra { FreeMonoid, PointwisePower } import std.primitives { empty_map_contract, map_insert_contract, PrimitiveContract } import v2.std.algebra { fold_list, is_empty } import std.types { Set, Map } diff --git a/src/v2/std/grammar.dag b/src/v2/std/grammar.dag index f8a1fd550f4..5c372950cf8 100644 --- a/src/v2/std/grammar.dag +++ b/src/v2/std/grammar.dag @@ -4,7 +4,7 @@ import std.algebra { Cons, Empty } import v2.std.algebra { fold_list, fold_list_node, list_append, list_snoc_item, zip_eq } import v2.std.collection { List, - Set, + PointwisePower, list_nth } import v2.std.optional { @@ -73,8 +73,8 @@ type FormalProduction { } type FormalGrammar { - nonterminals: Set - terminals: Set + nonterminals: PointwisePower + terminals: PointwisePower productions: List start: FormalNonterminal } @@ -101,8 +101,8 @@ fn validate_grammar_diagnostic(reason: Symbol) -> Diagnostic { } fn formal_grammar_symbol_in_alphabet( - nonterminals: Set, - terminals: Set, + nonterminals: PointwisePower, + terminals: PointwisePower, symbol: FormalGrammarSymbol ) -> Bool { match symbol { @@ -114,8 +114,8 @@ fn formal_grammar_symbol_in_alphabet( } fn formal_production_rhs_in_alphabet( - nonterminals: Set, - terminals: Set, + nonterminals: PointwisePower, + terminals: PointwisePower, production: FormalProduction ) -> Bool { fold_list( @@ -294,9 +294,9 @@ type GrammarProduction { // A grammar's error-recovery sync tokens are finite and known at authoring time — every producer in // the corpus writes either an empty set or a literal list of keyword classes. Carrying them as // `Set` made them a POINTWISE-POWER characteristic function (`std.types` grounds -// `Set = PointwisePower`), which is the right grounding for a set in general and -// the wrong carrier for six literal keywords: a characteristic function cannot be enumerated, so -// the whole grammar value became unhashable through this one field. +// `Set = PointwisePower`), which is the right grounding for a predicate and the +// wrong carrier for six literal keywords: a characteristic function cannot be enumerated, so the +// whole grammar value became unhashable through this one field. // // That was not a theoretical loss. `prepare_grammar` is memoized cross-claim on // (declaration identity, content hash of the grammar), and the interpreter's content-hash walk @@ -304,8 +304,10 @@ type GrammarProduction { // language in the corpus and not only `.dag`. The measured consequence was a full ~12s grammar // preparation on every parse, including of an empty module. // -// The field is therefore the enumeration it always was. `Set` keeps its grounding untouched; what -// changed is that this field stopped borrowing a power-set to carry a list. +// The field is therefore the enumeration it always was; what changed is that this field stopped +// borrowing a power-set to carry a list. The sibling fields beside it went the other way: they are +// predicates and now say so, carrying `PointwisePower` and +// `PointwisePower` under their own name rather than under `Set`. type GrammarRoot { start: Symbol productions: List diff --git a/src/v2/std/language_model.dag b/src/v2/std/language_model.dag index c8d76d47a9b..494ef2ecece 100644 --- a/src/v2/std/language_model.dag +++ b/src/v2/std/language_model.dag @@ -1,6 +1,6 @@ module v2.std.language_model -import v2.std.collection { Set } +import v2.std.collection { PointwisePower } import v2.std.grammar { ParseGrammar, VoidGrammar, @@ -20,7 +20,7 @@ type LanguageModel { lex: LexRules grammar: ParseGrammar language_identity: Symbol - canonical_symbols: Set + canonical_symbols: PointwisePower core: ModelCore } @@ -31,8 +31,8 @@ fn language_model_named_edge(name: Symbol, target: Node) -> Edge { } } -fn language_model_empty_canonical_symbols() -> Set { - Set { +fn language_model_empty_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(_) { false } @@ -49,7 +49,7 @@ fn void_language_model(identity: Symbol) -> LanguageModel { } } -fn language_model_canonical_symbols_to_node(symbols: Set) -> Node { +fn language_model_canonical_symbols_to_node(symbols: PointwisePower) -> Node { grammar_empty_node() } diff --git a/src/v2/test/claim/grammar/validate_grammar_test.dag b/src/v2/test/claim/grammar/validate_grammar_test.dag index c93bbccdef6..31023863f59 100644 --- a/src/v2/test/claim/grammar/validate_grammar_test.dag +++ b/src/v2/test/claim/grammar/validate_grammar_test.dag @@ -8,12 +8,26 @@ data validate_grammar_fixture_other_nt: Symbol = ^validate_grammar_fixture_other data validate_grammar_fixture_bad_lhs: Symbol = ^validate_grammar_fixture_bad_lhs data validate_grammar_fixture_orphan_terminal: Symbol = ^validate_grammar_fixture_orphan_terminal +// The two singleton predicates every fixture below builds. Extracted for a reason beyond +// de-duplication: before this, `PointwisePower` reached this module's emitted text ONLY through a +// value-position record literal, and the import derivation in `v1.compiler.emit_rust` +// `reference_derived_use_lines` walks SIGNATURE-level type positions -- a name spelled only inside +// a body construction is never proposed as a use-line. A declared return type puts the reference +// where the derivation can see it. +fn validate_grammar_fixture_nonterminal_singleton(only: FormalNonterminal) -> PointwisePower { + PointwisePower { member: fn(n) { n == only } } +} + +fn validate_grammar_fixture_terminal_singleton(only: FormalTerminal) -> PointwisePower { + PointwisePower { member: fn(t) { t == only } } +} + fn validate_grammar_fixture_well_formed() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: Set { member: fn(n) { n == start } }, - terminals: Set { member: fn(t) { t == terminal } }, + nonterminals: validate_grammar_fixture_nonterminal_singleton(only: start), + terminals: validate_grammar_fixture_terminal_singleton(only: terminal), productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_start, @@ -30,8 +44,8 @@ fn validate_grammar_fixture_start_not_in_nonterminals() -> FormalGrammar { let other_nt = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_other_nt) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: Set { member: fn(n) { n == other_nt } }, - terminals: Set { member: fn(t) { t == terminal } }, + nonterminals: validate_grammar_fixture_nonterminal_singleton(only: other_nt), + terminals: validate_grammar_fixture_terminal_singleton(only: terminal), productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_other_nt, @@ -47,8 +61,8 @@ fn validate_grammar_fixture_lhs_not_in_nonterminals() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: Set { member: fn(n) { n == start } }, - terminals: Set { member: fn(t) { t == terminal } }, + nonterminals: validate_grammar_fixture_nonterminal_singleton(only: start), + terminals: validate_grammar_fixture_terminal_singleton(only: terminal), productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_bad_lhs, @@ -64,8 +78,8 @@ fn validate_grammar_fixture_rhs_symbol_not_in_alphabet() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: Set { member: fn(n) { n == start } }, - terminals: Set { member: fn(t) { t == terminal } }, + nonterminals: validate_grammar_fixture_nonterminal_singleton(only: start), + terminals: validate_grammar_fixture_terminal_singleton(only: terminal), productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_start, diff --git a/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag b/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag index 2337ed54e06..aae5ef9177d 100644 --- a/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag +++ b/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag @@ -25,7 +25,7 @@ import v2.lens.subsumption { import v2.std.cardinality { RankingDimension, TerminationProof } import v2.std.collection { Map, - Set + PointwisePower } import v2.std.optional { Optional, @@ -100,8 +100,8 @@ type MechanicalReverificationRun { test_claim: TestClaimId applied_root_fix: DiffId execution: MechanicalReverificationExecution - findings_before: Set - findings_after: Set + findings_before: PointwisePower + findings_after: PointwisePower } type MechanicalReverificationError @@ -216,7 +216,7 @@ fn mechanical_reverification_execution_for_run(run: TestClaimRun, observed: Set) -> OptionalDiffId { +fn missing_subsumed_fix_before(expected: PointwisePower, observed: PointwisePower) -> OptionalDiffId { let template = DiffId { id: ^emit_rust_template_leaf_fix } let name_dispatch = DiffId { id: ^emit_rust_name_dispatch_leaf_fix } if expected.member(template) && !observed.member(template) { @@ -228,7 +228,7 @@ fn missing_subsumed_fix_before(expected: Set, observed: Set) -> } } -fn surviving_subsumed_fix_after(observed: Set) -> OptionalDiffId { +fn surviving_subsumed_fix_after(observed: PointwisePower) -> OptionalDiffId { let template = DiffId { id: ^emit_rust_template_leaf_fix } let name_dispatch = DiffId { id: ^emit_rust_name_dispatch_leaf_fix } if observed.member(template) { @@ -443,8 +443,8 @@ data run_rust_language_model_emit_mechanical_reverification_claim: TestClaimRun< subject: subject_rust_language_model_emit_mechanical_reverification_claim ) -fn rust_language_model_emit_observed_before_value() -> Set { - Set { +fn rust_language_model_emit_observed_before_value() -> PointwisePower { + PointwisePower { member: fn(d) { d.id == ^emit_rust_template_leaf_fix || d.id == ^emit_rust_name_dispatch_leaf_fix @@ -452,17 +452,17 @@ fn rust_language_model_emit_observed_before_value() -> Set { } } -data rust_language_model_emit_observed_before: Set = rust_language_model_emit_observed_before_value() +data rust_language_model_emit_observed_before: PointwisePower = rust_language_model_emit_observed_before_value() -fn rust_language_model_emit_observed_after_value() -> Set { - Set { +fn rust_language_model_emit_observed_after_value() -> PointwisePower { + PointwisePower { member: fn(_) { false } } } -data rust_language_model_emit_observed_after: Set = rust_language_model_emit_observed_after_value() +data rust_language_model_emit_observed_after: PointwisePower = rust_language_model_emit_observed_after_value() data rust_language_model_emit_lens_ci_report: MechanicalReverificationRun = MechanicalReverificationRun { test_claim: TestClaimId { id: ^rust_language_model_emit_mechanical_reverification_claim }, diff --git a/src/v2/test/claim/parse/parse_table_claims_test.dag b/src/v2/test/claim/parse/parse_table_claims_test.dag index 003184cda7f..353540a2eaa 100644 --- a/src/v2/test/claim/parse/parse_table_claims_test.dag +++ b/src/v2/test/claim/parse/parse_table_claims_test.dag @@ -20,8 +20,8 @@ test fn parse_table_token_position_indices_no_extra_append_holds() -> Bool { && ((length(xs: token_position_indices(tokens: parse_table_two_tokens)) == 4) == false) } -fn nullable_set_singleton(name: Symbol) -> Set { - Set { member: fn(sym) { sym == name } } +fn nullable_set_singleton(name: Symbol) -> PointwisePower { + PointwisePower { member: fn(sym) { sym == name } } } test fn parse_table_nullable_morphism_holds() -> Bool {