diff --git a/dag/gunbc/ci_workflow.dag b/dag/gunbc/ci_workflow.dag index 34a2ca0765b..6ea3c7ce090 100644 --- a/dag/gunbc/ci_workflow.dag +++ b/dag/gunbc/ci_workflow.dag @@ -479,7 +479,7 @@ data gunbc_ci_job_timeout_policy_minutes: Int = 90 data gunbc_ci_floor_step_timeout_minutes: Duration = 270 -data gunbc_ci_floor_step_timeout_discovery_flip_note: String = "-> 270 at PR #6464 receipt run 29151777611 (2026-07-11): 180m step cap still timed out mid batch 2 — 1535 SKIP rows finished @ 12:35:43, then ~147m silent witness-execution phase until the 180m kill @ 15:03:12 with batch 2 never completing (~177m in-batch from 12:06:38; ~443 non-skipped rows in roster of 1978). Prior -> 180 at run 29148344466 (~116m in-batch, ~87m post-skip). Prior -> 120 at run 29145270700. Prior -> 90 at run 29141663541. Prior -> 90 at body_lowering normalize hook (#6459 receipt run 29148735992 @ 3a372b7: floor step timed out at 60m MID discovery corpus after ~320 SKIP lines — batch-1 compile-clean normalize reconcile ~263s with body_lowering_fold in the normalize import closure; discovery still resolves every unique entry file before skip, so resolve->normalize pulled the ~1.3k-line scaffold into most closure walks). Structural fix on the same lane: NormalizedTree moved to v2.compiler.normalized_tree so v2.compiler.resolve no longer imports normalize (dissolve-on: skip-before-resolve so skipped rows never pay entry resolve). Prior step budget -> 60 at the discovery flip (gunbc.ci_spec ci_spec_discovery_flip_note; authored as 30 -> 60 on #6403, main had meanwhile bumped 30 -> 45 with the #6422 enrollments): the corpus discovery batch adds a whole-tree resolve plus the always-run live-tree rows to the floor step. Discovery corpus spawn_width_cap stays pinned to 1 (ci_corpus_discovery_spawn_width_cap in v2.workflow.ci_floor_plan): at width W the executor holds the parent's process-shared index PLUS W private shard indexes ((1+W) x whole-tree residency; width=2 OOM receipt run 28999086030), while width=1 runs rows on the main thread against the ONE shared index (union-resolve S1). CORRECTED RECEIPT (2026-07-10): run 29000557166's floor did NOT complete - the executor was host-OOM-killed ~8min in, MID discovery corpus (the log's later ExitSuccess belongs to the merge-admission STAMP tool, which stamped CI_FLOOR_EXIT=137); no flipped corpus has completed in CI yet - the only completion receipt is local (33.5GiB container, ~40min at width 5). The kill vector is host-level oversubscription (see gunbc_falsifier_plan_spawn_width_note), not this width model. #6475 receipt run 29143617420 @ 0c0f73: batch-1 compile-clean ~4m green; batch-2 discovery killed at 90m step cap mid-manual (last skip rust_wire_serde @ 07:47:49; ~15GiB peak). #6475 receipt run 29146814967 @ 6a61fce: same stall at 120m (last skip rust_wire_serde @ 09:34:49; ~85m silent eval). #6475 receipt run 29150477894 @ 6cd5326: same stall at 180m (last skip rust_wire_serde @ 11:43:46; ~88m silent eval) — local gunbc run on s1_closure_parses_holds reads 3/40 closure paths in 10m before timeout, matching the silent-eval class (live filesystem_read per path, not a skip-logged row). #6475 receipt run 29161709373 @ 9d9852c: batch-1 compile-clean refused — gunbc_ci_floor_step_timeout_discovery_flip_note string literal terminated early at col 2043 (body_lowering suffix spliced after closing quote during rebase merge); restored single-line literal on rebase to main #6464 note. Revisit down when floor memoization / resolver graph-major shrink the resolve wall; the affected-set selection receipts (skip counts per PR) are the cost dial to watch." +data gunbc_ci_floor_step_timeout_discovery_flip_note: String = "-> 270 restored 2026-07-12 on #6512 after 60m fail-fast regressed merge CI (receipt run 29197126623 @ 35f212fa5d: 60m step kill with 0 witness FAILs — batch-1 compile-clean PASS @ 15:01, batch-2 skip walk ~26m to recompute_trace_probe_test, then ~34m silent eval until kill; same serial-floor-wall class as 29183446733). Prior -> 60 operator ruling 2026-07-12: lower floor step cap from 270m so CI fails fast while the serial floor wall is debugged separately (receipt run 29183446733 @ 2e856a5617: 270m kill with 0 witness FAILs, batch-2 still in discovery SKIP walk). Prior -> 270 at PR #6464 receipt run 29151777611 (2026-07-11): 180m step cap still timed out mid batch 2 — 1535 SKIP rows finished @ 12:35:43, then ~147m silent witness-execution phase until the 180m kill @ 15:03:12 with batch 2 never completing (~177m in-batch from 12:06:38; ~443 non-skipped rows in roster of 1978). Prior -> 180 at run 29148344466 (~116m in-batch, ~87m post-skip). Prior -> 120 at run 29145270700. Prior -> 90 at run 29141663541. Prior -> 90 at body_lowering normalize hook (#6459 receipt run 29148735992 @ 3a372b7: floor step timed out at 60m MID discovery corpus after ~320 SKIP lines — batch-1 compile-clean normalize reconcile ~263s with body_lowering_fold in the normalize import closure; discovery still resolves every unique entry file before skip, so resolve->normalize pulled the ~1.3k-line scaffold into most closure walks). Structural fix on the same lane: NormalizedTree moved to v2.compiler.normalized_tree so v2.compiler.resolve no longer imports normalize (dissolve-on: skip-before-resolve so skipped rows never pay entry resolve). Prior step budget -> 60 at the discovery flip (gunbc.ci_spec ci_spec_discovery_flip_note; authored as 30 -> 60 on #6403, main had meanwhile bumped 30 -> 45 with the #6422 enrollments): the corpus discovery batch adds a whole-tree resolve plus the always-run live-tree rows to the floor step. Discovery corpus spawn_width_cap stays pinned to 1 (ci_corpus_discovery_spawn_width_cap in v2.workflow.ci_floor_plan): at width W the executor holds the parent's process-shared index PLUS W private shard indexes ((1+W) x whole-tree residency; width=2 OOM receipt run 28999086030), while width=1 runs rows on the main thread against the ONE shared index (union-resolve S1). CORRECTED RECEIPT (2026-07-10): run 29000557166's floor did NOT complete - the executor was host-OOM-killed ~8min in, MID discovery corpus (the log's later ExitSuccess belongs to the merge-admission STAMP tool, which stamped CI_FLOOR_EXIT=137); no flipped corpus has completed in CI yet - the only completion receipt is local (33.5GiB container, ~40min at width 5). The kill vector is host-level oversubscription (see gunbc_falsifier_plan_spawn_width_note), not this width model. #6475 receipt run 29143617420 @ 0c0f73: batch-1 compile-clean ~4m green; batch-2 discovery killed at 90m step cap mid-manual (last skip rust_wire_serde @ 07:47:49; ~15GiB peak). #6475 receipt run 29146814967 @ 6a61fce: same stall at 120m (last skip rust_wire_serde @ 09:34:49; ~85m silent eval). #6475 receipt run 29150477894 @ 6cd5326: same stall at 180m (last skip rust_wire_serde @ 11:43:46; ~88m silent eval) — local gunbc run on s1_closure_parses_holds reads 3/40 closure paths in 10m before timeout, matching the silent-eval class (live filesystem_read per path, not a skip-logged row). #6475 receipt run 29161709373 @ 9d9852c: batch-1 compile-clean refused — gunbc_ci_floor_step_timeout_discovery_flip_note string literal terminated early at col 2043 (body_lowering suffix spliced after closing quote during rebase merge); restored single-line literal on rebase to main #6464 note. Revisit down when floor memoization / resolver graph-major shrink the resolve wall; the affected-set selection receipts (skip counts per PR) are the cost dial to watch." data gunbc_ci_step_timeout_measure_grounding_disposition: Disposition = Scaffold { dissolves_to: SingleAuthority, diff --git a/src/v2/compiler/03_normalize.dag b/src/v2/compiler/03_normalize.dag index 91ce1cc405e..894fea379c6 100644 --- a/src/v2/compiler/03_normalize.dag +++ b/src/v2/compiler/03_normalize.dag @@ -33,7 +33,10 @@ import v2.std.compilers.sugar { apply_sugar, sugar_rule_for_key } -import v2.compiler.body_lowering_fold { body_lower_finish } +import v2.compiler.body_lowering_fold { + body_lower_finish, + body_lower_is_deferred_lower_emitted +} import v2.compiler.normalized_tree { NormalizedTree } import v2.extdeps.languages.dag { parse_production_emitted_identity_optional @@ -114,6 +117,22 @@ fn normalize_sugar_finish(n: Node, folded: Node, cd: Diagnostics) -> Outcome Outcome { + match parse_production_emitted_identity_optional(node: n) { + Present { value: emitted } => + if body_lower_is_deferred_lower_emitted(emitted: emitted) { + match body_lower_finish(n: n, folded: n, cd: None) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: after_body, diagnostics: cd0 } => + normalize_sugar_finish(n: n, folded: after_body, cd: cd0) + } + } else { + normalize_node_fold_children(n: n) + } + Absent => normalize_node_fold_children(n: n) + } +} + +fn normalize_node_fold_children(n: Node) -> Outcome { match fold(n.children, init: normalize_fold_init(n: n), f: fn(acc, e) { normalize_fold_step(acc: acc, edge: e, child: normalize_node(n: e.target)) }) { diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index b904296a4cd..de9a07ee2a9 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -14,7 +14,9 @@ import v2.std.collection { Map, Optional, Present, - list_at_optional + list_at_optional, + optional_absent, + optional_present } import v2.std.constraints { CanonicalGrounding, @@ -34,6 +36,7 @@ import v2.std.diagnostic { Accepted, None, Rejected, + Some, bind_outcome, diagnostics_merge, diagnostics_singleton, @@ -43,12 +46,15 @@ import v2.std.diagnostic { } import v2.std.logic { Bool, bool_node } import v2.std.node { + Arrow, Atom, Branch, ComputationNode, + Conj, Edge, Loop, Match, + Named, Node, NodeFold, Symbol, @@ -214,6 +220,14 @@ fn infer_match_non_exhaustive_diagnostic(node: Node) -> Diagnostic { } } +fn infer_match_int_scrutinee_bool_literal_scaffold_diagnostic(node: Node) -> Diagnostic { + Diagnostic { + reason: ^infer_match_int_scrutinee_bool_literal_scaffold, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + fn algebra_ref_is_grounded(algebra: Node) -> Bool { match algebra.kind { TypeNode { connective: c } => @@ -457,16 +471,90 @@ fn infer_branch_is_int_literal_atom(node: Node) -> Bool { } } -fn infer_branch_operand_resolved_type(node: Node, facts: InferredFacts) -> Node { +fn infer_atom_binding_sym(node: Node) -> Optional { + match node.kind { + TypeNode { connective: Atom { identity: sym } } => Present { value: sym } + _ => Absent + } +} + +fn infer_conj_edge_named_type_for_binding(edge: Edge, binding: Symbol) -> Optional { + match edge.label { + Named { name: sym } => + if sym == binding { + optional_present(value: edge.target) + } else { + optional_absent() + } + Positional => optional_absent() + } +} + +fn infer_conj_named_type_for_binding(domain: Node, binding: Symbol) -> Optional { + match domain.kind { + TypeNode { connective: Conj } => + fold(domain.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => infer_conj_edge_named_type_for_binding(edge: e, binding: binding) + } + }) + _ => Absent + } +} + +fn infer_arrow_domain_type_for_binding(arrow: Node, binding: Symbol) -> Optional { + match arrow.kind { + TypeNode { connective: Arrow } => + match list_at_optional(xs: node_positional_child_targets(node: arrow), index: 0) { + Present { value: domain } => + infer_conj_named_type_for_binding(domain: domain, binding: binding) + Absent => Absent + } + _ => Absent + } +} + +data infer_arrow_domain_binding_heuristic_note: String = "interim: infer_find_arrow_domain_type_in_tree DFS-walks the resolved tree for the first Arrow whose Conj domain names the atom-binding symbol — symbol-name collision across unrelated arrows picks first-visit order, not lexical scope. dissolve-on: namespace-only name resolution consumes containment-tree binding→domain (DESIGN open thread §namespace-only); delete this heuristic walker when SymbolIndex lookup lands." + +fn infer_find_arrow_domain_type_in_tree(root: Node, binding: Symbol) -> Optional { + match infer_arrow_domain_type_for_binding(arrow: root, binding: binding) { + Present { value: ty } => Present { value: ty } + Absent => + fold(root.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => infer_find_arrow_domain_type_in_tree(root: e.target, binding: binding) + } + }) + } +} + +fn infer_branch_operand_resolved_type_in_tree( + node: Node, + facts: InferredFacts, + tree: Node, +) -> Node { if infer_branch_is_bool_literal_atom(node: node) { bool_node() } else if infer_branch_is_int_literal_atom(node: node) { infer_branch_int_binding_type_node() } else { - inferred_facts_resolved_type(facts: facts) + match infer_atom_binding_sym(node: node) { + Present { value: binding } => + match infer_find_arrow_domain_type_in_tree(root: tree, binding: binding) { + Present { value: domain_ty } => domain_ty + Absent => inferred_facts_resolved_type(facts: facts) + } + Absent => inferred_facts_resolved_type(facts: facts) + } } } +fn infer_branch_operand_resolved_type(node: Node, facts: InferredFacts) -> Node { + infer_branch_operand_resolved_type_in_tree(node: node, facts: facts, tree: node) +} + fn infer_branch_canonical_grounding(node: Node, unified_type: Node) -> CanonicalGrounding { CanonicalGrounding { node: node, @@ -501,6 +589,115 @@ fn infer_branch_type_is_bool(type_node: Node) -> Bool { } } +fn infer_branch_type_is_int(type_node: Node) -> Bool { + match type_node.kind { + TypeNode { connective: Atom { identity: id } } => id == ^dag_binding_type_int + _ => false + } +} + +data infer_match_int_scrutinee_bool_literal_body_note: String = "Int-scrutinee bool-literal match arms ground body type as Int at arm-row construction (same octet 0/1 authority as eval allocate_literal), not a post-unification rewrite. dissolve-on: bool keywords carry Int type in Int-valued match bodies at normalize/ingest. scaffold-widen: Int scrutinee on bool-literal match emits infer_match_int_scrutinee_bool_literal_scaffold diagnostic (countable on Accepted path). paired-scaffold: emit half = target_value_expr_int_bool_octet_channel_dissolution_note (target_model.dag) — dissolve both halves together on octet↔bool codec inhabitation." + +fn infer_match_bool_consumer_diagnostics_with_int_scrutinee_scaffold( + consumer: Node, + cd: Diagnostics, + scrutinee_type: Node +) -> Diagnostics { + if infer_branch_type_is_int(type_node: scrutinee_type) { + diagnostics_merge( + outer: cd, + inner: Some { + diagnostics: diagnostics_singleton( + d: infer_match_int_scrutinee_bool_literal_scaffold_diagnostic(node: consumer) + ) + } + ) + } else { + cd + } +} + +fn infer_match_bool_arm_body_type( + body_target: Node, + body_facts: InferredFacts, + scrutinee_type: Node +) -> Node { + if infer_branch_type_is_int(type_node: scrutinee_type) + && infer_branch_is_bool_literal_atom(node: body_target) { + infer_branch_int_binding_type_node() + } else { + infer_branch_operand_resolved_type(node: body_target, facts: body_facts) + } +} + +fn infer_match_bool_arm_rows_accept( + node: Node, + partials: List, + entries: List, + first_arm_target: Node, + second_arm_target: Node, + cd: Diagnostics, + scrutinee_type: Node +) -> Outcome { + match infer_match_bool_arm_row( + arm: first_arm_target, + entries: entries, + scrutinee_type: scrutinee_type + ) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: first_row, diagnostics: fd } => + match infer_match_bool_arm_row( + arm: second_arm_target, + entries: entries, + scrutinee_type: scrutinee_type + ) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: second_row, diagnostics: sd } => + let first_body = first_row.body_type + let second_body = second_row.body_type + match infer_bool_literal_exhaustiveness_merge( + left: first_row.coverage, + right: second_row.coverage + ) { + InferBoolLiteralExhaustive => + if !infer_branch_type_atoms_equal(a: first_body, b: second_body) { + outcome_rejected(infer_match_arm_type_mismatch_diagnostic(node: node)) + } else { + match infer_descent_witness_for_node(n: node) { + Violates { diagnostic: d } => + Rejected { diagnostics: diagnostics_singleton(d: d) } + Holds { value: descent_proof } => + bind_outcome( + o: inferred_facts_from_grounding( + grounding: infer_branch_canonical_grounding( + node: node, + unified_type: first_body + ), + descent: Holds { value: descent_proof } + ), + f: fn(facts) { + Accepted { + value: facts, + diagnostics: diagnostics_merge( + outer: diagnostics_merge(outer: cd, inner: fd), + inner: sd + ) + } + } + ) + } + } + InferBoolLiteralMissingTrue => + outcome_rejected(infer_match_non_exhaustive_diagnostic(node: node)) + InferBoolLiteralMissingFalse => + outcome_rejected(infer_match_non_exhaustive_diagnostic(node: node)) + InferBoolLiteralMissingBoth => + outcome_rejected(infer_match_non_exhaustive_diagnostic(node: node)) + } + } + } +} + fn infer_unify_branch_arm_types( then_node: Node, then_facts: InferredFacts, @@ -676,6 +873,7 @@ fn infer_bool_literal_exhaustiveness_merge( fn infer_match_bool_arm_row( arm: Node, entries: List, + scrutinee_type: Node ) -> Outcome { match arm.kind { TypeNode { connective: Conj } => @@ -698,9 +896,10 @@ fn infer_match_bool_arm_row( Accepted { value: InferMatchArmRow { coverage: coverage, - body_type: infer_branch_operand_resolved_type( - node: body_target, - facts: body_facts + body_type: infer_match_bool_arm_body_type( + body_target: body_target, + body_facts: body_facts, + scrutinee_type: scrutinee_type ) }, diagnostics: diagnostics_merge(outer: pd, inner: bd) @@ -717,6 +916,7 @@ fn infer_match_bool( node: Node, partials: List, entries: List, + tree: Node, ) -> Outcome { let positional_targets = node_positional_child_targets(node: node) if !all_edges_positional(children: node.children) || length(xs: positional_targets) != 3 { @@ -737,64 +937,28 @@ fn infer_match_bool( match infer_bounded_lattice_consumer_gate(consumer: node, partials: partials) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: _, diagnostics: cd } => - if !infer_branch_type_is_bool( - type_node: infer_branch_operand_resolved_type( - node: scrutinee_target, - facts: scrutinee_facts + let scrutinee_type = infer_branch_operand_resolved_type_in_tree( + node: scrutinee_target, + facts: scrutinee_facts, + tree: tree + ) + if infer_branch_type_is_bool(type_node: scrutinee_type) + || infer_branch_type_is_int(type_node: scrutinee_type) { + infer_match_bool_arm_rows_accept( + node: node, + partials: partials, + entries: entries, + first_arm_target: first_arm_target, + second_arm_target: second_arm_target, + cd: infer_match_bool_consumer_diagnostics_with_int_scrutinee_scaffold( + consumer: node, + cd: cd, + scrutinee_type: scrutinee_type + ), + scrutinee_type: scrutinee_type ) - ) { - outcome_rejected(infer_match_scrutinee_not_bool_diagnostic(node: node)) } else { - match infer_match_bool_arm_row(arm: first_arm_target, entries: entries) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: first_row, diagnostics: fd } => - match infer_match_bool_arm_row(arm: second_arm_target, entries: entries) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: second_row, diagnostics: sd } => - match infer_bool_literal_exhaustiveness_merge( - left: first_row.coverage, - right: second_row.coverage - ) { - InferBoolLiteralExhaustive => - if !infer_branch_type_atoms_equal( - a: first_row.body_type, - b: second_row.body_type - ) { - outcome_rejected(infer_match_arm_type_mismatch_diagnostic(node: node)) - } else { - match infer_descent_witness_for_node(n: node) { - Violates { diagnostic: d } => - Rejected { diagnostics: diagnostics_singleton(d: d) } - Holds { value: descent_proof } => - bind_outcome( - o: inferred_facts_from_grounding( - grounding: infer_branch_canonical_grounding( - node: node, - unified_type: first_row.body_type - ), - descent: Holds { value: descent_proof } - ), - f: fn(facts) { - Accepted { - value: facts, - diagnostics: diagnostics_merge( - outer: diagnostics_merge(outer: cd, inner: fd), - inner: sd - ) - } - } - ) - } - } - InferBoolLiteralMissingTrue => - outcome_rejected(infer_match_non_exhaustive_diagnostic(node: node)) - InferBoolLiteralMissingFalse => - outcome_rejected(infer_match_non_exhaustive_diagnostic(node: node)) - InferBoolLiteralMissingBoth => - outcome_rejected(infer_match_non_exhaustive_diagnostic(node: node)) - } - } - } + outcome_rejected(infer_match_scrutinee_not_bool_diagnostic(node: node)) } } } @@ -1014,8 +1178,9 @@ fn infer_gather_match_row_on_entries( entries: List, pending: Diagnostics, partials: List, + tree: Node, ) -> InferGatherFoldAcc { - match infer_match_bool(node: node, partials: partials, entries: entries) { + match infer_match_bool(node: node, partials: partials, entries: entries, tree: tree) { Rejected { diagnostics: r } => infer_gather_fold_acc_failed( node: node, @@ -1181,6 +1346,7 @@ fn infer_gather_fold_step( edge: Edge, child: InferGatherFoldAcc, partials: List, + tree: Node, ) -> InferGatherFoldAcc { if acc.failed { acc @@ -1212,7 +1378,8 @@ fn infer_gather_fold_step( node: acc.node, entries: merged_entries, pending: merged_pending, - partials: partials + partials: partials, + tree: tree ) } else if acc.await_loop_row && children_remaining == 0 { infer_gather_loop_row_on_entries( @@ -1235,13 +1402,13 @@ fn infer_gather_fold_step( } } -fn infer_gather_fold_algebra(partials: List) -> NodeFold { +fn infer_gather_fold_algebra(partials: List, tree: Node) -> NodeFold { NodeFold { init: fn(n0) { infer_gather_fold_init(n: n0, partials: partials) }, step: fn(acc, e, child) { - infer_gather_fold_step(acc: acc, edge: e, child: child, partials: partials) + infer_gather_fold_step(acc: acc, edge: e, child: child, partials: partials, tree: tree) } } } @@ -1253,7 +1420,7 @@ fn infer_grounding_admits_infer_facts(grounding: CanonicalGrounding) -> Bool { fn infer_entries_for_tree(tree: ResolvedTree) -> Outcome> { let partials = partial_bounded_lattice_instances_in_tree(tree: tree) infer_gather_acc_to_outcome( - acc: fold_node(n: tree, algebra: infer_gather_fold_algebra(partials: partials)) + acc: fold_node(n: tree, algebra: infer_gather_fold_algebra(partials: partials, tree: tree)) ) } fn infer(tree: ResolvedTree) -> Outcome { diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 899229f0bce..c0a68963fb4 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -1,6 +1,6 @@ module v2.compiler.body_lowering_fold -import std.algebra { Empty } +import std.algebra { Cons, Empty } import v2.compiler.fold_lowering { fold_call_head_symbol, fold_call_to_loop, @@ -12,14 +12,15 @@ import v2.extdeps.languages.dag { dag_binding_branded_atom_identity, dag_int_type_binding, dag_lex_token_symbol, + dag_match_arm_node, dag_resolve_preserve_module_metadata_subtree, parse_production_captured_child_optional, parse_production_emitted_identity_optional, parse_subtree_find_production_captured } -import v2.std.algebra { list_append, list_snoc_item } +import v2.std.algebra { list_append, list_snoc_item, length } import v2.std.collection { Absent, List, Optional, Present, list_at_optional, optional_absent, optional_present } -import v2.std.compilers.body_lowering { lower_binary_infix } +import v2.std.compilers.body_lowering { lower_binary_infix, lower_match } import v2.std.compilers.lexing { symbol_lexeme } import v2.std.compilers.sugar { sugar_sequence_pair_optional } import v2.std.diagnostic { @@ -28,8 +29,10 @@ import v2.std.diagnostic { Diagnostics, ExternalContractUnknown, Outcome, + Rejected, Some, Unavailable, + bind_outcome, diagnostics_singleton, node_locus, diagnostics_merge, @@ -37,7 +40,7 @@ import v2.std.diagnostic { outcome_rejected, rejected_with_pending } -import v2.std.grammar { node_atom_identity_optional } +import v2.std.integer { Int } import v2.std.node { Arrow, Atom, @@ -51,6 +54,8 @@ import v2.std.node { Transform, TypeNode, is_empty_conj_root, + match_arm_body, + match_arm_pattern, node_synthetic } import v2.std.node_query { find_named_child } @@ -59,6 +64,33 @@ data body_lowering_fold_note: String = "Forward body producer fold (general-body data body_lowering_fold_dissolution_contract: String = "FLAG E dissolution DELETES this module — do NOT port its interim walker arms into the SugarKey table. The hand-authored families (body_lower_deep_unwrap*, body_lower_operand_ref*, body_lower_operator_tail/infix*, body_lower_postfix_projection*) are receipt scaffolding only; the row-selected GrammarRelationRow forward fold (general-body-producer-design §3) replaces them wholesale. Acceptance: this file is gone and coverage lives in forward rows + existing witnesses." +type BodyLoweringInterimScaffoldDisposition + = SeedRetained { reason: Symbol, migration_trigger: Symbol } + +type BodyLoweringInterimScaffoldRow { + site: Symbol + disposition: BodyLoweringInterimScaffoldDisposition +} + +data body_lowering_interim_scaffold_row_match_hand_walker: BodyLoweringInterimScaffoldRow = BodyLoweringInterimScaffoldRow { + site: ^body_lower_try_match_from_node, + disposition: SeedRetained { + reason: ^body_lowering_match_interim_hand_walker_reason, + migration_trigger: ^migrate_when_general_body_producer_lands + } +} + +fn body_lowering_interim_scaffold_rows() -> List { + Cons { + head: body_lowering_interim_scaffold_row_match_hand_walker, + tail: Empty + } +} + +fn body_lowering_interim_scaffold_seed_retained_count() -> Int { + length(xs: body_lowering_interim_scaffold_rows()) +} + fn body_lower_diagnostic(reason: Symbol, n: Node) -> Diagnostic { Diagnostic { reason: reason, @@ -76,6 +108,8 @@ fn body_lower_canonical_type_binding_optional(sym: Symbol) -> Optional { optional_present(value: sym) } else if symbol_lexeme(sym: sym) == "Int" { optional_present(value: dag_int_type_binding()) + } else if symbol_lexeme(sym: sym) == "Bool" { + optional_present(value: ^bool_node_symbol) } else { optional_absent() } @@ -116,6 +150,7 @@ fn body_lower_is_pass_through_emitted(emitted: Symbol) -> Bool { (emitted == ^dag_surface_expr) || (emitted == ^dag_surface_binary_expr) || (emitted == ^dag_surface_unary_expr) + || (emitted == ^dag_surface_postfix_expr) || (emitted == ^dag_surface_block_expr) || (emitted == ^dag_surface_stmt) || (emitted == ^dag_surface_stmt_seq) @@ -123,7 +158,10 @@ fn body_lower_is_pass_through_emitted(emitted: Symbol) -> Bool { } fn body_lower_is_deferred_lower_emitted(emitted: Symbol) -> Bool { - emitted == ^dag_surface_fn_body + (emitted == ^dag_surface_fn_body) + || (emitted == ^dag_surface_pattern) + || (emitted == ^dag_surface_match_arm) + || (emitted == ^dag_surface_match_arm_stmt_body) } fn body_lower_is_metadata_preserved_emitted(emitted: Symbol) -> Bool { @@ -171,7 +209,11 @@ fn body_lower_operand_ref_optional(node: Node) -> Optional { match node_atom_identity_optional(node: node) { Present { value: id } => if dag_lex_token_symbol(sym: id) { - optional_absent() + if (id == ^dag_token_kw_true) || (id == ^dag_token_kw_false) { + optional_present(value: body_lower_param_ref_atom(identity: id)) + } else { + optional_absent() + } } else { optional_present(value: body_lower_param_ref_atom(identity: id)) } @@ -801,43 +843,70 @@ fn body_lower_return_type_from_fn_captured(captured: Node) -> Optional { body_lower_return_type_after_arrow_walk(node: captured) } +fn body_lower_find_core_substrate_optional(root: Node) -> Optional { + if body_lower_is_core_substrate(node: root) { + optional_present(value: root) + } else { + fold(root.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => body_lower_find_core_substrate_optional(root: e.target) + } + }) + } +} + fn body_lower_try_body_lowered(node: Node) -> Outcome> { - match body_lower_try_postfix_projection(node: node) { + if body_lower_is_core_substrate(node: node) { + outcome_accepted(value: optional_present(value: node)) + } else { + match body_lower_try_match_from_node(node: node) { Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: projection, diagnostics: pd } => - match projection { + Accepted { value: match_found, diagnostics: md } => + match match_found { Present { value: lowered } => - outcome_accepted(value: optional_present(value: lowered), diagnostics: pd) + outcome_accepted(value: optional_present(value: lowered), diagnostics: md) Absent => - match body_lower_try_infix_transform(node: node) { - Present { value: lowered } => outcome_accepted(value: optional_present(value: lowered)) - Absent => - match body_lower_try_fold_loop(node: node) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: fold_result, diagnostics: _ } => - match fold_result { + match body_lower_try_postfix_projection(node: node) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: projection, diagnostics: pd } => + match projection { + Present { value: lowered } => + outcome_accepted(value: optional_present(value: lowered), diagnostics: pd) + Absent => + match body_lower_try_infix_transform(node: node) { Present { value: lowered } => outcome_accepted(value: optional_present(value: lowered)) Absent => - let stripped = body_lower_unwrap_surface_shell(node: node) - match body_lower_try_postfix_projection(node: stripped) { + match body_lower_try_fold_loop(node: node) { Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: stripped_proj, diagnostics: spd } => - match stripped_proj { + Accepted { value: fold_result, diagnostics: _ } => + match fold_result { Present { value: lowered } => - outcome_accepted( - value: optional_present(value: lowered), - diagnostics: spd - ) + outcome_accepted(value: optional_present(value: lowered)) Absent => - match body_lower_try_infix_transform(node: stripped) { - Present { value: lowered } => - outcome_accepted(value: optional_present(value: lowered)) - Absent => - match body_lower_try_fold_loop(node: stripped) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: stripped_fold, diagnostics: _ } => - outcome_accepted(value: stripped_fold) + let stripped = body_lower_unwrap_surface_shell(node: node) + match body_lower_try_postfix_projection(node: stripped) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: stripped_proj, diagnostics: spd } => + match stripped_proj { + Present { value: lowered } => + outcome_accepted( + value: optional_present(value: lowered), + diagnostics: spd + ) + Absent => + match body_lower_try_infix_transform(node: stripped) { + Present { value: lowered } => + outcome_accepted(value: optional_present(value: lowered)) + Absent => + match body_lower_try_fold_loop(node: stripped) { + Rejected { diagnostics: r } => + Rejected { diagnostics: r } + Accepted { value: stripped_fold, diagnostics: _ } => + outcome_accepted(value: stripped_fold) + } + } } } } @@ -847,6 +916,7 @@ fn body_lower_try_body_lowered(node: Node) -> Outcome> { } } } + } } fn body_lower_body_subtree_lower(captured: Node) -> Outcome> { @@ -856,6 +926,13 @@ fn body_lower_body_subtree_lower(captured: Node) -> Outcome> { match found { Present { value: lowered } => outcome_accepted(value: optional_present(value: lowered)) Absent => + match parse_subtree_find_production_captured( + root: captured, + emitted: ^dag_surface_match_expr + ) { + ParseSubtreeFound { captured: match_capture } => + body_lower_try_match_from_captured(captured: match_capture) + ParseSubtreeAbsent => match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_binary_expr) { ParseSubtreeFound { captured: binary } => body_lower_try_body_lowered(node: binary) @@ -876,14 +953,20 @@ fn body_lower_body_subtree_lower(captured: Node) -> Outcome> { ParseSubtreeFound { captured: stmt } => body_lower_body_subtree_lower(captured: stmt) ParseSubtreeAbsent => - body_lower_try_body_lowered( - node: body_lower_unwrap_surface_shell(node: captured) - ) + match body_lower_find_core_substrate_optional(root: captured) { + Present { value: lowered } => + outcome_accepted(value: optional_present(value: lowered)) + Absent => + body_lower_try_body_lowered( + node: body_lower_unwrap_surface_shell(node: captured) + ) + } } } } } } + } } } } @@ -1007,13 +1090,42 @@ fn body_lower_fn_decl_to_arrow(shell: Node) -> Outcome { } } +fn body_lower_literal_bool_atom_optional(node: Node) -> Optional { + match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: node)) { + Present { value: id } => + if (id == ^dag_token_kw_true) || (id == ^dag_token_kw_false) { + optional_present(value: body_lower_param_ref_atom(identity: id)) + } else { + optional_absent() + } + Absent => + fold(node.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => body_lower_literal_bool_atom_optional(node: e.target) + } + }) + } +} + fn body_lower_try_operand_or_reject(shell: Node, captured: Node) -> Outcome { match body_lower_operand_ref_optional(node: captured) { Present { value: operand } => outcome_accepted(value: operand) Absent => - outcome_rejected( - d: body_lower_diagnostic(reason: ^body_lowering_reason_unsupported_form, n: shell) - ) + match body_lower_literal_bool_atom_optional(node: captured) { + Present { value: lit } => outcome_accepted(value: lit) + Absent => + match body_lower_pattern_first_atom_optional(node: captured) { + Present { value: pat_atom } => outcome_accepted(value: pat_atom) + Absent => + outcome_rejected( + d: body_lower_diagnostic( + reason: ^body_lowering_reason_unsupported_form, + n: shell + ) + ) + } + } } } @@ -1380,6 +1492,603 @@ fn body_lower_try_postfix_projection(node: Node) -> Outcome> { } } +fn body_lower_match_arm_wire(pat_node: Node, body: Node) -> Node { + node_synthetic( + kind: TypeNode { connective: Conj }, + children: [ + Edge { label: Named { name: match_arm_pattern }, target: pat_node }, + Edge { label: Named { name: match_arm_body }, target: body } + ] + ) +} + +fn body_lower_pattern_leaf_atom_optional(node: Node) -> Optional { + let stripped = body_lower_deep_unwrap_optional(node: node) + match dag_binding_branded_atom_identity(node: stripped) { + Present { value: binding } => + optional_present(value: body_lower_param_ref_atom(identity: binding)) + Absent => + match parse_production_emitted_identity_optional(node: stripped) { + Present { value: emitted } => + match parse_production_captured_child_optional(node: stripped) { + Present { value: captured } => body_lower_pattern_leaf_atom_optional(node: captured) + Absent => + if emitted == ^dag_surface_pattern { + fold(stripped.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => body_lower_pattern_leaf_atom_optional(node: e.target) + } + }) + } else { + optional_absent() + } + } + Absent => + match node_atom_identity_optional(node: stripped) { + Present { value: id } => + if dag_lex_token_symbol(sym: id) { + if (id == ^dag_token_kw_true) || (id == ^dag_token_kw_false) { + optional_present(value: body_lower_param_ref_atom(identity: id)) + } else { + optional_absent() + } + } else { + optional_present(value: body_lower_param_ref_atom(identity: id)) + } + Absent => + fold(stripped.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => body_lower_pattern_leaf_atom_optional(node: e.target) + } + }) + } + } + } +} + +fn body_lower_pattern_first_atom_optional(node: Node) -> Optional { + match body_lower_pattern_leaf_atom_optional(node: node) { + Present { value: atom } => Present { value: atom } + Absent => + fold(node.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => body_lower_pattern_first_atom_optional(node: e.target) + } + }) + } +} + +fn body_lower_pattern_atom_optional(pattern_capture: Node) -> Optional { + body_lower_pattern_first_atom_optional(node: pattern_capture) +} + +fn body_lower_match_arm_navigation_reject(arm_capture: Node) -> Outcome { + outcome_rejected( + d: body_lower_diagnostic( + reason: ^body_lowering_reason_match_arm_navigation_refused, + n: arm_capture + ) + ) +} + +fn body_lower_match_arm_body_capture_optional(stripped: Node) -> Optional { + match parse_subtree_find_production_captured(root: stripped, emitted: ^dag_surface_expr) { + ParseSubtreeFound { captured: expr } => optional_present(value: expr) + ParseSubtreeAbsent => + match parse_subtree_find_production_captured( + root: stripped, + emitted: ^dag_surface_primary_expr + ) { + ParseSubtreeFound { captured: primary } => optional_present(value: primary) + ParseSubtreeAbsent => + match parse_subtree_find_production_captured( + root: stripped, + emitted: ^dag_surface_postfix_expr + ) { + ParseSubtreeFound { captured: postfix } => optional_present(value: postfix) + ParseSubtreeAbsent => optional_absent() + } + } + } +} + +fn body_lower_match_arm_body_optional(body_capture: Node) -> Optional { + match parse_subtree_find_production_captured(root: body_capture, emitted: ^dag_surface_expr) { + ParseSubtreeFound { captured: expr } => body_lower_operand_ref_optional(node: expr) + ParseSubtreeAbsent => + match parse_production_emitted_identity_optional(node: body_capture) { + Present { value: emitted } => + if emitted == ^dag_surface_expr { + match parse_production_captured_child_optional(node: body_capture) { + Present { value: captured } => + body_lower_match_arm_body_optional(body_capture: captured) + Absent => optional_absent() + } + } else if emitted == ^dag_surface_match_arm_stmt_body { + match parse_production_captured_child_optional(node: body_capture) { + Present { value: captured } => + body_lower_match_arm_body_optional(body_capture: captured) + Absent => optional_absent() + } + } else { + body_lower_operand_ref_optional(node: body_capture) + } + Absent => + match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: body_capture)) { + Present { value: id } => + if dag_lex_token_symbol(sym: id) { + optional_present(value: body_lower_param_ref_atom(identity: id)) + } else { + body_lower_operand_ref_optional(node: body_capture) + } + Absent => body_lower_operand_ref_optional(node: body_capture) + } + } + } +} + +fn body_lower_match_arm_wire_from_sequence(stripped: Node) -> Outcome { + match parse_subtree_find_production_captured( + root: stripped, + emitted: ^dag_surface_pattern + ) { + ParseSubtreeFound { captured: pat_capture } => + match body_lower_pattern_atom_optional(pattern_capture: pat_capture) { + Present { value: pat_node } => + match body_lower_match_arm_body_capture_optional(stripped: stripped) { + Present { value: body_capture } => + match body_lower_match_arm_body_optional(body_capture: body_capture) { + Present { value: body } => + outcome_accepted( + value: body_lower_match_arm_wire(pat_node: pat_node, body: body) + ) + Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + ParseSubtreeAbsent => + match body_lower_match_spine_left(spine: stripped) { + Present { value: left } => + match body_lower_match_spine_right(spine: stripped) { + Present { value: right } => + match body_lower_pattern_atom_optional(pattern_capture: left) { + Present { value: pat_node } => + match body_lower_match_spine_left(spine: right) { + Present { value: arrow_node } => + match node_atom_identity_optional(node: arrow_node) { + Present { value: arrow } => + if arrow == ^dag_token_fat_arrow { + match body_lower_match_spine_right(spine: right) { + Present { value: body_capture } => + match body_lower_match_arm_body_optional( + body_capture: body_capture + ) { + Present { value: body } => + outcome_accepted( + value: body_lower_match_arm_wire( + pat_node: pat_node, + body: body + ) + ) + Absent => + body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => + body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + } else { + body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => + match sugar_sequence_pair_optional(node: right) { + Present { value: after_pattern } => + match node_atom_identity_optional(node: after_pattern.left) { + Present { value: arrow } => + if arrow == ^dag_token_fat_arrow { + match body_lower_match_arm_body_optional( + body_capture: after_pattern.right + ) { + Present { value: body } => + outcome_accepted( + value: body_lower_match_arm_wire( + pat_node: pat_node, + body: body + ) + ) + Absent => + body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + } else { + body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => + body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + } + Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) + } + } +} + +fn body_lower_is_match_arm_navigate_emitted(emitted: Symbol) -> Bool { + (emitted == ^dag_surface_pattern) + || (emitted == ^dag_surface_primary_expr) + || (emitted == ^dag_surface_match_arm_stmt_body) + || body_lower_is_pass_through_emitted(emitted: emitted) +} + +fn body_lower_match_arm_from_comma_repeat_elem(repeat_elem: Node) -> Outcome { + let stripped = body_lower_deep_unwrap_optional(node: repeat_elem) + match sugar_sequence_pair_optional(node: stripped) { + Present { value: pair } => + body_lower_wire_match_arm_capture( + arm_capture: body_lower_postfix_optional_unwrap(node: pair.right) + ) + Absent => + body_lower_wire_match_arm_capture(arm_capture: stripped) + } +} + +fn body_lower_extract_comma_list_arm_head(node: Node) -> Outcome { + let stripped = body_lower_deep_unwrap_optional(node: node) + match body_lower_wire_match_arm_capture(arm_capture: stripped) { + Rejected { diagnostics: _ } => + body_lower_match_arm_from_comma_repeat_elem(repeat_elem: stripped) + Accepted { value: arm, diagnostics: d } => + Accepted { value: arm, diagnostics: d } + } +} + +fn body_lower_wire_match_arm_capture(arm_capture: Node) -> Outcome { + let stripped = body_lower_deep_unwrap_optional(node: arm_capture) + match parse_production_emitted_identity_optional(node: stripped) { + Present { value: emitted } => + if emitted == ^dag_surface_match_arm { + match parse_production_captured_child_optional(node: stripped) { + Present { value: captured } => + body_lower_wire_match_arm_capture(arm_capture: captured) + Absent => body_lower_match_arm_wire_from_sequence(stripped: stripped) + } + } else if body_lower_is_match_arm_navigate_emitted(emitted: emitted) { + match parse_production_captured_child_optional(node: stripped) { + Present { value: captured } => + body_lower_wire_match_arm_capture(arm_capture: captured) + Absent => body_lower_match_arm_navigation_reject(arm_capture: arm_capture) + } + } else { + body_lower_match_arm_navigation_reject(arm_capture: arm_capture) + } + Absent => body_lower_match_arm_wire_from_sequence(stripped: stripped) + } +} + +fn body_lower_collect_match_arms_from_repeat_tail(repeat_capture: Node) -> Outcome> { + if is_empty_conj_root(n: repeat_capture) { + outcome_accepted(value: Empty) + } else { + match find_named_child(root: repeat_capture, name: ^grammar_sequence_left_node_projection) { + Accepted { value: head, diagnostics: _ } => + match body_lower_extract_comma_list_arm_head(node: head) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: arm, diagnostics: d } => + match find_named_child(root: repeat_capture, name: ^grammar_sequence_right_node_projection) { + Accepted { value: tail, diagnostics: _ } => + match body_lower_collect_match_arms_from_repeat_tail(repeat_capture: tail) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: rest, diagnostics: rd } => + Accepted { + value: list_append(left: [arm], right: rest), + diagnostics: diagnostics_merge(outer: d, inner: rd) + } + } + Rejected { diagnostics: _ } => + Accepted { value: [arm], diagnostics: d } + } + } + Rejected { diagnostics: _ } => outcome_accepted(value: Empty) + } + } +} + +fn body_lower_collect_match_arms(sequence_capture: Node) -> Outcome> { + let unwrapped = body_lower_postfix_optional_unwrap(node: sequence_capture) + match find_named_child(root: unwrapped, name: ^grammar_sequence_left_node_projection) { + Accepted { value: first, diagnostics: _ } => + match body_lower_extract_comma_list_arm_head(node: first) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: arm, diagnostics: d } => + match find_named_child(root: unwrapped, name: ^grammar_sequence_right_node_projection) { + Accepted { value: tail, diagnostics: _ } => + match body_lower_collect_match_arms_from_repeat_tail(repeat_capture: tail) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: rest, diagnostics: rd } => + Accepted { + value: list_append(left: [arm], right: rest), + diagnostics: diagnostics_merge(outer: d, inner: rd) + } + } + Rejected { diagnostics: _ } => + Accepted { value: [arm], diagnostics: d } + } + } + Rejected { diagnostics: _ } => + match sugar_sequence_pair_optional(node: unwrapped) { + Present { value: pair } => + match body_lower_extract_comma_list_arm_head(node: pair.left) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: arm, diagnostics: d } => + match body_lower_after_comma_tail_optional(node: pair.right) { + Present { value: tail } => + match body_lower_collect_match_arms(sequence_capture: tail) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: rest, diagnostics: rd } => + Accepted { + value: list_append(left: [arm], right: rest), + diagnostics: diagnostics_merge(outer: d, inner: rd) + } + } + Absent => Accepted { value: [arm], diagnostics: d } + } + } + Absent => + match body_lower_extract_comma_list_arm_head(node: unwrapped) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: arm, diagnostics: d } => + Accepted { value: [arm], diagnostics: d } + } + } + } +} + +fn body_lower_match_arms_from_brace_interior(interior: Node) -> Outcome> { + let unwrapped = body_lower_postfix_optional_unwrap(node: interior) + match sugar_sequence_pair_optional(node: unwrapped) { + Present { value: pair } => + body_lower_collect_match_arms( + sequence_capture: body_lower_unwrap_optional_element(node: pair.left) + ) + Absent => + body_lower_collect_match_arms(sequence_capture: unwrapped) + } +} + +fn body_lower_match_spine_left(spine: Node) -> Optional { + match find_named_child(root: spine, name: ^grammar_sequence_left_node_projection) { + Accepted { value: left, diagnostics: _ } => Present { value: left } + Rejected { diagnostics: _ } => + match sugar_sequence_pair_optional(node: spine) { + Present { value: pair } => Present { value: pair.left } + Absent => Absent + } + } +} + +fn body_lower_match_spine_right(spine: Node) -> Optional { + match find_named_child(root: spine, name: ^grammar_sequence_right_node_projection) { + Accepted { value: right, diagnostics: _ } => Present { value: right } + Rejected { diagnostics: _ } => + match sugar_sequence_pair_optional(node: spine) { + Present { value: pair } => Present { value: pair.right } + Absent => Absent + } + } +} + +fn body_lower_match_scrutinee_on_token(id: Symbol, left: Node, right: Node) -> Optional { + match id == ^dag_token_lbrace { + true => Absent + false => + match id == ^dag_token_kw_match { + true => body_lower_match_scrutinee_from_spine(spine: right) + false => + match body_lower_operand_ref_optional(node: left) { + Present { value: op } => Present { value: op } + Absent => body_lower_match_scrutinee_from_spine(spine: right) + } + } + } +} + +fn body_lower_match_scrutinee_from_spine(spine: Node) -> Optional { + if is_empty_conj_root(n: spine) { + Absent + } else { + match body_lower_match_spine_left(spine: spine) { + Present { value: left } => + match body_lower_match_spine_right(spine: spine) { + Present { value: right } => + match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: left)) { + Present { value: id } => + body_lower_match_scrutinee_on_token(id: id, left: left, right: right) + Absent => + match body_lower_operand_ref_optional(node: left) { + Present { value: op } => Present { value: op } + Absent => body_lower_match_scrutinee_from_spine(spine: right) + } + } + Absent => Absent + } + Absent => Absent + } + } +} + +fn body_lower_match_scrutinee_optional(captured: Node) -> Optional { + match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_binary_expr) { + ParseSubtreeFound { captured: binary } => + body_lower_operand_ref_optional(node: binary) + ParseSubtreeAbsent => + match parse_subtree_find_production_captured(root: captured, emitted: ^dag_surface_postfix_expr) { + ParseSubtreeFound { captured: postfix } => + body_lower_operand_ref_optional(node: postfix) + ParseSubtreeAbsent => + body_lower_match_scrutinee_from_spine( + spine: body_lower_unwrap_surface_shell(node: captured) + ) + } + } +} + +fn body_lower_match_arms_on_lbrace_token(id: Symbol, right: Node) -> Outcome>> { + match id == ^dag_token_lbrace { + true => + match body_lower_match_arms_from_brace_interior(interior: right) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: arms, diagnostics: d } => + if count(arms) > 0 { + Accepted { + value: optional_present(value: arms), + diagnostics: d + } + } else { + outcome_rejected( + d: body_lower_diagnostic( + reason: ^body_lowering_reason_match_arm_navigation_refused, + n: right + ) + ) + } + } + false => body_lower_match_arms_after_lbrace_optional(spine: right) + } +} + +fn body_lower_match_arms_after_lbrace_optional(spine: Node) -> Outcome>> { + if is_empty_conj_root(n: spine) { + outcome_accepted(value: optional_absent()) + } else { + match body_lower_match_spine_left(spine: spine) { + Present { value: left } => + match body_lower_match_spine_right(spine: spine) { + Present { value: right } => + match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: left)) { + Present { value: id } => + body_lower_match_arms_on_lbrace_token(id: id, right: right) + Absent => + body_lower_match_arms_after_lbrace_optional(spine: right) + } + Absent => outcome_accepted(value: optional_absent()) + } + Absent => outcome_accepted(value: optional_absent()) + } + } +} + +fn body_lower_match_arms_optional(captured: Node) -> Outcome>> { + body_lower_match_arms_after_lbrace_optional( + spine: body_lower_unwrap_surface_shell(node: captured) + ) +} + +fn body_lower_try_match_from_captured(captured: Node) -> Outcome> { + match body_lower_match_scrutinee_optional(captured: captured) { + Present { value: scrutinee } => + match body_lower_match_arms_optional(captured: captured) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: arms_opt, diagnostics: d } => + match arms_opt { + Present { value: arms } => + if count(arms) > 0 { + Accepted { + value: optional_present(value: lower_match(scrutinee: scrutinee, arms: arms)), + diagnostics: d + } + } else { + outcome_rejected( + d: body_lower_diagnostic( + reason: ^body_lowering_reason_match_arm_navigation_refused, + n: captured + ) + ) + } + Absent => + outcome_rejected( + d: body_lower_diagnostic( + reason: ^body_lowering_reason_match_arm_navigation_refused, + n: captured + ) + ) + } + } + Absent => + outcome_rejected( + d: body_lower_diagnostic( + reason: ^body_lowering_reason_match_arm_navigation_refused, + n: captured + ) + ) + } +} + +fn body_lower_match_capture_heads_spine(spine: Node) -> Bool { + match body_lower_match_spine_left(spine: spine) { + Present { value: left } => + match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: left)) { + Present { value: id } => id == ^dag_token_kw_match + Absent => false + } + Absent => false + } +} + +fn body_lower_try_match_from_node(node: Node) -> Outcome> { + match parse_production_emitted_identity_optional(node: node) { + Present { value: emitted } => + if emitted == ^dag_surface_match_expr { + match body_lower_unwrap_captured(shell: node) { + Present { value: captured } => + body_lower_try_match_from_captured(captured: captured) + Absent => outcome_accepted(value: optional_absent()) + } + } else { + outcome_accepted(value: optional_absent()) + } + Absent => + if body_lower_match_capture_heads_spine( + spine: body_lower_unwrap_surface_shell(node: node) + ) { + body_lower_try_match_from_captured(captured: node) + } else { + outcome_accepted(value: optional_absent()) + } + } +} + +fn body_lower_match_expr(shell: Node) -> Outcome { + match body_lower_unwrap_captured(shell: shell) { + Absent => + outcome_rejected( + d: body_lower_diagnostic(reason: ^body_lowering_reason_unsupported_form, n: shell) + ) + Present { value: captured } => + match body_lower_try_match_from_captured(captured: captured) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: lowered_opt, diagnostics: d } => + match lowered_opt { + Present { value: lowered } => + Accepted { value: lowered, diagnostics: d } + Absent => + outcome_rejected( + d: body_lower_diagnostic(reason: ^body_lowering_reason_unsupported_form, n: shell) + ) + } + } + } +} + fn body_lower_postfix_expr(shell: Node) -> Outcome { match body_lower_unwrap_captured(shell: shell) { Absent => @@ -1387,8 +2096,19 @@ fn body_lower_postfix_expr(shell: Node) -> Outcome { d: body_lower_diagnostic(reason: ^body_lowering_reason_unsupported_form, n: shell) ) Present { value: captured } => + match body_lower_pattern_first_atom_optional(node: captured) { + Present { value: atom } => outcome_accepted(value: atom) + Absent => match body_lower_try_postfix_projection(node: captured) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } + Rejected { diagnostics: r } => + match body_lower_literal_bool_atom_optional(node: captured) { + Present { value: lit } => outcome_accepted(value: lit) + Absent => + match body_lower_pattern_first_atom_optional(node: captured) { + Present { value: atom } => outcome_accepted(value: atom) + Absent => Rejected { diagnostics: r } + } + } Accepted { value: found, diagnostics: d } => match found { Present { value: transform } => @@ -1398,7 +2118,8 @@ fn body_lower_postfix_expr(shell: Node) -> Outcome { Present { value: transform } => outcome_accepted(value: transform) Absent => match body_lower_try_fold_loop(node: captured) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } + Rejected { diagnostics: _ } => + body_lower_try_operand_or_reject(shell: shell, captured: captured) Accepted { value: fold_result, diagnostics: _ } => match fold_result { Present { value: loop_node } => outcome_accepted(value: loop_node) @@ -1408,6 +2129,7 @@ fn body_lower_postfix_expr(shell: Node) -> Outcome { } } } + } } } @@ -1418,8 +2140,19 @@ fn body_lower_primary_expr(shell: Node) -> Outcome { d: body_lower_diagnostic(reason: ^body_lowering_reason_unsupported_form, n: shell) ) Present { value: captured } => + match body_lower_pattern_first_atom_optional(node: captured) { + Present { value: atom } => outcome_accepted(value: atom) + Absent => match body_lower_try_postfix_projection(node: captured) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } + Rejected { diagnostics: r } => + match body_lower_literal_bool_atom_optional(node: captured) { + Present { value: lit } => outcome_accepted(value: lit) + Absent => + match body_lower_pattern_first_atom_optional(node: captured) { + Present { value: atom } => outcome_accepted(value: atom) + Absent => Rejected { diagnostics: r } + } + } Accepted { value: found, diagnostics: d } => match found { Present { value: transform } => @@ -1429,7 +2162,8 @@ fn body_lower_primary_expr(shell: Node) -> Outcome { Present { value: transform } => outcome_accepted(value: transform) Absent => match body_lower_try_fold_loop(node: captured) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } + Rejected { diagnostics: _ } => + body_lower_try_operand_or_reject(shell: shell, captured: captured) Accepted { value: fold_result, diagnostics: _ } => match fold_result { Present { value: loop_node } => outcome_accepted(value: loop_node) @@ -1439,6 +2173,7 @@ fn body_lower_primary_expr(shell: Node) -> Outcome { } } } + } } } @@ -1449,6 +2184,8 @@ fn body_lower_production_emitted(shell: Node, emitted: Symbol) -> Outcome body_lower_fn_decl_to_arrow(shell: shell) } else if emitted == ^dag_surface_postfix_expr { body_lower_postfix_expr(shell: shell) + } else if emitted == ^dag_surface_match_expr { + body_lower_match_expr(shell: shell) } else if body_lower_is_pass_through_emitted(emitted: emitted) { body_lower_unwrap_pass_through(shell: shell) } else if emitted == ^dag_surface_primary_expr { diff --git a/src/v2/compiler/emit_produced.dag b/src/v2/compiler/emit_produced.dag index 90232a48d02..9ed85003350 100644 --- a/src/v2/compiler/emit_produced.dag +++ b/src/v2/compiler/emit_produced.dag @@ -7,8 +7,8 @@ import v2.extdeps.languages.rust { rust_produced_decl_target, rust_signature_with_open_from_decl } -import extdeps.communication.medium { Medium } import v2.std.compilers.target_model { TargetModel } +import extdeps.communication.medium { Medium } import v2.std.collection { Absent, List, Present, list_at_optional } import v2.std.algebra { fold_list, list_append } import std.algebra { Empty } @@ -65,26 +65,30 @@ fn emit_produced_decl_inner_arrow(decl: Node) -> Outcome { } } +fn emit_produced_decl_rust_with_target( + decl: Node, + target: TargetModel +) -> Outcome> { + bind_outcome( + o: emit_produced_decl_inner_arrow(decl: decl), + f: fn(arrow) { + bind_outcome( + o: target_serialize_bodied_arrow_from_model(target: target, emitted: arrow), + f: fn(text) { + target_source_medium(text: text, target: target) + } + ) + } + ) +} + fn emit_produced_decl_rust(decl: Node) -> Outcome> { bind_outcome( o: rust_signature_with_open_from_decl(decl: decl), f: fn(signature) { - bind_outcome( - o: emit_produced_decl_inner_arrow(decl: decl), - f: fn(arrow) { - bind_outcome( - o: target_serialize_bodied_arrow_from_model( - target: rust_produced_decl_target(signature_with_open: signature), - emitted: arrow - ), - f: fn(text) { - target_source_medium( - text: text, - target: rust_produced_decl_target(signature_with_open: signature) - ) - } - ) - } + emit_produced_decl_rust_with_target( + decl: decl, + target: rust_produced_decl_target(signature_with_open: signature) ) } ) diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 03afa8c9a60..9c65744c88d 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -174,6 +174,8 @@ data dag_bind_wrong_value_source_text: String = "fn one() -> Int { let x = 2 in data dag_match_source_text: String = "fn one_or_two() -> Int { match true { true => 1, false => 2 } }" +data dag_classical_not_source_text: String = "fn classical_not(a: Classical) -> Classical { match a { True => False, False => True } }" + data dag_rec_source_text: String = "fn mk() -> Rec { Rec { v: 9 } }" data dag_field_access_source_text: String = "fn get(r: Rec) -> Int { r.v }" diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index 2271af4c1d2..a329cf3b3d4 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -1882,7 +1882,7 @@ fn rust_runtime_row() -> TargetEmitHostRuntimeRow { fn rust_target_model_staging() -> TargetModel { TargetModel { bundle: rust_target_model_bundle_core(), - lex: rust_fn_add_lex(), + lex: rust_staging_lex(), binding_spellings: rust_binding_spellings(), token_class_emit_transforms: target_model_emit_transforms_empty, authority_source_text: rust_source_text_authority(), @@ -1998,6 +1998,28 @@ fn rust_ident_lex_rule() -> LexRule { } } +fn rust_staging_match_additional_lex_rules() -> List { + [ + rust_lex_rule(token_class: ^rust_token_unwired_match, text: "match "), + rust_lex_rule(token_class: ^rust_token_unwired_fat_arrow, text: " => "), + rust_lex_rule(token_class: ^dag_token_kw_true, text: "true"), + rust_lex_rule(token_class: ^dag_token_kw_false, text: "false") + ] +} + +fn rust_staging_lex_rules() -> LexRuleSet { + LexRuleSet { + rules: list_append( + left: rust_fn_add_lex_rules().rules, + right: rust_staging_match_additional_lex_rules() + ) + } +} + +fn rust_staging_lex() -> LexRules { + ModeledLexRules { root: rust_staging_lex_rules() } +} + fn rust_fn_add_lex_rules() -> LexRuleSet { LexRuleSet { rules: list_append( diff --git a/src/v2/extdeps/languages/rust_test.dag b/src/v2/extdeps/languages/rust_test.dag index e05ac8f2d59..90beae62cbf 100644 --- a/src/v2/extdeps/languages/rust_test.dag +++ b/src/v2/extdeps/languages/rust_test.dag @@ -121,6 +121,7 @@ import v2.extdeps.languages.rust { rust_selection_policy_node, rust_sg_rc_use_site_ownership_catalog, rust_source_text_authority, + rust_staging_lex, rust_target_model_bundle_core, rust_target_model_core_edges_with_operators, rust_type_expression_projection_bundle_node, @@ -781,6 +782,142 @@ fn rust_match_target_model_staging() -> TargetModel { } } +data rust_classical_not_ingested_emit_host_main_suffix: String = "\n\nfn main() { let value = classical_not(1); let bytes = [0u8, (value & 0xff) as u8, ((value >> 8) & 0xff) as u8, ((value >> 16) & 0xff) as u8, ((value >> 24) & 0xff) as u8]; let _ = std::io::Write::write_all(&mut std::io::stdout(), &bytes); }\n" + +fn rust_classical_not_ingested_host_transport_descriptor() -> HostTransportDescriptor { + HostTransportDescriptor { + identity: ^rust_host_transport_classical_not_ingested_identity, + workspace: [ + WorkspaceFile { + path: "Cargo.toml", + content: FixedText { text: rust_emit_host_cargo_manifest } + }, + WorkspaceFile { + path: "src/main.rs", + content: EmittedWithSuffix { suffix: rust_classical_not_ingested_emit_host_main_suffix } + } + ], + build: [ + ProcessInvocation { + tool: ^host_tool_cargo, + args: [LiteralArg { text: "build" }, LiteralArg { text: "--quiet" }] + } + ], + run: ProcessInvocation { + tool: ^host_tool_cargo, + args: [LiteralArg { text: "run" }, LiteralArg { text: "--quiet" }] + }, + runtime_value_codec: FixedWidthBytes { width: 5 } + } +} + +fn rust_classical_not_ingested_runtime_row() -> TargetEmitHostRuntimeRow { + HostRuntimeRowPresent { + row: EmitHostRuntimeRow { + transport: rust_classical_not_ingested_host_transport_descriptor(), + runtime_primitive_type: rust_emit_host_runtime_primitive_type_node() + } + } +} + +fn rust_classical_not_block_close() -> List { + [ + FixedToken { token_class: ^rust_token_rbrace } + ] +} + +fn rust_classical_not_signature_with_open() -> List { + [ + FixedToken { token_class: ^rust_token_kw_fn }, + BoundToken { token_class: ^rust_token_ident, binding: ^dag_binding_fn_classical_not }, + FixedToken { token_class: ^rust_token_lparen }, + BoundToken { token_class: ^rust_token_ident, binding: ^dag_binding_param_x }, + FixedToken { token_class: ^rust_token_colon }, + FixedToken { token_class: ^rust_token_ty_i32 }, + FixedToken { token_class: ^rust_token_rparen }, + FixedToken { token_class: ^rust_token_arrow }, + FixedToken { token_class: ^rust_token_ty_i32 }, + FixedToken { token_class: ^rust_token_lbrace } + ] +} + +fn rust_classical_not_bodied_arrow_statement_scaffold() -> TargetBodiedArrowStatementScaffold { + derive_bodied_arrow_scaffold( + signature_with_open: rust_classical_not_signature_with_open(), + block_close: rust_classical_not_block_close(), + mode: ValueProducing + ) +} + +fn rust_classical_not_bodied_relation_row_node() -> Node { + grammar_relation_row_attach_bodied_scaffold( + row: rust_grammar_relation_row_node(row: rust_match_grammar_relation_row()), + scaffold: rust_classical_not_bodied_arrow_statement_scaffold() + ) +} + +fn rust_classical_not_translation_rules_node() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + rust_named_edge( + name: ^rust_relation_rule_fn_classical_not, + target: rust_classical_not_bodied_relation_row_node() + ) + ], + occurrence_id: SyntheticOccurrence + } +} + +fn rust_classical_not_target_model_bundle_core() -> Node { + let core = rust_target_model_core_edges_with_operators( + operator_catalog: rust_operator_realizations_catalog_node() + ) + Node { + kind: TypeNode { connective: Conj }, + children: fold( + core, + init: Empty, + f: fn(acc, edge) { + match edge.label { + Named { name: n } => + if n == ^target_model_edge_translation_rules { + list_snoc_item( + xs: acc, + item: rust_named_edge( + name: ^target_model_edge_translation_rules, + target: rust_classical_not_translation_rules_node() + ) + ) + } else { + list_snoc_item(xs: acc, item: edge) + } + Positional => list_snoc_item(xs: acc, item: edge) + } + } + ), + occurrence_id: SyntheticOccurrence + } +} + +fn rust_classical_not_ingested_binding_spellings() -> Map { + let m0 = rust_binding_spellings() + let m1 = map_insert(m0, ^dag_binding_fn_classical_not, "classical_not") + let m2 = map_insert(m1, ^dag_binding_octet_one, "1") + map_insert(m2, ^dag_binding_octet_zero, "0") +} + +fn rust_classical_not_ingested_target_model_staging() -> TargetModel { + TargetModel { + bundle: rust_classical_not_target_model_bundle_core(), + lex: rust_staging_lex(), + binding_spellings: rust_classical_not_ingested_binding_spellings(), + token_class_emit_transforms: target_model_emit_transforms_empty, + authority_source_text: rust_source_text_authority(), + runtime_row: rust_classical_not_ingested_runtime_row() + } +} + data rust_field_access_source_text: String = "fn get(r: (i32,)) -> i32 { r.0 }" data rust_field_access_wrong_field_source_text: String = "fn get(r: (i32,)) -> i32 { r.1 }" diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index 4d743f97303..a8ab5551cdb 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -5884,6 +5884,23 @@ fn target_value_expr_match_arms_from_wire( } } +fn concrete_syntax_tokens_extend( + acc: List, + more: List +) -> List { + list_append(left: acc, right: more) +} + +fn concrete_syntax_tokens_snoc_fixed( + acc: List, + token_class: Symbol +) -> List { + list_snoc_item( + xs: acc, + item: FixedToken { token_class: token_class } + ) +} + fn target_value_expr_match_arm_tokens( arms: List, projection: TargetValueExpressionProjection, @@ -5910,33 +5927,200 @@ fn target_value_expr_match_arm_tokens( catalog: catalog ), f: fn(body_tokens) { - let arm_chunk = list_append( - left: list_append( - left: pattern_tokens, - right: Cons { - head: FixedToken { - token_class: projection.match_form.fat_arrow - }, - tail: Empty - } + let arm_chunk = concrete_syntax_tokens_extend( + acc: concrete_syntax_tokens_snoc_fixed( + acc: pattern_tokens, + token_class: projection.match_form.fat_arrow ), - right: body_tokens + more: body_tokens ) if is_empty(xs: prior_tokens) { outcome_accepted(arm_chunk) } else { outcome_accepted( - list_append( - left: list_append( - left: prior_tokens, - right: Cons { - head: FixedToken { - token_class: projection.match_form.arm_separator - }, - tail: Empty - } + concrete_syntax_tokens_extend( + acc: concrete_syntax_tokens_snoc_fixed( + acc: prior_tokens, + token_class: projection.match_form.arm_separator + ), + more: arm_chunk + ) + ) + } + } + ) + } + ) + } + } + ) { + Accepted { value: tokens, diagnostics: d } => Accepted { value: tokens, diagnostics: d } + Rejected { diagnostics: r } => Rejected { diagnostics: r } + } +} + +data target_value_expr_int_bool_octet_channel_dissolution_note: String = "Staging bridge only: inline scrutinee `x != 0` decodes Int wire to bool at the match seam. Ground on the modeled octet↔bool codec authority once inhabited ({0,1} domain, not general nonzero) — do not let this bridge harden into a second decode nickname. interim bindings: ^dag_binding_octet_zero/^dag_binding_octet_one spell 0/1 until codec rows land. scaffold-widen: infer half emits infer_match_int_scrutinee_bool_literal_scaffold diagnostic on Int-scrutinee bool-literal match (countable). paired-scaffold: infer half = infer_match_int_scrutinee_bool_literal_body_note (04_infer.dag) — dissolve both halves together on octet↔bool codec inhabitation." + +fn target_value_expr_is_bool_kw_symbol_identity(expr: TargetValueExpression) -> Bool { + match expr.kind { + TargetValueExprSymbolIdentity => + match target_value_expression_symbol_identity_from_wire(wire: expr.node) { + Accepted { value: id, diagnostics: _ } => + id == ^dag_token_kw_true || id == ^dag_token_kw_false + Rejected { diagnostics: _ } => false + } + _ => false + } +} + +fn target_value_expr_match_arms_are_int_bool_octet_channel( + arms: List +) -> Bool { + if is_empty(xs: arms) { + false + } else { + !any( + xs: arms, + predicate: fn(arm) { + !target_value_expr_is_bool_kw_symbol_identity(expr: arm.pattern) + || !target_value_expr_is_bool_kw_symbol_identity(expr: arm.body) + } + ) + } +} + +fn target_value_expr_match_is_int_bool_octet_channel( + scrutinee: TargetValueExpression, + arms: List +) -> Bool { + match scrutinee.kind { + TargetValueExprBindingRef => + target_value_expr_match_arms_are_int_bool_octet_channel(arms: arms) + _ => false + } +} + +fn target_value_expr_bool_kw_octet_body_tokens( + expr: TargetValueExpression, + projection: TargetValueExpressionProjection +) -> Outcome> { + bind_outcome( + o: target_value_expression_symbol_identity_from_wire(wire: expr.node), + f: fn(token_class) { + if token_class == ^dag_token_kw_false { + outcome_accepted( + Cons { + head: target_value_expression_binding_ref_token( + binding: ^dag_binding_octet_zero, + projection: projection + ), + tail: Empty + } + ) + } else if token_class == ^dag_token_kw_true { + outcome_accepted( + Cons { + head: target_value_expression_binding_ref_token( + binding: ^dag_binding_octet_one, + projection: projection + ), + tail: Empty + } + ) + } else { + outcome_rejected( + target_value_expr_diagnostic( + reason: ^target_value_expr_reason_transform_shape_invalid, + node: expr.node + ) + ) + } + } + ) +} + +fn target_value_expr_int_bool_octet_scrutinee_carrier_tokens( + scrutinee_tokens: List, + catalog: Node, + projection: TargetValueExpressionProjection +) -> Outcome> { + bind_outcome( + o: target_operator_realization_catalog_lookup( + catalog: catalog, + canonical_op: canonical_operation_op_ne() + ), + f: fn(ne_realization) { + match ne_realization.shape { + InfixToken { token: ne_token } => + outcome_accepted( + concrete_syntax_tokens_extend( + acc: concrete_syntax_tokens_extend( + acc: scrutinee_tokens, + more: Cons { + head: FixedToken { token_class: ne_token }, + tail: Empty + } + ), + more: Cons { + head: target_value_expression_binding_ref_token( + binding: ^dag_binding_octet_zero, + projection: projection + ), + tail: Empty + } + ) + ) + _ => + outcome_rejected( + target_operator_realization_catalog_miss_diagnostic(catalog: catalog) + ) + } + } + ) +} + +fn target_value_expr_match_arm_tokens_int_bool_octet_channel( + arms: List, + projection: TargetValueExpressionProjection, + catalog: Node +) -> Outcome> { + match fold( + arms, + init: Accepted { value: Empty, diagnostics: None }, + f: fn(acc, arm) { + match acc { + Rejected { diagnostics: r } => acc + Accepted { value: prior_tokens, diagnostics: d } => + bind_outcome( + o: target_value_expression_to_concrete_tokens( + expr: arm.pattern, + projection: projection, + catalog: catalog + ), + f: fn(pattern_tokens) { + bind_outcome( + o: target_value_expr_bool_kw_octet_body_tokens( + expr: arm.body, + projection: projection + ), + f: fn(body_tokens) { + let arm_chunk = concrete_syntax_tokens_extend( + acc: concrete_syntax_tokens_snoc_fixed( + acc: pattern_tokens, + token_class: projection.match_form.fat_arrow + ), + more: body_tokens + ) + if is_empty(xs: prior_tokens) { + outcome_accepted(arm_chunk) + } else { + outcome_accepted( + concrete_syntax_tokens_extend( + acc: concrete_syntax_tokens_snoc_fixed( + acc: prior_tokens, + token_class: projection.match_form.arm_separator ), - right: arm_chunk + more: arm_chunk ) ) } @@ -5993,61 +6177,53 @@ fn target_value_expression_match_to_concrete_tokens_inner( catalog: catalog ), f: fn(scrutinee_tokens) { - bind_outcome( - o: target_value_expr_match_arm_tokens( - arms: arms, - projection: projection, - catalog: catalog - ), - f: fn(arm_tokens) { - outcome_accepted( - list_append( - left: list_append( - left: list_append( - left: list_append( - left: list_append( - left: list_append( - left: Cons { - head: FixedToken { - token_class: projection.match_form.match_token - }, - tail: Empty - }, - right: Cons { - head: FixedToken { - token_class: projection.match_form.scrutinee_open - }, - tail: Empty - } - ), - right: scrutinee_tokens - ), - right: Cons { - head: FixedToken { - token_class: projection.match_form.scrutinee_close - }, - tail: Empty - } - ), - right: Cons { - head: FixedToken { - token_class: projection.match_form.open - }, - tail: Empty - } - ), - right: arm_tokens + if target_value_expr_match_is_int_bool_octet_channel( + scrutinee: scrutinee, + arms: arms + ) { + bind_outcome( + o: target_value_expr_int_bool_octet_scrutinee_carrier_tokens( + scrutinee_tokens: scrutinee_tokens, + catalog: catalog, + projection: projection + ), + f: fn(carrier_scrutinee_tokens) { + bind_outcome( + o: target_value_expr_match_arm_tokens_int_bool_octet_channel( + arms: arms, + projection: projection, + catalog: catalog ), - right: Cons { - head: FixedToken { - token_class: projection.match_form.close - }, - tail: Empty + f: fn(arm_tokens) { + outcome_accepted( + target_value_expression_match_concrete_token_shell( + scrutinee_tokens: carrier_scrutinee_tokens, + arm_tokens: arm_tokens, + projection: projection + ) + ) } ) - ) - } - ) + } + ) + } else { + bind_outcome( + o: target_value_expr_match_arm_tokens( + arms: arms, + projection: projection, + catalog: catalog + ), + f: fn(arm_tokens) { + outcome_accepted( + target_value_expression_match_concrete_token_shell( + scrutinee_tokens: scrutinee_tokens, + arm_tokens: arm_tokens, + projection: projection + ) + ) + } + ) + } } ) } @@ -6058,18 +6234,66 @@ fn target_value_expression_match_to_concrete_tokens_inner( ) } +fn target_value_expression_match_concrete_token_shell( + scrutinee_tokens: List, + arm_tokens: List, + projection: TargetValueExpressionProjection +) -> List { + let prefix = concrete_syntax_tokens_snoc_fixed( + acc: concrete_syntax_tokens_snoc_fixed( + acc: Empty, + token_class: projection.match_form.match_token + ), + token_class: projection.match_form.scrutinee_open + ) + let with_scrutinee = concrete_syntax_tokens_extend( + acc: prefix, + more: scrutinee_tokens + ) + let with_scrutinee_close = concrete_syntax_tokens_snoc_fixed( + acc: with_scrutinee, + token_class: projection.match_form.scrutinee_close + ) + let with_open = concrete_syntax_tokens_snoc_fixed( + acc: with_scrutinee_close, + token_class: projection.match_form.open + ) + let with_arms = concrete_syntax_tokens_extend( + acc: with_open, + more: arm_tokens + ) + concrete_syntax_tokens_snoc_fixed( + acc: with_arms, + token_class: projection.match_form.close + ) +} + fn target_value_expression_symbol_identity_to_concrete_tokens( - expr: TargetValueExpression + expr: TargetValueExpression, + projection: TargetValueExpressionProjection ) -> Outcome> { bind_outcome( o: target_value_expression_symbol_identity_from_wire(wire: expr.node), f: fn(token_class) { - outcome_accepted( - Cons { - head: FixedToken { token_class: token_class }, - tail: Empty - } - ) + match target_value_expr_binding_ref_for_literal_atom(id: token_class) { + Present { value: binding } => + outcome_accepted( + Cons { + head: target_value_expression_binding_ref_token( + binding: binding, + projection: projection + ), + tail: Empty + } + ) + Absent => + outcome_accepted( + Cons { + head: FixedToken { token_class: token_class }, + tail: Empty + } + ) + } } ) } @@ -6526,7 +6750,10 @@ fn target_value_expression_to_concrete_tokens( catalog: catalog ) TargetValueExprSymbolIdentity => - target_value_expression_symbol_identity_to_concrete_tokens(expr: expr) + target_value_expression_symbol_identity_to_concrete_tokens( + expr: expr, + projection: projection + ) TargetValueExprConditional => target_value_expression_conditional_to_concrete_tokens( expr: expr, @@ -10648,6 +10875,43 @@ fn target_value_expr_binding_in_declared_param_list( }) } +fn target_value_expr_param_binding_for_referent( + referent: Symbol, + bindings: List, + target: TargetModel +) -> Optional { + if target_value_expr_binding_in_declared_param_list(binding: referent, bindings: bindings) { + optional_present(value: referent) + } else { + match target_binding_spelling_lookup(target: target, binding: referent) { + Accepted { value: referent_spelling, diagnostics: _ } => + fold_list( + xs: bindings, + empty: optional_absent(), + cons: fn(acc, param_binding) { + match acc { + Present { value: _ } => acc + Absent => + match target_binding_spelling_lookup( + target: target, + binding: param_binding + ) { + Accepted { value: param_spelling, diagnostics: _ } => + if param_spelling == referent_spelling { + optional_present(value: param_binding) + } else { + acc + } + Rejected { diagnostics: _ } => acc + } + } + } + ) + Rejected { diagnostics: _ } => optional_absent() + } + } +} + fn target_value_expr_arrow_body_scope_binding( arrow: Node, body: Node, @@ -10657,19 +10921,31 @@ fn target_value_expr_arrow_body_scope_binding( bind_outcome( o: arrow_domain_named_param_bindings(arrow: arrow), f: fn(bindings) { - if target_value_expr_binding_in_declared_param_list(binding: binding, bindings: bindings) - && ( - target_value_expr_add_signature_matches_for_target(arrow: arrow, target: target) - || target_value_expr_arrow_has_transform_body(arrow: arrow) - ) { - outcome_accepted(binding) - } else { - outcome_rejected( - target_value_expr_diagnostic( - reason: ^target_value_expr_reason_body_scope_binding_invalid, - node: body + match target_value_expr_param_binding_for_referent( + referent: binding, + bindings: bindings, + target: target + ) { + Present { value: scoped } => + if target_value_expr_add_signature_matches_for_target(arrow: arrow, target: target) + || target_value_expr_arrow_has_transform_body(arrow: arrow) + || target_value_expr_arrow_has_match_body(arrow: arrow) { + outcome_accepted(scoped) + } else { + outcome_rejected( + target_value_expr_diagnostic( + reason: ^target_value_expr_reason_body_scope_binding_invalid, + node: body + ) + ) + } + Absent => + outcome_rejected( + target_value_expr_diagnostic( + reason: ^target_value_expr_reason_body_scope_binding_invalid, + node: body + ) ) - ) } } ) @@ -10838,38 +11114,86 @@ fn target_value_expr_branch_bool_gate(node: Node) -> Bool { } } -fn target_value_expr_project_pick_literal_atom(id: Symbol) -> Outcome { +fn target_value_expr_binding_ref_for_literal_atom(id: Symbol) -> Optional { if id == ^dag_pick_lit_one { - outcome_accepted( - target_value_expression_binding_ref(binding: ^dag_binding_pick_lit_one) - ) + optional_present(value: ^dag_binding_pick_lit_one) } else if id == ^dag_pick_lit_two { - outcome_accepted( - target_value_expression_binding_ref(binding: ^dag_binding_pick_lit_two) - ) + optional_present(value: ^dag_binding_pick_lit_two) } else if id == ^dag_rec_lit_nine { - outcome_accepted( - target_value_expression_binding_ref(binding: ^dag_binding_rec_lit_nine) - ) + optional_present(value: ^dag_binding_rec_lit_nine) } else if id == ^dag_binding_param_r { - outcome_accepted( - target_value_expression_binding_ref(binding: ^dag_binding_param_r) - ) + optional_present(value: ^dag_binding_param_r) + } else if id == ^dag_binding_param_x { + optional_present(value: ^dag_binding_param_x) + } else if id == ^dag_binding_param_y { + optional_present(value: ^dag_binding_param_y) + } else if id == ^rust_binding_param_x { + optional_present(value: ^rust_binding_param_x) + } else if id == ^rust_binding_param_y { + optional_present(value: ^rust_binding_param_y) } else if id == ^dag_binding_rec_v { - outcome_accepted( - target_value_expression_binding_ref(binding: ^dag_binding_rec_v) - ) + optional_present(value: ^dag_binding_rec_v) } else { - outcome_accepted( - target_value_expression_symbol_identity(identity: id) - ) + optional_absent() + } +} + +fn target_value_expr_project_pick_literal_atom(id: Symbol) -> Outcome { + match target_value_expr_binding_ref_for_literal_atom(id: id) { + Present { value: binding } => + outcome_accepted( + target_value_expression_binding_ref(binding: binding) + ) + Absent => + outcome_accepted( + target_value_expression_symbol_identity(identity: id) + ) + } +} + +fn target_value_expr_project_atom_in_arrow_scope( + arrow: Node, + node: Node, + target: TargetModel +) -> Outcome { + match node.kind { + TypeNode { connective: Atom { identity: id } } => + match target_value_expr_arrow_body_scope_binding( + arrow: arrow, + body: node, + binding: id, + target: target + ) { + Accepted { value: scoped, diagnostics: d } => + outcome_accepted( + target_value_expression_binding_ref(binding: scoped) + ) + Rejected { diagnostics: _ } => + target_value_expr_project_atom_literal(node: node) + } + _ => + outcome_rejected( + target_value_expr_diagnostic( + reason: ^target_value_expr_reason_transform_shape_invalid, + node: node + ) + ) } } fn target_value_expr_project_atom_literal(node: Node) -> Outcome { match node.kind { TypeNode { connective: Atom { identity: id } } => - target_value_expr_project_pick_literal_atom(id: id) + if id == ^target_value_expression_symbol_identity_atom { + bind_outcome( + o: target_value_expression_symbol_identity_from_wire(wire: node), + f: fn(inner_id) { + target_value_expr_project_pick_literal_atom(id: inner_id) + } + ) + } else { + target_value_expr_project_pick_literal_atom(id: id) + } _ => outcome_rejected( target_value_expr_diagnostic( @@ -11489,7 +11813,11 @@ fn target_value_expr_project_body_subexpression( handle_transform: handle_transform ) TypeNode { connective: Atom { identity: _ } } => - target_value_expr_project_atom_literal(node: node) + target_value_expr_project_atom_in_arrow_scope( + arrow: arrow, + node: node, + target: target + ) _ => outcome_rejected( target_value_expr_diagnostic( diff --git a/src/v2/test/claim/manual/body_lowering_match.dag b/src/v2/test/claim/manual/body_lowering_match.dag new file mode 100644 index 00000000000..f25d61e31eb --- /dev/null +++ b/src/v2/test/claim/manual/body_lowering_match.dag @@ -0,0 +1,313 @@ +module v2.test.manual.body_lowering_match + +import v2.compiler.body_lowering_fold { + body_lower_match_arms_optional, + body_lower_try_match_from_captured, + body_lower_unwrap_captured, + body_lower_wire_match_arm_capture +} +import v2.compiler.normalize { normalize } +import v2.compiler.parse { parse_module } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { + dag_language_model, + parse_production_emitted_identity_optional, + parse_subtree_find_production_captured +} +import std.algebra { Empty } +import v2.std.algebra { length } +import v2.std.collection { Absent, Optional, Present } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.logic { Bool } +import v2.std.node { + Atom, + ComputationNode, + Conj, + Match, + Node, + TypeNode, + node_synthetic +} +import v2.std.verification { + EqualsClaim, + ManualAnchorAbsent, + TestClaim, + TestClassification, + Tier1, + Unit, + manual_claim_anchor +} + +data body_lowering_match_source: String = "module m\n\nfn classical_not(a: Int) -> Int {\n match a {\n true => false,\n false => true\n }\n}\n" + +data body_lowering_match_swapped_source: String = "module m\n\nfn classical_not(a: Int) -> Int {\n match a {\n true => true,\n false => false\n }\n}\n" + +fn body_lowering_match_bool_node(pass: Bool) -> Node { + if pass { + node_synthetic( + kind: TypeNode { connective: Atom { identity: ^body_lowering_match_pass } }, + children: [] + ) + } else { + node_synthetic( + kind: TypeNode { connective: Atom { identity: ^body_lowering_match_fail } }, + children: [] + ) + } +} + +fn body_lowering_find_match_expr(root: Node) -> Optional { + match parse_production_emitted_identity_optional(node: root) { + Present { value: emitted } => + match emitted == ^dag_surface_match_expr { + true => Present { value: root } + false => + fold(root.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => body_lowering_find_match_expr(root: e.target) + } + }) + } + Absent => + fold(root.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => body_lowering_find_match_expr(root: e.target) + } + }) + } +} + +fn body_lowering_tree_has_match_behavior(root: Node) -> Bool { + match root.kind { + ComputationNode { behavior: Match } => true + _ => + fold(root.children, init: false, f: fn(found, e) { + if found { + true + } else { + body_lowering_tree_has_match_behavior(root: e.target) + } + }) + } +} + +fn body_lowering_parsed_tree(source: String) -> Optional { + let lm = dag_language_model() + match tokenize(text: source, file: ^body_lowering_match_file, rules: lm.lex) { + Rejected { diagnostics: _ } => Absent + Accepted { value: ts, diagnostics: _ } => + match parse_module(tokens: ts, grammar: lm.grammar) { + Rejected { diagnostics: _ } => Absent + Accepted { value: artifact, diagnostics: _ } => Present { value: artifact.tree } + } + } +} + +fn body_lowering_match_lowers_to_match() -> Bool { + match body_lowering_parsed_tree(source: body_lowering_match_source) { + Absent => false + Present { value: tree } => + match body_lowering_find_match_expr(root: tree) { + Absent => false + Present { value: shell } => + match body_lower_unwrap_captured(shell: shell) { + Present { value: captured } => + match body_lower_try_match_from_captured(captured: captured) { + Rejected { diagnostics: _ } => false + Accepted { value: lowered_opt, diagnostics: _ } => + match lowered_opt { + Present { value: lowered } => + match lowered.kind { + ComputationNode { behavior: Match } => true + _ => false + } + Absent => false + } + } + Absent => false + } + } + } +} + +fn body_lowering_normalize_accepts_match_module() -> Bool { + match body_lowering_parsed_tree(source: body_lowering_match_source) { + Absent => false + Present { value: tree } => + match normalize(parse_tree: tree) { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: _ } => true + } + } +} + +fn body_lowering_normalized_module_has_match() -> Bool { + match body_lowering_parsed_tree(source: body_lowering_match_source) { + Absent => false + Present { value: tree } => + match normalize(parse_tree: tree) { + Rejected { diagnostics: _ } => false + Accepted { value: normalized, diagnostics: _ } => + body_lowering_tree_has_match_behavior(root: normalized) + } + } +} + +fn body_lowering_match_swapped_arms_normalize_accepts() -> Bool { + match body_lowering_parsed_tree(source: body_lowering_match_swapped_source) { + Absent => false + Present { value: tree } => + match normalize(parse_tree: tree) { + Rejected { diagnostics: _ } => false + Accepted { value: _, diagnostics: _ } => true + } + } +} + +fn body_lowering_match_arms_found() -> Bool { + match body_lowering_parsed_tree(source: body_lowering_match_source) { + Absent => false + Present { value: tree } => + match body_lowering_find_match_expr(root: tree) { + Absent => false + Present { value: shell } => + match body_lower_unwrap_captured(shell: shell) { + Present { value: captured } => + match body_lower_match_arms_optional(captured: captured) { + Rejected { diagnostics: _ } => false + Accepted { value: arms_opt, diagnostics: _ } => + match arms_opt { + Present { value: arms } => length(xs: arms) > 0 + Absent => false + } + } + Absent => false + } + } + } +} + +fn body_lowering_match_first_arm_wires() -> Bool { + match body_lowering_parsed_tree(source: body_lowering_match_source) { + Absent => false + Present { value: tree } => + match body_lowering_find_match_expr(root: tree) { + Absent => false + Present { value: shell } => + match body_lower_unwrap_captured(shell: shell) { + Present { value: captured } => + match parse_subtree_find_production_captured( + root: captured, + emitted: ^dag_surface_match_arm + ) { + ParseSubtreeFound { captured: arm } => + match body_lower_wire_match_arm_capture(arm_capture: arm) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } + ParseSubtreeAbsent => false + } + Absent => false + } + } + } +} + +fn body_lowering_match_unnavigable_arm_refuses() -> Bool { + match body_lower_wire_match_arm_capture( + arm_capture: node_synthetic( + kind: TypeNode { connective: Conj }, + children: Empty + ) + ) { + Rejected { diagnostics: d } => + d.head.reason == ^body_lowering_reason_match_arm_navigation_refused + Accepted { value: _, diagnostics: _ } => false + } +} + +data claim_body_lowering_match_arms_found: TestClaim = EqualsClaim { + label: "manual/body-lowering-match: classical_not arms discoverable", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: body_lowering_match_bool_node(pass: body_lowering_match_arms_found()), + rhs: body_lowering_match_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_body_lowering_match_lowers_to_match: TestClaim = EqualsClaim { + label: "manual/body-lowering-match: match_expr lowers to Match computation", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: body_lowering_match_bool_node(pass: body_lowering_match_lowers_to_match()), + rhs: body_lowering_match_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_body_lowering_match_normalize_accepts: TestClaim = EqualsClaim { + label: "manual/body-lowering-match: classical_not module normalizes without refusal", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: body_lowering_match_bool_node(pass: body_lowering_normalize_accepts_match_module()), + rhs: body_lowering_match_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_body_lowering_match_normalized_has_match: TestClaim = EqualsClaim { + label: "manual/body-lowering-match: normalized classical_not retains Match behavior", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: body_lowering_match_bool_node(pass: body_lowering_normalized_module_has_match()), + rhs: body_lowering_match_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_body_lowering_match_swapped_normalize_accepts: TestClaim = EqualsClaim { + label: "manual/body-lowering-match: swapped-arm module normalizes without refusal", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: body_lowering_match_bool_node(pass: body_lowering_match_swapped_arms_normalize_accepts()), + rhs: body_lowering_match_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_body_lowering_match_first_arm_wires: TestClaim = EqualsClaim { + label: "manual/body-lowering-match: true=>false arm wires pattern and body", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: body_lowering_match_bool_node(pass: body_lowering_match_first_arm_wires()), + rhs: body_lowering_match_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_body_lowering_match_unnavigable_arm_refuses: TestClaim = EqualsClaim { + label: "manual/body-lowering-match: unnavigable arm subtree refuses (fail-closed)", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: body_lowering_match_bool_node(pass: body_lowering_match_unnavigable_arm_refuses()), + rhs: body_lowering_match_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +fn body_lowering_match_arms_found_witness() -> Bool { + body_lowering_match_arms_found() +} + +fn body_lowering_match_lowers_to_match_witness() -> Bool { + body_lowering_match_lowers_to_match() +} + +fn body_lowering_normalize_accepts_match_module_witness() -> Bool { + body_lowering_normalize_accepts_match_module() +} + +fn body_lowering_normalized_module_has_match_witness() -> Bool { + body_lowering_normalized_module_has_match() +} + +fn body_lowering_match_swapped_arms_normalize_accepts_witness() -> Bool { + body_lowering_match_swapped_arms_normalize_accepts() +} + +fn body_lowering_match_first_arm_wires_witness() -> Bool { + body_lowering_match_first_arm_wires() +} + +fn body_lowering_match_unnavigable_arm_refuses_witness() -> Bool { + body_lowering_match_unnavigable_arm_refuses() +} diff --git a/src/v2/test/claim/manual/emit_host_classical_not_ingested_equals_eval_test.dag b/src/v2/test/claim/manual/emit_host_classical_not_ingested_equals_eval_test.dag new file mode 100644 index 00000000000..ef6341f2ad8 --- /dev/null +++ b/src/v2/test/claim/manual/emit_host_classical_not_ingested_equals_eval_test.dag @@ -0,0 +1,593 @@ +module v2.test.manual.emit_host_classical_not_ingested_equals_eval + +import v2.compiler.emit { emit } +import v2.compiler.emit_host { + emit_host_octets_byte_string, + run_test_claim_emit_vs_eval +} +import v2.compiler.eval { + EvalContext, + TestClaimEvalSubject, + TestClaimRun, + eval, + eval_context_with_semantics, + eval_test_claim_subject, + inputs_root_only +} +import extdeps.communication.medium { Medium } +import v2.compiler.infer { InferredFacts, InferredTree, infer } +import v2.compiler.normalize { normalize } +import v2.compiler.parse { parse_module } +import v2.compiler.resolve { resolve } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { + dag_arrow_with_body_node, + dag_language_model, + dag_match_arm_node, + dag_match_body_from_arms, + dag_type_atom_node +} +import v2.extdeps.languages.rust { rust_emit_host_runtime_primitive_type_node, rust_target_model_staging } +import v2.extdeps.languages.rust_test { + rust_classical_not_ingested_target_model_staging, + rust_match_target_model_staging +} +import v2.test.lens_common.infer_fixture { claim_inferred_facts_from_nodes } +import v2.std.cardinality { RankingDimension, TerminationProof } +import v2.std.collection { Absent, List, Map, Optional, Present, list_at_optional } +import v2.std.compilers.target_model { match_arm_body } +import v2.std.diagnostic { + Accepted, + Diagnostic, + ExternalContractUnknown, + Outcome, + Rejected, + Unavailable, + bind_outcome, + node_locus, + outcome_accepted, + outcome_rejected +} +import v2.std.logic { Bool } +import v2.std.node { + Arrow, + Atom, + ComputationNode, + Conj, + Edge, + Match, + Node, + Symbol, + SyntheticOccurrence, + TypeNode +} +import v2.std.node_query { find_arrow_body_child, find_named_child } +import v2.std.runtime { + BindInterpreter, + BranchInterpreter, + ControlTransfer, + EnvironmentBindingKey, + EvaluationEnvironment, + InterpretationAlgebra, + InterpretationStructureWitness, + LoopInterpreter, + MatchInterpreter, + RuntimePrimitive, + RuntimePrimitiveValue, + RuntimeValue, + TransformInterpreter, + ValueInterpreter +} +import v2.std.verdict { Deferred, Fail, Pass } +import v2.std.verification { + EqualsClaim, + Integration, + ManualAnchorAbsent, + TestClaim, + TestClassification, + Tier3, + manual_claim_anchor +} +import v2.std.witness { Holds, Witness } + +data ingested_classical_not_source: String = "module m\n\nfn classical_not(x: Int) -> Int {\n match x {\n true => false,\n false => true\n }\n}\n" + +data ingested_classical_not_swapped_source: String = "module m\n\nfn classical_not(x: Int) -> Int {\n match x {\n true => true,\n false => false\n }\n}\n" + +fn ingested_find_arrow_in_module(root: Node) -> Optional { + match root.kind { + TypeNode { connective: Arrow } => Present { value: root } + _ => + fold(root.children, init: Absent, f: fn(acc, e) { + match acc { + Present { value: _ } => acc + Absent => ingested_find_arrow_in_module(root: e.target) + } + }) + } +} + +fn ingested_resolved_module_from_source(source: String) -> Outcome { + let lm = dag_language_model() + bind_outcome( + o: tokenize(text: source, file: ^ingested_classical_not_file, rules: lm.lex), + f: fn(tokens) { + bind_outcome( + o: parse_module(tokens: tokens, grammar: lm.grammar), + f: fn(artifact) { + bind_outcome( + o: normalize(parse_tree: artifact.tree), + f: fn(normalized) { + resolve(tree: normalized, lm: lm) + } + ) + } + ) + } + ) +} + +fn ingested_arrow_from_source(source: String) -> Outcome { + bind_outcome( + o: ingested_resolved_module_from_source(source: source), + f: fn(resolved) { + match ingested_find_arrow_in_module(root: resolved) { + Present { value: arrow } => outcome_accepted(value: arrow) + Absent => + outcome_rejected( + d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_arrow_miss, node: resolved) + ) + } + } + ) +} + +fn ingested_match_body_from_source(source: String) -> Outcome { + bind_outcome( + o: ingested_arrow_from_source(source: source), + f: fn(arrow) { + find_arrow_body_child(root: arrow) + } + ) +} +fn ingested_inferred_tree_from_source(source: String) -> Outcome { + bind_outcome( + o: ingested_arrow_from_source(source: source), + f: fn(arrow) { + bind_outcome( + o: infer(tree: arrow), + f: fn(inferred) { + outcome_accepted( + value: InferredTree { + root: inferred.root, + facts: Map { + lookup: fn(key) { + match inferred.facts.lookup(key: key) { + Holds { value: _ } => inferred.facts.lookup(key: key) + Violates { diagnostic: _ } => + ingested_classical_not_composed_facts(key: key) + } + } + } + } + ) + } + ) + } + ) +} + +fn ingested_classical_not_eval_subgraph_canonical() -> Node { + dag_match_body_from_arms( + scrutinee: dag_type_atom_node(identity: ^dag_token_kw_true), + true_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_true, + body_lit: ^dag_token_kw_false + ), + false_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_false, + body_lit: ^dag_token_kw_true + ) + ) +} + +fn ingested_classical_not_eval_subgraph_swapped() -> Node { + dag_match_body_from_arms( + scrutinee: dag_type_atom_node(identity: ^dag_token_kw_true), + true_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_true, + body_lit: ^dag_token_kw_true + ), + false_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_false, + body_lit: ^dag_token_kw_false + ) + ) +} + +fn ingested_classical_not_diagnostic(reason: Symbol, node: Node) -> Diagnostic { + Diagnostic { + reason: reason, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn ingested_resolves(source: String) -> Bool { + match ingested_resolved_module_from_source(source: source) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +fn ingested_arrow_has_match_body(source: String) -> Bool { + match ingested_arrow_from_source(source: source) { + Accepted { value: arrow, diagnostics: _ } => + match find_arrow_body_child(root: arrow) { + Accepted { value: body, diagnostics: _ } => + match body.kind { + ComputationNode { behavior: Match } => true + _ => false + } + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +fn ingested_classical_not_generic_facts(node: Node) -> InferredFacts { + claim_inferred_facts_from_nodes( + resolved: node, + algebra: rust_emit_host_runtime_primitive_type_node(), + descent: Holds { + value: TerminationProof { + non_increasing: [], + strict: RankingDimension { measured: ^ingested_classical_not_generic_descent } + } + } + ) +} + +fn ingested_classical_not_composed_facts(key: Node) -> Witness { + Holds { value: ingested_classical_not_generic_facts(node: key) } +} + +fn ingested_classical_not_octet_value(n: Int) -> RuntimeValue { + RuntimePrimitive { + value: RuntimePrimitiveValue { + primitive_type: rust_emit_host_runtime_primitive_type_node(), + bytes: emit_host_octets_byte_string(octets: [0, n, 0, 0, 0]) + } + } +} + +fn ingested_classical_not_bool_true(value: RuntimeValue) -> Bool { + value == ingested_classical_not_octet_value(n: 1) +} + +fn ingested_classical_not_bool_false(value: RuntimeValue) -> Bool { + value == ingested_classical_not_octet_value(n: 0) +} + +fn ingested_classical_not_allocate_literal(node: Node, _env: EvaluationEnvironment) -> Outcome { + match node.kind { + TypeNode { connective: Atom { identity: id } } => + if id == ^dag_token_kw_true { + outcome_accepted(value: ingested_classical_not_octet_value(n: 1)) + } else if id == ^dag_token_kw_false { + outcome_accepted(value: ingested_classical_not_octet_value(n: 0)) + } else { + outcome_rejected( + d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_literal_miss, node: node) + ) + } + _ => + outcome_rejected( + d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_literal_miss, node: node) + ) + } +} + +fn ingested_classical_not_call_primitive( + node: Node, + _args: List, + _env: EvaluationEnvironment +) -> Outcome { + outcome_rejected( + d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_call_primitive_miss, node: node) + ) +} + +fn ingested_classical_not_choose_branch( + node: Node, + _value: RuntimeValue, + _env: EvaluationEnvironment +) -> Outcome { + outcome_rejected( + d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_branch_miss, node: node) + ) +} + +fn ingested_classical_not_step_loop( + node: Node, + _env: EvaluationEnvironment +) -> Outcome { + outcome_rejected( + d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_loop_miss, node: node) + ) +} + +fn ingested_classical_not_bind_value( + _key: EnvironmentBindingKey, + _value: RuntimeValue, + env: EvaluationEnvironment +) -> Outcome { + outcome_accepted(value: env) +} + +fn ingested_classical_not_nth_arm_wire(node: Node, wanted: Int) -> Outcome { + match list_at_optional(xs: node.children, index: wanted) { + Present { value: child } => + match child { + Edge { label: _, target: arm_wire } => outcome_accepted(value: arm_wire) + } + Absent => + outcome_rejected( + d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_arm_miss, node: node) + ) + } +} + +fn ingested_classical_not_arm_body_node(arm_wire: Node) -> Outcome { + match find_named_child(root: arm_wire, name: match_arm_body) { + Accepted { value: body, diagnostics: _ } => outcome_accepted(value: body) + Rejected { diagnostics: r } => Rejected { diagnostics: r } + } +} + +fn ingested_classical_not_choose_arm( + node: Node, + scrutinee: RuntimeValue, + _env: EvaluationEnvironment +) -> Outcome { + if ingested_classical_not_bool_true(value: scrutinee) { + match ingested_classical_not_nth_arm_wire(node: node, wanted: 1) { + Accepted { value: arm, diagnostics: _ } => + ingested_classical_not_arm_body_node(arm_wire: arm) + Rejected { diagnostics: r } => Rejected { diagnostics: r } + } + } else if ingested_classical_not_bool_false(value: scrutinee) { + match ingested_classical_not_nth_arm_wire(node: node, wanted: 2) { + Accepted { value: arm, diagnostics: _ } => + ingested_classical_not_arm_body_node(arm_wire: arm) + Rejected { diagnostics: r } => Rejected { diagnostics: r } + } + } else { + outcome_rejected( + d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_arm_miss, node: node) + ) + } +} + +fn ingested_classical_not_interpretation() -> InterpretationAlgebra { + InterpretationAlgebra { + value: ValueInterpreter { allocate_literal: ingested_classical_not_allocate_literal }, + transform: TransformInterpreter { call_primitive: ingested_classical_not_call_primitive }, + branch: BranchInterpreter { choose_branch: ingested_classical_not_choose_branch }, + loop: LoopInterpreter { step_loop: ingested_classical_not_step_loop }, + bind: BindInterpreter { bind_value: ingested_classical_not_bind_value }, + match: MatchInterpreter { choose_arm: ingested_classical_not_choose_arm } + } +} + +fn ingested_classical_not_structure_witness() -> InterpretationStructureWitness { + InterpretationStructureWitness { + allocate_literal: ^ingested_classical_not_allocate_literal_sym, + call_primitive: ^ingested_classical_not_call_primitive_sym, + choose_branch: ^ingested_classical_not_choose_branch_sym, + step_loop: ^ingested_classical_not_step_loop_sym, + bind_value: ^ingested_classical_not_bind_value_sym, + choose_arm: ^ingested_classical_not_choose_arm_sym + } +} + +fn ingested_classical_not_context() -> EvalContext { + eval_context_with_semantics( + runtime_identity: ^ingested_classical_not_interpretation_pin, + interpretation: ingested_classical_not_interpretation(), + structure_witness: ingested_classical_not_structure_witness() + ) +} + +fn ingested_classical_not_claim(rhs_result_node: Node) -> TestClaim { + EqualsClaim { + label: "Wave1 exit: ingested classical_not emit-host == eval (true scrutinee → false)", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: rhs_result_node, + rhs: rhs_result_node, + classification: TestClassification { tier: Tier3, layer: Integration } + } +} + +fn ingested_classical_not_subject(tree: InferredTree, subgraph: Node) -> TestClaimEvalSubject { + eval_test_claim_subject( + claim: ingested_classical_not_claim(rhs_result_node: subgraph), + context: ingested_classical_not_context(), + tree: tree, + evaluator_pin: ^ingested_classical_not_evaluator_pin + ) +} + +fn ingested_classical_not_run(tree: InferredTree, subgraph: Node) -> TestClaimRun { + run_test_claim_emit_vs_eval( + subject: ingested_classical_not_subject(tree: tree, subgraph: subgraph), + target: rust_classical_not_ingested_target_model_staging() + ) +} + +fn ingested_classical_not_verdict_is_pass(run: TestClaimRun) -> Bool { + match run.verdict { + Pass => true + Fail { actual: _, falsification: _ } => false + Deferred { actual: _, diagnostic: _ } => false + } +} + +fn ingested_classical_not_verdict_is_fail(run: TestClaimRun) -> Bool { + match run.verdict { + Fail { actual: _, falsification: _ } => true + Pass => false + Deferred { actual: _, diagnostic: _ } => false + } +} + +test fn ingested_classical_not_eval_subgraph_canonical_octet_zero_holds() -> Bool { + match ingested_inferred_tree_from_source(source: ingested_classical_not_source) { + Accepted { value: tree, diagnostics: _ } => + match eval( + tree: tree, + interpretation: ingested_classical_not_interpretation(), + inputs: inputs_root_only(root: ingested_classical_not_eval_subgraph_canonical()) + ) { + Accepted { value: v, diagnostics: _ } => + v == ingested_classical_not_octet_value(n: 0) + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn ingested_classical_not_emit_octet_bridge_shape_holds() -> Bool { + match ingested_inferred_tree_from_source(source: ingested_classical_not_source) { + Accepted { value: tree, diagnostics: _ } => + match emit(tree: tree, target: rust_classical_not_ingested_target_model_staging()) { + Accepted { value: Medium { carried: source, fidelity: _ }, diagnostics: _ } => + string_contains(s: source, pattern: "!= ") + && string_contains(s: source, pattern: "true => 0") + && string_contains(s: source, pattern: "false => 1") + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn ingested_classical_not_emit_source_arm_shape_holds() -> Bool { + match ingested_inferred_tree_from_source(source: ingested_classical_not_source) { + Accepted { value: tree, diagnostics: _ } => + match emit(tree: tree, target: rust_classical_not_ingested_target_model_staging()) { + Accepted { value: Medium { carried: source, fidelity: _ }, diagnostics: _ } => + string_contains(s: source, pattern: "pub fn classical_not(x") + || string_contains(s: source, pattern: "fn classical_not(x") + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn ingested_classical_not_resolves_holds() -> Bool { + ingested_resolves(source: ingested_classical_not_source) +} + +test fn ingested_classical_not_arrow_has_match_holds() -> Bool { + ingested_arrow_has_match_body(source: ingested_classical_not_source) +} + +test fn emit_host_classical_not_ingested_equals_eval_holds() -> Bool { + match ingested_inferred_tree_from_source(source: ingested_classical_not_source) { + Accepted { value: tree, diagnostics: _ } => + ingested_classical_not_verdict_is_pass( + run: ingested_classical_not_run( + tree: tree, + subgraph: ingested_classical_not_eval_subgraph_canonical() + ) + ) + Rejected { diagnostics: _ } => false + } +} + +test fn emit_host_classical_not_ingested_swapped_refuses_holds() -> Bool { + match ingested_inferred_tree_from_source(source: ingested_classical_not_swapped_source) { + Accepted { value: tree, diagnostics: _ } => + ingested_classical_not_verdict_is_fail( + run: ingested_classical_not_run( + tree: tree, + subgraph: ingested_classical_not_eval_subgraph_canonical() + ) + ) + Rejected { diagnostics: _ } => false + } +} + +test fn ingested_classical_not_emit_accepts_holds() -> Bool { + match ingested_inferred_tree_from_source(source: ingested_classical_not_source) { + Accepted { value: tree, diagnostics: _ } => + match emit(tree: tree, target: rust_target_model_staging()) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn ingested_classical_not_real_infer_holds() -> Bool { + match ingested_arrow_from_source(source: ingested_classical_not_source) { + Accepted { value: arrow, diagnostics: _ } => + match infer(tree: arrow) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +fn ingested_classical_not_match_only_param_body_fixture() -> Node { + dag_match_body_from_arms( + scrutinee: dag_type_atom_node(identity: ^dag_binding_param_x), + true_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_true, + body_lit: ^dag_token_kw_false + ), + false_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_false, + body_lit: ^dag_token_kw_true + ) + ) +} + +fn ingested_classical_not_arrow_empty_domain_fixture() -> Node { + dag_arrow_with_body_node( + domain: Node { + kind: TypeNode { connective: Conj }, + children: [], + occurrence_id: SyntheticOccurrence + }, + return_type_binding: ^dag_binding_type_int, + body: ingested_classical_not_match_only_param_body_fixture() + ) +} + +fn ingested_classical_not_param_scrutinee_domain_unresolved_infer_refuses(tree: Node) -> Bool { + match infer(tree: tree) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn ingested_classical_not_match_only_param_scrutinee_infer_refuses_holds() -> Bool { + ingested_classical_not_param_scrutinee_domain_unresolved_infer_refuses( + tree: ingested_classical_not_match_only_param_body_fixture() + ) +} + +test fn ingested_classical_not_arrow_empty_domain_infer_refuses_holds() -> Bool { + ingested_classical_not_param_scrutinee_domain_unresolved_infer_refuses( + tree: ingested_classical_not_arrow_empty_domain_fixture() + ) +} + +test fn emit_host_classical_not_ingested_all_holds() -> Bool { + ingested_classical_not_resolves_holds() + && ingested_classical_not_arrow_has_match_holds() + && emit_host_classical_not_ingested_equals_eval_holds() + && emit_host_classical_not_ingested_swapped_refuses_holds() +} diff --git a/src/v2/test/claim/manual/match_infer_fail_open_audit_test.dag b/src/v2/test/claim/manual/match_infer_fail_open_audit_test.dag index 95eea519e76..29793a710af 100644 --- a/src/v2/test/claim/manual/match_infer_fail_open_audit_test.dag +++ b/src/v2/test/claim/manual/match_infer_fail_open_audit_test.dag @@ -2,20 +2,37 @@ module v2.test.manual.match_infer_fail_open_audit import v2.compiler.infer { infer } import v2.extdeps.languages.dag { + dag_arrow_with_body_node, + dag_complement_arrow_with_body_fixture, + dag_complement_body_fixture, dag_match_arm_node, dag_match_body_from_arms, dag_match_if_body_fixture, dag_type_atom_node } -import v2.std.diagnostic { Accepted, None, Outcome, Rejected } +import v2.std.algebra { fold_list } +import v2.std.diagnostic { + Accepted, + Diagnostics, + None, + NonEmptyDiagnostics, + Outcome, + Rejected, + Some +} import v2.std.logic { Bool } import v2.std.node { + Atom, + Conj, ComputationNode, Edge, Match, + Named, Node, Positional, - SyntheticOccurrence + Symbol, + SyntheticOccurrence, + TypeNode } import v2.std.verification { BoolWitness, @@ -26,6 +43,27 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly +fn diagnostics_contain_reason(d: Diagnostics, reason: Symbol) -> Bool { + match d { + None => false + Some { diagnostics: nes } => non_empty_diagnostics_contain_reason(nes: nes, reason: reason) + } +} + +fn non_empty_diagnostics_contain_reason(nes: NonEmptyDiagnostics, reason: Symbol) -> Bool { + if nes.head.reason == reason { + true + } else { + fold_list( + xs: nes.tail, + empty: false, + cons: fn(acc, diag) { + acc || diag.reason == reason + } + ) + } +} + fn match_infer_fail_open_audit_body() -> Node { dag_match_body_from_arms( scrutinee: dag_type_atom_node(identity: ^dag_token_kw_true), @@ -121,3 +159,91 @@ fn match_infer_fail_open_audit_literal_arm_accepts_holds() -> Bool { Rejected { diagnostics: _ } => false } } + +fn classical_not_int_match_arrow_fixture() -> Node { + dag_arrow_with_body_node( + domain: Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: ^dag_binding_param_x }, + target: dag_type_atom_node(identity: ^dag_binding_type_int) + } + ], + occurrence_id: SyntheticOccurrence + }, + return_type_binding: ^dag_binding_type_int, + body: dag_match_body_from_arms( + scrutinee: dag_type_atom_node(identity: ^dag_binding_param_x), + true_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_true, + body_lit: ^dag_token_kw_false + ), + false_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_false, + body_lit: ^dag_token_kw_true + ) + ) + ) +} + +test fn complement_body_real_infer_refuses_unsupported_pattern_holds() -> Bool { + match infer(tree: dag_complement_body_fixture) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn classical_not_int_match_arrow_real_infer_holds() -> Bool { + match infer(tree: classical_not_int_match_arrow_fixture()) { + Accepted { value: _, diagnostics: d } => + diagnostics_contain_reason( + d: d, + reason: ^infer_match_int_scrutinee_bool_literal_scaffold + ) + Rejected { diagnostics: _ } => false + } +} + +fn classical_not_int_match_non_octet_arm_fixture() -> Node { + dag_arrow_with_body_node( + domain: Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: ^dag_binding_param_x }, + target: dag_type_atom_node(identity: ^dag_binding_type_int) + } + ], + occurrence_id: SyntheticOccurrence + }, + return_type_binding: ^dag_binding_type_int, + body: dag_match_body_from_arms( + scrutinee: dag_type_atom_node(identity: ^dag_binding_param_x), + true_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_true, + body_lit: ^dag_pick_lit_one + ), + false_arm: dag_match_arm_node( + pattern_lit: ^dag_token_kw_false, + body_lit: ^dag_token_ident + ) + ) + ) +} + +test fn classical_not_int_match_non_octet_arm_rejects_holds() -> Bool { + match infer(tree: classical_not_int_match_non_octet_arm_fixture()) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn complement_arrow_real_infer_refuses_unsupported_pattern_holds() -> Bool { + match infer(tree: dag_complement_arrow_with_body_fixture) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +data complement_arrow_post_exit_wave1_breadth_note: String = "complement infer refuses because match patterns use dag_complement_lit_* (unsupported by infer_bool_literal_pattern_classify — only dag_token_kw_true/false). Refuse is fail-closed-correct for that unsupported shape. Counted deficit: ground complement_lit on the bool-literal authority (post-exit breadth); target witness is then complement_arrow_real_infer_holds."