Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/v2/compiler/body_lowering_fold.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 `<anonymous-parameter-N>` 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.
Expand Down
6 changes: 4 additions & 2 deletions src/v2/std/arrow_signature.dag
Original file line number Diff line number Diff line change
Expand Up @@ -70,8 +70,10 @@ fn declared_signature(params: List<Edge>, 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
Expand Down
87 changes: 81 additions & 6 deletions src/v2/std/compilers/target_model.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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<List<Edge>> {
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<Edge> {
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
Expand All @@ -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 =>
Expand Down Expand Up @@ -15417,7 +15492,7 @@ fn symbol_list_contains(xs: List<Symbol>, 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
Expand Down
170 changes: 170 additions & 0 deletions src/v2/test/claim/emit/produced_item_parameter_order_test.dag
Original file line number Diff line number Diff line change
@@ -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<Edge>
}

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<Edge>) -> List<Symbol> {
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<Edge>) -> 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<Edge>) -> 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<Edge> {
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
}
}
Loading