diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 789f4c1250c..6cc6a7fb670 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -4040,8 +4040,8 @@ fn body_lower_function_value_type_var_atom(tv: Symbol) -> Node { // THE DOMAIN AND ITS DECLARED ORDER COME OUT OF THE ONE PARAMETER-LIST MINT (v2.std.anonymous_binder // anonymous_binder_mint_parameter_list), exactly as a named fn's do: every binder the author spelled // `_` is relabelled `` by its slot, every other binder keeps its name, and the -// labels' authored order is carried beside the domain, because the domain is a Conj sorted by label -// and cannot carry it. The minted labels then key both the domain edge and its fresh type parameter. +// labels' authored order is carried beside the domain, because the domain is a Conj -- a set of +// labelled binders that canonicalization sorts by label -- and cannot carry it. The minted labels then key both the domain edge and its fresh type parameter. // The mint relabels Named edges and passes any other edge through unchanged, so every edge here is // Named; one that were not would be kept in the domain as is, where v2.std.node edges_conform refuses // a Positional edge in a record -- loudly. diff --git a/src/v2/std/arrow_signature.dag b/src/v2/std/arrow_signature.dag index aa4edb75488..e9645c966b2 100644 --- a/src/v2/std/arrow_signature.dag +++ b/src/v2/std/arrow_signature.dag @@ -70,8 +70,10 @@ fn declared_signature(params: List, source: Node) -> DeclaredSignatureEdge // THE ONE READER OF DECLARED PARAMETER ORDER, and the only thing positional binding may read it from. // An Arrow built from a declared signature carries one ^arrow_signature_order_edge whose target is a -// FreeMonoid introduction of its parameter labels (signature_order_edge). ArrowParameterOrderAbsent is not a fallback to label order: the -// domain is a Conj sorted by label, so its stored sequence is not the declared one, and a binder +// FreeMonoid introduction of its parameter labels (signature_order_edge). ArrowParameterOrderAbsent is not a fallback to domain order: +// the domain is a Conj, a set of labelled binders whose stored sequence is not a fact about the +// signature (lowering keeps the authored sequence, canonicalization sorts it by label -- v2.std.node +// arrow_signature_order_conforms), so no reader may take positions from it, and a binder // that finds no order edge refuses (v2.compiler.infer infer_application_formals, // v2.compiler.eval eval_bind_arrow_params). type ArrowParameterOrder diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index 1e33f083511..a781162263d 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -142,9 +142,13 @@ import v2.std.witness { } import v2.std.anonymous_binder { is_anonymous_param_label } import v2.std.node_query { + NamedChildAmbiguous, + NamedChildFound, + NamedChildMissing, arrow_domain_named_param_bindings, find_arrow_body_child, find_named_child, + named_child_lookup, node_labeled_child_edges, node_positional_child_targets, nullary_inhabitant_by_discriminant, @@ -671,6 +675,72 @@ fn produced_decl_signature_segments_tokens( ) } +// A FUNCTION ITEM'S PARAMETERS, IN DECLARED ORDER. The item is called positionally, so its emitted +// parameter list is the Arrow's declared order (v2.std.arrow_signature arrow_declared_parameter_order, +// the one reader of ^arrow_signature_order_edge) -- never the domain Conj's stored sequence, which is +// a set's storage and which canonicalization sorts by label. The domain is read only for MEMBERSHIP: +// each declared label selects its binder edge, so the parameter's type still comes from the domain. +// A domain that binds named parameters but carries no readable order refuses typed; there is no +// domain-order fallback. A domain that binds no name -- a function TYPE's positional product, or a +// lone parameter type (produced_decl_function_type_domain_edges) -- has no labels to order: its +// positional edges are the sequence, so its children pass through. A domain mixing named and +// positional edges is neither and refuses as malformed rather than dropping the positional ones. +fn produced_decl_ordered_params(arrow: Node, domain: Node) -> Outcome> { + match arrow_domain_binder_names(arrow: arrow) { + Empty => outcome_accepted(value: domain.children) + Cons { head: _, tail: _ } => + match arrow_declared_parameter_order(arrow: arrow) { + ArrowParameterOrderDeclared { labels: labels } => + if length(xs: labels) != length(xs: domain.children) { + outcome_rejected( + d: produced_decl_render_diagnostic(reason: ^produced_decl_render_parameter_order_malformed, node: arrow) + ) + } else { + fold_list( + xs: labels, + empty: outcome_accepted(value: Empty), + cons: fn(acc, label) { + bind_outcome( + o: acc, + f: fn(so_far) { + bind_outcome( + o: produced_decl_domain_binder(arrow: arrow, domain: domain, label: label), + f: fn(edge) { outcome_accepted(value: list_snoc_item(xs: so_far, item: edge)) } + ) + } + ) + } + ) + } + ArrowParameterOrderAbsent => + outcome_rejected( + d: produced_decl_render_diagnostic(reason: ^produced_decl_render_parameter_order_absent, node: arrow) + ) + ArrowParameterOrderMalformed => + outcome_rejected( + d: produced_decl_render_diagnostic(reason: ^produced_decl_render_parameter_order_malformed, node: arrow) + ) + } + } +} + +// The membership read: the one domain binder a declared label names. arrow_declared_parameter_order +// admits only an order that is a permutation of the domain's binders, so a missing or repeated +// binder here is a wall the reader already holds; it still refuses typed rather than dropping one. +fn produced_decl_domain_binder(arrow: Node, domain: Node, label: Symbol) -> Outcome { + match named_child_lookup(root: domain, name: label) { + NamedChildFound { target: t } => outcome_accepted(value: Edge { label: Named { name: label }, target: t }) + NamedChildMissing => + outcome_rejected( + d: produced_decl_render_diagnostic(reason: ^produced_decl_render_parameter_order_malformed, node: arrow) + ) + NamedChildAmbiguous => + outcome_rejected( + d: produced_decl_render_diagnostic(reason: ^produced_decl_render_parameter_order_malformed, node: arrow) + ) + } +} + fn produced_decl_subject_from_name_and_arrow( fn_name: Symbol, arrow: Node @@ -679,11 +749,16 @@ fn produced_decl_subject_from_name_and_arrow( Present { value: domain } => match list_at_optional(xs: node_positional_child_targets(node: arrow), index: 1) { Present { value: codomain } => - outcome_accepted( - value: ProducedDeclSignatureSubject { - fn_name: fn_name, - params: domain.children, - codomain: codomain + bind_outcome( + o: produced_decl_ordered_params(arrow: arrow, domain: domain), + f: fn(params) { + outcome_accepted( + value: ProducedDeclSignatureSubject { + fn_name: fn_name, + params: params, + codomain: codomain + } + ) } ) Absent => @@ -15417,7 +15492,7 @@ fn symbol_list_contains(xs: List, wanted: Symbol) -> Bool { // A RETURNED CLOSURE'S PARAMETERS, IN DECLARED ORDER. The emitted closure is applied positionally, // so its parameter list is the Arrow's declared order (v2.std.compilers.body_lowering // arrow_declared_parameter_order, the one reader of ^arrow_signature_order_edge) -- never the domain -// Conj's stored sequence, which is sorted by label and is not the signature (#12361). Scope +// Conj's stored sequence, which canonicalization sorts by label and is not the signature (#12361). Scope // MEMBERSHIP for captures stays arrow_domain_binder_names, an unordered set question. A domain that // binds names but carries no readable order refuses typed, exactly as eval's // eval_param_labels_in_declared_order does: there is no domain-order fallback. A domain that binds diff --git a/src/v2/test/claim/emit/produced_item_parameter_order_test.dag b/src/v2/test/claim/emit/produced_item_parameter_order_test.dag new file mode 100644 index 00000000000..693934792f3 --- /dev/null +++ b/src/v2/test/claim/emit/produced_item_parameter_order_test.dag @@ -0,0 +1,170 @@ +module v2.test.claim.emit.produced_item_parameter_order + +import v2.std.collection { Absent, List, Present, list_at_optional } +import v2.std.arrow_signature { declared_signature } +import v2.std.compilers.target_model { ProducedDeclSignatureSubject, arrow_domain_binder_names, produced_decl_subject_from_name_and_arrow } +import v2.std.diagnostic { Accepted, Rejected, diagnostics_fatal_reason } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { + Arrow, + Atom, + Edge, + Named, + Node, + Positional, + Symbol, + TypeNode, + canonicalize_node_for_content_hash, + node_synthetic +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A FUNCTION ITEM IS EMITTED WITH ITS PARAMETERS IN DECLARED ORDER, asked at its one interface +// (DESIGN section 3's witness rule) with supplied item Arrows: an item is called positionally, so +// v2.std.compilers.target_model produced_decl_subject_from_name_and_arrow -- the subject every +// produced declaration's signature is rendered from -- must list the Arrow's declared order, not its +// domain Conj's stored sequence. The specimen declares (z: Int, a: Bool): its domain is built by the +// declared-signature constructor lowering uses (v2.std.arrow_signature declared_signature), and a +// second copy has only its domain canonicalized. Both denote the same function, so both must answer +// [z, a] with z still typed Int; the stored-order read of the canonical domain answers [a, z] +// (asserted below as the mutation this claim discriminates). The real path -- a real module through +// the production front end into this renderer, whose emitted text is compared to a golden -- is +// already executed by v2.test.emit.rust_produced_decl_emit rust_produced_decl_name_discriminates and +// v2.test.long.emit_host_produced_module_equals_eval produced_module_two_distinct_fns_assemble; with +// this reader in place both reach it through the declared-order arm (their decls carry an order +// edge), so they are this interface's inhabitance claims. A second real-module claim here would +// re-pay the whole front end for no discrimination: lowering keeps the authored sequence, so no +// real module can tell a stored-order read from a declared-order one. +fn ipo_atom(id: Symbol) -> Node { + node_synthetic(kind: TypeNode { connective: Atom { identity: id } }, children: []) +} + +fn ipo_item() -> Node { + let sig = declared_signature( + params: [ + Edge { label: Named { name: ^ipo_z }, target: ipo_atom(id: ^ipo_int) }, + Edge { label: Named { name: ^ipo_a }, target: ipo_atom(id: ^ipo_bool) } + ], + source: ipo_atom(id: ^ipo_source) + ) + node_synthetic( + kind: TypeNode { connective: Arrow }, + children: [ + sig.domain, + Edge { label: Positional, target: ipo_atom(id: ^ipo_int) }, + sig.order, + Edge { label: Named { name: ^arrow_body_edge }, target: ipo_atom(id: ^ipo_z) } + ] + ) +} + +type IpoDomainWalk { + done: Bool + edges: List +} + +fn ipo_canonical_domain(arrow: Node) -> Node { + let seen = fold(arrow.children, init: IpoDomainWalk { done: false, edges: [] }, f: fn(acc, e) { + match e.label { + Positional => + if acc.done { + IpoDomainWalk { done: true, edges: concat(acc.edges, [e]) } + } else { + IpoDomainWalk { done: true, edges: concat(acc.edges, [Edge { label: Positional, target: canonicalize_node_for_content_hash(n: e.target) }]) } + } + Named { name: _ } => IpoDomainWalk { done: acc.done, edges: concat(acc.edges, [e]) } + } + }) + Node { kind: arrow.kind, children: seen.edges, occurrence_id: arrow.occurrence_id } +} + +fn ipo_without_order(arrow: Node) -> Node { + Node { + kind: arrow.kind, + children: fold(arrow.children, init: [], f: fn(acc, e) { + match e.label { + Named { name: sym } => if sym == ^arrow_signature_order_edge { acc } else { concat(acc, [e]) } + Positional => concat(acc, [e]) + } + }), + occurrence_id: arrow.occurrence_id + } +} + +// Each parameter as its label then its type atom, so the claim reads order AND the binding of each +// label to its own type. +fn ipo_param_symbols(params: List) -> List { + fold(params, init: [], f: fn(acc, e) { + let name = match e.label { + Named { name: n } => n + Positional => ^ipo_positional + } + let ty = match e.target.kind { + TypeNode { connective: Atom { identity: t } } => t + _ => ^ipo_not_an_atom + } + concat(acc, [name, ty]) + }) +} + +fn ipo_is_z_int_then_a_bool(params: List) -> Bool { + ipo_param_symbols(params: params) == [^ipo_z, ^ipo_int, ^ipo_a, ^ipo_bool] +} + +fn ipo_ordered(arrow: Node) -> Bool { + match produced_decl_subject_from_name_and_arrow(fn_name: ^ipo_f, arrow: arrow) { + Accepted { value: subject, diagnostics: _ } => ipo_is_z_int_then_a_bool(params: subject.params) + Rejected { diagnostics: _ } => false + } +} + +test fn an_item_emits_its_parameters_in_declared_order() -> Bool { + ipo_ordered(arrow: ipo_item()) +} + +test fn a_domain_canonicalized_item_emits_the_same_parameter_order() -> Bool { + ipo_ordered(arrow: ipo_canonical_domain(arrow: ipo_item())) +} + +// POSITIONAL BEHAVIOR AT A CALL SITE, not only an equal-looking list. The emitted item is applied +// positionally: the k-th actual of a call f(first, second) binds the k-th rendered parameter. So the +// rendered list is read as the call does -- zipped against the actuals in order -- and z, the first +// declared parameter, must receive the FIRST actual on the original item AND on the +// domain-canonicalized copy, and the two copies must render the identical parameter list. A +// renderer that read the canonical domain's stored order would bind z to the second actual. +fn ipo_bound_to_first_actual(params: List) -> Symbol { + match list_at_optional(xs: ipo_param_symbols(params: params), index: 0) { + Present { value: n } => n + Absent => ^ipo_no_parameter + } +} + +fn ipo_rendered_params(arrow: Node) -> List { + match produced_decl_subject_from_name_and_arrow(fn_name: ^ipo_f, arrow: arrow) { + Accepted { value: subject, diagnostics: _ } => subject.params + Rejected { diagnostics: _ } => [] + } +} + +test fn a_positional_call_binds_z_to_the_first_actual_on_both_copies() -> Bool { + let original = ipo_rendered_params(arrow: ipo_item()) + let canonical = ipo_rendered_params(arrow: ipo_canonical_domain(arrow: ipo_item())) + ipo_bound_to_first_actual(params: original) == ^ipo_z + && ipo_bound_to_first_actual(params: canonical) == ^ipo_z + && ipo_param_symbols(params: original) == ipo_param_symbols(params: canonical) +} + +// THE MUTATION THIS DISCRIMINATES: the stored-order read of the canonical domain is [a, z], so a +// renderer restoring domain.children as the parameter list fails the claim above. +test fn the_canonical_domain_stored_order_is_not_the_declared_order() -> Bool { + arrow_domain_binder_names(arrow: ipo_canonical_domain(arrow: ipo_item())) == [^ipo_a, ^ipo_z] +} + +test fn an_item_with_parameters_and_no_order_refuses_typed() -> Bool { + match produced_decl_subject_from_name_and_arrow(fn_name: ^ipo_f, arrow: ipo_without_order(arrow: ipo_item())) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^produced_decl_render_parameter_order_absent + } +}