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
19 changes: 15 additions & 4 deletions src/v2/test/claim/emit/produced_item_parameter_order_test.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
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.arrow_signature { ArrowParameterOrderMalformed, arrow_declared_parameter_order, 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 }
Expand Down Expand Up @@ -163,9 +163,20 @@ 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]
}

// AN ITEM WHOSE DOMAIN BINDS NAMES BUT CARRIES NO ORDER EDGE IS ILL FORMED (A4, gunbc#12770): such an
// Arrow has no admitted meaning (v2.std.node arrow_signature_edges_conform refuses it at Node
// admission), so the declared-order read answers Malformed for it and the renderer refuses with the
// malformed reason. Before A4 the same Arrow was well formed and refused later, as order ABSENT; the
// refusal moved earlier, it did not go away. The claim pins both the route (the admission wall's
// answer) and the typed refusal, and still reds if the renderer ever accepts the order-less item.
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
let stripped = ipo_without_order(arrow: ipo_item())
match arrow_declared_parameter_order(arrow: stripped) {
ArrowParameterOrderMalformed =>
match produced_decl_subject_from_name_and_arrow(fn_name: ^ipo_f, arrow: stripped) {
Accepted { value: _, diagnostics: _ } => false
Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^produced_decl_render_parameter_order_malformed
}
_ => false
}
}
18 changes: 14 additions & 4 deletions src/v2/test/claim/emit/realized_closure_parameter_order_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module v2.test.claim.emit.realized_closure_parameter_order

import std.occurrence_identity { OccurrenceSynthetic }
import v2.std.collection { List }
import v2.std.arrow_signature { declared_signature }
import v2.std.arrow_signature { ArrowParameterOrderMalformed, arrow_declared_parameter_order, declared_signature }
import v2.std.compilers.target_model { arrow_domain_binder_names, realized_closure_ordered_params }
import v2.std.diagnostic { Accepted, Rejected, diagnostics_fatal_reason }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
Expand Down Expand Up @@ -117,9 +117,19 @@ test fn the_canonical_domain_stored_order_is_not_the_declared_order() -> Bool {
!rcp_is_z_then_a(xs: arrow_domain_binder_names(arrow: rcp_canonical_domain(arrow: rcp_closure())))
}

// A CLOSURE WHOSE DOMAIN BINDS NAMES BUT CARRIES NO ORDER EDGE IS ILL FORMED (A4, gunbc#12770): the
// declared-order read answers Malformed at the admission wall (v2.std.node
// arrow_signature_edges_conform), and the closure realization refuses with the malformed reason --
// earlier than the order-ABSENT refusal it reached before A4. The claim pins the wall's answer and
// the typed refusal, and still reds if the order-less closure is ever realized.
test fn a_closure_with_named_parameters_and_no_order_refuses_typed() -> Bool {
match realized_closure_ordered_params(closure: rcp_without_order(arrow: rcp_closure())) {
Accepted { value: _, diagnostics: _ } => false
Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^target_value_expr_reason_closure_parameter_order_absent
let stripped = rcp_without_order(arrow: rcp_closure())
match arrow_declared_parameter_order(arrow: stripped) {
ArrowParameterOrderMalformed =>
match realized_closure_ordered_params(closure: stripped) {
Accepted { value: _, diagnostics: _ } => false
Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^target_value_expr_reason_closure_parameter_order_malformed
}
_ => false
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,10 @@ import v2.std.decl_index {
export_signature_facts,
export_signature_facts_host_scaffold_dissolution_trigger
}
import v2.std.arrow_signature { ArrowParameterOrderAbsent, ArrowParameterOrderDeclared, arrow_declared_parameter_order }
import v2.std.arrow_signature { ArrowParameterOrderDeclared, ArrowParameterOrderMalformed, arrow_declared_parameter_order }
import v2.std.anonymous_binder { anonymous_param_label }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.node { Arrow, Atom, Conj, Edge, Named, Node, Positional, TypeNode, symbol_intern_lexeme }
import v2.std.node { Arrow, Atom, Conj, Edge, Named, Node, Positional, TypeNode, arrow_signature_order_label, edge_label_of, symbol_intern_lexeme }
import std.occurrence_identity { OccurrenceSynthetic }
import v2.std.logic { Bool }
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }
Expand Down Expand Up @@ -152,15 +152,20 @@ test fn exported_signature_carries_named_binders_and_declared_order() -> Bool {

// THE ROUTE, NOT ONLY THE ANSWER: the host seam's own Arrow carries no order edge, so the order above
// exists only because the lift passed it through declared_signature. Deleting the lift reddens the
// claim above; this one pins that the host did not mint a second order constructor.
// claim above; this one pins that the host did not mint a second order constructor -- read
// STRUCTURALLY, as no edge carrying the order label. Since A4 (gunbc#12770) a domain that binds names
// and carries no order edge is ill formed, so the declared-order read answers Malformed for the raw
// host Arrow (it answered Absent before): that is why the raw seam value is consumed ONLY through
// export_signature_declared_facts, whose lift is the one constructor that makes it well formed.
test fn export_signature_host_seam_mints_no_order_edge() -> Bool {
match firewall_ordered_fact(facts: export_signature_facts(pool_roots: firewall_order_roots)) {
Absent => false
Present { value: fact } =>
match arrow_declared_parameter_order(arrow: fact.node) {
ArrowParameterOrderAbsent => true
_ => false
}
!fold(fact.node.children, init: false, f: fn(acc, e) { acc || (edge_label_of(e: e) == arrow_signature_order_label) })
&& match arrow_declared_parameter_order(arrow: fact.node) {
ArrowParameterOrderMalformed => true
_ => false
}
}
}

Expand Down