diff --git a/dag/extdeps/languages/go/types.dag b/dag/extdeps/languages/go/types.dag index 6dccdd47017..0c8575c91e9 100644 --- a/dag/extdeps/languages/go/types.dag +++ b/dag/extdeps/languages/go/types.dag @@ -33,7 +33,7 @@ data go_algebra_inhabitants: List = [ import_path: none, is_copy: none }, - { algebra: "BooleanAlgebra", + { algebra: "FinitePowerSet", template: "map[\{0\}]struct{}", arity: 1, identity_expr: "nil", @@ -54,6 +54,13 @@ data go_algebra_inhabitants: List = [ import_path: none, is_copy: none }, + { algebra: "FinitelySupportedFunction", + template: "map[\{0\}]\{1\}", + arity: 2, + identity_expr: "nil", + import_path: none, + is_copy: none }, + { algebra: "OrderedRing", template: "int64", arity: 0, diff --git a/dag/extdeps/languages/python/types.dag b/dag/extdeps/languages/python/types.dag index 1656c9b54c0..adb244c0533 100644 --- a/dag/extdeps/languages/python/types.dag +++ b/dag/extdeps/languages/python/types.dag @@ -32,7 +32,7 @@ data python_algebra_inhabitants: List = [ import_path: none, is_copy: none }, - { algebra: "BooleanAlgebra", + { algebra: "FinitePowerSet", template: "set[\{0\}]", arity: 1, identity_expr: "set()", @@ -53,6 +53,13 @@ data python_algebra_inhabitants: List = [ import_path: none, is_copy: none }, + { algebra: "FinitelySupportedFunction", + template: "dict[\{0\}, \{1\}]", + arity: 2, + identity_expr: "{}", + import_path: none, + is_copy: none }, + { algebra: "OrderedRing", template: "int", arity: 0, diff --git a/dag/extdeps/languages/rust/types.dag b/dag/extdeps/languages/rust/types.dag index 1694de474e6..b75986b3415 100644 --- a/dag/extdeps/languages/rust/types.dag +++ b/dag/extdeps/languages/rust/types.dag @@ -43,7 +43,7 @@ data rust_algebra_inhabitants: List = [ import_path: none, is_copy: false }, - { algebra: "BooleanAlgebra", + { algebra: "FinitePowerSet", template: "BTreeSet<\{0\}>", arity: 1, identity_expr: "BTreeSet::new()", @@ -64,6 +64,13 @@ data rust_algebra_inhabitants: List = [ import_path: none, is_copy: false }, + { algebra: "FinitelySupportedFunction", + template: "HashMap<\{0\}, \{1\}>", + arity: 2, + identity_expr: "HashMap::new()", + import_path: none, + is_copy: false }, + { algebra: "OrderedRing", template: "i64", arity: 0, diff --git a/dag/extdeps/languages/typescript/types.dag b/dag/extdeps/languages/typescript/types.dag index 78b75907838..76593826367 100644 --- a/dag/extdeps/languages/typescript/types.dag +++ b/dag/extdeps/languages/typescript/types.dag @@ -33,7 +33,7 @@ data ts_algebra_inhabitants: List = [ import_path: none, is_copy: false }, - { algebra: "BooleanAlgebra", + { algebra: "FinitePowerSet", template: "Set<\{0\}>", arity: 1, identity_expr: "new Set()", @@ -54,6 +54,13 @@ data ts_algebra_inhabitants: List = [ import_path: none, is_copy: false }, + { algebra: "FinitelySupportedFunction", + template: "Map<\{0\}, \{1\}>", + arity: 2, + identity_expr: "new Map()", + import_path: none, + is_copy: false }, + { algebra: "OrderedRing", template: "number", arity: 0, diff --git a/dag/gunbc/plans/representation_minimization.dag b/dag/gunbc/plans/representation_minimization.dag index edb27ae0201..d5bd6499862 100644 --- a/dag/gunbc/plans/representation_minimization.dag +++ b/dag/gunbc/plans/representation_minimization.dag @@ -23,7 +23,7 @@ fn representation_minimization_body() -> List { p(text: "Lever B attacks BYTES-PER-NODE; Lever C (item 2) attacks MODULES-HELD-AT-ONCE. The two axes are orthogonal and compose multiplicatively — neither blocks the other. Lever B is gated on emitter determinism (#5879) and lands in the v2/.dag realization. Lever C has no dependency on the emitter gate and is deferred to the v2 streaming-infer realization when v2 infer becomes the live path (see the Lever C disposition section; decision A3)."), h2(text: "Lever C (item 2) disposition — design note (2026-06-28)"), p(text: "Design-first investigation result. The §2 finding is real and verified by execution: the floor / claim-execution interpreter consumes only the resolved Node tree (module items + item_registry + source_indices), NEVER the per-module type_env/func_env (proven by a discriminating teeth control — evicting items/item_registry turns reflection witnesses RED, while evicting only type_env/func_env keeps the whole 1109-witness floor GREEN). The emit path (a separate process) genuinely consumes the envs and stays byte-identical."), - p(text: "Extend, do not fork (DESIGN §3): the v2 self-host compiler ALREADY models the consumed-core-vs-envs split — `03_resolve.dag` `ResolvedTree = Node` (env-free) versus `04_infer.dag` `InferredTree { root: Node, facts: Map }`, where the facts side-map (grounding + termination descent) is v2's analog of v1's type_env/func_env. v1's monolithic `ResolvedGraph { Vec }` is the bootstrap-seed artifact that conflates what v2 already splits. No new resolve-output type is minted; Lever C aligns to the existing v2 types."), + p(text: "Extend, do not fork (DESIGN §3): the v2 self-host compiler ALREADY models the consumed-core-vs-envs split — `03_resolve.dag` `ResolvedTree = Node` (env-free) versus `04_infer.dag` `InferredTree { root: Node, facts: PartialFunction }`, where the facts side-map (grounding + termination descent) is v2's analog of v1's type_env/func_env. v1's monolithic `ResolvedGraph { Vec }` is the bootstrap-seed artifact that conflates what v2 already splits. No new resolve-output type is minted; Lever C aligns to the existing v2 types."), p(text: "The v2-surviving root is a RETENTION/EVICTION POLICY, not a type and not a fact-elimination: a module's inference facts are live only while it and its DIRECT dependents are processed (typecheck reads direct imports' facts; imported types are copied by value), so a module's facts evict once the dependency frontier passes — peak bounded by frontier width, not total modules (the #5867 shared-intern_table precedent: an algorithmic single authority). v2 `00_compile` today holds `InferredTree` WHOLE across infer→lens-gates→emit/eval, so this bound is genuinely OWED at v2 `00_compile`, unrealized."), p(text: "Why this is a design note and not a modeled lens today (DESIGN §5/§6): v1 is hand-written bootstrap Rust that does NOT consume the .dag authority, so a .dag-modeled bound plus a hand-coded v1 frontier-evict would be parallel representation with no derivation link, and a lens asserting the bound over v2 infer would be inert (v2 infer is not the live path — no executing consumer). The bound is therefore recorded here, to be realized as v2 infer's streaming-infer when v2 becomes the live compiler. The interim bulk-eviction PR (#5886) was dropped: it trimmed only SUSTAINED interp RSS, not the per-shard resolve/infer PEAK that is the floor OOM axis (concurrency is peak-bound, #5867/CI-floor)."), p(text: "Decision (MEASURED 2026-06-28): A3 — frontier-evict is NOT written into the doomed v1 typecheck seed; the ~4 GiB eviction prize is captured durably by the v2 streaming-infer realization of the frontier-bounded retention bound (the resolution-strategy fact above), when v2 infer becomes the live path. This was a data-gated decision and the data resolved to A3, robustly: the post-cutover floor measurement (claim_executor per-shard VmHWM × spawn_width=2, sccache excluded as a separate process tree) is co-resident 5.98 GiB — 1.82 GiB UNDER the ~7.8 GiB safety threshold below the 8 GiB host cgroup cap, only +0.7 percent above the 5.94 GiB pre-cutover baseline (noise). The cheaper fixes already in main — the floor alloc-clamp binding concurrency to the live cgroup limit, the shared intern_table, and the spawn-width-from-budget throttle — hold the floor comfortably under cap, and the cutover does not regress it. So v1 frontier-evict is NOT forced (the acute-pain justification that would have cemented doomed-seed Rust is absent). Its residual value at this margin is throughput-headroom (a lower per-shard peak permits a higher spawn_width), which belongs to the allocation lane (`docs/plans/resource-aware-scheduler.md`), not this representation lane. Verdict metric note: co-resident = per-shard VmHWM × spawn_width is a deliberately conservative upper bound (assumes simultaneous shard peaks), the correct fail-closed bias for a hard cap; the 1.82 GiB margin makes A3 robust rather than borderline. The flip-to-A1 trigger stays documented and re-auditable: if the corpus later grows enough that the post-cutover co-resident peak reaches ~7.8 GiB, A1 re-activates — implement frontier-evict on the claim-scoped `MultiEntryIndex.typed_module_cache` (eviction predicate fail-closed: a module's typed graph is evictable only once every module that imports it has been resolved, conservative-when-uncertain), gated on a consumer-completeness design read since that cache is load-bearing floor infrastructure. UN-tripped today at the measured 1.82 GiB margin."), diff --git a/dag/std/algebra.dag b/dag/std/algebra.dag index 80b98313d02..9203168cba9 100644 --- a/dag/std/algebra.dag +++ b/dag/std/algebra.dag @@ -118,6 +118,35 @@ type PointwisePower { member: fn(T) -> Bool } +// THE FINITE POWER SET -- Pfin, the set of FINITE subsets -- is the enumerable counterpart of +// `PointwisePower` above, which presents the full power set as a characteristic function. The two +// sit on the SUPPORT axis exactly as `PartialFunction` and `FinitelySupportedFunction` do below: +// one answers membership and nothing else, the other can be walked. +// +// AUTHORED HERE BECAUSE THE CONCEPT WAS ALREADY IN TREE UNDER A BORROWED NAME. Every language that +// carries an algebra inhabitant row files the finite-set realization under `"BooleanAlgebra"`: +// +// rust BTreeSet<{0}> go map[{0}]struct{} +// python set[{0}] typescript Set<{0}> +// +// Four independent realizations, four finite-set containers, not one lattice among them -- while +// the TYPE `BooleanAlgebra` is `{ meet, join, complement, top, bottom }` and its only +// construction in the corpus is `v2.std.logic` `bool_boolean_algebra`, a genuine Boolean algebra +// over `Bool`. The realization roster and the type disagreed about what the name meant, and the +// rust roster carried the tell outright: the `"BooleanAlgebra"` and `"PointwisePower"` rows were +// BYTE-IDENTICAL, two algebra names resolving to one realization with nothing saying which was +// which. This declaration takes the finite-set concept out from under the lattice's name; the +// lattice keeps its name, its type and its one construction site unchanged. +type FinitePowerSet { + member: fn(T) -> Bool + union: fn(FinitePowerSet) -> FinitePowerSet + intersect: fn(FinitePowerSet) -> FinitePowerSet + diff: fn(FinitePowerSet) -> FinitePowerSet + contains: fn(T) -> Bool + count: fn() -> Int + length: fn() -> Int +} + type FreeMonoid = Empty | Cons { head: T, tail: FreeMonoid } @@ -127,12 +156,52 @@ type FreeSemigroup { tail: FreeMonoid } +// TWO AXES, THREE INHABITED CORNERS. The family below is a 2x2 space and the corpus lives in +// three of its corners, so three carriers are authored and the fourth is named rather than +// silently omitted. +// +// TOTALITY -- does the function answer at every point (`fn(K) -> V`) or may it decline +// (`fn(K) -> V?`) -- is independent of SUPPORT -- does it differ from the absent value at +// finitely many points, so that it can be enumerated, or at arbitrarily many, so that it cannot. +// +// arbitrary support finite support +// total TotalMap (uninhabited) +// partial PartialFunction FinitelySupportedFunction +// +// The uninhabited corner is REPRESENTABLE, not impossible: a total function taking a non-default +// value at finitely many points is a perfectly good object. It is unauthored because no corpus +// site needs one. The condition that fills it is a site that must both answer everywhere and be +// enumerated; author it then, and not before. +// +// The predicate family sits on the same support axis one row up: `PointwisePower` is the full +// power set presented as a characteristic function, and its finite counterpart has no carrier +// yet -- see the `Set` alias in `std.types` for that open half and its trigger. type PartialFunction { lookup: fn(K) -> V? - empty: PartialFunction +} + +// FINITE SUPPORT IS WHAT MAKES THE ENUMERATION SURFACE HONEST. Everything below `lookup` here -- +// keys, values, size, and the insert/merge that must preserve them -- is answerable only because +// the support is finite. That is exactly why these rows may not sit on `PartialFunction`: an open +// partial function cannot produce `map_keys` at all, and until this split every one of the 145 +// `Map { lookup: .. }` literals in the corpus named a carrier promising ten operations it +// supplied one of. Measured before the split: 0 of those 145 supplied any field beyond `lookup`. +// +// `lookup` appears on BOTH carriers rather than being inherited, because the substrate has no +// subtyping: a finite map really does answer lookup, and saying so twice is the honest encoding +// of "this one can do everything that one can, and more". +// +// RECORDED, NOT INTRODUCED, and not dissolved here: `lookup`, `get` and `map_get` are three +// spellings of one operation, which the template rosters below carry as three rows. That is the +// same Section 3 fork `algebra_count_length_name_fork_note` records for count/length/size, it +// predates this change, and collapsing it is a corpus-wide rename touching every call site -- +// its own lane. The split neither widens nor narrows it; the three spellings move together. +type FinitelySupportedFunction { + lookup: fn(K) -> V? + empty: FinitelySupportedFunction get: fn(K) -> V? - insert: fn(K, V) -> PartialFunction - merge: fn(PartialFunction) -> PartialFunction + insert: fn(K, V) -> FinitelySupportedFunction + merge: fn(FinitelySupportedFunction) -> FinitelySupportedFunction map_keys: fn() -> FreeMonoid map_values: fn() -> FreeMonoid map_has: fn(K) -> Bool @@ -140,6 +209,25 @@ type PartialFunction { size: fn() -> Int } +// MOVED HERE from `v2.std.collection` by the change that split `PartialFunction`. They are the +// total corner of the family above, and leaving them in a different module from their own axis is +// where a fork starts. `TotalPolicy` travels with `TotalMap` rather than staying behind: it is the +// same total lookup carrying a context argument, and splitting a pair across two modules is the +// thing this change exists to stop doing. +// +// Both had ZERO code consumers at the time of the move -- one declaration each and two prose cells +// in `gunbc.plans.self_applying_lenses`, which marks `table_decision_tree` as an Unrealized +// scaffold and names these as its target substrate rows. So they are carriers authored ahead of a +// consumer that a plan does declare, which is weaker than an untracked scaffold and stronger than +// healthy. The home is the cheap part of the answer; the consumer is that plan's to land. +type TotalMap { + lookup: fn(K) -> V +} + +type TotalPolicy { + lookup: fn(K, Context) -> RowTemplate +} + type Ordering = Less | Equal | Greater type OrderingFold { @@ -171,11 +259,12 @@ type AlgebraProfile = OrderedRingProfile | ApproximateFieldProfile | BooleanAlgebraProfile - | BooleanAlgebraCollectionProfile + | FinitePowerSetProfile | PointwisePowerCollectionProfile | FreeMonoidScalarProfile | FreeMonoidCollectionProfile | PartialFunctionProfile + | FinitelySupportedFunctionProfile type ContainerSource = SameAsReceiver @@ -215,6 +304,25 @@ type AlgebraFieldTemplate { callback_element_position: Int? } +// THE CARRIER NAMES ARE KEYS HERE, NOT ONLY THE ALIAS SPELLINGS, and that is a repair rather +// than an extension. This map is what `kernel_profile_lookup` consults to decide whether a +// receiver has a declared method surface at all; `04_infer.dag`'s method-existence wall refuses +// with `MethodExistenceUndecided` when it does not. Keyed on `"Set"` and `"Map"` alone, a +// declaration that wrote the CARRIER name instead of the alias had no surface — so +// `tree.facts.lookup(node)` on a `PartialFunction` receiver refused, while +// the byte-identical call on a `Map` receiver resolved. One concept, two answers, decided by +// which of two spellings for it the author happened to write: the §3 fork exactly. +// +// It was invisible while every site wrote the alias. The carrier decomposition made the carrier +// names the ones declarations write, and the hole surfaced immediately at the floor's strict +// preparation — a stricter instrument than the compile board, which reported 0 blocking on the +// same tree. +// +// `PointwisePower` is deliberately NOT added here. Its 80 declaration positions predate this +// lane, its templates are a different set from `FinitePowerSet`'s, and adding it changes the +// wall from UNDECIDED to DECIDED for every one of them at once — which would turn any method +// absent from `pointwise_power_collection_templates` into a hard `MethodNotFound`. That is a +// measurement this change has not taken, so the row is named as residue rather than added blind. fn kernel_algebra_profile_value() -> Map { map_insert( map_insert( @@ -222,13 +330,19 @@ fn kernel_algebra_profile_value() -> Map { map_insert( map_insert( map_insert( - map_insert(empty_map(), "Int", OrderedRingProfile), - "Float", ApproximateFieldProfile), - "Bool", BooleanAlgebraProfile), - "String", FreeMonoidScalarProfile), - "List", FreeMonoidCollectionProfile), - "Set", PointwisePowerCollectionProfile), - "Map", PartialFunctionProfile) + map_insert( + map_insert( + map_insert( + map_insert(empty_map(), "Int", OrderedRingProfile), + "Float", ApproximateFieldProfile), + "Bool", BooleanAlgebraProfile), + "String", FreeMonoidScalarProfile), + "List", FreeMonoidCollectionProfile), + "Set", FinitePowerSetProfile), + "Map", FinitelySupportedFunctionProfile), + "FinitePowerSet", FinitePowerSetProfile), + "FinitelySupportedFunction", FinitelySupportedFunctionProfile), + "PartialFunction", PartialFunctionProfile) } data kernel_algebra_profile: Map = kernel_algebra_profile_value() @@ -267,7 +381,7 @@ fn boolean_algebra_templates() -> List { ] } -fn boolean_algebra_collection_templates() -> List { +fn finite_power_set_templates() -> List { [ { name: "union", param_types: [ReceiverSelf, ReceiverSelf], return_type: ReceiverSelf, size_effect: none, cost_shape: none, callback_element_position: none }, { name: "intersect", param_types: [ReceiverSelf, ReceiverSelf], return_type: ReceiverSelf, size_effect: none, cost_shape: none, callback_element_position: none }, @@ -345,6 +459,14 @@ fn free_monoid_collection_templates() -> List { } fn partial_function_templates() -> List { + [ + { name: "get", param_types: [ReceiverSelf, ReceiverKey], return_type: OptionalOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none }, + { name: "map_get", param_types: [ReceiverSelf, ReceiverKey], return_type: OptionalOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none }, + { name: "lookup", param_types: [ReceiverSelf, ReceiverKey], return_type: OptionalOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none } + ] +} + +fn finitely_supported_function_templates() -> List { [ { name: "get", param_types: [ReceiverSelf, ReceiverKey], return_type: OptionalOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none }, { name: "map_get", param_types: [ReceiverSelf, ReceiverKey], return_type: OptionalOf { inner: ReceiverValue }, size_effect: none, cost_shape: none, callback_element_position: none }, @@ -372,11 +494,12 @@ fn algebra_templates_for_profile(profile: AlgebraProfile) -> List ordered_ring_templates() ApproximateFieldProfile => approximate_field_templates() BooleanAlgebraProfile => boolean_algebra_templates() - BooleanAlgebraCollectionProfile => boolean_algebra_collection_templates() + FinitePowerSetProfile => finite_power_set_templates() PointwisePowerCollectionProfile => pointwise_power_collection_templates() FreeMonoidScalarProfile => free_monoid_scalar_templates() FreeMonoidCollectionProfile => free_monoid_collection_templates() PartialFunctionProfile => partial_function_templates() + FinitelySupportedFunctionProfile => finitely_supported_function_templates() } } @@ -385,11 +508,12 @@ fn algebra_type_param_names(profile: AlgebraProfile) -> List { OrderedRingProfile => [] ApproximateFieldProfile => [] BooleanAlgebraProfile => [] - BooleanAlgebraCollectionProfile => ["T"] + FinitePowerSetProfile => ["T"] PointwisePowerCollectionProfile => ["T"] FreeMonoidScalarProfile => [] FreeMonoidCollectionProfile => ["T"] PartialFunctionProfile => ["K", "V"] + FinitelySupportedFunctionProfile => ["K", "V"] } } @@ -398,11 +522,12 @@ fn all_algebra_profiles() -> List { OrderedRingProfile, ApproximateFieldProfile, BooleanAlgebraProfile, - BooleanAlgebraCollectionProfile, + FinitePowerSetProfile, PointwisePowerCollectionProfile, FreeMonoidScalarProfile, FreeMonoidCollectionProfile, PartialFunctionProfile, + FinitelySupportedFunctionProfile, ] } diff --git a/dag/std/computation.dag b/dag/std/computation.dag index be2594ce178..6f28a7fd22f 100644 --- a/dag/std/computation.dag +++ b/dag/std/computation.dag @@ -8,10 +8,10 @@ import std.termination { } import std.algebra { AlgebraProfile, OrderedRingProfile, ApproximateFieldProfile, - BooleanAlgebraProfile, BooleanAlgebraCollectionProfile, + BooleanAlgebraProfile, FinitePowerSetProfile, PointwisePowerCollectionProfile, FreeMonoidScalarProfile, FreeMonoidCollectionProfile, - PartialFunctionProfile, + PartialFunctionProfile, FinitelySupportedFunctionProfile, kernel_algebra_profile } @@ -142,16 +142,23 @@ type IterationDimension | CollectionFold | ArithmeticRepeat +// THE FOLDABLE PROFILES ARE EXACTLY THE FINITELY SUPPORTED ONES, and saying that became possible +// only once the carriers were split. `PartialFunctionProfile` answered `CollectionFold` here while +// `PointwisePowerCollectionProfile` answered `none` -- the same distinction, decided two different +// ways, because one name carried both an open function and a finite table. An open partial +// function has no iteration dimension for the same reason an open characteristic function does +// not: there is nothing to walk. The two open profiles now agree, and the two finite ones do. fn algebra_profile_to_dimension(profile: AlgebraProfile) -> IterationDimension? { match profile { - FreeMonoidCollectionProfile => Present { value: CollectionFold } - FreeMonoidScalarProfile => Present { value: CollectionFold } - BooleanAlgebraCollectionProfile => Present { value: CollectionFold } - PointwisePowerCollectionProfile => none - PartialFunctionProfile => Present { value: CollectionFold } - OrderedRingProfile => Present { value: ArithmeticRepeat } - ApproximateFieldProfile => Present { value: ArithmeticRepeat } - BooleanAlgebraProfile => none + FreeMonoidCollectionProfile => Present { value: CollectionFold } + FreeMonoidScalarProfile => Present { value: CollectionFold } + FinitePowerSetProfile => Present { value: CollectionFold } + FinitelySupportedFunctionProfile => Present { value: CollectionFold } + PointwisePowerCollectionProfile => none + PartialFunctionProfile => none + OrderedRingProfile => Present { value: ArithmeticRepeat } + ApproximateFieldProfile => Present { value: ArithmeticRepeat } + BooleanAlgebraProfile => none } } diff --git a/dag/std/types.dag b/dag/std/types.dag index 5a3939b4689..6accc6893a8 100644 --- a/dag/std/types.dag +++ b/dag/std/types.dag @@ -1,6 +1,6 @@ module std.types -import std.algebra { FreeMonoid, PartialFunction, PointwisePower, kernel_algebra_profile, algebra_type_param_names } +import std.algebra { FinitePowerSet, FinitelySupportedFunction, FreeMonoid, kernel_algebra_profile, algebra_type_param_names } data kernel_type_set: Map = { "String": true, "Int": true, "Bool": true, "Float": true, @@ -59,27 +59,53 @@ fn is_ordered_element_collection(name: String) -> Bool { data container_template_algebra_rows: Map = { "List": "FreeMonoid", "list": "FreeMonoid", - "Set": "PointwisePower", - "set": "PointwisePower", - "Map": "PartialFunction", - "map": "PartialFunction", + "Set": "FinitePowerSet", + "set": "FinitePowerSet", + "Map": "FinitelySupportedFunction", + "map": "FinitelySupportedFunction", "FreeMonoid": "FreeMonoid", "free_monoid": "FreeMonoid", "BooleanAlgebra": "BooleanAlgebra", "boolean_algebra": "BooleanAlgebra", + "FinitePowerSet": "FinitePowerSet", + "finite_power_set": "FinitePowerSet", + "FinitelySupportedFunction": "FinitelySupportedFunction", + "finitely_supported_function": "FinitelySupportedFunction", "PartialFunction": "PartialFunction", "partial_function": "PartialFunction", "PointwisePower": "PointwisePower", "pointwise_power": "PointwisePower" } +// PARTIALFUNCTION IS HERE BECAUSE THIS MAP DECIDES WHAT RESOLVES AS A CONTAINER, not merely what +// is an alias for something else. `is_declared_container_alias_spelling` reads it, and +// `resolve_method_receiver_type` short-circuits on that predicate to return the receiver AS +// AUTHORED, type arguments intact. A spelling absent from here takes the other branch, resolves to +// the carrier's own record shape, and arrives at method lookup as a bare leaf -- so +// `lookup`'s declared `OptionalOf { inner: ReceiverValue }` has no `ReceiverValue` to substitute +// and the optional collapses. Measured: `tree.facts.lookup(node)` on a `PartialFunction` receiver +// produced four `variant 'Present' not found in type 'InferredFacts'` refusals, the Optional's +// cardinality dropped and the inner product arriving in its place -- which is one of the four +// receiver-resolution shapes `unresolved_method_frontier` already names as residue. +// +// A self-mapping row is not a nickname. The value is the ALGEBRA and the key is a SPELLING that +// resolves to it; `FreeMonoid` and `PointwisePower` are equally absent and would fail the same way +// if written directly, which is why `List` and `Set` exist as keys at all. The carriers this lane +// makes directly writable therefore need their own keys. +// +// Only `PartialFunction` is added, and the reason is `container_alias_canonical_spelling`: it +// returns the FIRST sorted key mapping to an algebra, so a `"FinitelySupportedFunction"` key would +// sort ahead of `"Map"` and silently become the canonical spelling for that algebra everywhere it +// is emitted. No existing key maps to `PartialFunction`, so this addition competes with nothing. data container_template_alias_rows: Map = { "List": "FreeMonoid", "list": "FreeMonoid", - "Set": "PointwisePower", - "set": "PointwisePower", - "Map": "PartialFunction", - "map": "PartialFunction" + "Set": "FinitePowerSet", + "set": "FinitePowerSet", + "Map": "FinitelySupportedFunction", + "map": "FinitelySupportedFunction", + "PartialFunction": "PartialFunction", + "partial_function": "PartialFunction" } fn container_template_algebra(name: String) -> String? { @@ -90,8 +116,20 @@ fn container_template_alias_algebra(name: String) -> String? { map_get(container_template_alias_rows, name) } +// THE COMPLETE ROSTER, and completing it is what lets its consumer stop patching it. This list +// feeds `v1.compiler.coercion` `inhabitant_test_names`, which used to read +// `concat(canonical_container_names(), ["PointwisePower"])` -- a hand-appended name compensating +// for one this list omitted. That append is deleted with this change: a caller patching its +// authority's answer is the authority being wrong, not the caller being thorough. +// +// TWO CORRECTIONS THE CARRIER SPLIT FORCED, both of which an unedited list would have got wrong in +// opposite directions. `BooleanAlgebra` LEAVES: its container inhabitant row moved to +// `FinitePowerSet`, so it names no container any more -- it is the lattice, and a lattice in a +// container roster is the misfiling this change exists to end. `PartialFunction` STAYS: it keeps a +// row and is now reachable as a declared spelling in its own right, so dropping it would have +// silently retired its coercion coverage at the moment it acquired real callers. fn canonical_container_names() -> List { - ["BooleanAlgebra", "FreeMonoid", "List", "Map", "PartialFunction", "Set", "Witness"] + ["FinitePowerSet", "FinitelySupportedFunction", "FreeMonoid", "List", "Map", "PartialFunction", "PointwisePower", "Set", "Witness"] } type Bool = True | False @@ -104,26 +142,46 @@ 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`. +// BOTH ALIASES NAME THE FINITE CARRIER, and this is the motion the predicate-half change +// (`PointwisePower`, landed separately) was waiting for. A `Set` or a `Map` in a declaration +// position has always LOWERED to a finite container -- `im::OrdSet` and `HashMap` in Rust, and the +// same story in Go, Python and TypeScript -- so pointing the aliases at the finite carriers makes +// the declaration say what the realization already did. The open carriers keep their own names: +// `std.algebra` `PointwisePower` for a characteristic function, `PartialFunction` for a partial +// one. +// +// Why the two rows move together rather than one at a time: they are one row set. Retargeting +// `Map` while `Set` still resolved to the predicate would leave the fork intact on the Set side +// and make the pair inconsistent for the interval, which is the dual-authority state the +// replacement-migration doctrine exists to avoid. The transition is atomic in the AUTHORITY sense +// -- one motion, no interval in which both answers are live -- whatever the diff size. +// +// RUNG: STILL MITIGATABLE. This change does NOT make the bad literal unwritable, and saying it did +// would be the inflation DESIGN 4b calls worse than sitting low. `FinitePowerSet` carries `member` +// and `FinitelySupportedFunction` carries `lookup`, because a finite set really does answer +// membership and a finite map really does answer lookup -- so `Set { member: .. }` and +// `Map { lookup: .. }` still typecheck. They must: 145 `Map { lookup: .. }` literals are live in +// the corpus and are re-authored by the following change, not by this one. +// +// The correction is that the invalid state was never "a literal supplying `member` or `lookup`". +// It is "a literal supplying ONLY those, on a carrier whose remaining fields promise an +// enumeration it cannot perform" -- a construction-COMPLETENESS question, and record literals in +// this substrate do not require every field. So the real NEXT-RUNG TRIGGER is field-completeness +// enforcement on record construction, which would make the deficient literal unwritable at every +// carrier at once rather than at these two. Until that exists the class stays mitigatable and only +// review sees a new one; what this change buys is that each alias now names a carrier that can +// answer for it, which is the single-authority half, not the wall. // -// 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 +// CARRIED FORWARD FROM THE PREDICATE-HALF CHANGE (#9055), whose note this row replaces: the +// fusion was measured, not argued -- `extdeps.languages.rust.types` gave `PointwisePower` the +// inhabitant `BTreeSet<{0}>`, so a declaration position lowered to `im::OrdSet` while a record +// literal lowered to the algebra struct, and the two met as a rustc refusal wherever one compiled +// closure held both (`docs/probes/t3_collection_realization_2026-08-22.md`). That change also +// closed the predicate half: no `Set { member: .. }` literal survives in `src/v2`, so the Set side +// of the fork is a spelling question only. Its stated NEXT-RUNG TRIGGER was the Map-side +// decomposition landing, after which both rows retarget in one motion. That is this row. +type Set = FinitePowerSet +type Map = FinitelySupportedFunction fn list_length(items: List) -> Int { fold(items, init: 0, f: (acc, _) => acc + 1) diff --git a/src/v1/04_types.dag b/src/v1/04_types.dag index db8e0967809..7179eb5a0fe 100644 --- a/src/v1/04_types.dag +++ b/src/v1/04_types.dag @@ -6,9 +6,9 @@ import std.types { SourceSpan, is_container_type, container_expected_arity, cont import std.algebra { AlgebraProfile, OrderedRingProfile, ApproximateFieldProfile, - BooleanAlgebraProfile, BooleanAlgebraCollectionProfile, + BooleanAlgebraProfile, FinitePowerSetProfile, FreeMonoidScalarProfile, - FreeMonoidCollectionProfile, PartialFunctionProfile, + FreeMonoidCollectionProfile, PartialFunctionProfile, FinitelySupportedFunctionProfile, AlgebraTypeTemplate, ReceiverSelf, ReceiverElement, ReceiverKey, ReceiverValue, NamedTemplate, ContainerOf, ContainerSource, SameAsReceiver, Named, OptionalOf, WitnessOf, TupleOf, AlgebraTypeVariable, AlgebraFieldTemplate, diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index d842048873b..4939313dfaa 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -4996,6 +4996,9 @@ fn emit_faithful_text_carrier_import_lines(imported_names: List, local_t let needs_int = items |> any(item => module_item_references_type_name(item: item, type_name: "Int", source_indices: source_indices)) let needs_partial_function = items |> any(item => module_item_references_type_name(item: item, type_name: "PartialFunction", source_indices: source_indices) + ) + let needs_finitely_supported_function = items |> any(item => + module_item_references_type_name(item: item, type_name: "FinitelySupportedFunction", source_indices: source_indices) || module_item_references_type_name(item: item, type_name: "Map", source_indices: source_indices) ) let needs_measure_phantoms = closure_has_std_measure && items |> any(item => module_item_references_faithful_expanded_type(item: item, source_indices: source_indices)) @@ -5024,6 +5027,11 @@ fn emit_faithful_text_carrier_import_lines(imported_names: List, local_t } else { [concat(rust_visibility_prefix(), "use crate::std_algebra::PartialFunction;")] } + let finitely_supported_function = if !needs_finitely_supported_function || rust_import_name_already_resolved(imported_names: imported_names, local_type_names: local_type_names, name: "FinitelySupportedFunction") { + [] + } else { + [concat(rust_visibility_prefix(), "use crate::std_algebra::FinitelySupportedFunction;")] + } let memory = if !needs_measure_phantoms || rust_import_name_already_resolved(imported_names: imported_names, local_type_names: local_type_names, name: "Memory") { [] } else { @@ -5034,7 +5042,7 @@ fn emit_faithful_text_carrier_import_lines(imported_names: List, local_t } else { [concat(rust_visibility_prefix(), "use crate::std_measure::One;")] } - concat(free_monoid, char_line, non_empty_str, int_line, partial_function, memory, one) + concat(free_monoid, char_line, non_empty_str, int_line, partial_function, finitely_supported_function, memory, one) } fn emit_prelude(imported_names: List, local_type_names: List) -> String { diff --git a/src/v1/coercion.dag b/src/v1/coercion.dag index f33a3380720..18ac2153115 100644 --- a/src/v1/coercion.dag +++ b/src/v1/coercion.dag @@ -374,7 +374,7 @@ fn checkpoint_tests(target: RenderTarget) -> List { } fn inhabitant_test_names() -> List { - concat(canonical_container_names(), ["PointwisePower"]) + canonical_container_names() } fn inhabitant_tests(target: RenderTarget) -> List { diff --git a/src/v1/stage0/src/compiler_tests.rs b/src/v1/stage0/src/compiler_tests.rs index a70bfdc921b..3126099aac8 100644 --- a/src/v1/stage0/src/compiler_tests.rs +++ b/src/v1/stage0/src/compiler_tests.rs @@ -1950,9 +1950,13 @@ mod compiler_tests { fn coercion_rust_inhabitant_resolves_containers() { use crate::v1_compiler_coercion::*; assert_eq!( - coerce_container_template(RenderTarget::Rust, "BooleanAlgebra".into()), + coerce_container_template(RenderTarget::Rust, "FinitePowerSet".into()), Some("BTreeSet<{0}>".to_string()) ); + assert_eq!( + coerce_container_template(RenderTarget::Rust, "FinitelySupportedFunction".into()), + Some("HashMap<{0}, {1}>".to_string()) + ); assert_eq!( coerce_container_template(RenderTarget::Rust, "FreeMonoid".into()), Some("Vec<{0}>".to_string()) @@ -1970,11 +1974,11 @@ mod compiler_tests { Some("HashMap<{0}, {1}>".to_string()) ); assert_eq!( - coerce_container_template(RenderTarget::Rust, "Set".into()), + coerce_container_template(RenderTarget::Rust, "PointwisePower".into()), Some("BTreeSet<{0}>".to_string()) ); assert_eq!( - coerce_container_template(RenderTarget::Rust, "PointwisePower".into()), + coerce_container_template(RenderTarget::Rust, "Set".into()), Some("BTreeSet<{0}>".to_string()) ); } @@ -1983,9 +1987,13 @@ mod compiler_tests { fn coercion_python_inhabitant_resolves_containers() { use crate::v1_compiler_coercion::*; assert_eq!( - coerce_container_template(RenderTarget::Python, "BooleanAlgebra".into()), + coerce_container_template(RenderTarget::Python, "FinitePowerSet".into()), Some("set[{0}]".to_string()) ); + assert_eq!( + coerce_container_template(RenderTarget::Python, "FinitelySupportedFunction".into()), + Some("dict[{0}, {1}]".to_string()) + ); assert_eq!( coerce_container_template(RenderTarget::Python, "FreeMonoid".into()), Some("list[{0}]".to_string()) @@ -2003,11 +2011,11 @@ mod compiler_tests { Some("dict[{0}, {1}]".to_string()) ); assert_eq!( - coerce_container_template(RenderTarget::Python, "Set".into()), + coerce_container_template(RenderTarget::Python, "PointwisePower".into()), Some("set[{0}]".to_string()) ); assert_eq!( - coerce_container_template(RenderTarget::Python, "PointwisePower".into()), + coerce_container_template(RenderTarget::Python, "Set".into()), Some("set[{0}]".to_string()) ); } @@ -2016,9 +2024,13 @@ mod compiler_tests { fn coercion_go_inhabitant_resolves_containers() { use crate::v1_compiler_coercion::*; assert_eq!( - coerce_container_template(RenderTarget::Go, "BooleanAlgebra".into()), + coerce_container_template(RenderTarget::Go, "FinitePowerSet".into()), Some("map[{0}]struct{}".to_string()) ); + assert_eq!( + coerce_container_template(RenderTarget::Go, "FinitelySupportedFunction".into()), + Some("map[{0}]{1}".to_string()) + ); assert_eq!( coerce_container_template(RenderTarget::Go, "FreeMonoid".into()), Some("[]{0}".to_string()) @@ -2036,11 +2048,11 @@ mod compiler_tests { Some("map[{0}]{1}".to_string()) ); assert_eq!( - coerce_container_template(RenderTarget::Go, "Set".into()), + coerce_container_template(RenderTarget::Go, "PointwisePower".into()), Some("map[{0}]struct{}".to_string()) ); assert_eq!( - coerce_container_template(RenderTarget::Go, "PointwisePower".into()), + coerce_container_template(RenderTarget::Go, "Set".into()), Some("map[{0}]struct{}".to_string()) ); } diff --git a/src/v1/stage0/src/extdeps_languages_go_types.rs b/src/v1/stage0/src/extdeps_languages_go_types.rs index bf1e28f3762..189a6fc56e2 100644 --- a/src/v1/stage0/src/extdeps_languages_go_types.rs +++ b/src/v1/stage0/src/extdeps_languages_go_types.rs @@ -39,7 +39,7 @@ pub fn go_type_checkpoints() -> Rc>> { pub fn go_algebra_inhabitants() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"algebra": "FreeMonoid", "template": "[]{0}", "arity": 1, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "BooleanAlgebra", "template": "map[{0}]struct{}", "arity": 1, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "PointwisePower", "template": "map[{0}]struct{}", "arity": 1, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "PartialFunction", "template": "map[{0}]{1}", "arity": 2, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "OrderedRing", "template": "int64", "arity": 0, "identity_expr": "0", "import_path": null, "is_copy": null}, {"algebra": "ApproximateField", "template": "float64", "arity": 0, "identity_expr": "0.0", "import_path": null, "is_copy": null}])) + serde_json::from_value(serde_json::json!([{"algebra": "FreeMonoid", "template": "[]{0}", "arity": 1, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "FinitePowerSet", "template": "map[{0}]struct{}", "arity": 1, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "PointwisePower", "template": "map[{0}]struct{}", "arity": 1, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "PartialFunction", "template": "map[{0}]{1}", "arity": 2, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "FinitelySupportedFunction", "template": "map[{0}]{1}", "arity": 2, "identity_expr": "nil", "import_path": null, "is_copy": null}, {"algebra": "OrderedRing", "template": "int64", "arity": 0, "identity_expr": "0", "import_path": null, "is_copy": null}, {"algebra": "ApproximateField", "template": "float64", "arity": 0, "identity_expr": "0.0", "import_path": null, "is_copy": null}])) .expect("valid data definition") }; } diff --git a/src/v1/stage0/src/extdeps_languages_python_types.rs b/src/v1/stage0/src/extdeps_languages_python_types.rs index 68f032bde82..427946724ea 100644 --- a/src/v1/stage0/src/extdeps_languages_python_types.rs +++ b/src/v1/stage0/src/extdeps_languages_python_types.rs @@ -40,7 +40,7 @@ pub fn python_type_checkpoints() -> Rc>> { pub fn python_algebra_inhabitants() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"algebra": "FreeMonoid", "template": "list[{0}]", "arity": 1, "identity_expr": "[]", "import_path": null, "is_copy": null}, {"algebra": "BooleanAlgebra", "template": "set[{0}]", "arity": 1, "identity_expr": "set()", "import_path": null, "is_copy": null}, {"algebra": "PointwisePower", "template": "set[{0}]", "arity": 1, "identity_expr": "set()", "import_path": null, "is_copy": null}, {"algebra": "PartialFunction", "template": "dict[{0}, {1}]", "arity": 2, "identity_expr": "{}", "import_path": null, "is_copy": null}, {"algebra": "OrderedRing", "template": "int", "arity": 0, "identity_expr": "0", "import_path": null, "is_copy": null}, {"algebra": "ApproximateField", "template": "float", "arity": 0, "identity_expr": "0.0", "import_path": null, "is_copy": null}])) + serde_json::from_value(serde_json::json!([{"algebra": "FreeMonoid", "template": "list[{0}]", "arity": 1, "identity_expr": "[]", "import_path": null, "is_copy": null}, {"algebra": "FinitePowerSet", "template": "set[{0}]", "arity": 1, "identity_expr": "set()", "import_path": null, "is_copy": null}, {"algebra": "PointwisePower", "template": "set[{0}]", "arity": 1, "identity_expr": "set()", "import_path": null, "is_copy": null}, {"algebra": "PartialFunction", "template": "dict[{0}, {1}]", "arity": 2, "identity_expr": "{}", "import_path": null, "is_copy": null}, {"algebra": "FinitelySupportedFunction", "template": "dict[{0}, {1}]", "arity": 2, "identity_expr": "{}", "import_path": null, "is_copy": null}, {"algebra": "OrderedRing", "template": "int", "arity": 0, "identity_expr": "0", "import_path": null, "is_copy": null}, {"algebra": "ApproximateField", "template": "float", "arity": 0, "identity_expr": "0.0", "import_path": null, "is_copy": null}])) .expect("valid data definition") }; } diff --git a/src/v1/stage0/src/extdeps_languages_rust_types.rs b/src/v1/stage0/src/extdeps_languages_rust_types.rs index cc75e6558be..c6887dc2d3d 100644 --- a/src/v1/stage0/src/extdeps_languages_rust_types.rs +++ b/src/v1/stage0/src/extdeps_languages_rust_types.rs @@ -59,7 +59,7 @@ pub fn rust_checkpoint_scalar_arity_note() -> String { pub fn rust_algebra_inhabitants() -> Rc>> { thread_local! { static CACHED: Rc>> = { - serde_json::from_value(serde_json::json!([{"algebra": "FreeMonoid", "template": "Vec<{0}>", "arity": 1, "identity_expr": "Vec::new()", "import_path": null, "is_copy": false}, {"algebra": "BooleanAlgebra", "template": "BTreeSet<{0}>", "arity": 1, "identity_expr": "BTreeSet::new()", "import_path": null, "is_copy": false}, {"algebra": "PointwisePower", "template": "BTreeSet<{0}>", "arity": 1, "identity_expr": "BTreeSet::new()", "import_path": null, "is_copy": false}, {"algebra": "PartialFunction", "template": "HashMap<{0}, {1}>", "arity": 2, "identity_expr": "HashMap::new()", "import_path": null, "is_copy": false}, {"algebra": "OrderedRing", "template": "i64", "arity": 0, "identity_expr": "0i64", "import_path": null, "is_copy": true}, {"algebra": "ApproximateField", "template": "f64", "arity": 0, "identity_expr": "0.0f64", "import_path": null, "is_copy": true}])) + serde_json::from_value(serde_json::json!([{"algebra": "FreeMonoid", "template": "Vec<{0}>", "arity": 1, "identity_expr": "Vec::new()", "import_path": null, "is_copy": false}, {"algebra": "FinitePowerSet", "template": "BTreeSet<{0}>", "arity": 1, "identity_expr": "BTreeSet::new()", "import_path": null, "is_copy": false}, {"algebra": "PointwisePower", "template": "BTreeSet<{0}>", "arity": 1, "identity_expr": "BTreeSet::new()", "import_path": null, "is_copy": false}, {"algebra": "PartialFunction", "template": "HashMap<{0}, {1}>", "arity": 2, "identity_expr": "HashMap::new()", "import_path": null, "is_copy": false}, {"algebra": "FinitelySupportedFunction", "template": "HashMap<{0}, {1}>", "arity": 2, "identity_expr": "HashMap::new()", "import_path": null, "is_copy": false}, {"algebra": "OrderedRing", "template": "i64", "arity": 0, "identity_expr": "0i64", "import_path": null, "is_copy": true}, {"algebra": "ApproximateField", "template": "f64", "arity": 0, "identity_expr": "0.0f64", "import_path": null, "is_copy": true}])) .expect("valid data definition") }; } diff --git a/src/v1/stage0/src/std_algebra.rs b/src/v1/stage0/src/std_algebra.rs index 33126cb90ba..cf47b77abe5 100644 --- a/src/v1/stage0/src/std_algebra.rs +++ b/src/v1/stage0/src/std_algebra.rs @@ -226,6 +226,18 @@ pub struct PointwisePower { pub _phantom: std::marker::PhantomData, } +#[derive(Clone)] +pub struct FinitePowerSet { + pub member: Rc bool>, + pub union: Rc>) -> Rc>>, + pub intersect: Rc>) -> Rc>>, + pub diff: Rc>) -> Rc>>, + pub contains: Rc bool>, + pub count: Rc i64>, + pub length: Rc i64>, + pub _phantom: std::marker::PhantomData, +} + pub type FreeMonoid = Vec; #[derive(Clone, serde::Serialize, serde::Deserialize)] @@ -257,10 +269,17 @@ impl PartialEq for FreeSemigroup { #[derive(Clone)] pub struct PartialFunction { pub lookup: Rc Option>, - pub empty: Rc>, + pub _phantom: std::marker::PhantomData<(K, V)>, +} + +#[derive(Clone)] +pub struct FinitelySupportedFunction { + pub lookup: Rc Option>, + pub empty: Rc>, pub get: Rc Option>, - pub insert: Rc Rc>>, - pub merge: Rc>) -> Rc>>, + pub insert: Rc Rc>>, + pub merge: + Rc>) -> Rc>>, pub map_keys: Rc Rc>>, pub map_values: Rc Rc>>, pub map_has: Rc bool>, @@ -269,6 +288,18 @@ pub struct PartialFunction { pub _phantom: std::marker::PhantomData<(K, V)>, } +#[derive(Clone)] +pub struct TotalMap { + pub lookup: Rc V>, + pub _phantom: std::marker::PhantomData<(K, V)>, +} + +#[derive(Clone)] +pub struct TotalPolicy { + pub lookup: Rc RowTemplate>, + pub _phantom: std::marker::PhantomData<(K, Context, RowTemplate)>, +} + #[derive( Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, )] @@ -315,11 +346,12 @@ pub enum AlgebraProfile { OrderedRingProfile, ApproximateFieldProfile, BooleanAlgebraProfile, - BooleanAlgebraCollectionProfile, + FinitePowerSetProfile, PointwisePowerCollectionProfile, FreeMonoidScalarProfile, FreeMonoidCollectionProfile, PartialFunctionProfile, + FinitelySupportedFunctionProfile, } #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] @@ -409,26 +441,38 @@ pub fn kernel_algebra_profile_value() -> Rc> { v1_rt::rc_map_insert( v1_rt::rc_map_insert( v1_rt::rc_map_insert( - v1_rt::rc_empty_map::(), - "Int".to_string(), - AlgebraProfile::OrderedRingProfile, + v1_rt::rc_map_insert( + v1_rt::rc_map_insert( + v1_rt::rc_map_insert( + v1_rt::rc_empty_map::(), + "Int".to_string(), + AlgebraProfile::OrderedRingProfile, + ), + "Float".to_string(), + AlgebraProfile::ApproximateFieldProfile, + ), + "Bool".to_string(), + AlgebraProfile::BooleanAlgebraProfile, + ), + "String".to_string(), + AlgebraProfile::FreeMonoidScalarProfile, ), - "Float".to_string(), - AlgebraProfile::ApproximateFieldProfile, + "List".to_string(), + AlgebraProfile::FreeMonoidCollectionProfile, ), - "Bool".to_string(), - AlgebraProfile::BooleanAlgebraProfile, + "Set".to_string(), + AlgebraProfile::FinitePowerSetProfile, ), - "String".to_string(), - AlgebraProfile::FreeMonoidScalarProfile, + "Map".to_string(), + AlgebraProfile::FinitelySupportedFunctionProfile, ), - "List".to_string(), - AlgebraProfile::FreeMonoidCollectionProfile, + "FinitePowerSet".to_string(), + AlgebraProfile::FinitePowerSetProfile, ), - "Set".to_string(), - AlgebraProfile::PointwisePowerCollectionProfile, + "FinitelySupportedFunction".to_string(), + AlgebraProfile::FinitelySupportedFunctionProfile, ), - "Map".to_string(), + "PartialFunction".to_string(), AlgebraProfile::PartialFunctionProfile, ) } @@ -641,7 +685,7 @@ pub fn boolean_algebra_templates() -> Rc>> { ]) } -pub fn boolean_algebra_collection_templates() -> Rc>> { +pub fn finite_power_set_templates() -> Rc>> { Rc::new(vec![ Rc::new(AlgebraFieldTemplate { name: "union".to_string(), @@ -1415,6 +1459,50 @@ pub fn free_monoid_collection_templates() -> Rc>> { } pub fn partial_function_templates() -> Rc>> { + Rc::new(vec![ + Rc::new(AlgebraFieldTemplate { + name: "get".to_string(), + param_types: Rc::new(vec![ + Rc::new(AlgebraTypeTemplate::ReceiverSelf), + Rc::new(AlgebraTypeTemplate::ReceiverKey), + ]), + return_type: Rc::new(AlgebraTypeTemplate::OptionalOf { + inner: Rc::new(AlgebraTypeTemplate::ReceiverValue), + }), + size_effect: None, + cost_shape: None, + callback_element_position: None, + }), + Rc::new(AlgebraFieldTemplate { + name: "map_get".to_string(), + param_types: Rc::new(vec![ + Rc::new(AlgebraTypeTemplate::ReceiverSelf), + Rc::new(AlgebraTypeTemplate::ReceiverKey), + ]), + return_type: Rc::new(AlgebraTypeTemplate::OptionalOf { + inner: Rc::new(AlgebraTypeTemplate::ReceiverValue), + }), + size_effect: None, + cost_shape: None, + callback_element_position: None, + }), + Rc::new(AlgebraFieldTemplate { + name: "lookup".to_string(), + param_types: Rc::new(vec![ + Rc::new(AlgebraTypeTemplate::ReceiverSelf), + Rc::new(AlgebraTypeTemplate::ReceiverKey), + ]), + return_type: Rc::new(AlgebraTypeTemplate::OptionalOf { + inner: Rc::new(AlgebraTypeTemplate::ReceiverValue), + }), + size_effect: None, + cost_shape: None, + callback_element_position: None, + }), + ]) +} + +pub fn finitely_supported_function_templates() -> Rc>> { Rc::new(vec![ Rc::new(AlgebraFieldTemplate { name: "get".to_string(), @@ -1608,11 +1696,12 @@ pub fn algebra_templates_for_profile(profile: AlgebraProfile) -> Rc ordered_ring_templates(), AlgebraProfile::ApproximateFieldProfile => approximate_field_templates(), AlgebraProfile::BooleanAlgebraProfile => boolean_algebra_templates(), - AlgebraProfile::BooleanAlgebraCollectionProfile => boolean_algebra_collection_templates(), + AlgebraProfile::FinitePowerSetProfile => finite_power_set_templates(), AlgebraProfile::PointwisePowerCollectionProfile => pointwise_power_collection_templates(), AlgebraProfile::FreeMonoidScalarProfile => free_monoid_scalar_templates(), AlgebraProfile::FreeMonoidCollectionProfile => free_monoid_collection_templates(), AlgebraProfile::PartialFunctionProfile => partial_function_templates(), + AlgebraProfile::FinitelySupportedFunctionProfile => finitely_supported_function_templates(), } } @@ -1621,11 +1710,14 @@ pub fn algebra_type_param_names(profile: AlgebraProfile) -> Rc> { AlgebraProfile::OrderedRingProfile => Rc::new(vec![]), AlgebraProfile::ApproximateFieldProfile => Rc::new(vec![]), AlgebraProfile::BooleanAlgebraProfile => Rc::new(vec![]), - AlgebraProfile::BooleanAlgebraCollectionProfile => Rc::new(vec!["T".to_string()]), + AlgebraProfile::FinitePowerSetProfile => Rc::new(vec!["T".to_string()]), AlgebraProfile::PointwisePowerCollectionProfile => Rc::new(vec!["T".to_string()]), AlgebraProfile::FreeMonoidScalarProfile => Rc::new(vec![]), AlgebraProfile::FreeMonoidCollectionProfile => Rc::new(vec!["T".to_string()]), AlgebraProfile::PartialFunctionProfile => Rc::new(vec!["K".to_string(), "V".to_string()]), + AlgebraProfile::FinitelySupportedFunctionProfile => { + Rc::new(vec!["K".to_string(), "V".to_string()]) + } } } @@ -1634,11 +1726,12 @@ pub fn all_algebra_profiles() -> Rc> { AlgebraProfile::OrderedRingProfile, AlgebraProfile::ApproximateFieldProfile, AlgebraProfile::BooleanAlgebraProfile, - AlgebraProfile::BooleanAlgebraCollectionProfile, + AlgebraProfile::FinitePowerSetProfile, AlgebraProfile::PointwisePowerCollectionProfile, AlgebraProfile::FreeMonoidScalarProfile, AlgebraProfile::FreeMonoidCollectionProfile, AlgebraProfile::PartialFunctionProfile, + AlgebraProfile::FinitelySupportedFunctionProfile, ]) } @@ -1692,7 +1785,7 @@ pub struct ApproximateFieldProfile; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct BooleanAlgebraProfile; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] -pub struct BooleanAlgebraCollectionProfile; +pub struct FinitePowerSetProfile; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct PointwisePowerCollectionProfile; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] @@ -1702,6 +1795,8 @@ pub struct FreeMonoidCollectionProfile; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct PartialFunctionProfile; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct FinitelySupportedFunctionProfile; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct ShrinkEffect; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct ProjectionEffect; diff --git a/src/v1/stage0/src/std_computation.rs b/src/v1/stage0/src/std_computation.rs index c53c79e5312..746fc138977 100644 --- a/src/v1/stage0/src/std_computation.rs +++ b/src/v1/stage0/src/std_computation.rs @@ -9,9 +9,9 @@ use self::SizeBound::*; pub use crate::std_algebra::kernel_algebra_profile; pub use crate::std_algebra::AlgebraProfile; use crate::std_algebra::AlgebraProfile::{ - ApproximateFieldProfile, BooleanAlgebraCollectionProfile, BooleanAlgebraProfile, - FreeMonoidCollectionProfile, FreeMonoidScalarProfile, OrderedRingProfile, - PartialFunctionProfile, PointwisePowerCollectionProfile, + ApproximateFieldProfile, BooleanAlgebraProfile, FinitePowerSetProfile, + FinitelySupportedFunctionProfile, FreeMonoidCollectionProfile, FreeMonoidScalarProfile, + OrderedRingProfile, PartialFunctionProfile, PointwisePowerCollectionProfile, }; pub use crate::std_termination::positive_descent_count; use crate::std_termination::DescentEvidence::DescentUnknown; @@ -224,9 +224,12 @@ pub fn algebra_profile_to_dimension(profile: AlgebraProfile) -> Option Some(IterationDimension::CollectionFold), AlgebraProfile::FreeMonoidScalarProfile => Some(IterationDimension::CollectionFold), - AlgebraProfile::BooleanAlgebraCollectionProfile => Some(IterationDimension::CollectionFold), + AlgebraProfile::FinitePowerSetProfile => Some(IterationDimension::CollectionFold), + AlgebraProfile::FinitelySupportedFunctionProfile => { + Some(IterationDimension::CollectionFold) + } AlgebraProfile::PointwisePowerCollectionProfile => None, - AlgebraProfile::PartialFunctionProfile => Some(IterationDimension::CollectionFold), + AlgebraProfile::PartialFunctionProfile => None, AlgebraProfile::OrderedRingProfile => Some(IterationDimension::ArithmeticRepeat), AlgebraProfile::ApproximateFieldProfile => Some(IterationDimension::ArithmeticRepeat), AlgebraProfile::BooleanAlgebraProfile => None, diff --git a/src/v1/stage0/src/std_types.rs b/src/v1/stage0/src/std_types.rs index 1d767804ca4..e60310dae5c 100644 --- a/src/v1/stage0/src/std_types.rs +++ b/src/v1/stage0/src/std_types.rs @@ -8,7 +8,7 @@ use self::FermiDepth::*; use self::HttpMethod::*; use self::TopologyNodeKind::*; pub use crate::std_algebra::{algebra_type_param_names, kernel_algebra_profile}; -pub use crate::std_algebra::{FreeMonoid, PartialFunction, PointwisePower}; +pub use crate::std_algebra::{FinitePowerSet, FinitelySupportedFunction, FreeMonoid}; use crate::v1_rt; use crate::v1_rt::{VecCompat, VecJoin}; use crate::NonEmptyBTreeSet; @@ -139,14 +139,18 @@ pub fn container_template_algebra_rows() -> Rc> { let mut __m = HashMap::new(); __m.insert("List".to_string(), "FreeMonoid".to_string()); __m.insert("list".to_string(), "FreeMonoid".to_string()); - __m.insert("Set".to_string(), "PointwisePower".to_string()); - __m.insert("set".to_string(), "PointwisePower".to_string()); - __m.insert("Map".to_string(), "PartialFunction".to_string()); - __m.insert("map".to_string(), "PartialFunction".to_string()); + __m.insert("Set".to_string(), "FinitePowerSet".to_string()); + __m.insert("set".to_string(), "FinitePowerSet".to_string()); + __m.insert("Map".to_string(), "FinitelySupportedFunction".to_string()); + __m.insert("map".to_string(), "FinitelySupportedFunction".to_string()); __m.insert("FreeMonoid".to_string(), "FreeMonoid".to_string()); __m.insert("free_monoid".to_string(), "FreeMonoid".to_string()); __m.insert("BooleanAlgebra".to_string(), "BooleanAlgebra".to_string()); __m.insert("boolean_algebra".to_string(), "BooleanAlgebra".to_string()); + __m.insert("FinitePowerSet".to_string(), "FinitePowerSet".to_string()); + __m.insert("finite_power_set".to_string(), "FinitePowerSet".to_string()); + __m.insert("FinitelySupportedFunction".to_string(), "FinitelySupportedFunction".to_string()); + __m.insert("finitely_supported_function".to_string(), "FinitelySupportedFunction".to_string()); __m.insert("PartialFunction".to_string(), "PartialFunction".to_string()); __m.insert("partial_function".to_string(), "PartialFunction".to_string()); __m.insert("PointwisePower".to_string(), "PointwisePower".to_string()); @@ -163,10 +167,12 @@ pub fn container_template_alias_rows() -> Rc> { let mut __m = HashMap::new(); __m.insert("List".to_string(), "FreeMonoid".to_string()); __m.insert("list".to_string(), "FreeMonoid".to_string()); - __m.insert("Set".to_string(), "PointwisePower".to_string()); - __m.insert("set".to_string(), "PointwisePower".to_string()); - __m.insert("Map".to_string(), "PartialFunction".to_string()); - __m.insert("map".to_string(), "PartialFunction".to_string()); + __m.insert("Set".to_string(), "FinitePowerSet".to_string()); + __m.insert("set".to_string(), "FinitePowerSet".to_string()); + __m.insert("Map".to_string(), "FinitelySupportedFunction".to_string()); + __m.insert("map".to_string(), "FinitelySupportedFunction".to_string()); + __m.insert("PartialFunction".to_string(), "PartialFunction".to_string()); + __m.insert("partial_function".to_string(), "PartialFunction".to_string()); Rc::new(__m) }; } @@ -183,11 +189,13 @@ pub fn container_template_alias_algebra(name: String) -> Option { pub fn canonical_container_names() -> Rc> { Rc::new(vec![ - "BooleanAlgebra".to_string(), + "FinitePowerSet".to_string(), + "FinitelySupportedFunction".to_string(), "FreeMonoid".to_string(), "List".to_string(), "Map".to_string(), "PartialFunction".to_string(), + "PointwisePower".to_string(), "Set".to_string(), "Witness".to_string(), ]) @@ -219,9 +227,9 @@ pub type Char = i64; pub type List = Vec; -pub type Set = Rc>; +pub type Set = Rc>; -pub type Map = Rc>; +pub type Map = Rc>; pub fn list_length(items: Rc>) -> i64 { items.iter().fold(0, |acc: i64, _: _| (acc + 1)) diff --git a/src/v1/stage0/src/v1_compiler_coercion.rs b/src/v1/stage0/src/v1_compiler_coercion.rs index f31fe653ced..353d80a3ac0 100644 --- a/src/v1/stage0/src/v1_compiler_coercion.rs +++ b/src/v1/stage0/src/v1_compiler_coercion.rs @@ -456,10 +456,7 @@ pub fn checkpoint_tests(target: RenderTarget) -> Rc>> } pub fn inhabitant_test_names() -> Rc> { - v1_rt::concat( - canonical_container_names(), - Rc::new(vec!["PointwisePower".to_string()]), - ) + canonical_container_names() } pub fn inhabitant_tests(target: RenderTarget) -> Rc>> { diff --git a/src/v1/stage0/src/v1_compiler_emit_rust.rs b/src/v1/stage0/src/v1_compiler_emit_rust.rs index b71ce441aed..39713cad30b 100644 --- a/src/v1/stage0/src/v1_compiler_emit_rust.rs +++ b/src/v1/stage0/src/v1_compiler_emit_rust.rs @@ -12066,10 +12066,24 @@ pub fn emit_faithful_text_carrier_import_lines( let needs_partial_function = { let mut __found = false; for item in items.iter().cloned() { - if (module_item_references_type_name( + if module_item_references_type_name( item.clone(), "PartialFunction".to_string(), source_indices.clone(), + ) { + __found = true; + break; + } + } + __found + }; + let needs_finitely_supported_function = { + let mut __found = false; + for item in items.iter().cloned() { + if (module_item_references_type_name( + item.clone(), + "FinitelySupportedFunction".to_string(), + source_indices.clone(), ) || module_item_references_type_name( item.clone(), "Map".to_string(), @@ -12163,6 +12177,19 @@ pub fn emit_faithful_text_carrier_import_lines( "use crate::std_algebra::PartialFunction;".to_string(), )]) }; + let finitely_supported_function = if (!needs_finitely_supported_function.clone() + || rust_import_name_already_resolved( + imported_names.clone(), + local_type_names.clone(), + "FinitelySupportedFunction".to_string(), + )) { + Rc::new(vec![]) + } else { + Rc::new(vec![v1_rt::concat( + rust_visibility_prefix(), + "use crate::std_algebra::FinitelySupportedFunction;".to_string(), + )]) + }; let memory = if (!needs_measure_phantoms.clone() || rust_import_name_already_resolved( imported_names.clone(), @@ -12194,12 +12221,15 @@ pub fn emit_faithful_text_carrier_import_lines( v1_rt::concat( v1_rt::concat( v1_rt::concat( - v1_rt::concat(free_monoid.clone(), char_line.clone()), - non_empty_str.clone(), + v1_rt::concat( + v1_rt::concat(free_monoid.clone(), char_line.clone()), + non_empty_str.clone(), + ), + int_line.clone(), ), - int_line.clone(), + partial_function.clone(), ), - partial_function.clone(), + finitely_supported_function.clone(), ), memory.clone(), ), diff --git a/src/v1/stage0/src/v1_compiler_infer_types.rs b/src/v1/stage0/src/v1_compiler_infer_types.rs index 01d0dfa7c07..4906512027c 100644 --- a/src/v1/stage0/src/v1_compiler_infer_types.rs +++ b/src/v1/stage0/src/v1_compiler_infer_types.rs @@ -3,9 +3,9 @@ use self::TypeResolutionVerdict::*; use crate::std_algebra::AlgebraProfile::{ - ApproximateFieldProfile, BooleanAlgebraCollectionProfile, BooleanAlgebraProfile, - FreeMonoidCollectionProfile, FreeMonoidScalarProfile, OrderedRingProfile, - PartialFunctionProfile, + ApproximateFieldProfile, BooleanAlgebraProfile, FinitePowerSetProfile, + FinitelySupportedFunctionProfile, FreeMonoidCollectionProfile, FreeMonoidScalarProfile, + OrderedRingProfile, PartialFunctionProfile, }; use crate::std_algebra::AlgebraTypeTemplate::{ AlgebraTypeVariable, ContainerOf, NamedTemplate, OptionalOf, ReceiverElement, ReceiverKey, diff --git a/src/v1/stage0/src/v1_compiler_trait_derive_emit.rs b/src/v1/stage0/src/v1_compiler_trait_derive_emit.rs index f24763137a8..019388d078a 100644 --- a/src/v1/stage0/src/v1_compiler_trait_derive_emit.rs +++ b/src/v1/stage0/src/v1_compiler_trait_derive_emit.rs @@ -265,7 +265,9 @@ pub fn v1_keyed_map_verdict_from_algebra( ) -> Rc { match container_template_algebra(authored_name_at(source_indices.clone(), type_expr.clone())) { Some(algebra) => { - if (algebra.clone() == "PartialFunction".to_string()) { + if ((algebra.clone() == "FinitelySupportedFunction".to_string()) + || (algebra.clone() == "PartialFunction".to_string())) + { Rc::new(KeyedMapVerdict::KeyedMap) } else { Rc::new(KeyedMapVerdict::NotKeyedMap) diff --git a/src/v1/trait_derive_emit.dag b/src/v1/trait_derive_emit.dag index 50fe6bd427a..4c22d6d8f9a 100644 --- a/src/v1/trait_derive_emit.dag +++ b/src/v1/trait_derive_emit.dag @@ -150,7 +150,7 @@ fn v1_repr_grounding_derive_elem_shape_for_ord_carrier( // ever produce — and std.trait_derive_shape could not even name Hash until this landed, which is why // the gap was structural rather than an oversight in the table. The requirement is one row, // map_key_required_derive_traits, grounded on im 15.1.0 HashMap declaring K: Hash + Eq (the -// container Map lowers to, via std.types container_template_algebra PartialFunction). +// container Map lowers to, via std.types container_template_algebra FinitelySupportedFunction). // v1_map_key_required_type_names computes the subject population as a LEAST FIXPOINT over the // declared-type graph, the same shape as the Clone-bound fixpoint above and for the same reason: // derive(Hash) on a record emits an impl requiring every FIELD type to be Hash, so a required type @@ -203,9 +203,18 @@ fn v1_type_expr_keyed_map_verdict(type_expr: Node, source_indices: Map` and therefore actually imposes `K: Hash + Eq`. Testing +// the old name alone would classify every `Map` field NotKeyedMap and drop the key derives that +// `map_key_required_derive_traits` exists to add -- a silent loss of a required bound, not a +// diagnostic. `PartialFunction` stays in the test because a declaration may now name the open +// carrier directly, and a keyed lookup is what both carriers are for. fn v1_keyed_map_verdict_from_algebra(type_expr: Node, source_indices: Map) -> KeyedMapVerdict { match container_template_algebra(name: authored_name_at(source_indices: source_indices, node: type_expr)) { - Present { value: algebra } => if algebra == "PartialFunction" { KeyedMap } else { NotKeyedMap } + Present { value: algebra } => + if algebra == "FinitelySupportedFunction" || algebra == "PartialFunction" { KeyedMap } else { NotKeyedMap } Absent => NotKeyedMap } } diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 18360abeecb..69c0beecc15 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -175,7 +175,7 @@ data infer_emit_shape_frontier_note: String = "Test-only emit-shape frontier (re fn infer_emit_shape_frontier_inferred_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: fn(_key) { Absent } @@ -486,7 +486,7 @@ fn lookup_inferred_facts_in_entries( ) } -fn facts_map_from_entries(entries: List) -> Outcome> { +fn facts_map_from_entries(entries: List) -> Outcome> { match fold(entries, init: Accepted { value: empty_inferred_facts_entry_list(), diagnostics: None }, f: fn(acc, entry) { match acc { Rejected { diagnostics: r } => Rejected { diagnostics: r } @@ -505,7 +505,7 @@ fn facts_map_from_entries(entries: List) -> Outcome Rejected { diagnostics: r } Accepted { value: admitted, diagnostics: d } => Accepted { - value: Map { + value: PartialFunction { lookup: fn(key) { lookup_inferred_facts_in_entries(entries: admitted, key: key) } diff --git a/src/v2/compiler/05_emit_orchestration.dag b/src/v2/compiler/05_emit_orchestration.dag index 73aff4995e8..a7a01a2d1a3 100644 --- a/src/v2/compiler/05_emit_orchestration.dag +++ b/src/v2/compiler/05_emit_orchestration.dag @@ -161,7 +161,7 @@ fn orch_emit_from_registry( emit( tree: InferredTree { root: emitted_root, - facts: Map { lookup: orch_emit_facts_lookup } + facts: PartialFunction { lookup: orch_emit_facts_lookup } }, target: target ) @@ -174,7 +174,7 @@ fn orch_emit_node_spelling(emitted_root: Node, target: TargetModel) -> Outcome Optional Map { - Map { +fn empty_runtime_bindings() -> PartialFunction { + PartialFunction { lookup: runtime_binding_lookup_miss } } diff --git a/src/v2/compiler/inferred_tree.dag b/src/v2/compiler/inferred_tree.dag index 0e20caefc06..d812e1477cb 100644 --- a/src/v2/compiler/inferred_tree.dag +++ b/src/v2/compiler/inferred_tree.dag @@ -31,7 +31,7 @@ type InferredFacts { type InferredTree { root: Node - facts: Map + facts: PartialFunction } type InferredFactsEntry { diff --git a/src/v2/compiler/program_partition.dag b/src/v2/compiler/program_partition.dag index ac7d5cb8c40..58501cadf66 100644 --- a/src/v2/compiler/program_partition.dag +++ b/src/v2/compiler/program_partition.dag @@ -468,7 +468,7 @@ fn facts_closure_entries_fold( ) } -fn facts_closure_fold(partition: ProgramPartition) -> Outcome> { +fn facts_closure_fold(partition: ProgramPartition) -> Outcome> { match partition.boundary { AmbientContextAvailable => outcome_accepted(value: partition.ambient.facts) diff --git a/src/v2/compiler/self_host/direct_rust_door_fixture.dag b/src/v2/compiler/self_host/direct_rust_door_fixture.dag index 6dbe6b092dd..4400ec68449 100644 --- a/src/v2/compiler/self_host/direct_rust_door_fixture.dag +++ b/src/v2/compiler/self_host/direct_rust_door_fixture.dag @@ -262,7 +262,7 @@ fn direct_rust_door_facts_lookup(key: Node) -> Optional { data direct_rust_door_inferred_tree: InferredTree = InferredTree { root: rust_fixture_emitted_add_fn, - facts: Map { + facts: PartialFunction { lookup: direct_rust_door_facts_lookup } } diff --git a/src/v2/extdeps/formats/sql.dag b/src/v2/extdeps/formats/sql.dag index 9a34cddf87b..83c989f8c48 100644 --- a/src/v2/extdeps/formats/sql.dag +++ b/src/v2/extdeps/formats/sql.dag @@ -6,7 +6,9 @@ import std.algebra { Cons, Empty } import v2.std.algebra { fold_list, list_append, list_snoc_item } import v2.std.collection { List, - Map + Map, + empty_map, + map_insert } import v2.std.optional { Absent, @@ -261,43 +263,35 @@ fn sql_nonnumeric_facts_node(facts: SqlNonNumericPrimitiveFacts) -> Node { } fn sql_integer_spec_facts(facts: SqlIntegerPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: sql_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: sql_inhabitant_atom(id: ^sql_tag_signed) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + sql_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisSignedness {}), + sql_inhabitant_atom(id: ^sql_tag_signed) + ) } fn sql_float_spec_facts(facts: SqlFloatPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: sql_inhabitant_atom(id: facts.surface_spelling) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + sql_inhabitant_atom(id: facts.surface_spelling) + ) } fn sql_nonnumeric_spec_facts(facts: SqlNonNumericPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: sql_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: sql_inhabitant_atom(id: facts.representation) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + sql_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + sql_inhabitant_atom(id: facts.representation) + ) } fn sql_primitive_bundle_from_integer_facts(facts: SqlIntegerPrimitiveFacts) -> PrimitiveFactBundle { diff --git a/src/v2/extdeps/languages/cpp.dag b/src/v2/extdeps/languages/cpp.dag index 063147f0a58..004fd60e0a0 100644 --- a/src/v2/extdeps/languages/cpp.dag +++ b/src/v2/extdeps/languages/cpp.dag @@ -593,55 +593,59 @@ fn cpp_language_model_canonical_symbols(target_profile: Node) -> PointwisePower< } fn cpp_integer_spec_facts(facts: CppIntegerPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: cpp_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: facts.width_fact } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: facts.signedness_fact } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: facts.encoding_fact } - } else if axis == discriminant(v: ModelCoreFactAxisOverflowDisposition {}) { - v2.std.optional.Present { value: facts.overflow_fact } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + cpp_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + facts.width_fact + ), + discriminant(v: ModelCoreFactAxisSignedness {}), + facts.signedness_fact + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + facts.encoding_fact + ), + discriminant(v: ModelCoreFactAxisOverflowDisposition {}), + facts.overflow_fact + ) } fn cpp_character_spec_facts(facts: CppCharacterPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: cpp_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: facts.width_fact } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: facts.signedness_fact } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: facts.encoding_fact } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + cpp_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + facts.width_fact + ), + discriminant(v: ModelCoreFactAxisSignedness {}), + facts.signedness_fact + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + facts.encoding_fact + ) } fn cpp_bool_spec_facts(facts: CppBoolPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: cpp_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: facts.encoding_fact } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + cpp_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + facts.encoding_fact + ) } fn cpp_primitive_bundle_from_integer_facts(facts: CppIntegerPrimitiveFacts) -> PrimitiveFactBundle { diff --git a/src/v2/extdeps/languages/ecmascript.dag b/src/v2/extdeps/languages/ecmascript.dag index 59710250f57..4574855e8e9 100644 --- a/src/v2/extdeps/languages/ecmascript.dag +++ b/src/v2/extdeps/languages/ecmascript.dag @@ -270,17 +270,15 @@ fn ecmascript_primitive_spec_facts( surface_spelling: Symbol, encoding_value: Symbol ) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: ecmascript_inhabitant_atom(id: surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: ecmascript_inhabitant_atom(id: encoding_value) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + ecmascript_inhabitant_atom(id: surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + ecmascript_inhabitant_atom(id: encoding_value) + ) } fn ecmascript_primitive_algebra_witness_node( diff --git a/src/v2/extdeps/languages/go.dag b/src/v2/extdeps/languages/go.dag index b5c9abb5c25..707b64d5313 100644 --- a/src/v2/extdeps/languages/go.dag +++ b/src/v2/extdeps/languages/go.dag @@ -633,11 +633,7 @@ fn go_string_facts_node(facts: GoStringPrimitiveFacts) -> Node { } fn go_empty_primitive_spec_facts() -> Map { - Map { - lookup: fn(axis) { - v2.std.optional.Absent - } - } + empty_map() } fn go_primitive_fact_map_2( diff --git a/src/v2/extdeps/languages/java.dag b/src/v2/extdeps/languages/java.dag index 5a33a634d3b..59631b26208 100644 --- a/src/v2/extdeps/languages/java.dag +++ b/src/v2/extdeps/languages/java.dag @@ -1602,51 +1602,51 @@ fn java_language_model_canonical_symbols() -> PointwisePower { } fn java_integer_spec_facts(facts: JavaIntegerPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: java_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: java_int_width_node(width: facts.width) } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: java_int_kind_node(kind: facts.signedness) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: java_integer_encoding_fact(facts: facts) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + java_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + java_int_width_node(width: facts.width) + ), + discriminant(v: ModelCoreFactAxisSignedness {}), + java_int_kind_node(kind: facts.signedness) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + java_integer_encoding_fact(facts: facts) + ) } fn java_float_spec_facts(facts: JavaFloatPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: java_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: java_float_width_node(width: facts.width) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: java_inhabitant_atom(id: facts.ieee754_binary) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + java_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + java_float_width_node(width: facts.width) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + java_inhabitant_atom(id: facts.ieee754_binary) + ) } fn java_noninteger_spec_facts(facts: JavaNonIntegerPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: java_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: java_inhabitant_atom(id: facts.representation) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + java_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + java_inhabitant_atom(id: facts.representation) + ) } fn java_primitive_bundle_from_integer_facts(facts: JavaIntegerPrimitiveFacts) -> PrimitiveFactBundle { diff --git a/src/v2/extdeps/languages/kotlin.dag b/src/v2/extdeps/languages/kotlin.dag index 9e1062c2979..cb9a6d44f05 100644 --- a/src/v2/extdeps/languages/kotlin.dag +++ b/src/v2/extdeps/languages/kotlin.dag @@ -555,67 +555,71 @@ fn kotlin_nonnumeric_value_fact_node(value_fact: KotlinNonNumericValueFact) -> N } fn kotlin_integer_spec_facts(facts: KotlinIntegerPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: kotlin_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: kotlin_int_width_node(width: facts.width) } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: kotlin_atom(id: ^kotlin_tag_signed) } - } else if axis == discriminant(v: ModelCoreFactAxisOverflowDisposition {}) { - v2.std.optional.Present { value: kotlin_overflow_node(overflow: facts.overflow) } - } else if axis == ^kotlin_primitive_fact_axis_runtime_representation { - v2.std.optional.Present { value: kotlin_runtime_representation_node(representation: facts.representation) } - } else if axis == ^kotlin_primitive_fact_axis_scalar_classifier { - v2.std.optional.Present { value: kotlin_scalar_node(scalar: IntScalar { width: facts.width }) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + kotlin_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + kotlin_int_width_node(width: facts.width) + ), + discriminant(v: ModelCoreFactAxisSignedness {}), + kotlin_atom(id: ^kotlin_tag_signed) + ), + discriminant(v: ModelCoreFactAxisOverflowDisposition {}), + kotlin_overflow_node(overflow: facts.overflow) + ), + ^kotlin_primitive_fact_axis_runtime_representation, + kotlin_runtime_representation_node(representation: facts.representation) + ), + ^kotlin_primitive_fact_axis_scalar_classifier, + kotlin_scalar_node(scalar: IntScalar { width: facts.width }) + ) } fn kotlin_float_spec_facts(facts: KotlinFloatPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: kotlin_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: kotlin_float_width_node(width: facts.width) } - } else if axis == ^kotlin_primitive_fact_axis_value_format { - v2.std.optional.Present { value: kotlin_float_value_format_node(value_format: facts.value_format) } - } else if axis == ^kotlin_primitive_fact_axis_runtime_representation { - v2.std.optional.Present { value: kotlin_runtime_representation_node(representation: facts.representation) } - } else if axis == ^kotlin_primitive_fact_axis_scalar_classifier { - v2.std.optional.Present { value: kotlin_scalar_node(scalar: FloatScalar { width: facts.width }) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + kotlin_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + kotlin_float_width_node(width: facts.width) + ), + ^kotlin_primitive_fact_axis_value_format, + kotlin_float_value_format_node(value_format: facts.value_format) + ), + ^kotlin_primitive_fact_axis_runtime_representation, + kotlin_runtime_representation_node(representation: facts.representation) + ), + ^kotlin_primitive_fact_axis_scalar_classifier, + kotlin_scalar_node(scalar: FloatScalar { width: facts.width }) + ) } fn kotlin_nonnumeric_spec_facts(facts: KotlinNonNumericPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: kotlin_atom(id: facts.surface_spelling) } - } else { - if axis == kotlin_nonnumeric_value_fact_axis(value_fact: facts.value_fact) { - v2.std.optional.Present { - value: kotlin_nonnumeric_value_fact_node(value_fact: facts.value_fact) - } - } else { - if axis == ^kotlin_primitive_fact_axis_scalar_classifier { - v2.std.optional.Present { value: kotlin_scalar_node(scalar: facts.scalar) } - } else { - v2.std.optional.Absent - } - } - } - } - } + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + kotlin_atom(id: facts.surface_spelling) + ), + kotlin_nonnumeric_value_fact_axis(value_fact: facts.value_fact), + kotlin_nonnumeric_value_fact_node(value_fact: facts.value_fact) + ), + ^kotlin_primitive_fact_axis_scalar_classifier, + kotlin_scalar_node(scalar: facts.scalar) + ) } fn kotlin_primitive_bundle_from_integer_facts( diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 77d6423f950..8a34c6795cc 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, PointwisePower, Present } +import v2.std.collection { Absent, List, Map, Optional, PointwisePower, Present, empty_map, map_insert } 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 } @@ -617,65 +617,63 @@ fn lean_fixed_int_spec_facts( width: LeanIntegerWidth, overflow: LeanAdmittedOverflowSemantics ) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: lean_integer_width_node(width: width) } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: lean_signedness_node(signedness: signedness) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.representation) } - } else if axis == discriminant(v: ModelCoreFactAxisOverflowDisposition {}) { - v2.std.optional.Present { value: lean_overflow_semantics_node(semantics: overflow.semantics) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + lean_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + lean_integer_width_node(width: width) + ), + discriminant(v: ModelCoreFactAxisSignedness {}), + lean_signedness_node(signedness: signedness) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + lean_inhabitant_atom(id: facts.representation) + ), + discriminant(v: ModelCoreFactAxisOverflowDisposition {}), + lean_overflow_semantics_node(semantics: overflow.semantics) + ) } fn lean_bool_spec_facts(facts: LeanPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.representation) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + lean_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + lean_inhabitant_atom(id: facts.representation) + ) } fn lean_width_admission_refused_spec_facts(facts: LeanPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.representation) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + lean_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + lean_inhabitant_atom(id: facts.representation) + ) } fn lean_overflow_admission_refused_spec_facts(facts: LeanPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: lean_inhabitant_atom(id: facts.representation) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + lean_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + lean_inhabitant_atom(id: facts.representation) + ) } fn lean_primitive_bundle_from_facts(facts: LeanPrimitiveFacts) -> PrimitiveFactBundle { diff --git a/src/v2/extdeps/languages/llvm_ir.dag b/src/v2/extdeps/languages/llvm_ir.dag index 8e72cc6e6e7..a7f42f5a54f 100644 --- a/src/v2/extdeps/languages/llvm_ir.dag +++ b/src/v2/extdeps/languages/llvm_ir.dag @@ -39,7 +39,7 @@ import v2.std.compilers.lexing { import std.algebra { Empty } import v2.std.algebra { fold_list, list_append, list_snoc_item } import v2.std.cardinality { NonZeroNat } -import v2.std.collection { Absent, List, Map, Present } +import v2.std.collection { Absent, List, Map, Present, empty_map, map_insert } import v2.std.model_core { EffectSemanticsDecl, ModelCore, @@ -657,33 +657,31 @@ fn llvm_float_facts_node(facts: LlvmFloatPrimitiveFacts) -> Node { } fn llvm_integer_spec_facts(facts: LlvmIntegerPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: llvm_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: llvm_integer_bits_node(bits: facts.bits) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: llvm_inhabitant_atom(id: ^llvm_repr_sign_agnostic_integer) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + llvm_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + llvm_integer_bits_node(bits: facts.bits) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + llvm_inhabitant_atom(id: ^llvm_repr_sign_agnostic_integer) + ) } fn llvm_float_spec_facts(facts: LlvmFloatPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: llvm_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: llvm_float_kind_node(kind: facts.kind) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + llvm_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + llvm_float_kind_node(kind: facts.kind) + ) } fn llvm_primitive_bundle_from_integer_facts(facts: LlvmIntegerPrimitiveFacts) -> PrimitiveFactBundle { diff --git a/src/v2/extdeps/languages/machine_code.dag b/src/v2/extdeps/languages/machine_code.dag index 68c74872de4..9c5e3ce5501 100644 --- a/src/v2/extdeps/languages/machine_code.dag +++ b/src/v2/extdeps/languages/machine_code.dag @@ -18,7 +18,7 @@ import v2.std.compilers.lexing { } import std.algebra { Empty } import v2.std.algebra { list_map } -import v2.std.collection { Absent, List, Map, Present } +import v2.std.collection { Absent, List, Map, Present, empty_map, map_insert } import v2.std.machine { Byte } import v2.std.text { String } import v2.std.model_core { @@ -372,23 +372,27 @@ fn mc_integer_facts_node(facts: MachineIntegerPrimitiveFacts) -> Node { } fn mc_integer_spec_facts(facts: MachineIntegerPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: mc_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: mc_int_width_node(width: facts.width) } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: mc_int_kind_node(kind: facts.kind) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: mc_inhabitant_atom(id: ^mc_repr_twos_complement) } - } else if axis == discriminant(v: ModelCoreFactAxisOverflowDisposition {}) { - v2.std.optional.Present { value: mc_overflow_node(overflow: facts.overflow_release) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + mc_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + mc_int_width_node(width: facts.width) + ), + discriminant(v: ModelCoreFactAxisSignedness {}), + mc_int_kind_node(kind: facts.kind) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + mc_inhabitant_atom(id: ^mc_repr_twos_complement) + ), + discriminant(v: ModelCoreFactAxisOverflowDisposition {}), + mc_overflow_node(overflow: facts.overflow_release) + ) } fn mc_primitive_bundle_from_integer_facts(facts: MachineIntegerPrimitiveFacts) -> PrimitiveFactBundle { diff --git a/src/v2/extdeps/languages/swift.dag b/src/v2/extdeps/languages/swift.dag index 5af6f790f0b..8a41e6214f0 100644 --- a/src/v2/extdeps/languages/swift.dag +++ b/src/v2/extdeps/languages/swift.dag @@ -1621,11 +1621,7 @@ fn swift_lex_token_symbol(sym: Symbol) -> Bool { } fn swift_empty_primitive_spec_facts() -> Map { - Map { - lookup: fn(axis) { - v2.std.optional.Absent - } - } + empty_map() } fn swift_primitive_fact_map_4( diff --git a/src/v2/extdeps/languages/typescript.dag b/src/v2/extdeps/languages/typescript.dag index 5f3e3c17f57..4ac715bbdc5 100644 --- a/src/v2/extdeps/languages/typescript.dag +++ b/src/v2/extdeps/languages/typescript.dag @@ -2159,47 +2159,43 @@ fn ts_language_model_canonical_symbols() -> PointwisePower { } fn ts_number_spec_facts(facts: TsNumberPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: ts_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: ts_inhabitant_atom(id: ^ts_tag_bits64) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: ts_inhabitant_atom(id: facts.ieee754_binary) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + ts_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + ts_inhabitant_atom(id: ^ts_tag_bits64) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + ts_inhabitant_atom(id: facts.ieee754_binary) + ) } fn ts_bigint_spec_facts(facts: TsBigIntPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: ts_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: ts_inhabitant_atom(id: facts.encoding) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + ts_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + ts_inhabitant_atom(id: facts.encoding) + ) } fn ts_bool_spec_facts(facts: TsBooleanPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: ts_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: ts_inhabitant_atom(id: facts.encoding) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + ts_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + ts_inhabitant_atom(id: facts.encoding) + ) } fn ts_primitive_bundle_from_number_facts(facts: TsNumberPrimitiveFacts) -> PrimitiveFactBundle { diff --git a/src/v2/extdeps/languages/wasm.dag b/src/v2/extdeps/languages/wasm.dag index 0d35daa1239..22069324cec 100644 --- a/src/v2/extdeps/languages/wasm.dag +++ b/src/v2/extdeps/languages/wasm.dag @@ -1595,39 +1595,43 @@ fn wasm_language_model_canonical_symbols() -> PointwisePower { } fn wasm_integer_spec_facts(facts: WasmIntegerPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: wasm_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: wasm_int_width_node(width: facts.width) } - } else if axis == discriminant(v: ModelCoreFactAxisSignedness {}) { - v2.std.optional.Present { value: wasm_inhabitant_atom(id: ^wasm_tag_sign_agnostic_modular) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: wasm_inhabitant_atom(id: ^wasm_repr_sign_agnostic_modular) } - } else if axis == discriminant(v: ModelCoreFactAxisOverflowDisposition {}) { - v2.std.optional.Present { value: wasm_inhabitant_atom(id: ^wasm_tag_modular_wrap) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + wasm_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + wasm_int_width_node(width: facts.width) + ), + discriminant(v: ModelCoreFactAxisSignedness {}), + wasm_inhabitant_atom(id: ^wasm_tag_sign_agnostic_modular) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + wasm_inhabitant_atom(id: ^wasm_repr_sign_agnostic_modular) + ), + discriminant(v: ModelCoreFactAxisOverflowDisposition {}), + wasm_inhabitant_atom(id: ^wasm_tag_modular_wrap) + ) } fn wasm_float_spec_facts(facts: WasmFloatPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - if axis == discriminant(v: ModelCoreFactAxisSurfaceSpelling {}) { - v2.std.optional.Present { value: wasm_inhabitant_atom(id: facts.surface_spelling) } - } else if axis == discriminant(v: ModelCoreFactAxisWidth {}) { - v2.std.optional.Present { value: wasm_float_width_node(width: facts.width) } - } else if axis == discriminant(v: ModelCoreFactAxisEncoding {}) { - v2.std.optional.Present { value: wasm_inhabitant_atom(id: facts.ieee754_binary) } - } else { - v2.std.optional.Absent - } - } - } + map_insert( + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisSurfaceSpelling {}), + wasm_inhabitant_atom(id: facts.surface_spelling) + ), + discriminant(v: ModelCoreFactAxisWidth {}), + wasm_float_width_node(width: facts.width) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + wasm_inhabitant_atom(id: facts.ieee754_binary) + ) } fn wasm_primitive_bundle_from_integer_facts(facts: WasmIntegerPrimitiveFacts) -> PrimitiveFactBundle { diff --git a/src/v2/extdeps/runtimes/v2_effect_io_pure.dag b/src/v2/extdeps/runtimes/v2_effect_io_pure.dag index a23971cbd3c..b3adaa88c3e 100644 --- a/src/v2/extdeps/runtimes/v2_effect_io_pure.dag +++ b/src/v2/extdeps/runtimes/v2_effect_io_pure.dag @@ -2,10 +2,10 @@ module v2.extdeps.runtimes.v2_effect_io_pure import std.algebra { Cons, Empty } import v2.std.collection { + Absent, List, Map, Present, - Absent, empty_map, list_nth, map_get, @@ -107,7 +107,7 @@ fn effect_io_pure_operation_ref() -> PrimitiveOperationRef { fn effect_io_pure_empty_environment() -> EvaluationEnvironment { EvaluationEnvironment { - bindings: Map { + bindings: PartialFunction { lookup: fn(_) { Absent } diff --git a/src/v2/extdeps/runtimes/v2_evaluator.dag b/src/v2/extdeps/runtimes/v2_evaluator.dag index a204e6783f7..2567f1f6a7f 100644 --- a/src/v2/extdeps/runtimes/v2_evaluator.dag +++ b/src/v2/extdeps/runtimes/v2_evaluator.dag @@ -171,8 +171,8 @@ fn v2_eval_binding_lookup_miss(_key: EnvironmentBindingKey) -> Witness Map { - Map { +fn v2_eval_empty_bindings() -> PartialFunction { + PartialFunction { lookup: v2_eval_binding_lookup_miss } } diff --git a/src/v2/lens/common/infer_fixture.dag b/src/v2/lens/common/infer_fixture.dag index f27eecf4fb7..5ede1b0aead 100644 --- a/src/v2/lens/common/infer_fixture.dag +++ b/src/v2/lens/common/infer_fixture.dag @@ -92,8 +92,8 @@ fn claim_inferred_facts( ) } -fn claim_inferred_facts_map(facts: InferredFacts) -> Map { - Map { +fn claim_inferred_facts_map(facts: InferredFacts) -> PartialFunction { + PartialFunction { lookup: fn(_) { Present { value: facts } } diff --git a/src/v2/lens/structural_resolution/binds_to_resolved_test.dag b/src/v2/lens/structural_resolution/binds_to_resolved_test.dag index cc8b581fd29..52fb1743181 100644 --- a/src/v2/lens/structural_resolution/binds_to_resolved_test.dag +++ b/src/v2/lens/structural_resolution/binds_to_resolved_test.dag @@ -38,8 +38,8 @@ fn sr_claim_facts() -> InferredFacts { ) } -fn sr_claim_fact_map(facts: InferredFacts) -> Map { - Map { +fn sr_claim_fact_map(facts: InferredFacts) -> PartialFunction { + PartialFunction { lookup: fn(_) { Present { value: facts } } diff --git a/src/v2/lens/structural_resolution/facts_lookup_miss.dag b/src/v2/lens/structural_resolution/facts_lookup_miss.dag index 752cc585628..b4e00501ac1 100644 --- a/src/v2/lens/structural_resolution/facts_lookup_miss.dag +++ b/src/v2/lens/structural_resolution/facts_lookup_miss.dag @@ -42,9 +42,9 @@ fn sr_lookup_usage_site_witness() -> Optional { optional_absent() } -fn sr_lookup_claim_fact_map() -> Map { +fn sr_lookup_claim_fact_map() -> PartialFunction { let resolved = sr_lookup_resolved_facts() - Map { + PartialFunction { lookup: fn(key) { if key == sr_lookup_use { optional_absent() diff --git a/src/v2/lens/structural_resolution/module_import_out_of_scope.dag b/src/v2/lens/structural_resolution/module_import_out_of_scope.dag index 2c26a662740..a6ab37eb5ec 100644 --- a/src/v2/lens/structural_resolution/module_import_out_of_scope.dag +++ b/src/v2/lens/structural_resolution/module_import_out_of_scope.dag @@ -48,8 +48,8 @@ fn sr_mod_claim_facts() -> InferredFacts { ) } -fn sr_mod_claim_fact_map(facts: InferredFacts) -> Map { - Map { +fn sr_mod_claim_fact_map(facts: InferredFacts) -> PartialFunction { + PartialFunction { lookup: fn(_) { Present { value: facts } } diff --git a/src/v2/lens/structural_resolution/unbound_symbol_at_use.dag b/src/v2/lens/structural_resolution/unbound_symbol_at_use.dag index f50d63bc1d9..8aa98c60151 100644 --- a/src/v2/lens/structural_resolution/unbound_symbol_at_use.dag +++ b/src/v2/lens/structural_resolution/unbound_symbol_at_use.dag @@ -54,9 +54,9 @@ fn sr_unbound_usage_site_witness() -> Optional { optional_absent() } -fn sr_unbound_claim_fact_map() -> Map { +fn sr_unbound_claim_fact_map() -> PartialFunction { let resolved = sr_unbound_resolved_facts() - Map { + PartialFunction { lookup: fn(key) { if key == sr_unbound_use { optional_absent() diff --git a/src/v2/lens/structural_resolution/unresolved_infer_witness.dag b/src/v2/lens/structural_resolution/unresolved_infer_witness.dag index 34be3f90906..5dd08007e95 100644 --- a/src/v2/lens/structural_resolution/unresolved_infer_witness.dag +++ b/src/v2/lens/structural_resolution/unresolved_infer_witness.dag @@ -42,9 +42,9 @@ fn sr_infer_usage_site_witness() -> Optional { optional_absent() } -fn sr_infer_claim_fact_map() -> Map { +fn sr_infer_claim_fact_map() -> PartialFunction { let resolved = sr_infer_resolved_facts() - Map { + PartialFunction { lookup: fn(key) { if key == sr_infer_use { optional_absent() diff --git a/src/v2/program.dag b/src/v2/program.dag index fccb5d21607..2917e1e783f 100644 --- a/src/v2/program.dag +++ b/src/v2/program.dag @@ -362,7 +362,7 @@ fn program_facts_lookup(node: Node) -> Optional { fn program_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: program_facts_lookup } + facts: PartialFunction { lookup: program_facts_lookup } } } @@ -400,7 +400,7 @@ fn program_pick_if_arrow_facts_lookup(node: Node) -> Optional { fn program_pick_if_arrow_tree(callee: Node) -> InferredTree { InferredTree { root: callee, - facts: Map { lookup: program_pick_if_arrow_facts_lookup } + facts: PartialFunction { lookup: program_pick_if_arrow_facts_lookup } } } diff --git a/src/v2/std/collection.dag b/src/v2/std/collection.dag index e7b48d72334..7e3979716c0 100644 --- a/src/v2/std/collection.dag +++ b/src/v2/std/collection.dag @@ -126,9 +126,4 @@ type FiniteSet { head: T tail: List } -type TotalMap { - lookup: fn(K) -> V -} -type TotalPolicy { - lookup: fn(K, Context) -> RowTemplate -} + diff --git a/src/v2/std/model_core.dag b/src/v2/std/model_core.dag index 4bcad6e917a..2f57b839dcd 100644 --- a/src/v2/std/model_core.dag +++ b/src/v2/std/model_core.dag @@ -1,6 +1,6 @@ module v2.std.model_core -import v2.std.collection { Absent, List, Map, Present } +import v2.std.collection { Absent, List, Map, Present, empty_map, map_insert } import v2.std.diagnostic { Diagnostic, Textual, @@ -148,14 +148,15 @@ fn model_core_bool_fact_lookup(facts: BoolPrimitiveFacts, axis: Symbol) -> Witne } fn model_core_bool_spec_facts(facts: BoolPrimitiveFacts) -> Map { - Map { - lookup: fn(axis) { - match model_core_bool_fact_lookup(facts: facts, axis: axis) { - Holds { value: v } => Present { value: v } - Violates { diagnostic: _ } => Absent - } - } - } + map_insert( + map_insert( + empty_map(), + discriminant(v: ModelCoreFactAxisWidth {}), + bool_width_fact_node(width: facts.width) + ), + discriminant(v: ModelCoreFactAxisEncoding {}), + bool_encoding_fact_node(encoding: facts.encoding) + ) } fn model_core_bool_primitive_bundle() -> PrimitiveFactBundle { diff --git a/src/v2/std/runtime.dag b/src/v2/std/runtime.dag index 10135c68890..bf64b5795cd 100644 --- a/src/v2/std/runtime.dag +++ b/src/v2/std/runtime.dag @@ -54,7 +54,7 @@ fn environment_binding_key_for_symbol(sym: Symbol) -> EnvironmentBindingKey { } type EvaluationEnvironment { - bindings: Map + bindings: PartialFunction } type RuntimePrimitiveValue { diff --git a/src/v2/test/claim/bash_build_round_trip_test.dag b/src/v2/test/claim/bash_build_round_trip_test.dag index e097c527dd6..2307d4c692a 100644 --- a/src/v2/test/claim/bash_build_round_trip_test.dag +++ b/src/v2/test/claim/bash_build_round_trip_test.dag @@ -72,7 +72,7 @@ fn bash_build_round_trip_via_emit_matches_golden( ) -> Bool { let tree = InferredTree { root: emitted, - facts: Map { lookup: bash_build_round_trip_facts_lookup } + facts: PartialFunction { lookup: bash_build_round_trip_facts_lookup } } match emit(tree: tree, target: target) { Accepted { value: source, diagnostics: d } => diff --git a/src/v2/test/claim/body_lowering/arrow_body_form_semantic_helpers.dag b/src/v2/test/claim/body_lowering/arrow_body_form_semantic_helpers.dag index 89d4266d83c..b9298c67463 100644 --- a/src/v2/test/claim/body_lowering/arrow_body_form_semantic_helpers.dag +++ b/src/v2/test/claim/body_lowering/arrow_body_form_semantic_helpers.dag @@ -176,7 +176,7 @@ fn arrow_body_form_eval_facts_lookup(key: Node) -> Optional { fn arrow_body_form_eval_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: arrow_body_form_eval_facts_lookup } + facts: PartialFunction { lookup: arrow_body_form_eval_facts_lookup } } } diff --git a/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag b/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag index c76f5af0d2c..7d57c614555 100644 --- a/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag +++ b/src/v2/test/claim/compiler/compile_eval_thesis_proof_test.dag @@ -62,7 +62,7 @@ fn compile_eval_thesis_facts_lookup(key: Node) -> Optional { fn compile_eval_thesis_inferred(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: compile_eval_thesis_facts_lookup } } diff --git a/src/v2/test/claim/emit/rust_bind_let_emit_test.dag b/src/v2/test/claim/emit/rust_bind_let_emit_test.dag index 6c5433bb7fc..4f506df4e98 100644 --- a/src/v2/test/claim/emit/rust_bind_let_emit_test.dag +++ b/src/v2/test/claim/emit/rust_bind_let_emit_test.dag @@ -99,7 +99,7 @@ fn rust_bind_let_facts_miss(key: Node) -> Optional { fn rust_bind_let_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_bind_let_facts_miss } + facts: PartialFunction { lookup: rust_bind_let_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_binop_emit_test.dag b/src/v2/test/claim/emit/rust_binop_emit_test.dag index 650ba9bd741..8f161471287 100644 --- a/src/v2/test/claim/emit/rust_binop_emit_test.dag +++ b/src/v2/test/claim/emit/rust_binop_emit_test.dag @@ -83,7 +83,7 @@ fn rust_binop_facts_miss(key: Node) -> Optional { fn rust_binop_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_binop_facts_miss } + facts: PartialFunction { lookup: rust_binop_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_body_add_emit_test.dag b/src/v2/test/claim/emit/rust_body_add_emit_test.dag index f90c8cd619d..af2a0ec5692 100644 --- a/src/v2/test/claim/emit/rust_body_add_emit_test.dag +++ b/src/v2/test/claim/emit/rust_body_add_emit_test.dag @@ -59,7 +59,7 @@ fn rust_body_add_facts_miss(key: Node) -> Optional { fn rust_body_add_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_body_add_facts_miss } + facts: PartialFunction { lookup: rust_body_add_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_call_emit_test.dag b/src/v2/test/claim/emit/rust_call_emit_test.dag index f7bd41d8c39..839a0770c10 100644 --- a/src/v2/test/claim/emit/rust_call_emit_test.dag +++ b/src/v2/test/claim/emit/rust_call_emit_test.dag @@ -225,7 +225,7 @@ fn rust_call_facts_miss(key: Node) -> Optional { fn rust_call_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_call_facts_miss } + facts: PartialFunction { lookup: rust_call_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_conditional_emit_test.dag b/src/v2/test/claim/emit/rust_conditional_emit_test.dag index 8c212d1c4d4..9cd78a0ca2a 100644 --- a/src/v2/test/claim/emit/rust_conditional_emit_test.dag +++ b/src/v2/test/claim/emit/rust_conditional_emit_test.dag @@ -49,7 +49,7 @@ fn rust_conditional_emit_facts_miss(key: Node) -> Optional { fn rust_conditional_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_conditional_emit_facts_miss } + facts: PartialFunction { lookup: rust_conditional_emit_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_field_access_emit_test.dag b/src/v2/test/claim/emit/rust_field_access_emit_test.dag index 2bcbfbf3ae9..5cceb64c46c 100644 --- a/src/v2/test/claim/emit/rust_field_access_emit_test.dag +++ b/src/v2/test/claim/emit/rust_field_access_emit_test.dag @@ -88,7 +88,7 @@ fn rust_field_access_emit_facts_miss(key: Node) -> Optional { fn rust_field_access_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_field_access_emit_facts_miss } + facts: PartialFunction { lookup: rust_field_access_emit_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_fold_call_closure_emit_test.dag b/src/v2/test/claim/emit/rust_fold_call_closure_emit_test.dag index c4f6b6f47cb..e0aab192e2b 100644 --- a/src/v2/test/claim/emit/rust_fold_call_closure_emit_test.dag +++ b/src/v2/test/claim/emit/rust_fold_call_closure_emit_test.dag @@ -48,7 +48,7 @@ fn rust_fold_call_emit_facts_miss(key: Node) -> Optional { fn rust_fold_call_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_fold_call_emit_facts_miss } + facts: PartialFunction { lookup: rust_fold_call_emit_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_literal_bind_emit_test.dag b/src/v2/test/claim/emit/rust_literal_bind_emit_test.dag index b9c7804c234..9ffa4a1afbb 100644 --- a/src/v2/test/claim/emit/rust_literal_bind_emit_test.dag +++ b/src/v2/test/claim/emit/rust_literal_bind_emit_test.dag @@ -64,7 +64,7 @@ fn rust_literal_bind_facts_miss(key: Node) -> Optional { fn rust_literal_bind_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_literal_bind_facts_miss } + facts: PartialFunction { lookup: rust_literal_bind_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_logic_complement_emit_test.dag b/src/v2/test/claim/emit/rust_logic_complement_emit_test.dag index e58ed9f291f..01c87cdaa76 100644 --- a/src/v2/test/claim/emit/rust_logic_complement_emit_test.dag +++ b/src/v2/test/claim/emit/rust_logic_complement_emit_test.dag @@ -44,7 +44,7 @@ fn rust_logic_complement_emit_facts_miss(key: Node) -> Optional { fn rust_logic_complement_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_logic_complement_emit_facts_miss } + facts: PartialFunction { lookup: rust_logic_complement_emit_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_logic_meet_join_emit_test.dag b/src/v2/test/claim/emit/rust_logic_meet_join_emit_test.dag index df11e8e0a7f..520e68b3c1d 100644 --- a/src/v2/test/claim/emit/rust_logic_meet_join_emit_test.dag +++ b/src/v2/test/claim/emit/rust_logic_meet_join_emit_test.dag @@ -50,7 +50,7 @@ fn meet_join_emit_facts_miss(key: Node) -> Optional { fn meet_join_emit_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: meet_join_emit_facts_miss } + facts: PartialFunction { lookup: meet_join_emit_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_loop_emit_test.dag b/src/v2/test/claim/emit/rust_loop_emit_test.dag index cb427909820..52a162aadd3 100644 --- a/src/v2/test/claim/emit/rust_loop_emit_test.dag +++ b/src/v2/test/claim/emit/rust_loop_emit_test.dag @@ -48,7 +48,7 @@ fn rust_loop_emit_facts_miss(key: Node) -> Optional { fn rust_loop_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_loop_emit_facts_miss } + facts: PartialFunction { lookup: rust_loop_emit_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_match_emit_test.dag b/src/v2/test/claim/emit/rust_match_emit_test.dag index 3ad6153bbe1..7ca2cc79d2d 100644 --- a/src/v2/test/claim/emit/rust_match_emit_test.dag +++ b/src/v2/test/claim/emit/rust_match_emit_test.dag @@ -49,7 +49,7 @@ fn rust_match_emit_facts_miss(key: Node) -> Optional { fn rust_match_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_match_emit_facts_miss } + facts: PartialFunction { lookup: rust_match_emit_facts_miss } } } diff --git a/src/v2/test/claim/emit/rust_record_construct_emit_test.dag b/src/v2/test/claim/emit/rust_record_construct_emit_test.dag index 20d953dc313..852e336ac56 100644 --- a/src/v2/test/claim/emit/rust_record_construct_emit_test.dag +++ b/src/v2/test/claim/emit/rust_record_construct_emit_test.dag @@ -42,7 +42,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data rust_record_construct_emit_inferred_tree: InferredTree = InferredTree { root: dag_fixture_emitted_rec_fn, - facts: Map { lookup: rust_record_construct_emit_facts_miss } + facts: PartialFunction { lookup: rust_record_construct_emit_facts_miss } } fn rust_record_construct_emit_facts_miss(key: Node) -> Optional { diff --git a/src/v2/test/claim/emit/rust_variant_construct_emit_test.dag b/src/v2/test/claim/emit/rust_variant_construct_emit_test.dag index d85acb58544..e71938ce550 100644 --- a/src/v2/test/claim/emit/rust_variant_construct_emit_test.dag +++ b/src/v2/test/claim/emit/rust_variant_construct_emit_test.dag @@ -48,7 +48,7 @@ fn rust_variant_construct_emit_facts_miss(key: Node) -> Optional fn rust_variant_construct_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: rust_variant_construct_emit_facts_miss } + facts: PartialFunction { lookup: rust_variant_construct_emit_facts_miss } } } diff --git a/src/v2/test/claim/execution/bind_round_trip_test.dag b/src/v2/test/claim/execution/bind_round_trip_test.dag index fbea01be051..dd6455c2ecc 100644 --- a/src/v2/test/claim/execution/bind_round_trip_test.dag +++ b/src/v2/test/claim/execution/bind_round_trip_test.dag @@ -165,7 +165,7 @@ fn bind_round_trip_facts_lookup(key: Node) -> Optional { data bind_inferred_tree: InferredTree = InferredTree { root: bind_emitted_root, - facts: Map { + facts: PartialFunction { lookup: bind_round_trip_facts_lookup } } diff --git a/src/v2/test/claim/execution/branch_eval_by_execution_test.dag b/src/v2/test/claim/execution/branch_eval_by_execution_test.dag index 90d4a65ff4f..0a5133d4de6 100644 --- a/src/v2/test/claim/execution/branch_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/branch_eval_by_execution_test.dag @@ -365,7 +365,7 @@ fn branch_facts_lookup(key: Node) -> Optional { fn branch_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: branch_facts_lookup } } diff --git a/src/v2/test/claim/execution/branch_if_then_else_round_trip_test.dag b/src/v2/test/claim/execution/branch_if_then_else_round_trip_test.dag index 878d4ff6d88..e49f49e7b01 100644 --- a/src/v2/test/claim/execution/branch_if_then_else_round_trip_test.dag +++ b/src/v2/test/claim/execution/branch_if_then_else_round_trip_test.dag @@ -156,7 +156,7 @@ fn branch_if_then_else_facts_lookup(key: Node) -> Optional { data branch_if_then_else_inferred_tree: InferredTree = InferredTree { root: branch_if_then_else_emitted_root, - facts: Map { + facts: PartialFunction { lookup: branch_if_then_else_facts_lookup } } diff --git a/src/v2/test/claim/execution/dag_add_emit_round_trip_test.dag b/src/v2/test/claim/execution/dag_add_emit_round_trip_test.dag index 71dd3e405aa..912d237f164 100644 --- a/src/v2/test/claim/execution/dag_add_emit_round_trip_test.dag +++ b/src/v2/test/claim/execution/dag_add_emit_round_trip_test.dag @@ -140,7 +140,7 @@ fn dag_add_facts_lookup(key: Node) -> Optional { data dag_add_inferred_tree: InferredTree = InferredTree { root: dag_add_emitted_root, - facts: Map { + facts: PartialFunction { lookup: dag_add_facts_lookup } } @@ -213,7 +213,7 @@ test fn dag_add_domain_translate_accepts_holds() -> Bool { match translate_emitted_node( tree: InferredTree { root: dag_arrow_domain_conj_node(), - facts: Map { lookup: dag_add_facts_lookup } + facts: PartialFunction { lookup: dag_add_facts_lookup } }, target: dag_add_target_model ) { diff --git a/src/v2/test/claim/execution/effect_io_eval_by_execution_test.dag b/src/v2/test/claim/execution/effect_io_eval_by_execution_test.dag index a828ee86cff..90749ff3f8c 100644 --- a/src/v2/test/claim/execution/effect_io_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/effect_io_eval_by_execution_test.dag @@ -228,7 +228,7 @@ fn effect_io_eval_fact_lookup(node: Node) -> Optional { fn effect_io_eval_tree() -> InferredTree { InferredTree { root: effect_io_eval_roundtrip_node, - facts: Map { lookup: effect_io_eval_fact_lookup } + facts: PartialFunction { lookup: effect_io_eval_fact_lookup } } } diff --git a/src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag index ad54f927e99..a2234875606 100644 --- a/src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag @@ -228,7 +228,7 @@ fn emit_eval_composed_facts(node: Node) -> Optional { fn emit_eval_subject_tree() -> InferredTree { InferredTree { root: rust_fixture_emitted_add_fn, - facts: Map { lookup: emit_eval_composed_facts } + facts: PartialFunction { lookup: emit_eval_composed_facts } } } diff --git a/src/v2/test/claim/execution/emit_host_complement_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_complement_equals_eval_test.dag index c5f8d9d7046..27034f4d881 100644 --- a/src/v2/test/claim/execution/emit_host_complement_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_complement_equals_eval_test.dag @@ -111,7 +111,7 @@ fn emit_complement_eval_composed_facts(key: Node) -> Optional { fn emit_complement_eval_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: emit_complement_eval_composed_facts } + facts: PartialFunction { lookup: emit_complement_eval_composed_facts } } } diff --git a/src/v2/test/claim/execution/emit_host_field_access_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_field_access_equals_eval_test.dag index 3e74cfea3af..d857f9e1358 100644 --- a/src/v2/test/claim/execution/emit_host_field_access_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_field_access_equals_eval_test.dag @@ -148,7 +148,7 @@ fn emit_field_eval_producer_tree() -> Outcome { outcome_accepted( value: InferredTree { root: dag_field_access_arrow_with_body_fixture, - facts: Map { lookup: emit_field_eval_composed_facts } + facts: PartialFunction { lookup: emit_field_eval_composed_facts } } ) } @@ -157,7 +157,7 @@ fn emit_field_eval_alt_descent_producer_tree() -> Outcome { outcome_accepted( value: InferredTree { root: dag_field_access_arrow_with_body_fixture, - facts: Map { lookup: emit_field_eval_alt_descent_composed_facts } + facts: PartialFunction { lookup: emit_field_eval_alt_descent_composed_facts } } ) } diff --git a/src/v2/test/claim/execution/emit_host_fold_closure_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_fold_closure_equals_eval_test.dag index fe625a1deea..5a240e151fc 100644 --- a/src/v2/test/claim/execution/emit_host_fold_closure_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_fold_closure_equals_eval_test.dag @@ -117,7 +117,7 @@ fn emit_fold_eval_composed_facts(key: Node) -> Optional { fn emit_fold_eval_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: emit_fold_eval_composed_facts } + facts: PartialFunction { lookup: emit_fold_eval_composed_facts } } } diff --git a/src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag index dcd58fea4ca..34cfd38beb7 100644 --- a/src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag @@ -111,7 +111,7 @@ fn emit_loop_eval_producer_tree() -> Outcome { outcome_accepted( value: InferredTree { root: root, - facts: Map { lookup: emit_loop_eval_composed_facts } + facts: PartialFunction { lookup: emit_loop_eval_composed_facts } } ) Rejected { diagnostics: r } => Rejected { diagnostics: r } @@ -124,7 +124,7 @@ fn emit_loop_eval_wrong_value_producer_tree() -> Outcome { outcome_accepted( value: InferredTree { root: root, - facts: Map { lookup: emit_loop_eval_composed_facts } + facts: PartialFunction { lookup: emit_loop_eval_composed_facts } } ) Rejected { diagnostics: r } => Rejected { diagnostics: r } diff --git a/src/v2/test/claim/execution/emit_host_match_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_match_equals_eval_test.dag index e75ed7170d2..c222146e9b9 100644 --- a/src/v2/test/claim/execution/emit_host_match_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_match_equals_eval_test.dag @@ -119,7 +119,7 @@ fn emit_match_eval_producer_tree() -> Outcome { outcome_accepted( value: InferredTree { root: root, - facts: Map { lookup: emit_match_eval_composed_facts } + facts: PartialFunction { lookup: emit_match_eval_composed_facts } } ) Rejected { diagnostics: r } => Rejected { diagnostics: r } @@ -132,7 +132,7 @@ fn emit_match_eval_swapped_producer_tree() -> Outcome { outcome_accepted( value: InferredTree { root: root, - facts: Map { lookup: emit_match_eval_composed_facts } + facts: PartialFunction { lookup: emit_match_eval_composed_facts } } ) Rejected { diagnostics: r } => Rejected { diagnostics: r } diff --git a/src/v2/test/claim/execution/emit_host_meet_join_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_meet_join_equals_eval_test.dag index 881b83bf0db..6280ecab5e2 100644 --- a/src/v2/test/claim/execution/emit_host_meet_join_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_meet_join_equals_eval_test.dag @@ -118,7 +118,7 @@ fn meet_join_eval_composed_facts(key: Node) -> Optional { fn meet_join_eval_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: meet_join_eval_composed_facts } + facts: PartialFunction { lookup: meet_join_eval_composed_facts } } } diff --git a/src/v2/test/claim/execution/emit_host_variant_construct_equals_eval_test.dag b/src/v2/test/claim/execution/emit_host_variant_construct_equals_eval_test.dag index 47590c343be..90b519f80f6 100644 --- a/src/v2/test/claim/execution/emit_host_variant_construct_equals_eval_test.dag +++ b/src/v2/test/claim/execution/emit_host_variant_construct_equals_eval_test.dag @@ -112,7 +112,7 @@ fn emit_variant_construct_eval_composed_facts(key: Node) -> Optional InferredTree { InferredTree { root: root, - facts: Map { lookup: emit_variant_construct_eval_composed_facts } + facts: PartialFunction { lookup: emit_variant_construct_eval_composed_facts } } } diff --git a/src/v2/test/claim/execution/eval_bind_non_bind_interpreter_rejects_test.dag b/src/v2/test/claim/execution/eval_bind_non_bind_interpreter_rejects_test.dag index 0896bc87e76..be0ab082147 100644 --- a/src/v2/test/claim/execution/eval_bind_non_bind_interpreter_rejects_test.dag +++ b/src/v2/test/claim/execution/eval_bind_non_bind_interpreter_rejects_test.dag @@ -11,7 +11,7 @@ test fn eval_bind_node_eval_rejects_value_interpreter_holds() -> Bool { } let tree = InferredTree { root: node, - facts: Map { + facts: PartialFunction { lookup: fn(n) { Absent } diff --git a/src/v2/test/claim/execution/long/add_arrow_eval_by_execution_test.dag b/src/v2/test/claim/execution/long/add_arrow_eval_by_execution_test.dag index f058fa9f9dc..bc35ef06cfd 100644 --- a/src/v2/test/claim/execution/long/add_arrow_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/long/add_arrow_eval_by_execution_test.dag @@ -406,7 +406,7 @@ fn add_arrow_eval_facts_lookup(key: Node) -> Optional { fn add_arrow_eval_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: add_arrow_eval_facts_lookup } } @@ -837,7 +837,7 @@ fn add_arrow_eval_lazy_arm_loop_node() -> Node { fn add_arrow_eval_loop_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: fn(key) { match key.kind { ComputationNode { behavior: Loop } => diff --git a/src/v2/test/claim/execution/long/bind_eval_by_execution_test.dag b/src/v2/test/claim/execution/long/bind_eval_by_execution_test.dag index f7d2644ba0f..a710ac16082 100644 --- a/src/v2/test/claim/execution/long/bind_eval_by_execution_test.dag +++ b/src/v2/test/claim/execution/long/bind_eval_by_execution_test.dag @@ -293,7 +293,7 @@ fn bind_facts_lookup(key: Node) -> Optional { fn bind_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: bind_facts_lookup } } diff --git a/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag b/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag index cde17ddfd27..2df6a22b06e 100644 --- a/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag +++ b/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag @@ -186,7 +186,7 @@ fn ingested_staging_inferred_tree_from_source(source: String) -> Outcome Outcome Outcome Optional { fn loop_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: loop_facts_lookup } } diff --git a/src/v2/test/claim/execution/long/pick_ingested_structural_lowering_test.dag b/src/v2/test/claim/execution/long/pick_ingested_structural_lowering_test.dag index dc005ab488d..2db6dc7d421 100644 --- a/src/v2/test/claim/execution/long/pick_ingested_structural_lowering_test.dag +++ b/src/v2/test/claim/execution/long/pick_ingested_structural_lowering_test.dag @@ -331,7 +331,7 @@ fn pick_eval_facts_lookup(key: Node) -> Optional { fn pick_eval_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: pick_eval_facts_lookup } } diff --git a/src/v2/test/claim/execution/loop_round_trip_test.dag b/src/v2/test/claim/execution/loop_round_trip_test.dag index 6338c30035b..10aad5683d8 100644 --- a/src/v2/test/claim/execution/loop_round_trip_test.dag +++ b/src/v2/test/claim/execution/loop_round_trip_test.dag @@ -174,7 +174,7 @@ fn loop_round_trip_facts_lookup(key: Node) -> Optional { data loop_inferred_tree: InferredTree = InferredTree { root: loop_emitted_root, - facts: Map { + facts: PartialFunction { lookup: loop_round_trip_facts_lookup } } diff --git a/src/v2/test/claim/execution/match_bool_round_trip_test.dag b/src/v2/test/claim/execution/match_bool_round_trip_test.dag index fe716a714c7..84597d74e6d 100644 --- a/src/v2/test/claim/execution/match_bool_round_trip_test.dag +++ b/src/v2/test/claim/execution/match_bool_round_trip_test.dag @@ -155,7 +155,7 @@ fn match_bool_facts_lookup(key: Node) -> Optional { data match_bool_inferred_tree: InferredTree = InferredTree { root: match_bool_emitted_root, - facts: Map { + facts: PartialFunction { lookup: match_bool_facts_lookup } } diff --git a/src/v2/test/claim/execution/rust_emit_host_call_equals_eval_test.dag b/src/v2/test/claim/execution/rust_emit_host_call_equals_eval_test.dag index cbc82b3f444..10ace6410d7 100644 --- a/src/v2/test/claim/execution/rust_emit_host_call_equals_eval_test.dag +++ b/src/v2/test/claim/execution/rust_emit_host_call_equals_eval_test.dag @@ -217,7 +217,7 @@ fn emit_call_eval_composed_facts(key: Node) -> Optional { fn emit_call_eval_producer_tree() -> InferredTree { InferredTree { root: rust_call_helper_arrow(), - facts: Map { lookup: emit_call_eval_composed_facts } + facts: PartialFunction { lookup: emit_call_eval_composed_facts } } } diff --git a/src/v2/test/claim/execution/rust_record_construct_emit_host_equals_eval_test.dag b/src/v2/test/claim/execution/rust_record_construct_emit_host_equals_eval_test.dag index 1361fdeed94..9d56da1d169 100644 --- a/src/v2/test/claim/execution/rust_record_construct_emit_host_equals_eval_test.dag +++ b/src/v2/test/claim/execution/rust_record_construct_emit_host_equals_eval_test.dag @@ -148,7 +148,7 @@ fn rust_rec_nine_eval_composed_facts(key: Node) -> Optional { fn rust_rec_nine_eval_inferred_tree() -> InferredTree { InferredTree { root: rust_rec_nine_arrow_node(), - facts: Map { lookup: rust_rec_nine_eval_composed_facts } + facts: PartialFunction { lookup: rust_rec_nine_eval_composed_facts } } } diff --git a/src/v2/test/claim/generated/idempotent_operation_conformance.dag b/src/v2/test/claim/generated/idempotent_operation_conformance.dag index 5c931eb102c..a9506e5d63f 100644 --- a/src/v2/test/claim/generated/idempotent_operation_conformance.dag +++ b/src/v2/test/claim/generated/idempotent_operation_conformance.dag @@ -174,7 +174,7 @@ fn idempotent_operation_inferred_tree(root: Node) -> InferredTree { let facts = idempotent_operation_inferred_facts(root: root) InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: fn(_) { Present { value: facts } } diff --git a/src/v2/test/claim/generated/language_behavior_equivalence_test.dag b/src/v2/test/claim/generated/language_behavior_equivalence_test.dag index a8c7899b4e4..3beb0ad5678 100644 --- a/src/v2/test/claim/generated/language_behavior_equivalence_test.dag +++ b/src/v2/test/claim/generated/language_behavior_equivalence_test.dag @@ -146,7 +146,7 @@ fn lbe_inferred_tree(root: Node) -> InferredTree { let facts = lbe_inferred_facts(resolved: root) InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: fn(_) { Present { value: facts } } diff --git a/src/v2/test/claim/manual/add_body_emit_typescript_test.dag b/src/v2/test/claim/manual/add_body_emit_typescript_test.dag index fa2cd68d47a..23761329727 100644 --- a/src/v2/test/claim/manual/add_body_emit_typescript_test.dag +++ b/src/v2/test/claim/manual/add_body_emit_typescript_test.dag @@ -398,7 +398,7 @@ fn add_body_ts_facts_lookup(key: Node) -> Optional { fn add_body_ts_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: add_body_ts_facts_lookup } + facts: PartialFunction { lookup: add_body_ts_facts_lookup } } } diff --git a/src/v2/test/claim/manual/bash_emit_command_test.dag b/src/v2/test/claim/manual/bash_emit_command_test.dag index db9df690e29..f2b121accec 100644 --- a/src/v2/test/claim/manual/bash_emit_command_test.dag +++ b/src/v2/test/claim/manual/bash_emit_command_test.dag @@ -138,7 +138,7 @@ test fn bash_emit_lhs_exact_arrow_emitted_rejects_holds() -> Bool { data bash_emit_inferred_tree: InferredTree = InferredTree { root: bash_emitted_command, - facts: Map { + facts: PartialFunction { lookup: bash_facts_lookup } } @@ -191,7 +191,7 @@ test fn bash_emit_missing_rules_rejects_holds() -> Bool { data bash_bound_words_emit_inferred_tree: InferredTree = InferredTree { root: bash_bound_words_emitted_command, - facts: Map { + facts: PartialFunction { lookup: bash_facts_lookup } } @@ -212,7 +212,7 @@ test fn bash_emit_bound_words_holds() -> Bool { data bash_embedded_quote_emit_inferred_tree: InferredTree = InferredTree { root: bash_embedded_quote_emitted_command, - facts: Map { + facts: PartialFunction { lookup: bash_facts_lookup } } @@ -233,7 +233,7 @@ test fn bash_emit_embedded_quote_holds() -> Bool { data bash_source_root_ingest_gate_emit_inferred_tree: InferredTree = InferredTree { root: bash_source_root_ingest_gate_emitted_command, - facts: Map { + facts: PartialFunction { lookup: bash_facts_lookup } } @@ -262,7 +262,7 @@ fn bash_emit_slice4_holds( ) -> Bool { let tree = InferredTree { root: emitted, - facts: Map { lookup: bash_facts_lookup } + facts: PartialFunction { lookup: bash_facts_lookup } } match emit(tree: tree, target: target) { Accepted { value: source, diagnostics: d } => (source.carried == source_text) && (d == None) @@ -365,7 +365,7 @@ test fn bash_emit_pipe_and_or_flat_wrong_model_holds() -> Bool { fn bash_emit_pipe_brace_grouped_wrong_flat_model_rejects() -> Bool { let tree = InferredTree { root: bash_pipe_and_or_brace_grouped_emitted, - facts: Map { lookup: bash_facts_lookup } + facts: PartialFunction { lookup: bash_facts_lookup } } match emit(tree: tree, target: bash_pipe_and_or_flat_wrong_target_model()) { Accepted { value: source, diagnostics: d } => diff --git a/src/v2/test/claim/manual/bind_demand_driven_eval_test.dag b/src/v2/test/claim/manual/bind_demand_driven_eval_test.dag index bfc3eb985dc..bb28f75f445 100644 --- a/src/v2/test/claim/manual/bind_demand_driven_eval_test.dag +++ b/src/v2/test/claim/manual/bind_demand_driven_eval_test.dag @@ -356,7 +356,7 @@ fn bind_eval_facts_lookup(key: Node) -> Optional { fn bind_eval_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: bind_eval_facts_lookup } + facts: PartialFunction { lookup: bind_eval_facts_lookup } } } diff --git a/src/v2/test/claim/manual/bind_emit_test.dag b/src/v2/test/claim/manual/bind_emit_test.dag index 038fa31e011..7d661af8f4f 100644 --- a/src/v2/test/claim/manual/bind_emit_test.dag +++ b/src/v2/test/claim/manual/bind_emit_test.dag @@ -61,7 +61,7 @@ fn bind_emit_facts_lookup(key: Node) -> Optional { fn bind_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: bind_emit_facts_lookup } + facts: PartialFunction { lookup: bind_emit_facts_lookup } } } diff --git a/src/v2/test/claim/manual/branch_if_then_else_emit_test.dag b/src/v2/test/claim/manual/branch_if_then_else_emit_test.dag index 682a160a20d..42c6fa4fd38 100644 --- a/src/v2/test/claim/manual/branch_if_then_else_emit_test.dag +++ b/src/v2/test/claim/manual/branch_if_then_else_emit_test.dag @@ -65,7 +65,7 @@ fn branch_if_then_else_emit_facts_lookup(key: Node) -> Optional { fn branch_if_then_else_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: branch_if_then_else_emit_facts_lookup } + facts: PartialFunction { lookup: branch_if_then_else_emit_facts_lookup } } } diff --git a/src/v2/test/claim/manual/branch_lazy_arm_eval_acceptance_test.dag b/src/v2/test/claim/manual/branch_lazy_arm_eval_acceptance_test.dag index 16266d3c48e..9601950ac74 100644 --- a/src/v2/test/claim/manual/branch_lazy_arm_eval_acceptance_test.dag +++ b/src/v2/test/claim/manual/branch_lazy_arm_eval_acceptance_test.dag @@ -506,7 +506,7 @@ fn lazy_arm_facts_lookup(key: Node) -> Optional { fn lazy_arm_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: lazy_arm_facts_lookup } + facts: PartialFunction { lookup: lazy_arm_facts_lookup } } } diff --git a/src/v2/test/claim/manual/c_add_emit_translate_test.dag b/src/v2/test/claim/manual/c_add_emit_translate_test.dag index 1c11417b16d..12dc59c3311 100644 --- a/src/v2/test/claim/manual/c_add_emit_translate_test.dag +++ b/src/v2/test/claim/manual/c_add_emit_translate_test.dag @@ -146,7 +146,7 @@ fn c_add_facts_lookup(key: Node) -> Optional { data c_add_inferred_tree: InferredTree = InferredTree { root: c_add_emitted_root, - facts: Map { lookup: c_add_facts_lookup } + facts: PartialFunction { lookup: c_add_facts_lookup } } fn c_add_emit_accepts() -> Outcome> { @@ -193,7 +193,7 @@ test fn c_add_serialize_rejects_missing_translation_rules_holds() -> Bool { test fn c_add_emit_wrong_node_refuses_holds() -> Bool { let wrong_tree = InferredTree { root: c_add_wrong_emitted_root, - facts: Map { lookup: c_add_facts_lookup } + facts: PartialFunction { lookup: c_add_facts_lookup } } match emit(tree: wrong_tree, target: c_add_target_model) { Accepted { value: source, diagnostics: d } => diff --git a/src/v2/test/claim/manual/cpp_add_emit_translate_test.dag b/src/v2/test/claim/manual/cpp_add_emit_translate_test.dag index a654c3cbd18..bc8624be097 100644 --- a/src/v2/test/claim/manual/cpp_add_emit_translate_test.dag +++ b/src/v2/test/claim/manual/cpp_add_emit_translate_test.dag @@ -300,7 +300,7 @@ fn cpp_add_facts_lookup(key: Node) -> Optional { data cpp_add_inferred_tree: InferredTree = InferredTree { root: cpp_add_emitted_root, - facts: Map { + facts: PartialFunction { lookup: cpp_add_facts_lookup } } diff --git a/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag b/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag index aae5ef9177d..6bca410d7b5 100644 --- a/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag +++ b/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag @@ -397,7 +397,7 @@ fn subsumption_fact_lookup(node: Node) -> Optional { fn subsumption_inferred_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: subsumption_fact_lookup } } diff --git a/src/v2/test/claim/manual/emit_directive_bash_test.dag b/src/v2/test/claim/manual/emit_directive_bash_test.dag index 4f93be895bc..f489e511ddb 100644 --- a/src/v2/test/claim/manual/emit_directive_bash_test.dag +++ b/src/v2/test/claim/manual/emit_directive_bash_test.dag @@ -65,7 +65,7 @@ fn emit_directive_bash_emit(d: EmitDirective) -> Outcome> { emit( tree: InferredTree { root: emit_directive_bash_emitted_command, - facts: Map { lookup: emit_directive_facts_lookup } + facts: PartialFunction { lookup: emit_directive_facts_lookup } }, target: emit_directive_bash_target_model(d: d) ) @@ -106,7 +106,7 @@ fn emit_directive_bash_emit_to_stdout_wrong(d: EmitDirective) -> Outcome Outcome> { emit( tree: InferredTree { root: emit_directive_bash_emitted_command, - facts: Map { lookup: emit_directive_facts_lookup } + facts: PartialFunction { lookup: emit_directive_facts_lookup } }, target: emit_directive_gha_target_model(d: d) ) @@ -74,7 +74,7 @@ fn emit_directive_bash_emit(d: EmitDirective) -> Outcome> { emit( tree: InferredTree { root: emit_directive_bash_emitted_command, - facts: Map { lookup: emit_directive_facts_lookup } + facts: PartialFunction { lookup: emit_directive_facts_lookup } }, target: emit_directive_bash_target_model(d: d) ) diff --git a/src/v2/test/claim/manual/emit_directive_rust_test.dag b/src/v2/test/claim/manual/emit_directive_rust_test.dag index 800b9ab63e0..14e45c1c443 100644 --- a/src/v2/test/claim/manual/emit_directive_rust_test.dag +++ b/src/v2/test/claim/manual/emit_directive_rust_test.dag @@ -72,7 +72,7 @@ fn emit_directive_rust_emit(d: EmitDirective) -> Outcome> { emit( tree: InferredTree { root: rust_emit_directive_emitted_call, - facts: Map { lookup: emit_directive_facts_lookup } + facts: PartialFunction { lookup: emit_directive_facts_lookup } }, target: rust_emit_directive_target_model(d: d) ) @@ -82,7 +82,7 @@ fn emit_directive_bash_emit(d: EmitDirective) -> Outcome> { emit( tree: InferredTree { root: emit_directive_bash_emitted_command, - facts: Map { lookup: emit_directive_facts_lookup } + facts: PartialFunction { lookup: emit_directive_facts_lookup } }, target: emit_directive_bash_target_model(d: d) ) diff --git a/src/v2/test/claim/manual/english_emit_add_test.dag b/src/v2/test/claim/manual/english_emit_add_test.dag index c3ec9069113..b5cb3677d18 100644 --- a/src/v2/test/claim/manual/english_emit_add_test.dag +++ b/src/v2/test/claim/manual/english_emit_add_test.dag @@ -162,7 +162,7 @@ fn english_emit_add_facts_lookup(key: Node) -> Optional { data english_emit_add_inferred_tree: InferredTree = InferredTree { root: english_emit_add_emitted_root, - facts: Map { + facts: PartialFunction { lookup: english_emit_add_facts_lookup } } diff --git a/src/v2/test/claim/manual/eval_runtime.dag b/src/v2/test/claim/manual/eval_runtime.dag index 54e45e73697..9866084625c 100644 --- a/src/v2/test/claim/manual/eval_runtime.dag +++ b/src/v2/test/claim/manual/eval_runtime.dag @@ -317,7 +317,7 @@ fn eval_fact_lookup(node: Node) -> Optional { fn eval_inferred_tree() -> InferredTree { InferredTree { root: eval_add_subgraph(), - facts: Map { + facts: PartialFunction { lookup: eval_fact_lookup } } diff --git a/src/v2/test/claim/manual/field_access_emit_test.dag b/src/v2/test/claim/manual/field_access_emit_test.dag index 80756045487..7ac96ba6bc6 100644 --- a/src/v2/test/claim/manual/field_access_emit_test.dag +++ b/src/v2/test/claim/manual/field_access_emit_test.dag @@ -143,7 +143,7 @@ fn field_access_facts_lookup(key: Node) -> Optional { data field_access_inferred_tree: InferredTree = InferredTree { root: field_access_emitted_root, - facts: Map { lookup: field_access_facts_lookup } + facts: PartialFunction { lookup: field_access_facts_lookup } } test fn field_access_emit_holds() -> Bool { diff --git a/src/v2/test/claim/manual/go_add_emit_translate_test.dag b/src/v2/test/claim/manual/go_add_emit_translate_test.dag index e896c3f35e8..474b60fcbc3 100644 --- a/src/v2/test/claim/manual/go_add_emit_translate_test.dag +++ b/src/v2/test/claim/manual/go_add_emit_translate_test.dag @@ -290,7 +290,7 @@ fn go_add_facts_lookup(key: Node) -> Optional { data go_add_inferred_tree: InferredTree = InferredTree { root: go_add_emitted_root, - facts: Map { + facts: PartialFunction { lookup: go_add_facts_lookup } } diff --git a/src/v2/test/claim/manual/infer_emit_compile_anchor.dag b/src/v2/test/claim/manual/infer_emit_compile_anchor.dag index c8abd3b9a73..45007ffd949 100644 --- a/src/v2/test/claim/manual/infer_emit_compile_anchor.dag +++ b/src/v2/test/claim/manual/infer_emit_compile_anchor.dag @@ -31,7 +31,7 @@ data anchor_stub_inferred_facts: InferredFacts = claim_inferred_facts_from_nodes } ) -data anchor_stub_empty_facts_map: Map = Map { +data anchor_stub_empty_facts_map: PartialFunction = PartialFunction { lookup: fn(_) { Absent } diff --git a/src/v2/test/claim/manual/infer_ground_add.dag b/src/v2/test/claim/manual/infer_ground_add.dag index ec4d2746cc8..68b947155d1 100644 --- a/src/v2/test/claim/manual/infer_ground_add.dag +++ b/src/v2/test/claim/manual/infer_ground_add.dag @@ -16,7 +16,7 @@ import v2.compiler.infer { InferredTree } import v2.compiler.resolve { ResolvedTree } -import v2.std.collection { List, Map } +import v2.std.collection { List, Map, empty_map } import v2.std.diagnostic { Accepted, AmbiguousIntent, @@ -240,11 +240,7 @@ fn infer_receipt_context() -> EvalContext { fn infer_receipt_empty_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { - lookup: fn(_) { - Absent - } - } + facts: empty_map() } } diff --git a/src/v2/test/claim/manual/loop_demand_driven_eval_test.dag b/src/v2/test/claim/manual/loop_demand_driven_eval_test.dag index ba660621d82..6d22c70b046 100644 --- a/src/v2/test/claim/manual/loop_demand_driven_eval_test.dag +++ b/src/v2/test/claim/manual/loop_demand_driven_eval_test.dag @@ -316,7 +316,7 @@ fn loop_eval_tree_root(call: Node, expected: Node) -> Node { fn loop_eval_admitted_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: loop_eval_facts_lookup } + facts: PartialFunction { lookup: loop_eval_facts_lookup } } } diff --git a/src/v2/test/claim/manual/loop_emit_test.dag b/src/v2/test/claim/manual/loop_emit_test.dag index 7259384688c..d18b16e02f5 100644 --- a/src/v2/test/claim/manual/loop_emit_test.dag +++ b/src/v2/test/claim/manual/loop_emit_test.dag @@ -59,7 +59,7 @@ fn loop_emit_facts_lookup(key: Node) -> Optional { fn loop_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: loop_emit_facts_lookup } + facts: PartialFunction { lookup: loop_emit_facts_lookup } } } diff --git a/src/v2/test/claim/manual/match_bool_emit_test.dag b/src/v2/test/claim/manual/match_bool_emit_test.dag index c6b7ac6ec33..74981976a6e 100644 --- a/src/v2/test/claim/manual/match_bool_emit_test.dag +++ b/src/v2/test/claim/manual/match_bool_emit_test.dag @@ -68,7 +68,7 @@ fn match_bool_emit_facts_lookup(key: Node) -> Optional { fn match_bool_emit_inferred_tree_for(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { lookup: match_bool_emit_facts_lookup } + facts: PartialFunction { lookup: match_bool_emit_facts_lookup } } } diff --git a/src/v2/test/claim/manual/python_add_emit_translate_test.dag b/src/v2/test/claim/manual/python_add_emit_translate_test.dag index 0deb2d89ddc..a720a00d2ad 100644 --- a/src/v2/test/claim/manual/python_add_emit_translate_test.dag +++ b/src/v2/test/claim/manual/python_add_emit_translate_test.dag @@ -241,7 +241,7 @@ fn python_add_facts_lookup(key: Node) -> Optional { data python_add_inferred_tree: InferredTree = InferredTree { root: python_add_emitted_root, - facts: Map { + facts: PartialFunction { lookup: python_add_facts_lookup } } diff --git a/src/v2/test/claim/manual/record_construct_emit_test.dag b/src/v2/test/claim/manual/record_construct_emit_test.dag index 34566e63bca..21413e76104 100644 --- a/src/v2/test/claim/manual/record_construct_emit_test.dag +++ b/src/v2/test/claim/manual/record_construct_emit_test.dag @@ -141,7 +141,7 @@ fn record_construct_facts_lookup(key: Node) -> Optional { data record_construct_inferred_tree: InferredTree = InferredTree { root: record_construct_emitted_root, - facts: Map { lookup: record_construct_facts_lookup } + facts: PartialFunction { lookup: record_construct_facts_lookup } } test fn record_construct_emit_holds() -> Bool { diff --git a/src/v2/test/claim/manual/runtime_run_test.dag b/src/v2/test/claim/manual/runtime_run_test.dag index 4c03d148d9f..36e3eabf0b0 100644 --- a/src/v2/test/claim/manual/runtime_run_test.dag +++ b/src/v2/test/claim/manual/runtime_run_test.dag @@ -114,7 +114,7 @@ fn runtime_run_fact_lookup(node: Node) -> Optional { fn runtime_run_test_tree() -> InferredTree { InferredTree { root: runtime_run_node_a, - facts: Map { lookup: runtime_run_fact_lookup } + facts: PartialFunction { lookup: runtime_run_fact_lookup } } } diff --git a/src/v2/test/claim/manual/rust_add_emit_translate_test.dag b/src/v2/test/claim/manual/rust_add_emit_translate_test.dag index b2a01989959..4b943595a1a 100644 --- a/src/v2/test/claim/manual/rust_add_emit_translate_test.dag +++ b/src/v2/test/claim/manual/rust_add_emit_translate_test.dag @@ -323,7 +323,7 @@ fn rust_add_facts_lookup(key: Node) -> Optional { data rust_add_inferred_tree: InferredTree = InferredTree { root: rust_add_emitted_root, - facts: Map { + facts: PartialFunction { lookup: rust_add_facts_lookup } } diff --git a/src/v2/test/claim/manual/sg2_mode2_non_grammar_emit_test.dag b/src/v2/test/claim/manual/sg2_mode2_non_grammar_emit_test.dag index 4969aa397e1..2dc503266ae 100644 --- a/src/v2/test/claim/manual/sg2_mode2_non_grammar_emit_test.dag +++ b/src/v2/test/claim/manual/sg2_mode2_non_grammar_emit_test.dag @@ -92,14 +92,14 @@ fn sg2_mode2_facts_lookup(_key: Node) -> Optional { data sg2_mode2_inferred_tree: InferredTree = InferredTree { root: rust_sg2_instantiation_source_type_node(), - facts: Map { + facts: PartialFunction { lookup: sg2_mode2_facts_lookup } } data sg2_mode2_perturbed_inferred_tree: InferredTree = InferredTree { root: rust_sg2_foobar_xy_no_rc_source_type_node(), - facts: Map { + facts: PartialFunction { lookup: sg2_mode2_facts_lookup } } diff --git a/src/v2/test/claim/manual/typescript_add_emit_translate_test.dag b/src/v2/test/claim/manual/typescript_add_emit_translate_test.dag index 07ab517880e..0f567c48aa6 100644 --- a/src/v2/test/claim/manual/typescript_add_emit_translate_test.dag +++ b/src/v2/test/claim/manual/typescript_add_emit_translate_test.dag @@ -281,7 +281,7 @@ fn typescript_add_facts_lookup(key: Node) -> Optional { data typescript_add_inferred_tree: InferredTree = InferredTree { root: typescript_add_emitted_root, - facts: Map { + facts: PartialFunction { lookup: typescript_add_facts_lookup } } diff --git a/src/v2/test/claim/manual/typescript_pr3_typed_fn_translate_test.dag b/src/v2/test/claim/manual/typescript_pr3_typed_fn_translate_test.dag index d22d30f3210..3e88ccd2747 100644 --- a/src/v2/test/claim/manual/typescript_pr3_typed_fn_translate_test.dag +++ b/src/v2/test/claim/manual/typescript_pr3_typed_fn_translate_test.dag @@ -141,7 +141,7 @@ fn typescript_pr3_facts_lookup(key: Node) -> Optional { data typescript_pr3_inferred_tree: InferredTree = InferredTree { root: typescript_pr3_emitted_root, - facts: Map { lookup: typescript_pr3_facts_lookup } + facts: PartialFunction { lookup: typescript_pr3_facts_lookup } } fn anchor_typescript_pr3_emit_accepts() -> Outcome> { diff --git a/src/v2/test/claim/manual/typescript_record_task_translate_test.dag b/src/v2/test/claim/manual/typescript_record_task_translate_test.dag index f5d307aa9e3..dec3fdfb3b8 100644 --- a/src/v2/test/claim/manual/typescript_record_task_translate_test.dag +++ b/src/v2/test/claim/manual/typescript_record_task_translate_test.dag @@ -138,7 +138,7 @@ fn typescript_record_task_facts_lookup(key: Node) -> Optional { data typescript_record_task_inferred_tree: InferredTree = InferredTree { root: typescript_record_task_emitted_root, - facts: Map { lookup: typescript_record_task_facts_lookup } + facts: PartialFunction { lookup: typescript_record_task_facts_lookup } } fn anchor_typescript_record_task_emit_accepts() -> Outcome> { diff --git a/src/v2/test/claim/map_carrier_shape_gate_test.dag b/src/v2/test/claim/map_carrier_shape_gate_test.dag index ba75d56a57a..1deb5807791 100644 --- a/src/v2/test/claim/map_carrier_shape_gate_test.dag +++ b/src/v2/test/claim/map_carrier_shape_gate_test.dag @@ -27,11 +27,27 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // the delegate lands while any `Map { lookup: ... }` literal survives — which is exactly the // premature-landing defect, caught in seconds instead of by a floor run. // -// DISSOLUTION: when the finite `Map { lookup: ... }` literals have migrated to -// `empty_map` + `map_insert` and the delegate lands as the closing move, `record_shaped` inverts — -// it must then assert that the record route is unrepresentable, not that it works. It does not -// simply delete: deleting it would remove the only executing evidence that the two shapes were -// ever reconciled. +// DISSOLUTION, AND ITS PREMISE IS NOW NARROWER THAN WHEN IT WAS WRITTEN. The original condition +// read: when the finite `Map { lookup: ... }` literals have migrated to `empty_map` + `map_insert` +// and the delegate lands as the closing move, `record_shaped` inverts — asserting the record route +// is unrepresentable rather than that it works. It does not simply delete: that would remove the +// only executing evidence that the two shapes were ever reconciled. +// +// The migration named there has happened. The 25 finite fact maps are `map_insert` chains over +// `empty_map()`, the 8 empties are `empty_map()`, and the open population — every literal whose +// lookup is a delegate or an unbounded-domain closure — names `PartialFunction` and is no longer +// spelled `Map` at all. What survives is not a residue awaiting migration: `map_insert`'s own +// `.dag` body constructs a record-shaped `Map` and MUST, because that is the arm the interpreter +// falls through to. So the record route is now produced by exactly one authority — the insert +// itself — plus this file's fixture. +// +// That changes what the closing move can be. The delegate cannot land by waiting for literals to +// disappear, because the last one is `map_insert`'s own return value: making `map_insert` delegate +// to the primitive while its body is the only record producer is the self-recursion that killed 14 +// floor witnesses. The remaining condition is a HOST fact, not a corpus one — the interpreter's +// `free_call.map_insert` arm accepting the record shape, or the record shape ceasing to be +// reachable — and until one of those holds, this gate is a healthy guard being quiet, not a dead +// one. data map_carrier_shape_gate_note: String = "Gate for the map construction delegate. map_insert grounds on the native map shape only; its .dag body is the live arm for record-shaped maps built by Map { lookup: ... } literals. record_shaped_map_reaches_map_insert reds if the delegate lands while any such literal survives." fn native_map_after_insert() -> Optional { diff --git a/src/v2/test/claim/sql_create_table_fold_test.dag b/src/v2/test/claim/sql_create_table_fold_test.dag index 61037cb0b90..bf9ef45fd19 100644 --- a/src/v2/test/claim/sql_create_table_fold_test.dag +++ b/src/v2/test/claim/sql_create_table_fold_test.dag @@ -70,7 +70,7 @@ fn sql_fold_fold_serialize( Holds { value: emitted } => let tree = InferredTree { root: emitted, - facts: Map { lookup: sql_fold_facts_lookup } + facts: PartialFunction { lookup: sql_fold_facts_lookup } } match emit(tree: tree, target: target) { Accepted { value: source, diagnostics: d } => diff --git a/src/v2/test/claim/translate_underived_refusal_test.dag b/src/v2/test/claim/translate_underived_refusal_test.dag index 77ef6a25b40..d0601ae95b5 100644 --- a/src/v2/test/claim/translate_underived_refusal_test.dag +++ b/src/v2/test/claim/translate_underived_refusal_test.dag @@ -135,7 +135,7 @@ fn translate_mixed_tree_facts_lookup(key: Node) -> Optional { data translate_mixed_derived_root_underived_child_tree: InferredTree = InferredTree { root: translate_mixed_tree_root(), - facts: Map { lookup: translate_mixed_tree_facts_lookup } + facts: PartialFunction { lookup: translate_mixed_tree_facts_lookup } } fn translate_absent_parent_underived_child_facts_lookup(key: Node) -> Optional { @@ -148,7 +148,7 @@ fn translate_absent_parent_underived_child_facts_lookup(key: Node) -> Optional Node { @@ -180,7 +180,7 @@ fn translate_bodyless_emission_root_with_poison_child_facts_lookup(key: Node) -> data translate_bodyless_emission_root_with_poison_child_tree: InferredTree = InferredTree { root: translate_bodyless_emission_root_with_poison_child_root(), - facts: Map { lookup: translate_bodyless_emission_root_with_poison_child_facts_lookup } + facts: PartialFunction { lookup: translate_bodyless_emission_root_with_poison_child_facts_lookup } } fn translate_bodied_arrow_shortcut_root() -> Outcome { @@ -218,7 +218,7 @@ fn translate_bodied_arrow_shortcut_underived_descendant_tree() -> Outcome outcome_accepted( value: InferredTree { root: root, - facts: Map { lookup: translate_bodied_arrow_shortcut_facts_lookup } + facts: PartialFunction { lookup: translate_bodied_arrow_shortcut_facts_lookup } } ) } diff --git a/src/v2/test/fixture/rung_3_4_common.dag b/src/v2/test/fixture/rung_3_4_common.dag index 8f62fbc14f7..6c9b767f36d 100644 --- a/src/v2/test/fixture/rung_3_4_common.dag +++ b/src/v2/test/fixture/rung_3_4_common.dag @@ -29,7 +29,7 @@ fn rung34_descent_witness() -> Witness { fn rung34_inferred_tree(root: Node) -> InferredTree { InferredTree { root: root, - facts: Map { + facts: PartialFunction { lookup: fn(n) { Present { value: claim_inferred_facts_from_nodes( diff --git a/src/v2/workflow/orchestration_bash_test.dag b/src/v2/workflow/orchestration_bash_test.dag index 62db72431f3..93c3f8a6ec1 100644 --- a/src/v2/workflow/orchestration_bash_test.dag +++ b/src/v2/workflow/orchestration_bash_test.dag @@ -66,7 +66,7 @@ fn orch_emit_bash(root: Node, target: TargetModel) -> Outcome> { emit( tree: InferredTree { root: root, - facts: Map { lookup: orch_bash_facts_lookup } + facts: PartialFunction { lookup: orch_bash_facts_lookup } }, target: target ) diff --git a/src/v2/workflow/orchestration_retry_emit_test.dag b/src/v2/workflow/orchestration_retry_emit_test.dag index 30bfdd3ed6a..d2a273a3783 100644 --- a/src/v2/workflow/orchestration_retry_emit_test.dag +++ b/src/v2/workflow/orchestration_retry_emit_test.dag @@ -97,7 +97,7 @@ test fn orch_retry_row_direct_emit_accepted_holds() -> Bool { match emit( tree: InferredTree { root: orch_retry_emitted_command, - facts: Map { lookup: orch_retry_probe_facts } + facts: PartialFunction { lookup: orch_retry_probe_facts } }, target: orch_retry_target_model( occ1: "cmd", @@ -321,7 +321,7 @@ test fn orch_retry_escalation_final_row_emit_holds() -> Bool { match emit( tree: InferredTree { root: orch_retry_escalation_final_emitted_command, - facts: Map { lookup: orch_retry_probe_facts } + facts: PartialFunction { lookup: orch_retry_probe_facts } }, target: orch_retry_escalation_final_target_model( occ: "E3=1 cmd", @@ -337,7 +337,7 @@ test fn orch_retry_escalation_step_row_emit_holds() -> Bool { match emit( tree: InferredTree { root: orch_retry_escalation_step_emitted_command, - facts: Map { lookup: orch_retry_probe_facts } + facts: PartialFunction { lookup: orch_retry_probe_facts } }, target: orch_retry_escalation_step_target_model( occ: "E2=1 cmd", @@ -356,7 +356,7 @@ test fn orch_retry_1level_row_direct_emit_accepted_holds() -> Bool { match emit( tree: InferredTree { root: orch_retry_1level_emitted_command, - facts: Map { lookup: orch_retry_probe_facts } + facts: PartialFunction { lookup: orch_retry_probe_facts } }, target: orch_retry_1level_target_model( occ1: "cmd",