From 37ac704bf378982109b8f476a561952ab3b3ca0a Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 16 May 2026 01:28:47 +0200 Subject: [PATCH] iter revert: back out the Iteration-discipline milestone (it.1 + it.2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One forward iteration; main never rewound. 1ff7e81 (the pre-9973546 commit) is the per-region byte oracle — every reverted source/test file is byte-identical to it; crates/ailang-check/src/lib.rs fully so. Root cause being corrected: the Iteration-discipline milestone was an over-escalation of fieldtest finding F1 (a [friction] item whose own minimal recommendation was a DESIGN.md note). Its totality dichotomy made the maximally-LLM-natural build(d:Int)=Node(1,build(d-1), build(d-1)) inexpressible (it.3 BLOCKED); the only in-thesis escape (A1/it.2b) conceded the language's first documented-unenforced totality precondition — a purity-pillar dilution the user rejected in favour of a full revert + rebuild. Removed: Term::Loop/Term::Recur/LoopBinder; the verify_structural_ recursion guardedness pass + term_contains_loop + Diverge-injection + the transitively-it.2 module_fns plumbing; the five Recur*/ NonStructuralRecursion CheckError variants (+ code() + the 3 dedicated ctx() arms); the it.1 codegen loop-header/phi/back-edge + parallel block_terminated setter; all Loop/Recur walker arms; 16 it.1/it.2 fixtures; 2 pin files; bench/it3-oracle/. Restored: 2 RC fixtures to 1ff7e81 content. Surgically kept (not in 1ff7e81, landed with the milestone but independently sound): feature-acceptance clause 3 in DESIGN.md and skills/brainstorm/SKILL.md, with its worked example de-claimed from "shipped" to hypothetical-illustration form; the F3 P2 todo. bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json kept as historical record (like journals/plans). Sole net addition: an honest F1/F4 documented-idiom note in DESIGN.md (the tail-recursive accumulator fallback; examples/mut_counter.ail), guarded by a doc-presence test — "a documentation note is not a reshape", asserts nothing at the typecheck level. Roadmap: the Iteration-discipline block + blocking-fork section removed; the genuine total-Int-recursion ambition preserved as a deferred P2 milestone sequenced behind a future Nat/refinement-types milestone (not abandoned — correctly sequenced after the type machinery it needs). 2026-05-15-iteration-discipline.md carries a superseded header; it.1/it.2/it.3 journals + plans stay as history. Correctness gate PRISTINE: 164 surviving 1ff7e81-era fixtures ail check/ail run byte-identical to pre-milestone behaviour (verified against a 1ff7e81 worktree reference compiler, zero drift); cargo test --workspace 600/0; zero residual it.1/it.2 production surface. Spec docs/specs/2026-05-16-iteration-discipline-revert.md (b3853bf), plan docs/plans/2026-05-16-iter-revert.md (abf0013). --- bench/it3-oracle/MANIFEST.tsv | 41 - bench/it3-oracle/bench_closure_chain.out | 3 - bench/it3-oracle/bench_compute_collatz.out | 3 - bench/it3-oracle/bench_compute_intsum.out | 3 - bench/it3-oracle/bench_hof_pipeline.out | 3 - bench/it3-oracle/bench_latency_explicit.out | 1002 ---------------- bench/it3-oracle/bench_latency_implicit.out | 1002 ---------------- bench/it3-oracle/bench_list_sum.out | 3 - bench/it3-oracle/bench_list_sum_explicit.out | 3 - bench/it3-oracle/bench_mono_dispatch.out | 1 - bench/it3-oracle/bench_tree_walk.out | 3 - bench/it3-oracle/borrow_own_demo.out | 2 - bench/it3-oracle/ct_1_ordering_signum.out | 5 - bench/it3-oracle/escape_local_demo.out | 4 - .../fieldtest_floats_1_newton_sqrt.out | 1 - .../fieldtest_floats_2_average_int_list.out | 1 - .../fieldtest_forma_1_factorial.out | 2 - bench/it3-oracle/gc_stress.out | 1 - bench/it3-oracle/list.out | 1 - bench/it3-oracle/list_map.out | 3 - bench/it3-oracle/list_map_poly.out | 3 - bench/it3-oracle/mut_counter.out | 1 - bench/it3-oracle/mut_sum_floats.out | 1 - bench/it3-oracle/pat_extract_partial_drop.out | 1 - .../rc_drop_iterative_long_list.out | 1 - .../rc_let_alias_implicit_param.out | 1 - bench/it3-oracle/rc_let_owned_app_leak.out | 1 - bench/it3-oracle/rc_list_drop.out | 1 - bench/it3-oracle/rc_pin_recurse_implicit.out | 1 - .../it3-oracle/rc_tail_sum_explicit_leak.out | 1 - bench/it3-oracle/reuse_as_demo.out | 1 - bench/it3-oracle/sort.out | 11 - bench/it3-oracle/std_either_list.out | 1 - bench/it3-oracle/std_list.out | 1 - bench/it3-oracle/std_list_stress.out | 2 - bench/it3-oracle/struct_rec_foldl_sum.out | 1 - bench/it3-oracle/struct_rec_list_len.out | 1 - bench/it3-oracle/struct_rec_sum_e2e.out | 1 - bench/it3-oracle/struct_rec_tree_forest.out | 1 - bench/it3-oracle/sum.out | 1 - .../it3-oracle/test_mono_recursive_fn_bug.out | 1 - .../2026-05-16-iter-revert.json | 34 + crates/ail/src/main.rs | 61 - .../tests/codegen_import_map_fallback_pin.rs | 7 - crates/ail/tests/e2e.rs | 50 - crates/ailang-check/src/builtins.rs | 4 - crates/ailang-check/src/lib.rs | 1057 +---------------- crates/ailang-check/src/lift.rs | 29 +- crates/ailang-check/src/linearity.rs | 24 - crates/ailang-check/src/mono.rs | 30 - .../src/pre_desugar_validation.rs | 12 - crates/ailang-check/src/reuse_shape.rs | 11 - crates/ailang-check/src/uniqueness.rs | 11 - crates/ailang-check/tests/loop_recur_pin.rs | 60 - .../tests/structural_recursion_pin.rs | 129 -- crates/ailang-codegen/src/escape.rs | 40 - crates/ailang-codegen/src/lambda.rs | 28 - crates/ailang-codegen/src/lib.rs | 164 --- crates/ailang-core/specs/form_a.md | 19 - crates/ailang-core/src/ast.rs | 61 - crates/ailang-core/src/desugar.rs | 129 -- crates/ailang-core/src/workspace.rs | 28 - .../ailang-core/tests/carve_out_inventory.rs | 19 +- .../ailang-core/tests/design_schema_drift.rs | 30 +- crates/ailang-core/tests/schema_coverage.rs | 18 - crates/ailang-core/tests/spec_drift.rs | 13 - crates/ailang-prose/src/lib.rs | 121 -- crates/ailang-surface/src/parse.rs | 109 +- crates/ailang-surface/src/print.rs | 48 - docs/DESIGN.md | 64 +- docs/journals/2026-05-16-iter-revert.md | 174 +++ docs/journals/INDEX.md | 1 + docs/roadmap.md | 154 +-- docs/specs/2026-05-15-iteration-discipline.md | 8 + examples/loop_counter.ail | 12 - examples/loop_in_lambda_e2e.ail | 30 - examples/loop_needs_diverge.ail | 18 - examples/loop_nested_in_lambda.ail | 16 - examples/loop_smoke.ail | 11 - examples/rc_let_alias_implicit_param.ail | 10 +- examples/rc_pin_recurse_implicit.ail | 10 +- examples/struct_rec_foldl_sum.ail | 26 - examples/struct_rec_list_len.ail | 24 - examples/struct_rec_sum_e2e.ail | 41 - examples/struct_rec_tree_forest.ail | 43 - examples/test_loop_missing_diverge.ail.json | 1 - examples/test_mutual_cross_family.ail.json | 1 - .../test_non_structural_recursion.ail.json | 1 - examples/test_recur_arity_mismatch.ail.json | 60 - .../test_recur_not_in_tail_position.ail.json | 60 - examples/test_recur_outside_loop.ail.json | 34 - examples/test_recur_type_mismatch.ail.json | 53 - skills/brainstorm/SKILL.md | 2 +- 93 files changed, 307 insertions(+), 5014 deletions(-) delete mode 100644 bench/it3-oracle/MANIFEST.tsv delete mode 100644 bench/it3-oracle/bench_closure_chain.out delete mode 100644 bench/it3-oracle/bench_compute_collatz.out delete mode 100644 bench/it3-oracle/bench_compute_intsum.out delete mode 100644 bench/it3-oracle/bench_hof_pipeline.out delete mode 100644 bench/it3-oracle/bench_latency_explicit.out delete mode 100644 bench/it3-oracle/bench_latency_implicit.out delete mode 100644 bench/it3-oracle/bench_list_sum.out delete mode 100644 bench/it3-oracle/bench_list_sum_explicit.out delete mode 100644 bench/it3-oracle/bench_mono_dispatch.out delete mode 100644 bench/it3-oracle/bench_tree_walk.out delete mode 100644 bench/it3-oracle/borrow_own_demo.out delete mode 100644 bench/it3-oracle/ct_1_ordering_signum.out delete mode 100644 bench/it3-oracle/escape_local_demo.out delete mode 100644 bench/it3-oracle/fieldtest_floats_1_newton_sqrt.out delete mode 100644 bench/it3-oracle/fieldtest_floats_2_average_int_list.out delete mode 100644 bench/it3-oracle/fieldtest_forma_1_factorial.out delete mode 100644 bench/it3-oracle/gc_stress.out delete mode 100644 bench/it3-oracle/list.out delete mode 100644 bench/it3-oracle/list_map.out delete mode 100644 bench/it3-oracle/list_map_poly.out delete mode 100644 bench/it3-oracle/mut_counter.out delete mode 100644 bench/it3-oracle/mut_sum_floats.out delete mode 100644 bench/it3-oracle/pat_extract_partial_drop.out delete mode 100644 bench/it3-oracle/rc_drop_iterative_long_list.out delete mode 100644 bench/it3-oracle/rc_let_alias_implicit_param.out delete mode 100644 bench/it3-oracle/rc_let_owned_app_leak.out delete mode 100644 bench/it3-oracle/rc_list_drop.out delete mode 100644 bench/it3-oracle/rc_pin_recurse_implicit.out delete mode 100644 bench/it3-oracle/rc_tail_sum_explicit_leak.out delete mode 100644 bench/it3-oracle/reuse_as_demo.out delete mode 100644 bench/it3-oracle/sort.out delete mode 100644 bench/it3-oracle/std_either_list.out delete mode 100644 bench/it3-oracle/std_list.out delete mode 100644 bench/it3-oracle/std_list_stress.out delete mode 100644 bench/it3-oracle/struct_rec_foldl_sum.out delete mode 100644 bench/it3-oracle/struct_rec_list_len.out delete mode 100644 bench/it3-oracle/struct_rec_sum_e2e.out delete mode 100644 bench/it3-oracle/struct_rec_tree_forest.out delete mode 100644 bench/it3-oracle/sum.out delete mode 100644 bench/it3-oracle/test_mono_recursive_fn_bug.out create mode 100644 bench/orchestrator-stats/2026-05-16-iter-revert.json delete mode 100644 crates/ailang-check/tests/loop_recur_pin.rs delete mode 100644 crates/ailang-check/tests/structural_recursion_pin.rs create mode 100644 docs/journals/2026-05-16-iter-revert.md delete mode 100644 examples/loop_counter.ail delete mode 100644 examples/loop_in_lambda_e2e.ail delete mode 100644 examples/loop_needs_diverge.ail delete mode 100644 examples/loop_nested_in_lambda.ail delete mode 100644 examples/loop_smoke.ail delete mode 100644 examples/struct_rec_foldl_sum.ail delete mode 100644 examples/struct_rec_list_len.ail delete mode 100644 examples/struct_rec_sum_e2e.ail delete mode 100644 examples/struct_rec_tree_forest.ail delete mode 100644 examples/test_loop_missing_diverge.ail.json delete mode 100644 examples/test_mutual_cross_family.ail.json delete mode 100644 examples/test_non_structural_recursion.ail.json delete mode 100644 examples/test_recur_arity_mismatch.ail.json delete mode 100644 examples/test_recur_not_in_tail_position.ail.json delete mode 100644 examples/test_recur_outside_loop.ail.json delete mode 100644 examples/test_recur_type_mismatch.ail.json diff --git a/bench/it3-oracle/MANIFEST.tsv b/bench/it3-oracle/MANIFEST.tsv deleted file mode 100644 index 59430b4..0000000 --- a/bench/it3-oracle/MANIFEST.tsv +++ /dev/null @@ -1,41 +0,0 @@ -stem class migration runnable rec_fns note -bench_closure_chain a loop main run_loop:loop -bench_compute_collatz a loop main collatz_steps:loop,sum_steps_loop:loop -bench_compute_intsum a loop main intsum_loop:loop -bench_hof_pipeline a plaincall main build_n:structural,fold_with_fn:structural -bench_latency_explicit a BLOCKED main build_tree:BLOCKED,cons_n_acc:structural,sum_list_acc:structural,loop:structural BLOCKED:build_tree -bench_latency_implicit a BLOCKED main build_tree:BLOCKED,sum_tree:structural,cons_n_acc:structural,sum_list_acc:structural,loop:structural BLOCKED:build_tree -bench_list_sum a plaincall main cons_n_acc:structural,sum_acc:structural -bench_list_sum_explicit a plaincall main cons_n_acc:structural,sum_acc:structural -bench_mono_dispatch a plaincall-or-loop ? (self-rec via loop/letrec only) -bench_tree_walk b BLOCKED main build_tree:BLOCKED,sum_tree:structural BLOCKED:build_tree -borrow_own_demo c already-structural main list_length:structural,sum_list:structural -ct_1_ordering_signum a plaincall main drain:structural -escape_local_demo b loop main count:loop -fieldtest/floats_1_newton_sqrt a loop main newton_iter:loop -fieldtest/floats_2_average_int_list a plaincall main sum_acc:structural,count_acc:structural -fieldtest/forma_1_factorial a loop main fact_acc:loop -gc_stress b loop+structural main build:loop,sum_list:structural -list c already-structural main sum_list:structural -list_map c already-structural main map_int:structural,print_list:structural -list_map_poly a plaincall main map:structural,print_list:structural -mut_counter a loop main sum_helper:loop -mut_sum_floats a loop main sum_helper:loop -pat_extract_partial_drop c already-structural main sum_list:structural -rc_drop_iterative_long_list a plaincall main cons_n_acc:structural -rc_let_alias_implicit_param a BLOCKED main build:BLOCKED,loop:structural BLOCKED:build -rc_let_owned_app_leak b BLOCKED main build:BLOCKED BLOCKED:build -rc_list_drop c already-structural main sum_list:structural -rc_pin_recurse_implicit a BLOCKED main build:BLOCKED,loop:structural BLOCKED:build -rc_tail_sum_explicit_leak a plaincall main cons_n_acc:structural,sum_acc:structural -reuse_as_demo c already-structural main map_inc:structural,sum_list:structural -sort a plaincall main insert:structural,sort:structural,print_list:structural -std_either_list c already-structural checkonly lefts:structural,rights:structural,partition_eithers:structural -std_list a plaincall checkonly fold_left:structural,fold_right:structural,append:structural,map:structural,filter:structural,take:structural,drop:structural -std_list_stress b loop main build:loop -struct_rec_foldl_sum c already-structural checkonly go:structural -struct_rec_list_len c already-structural checkonly len:structural -struct_rec_sum_e2e c already-structural main sum:structural -struct_rec_tree_forest c already-structural checkonly forest_size:structural -sum b loop main sum:loop -test_mono_recursive_fn_bug a loop main loop:loop diff --git a/bench/it3-oracle/bench_closure_chain.out b/bench/it3-oracle/bench_closure_chain.out deleted file mode 100644 index 8c703c2..0000000 --- a/bench/it3-oracle/bench_closure_chain.out +++ /dev/null @@ -1,3 +0,0 @@ -49995000 -4999950000 -124999750000 diff --git a/bench/it3-oracle/bench_compute_collatz.out b/bench/it3-oracle/bench_compute_collatz.out deleted file mode 100644 index 4b16396..0000000 --- a/bench/it3-oracle/bench_compute_collatz.out +++ /dev/null @@ -1,3 +0,0 @@ -849666 -10753840 -62134795 diff --git a/bench/it3-oracle/bench_compute_intsum.out b/bench/it3-oracle/bench_compute_intsum.out deleted file mode 100644 index 8b421ab..0000000 --- a/bench/it3-oracle/bench_compute_intsum.out +++ /dev/null @@ -1,3 +0,0 @@ -3500003500000 -350000035000000 -8750000175000000 diff --git a/bench/it3-oracle/bench_hof_pipeline.out b/bench/it3-oracle/bench_hof_pipeline.out deleted file mode 100644 index b235fc9..0000000 --- a/bench/it3-oracle/bench_hof_pipeline.out +++ /dev/null @@ -1,3 +0,0 @@ -5000050000 -500000500000 -4500001500000 diff --git a/bench/it3-oracle/bench_latency_explicit.out b/bench/it3-oracle/bench_latency_explicit.out deleted file mode 100644 index 43e8c74..0000000 --- a/bench/it3-oracle/bench_latency_explicit.out +++ /dev/null @@ -1,1002 +0,0 @@ -8888 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -9999 diff --git a/bench/it3-oracle/bench_latency_implicit.out b/bench/it3-oracle/bench_latency_implicit.out deleted file mode 100644 index 43e8c74..0000000 --- a/bench/it3-oracle/bench_latency_implicit.out +++ /dev/null @@ -1,1002 +0,0 @@ -8888 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -124751 -9999 diff --git a/bench/it3-oracle/bench_list_sum.out b/bench/it3-oracle/bench_list_sum.out deleted file mode 100644 index 2164cfb..0000000 --- a/bench/it3-oracle/bench_list_sum.out +++ /dev/null @@ -1,3 +0,0 @@ -4999950000 -499999500000 -4499998500000 diff --git a/bench/it3-oracle/bench_list_sum_explicit.out b/bench/it3-oracle/bench_list_sum_explicit.out deleted file mode 100644 index 2164cfb..0000000 --- a/bench/it3-oracle/bench_list_sum_explicit.out +++ /dev/null @@ -1,3 +0,0 @@ -4999950000 -499999500000 -4499998500000 diff --git a/bench/it3-oracle/bench_mono_dispatch.out b/bench/it3-oracle/bench_mono_dispatch.out deleted file mode 100644 index 1797677..0000000 --- a/bench/it3-oracle/bench_mono_dispatch.out +++ /dev/null @@ -1 +0,0 @@ --2551317978420243992 diff --git a/bench/it3-oracle/bench_tree_walk.out b/bench/it3-oracle/bench_tree_walk.out deleted file mode 100644 index f38d013..0000000 --- a/bench/it3-oracle/bench_tree_walk.out +++ /dev/null @@ -1,3 +0,0 @@ -65535 -262143 -1048575 diff --git a/bench/it3-oracle/borrow_own_demo.out b/bench/it3-oracle/borrow_own_demo.out deleted file mode 100644 index 2559e5c..0000000 --- a/bench/it3-oracle/borrow_own_demo.out +++ /dev/null @@ -1,2 +0,0 @@ -3 -6 diff --git a/bench/it3-oracle/ct_1_ordering_signum.out b/bench/it3-oracle/ct_1_ordering_signum.out deleted file mode 100644 index 6754c39..0000000 --- a/bench/it3-oracle/ct_1_ordering_signum.out +++ /dev/null @@ -1,5 +0,0 @@ --1 -0 -1 --1 -1 diff --git a/bench/it3-oracle/escape_local_demo.out b/bench/it3-oracle/escape_local_demo.out deleted file mode 100644 index f974c9d..0000000 --- a/bench/it3-oracle/escape_local_demo.out +++ /dev/null @@ -1,4 +0,0 @@ -42 -42 -5 -0 diff --git a/bench/it3-oracle/fieldtest_floats_1_newton_sqrt.out b/bench/it3-oracle/fieldtest_floats_1_newton_sqrt.out deleted file mode 100644 index 26bede6..0000000 --- a/bench/it3-oracle/fieldtest_floats_1_newton_sqrt.out +++ /dev/null @@ -1 +0,0 @@ -1.41421 diff --git a/bench/it3-oracle/fieldtest_floats_2_average_int_list.out b/bench/it3-oracle/fieldtest_floats_2_average_int_list.out deleted file mode 100644 index a3ec5a4..0000000 --- a/bench/it3-oracle/fieldtest_floats_2_average_int_list.out +++ /dev/null @@ -1 +0,0 @@ -3.2 diff --git a/bench/it3-oracle/fieldtest_forma_1_factorial.out b/bench/it3-oracle/fieldtest_forma_1_factorial.out deleted file mode 100644 index b205837..0000000 --- a/bench/it3-oracle/fieldtest_forma_1_factorial.out +++ /dev/null @@ -1,2 +0,0 @@ -120 -3628800 diff --git a/bench/it3-oracle/gc_stress.out b/bench/it3-oracle/gc_stress.out deleted file mode 100644 index 9c113c6..0000000 --- a/bench/it3-oracle/gc_stress.out +++ /dev/null @@ -1 +0,0 @@ -1275 diff --git a/bench/it3-oracle/list.out b/bench/it3-oracle/list.out deleted file mode 100644 index d81cc07..0000000 --- a/bench/it3-oracle/list.out +++ /dev/null @@ -1 +0,0 @@ -42 diff --git a/bench/it3-oracle/list_map.out b/bench/it3-oracle/list_map.out deleted file mode 100644 index e2ba1ef..0000000 --- a/bench/it3-oracle/list_map.out +++ /dev/null @@ -1,3 +0,0 @@ -2 -4 -6 diff --git a/bench/it3-oracle/list_map_poly.out b/bench/it3-oracle/list_map_poly.out deleted file mode 100644 index dcf37cd..0000000 --- a/bench/it3-oracle/list_map_poly.out +++ /dev/null @@ -1,3 +0,0 @@ -2 -3 -4 diff --git a/bench/it3-oracle/mut_counter.out b/bench/it3-oracle/mut_counter.out deleted file mode 100644 index c3f407c..0000000 --- a/bench/it3-oracle/mut_counter.out +++ /dev/null @@ -1 +0,0 @@ -55 diff --git a/bench/it3-oracle/mut_sum_floats.out b/bench/it3-oracle/mut_sum_floats.out deleted file mode 100644 index c3f407c..0000000 --- a/bench/it3-oracle/mut_sum_floats.out +++ /dev/null @@ -1 +0,0 @@ -55 diff --git a/bench/it3-oracle/pat_extract_partial_drop.out b/bench/it3-oracle/pat_extract_partial_drop.out deleted file mode 100644 index 1e8b314..0000000 --- a/bench/it3-oracle/pat_extract_partial_drop.out +++ /dev/null @@ -1 +0,0 @@ -6 diff --git a/bench/it3-oracle/rc_drop_iterative_long_list.out b/bench/it3-oracle/rc_drop_iterative_long_list.out deleted file mode 100644 index d00491f..0000000 --- a/bench/it3-oracle/rc_drop_iterative_long_list.out +++ /dev/null @@ -1 +0,0 @@ -1 diff --git a/bench/it3-oracle/rc_let_alias_implicit_param.out b/bench/it3-oracle/rc_let_alias_implicit_param.out deleted file mode 100644 index 573541a..0000000 --- a/bench/it3-oracle/rc_let_alias_implicit_param.out +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/bench/it3-oracle/rc_let_owned_app_leak.out b/bench/it3-oracle/rc_let_owned_app_leak.out deleted file mode 100644 index d00491f..0000000 --- a/bench/it3-oracle/rc_let_owned_app_leak.out +++ /dev/null @@ -1 +0,0 @@ -1 diff --git a/bench/it3-oracle/rc_list_drop.out b/bench/it3-oracle/rc_list_drop.out deleted file mode 100644 index 60d3b2f..0000000 --- a/bench/it3-oracle/rc_list_drop.out +++ /dev/null @@ -1 +0,0 @@ -15 diff --git a/bench/it3-oracle/rc_pin_recurse_implicit.out b/bench/it3-oracle/rc_pin_recurse_implicit.out deleted file mode 100644 index 573541a..0000000 --- a/bench/it3-oracle/rc_pin_recurse_implicit.out +++ /dev/null @@ -1 +0,0 @@ -0 diff --git a/bench/it3-oracle/rc_tail_sum_explicit_leak.out b/bench/it3-oracle/rc_tail_sum_explicit_leak.out deleted file mode 100644 index d567f8a..0000000 --- a/bench/it3-oracle/rc_tail_sum_explicit_leak.out +++ /dev/null @@ -1 +0,0 @@ -4950 diff --git a/bench/it3-oracle/reuse_as_demo.out b/bench/it3-oracle/reuse_as_demo.out deleted file mode 100644 index ec63514..0000000 --- a/bench/it3-oracle/reuse_as_demo.out +++ /dev/null @@ -1 +0,0 @@ -9 diff --git a/bench/it3-oracle/sort.out b/bench/it3-oracle/sort.out deleted file mode 100644 index aa02339..0000000 --- a/bench/it3-oracle/sort.out +++ /dev/null @@ -1,11 +0,0 @@ -1 -1 -2 -3 -3 -4 -5 -5 -5 -6 -9 diff --git a/bench/it3-oracle/std_either_list.out b/bench/it3-oracle/std_either_list.out deleted file mode 100644 index db1816e..0000000 --- a/bench/it3-oracle/std_either_list.out +++ /dev/null @@ -1 +0,0 @@ -ok (53 symbols across 6 modules) diff --git a/bench/it3-oracle/std_list.out b/bench/it3-oracle/std_list.out deleted file mode 100644 index cda4759..0000000 --- a/bench/it3-oracle/std_list.out +++ /dev/null @@ -1 +0,0 @@ -ok (38 symbols across 3 modules) diff --git a/bench/it3-oracle/std_list_stress.out b/bench/it3-oracle/std_list_stress.out deleted file mode 100644 index e3bfce7..0000000 --- a/bench/it3-oracle/std_list_stress.out +++ /dev/null @@ -1,2 +0,0 @@ -500500 -500500 diff --git a/bench/it3-oracle/struct_rec_foldl_sum.out b/bench/it3-oracle/struct_rec_foldl_sum.out deleted file mode 100644 index d549e72..0000000 --- a/bench/it3-oracle/struct_rec_foldl_sum.out +++ /dev/null @@ -1 +0,0 @@ -ok (22 symbols across 2 modules) diff --git a/bench/it3-oracle/struct_rec_list_len.out b/bench/it3-oracle/struct_rec_list_len.out deleted file mode 100644 index d549e72..0000000 --- a/bench/it3-oracle/struct_rec_list_len.out +++ /dev/null @@ -1 +0,0 @@ -ok (22 symbols across 2 modules) diff --git a/bench/it3-oracle/struct_rec_sum_e2e.out b/bench/it3-oracle/struct_rec_sum_e2e.out deleted file mode 100644 index 60d3b2f..0000000 --- a/bench/it3-oracle/struct_rec_sum_e2e.out +++ /dev/null @@ -1 +0,0 @@ -15 diff --git a/bench/it3-oracle/struct_rec_tree_forest.out b/bench/it3-oracle/struct_rec_tree_forest.out deleted file mode 100644 index 37df063..0000000 --- a/bench/it3-oracle/struct_rec_tree_forest.out +++ /dev/null @@ -1 +0,0 @@ -ok (24 symbols across 2 modules) diff --git a/bench/it3-oracle/sum.out b/bench/it3-oracle/sum.out deleted file mode 100644 index c3f407c..0000000 --- a/bench/it3-oracle/sum.out +++ /dev/null @@ -1 +0,0 @@ -55 diff --git a/bench/it3-oracle/test_mono_recursive_fn_bug.out b/bench/it3-oracle/test_mono_recursive_fn_bug.out deleted file mode 100644 index 60d3b2f..0000000 --- a/bench/it3-oracle/test_mono_recursive_fn_bug.out +++ /dev/null @@ -1 +0,0 @@ -15 diff --git a/bench/orchestrator-stats/2026-05-16-iter-revert.json b/bench/orchestrator-stats/2026-05-16-iter-revert.json new file mode 100644 index 0000000..ecc2253 --- /dev/null +++ b/bench/orchestrator-stats/2026-05-16-iter-revert.json @@ -0,0 +1,34 @@ +{ + "iter_id": "revert", + "date": "2026-05-16", + "mode": "standard", + "outcome": "DONE", + "tasks_total": 11, + "tasks_completed": 11, + "reloops_per_task": { + "1": 0, + "2": 0, + "3": 0, + "4": 0, + "5": 0, + "6": 0, + "7": 0, + "8": 0, + "9": 0, + "10": 0, + "11": 0 + }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null, + "notes": { + "self_caught_implementer_corrections": 1, + "self_caught_detail": "Task 4: a scripted line-range delete also removed verify_tail_positions' match/fn closing braces; caught by the disciplined full-file oracle diff in the implementer phase and fixed forward within the same task (not a spec/quality re-loop).", + "stop_gates_cleared": ["task3-step1-helper-provenance", "task8-step1-fixture-split"], + "concerns": 2, + "concern_detail": "Task 3 plan file-map under-enumerated the module_fns signature threading (resolved via oracle authority, no bounce); Task 9 Step-6 single-line grep heuristic returned 0 due to verbatim-text line-wrap (substantive clause-3 retention positively verified otherwise).", + "behavioural_equivalence": "164 surviving fixtures, fail=0, zero check/run drift vs 1ff7e81 — pristine", + "workspace_tests": "600 passed, 0 failed", + "main_head_moved": false + } +} diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs index b125878..8b9788b 100644 --- a/crates/ail/src/main.rs +++ b/crates/ail/src/main.rs @@ -1544,26 +1544,6 @@ fn walk_term( } walk_term(value, out, builtins, scope); } - // Iter it.1: loop binder names bind inside the body and later - // binder inits, mirroring `Term::Mut`. Recur args are uses. - Term::Loop { binders, body } => { - let mut newly = Vec::new(); - for b in binders { - walk_term(&b.init, out, builtins, scope); - if scope.insert(b.name.clone()) { - newly.push(b.name.clone()); - } - } - walk_term(body, out, builtins, scope); - for n in newly { - scope.remove(&n); - } - } - Term::Recur { args } => { - for a in args { - walk_term(a, out, builtins, scope); - } - } } } @@ -2805,47 +2785,6 @@ fn rewrite_def( changed, ); } - // Iter it.1: rewrite types embedded in each - // `LoopBinder.ty` (loop binders carry full Type - // annotations like mut-vars) and recurse into each - // binder's `init` and the body. `Term::Recur` has no - // embedded type. - Term::Loop { binders, body } => { - for b in binders { - rewrite_type( - &mut b.ty, - owning_module, - local_types, - import_names, - changed, - ); - rewrite_term( - &mut b.init, - owning_module, - local_types, - import_names, - changed, - ); - } - rewrite_term( - body, - owning_module, - local_types, - import_names, - changed, - ); - } - Term::Recur { args } => { - for a in args { - rewrite_term( - a, - owning_module, - local_types, - import_names, - changed, - ); - } - } } } diff --git a/crates/ail/tests/codegen_import_map_fallback_pin.rs b/crates/ail/tests/codegen_import_map_fallback_pin.rs index 702a162..44b4296 100644 --- a/crates/ail/tests/codegen_import_map_fallback_pin.rs +++ b/crates/ail/tests/codegen_import_map_fallback_pin.rs @@ -101,13 +101,6 @@ fn synthesised_print_uses_user_module_show_via_fallback() { || contains_xmod_show_var(body) } Term::Assign { value, .. } => contains_xmod_show_var(value), - // Iter it.1: a `Term::Loop` cannot itself host a synth'd - // cross-module reference, but recurse defensively. - Term::Loop { binders, body } => { - binders.iter().any(|b| contains_xmod_show_var(&b.init)) - || contains_xmod_show_var(body) - } - Term::Recur { args } => args.iter().any(contains_xmod_show_var), Term::Lit { .. } => false, } } diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index 024980e..9950cb6 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -2828,56 +2828,6 @@ fn mut_counter_prints_55() { assert_eq!(stdout.trim(), "55", "mut_counter must print 55, got {stdout:?}"); } -/// Iter it.1: `examples/loop_counter.ail` exercises `Term::Loop` + -/// `Term::Recur` codegen — the loop-header block with one phi per -/// binder and `recur` as a back-edge `br`. The body -/// `(loop ((var acc Int 0) (var i Int 1)) (if (> i 10) acc (recur ...)))` -/// sums 1..10 and prints 55. End-to-end gate for the loop-header / -/// phi / recur-back-edge lowering. -#[test] -fn loop_counter_runs_and_prints_55() { - let stdout = build_and_run("loop_counter.ail"); - assert_eq!(stdout.trim(), "55", "loop_counter must print 55, got {stdout:?}"); -} - -/// Iter it.1: a `Term::Loop` inside a `Term::Lam` body, invoked via -/// a returned closure. Protects the lambda-boundary invariant: the -/// closure thunk scopes its own loop header / phis (the `loop_frames` -/// save+reset+restore across the lambda boundary, mut.3 analogue) — -/// a `recur` inside the lambda must back-edge to the lambda's own -/// loop header, not the outer fn's. The lambda computes x*x by -/// summing x exactly x times; apply 7 prints 49. -#[test] -fn loop_in_lambda_runs_and_prints_49() { - let stdout = build_and_run("loop_in_lambda_e2e.ail"); - assert_eq!(stdout.trim(), "49", "loop_in_lambda must print 49, got {stdout:?}"); -} - -/// Iter it.2 Phase-3: an it.2-clean structural recursion that runs. -/// `struct_rec_sum_e2e` sums [1,2,3,4,5] via plain non-tail -/// recursion on the Cons tail — the it.2 guardedness check -/// classifies it pure + total (no `!Diverge`, no `tail-app`). This -/// gate proves the structural-recursion "total" verdict is -/// behaviourally sound, not merely a typecheck assertion: a plain -/// (musttail-free) structurally-decreasing recursive call lowers -/// and runs to the correct value. -#[test] -fn struct_rec_sum_runs_and_prints_15() { - let stdout = build_and_run("struct_rec_sum_e2e.ail"); - assert_eq!(stdout.trim(), "15", "struct_rec_sum must print 15, got {stdout:?}"); -} - -/// Iter it.2 Phase-3: the `Diverge`-path twin. `loop_needs_diverge` -/// declares `!Diverge` (loop-bearing per DD-4) and runs the it.1 -/// accumulator loop to 55 — proving the Diverge-effect injection is -/// purely a typecheck-layer obligation with no codegen impact (the -/// loop lowers and runs identically to its pre-it.2 it.1 form). -#[test] -fn loop_needs_diverge_runs_and_prints_55() { - let stdout = build_and_run("loop_needs_diverge.ail"); - assert_eq!(stdout.trim(), "55", "loop_needs_diverge must print 55, got {stdout:?}"); -} - /// Iter mut.3: Float twin of `mut_counter_prints_55`. The mut-var /// is `Float`, init is `0.0`, the recursive helper returns the /// sum 1.0+...+10.0 = 55.0. The polymorphic `print` routes through diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs index d4f5d92..fbd7b1b 100644 --- a/crates/ailang-check/src/builtins.rs +++ b/crates/ailang-check/src/builtins.rs @@ -343,7 +343,6 @@ mod tests { install(&mut env); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -355,7 +354,6 @@ mod tests { &env, &mut locals, &mut mut_scope_stack, - &mut loop_stack, &mut effects, "", &mut subst, @@ -588,7 +586,6 @@ mod tests { install(&mut env); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -600,7 +597,6 @@ mod tests { &env, &mut locals, &mut mut_scope_stack, - &mut loop_stack, &mut effects, "", &mut subst, diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 24531e9..7061b06 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -35,7 +35,7 @@ use ailang_core::ast::*; use ailang_core::Workspace; use indexmap::IndexMap; -use std::collections::{BTreeMap, BTreeSet, HashSet}; +use std::collections::{BTreeMap, BTreeSet}; mod linearity; mod pre_desugar_validation; @@ -261,23 +261,6 @@ pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap Term::Loop { - binders: binders - .iter() - .map(|b| ailang_core::ast::LoopBinder { - name: b.name.clone(), - ty: substitute_rigids(&b.ty, mapping), - init: Box::new(substitute_rigids_in_term(&b.init, mapping)), - }) - .collect(), - body: Box::new(substitute_rigids_in_term(body, mapping)), - }, - Term::Recur { args } => Term::Recur { - args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(), - }, } } @@ -696,46 +679,6 @@ pub enum CheckError { #[error("mut-var `{name}` cannot be captured by a lambda — mut-vars are alloca-resident and do not escape their enclosing mut block. Either move the lambda outside the mut block, or restructure to pass `{name}` as a lambda parameter (deferring escape to a future milestone with ref-types and the !Mut effect).")] MutVarCapturedByLambda { name: String }, - /// Iter it.1: a `Term::Recur` was reached with no lexically - /// enclosing `Term::Loop`. Spec - /// `docs/specs/2026-05-15-iteration-discipline.md`. (No `span` - /// field — the `CheckError` variants in this crate do not carry - /// spans; the plan's pseudo-code referenced a type not in scope - /// here, so the real `MutAssignOutOfScope`-style shape is used.) - #[error("recur outside of any enclosing loop")] - RecurOutsideLoop, - - /// Iter it.1: a `Term::Recur`'s argument count differs from the - /// lexically nearest enclosing loop's binder count. - #[error("recur passes {got} argument(s) but the enclosing loop binds {want}")] - RecurArityMismatch { got: usize, want: usize }, - - /// Iter it.1: a `Term::Recur` argument's synth type does not - /// unify with the corresponding loop binder's declared type. - #[error("recur argument {pos} has type {got} but loop binder `{name}` is {want}")] - RecurTypeMismatch { - pos: usize, - name: String, - got: String, - want: String, - }, - - /// Iter it.1: a `Term::Recur` was reached outside the tail - /// context of its enclosing loop's body. Spec - /// `docs/specs/2026-05-15-iteration-discipline.md`. - #[error("recur must be in tail position of its enclosing loop")] - RecurNotInTailPosition, - - /// Iter it.2: a recursive call (self or mutual-group) passes a - /// non-structurally-smaller argument at every candidate structural - /// position. The author must express this iteration as an explicit - /// `(loop …)` / `recur` instead. Spec - /// `docs/specs/2026-05-15-iteration-discipline.md` (D1/D2). Display - /// body is bracket-`[code]`-free per the F2 convention — the CLI - /// formatter prepends the `[code]`. - #[error("recursive call to `{callee}` is not on a structurally-smaller argument (`{arg}`); express this iteration as `(loop …)` / `recur`")] - NonStructuralRecursion { callee: String, arg: String }, - /// Iter 22b.3: an internal invariant in the typechecker / mono pass /// was violated — surfaced as an error so callers can propagate /// rather than abort, but in well-formed inputs (typecheck has @@ -788,11 +731,6 @@ impl CheckError { CheckError::AssignTypeMismatch { .. } => "assign-type-mismatch", CheckError::UnsupportedMutVarType { .. } => "mut-var-unsupported-type", CheckError::MutVarCapturedByLambda { .. } => "mut-var-captured-by-lambda", - CheckError::RecurOutsideLoop => "recur-outside-loop", - CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch", - CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch", - CheckError::RecurNotInTailPosition => "recur-not-in-tail-position", - CheckError::NonStructuralRecursion { .. } => "non-structural-recursion", CheckError::Internal(_) => "internal", } } @@ -867,15 +805,6 @@ impl CheckError { CheckError::MutVarCapturedByLambda { name } => { serde_json::json!({"name": name}) } - CheckError::RecurArityMismatch { got, want } => { - serde_json::json!({"expected": want, "actual": got}) - } - CheckError::RecurTypeMismatch { pos, name, got, want } => { - serde_json::json!({"pos": pos, "name": name, "expected": want, "actual": got}) - } - CheckError::NonStructuralRecursion { callee, arg } => { - serde_json::json!({ "callee": callee, "arg": arg }) - } _ => serde_json::Value::Object(serde_json::Map::new()), } } @@ -1718,20 +1647,8 @@ fn check_in_workspace( env.imports = import_map; env.current_module = m.name.clone(); - // Iter it.2 (DD-3): the module's `Def::Fn`s, for the - // mutual-structural-group analysis. A single owned Vec built once - // per module; `verify_structural_recursion` reads it to decide - // whether a cross-call is to a same-group member. - let module_fns: Vec<&FnDef> = m - .defs - .iter() - .filter_map(|d| match d { - Def::Fn(f) => Some(f), - _ => None, - }) - .collect(); for def in &m.defs { - match check_def(def, &env, &module_fns, out_warnings) { + match check_def(def, &env, out_warnings) { Ok(()) => {} Err(e) => { errors.push(CheckError::Def(def.name().to_string(), Box::new(e))); @@ -1749,11 +1666,10 @@ fn check_in_workspace( fn check_def( def: &Def, env: &Env, - module_fns: &[&FnDef], out_warnings: &mut Vec, ) -> Result<()> { match def { - Def::Fn(f) => check_fn(f, env, module_fns, out_warnings), + Def::Fn(f) => check_fn(f, env, out_warnings), Def::Const(c) => check_const(c, env, out_warnings), Def::Type(td) => check_type_def(td, env), // bugfix-instance-body-unbound-var (2026-05-13): each instance @@ -1852,10 +1768,7 @@ fn check_instance( doc: None, suppress: Vec::new(), }; - // Iter it.2: a synthetic instance-method fn is not a - // module-level def and does not participate in the - // mutual-structural-group analysis; pass no siblings. - check_fn(&synthetic, env, &[], out_warnings)?; + check_fn(&synthetic, env, out_warnings)?; } Ok(()) } @@ -1948,12 +1861,7 @@ fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> { } } -fn check_fn( - f: &FnDef, - env: &Env, - module_fns: &[&FnDef], - out_warnings: &mut Vec, -) -> Result<()> { +fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec) -> Result<()> { // Peel an outer Forall (Iter 12a). The vars become rigid in the // inner env so they pass `check_type_well_formed` and unify only // with themselves. An empty `vars` list (vacuously polymorphic) @@ -2042,8 +1950,7 @@ fn check_fn( // pushed/popped by `Term::Mut` arms during the walk; discarded after // the body type-checks. let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); - let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?; + let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?; unify(&ret_ty, &body_ty, &mut subst)?; // mq.3: surface synth-time warnings into the caller-supplied // accumulator. The warnings already carry `def: Some(f.name)` @@ -2055,29 +1962,6 @@ fn check_fn( // call doesn't drown out the underlying type error. verify_tail_positions(&f.body, true)?; - // Iter it.2 (DD-1): structural-recursion guardedness. Sibling of - // `verify_tail_positions`; runs on the whole post-synth body so - // it can build the `smaller`-set provenance before judging any - // recursive call. Out of scope for synthetic Forall-peeled types - // — it reads `f.ty` directly via `adt_param_positions`. - verify_structural_recursion(f, &env, module_fns)?; - - // Iter it.2 (DD-4 / D2): the first real `Diverge` effect. A fn - // whose body syntactically contains a `Term::Loop` raises - // `Diverge`, exactly as a `do print` raises `IO`. The "calls a - // `Diverge`-declaring callee" half needs no code here — a - // callee's `Type::Fn.effects` already flows into `effects` - // during synth (identically to `IO`). The existing - // declared-vs-raised reconciliation below turns an undeclared - // `Diverge` into the existing `UndeclaredEffect` — no new - // diagnostic variant. Structural recursion injects nothing (it - // contains no `Term::Loop`). The lam boundary is honoured by - // `term_contains_loop` (a loop under a `Term::Lam` is that lam's - // arrow effect, reconciled at the lam sub-effect site). - if term_contains_loop(&f.body) { - effects.insert("Diverge".to_string()); - } - let declared: BTreeSet = declared_effs.into_iter().collect(); for e in &effects { if !declared.contains(e) { @@ -2795,763 +2679,6 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> { // be in tail position. Its `value` is also not in tail // position. Term::Assign { value, .. } => verify_tail_positions(value, false), - // Iter it.1 (DD-1): binder inits are evaluated before the - // loop head and are NOT in tail position. The body opens a - // "recur-legal, recur-must-be-tail" context — `verify_loop_body` - // walks it, accepting a `Term::Recur` only where the loop - // body's value is produced (tail position w.r.t. the loop). - Term::Loop { binders, body } => { - for b in binders { - verify_tail_positions(&b.init, false)?; - } - verify_loop_body(body) - } - // Iter it.1 (DD-1): a `Term::Recur` reached by the ordinary - // `verify_tail_positions` walk is, by construction, NOT in the - // tail context of any enclosing loop body (`verify_loop_body` - // intercepts the legal in-tail ones). Either there is no - // enclosing loop (synth flags `RecurOutsideLoop`) or this - // recur is in a non-tail position. - Term::Recur { .. } => Err(CheckError::RecurNotInTailPosition), - } -} - -/// Iter it.1 (DD-1): walks a `Term::Loop` body in the -/// "recur-is-legal-and-must-be-tail" context. A `Term::Recur` is -/// accepted only at a position that produces the loop body's value -/// (the loop-tail positions); anywhere else it is -/// `RecurNotInTailPosition`. Non-recur sub-terms that are NOT in the -/// loop's tail position are handed back to `verify_tail_positions` -/// (with `is_tail = false`) so `tail-app`/`tail-do` inside the loop -/// body are still validated; sub-terms in the loop's tail position -/// recurse through `verify_loop_body` so a nested `recur` there is -/// still legal. A nested `Term::Loop` starts its own recur scope. -fn verify_loop_body(t: &Term) -> Result<()> { - match t { - // Tail position of the loop body: a recur here is legal. - Term::Recur { args } => { - for a in args { - verify_tail_positions(a, false)?; - } - Ok(()) - } - Term::If { cond, then, else_ } => { - verify_tail_positions(cond, false)?; - verify_loop_body(then)?; - verify_loop_body(else_) - } - Term::Seq { lhs, rhs } => { - // Only `rhs` is in the loop's tail position. - verify_tail_positions(lhs, false)?; - verify_loop_body(rhs) - } - Term::Match { scrutinee, arms } => { - verify_tail_positions(scrutinee, false)?; - for arm in arms { - verify_loop_body(&arm.body)?; - } - Ok(()) - } - Term::Let { value, body, .. } => { - verify_tail_positions(value, false)?; - verify_loop_body(body) - } - // A nested loop is its own recur scope: a `recur` inside it - // binds the inner loop, not this one. Validate it through the - // ordinary tail-position walk in a fresh tail context. - Term::Loop { .. } => verify_tail_positions(t, true), - // Any other term is not a recur-carrying tail shape; validate - // it normally (it is the loop body's value but carries no - // loop-tail recur, so `is_tail = true` keeps a trailing - // `tail-app` legal). - other => verify_tail_positions(other, true), - } -} - -/// Iter it.2 (DD-4): true iff `t` syntactically contains a -/// `Term::Loop`, **not** descending into `Term::Lam` bodies. A -/// lambda is a value with its own arrow effect row — a loop inside -/// it executes on closure call, not here, so it carries `Diverge` -/// on the lam's arrow type (handled at the lam sub-effect reconcile -/// site), not on the enclosing fn. This mirrors exactly how `!IO` -/// inside a lam does not leak to the enclosing fn. -fn term_contains_loop(t: &Term) -> bool { - match t { - Term::Loop { .. } => true, - Term::Lam { .. } => false, - Term::Lit { .. } | Term::Var { .. } => false, - Term::Recur { args } => args.iter().any(term_contains_loop), - Term::App { callee, args, .. } => { - term_contains_loop(callee) || args.iter().any(term_contains_loop) - } - Term::Do { args, .. } => args.iter().any(term_contains_loop), - Term::Let { value, body, .. } => { - term_contains_loop(value) || term_contains_loop(body) - } - Term::LetRec { body, in_term, .. } => { - term_contains_loop(body) || term_contains_loop(in_term) - } - Term::If { cond, then, else_ } => { - term_contains_loop(cond) - || term_contains_loop(then) - || term_contains_loop(else_) - } - Term::Seq { lhs, rhs } => { - term_contains_loop(lhs) || term_contains_loop(rhs) - } - Term::Match { scrutinee, arms } => { - term_contains_loop(scrutinee) - || arms.iter().any(|a| term_contains_loop(&a.body)) - } - Term::Ctor { args, .. } => args.iter().any(term_contains_loop), - Term::Clone { value } => term_contains_loop(value), - Term::ReuseAs { source, body } => { - term_contains_loop(source) || term_contains_loop(body) - } - Term::Mut { vars, body } => { - vars.iter().any(|v| term_contains_loop(&v.init)) - || term_contains_loop(body) - } - Term::Assign { value, .. } => term_contains_loop(value), - } -} - -// ── Iter it.2: structural-recursion guardedness (DD-1/DD-2/DD-3) ── -// -// A recursive call (self, or to a same-ADT-family mutual-group -// member) must pass a structurally-smaller argument at some -// inferable parameter position. Accumulator positions are -// unconstrained (spec D1). it.2-only grandfather: a `tail:true` -// recursive call is not collected at all, so it never causes -// rejection (the 21 `tail-app` corpus fixtures stay clean through -// it.2; it.3 removes the `tail` field and this exemption together). - -/// One collected recursive call: the callee name, its argument -/// terms, and the `smaller` set live at the call site. `tail:true` -/// recursive calls are never collected (the grandfather). -struct RecCall { - callee: String, - args: Vec, - smaller: HashSet, -} - -/// Resolve a declared type to its ADT `type`-decl name, if it is a -/// non-primitive `Type::Con` that names a `type` decl reachable from -/// `env` (bare or one-dot-qualified). `Type::Fn`, `Type::Var`, -/// `Type::Forall`, and primitive cons return `None`. -fn adt_type_head(t: &Type, env: &Env) -> Option { - let Type::Con { name, .. } = t else { - return None; - }; - if ailang_core::primitives::is_primitive_name(name) { - return None; - } - if name.matches('.').count() == 1 { - let (prefix, suffix) = name.split_once('.').expect("checked"); - let target = env.imports.get(prefix)?; - if env - .module_types - .get(target) - .and_then(|tys| tys.get(suffix)) - .is_some() - { - return Some(name.clone()); - } - None - } else if env.types.contains_key(name) { - Some(name.clone()) - } else { - None - } -} - -/// Candidate structural parameter positions of `f`: indices whose -/// declared type is a non-primitive ADT `Type::Con` (DD-2). -fn adt_param_positions(f: &FnDef, env: &Env) -> Vec { - let inner = match &f.ty { - Type::Forall { body, .. } => (**body).clone(), - other => other.clone(), - }; - let Type::Fn { params, .. } = inner else { - return Vec::new(); - }; - params - .iter() - .enumerate() - .filter_map(|(i, p)| adt_type_head(p, env).map(|_| i)) - .collect() -} - -/// The constructor-bound field names of a flat post-desugar -/// pattern. `Pattern::Ctor` fields are `Var`/`Wild` (nested ctor -/// patterns were rejected upstream by `NestedCtorPatternNotAllowed`). -fn ctor_bound_names(p: &Pattern) -> Vec { - match p { - Pattern::Ctor { fields, .. } => fields - .iter() - .filter_map(|f| match f { - Pattern::Var { name } => Some(name.clone()), - _ => None, - }) - .collect(), - _ => Vec::new(), - } -} - -/// True iff `name` is the recursion name `f` calls itself by, or a -/// same-group mutual member (filled in Task 3 via `group`). -fn is_rec_callee(name: &str, rec_name: &str, group: &HashSet) -> bool { - name == rec_name || group.contains(name) -} - -/// Single `smaller`-threaded walk. Collects every non-`tail` -/// recursive call together with the `smaller` set in effect at that -/// syntactic position. `param_smaller_seed` is the set of parameter -/// names that are *themselves* candidate structural roots — a -/// `match` on one of them (or on an already-smaller var) extends -/// `smaller` with that arm's constructor-bound fields. `recur` / -/// `loop` bodies are walked (a `recur` is not a recursive *call*); -/// `Term::Lam` is NOT descended into (DD-3/DD-4 lam boundary). -#[allow(clippy::too_many_arguments)] -fn collect_rec_calls_walk( - t: &Term, - rec_name: &str, - group: &HashSet, - param_roots: &HashSet, - smaller: &HashSet, - out: &mut Vec, -) { - match t { - Term::Lit { .. } | Term::Var { .. } => {} - Term::App { callee, args, tail } => { - if !*tail { - if let Term::Var { name } = &**callee { - if is_rec_callee(name, rec_name, group) { - out.push(RecCall { - callee: name.clone(), - args: args.clone(), - smaller: smaller.clone(), - }); - } - } - } - collect_rec_calls_walk(callee, rec_name, group, param_roots, smaller, out); - for a in args { - collect_rec_calls_walk(a, rec_name, group, param_roots, smaller, out); - } - } - Term::Do { args, .. } => { - for a in args { - collect_rec_calls_walk(a, rec_name, group, param_roots, smaller, out); - } - } - Term::Let { name, value, body } => { - collect_rec_calls_walk(value, rec_name, group, param_roots, smaller, out); - // Alias propagation: `let v = ` where the bound term - // is a structural root (or already strictly smaller) - // makes `v` carry the same status in `body`. This is what - // makes the desugar-introduced `let $mp_N = ` - // (Iter 16a nested-pattern flattening) transparent to the - // guardedness walk — without it every nested-ctor-pattern - // recursion would be a false `NonStructuralRecursion`. - if let Term::Var { name: src } = &**value { - if smaller.contains(src) { - let mut s = smaller.clone(); - s.insert(name.clone()); - collect_rec_calls_walk(body, rec_name, group, param_roots, &s, out); - return; - } - if param_roots.contains(src) { - let mut r = param_roots.clone(); - r.insert(name.clone()); - collect_rec_calls_walk(body, rec_name, group, &r, smaller, out); - return; - } - } - collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out); - } - Term::LetRec { body, in_term, .. } => { - collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out); - collect_rec_calls_walk(in_term, rec_name, group, param_roots, smaller, out); - } - Term::If { cond, then, else_ } => { - collect_rec_calls_walk(cond, rec_name, group, param_roots, smaller, out); - collect_rec_calls_walk(then, rec_name, group, param_roots, smaller, out); - collect_rec_calls_walk(else_, rec_name, group, param_roots, smaller, out); - } - Term::Seq { lhs, rhs } => { - collect_rec_calls_walk(lhs, rec_name, group, param_roots, smaller, out); - collect_rec_calls_walk(rhs, rec_name, group, param_roots, smaller, out); - } - Term::Match { scrutinee, arms } => { - collect_rec_calls_walk(scrutinee, rec_name, group, param_roots, smaller, out); - // A match on a structural root (or an already-smaller var) - // makes that arm's constructor-bound fields strictly - // smaller. Other scrutinees do not extend `smaller`. - let extends = match &**scrutinee { - Term::Var { name } => param_roots.contains(name) || smaller.contains(name), - _ => false, - }; - for arm in arms { - if extends { - let mut s = smaller.clone(); - for n in ctor_bound_names(&arm.pat) { - s.insert(n); - } - collect_rec_calls_walk(&arm.body, rec_name, group, param_roots, &s, out); - } else { - collect_rec_calls_walk(&arm.body, rec_name, group, param_roots, smaller, out); - } - } - } - Term::Ctor { args, .. } => { - for a in args { - collect_rec_calls_walk(a, rec_name, group, param_roots, smaller, out); - } - } - // DD-3/DD-4: a lambda body is a separate def's territory; do - // not descend (consistent with the Diverge lam boundary). - Term::Lam { .. } => {} - Term::Clone { value } => { - collect_rec_calls_walk(value, rec_name, group, param_roots, smaller, out); - } - Term::ReuseAs { source, body } => { - collect_rec_calls_walk(source, rec_name, group, param_roots, smaller, out); - collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out); - } - Term::Mut { vars, body } => { - for v in vars { - collect_rec_calls_walk(&v.init, rec_name, group, param_roots, smaller, out); - } - collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out); - } - Term::Assign { value, .. } => { - collect_rec_calls_walk(value, rec_name, group, param_roots, smaller, out); - } - Term::Loop { binders, body } => { - for b in binders { - collect_rec_calls_walk(&b.init, rec_name, group, param_roots, smaller, out); - } - collect_rec_calls_walk(body, rec_name, group, param_roots, smaller, out); - } - Term::Recur { args } => { - for a in args { - collect_rec_calls_walk(a, rec_name, group, param_roots, smaller, out); - } - } - } -} - -/// Whether the recursive call `c` is structurally guarded at the -/// candidate position `i`: its `i`-th argument is a bare -/// `Term::Var` whose name is in the `smaller` set at the call site. -fn call_guarded_at(c: &RecCall, i: usize) -> bool { - match c.args.get(i) { - Some(Term::Var { name }) => c.smaller.contains(name), - _ => false, - } -} - -/// Display form of a recursive call's offending argument (the arg -/// at the first candidate position, else the first arg), for the -/// diagnostic. Mirrors the short pretty form the it.1 `Recur*` -/// diagnostics use. -fn rec_call_arg_display(c: &RecCall, cand: &[usize]) -> String { - let idx = cand.first().copied().unwrap_or(0); - match c.args.get(idx).or_else(|| c.args.first()) { - Some(Term::Var { name }) => name.clone(), - Some(Term::Ctor { ctor, .. }) => format!("{ctor}(…)"), - Some(Term::App { callee, .. }) => format!("{}(…)", callee_name(callee)), - Some(Term::Lit { .. }) => "".to_string(), - Some(_) => "".to_string(), - None => "".to_string(), - } -} - -/// DD-1/DD-2/DD-3: structural-recursion guardedness for a single -/// `FnDef`. A recursive call (self, or — Task 3 — a same-family -/// mutual-group member) must be structurally guarded at some -/// parameter position that is structural at *every* such call. -fn verify_structural_recursion( - f: &FnDef, - env: &Env, - module_fns: &[&FnDef], -) -> Result<()> { - let cand = adt_param_positions(f, env); - let group = mutual_structural_group(f, module_fns, env); - - // it.2 transitional boundary: a def with no ADT candidate - // position and no mutual cycle has no *structural* parameter to - // verify. Its recursion is integer-counter / other-shaped - // (`f(n) = … f(n - 1) …`) — genuinely non-structural, but its - // migration to `(loop …)` is the destructive it.3 corpus pass, - // not it.2's job. it.2 only rejects *misuse of an ADT structural - // position* (the spec's load-bearing case: the canonical - // `f(xs) = … f(xs) …` negative still fires because it HAS an ADT - // candidate). This keeps the corpus clean through it.2 without - // weakening the ADT structural check — the `tail==false` - // grandfather alone is insufficient because corpus fixtures like - // `build_tree(depth: Int)` recurse non-tail on a primitive arg. - // Recorded as a resolved spec/it.2-boundary clarification in the - // iter journal. - if cand.is_empty() && group.members.is_empty() { - return Ok(()); - } - - let param_roots: HashSet = cand - .iter() - .filter_map(|&i| f.params.get(i).cloned()) - .collect(); - - let mut calls: Vec = Vec::new(); - collect_rec_calls_walk( - &f.body, - &f.name, - &group.members, - ¶m_roots, - &HashSet::new(), - &mut calls, - ); - if calls.is_empty() { - return Ok(()); - } - - // Per-call guardedness verdict: - // - self-call (`callee == f.name`): guarded iff some candidate - // position of `f` receives a structurally-smaller arg. - // - cross-call into a mutual-cycle member: only meaningful if the - // cycle is a valid same-family group (`family_valid`); then - // guarded iff some candidate position of the *callee* receives - // a var in the caller's `smaller` set (DD-3). A cross-call into - // a family-INVALID cycle is unconditionally unguarded — the - // cross-family negative. - let guarded = |c: &RecCall| -> bool { - if c.callee == f.name { - cand.iter().any(|&i| call_guarded_at(c, i)) - } else if !group.family_valid { - false - } else { - module_fns - .iter() - .find(|g| g.name == c.callee) - .map(|g| adt_param_positions(g, env)) - .map(|gc| gc.iter().any(|&i| call_guarded_at(c, i))) - .unwrap_or(false) - } - }; - - // Structural iff there is a single candidate position of `f` - // structural at *every* self-call (the implicit-inference rule, - // DD-2) AND every cross-call into the mutual cycle is guarded. - let self_calls: Vec<&RecCall> = calls.iter().filter(|c| c.callee == f.name).collect(); - let self_clear = self_calls.is_empty() - || cand - .iter() - .any(|&i| self_calls.iter().all(|c| call_guarded_at(c, i))); - let cross_clear = calls - .iter() - .filter(|c| c.callee != f.name) - .all(guarded); - - if self_clear && cross_clear { - return Ok(()); - } - - // Not structural — emit on the first unguarded recursive call - // (all collected calls are already non-`tail`; the `tail:true` - // grandfather filtered them out at collection time). - let offending = calls.iter().find(|c| !guarded(c)).unwrap_or(&calls[0]); - Err(CheckError::NonStructuralRecursion { - callee: offending.callee.clone(), - arg: rec_call_arg_display(offending, &cand), - }) -} - -/// Tiny `BTreeMap`-backed union-find over type names (DD-3). No -/// external dependency; path-halving find, union-by-insertion. -struct TypeUnionFind { - parent: BTreeMap, -} - -impl TypeUnionFind { - fn new() -> Self { - TypeUnionFind { parent: BTreeMap::new() } - } - fn ensure(&mut self, x: &str) { - if !self.parent.contains_key(x) { - self.parent.insert(x.to_string(), x.to_string()); - } - } - fn find(&mut self, x: &str) -> String { - self.ensure(x); - let mut cur = x.to_string(); - while self.parent[&cur] != cur { - let grand = self.parent[&self.parent[&cur]].clone(); - self.parent.insert(cur.clone(), grand.clone()); - cur = self.parent[&cur].clone(); - } - cur - } - fn union(&mut self, a: &str, b: &str) { - let ra = self.find(a); - let rb = self.find(b); - if ra != rb { - self.parent.insert(ra, rb); - } - } - fn same(&mut self, a: &str, b: &str) -> bool { - self.find(a) == self.find(b) - } -} - -/// Collect the `Type::Con` head names referenced anywhere inside a -/// type (recursing through `Fn`/`Forall`/`Con` args), skipping -/// primitives and type vars. -fn referenced_con_names(t: &Type, out: &mut Vec) { - match t { - Type::Con { name, args } => { - if !ailang_core::primitives::is_primitive_name(name) { - out.push(name.clone()); - } - for a in args { - referenced_con_names(a, out); - } - } - Type::Fn { params, ret, .. } => { - for p in params { - referenced_con_names(p, out); - } - referenced_con_names(ret, out); - } - Type::Forall { body, .. } => referenced_con_names(body, out), - Type::Var { .. } => {} - } -} - -/// DD-3: connected components of the ADT type-reference graph. -/// Nodes are every visible `type` decl name; an undirected edge -/// joins `T` and any non-primitive `Con` head appearing in one of -/// `T`'s constructor field types. The result answers -/// "are these two ADT heads in one family?". -fn adt_families(env: &Env) -> TypeUnionFind { - let mut uf = TypeUnionFind::new(); - // All visible TypeDefs: the current module's plus every module's - // (workspace-flat). Bare names index the current module; that is - // the resolution `adt_type_head` already uses for fixtures. - let mut all: Vec<(&String, &TypeDef)> = env.types.iter().collect(); - for tys in env.module_types.values() { - all.extend(tys.iter()); - } - for (name, td) in &all { - uf.ensure(name); - for ctor in &td.ctors { - for field in &ctor.fields { - let mut refs = Vec::new(); - referenced_con_names(field, &mut refs); - for r in refs { - // Edge only between ADT decls (a referenced name - // that is not a known type decl, e.g. a builtin - // wrapper, contributes no family edge). - uf.union(name, &r); - } - } - } - } - uf -} - -/// DD-3: the mutual-recursion cycle `f` belongs to — the set of -/// *other* module fn names that `f` reaches and that reach `f` -/// through direct `Term::App` → `Term::Var` recursion (the -/// back-reaching connected component of the call graph restricted -/// to `module_fns`), plus whether that cycle is a valid same-ADT- -/// family structural group. Empty `members` ⇒ -/// `verify_structural_recursion` treats `f` as self-recursive only. -/// Non-empty `members` with `family_valid = false` ⇒ the cycle -/// spans unrelated ADT families: each cross-call is an unguarded -/// recursive call (the cross-family negative). -fn mutual_structural_group( - f: &FnDef, - module_fns: &[&FnDef], - env: &Env, -) -> MutualGroup { - // Direct-call adjacency among module fns (callee names that are - // module fns; ignore builtins / cross-module). - let names: HashSet<&str> = module_fns.iter().map(|g| g.name.as_str()).collect(); - let direct_callees = |g: &FnDef| -> HashSet { - let mut cs = Vec::new(); - collect_direct_app_var_callees(&g.body, &mut cs); - cs.into_iter().filter(|c| names.contains(c.as_str())).collect() - }; - - // Connected component of `f` in the (undirected) call graph. - let by_name: BTreeMap<&str, &FnDef> = - module_fns.iter().map(|g| (g.name.as_str(), *g)).collect(); - let mut adj: BTreeMap> = BTreeMap::new(); - for g in module_fns { - let cs = direct_callees(g); - for c in &cs { - adj.entry(g.name.clone()).or_default().insert(c.clone()); - adj.entry(c.clone()).or_default().insert(g.name.clone()); - } - } - let mut comp: HashSet = HashSet::new(); - let mut stack = vec![f.name.clone()]; - while let Some(n) = stack.pop() { - if !comp.insert(n.clone()) { - continue; - } - if let Some(neigh) = adj.get(&n) { - for m in neigh { - if !comp.contains(m) { - stack.push(m.clone()); - } - } - } - } - comp.remove(&f.name); - // Members that genuinely participate in a recursive cycle with - // `f`: keep only those that (transitively) call back to `f`. - // For the corpus shapes (tree/forest, even/odd) the component is - // already the mutual cycle; a one-way helper call would not put - // the helper into a back-reaching cycle, so it drops out here. - let reaches = |start: &str, target: &str| -> bool { - let mut seen: HashSet = HashSet::new(); - let mut st = vec![start.to_string()]; - while let Some(n) = st.pop() { - if n == target && n != start { - return true; - } - if !seen.insert(n.clone()) { - continue; - } - if let Some(g) = by_name.get(n.as_str()) { - for c in direct_callees(g) { - if c == target { - return true; - } - st.push(c); - } - } - } - false - }; - let members: HashSet = comp - .into_iter() - .filter(|m| reaches(&f.name, m) && reaches(m, &f.name)) - .collect(); - if members.is_empty() { - return MutualGroup { members, family_valid: true }; - } - - // DD-3 family test: `f` and every cycle member must have a - // structural ADT parameter, and all those parameter type heads - // must be in ONE family component. If not, the cycle is not a - // valid mutual structural group — `family_valid = false` makes - // every cross-call into it an unguarded recursive call (the - // cross-family negative). - let mut uf = adt_families(env); - let head_of = |g: &FnDef| -> Option { - let inner = match &g.ty { - Type::Forall { body, .. } => (**body).clone(), - other => other.clone(), - }; - let Type::Fn { params, .. } = inner else { return None }; - params.iter().find_map(|p| adt_type_head(p, env)) - }; - let family_valid = match head_of(f) { - None => false, - Some(f_head) => members.iter().all(|m| { - by_name - .get(m.as_str()) - .and_then(|mg| head_of(mg)) - .map(|h| uf.same(&f_head, &h)) - .unwrap_or(false) - }), - }; - MutualGroup { members, family_valid } -} - -/// DD-3: the mutual-recursion cycle `f` participates in, and -/// whether that cycle is a valid same-ADT-family structural group. -/// `members` is family-agnostic (used to collect cross-calls); a -/// cross-call into a `members` fn is judged structurally only when -/// `family_valid` holds, otherwise it is an unguarded recursive -/// call. -struct MutualGroup { - members: HashSet, - family_valid: bool, -} - -/// Direct `Term::App` whose callee is a `Term::Var` — the callee -/// names reachable by direct application (no descent into `Lam` -/// bodies, consistent with the guardedness walk's lam boundary). -fn collect_direct_app_var_callees(t: &Term, out: &mut Vec) { - match t { - Term::Lit { .. } | Term::Var { .. } | Term::Recur { .. } => {} - Term::App { callee, args, .. } => { - if let Term::Var { name } = &**callee { - out.push(name.clone()); - } - collect_direct_app_var_callees(callee, out); - for a in args { - collect_direct_app_var_callees(a, out); - } - } - Term::Do { args, .. } => { - for a in args { - collect_direct_app_var_callees(a, out); - } - } - Term::Let { value, body, .. } => { - collect_direct_app_var_callees(value, out); - collect_direct_app_var_callees(body, out); - } - Term::LetRec { body, in_term, .. } => { - collect_direct_app_var_callees(body, out); - collect_direct_app_var_callees(in_term, out); - } - Term::If { cond, then, else_ } => { - collect_direct_app_var_callees(cond, out); - collect_direct_app_var_callees(then, out); - collect_direct_app_var_callees(else_, out); - } - Term::Seq { lhs, rhs } => { - collect_direct_app_var_callees(lhs, out); - collect_direct_app_var_callees(rhs, out); - } - Term::Match { scrutinee, arms } => { - collect_direct_app_var_callees(scrutinee, out); - for arm in arms { - collect_direct_app_var_callees(&arm.body, out); - } - } - Term::Ctor { args, .. } => { - for a in args { - collect_direct_app_var_callees(a, out); - } - } - // Lam boundary (DD-3/DD-4): a closure body is a separate - // def's territory; do not descend. - Term::Lam { .. } => {} - Term::Clone { value } => collect_direct_app_var_callees(value, out), - Term::ReuseAs { source, body } => { - collect_direct_app_var_callees(source, out); - collect_direct_app_var_callees(body, out); - } - Term::Mut { vars, body } => { - for v in vars { - collect_direct_app_var_callees(&v.init, out); - } - collect_direct_app_var_callees(body, out); - } - Term::Assign { value, .. } => collect_direct_app_var_callees(value, out), - Term::Loop { binders, body } => { - for b in binders { - collect_direct_app_var_callees(&b.init, out); - } - collect_direct_app_var_callees(body, out); - } } } @@ -3576,8 +2703,7 @@ fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec) -> R // at this entry point — `Term::Mut` may appear inside a const body // and push frames as the walk descends). let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); - let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?; + let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?; out_warnings.extend(warnings); unify(&c.ty, &v, &mut subst)?; if !effects.is_empty() { @@ -3602,14 +2728,6 @@ pub(crate) fn synth( // name through it. Position: locals-adjacent because both are // per-fn-body lexical scope state. mut_scope_stack: &mut Vec>, - // Iter it.1 (DD-1): per-walk lexical loop-binder-type stack, - // threaded exactly as `mut_scope_stack`. Each frame is one - // `Term::Loop`'s binder type-vector (positional). Pushed on - // `Term::Loop` entry, popped on exit; `Term::Recur` reads the - // innermost frame for arity/type unification. Position: - // mut_scope_stack-adjacent because both are per-fn-body lexical - // scope state. - loop_stack: &mut Vec>, effects: &mut BTreeSet, in_def: &str, subst: &mut Subst, @@ -3998,7 +3116,7 @@ pub(crate) fn synth( Ok(maybe_instantiate(raw, counter)) } Term::App { callee, args, .. } => { - let cty = synth(callee, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let cty = synth(callee, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let cty = subst.apply(&cty); let (params, ret, fx) = match &cty { Type::Fn { params, ret, effects: fx, .. } => { @@ -4034,7 +3152,7 @@ pub(crate) fn synth( }); } for (a, exp) in args.iter().zip(params.iter()) { - let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; unify(exp, &actual, subst)?; } for e in fx { @@ -4043,9 +3161,9 @@ pub(crate) fn synth( Ok(subst.apply(&ret)) } Term::Let { name, value, body } => { - let v = synth(value, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let v = synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; let prev = locals.insert(name.clone(), v); - let r = synth(body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let r = synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; match prev { Some(p) => { locals.insert(name.clone(), p); @@ -4057,10 +3175,10 @@ pub(crate) fn synth( Ok(r) } Term::If { cond, then, else_ } => { - let c = synth(cond, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let c = synth(cond, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; unify(&Type::bool_(), &c, subst)?; - let t1 = synth(then, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; - let t2 = synth(else_, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let t1 = synth(then, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let t2 = synth(else_, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; unify(&t1, &t2, subst)?; Ok(subst.apply(&t1)) } @@ -4078,7 +3196,7 @@ pub(crate) fn synth( }); } for (a, exp) in args.iter().zip(sig.params.iter()) { - let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; unify(exp, &actual, subst)?; } effects.insert(sig.effect.clone()); @@ -4173,7 +3291,7 @@ pub(crate) fn synth( } for (a, exp) in args.iter().zip(qualified_fields.iter()) { let exp_inst = substitute_rigids(exp, &mapping); - let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; unify(&exp_inst, &actual, subst)?; } Ok(Type::Con { @@ -4182,7 +3300,7 @@ pub(crate) fn synth( }) } Term::Match { scrutinee, arms } => { - let s_ty = synth(scrutinee, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let s_ty = synth(scrutinee, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; if arms.is_empty() { return Err(CheckError::NonExhaustive { ty: ailang_core::pretty::type_to_string(&s_ty), @@ -4200,7 +3318,7 @@ pub(crate) fn synth( let prev = locals.insert(n.clone(), t.clone()); pushed.push((n.clone(), prev)); } - let body_ty = synth(&arm.body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let body_ty = synth(&arm.body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; for (n, prev) in pushed.into_iter().rev() { match prev { Some(p) => { @@ -4275,9 +3393,9 @@ pub(crate) fn synth( Ok(subst.apply(&result_ty.expect("checked arms is non-empty"))) } Term::Seq { lhs, rhs } => { - let lty = synth(lhs, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let lty = synth(lhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; unify(&Type::unit(), <y, subst)?; - synth(rhs, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) + synth(rhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) } Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => { // Iter mut.4-tidy: reject lambda-captures-of-mut-var. @@ -4311,7 +3429,7 @@ pub(crate) fn synth( pushed.push((n.clone(), prev)); } let mut body_effects: BTreeSet = BTreeSet::new(); - let body_ty = synth(body, env, locals, mut_scope_stack, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings); + let body_ty = synth(body, env, locals, mut_scope_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings); for (n, prev) in pushed.into_iter().rev() { match prev { Some(p) => { @@ -4324,16 +3442,6 @@ pub(crate) fn synth( } let body_ty = body_ty?; unify(ret_ty, &body_ty, subst)?; - // Iter it.2 (DD-4): a `(loop …)` directly in this lam's - // body makes the lam's arrow carry `Diverge` — coherent - // with how `!IO` scopes across the lam edge. A loop under - // a *further-nested* lam is that inner lam's concern; - // `term_contains_loop`'s own `Term::Lam => false` stops - // there. Reconciled against the lam's declared arrow - // effects exactly like every other raised effect. - if term_contains_loop(body) { - body_effects.insert("Diverge".to_string()); - } let declared: BTreeSet = lam_effects.iter().cloned().collect(); for e in &body_effects { if !declared.contains(e) { @@ -4409,7 +3517,7 @@ pub(crate) fn synth( // subset rule against `declared_effs` — exactly like // `Term::Lam`. let mut body_effects: BTreeSet = BTreeSet::new(); - let body_ty = synth(body, env, locals, mut_scope_stack, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings); + let body_ty = synth(body, env, locals, mut_scope_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings); // Restore body-scope locals (params + name). for (n, prev) in pushed.into_iter().rev() { @@ -4425,13 +3533,6 @@ pub(crate) fn synth( let body_ty = body_ty?; unify(&ret_ty, &body_ty, subst)?; - // Iter it.2 (DD-4): a `Term::LetRec` clause is a - // fn-equivalent (same as `check_fn` / `Term::Lam`); a - // `(loop …)` in its body makes its arrow carry `Diverge`. - // Same lam-boundary rule via `term_contains_loop`. - if term_contains_loop(body) { - body_effects.insert("Diverge".to_string()); - } let declared: BTreeSet = declared_effs.into_iter().collect(); for e in &body_effects { if !declared.contains(e) { @@ -4443,7 +3544,7 @@ pub(crate) fn synth( // scope (params are not visible here; only the recursive // binding is). let prev_in = locals.insert(name.clone(), ty.clone()); - let in_ty = synth(in_term, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings); + let in_ty = synth(in_term, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings); match prev_in { Some(p) => { locals.insert(name.clone(), p); @@ -4459,7 +3560,7 @@ pub(crate) fn synth( // No constraint generated, no environment change. The // wrapper records author intent for the future RC inc/dec // emission pass (18c.3); typing is pure passthrough. - synth(value, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) + synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) } Term::ReuseAs { source, body } => { // Iter 18d.1: `(reuse-as SRC NEW-CTOR)` requires `body` to @@ -4473,7 +3574,7 @@ pub(crate) fn synth( // shape-compatibility check (18d.2 will add a // `reuse-as-shape-mismatch` diagnostic when codegen has // the actual size info). - let _ = synth(source, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; + let _ = synth(source, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?; match body.as_ref() { Term::Ctor { .. } | Term::Lam { .. } => {} other => { @@ -4491,8 +3592,6 @@ pub(crate) fn synth( Term::ReuseAs { .. } => "reuse-as", Term::Mut { .. } => "mut", Term::Assign { .. } => "assign", - Term::Loop { .. } => "loop", - Term::Recur { .. } => "recur", Term::Ctor { .. } | Term::Lam { .. } => unreachable!(), }; return Err(CheckError::ReuseAsNonAllocatingBody { @@ -4503,7 +3602,7 @@ pub(crate) fn synth( } // Body's type is the result type of the whole reuse-as // expression. - synth(body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) + synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings) } // Iter mut.2: a mut block opens a fresh lexical scope for its // mut-vars. Each var's `init` is synthed in the outer scope @@ -4529,7 +3628,7 @@ pub(crate) fn synth( // the `mut_scope_stack` truthful at all times. mut_scope_stack.push(frame.clone()); let init_ty = synth( - &v.init, env, locals, mut_scope_stack, loop_stack, effects, in_def, + &v.init, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, )?; mut_scope_stack.pop(); @@ -4538,7 +3637,7 @@ pub(crate) fn synth( } mut_scope_stack.push(frame); let body_result = synth( - body, env, locals, mut_scope_stack, loop_stack, effects, in_def, + body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, ); mut_scope_stack.pop(); @@ -4572,7 +3671,7 @@ pub(crate) fn synth( } Some(declared_ty) => { let value_ty = synth( - value, env, locals, mut_scope_stack, loop_stack, effects, in_def, + value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings, )?; let applied_declared = subst.apply(&declared_ty); @@ -4588,84 +3687,6 @@ pub(crate) fn synth( } } } - // Iter it.1 (DD-1): each binder's `init` is synthesised in - // the outer scope plus the already-declared binders (init - // order = declaration order), unified against the binder's - // declared type. The binder names are bound into `locals` - // (save/restore like `Term::Let`) for the body; the binder - // type-vector is pushed onto `loop_stack` so an enclosed - // `Term::Recur` can check its arity/types. The loop's static - // type is the body's static type. - Term::Loop { binders, body } => { - let mut saved: Vec<(String, Option)> = Vec::new(); - let mut binder_tys: Vec = Vec::with_capacity(binders.len()); - for b in binders { - let init_ty = synth( - &b.init, env, locals, mut_scope_stack, loop_stack, effects, in_def, - subst, counter, residuals, free_fn_calls, warnings, - )?; - unify(&b.ty, &init_ty, subst)?; - let prev = locals.insert(b.name.clone(), b.ty.clone()); - saved.push((b.name.clone(), prev)); - binder_tys.push(b.ty.clone()); - } - loop_stack.push(binder_tys); - let body_result = synth( - body, env, locals, mut_scope_stack, loop_stack, effects, in_def, - subst, counter, residuals, free_fn_calls, warnings, - ); - loop_stack.pop(); - for (name, prev) in saved.into_iter().rev() { - match prev { - Some(p) => { - locals.insert(name, p); - } - None => { - locals.shift_remove(&name); - } - } - } - body_result - } - // Iter it.1 (DD-1): a `Term::Recur` re-enters the lexically - // nearest enclosing loop. Empty `loop_stack` ⇒ - // `RecurOutsideLoop`; arg count ≠ innermost binder count ⇒ - // `RecurArityMismatch`; per-position unify failure ⇒ - // `RecurTypeMismatch`. `recur` never falls through (it is - // always a tail jump), so its synth result is a fresh - // metavar — it unifies with any type, which is what makes - // `(if c then (recur ...))` typecheck. (The plan's named - // fallback was `Type::unit()`; a fresh metavar is the - // codebase-idiomatic bottom and resolves the plan's "Open - // risk" correctly — see the it.1 journal.) - Term::Recur { args } => { - let want = loop_stack - .last() - .cloned() - .ok_or(CheckError::RecurOutsideLoop)?; - if args.len() != want.len() { - return Err(CheckError::RecurArityMismatch { - got: args.len(), - want: want.len(), - }); - } - for (i, (a, wt)) in args.iter().zip(want.iter()).enumerate() { - let at = synth( - a, env, locals, mut_scope_stack, loop_stack, effects, in_def, - subst, counter, residuals, free_fn_calls, warnings, - )?; - if unify(&at, wt, subst).is_err() { - let applied_got = subst.apply(&at); - return Err(CheckError::RecurTypeMismatch { - pos: i, - name: format!("#{i}"), - got: ailang_core::pretty::type_to_string(&applied_got), - want: ailang_core::pretty::type_to_string(wt), - }); - } - } - Ok(Subst::fresh(counter)) - } } } @@ -5040,7 +4061,6 @@ mod tests { let env = Env::default(); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -5052,7 +4072,6 @@ mod tests { &env, &mut locals, &mut mut_scope_stack, - &mut loop_stack, &mut effects, "", &mut subst, @@ -5079,7 +4098,6 @@ mod tests { let mut locals: IndexMap = IndexMap::new(); locals.insert("x".into(), Type::int()); // outer let-style binding let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut frame: IndexMap = IndexMap::new(); frame.insert("x".into(), Type::float()); // inner mut-var mut_scope_stack.push(frame); @@ -5096,7 +4114,6 @@ mod tests { &env, &mut locals, &mut mut_scope_stack, - &mut loop_stack, &mut effects, "", &mut subst, @@ -5121,7 +4138,6 @@ mod tests { let env = Env::default(); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut outer: IndexMap = IndexMap::new(); outer.insert("x".into(), Type::int()); mut_scope_stack.push(outer); @@ -5141,7 +4157,6 @@ mod tests { &env, &mut locals, &mut mut_scope_stack, - &mut loop_stack, &mut effects, "", &mut subst, @@ -5236,7 +4251,6 @@ mod tests { let env = Env::default(); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -5244,7 +4258,7 @@ mod tests { let mut free_fn_calls: Vec = Vec::new(); let mut warnings: Vec = Vec::new(); let err = synth( - &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, + &term, &env, &mut locals, &mut mut_scope_stack, &mut effects, "", &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings, ) @@ -5277,7 +4291,6 @@ mod tests { let env = Env::default(); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -5285,7 +4298,7 @@ mod tests { let mut free_fn_calls: Vec = Vec::new(); let mut warnings: Vec = Vec::new(); let err = synth( - &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, + &term, &env, &mut locals, &mut mut_scope_stack, &mut effects, "", &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings, ) @@ -5317,7 +4330,6 @@ mod tests { let env = Env::default(); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -5325,7 +4337,7 @@ mod tests { let mut free_fn_calls: Vec = Vec::new(); let mut warnings: Vec = Vec::new(); let err = synth( - &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, + &term, &env, &mut locals, &mut mut_scope_stack, &mut effects, "", &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings, ) @@ -5420,7 +4432,6 @@ mod tests { let env = Env::default(); let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -5428,7 +4439,7 @@ mod tests { let mut free_fn_calls: Vec = Vec::new(); let mut warnings: Vec = Vec::new(); let err = synth( - &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, + &term, &env, &mut locals, &mut mut_scope_stack, &mut effects, "", &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings, ) @@ -8160,7 +7171,6 @@ mod tests { let term = Term::Var { name: "show".into() }; let mut locals: IndexMap = IndexMap::new(); let mut mut_scope_stack: Vec> = Vec::new(); - let mut loop_stack: Vec> = Vec::new(); let mut effects: BTreeSet = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; @@ -8172,7 +7182,6 @@ mod tests { &env, &mut locals, &mut mut_scope_stack, - &mut loop_stack, &mut effects, "test_call_site", &mut subst, diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs index a4ae3fe..ea56344 100644 --- a/crates/ailang-check/src/lift.rs +++ b/crates/ailang-check/src/lift.rs @@ -397,25 +397,6 @@ impl<'a> Lifter<'a> { name: name.clone(), value: Box::new(self.lift_in_term(value, locals, in_def)?), }), - Term::Loop { binders, body } => Ok(Term::Loop { - binders: binders - .iter() - .map(|b| { - Ok(ailang_core::ast::LoopBinder { - name: b.name.clone(), - ty: b.ty.clone(), - init: Box::new(self.lift_in_term(&b.init, locals, in_def)?), - }) - }) - .collect::>>()?, - body: Box::new(self.lift_in_term(body, locals, in_def)?), - }), - Term::Recur { args } => Ok(Term::Recur { - args: args - .iter() - .map(|a| self.lift_in_term(a, locals, in_def)) - .collect::>>()?, - }), Term::LetRec { name, ty, params, body, in_term } => { // Iter 16b.3: post-order traversal — lift any inner // LetRecs first. Within the body's scope, `name` and @@ -743,11 +724,7 @@ impl<'a> Lifter<'a> { // term at a time, beginning from a top-of-body position; fresh // empty mut-scope stack is correct. let mut mut_scope_stack: Vec> = Vec::new(); - // Iter it.1 (DD-1): lift's letrec-capture re-entry walks one - // term from a top-of-body position; fresh empty loop_stack is - // correct (a loop captured into a letrec carries its own). - let mut loop_stack: Vec> = Vec::new(); - let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?; + let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?; Ok(subst.apply(&ty)) } } @@ -784,10 +761,6 @@ fn contains_any_letrec(m: &Module) -> bool { vars.iter().any(|v| term_has_letrec(&v.init)) || term_has_letrec(body) } Term::Assign { value, .. } => term_has_letrec(value), - Term::Loop { binders, body } => { - binders.iter().any(|b| term_has_letrec(&b.init)) || term_has_letrec(body) - } - Term::Recur { args } => args.iter().any(term_has_letrec), } } for def in &m.defs { diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index 6867f45..83f9b66 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -609,17 +609,6 @@ impl<'a> Checker<'a> { // a tracked binder). Walk the `value` normally. self.walk(value, Position::Consume); } - Term::Loop { binders, body } => { - for b in binders { - self.walk(&b.init, Position::Consume); - } - self.walk(body, pos); - } - Term::Recur { args } => { - for a in args { - self.walk(a, Position::Consume); - } - } } } @@ -806,8 +795,6 @@ fn make_reuse_as_source_not_bare_var(def: &str, source: &Term, body: &Term) -> D Term::ReuseAs { .. } => "reuse-as", Term::Mut { .. } => "mut", Term::Assign { .. } => "assign", - Term::Loop { .. } => "loop", - Term::Recur { .. } => "recur", }; let replacement = term_to_form_a(body); Diagnostic::error( @@ -947,17 +934,6 @@ fn any_sub_binder_consumed_for( Term::Assign { value, .. } => { any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors) } - // Iter it.1: loop binders are scalar like mut-vars; recurse - // into children defensively so a genuine consume-of-`pname` - // inside a binder init / body / recur arg still surfaces. - Term::Loop { binders, body } => { - binders.iter().any(|b| { - any_sub_binder_consumed_for(&b.init, pname, uniq, def_name, ctors) - }) || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors) - } - Term::Recur { args } => args - .iter() - .any(|a| any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)), } } diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs index 83584e1..64b5f27 100644 --- a/crates/ailang-check/src/mono.rs +++ b/crates/ailang-check/src/mono.rs @@ -713,16 +713,11 @@ pub fn collect_mono_targets( // mut-scope, since any `Term::Mut` will push its own frame as the // walk descends. let mut mut_scope_stack: Vec> = Vec::new(); - // Iter it.1 (DD-1): mono re-synth from top-of-body — empty - // loop_stack; any `Term::Loop` pushes its own frame as the walk - // descends. - let mut loop_stack: Vec> = Vec::new(); crate::synth( &f.body, &env, &mut locals, &mut mut_scope_stack, - &mut loop_stack, &mut effects, &f.name, &mut subst, @@ -1244,17 +1239,6 @@ fn rewrite_mono_calls( Term::Assign { value, .. } => { rewrite_mono_calls(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals); } - Term::Loop { binders, body } => { - for b in binders.iter_mut() { - rewrite_mono_calls(&mut b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals); - } - rewrite_mono_calls(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals); - } - Term::Recur { args } => { - for a in args.iter_mut() { - rewrite_mono_calls(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals); - } - } Term::Lit { .. } => {} } } @@ -1359,14 +1343,11 @@ pub(crate) fn collect_residuals_ordered( // mut-scope, since any `Term::Mut` will push its own frame as the // walk descends. let mut mut_scope_stack: Vec> = Vec::new(); - // Iter it.1 (DD-1): empty loop_stack at top-of-body re-synth. - let mut loop_stack: Vec> = Vec::new(); crate::synth( &f.body, &env, &mut locals, &mut mut_scope_stack, - &mut loop_stack, &mut effects, &f.name, &mut subst, @@ -1632,17 +1613,6 @@ fn interleave_slots( Term::Assign { value, .. } => { interleave_slots(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out); } - Term::Loop { binders, body } => { - for b in binders { - interleave_slots(&b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out); - } - interleave_slots(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out); - } - Term::Recur { args } => { - for a in args { - interleave_slots(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out); - } - } Term::Lit { .. } => {} } } diff --git a/crates/ailang-check/src/pre_desugar_validation.rs b/crates/ailang-check/src/pre_desugar_validation.rs index d43cd12..c0bcda6 100644 --- a/crates/ailang-check/src/pre_desugar_validation.rs +++ b/crates/ailang-check/src/pre_desugar_validation.rs @@ -133,18 +133,6 @@ fn walk_term(t: &Term) -> Result<(), CheckError> { walk_term(body) } Term::Assign { value, .. } => walk_term(value), - Term::Loop { binders, body } => { - for b in binders { - walk_term(&b.init)?; - } - walk_term(body) - } - Term::Recur { args } => { - for a in args { - walk_term(a)?; - } - Ok(()) - } } } diff --git a/crates/ailang-check/src/reuse_shape.rs b/crates/ailang-check/src/reuse_shape.rs index 7fb7d3c..72f37cc 100644 --- a/crates/ailang-check/src/reuse_shape.rs +++ b/crates/ailang-check/src/reuse_shape.rs @@ -265,17 +265,6 @@ impl<'a> Checker<'a> { self.walk(body); } Term::Assign { value, .. } => self.walk(value), - Term::Loop { binders, body } => { - for b in binders { - self.walk(&b.init); - } - self.walk(body); - } - Term::Recur { args } => { - for a in args { - self.walk(a); - } - } } } diff --git a/crates/ailang-check/src/uniqueness.rs b/crates/ailang-check/src/uniqueness.rs index 42dc739..d102d48 100644 --- a/crates/ailang-check/src/uniqueness.rs +++ b/crates/ailang-check/src/uniqueness.rs @@ -352,17 +352,6 @@ impl<'a> Walker<'a> { Term::Assign { value, .. } => { self.walk(value, Position::Consume); } - Term::Loop { binders, body } => { - for b in binders { - self.walk(&b.init, Position::Consume); - } - self.walk(body, pos); - } - Term::Recur { args } => { - for a in args { - self.walk(a, Position::Consume); - } - } } } diff --git a/crates/ailang-check/tests/loop_recur_pin.rs b/crates/ailang-check/tests/loop_recur_pin.rs deleted file mode 100644 index 7c2dba9..0000000 --- a/crates/ailang-check/tests/loop_recur_pin.rs +++ /dev/null @@ -1,60 +0,0 @@ -//! Iter it.1 (Task 5): pin tests that the four `recur` negative -//! fixtures produce their exact diagnostic codes, and that the -//! positive `loop_smoke` fixture typechecks clean. -//! -//! Spec: `docs/specs/2026-05-15-iteration-discipline.md`. The four -//! negatives live as canonical `.ail.json` (diagnostic code is the -//! load-bearing assertion, not the surface form), mirroring the -//! `mut_typecheck_pin` carve-out precedent. - -use ailang_check::check_workspace; -use ailang_surface::load_workspace; -use std::path::PathBuf; - -fn examples_dir() -> PathBuf { - let manifest = env!("CARGO_MANIFEST_DIR"); - PathBuf::from(manifest) - .parent().expect("CARGO_MANIFEST_DIR has a parent (crates/ailang-check)") - .parent().expect("CARGO_MANIFEST_DIR has a grandparent (crates/)") - .join("examples") -} - -/// Load the named fixture under `examples/`, run check_workspace, and -/// return the diagnostic code list (one entry per Diagnostic). -fn check_fixture(fixture_name: &str) -> Vec { - let path = examples_dir().join(fixture_name); - let ws = load_workspace(&path) - .unwrap_or_else(|e| panic!("workspace `{fixture_name}` must load: {e:?}")); - let diags = check_workspace(&ws); - diags.iter().map(|d| d.code.clone()).collect() -} - -#[test] -fn loop_smoke_typechecks_clean() { - let codes = check_fixture("loop_smoke.ail"); - assert!(codes.is_empty(), "expected zero diagnostics, got {codes:?}"); -} - -#[test] -fn recur_outside_loop_is_rejected() { - let codes = check_fixture("test_recur_outside_loop.ail.json"); - assert_eq!(codes, vec!["recur-outside-loop".to_string()]); -} - -#[test] -fn recur_arity_mismatch_is_rejected() { - let codes = check_fixture("test_recur_arity_mismatch.ail.json"); - assert_eq!(codes, vec!["recur-arity-mismatch".to_string()]); -} - -#[test] -fn recur_type_mismatch_is_rejected() { - let codes = check_fixture("test_recur_type_mismatch.ail.json"); - assert_eq!(codes, vec!["recur-type-mismatch".to_string()]); -} - -#[test] -fn recur_not_in_tail_position_is_rejected() { - let codes = check_fixture("test_recur_not_in_tail_position.ail.json"); - assert_eq!(codes, vec!["recur-not-in-tail-position".to_string()]); -} diff --git a/crates/ailang-check/tests/structural_recursion_pin.rs b/crates/ailang-check/tests/structural_recursion_pin.rs deleted file mode 100644 index db9d5d9..0000000 --- a/crates/ailang-check/tests/structural_recursion_pin.rs +++ /dev/null @@ -1,129 +0,0 @@ -//! Iter it.2: pin tests for the structural-recursion guardedness -//! pass + the it.2-only `tail:true` grandfather + the first real -//! `Diverge` effect injection. -//! -//! Spec: `docs/specs/2026-05-15-iteration-discipline.md`. Mirrors the -//! it.1 `loop_recur_pin.rs` harness verbatim (same inline -//! `check_fixture` helper, no `mod common`). - -use ailang_check::check_workspace; -use ailang_surface::load_workspace; -use std::path::PathBuf; - -fn examples_dir() -> PathBuf { - let manifest = env!("CARGO_MANIFEST_DIR"); - PathBuf::from(manifest) - .parent().expect("CARGO_MANIFEST_DIR has a parent (crates/ailang-check)") - .parent().expect("CARGO_MANIFEST_DIR has a grandparent (crates/)") - .join("examples") -} - -/// Load the named fixture under `examples/`, run check_workspace, and -/// return the diagnostic code list (one entry per Diagnostic). -fn check_fixture(fixture_name: &str) -> Vec { - let path = examples_dir().join(fixture_name); - let ws = load_workspace(&path) - .unwrap_or_else(|e| panic!("workspace `{fixture_name}` must load: {e:?}")); - let diags = check_workspace(&ws); - diags.iter().map(|d| d.code.clone()).collect() -} - -#[test] -fn structural_list_len_is_clean() { - // Plain non-tail recursion on a Cons sub-component typechecks - // clean: structurally guarded ⇒ pure + total, no diagnostics. - assert!( - check_fixture("struct_rec_list_len.ail").is_empty(), - "expected zero diagnostics for structural list length" - ); -} - -#[test] -fn foldl_accumulator_is_structural_and_clean() { - // A foldl-shape accumulator walk (structural on the tail, - // unconstrained accumulator) classifies as structural recursion - // and stays clean + Diverge-free (spec D1). - assert!( - check_fixture("struct_rec_foldl_sum.ail").is_empty(), - "expected zero diagnostics for foldl-shape accumulator walk" - ); -} - -#[test] -fn non_structural_self_call_is_rejected() { - // A self-call passing the un-decreased parameter at every - // candidate position, not `tail`-marked, fires - // `non-structural-recursion`. - assert!( - check_fixture("test_non_structural_recursion.ail.json") - .contains(&"non-structural-recursion".to_string()), - "expected non-structural-recursion diagnostic" - ); -} - -#[test] -fn tree_forest_mutual_is_clean() { - // Mutual tree/forest recursion over one ADT family (the - // cross-reference edge unions {Tree, Forest}) classifies as a - // mutual structural group: clean, Diverge-free. - assert!( - check_fixture("struct_rec_tree_forest.ail").is_empty(), - "expected zero diagnostics for same-family mutual recursion" - ); -} - -#[test] -fn mutual_cross_family_is_rejected() { - // Mutual recursion whose members' structural params lie in two - // unrelated ADT families is not a valid mutual structural group - // (DD-3): the cross-call is an unguarded recursive call. - assert!( - check_fixture("test_mutual_cross_family.ail.json") - .contains(&"non-structural-recursion".to_string()), - "expected non-structural-recursion for cross-family mutual recursion" - ); -} - -#[test] -fn loop_fn_declaring_diverge_is_clean() { - // A loop-bearing fn that declares `!Diverge` in its effect row - // reconciles clean (DD-4 / D2). - assert!( - check_fixture("loop_needs_diverge.ail").is_empty(), - "expected zero diagnostics for loop fn declaring !Diverge" - ); -} - -#[test] -fn loop_fn_missing_diverge_is_rejected() { - // A loop-bearing fn missing `!Diverge` raises the existing - // `undeclared-effect` (no new diagnostic variant; DD-4). - assert!( - check_fixture("test_loop_missing_diverge.ail.json") - .contains(&"undeclared-effect".to_string()), - "expected undeclared-effect for loop fn missing !Diverge" - ); -} - -#[test] -fn structural_recursion_is_diverge_free() { - // Structural recursion injects no effect: a structural list walk - // with no `loop` and no declared `!Diverge` stays clean. - assert!( - check_fixture("struct_rec_list_len.ail").is_empty(), - "structural recursion must be Diverge-free" - ); -} - -#[test] -fn non_structural_recursion_code_is_registered() { - // A CheckError::NonStructuralRecursion must map to the kebab code. - // This step only pins the code() arm exists and returns the exact - // string; fixture-level behaviour is pinned in Task 2+. - use ailang_check::CheckError; - let e = CheckError::NonStructuralRecursion { - callee: "f".into(), - arg: "n".into(), - }; - assert_eq!(e.code(), "non-structural-recursion"); -} diff --git a/crates/ailang-codegen/src/escape.rs b/crates/ailang-codegen/src/escape.rs index dfeacb4..7a6f48d 100644 --- a/crates/ailang-codegen/src/escape.rs +++ b/crates/ailang-codegen/src/escape.rs @@ -201,17 +201,6 @@ fn walk(t: &Term, out: &mut NonEscapeSet) { walk(body, out); } Term::Assign { value, .. } => walk(value, out), - Term::Loop { binders, body } => { - for b in binders { - walk(&b.init, out); - } - walk(body, out); - } - Term::Recur { args } => { - for a in args { - walk(a, out); - } - } Term::Lit { .. } | Term::Var { .. } => {} } } @@ -406,15 +395,6 @@ fn escapes(t: &Term, tainted: &BTreeSet, in_tail: bool) -> bool { escapes(body, tainted, in_tail) } Term::Assign { value, .. } => escapes(value, tainted, false), - Term::Loop { binders, body } => { - for b in binders { - if escapes(&b.init, tainted, false) { - return true; - } - } - escapes(body, tainted, in_tail) - } - Term::Recur { args } => args.iter().any(|a| escapes(a, tainted, false)), } } @@ -544,26 +524,6 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet, out: &mut BTreeSet< } collect_free_vars(value, bound, out); } - // Iter it.1: loop binder names bind inside the body and later - // binder inits, mirroring `Term::Mut`. Recur args are uses. - Term::Loop { binders, body } => { - let mut newly: Vec = Vec::new(); - for b in binders { - collect_free_vars(&b.init, bound, out); - if bound.insert(b.name.clone()) { - newly.push(b.name.clone()); - } - } - collect_free_vars(body, bound, out); - for n in newly { - bound.remove(&n); - } - } - Term::Recur { args } => { - for a in args { - collect_free_vars(a, bound, out); - } - } } } diff --git a/crates/ailang-codegen/src/lambda.rs b/crates/ailang-codegen/src/lambda.rs index 97c6340..65a8eae 100644 --- a/crates/ailang-codegen/src/lambda.rs +++ b/crates/ailang-codegen/src/lambda.rs @@ -144,12 +144,6 @@ impl<'a> Emitter<'a> { let saved_mut_allocas = std::mem::take(&mut self.mut_var_allocas); let saved_pending_allocas = std::mem::take(&mut self.pending_entry_allocas); let saved_entry_marker = self.entry_block_end_marker.take(); - // Iter it.1: a `loop` inside a lambda body scopes its header / - // phis to the closure's own body, not the outer fn's. Save and - // reset `loop_frames` (the exact mut.3 analogue to - // `mut_var_allocas` above) so a `Term::Recur` inside the thunk - // cannot back-edge to an outer fn's loop header. - let saved_loop_frames = std::mem::take(&mut self.loop_frames); // Iter 18d.4 fix: a lambda thunk is its own fn frame for // param-mode lookup. The outer fn's params are not in scope // inside the thunk; the thunk's own params are pushed below @@ -264,7 +258,6 @@ impl<'a> Emitter<'a> { self.mut_var_allocas = saved_mut_allocas; self.pending_entry_allocas = saved_pending_allocas; self.entry_block_end_marker = saved_entry_marker; - self.loop_frames = saved_loop_frames; // 3. Emit allocation + capture filling + closure-pair packing // in the OUTER body. Captures use 8 bytes each; closure-pair @@ -512,27 +505,6 @@ impl<'a> Emitter<'a> { } Self::collect_captures(value, bound, captures, captures_set, builtins, top_level); } - // Iter it.1: loop binder names bind inside the body and - // later binder inits — they are NOT captures, mirroring - // the `Term::Mut` arm above. Recur args are uses. - Term::Loop { binders, body } => { - let mut newly_bound: Vec = Vec::new(); - for b in binders { - Self::collect_captures(&b.init, bound, captures, captures_set, builtins, top_level); - if bound.insert(b.name.clone()) { - newly_bound.push(b.name.clone()); - } - } - Self::collect_captures(body, bound, captures, captures_set, builtins, top_level); - for n in newly_bound { - bound.remove(&n); - } - } - Term::Recur { args } => { - for a in args { - Self::collect_captures(a, bound, captures, captures_set, builtins, top_level); - } - } } } diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 3fbb42e..e21ce13 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -735,28 +735,6 @@ struct Emitter<'a> { /// at fn-body emission. Used to splice `pending_entry_allocas` /// into the entry block once body lowering completes. entry_block_end_marker: Option, - /// Iter it.1: stack of in-flight `Term::Loop` frames. Innermost - /// last. `Term::Recur` consults the innermost frame for the - /// header label and records its back-edge incoming values; the - /// `Term::Loop` arm patches each phi's incoming list once the - /// body (and all its recur sites) has been lowered. Saved / - /// reset / restored across the lambda boundary (a `loop` inside - /// a closure scopes its header to the closure's own body), the - /// exact mut.3 analogue to `mut_var_allocas`. - loop_frames: Vec, -} - -/// Iter it.1: one in-flight `Term::Loop` being lowered. `phis` -/// carries, per binder, `(phi_ssa, llvm_ty, placeholder)` — the -/// placeholder is a unique token emitted in place of the phi's -/// back-edge incoming list and string-replaced once `recur_edges` -/// is complete. `recur_edges` collects `(pred_block_label, -/// [arg_ssa,...])` one entry per `Term::Recur` reached in the body. -#[derive(Debug, Clone)] -struct LoopFrame { - header: String, - phis: Vec<(String, String, String)>, - recur_edges: Vec<(String, Vec)>, } #[derive(Debug, Clone)] @@ -877,7 +855,6 @@ impl<'a> Emitter<'a> { mut_var_allocas: BTreeMap::new(), pending_entry_allocas: String::new(), entry_block_end_marker: None, - loop_frames: Vec::new(), } } @@ -1083,7 +1060,6 @@ impl<'a> Emitter<'a> { self.mut_var_allocas.clear(); self.pending_entry_allocas.clear(); self.entry_block_end_marker = None; - self.loop_frames.clear(); for (i, pname) in f.params.iter().enumerate() { let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit); self.current_param_modes.insert(pname.clone(), mode); @@ -1861,141 +1837,6 @@ impl<'a> Emitter<'a> { )); Ok(("0".into(), "i8".into())) } - // Iter it.1: a `Term::Loop` lowers to a header block with - // one `phi` per binder. Binder inits flow in from the - // predecessor block; every enclosed `Term::Recur` adds a - // back-edge incoming value. The phi's back-edge incoming - // list is emitted as a unique placeholder token and - // string-replaced once the body (and all its recur sites) - // has been lowered — phi instructions must syntactically - // precede the body, but the recur predecessors are only - // known after lowering it. - Term::Loop { binders, body } => { - // 1. Lower each binder init in the CURRENT block. - let pred = self.current_block.clone(); - // Per binder: (name, ail_ty, init_ssa, llvm_ty). - let mut init_ssa: Vec<(String, Type, String, String)> = Vec::new(); - for b in binders { - let lty = llvm_type(&b.ty)?; - let (v, vty) = self.lower_term(&b.init)?; - if vty != lty { - return Err(CodegenError::Internal(format!( - "Term::Loop binder `{}`: init LLVM type {vty} != declared {lty}", - b.name - ))); - } - init_ssa.push((b.name.clone(), b.ty.clone(), v, lty)); - } - let id = self.fresh_id(); - let header = format!("loop.header.{id}"); - self.body.push_str(&format!(" br label %{header}\n")); - self.start_block(&header); - - // 2. One phi per binder. Each phi's back-edge incoming - // list is a placeholder, patched in step 4. Bind the - // phi SSA into `self.locals` so a `Term::Var` for the - // binder name inside the body resolves to it (a loop - // binder shadows like a let binding). - let mut phis: Vec<(String, String, String)> = Vec::new(); - let mut saved_locals: Vec<(String, Option<(String, String, String, Type)>)> = - Vec::new(); - for (idx, (name, ail_ty, iv, lty)) in init_ssa.iter().enumerate() { - let p = self.fresh_ssa(); - let placeholder = format!("/*RECUR_EDGES.{id}.{idx}*/"); - self.body.push_str(&format!( - " {p} = phi {lty} [ {iv}, %{pred} ]{placeholder}\n" - )); - let prior = self - .locals - .iter() - .rposition(|(n, _, _, _)| n == name) - .map(|pos| self.locals.remove(pos)); - self.locals.push(( - name.clone(), - p.clone(), - lty.clone(), - ail_ty.clone(), - )); - saved_locals.push((name.clone(), prior)); - phis.push((p.clone(), lty.clone(), placeholder)); - } - - // 3. Lower the body inside this loop frame. - self.loop_frames.push(LoopFrame { - header: header.clone(), - phis: phis.clone(), - recur_edges: Vec::new(), - }); - let body_result = self.lower_term(body); - let frame = self - .loop_frames - .pop() - .expect("loop frame pushed above must still be on the stack"); - - // Restore the shadowed locals unconditionally so an - // error during body lowering does not leak the binder - // bindings into the outer scope. - for (name, prior) in saved_locals.into_iter().rev() { - if let Some(pos) = self.locals.iter().rposition(|(n, _, _, _)| n == &name) { - self.locals.remove(pos); - } - if let Some(p) = prior { - self.locals.push(p); - } - } - let (body_v, body_ty) = body_result?; - - // 4. Patch each phi placeholder with the collected - // back-edge incomings (one `[ arg, %pred ]` per - // recur site). A loop whose only exit is `recur` - // has zero non-recur predecessors after the entry - // edge — that is fine; the phi still lists the - // entry edge plus the recur edges. - for (binder_idx, (_p, _lty, placeholder)) in frame.phis.iter().enumerate() { - let mut edges = String::new(); - for (pred_lbl, args) in &frame.recur_edges { - let arg = args.get(binder_idx).ok_or_else(|| { - CodegenError::Internal(format!( - "recur edge from %{pred_lbl} missing arg #{binder_idx} \ - — typecheck guarantees arity" - )) - })?; - edges.push_str(&format!(", [ {arg}, %{pred_lbl} ]")); - } - self.body = self.body.replacen(placeholder.as_str(), &edges, 1); - } - - // 5. The loop's value is the body value on the - // non-recur exit path. If every path recurred, the - // body block is terminated and the value is unused. - Ok((body_v, body_ty)) - } - // Iter it.1: a `Term::Recur` is a back-edge `br` to the - // innermost enclosing loop header. It records its argument - // SSA values + the current block label so the loop arm can - // patch the header phis. `block_terminated = true` is a - // NEW, parallel setter (it.1 additive constraint — it does - // NOT touch the seven existing tail-driven setters). - Term::Recur { args } => { - let mut arg_ssa: Vec = Vec::with_capacity(args.len()); - for a in args { - let (v, _ty) = self.lower_term(a)?; - arg_ssa.push(v); - } - let from = self.current_block.clone(); - let frame = self.loop_frames.last_mut().ok_or_else(|| { - CodegenError::Internal( - "Term::Recur without an enclosing loop frame — \ - typecheck (RecurOutsideLoop) guarantees this cannot happen" - .into(), - ) - })?; - let header = frame.header.clone(); - frame.recur_edges.push((from, arg_ssa)); - self.body.push_str(&format!(" br label %{header}\n")); - self.block_terminated = true; - Ok(("0".into(), "i8".into())) - } } } @@ -3252,11 +3093,6 @@ impl<'a> Emitter<'a> { // is exhaustive on Term so the arms must exist. Term::Mut { body, .. } => self.synth_with_extras(body, extras), Term::Assign { .. } => Ok(Type::unit()), - // Iter it.1: a loop's static type is its body's static - // type (spec §"Data model"); `Term::Recur` does not fall - // through (its synth value is never consumed). - Term::Loop { binders: _, body } => self.synth_with_extras(body, extras), - Term::Recur { .. } => Ok(Type::unit()), } } } diff --git a/crates/ailang-core/specs/form_a.md b/crates/ailang-core/specs/form_a.md index 6c31d9b..2517bb6 100644 --- a/crates/ailang-core/specs/form_a.md +++ b/crates/ailang-core/specs/form_a.md @@ -284,8 +284,6 @@ Parenthesised forms: (mut (var NAME TYPE INIT)* BODY-TERM+) ; local mutable-state block (Iter mut.1) (var NAME TYPE INIT) ; mut-var declaration; only inside (mut ...) (assign NAME VALUE-TERM) ; mut-var update; only inside (mut ...) -(loop ((var NAME TYPE INIT)*) BODY-TERM+) ; named loop head (Iter it.1) -(recur TERM*) ; backward jump to nearest enclosing (loop ...) ``` Notes: @@ -324,23 +322,6 @@ Notes: pass (iter mut.2) rejects it with `mut-assign-out-of-scope`. The expression's static type is Unit. See spec `docs/specs/2026-05-15-mut-local.md`. -- `loop` introduces one or more named, typed, initialised binders - (the same `(var NAME TYPE INIT)` shape `mut` uses) wrapped in an - explicit binder list `(...)`, followed by one or more body terms - right-folded into `Term::Seq` exactly as `mut` does. Each binder's - `INIT` is evaluated in scope of the outer environment plus the - already-declared binders; the body is in scope of all binders. The - loop's static type is the body's static type. -- `recur` re-enters the lexically nearest enclosing `loop`, - rebinding its binders positionally. It must appear in tail - position of that loop's body. Diagnostics: `recur-outside-loop` - (no enclosing loop), `recur-arity-mismatch` (arg count ≠ binder - count), `recur-type-mismatch` (arg type ≠ binder type), - `recur-not-in-tail-position` (recur reached outside the loop - body's tail context). `loop`/`recur` are additive as of iter it.1; - the structural-recursion restriction and the `Diverge` effect land - in it.2. See spec - `docs/specs/2026-05-15-iteration-discipline.md`. ## Patterns diff --git a/crates/ailang-core/src/ast.rs b/crates/ailang-core/src/ast.rs index 412d5b8..6208405 100644 --- a/crates/ailang-core/src/ast.rs +++ b/crates/ailang-core/src/ast.rs @@ -537,19 +537,6 @@ pub enum Term { name: String, value: Box, }, - /// Named loop head. The only repetition form besides structural - /// recursion. Iter it.1. `recur` re-enters the lexically - /// nearest enclosing `Loop`, rebinding `binders` positionally. - Loop { - binders: Vec, - body: Box, - }, - /// Backward jump to the lexically nearest enclosing `Loop`. - /// Must be in tail position of that loop's body. Iter it.1. - Recur { - #[serde(default)] - args: Vec, - }, } /// One arm of a [`Term::Match`]. @@ -593,17 +580,6 @@ pub struct MutVar { pub init: Term, } -/// One named, typed, initialised binder of a [`Term::Loop`]. -/// Mirrors [`MutVar`] (DD-2): no `PartialEq` — codegen maps the -/// binder name to an SSA value, never compares binders. -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct LoopBinder { - pub name: String, - #[serde(rename = "type")] - pub ty: Type, - pub init: Box, -} - /// A match pattern. /// /// The JSON discriminator is the `p` field. Patterns are linear: each @@ -970,41 +946,4 @@ mod tests { other => panic!("variant mismatch: {other:?}"), } } - - /// Iter it.1: round-trip a `Term::Loop` through JSON. Pins the - /// canonical-form shape and the `LoopBinder.ty` serde rename - /// (`"type"`); a future rename or a `skip_serializing_if` on the - /// binder fields would break the content-addressed identity this - /// pin protects. - #[test] - fn term_loop_round_trips_through_json() { - let t = Term::Loop { - binders: vec![LoopBinder { - name: "i".into(), - ty: Type::int(), - init: Box::new(Term::Lit { - lit: Literal::Int { value: 0 }, - }), - }], - body: Box::new(Term::Recur { - args: vec![Term::Var { name: "i".into() }], - }), - }; - let j = serde_json::to_string(&t).expect("serialise"); - assert!(j.contains(r#""t":"loop""#)); - assert!(j.contains(r#""type":"#)); // LoopBinder.ty serde rename - let back: Term = serde_json::from_str(&j).expect("deserialise"); - assert_eq!(serde_json::to_string(&back).expect("re-serialise"), j); - } - - /// Iter it.1: a zero-arg `Term::Recur` round-trips. `args` carries - /// `#[serde(default)]` so an absent `args` key still deserialises; - /// the empty vector serialises explicitly. - #[test] - fn term_recur_empty_args_round_trips() { - let t = Term::Recur { args: vec![] }; - let j = serde_json::to_string(&t).expect("serialise"); - let back: Term = serde_json::from_str(&j).expect("deserialise"); - assert_eq!(serde_json::to_string(&back).expect("re-serialise"), j); - } } diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index 5651f96..10a2bd2 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -363,18 +363,6 @@ fn collect_used_in_term(t: &Term, used: &mut BTreeSet) { used.insert(name.clone()); collect_used_in_term(value, used); } - Term::Loop { binders, body } => { - for b in binders { - used.insert(b.name.clone()); - collect_used_in_term(&b.init, used); - } - collect_used_in_term(body, used); - } - Term::Recur { args } => { - for a in args { - collect_used_in_term(a, used); - } - } } } @@ -602,32 +590,6 @@ impl Desugarer { name: name.clone(), value: Box::new(self.desugar_term(value, scope)), }, - Term::Loop { binders, body } => { - // Iter it.1: loop binders introduce source-level names - // like mut-vars; extend the scope per-binder with a - // `LetBound` sentinel so a generated fresh name cannot - // collide. Binder inits see earlier binders. - let mut inner = scope.clone(); - let new_binders: Vec = binders - .iter() - .map(|b| { - let init = self.desugar_term(&b.init, &inner); - inner.insert(b.name.clone(), ScopeEntry::LetBound); - LoopBinder { - name: b.name.clone(), - ty: b.ty.clone(), - init: Box::new(init), - } - }) - .collect(); - Term::Loop { - binders: new_binders, - body: Box::new(self.desugar_term(body, &inner)), - } - } - Term::Recur { args } => Term::Recur { - args: args.iter().map(|a| self.desugar_term(a, scope)).collect(), - }, Term::LetRec { name, ty, params, body, in_term } => { // Iter 16b.1: lift to a synthetic top-level fn (no-capture). // Iter 16b.2: extend the lift to the path-1 safe subset — @@ -1272,23 +1234,6 @@ pub fn free_vars_in_term(t: &Term, bound: &BTreeSet, out: &mut BTreeSet< } free_vars_in_term(value, bound, out); } - Term::Loop { binders, body } => { - // Iter it.1: a loop binder name binds inside the body. - // Each binder's `init` is evaluated in scope of the OUTER - // environment plus the already-declared binders; the body - // is in scope of all binders. Mirrors `Term::Mut`. - let mut b = bound.clone(); - for binder in binders { - free_vars_in_term(&binder.init, &b, out); - b.insert(binder.name.clone()); - } - free_vars_in_term(body, &b, out); - } - Term::Recur { args } => { - for a in args { - free_vars_in_term(a, bound, out); - } - } } } @@ -1482,43 +1427,6 @@ pub fn subst_var(t: &Term, from: &str, to: &str) -> Term { name: name.clone(), value: Box::new(subst_var(value, from, to)), }, - Term::Loop { binders, body } => { - // Iter it.1: loop binders lexically shadow outer names, - // exactly like mut-vars (above). Once a binder named - // `from` is declared, later inits AND the body stop - // substituting. - let mut shadowed = false; - let new_binders: Vec = binders - .iter() - .map(|b| { - let init = if shadowed { - (*b.init).clone() - } else { - subst_var(&b.init, from, to) - }; - if b.name == from { - shadowed = true; - } - LoopBinder { - name: b.name.clone(), - ty: b.ty.clone(), - init: Box::new(init), - } - }) - .collect(); - let body_rw = if shadowed { - (**body).clone() - } else { - subst_var(body, from, to) - }; - Term::Loop { - binders: new_binders, - body: Box::new(body_rw), - } - } - Term::Recur { args } => Term::Recur { - args: args.iter().map(|a| subst_var(a, from, to)).collect(), - }, } } @@ -1660,23 +1568,6 @@ pub fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[Stri name: assign_name.clone(), value: Box::new(subst_call_with_extras(value, name, lifted, extras)), }, - Term::Loop { binders, body } => Term::Loop { - binders: binders - .iter() - .map(|b| LoopBinder { - name: b.name.clone(), - ty: b.ty.clone(), - init: Box::new(subst_call_with_extras(&b.init, name, lifted, extras)), - }) - .collect(), - body: Box::new(subst_call_with_extras(body, name, lifted, extras)), - }, - Term::Recur { args } => Term::Recur { - args: args - .iter() - .map(|a| subst_call_with_extras(a, name, lifted, extras)) - .collect(), - }, } } @@ -1749,14 +1640,6 @@ pub fn find_non_callee_use(t: &Term, name: &str) -> Option { find_non_callee_use(value, name) } } - // Iter it.1: scan each binder's init plus the body. Loop - // binders never appear in callee position, so any matching - // `Term::Var` inside a loop is non-callee by construction. - Term::Loop { binders, body } => binders - .iter() - .find_map(|b| find_non_callee_use(&b.init, name)) - .or_else(|| find_non_callee_use(body, name)), - Term::Recur { args } => args.iter().find_map(|a| find_non_callee_use(a, name)), } } @@ -1804,10 +1687,6 @@ mod tests { vars.iter().any(|v| any_nested_ctor(&v.init)) || any_nested_ctor(body) } Term::Assign { value, .. } => any_nested_ctor(value), - Term::Loop { binders, body } => { - binders.iter().any(|b| any_nested_ctor(&b.init)) || any_nested_ctor(body) - } - Term::Recur { args } => args.iter().any(any_nested_ctor), } } @@ -1838,10 +1717,6 @@ mod tests { vars.iter().any(|v| any_let_rec(&v.init)) || any_let_rec(body) } Term::Assign { value, .. } => any_let_rec(value), - Term::Loop { binders, body } => { - binders.iter().any(|b| any_let_rec(&b.init)) || any_let_rec(body) - } - Term::Recur { args } => args.iter().any(any_let_rec), } } @@ -2963,10 +2838,6 @@ mod tests { vars.iter().any(|v| any_lit_pattern(&v.init)) || any_lit_pattern(body) } Term::Assign { value, .. } => any_lit_pattern(value), - Term::Loop { binders, body } => { - binders.iter().any(|b| any_lit_pattern(&b.init)) || any_lit_pattern(body) - } - Term::Recur { args } => args.iter().any(any_lit_pattern), } } diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs index 0da8869..dad8361 100644 --- a/crates/ailang-core/src/workspace.rs +++ b/crates/ailang-core/src/workspace.rs @@ -1259,22 +1259,6 @@ where walk_term_embedded_types(body, f) } Term::Assign { value, .. } => walk_term_embedded_types(value, f), - // Iter it.1: each `LoopBinder.ty` is an embedded type — walk - // it, then recurse into each binder's `init` and the body. - // `Term::Recur` carries no embedded type. - Term::Loop { binders, body } => { - for b in binders { - walk_type(&b.ty, f)?; - walk_term_embedded_types(&b.init, f)?; - } - walk_term_embedded_types(body, f) - } - Term::Recur { args } => { - for a in args { - walk_term_embedded_types(a, f)?; - } - Ok(()) - } } } @@ -1408,18 +1392,6 @@ where walk_term(body, f) } Term::Assign { value, .. } => walk_term(value, f), - Term::Loop { binders, body } => { - for b in binders { - walk_term(&b.init, f)?; - } - walk_term(body, f) - } - Term::Recur { args } => { - for a in args { - walk_term(a, f)?; - } - Ok(()) - } } } diff --git a/crates/ailang-core/tests/carve_out_inventory.rs b/crates/ailang-core/tests/carve_out_inventory.rs index f508e5f..e36c78f 100644 --- a/crates/ailang-core/tests/carve_out_inventory.rs +++ b/crates/ailang-core/tests/carve_out_inventory.rs @@ -3,7 +3,7 @@ //! under `examples/*.ail.json` after milestone close. The list is //! hardcoded; any change is a deliberate, brainstorm-level decision. //! -//! Twenty carve-outs post iter it.2 (2026-05-15): +//! Twelve carve-outs post iter mut.2 (2026-05-15): //! - §C4 (a) subject-matter: 7 fixtures from form-a.1 milestone //! close (canonical-form rejection / unbound / class-def rejection). //! - Iter mut.2: 5 negative typecheck fixtures for the new mut / @@ -13,14 +13,6 @@ //! fixture convention. The positive nested-shadow case is a //! .ail.json carve-out for symmetry with its negative siblings //! (the driver tests all five from one helper). -//! - Iter mut.4-tidy: 1 lambda-capture-of-mut-var negative fixture. -//! - Iter it.1: 4 recur negative typecheck fixtures. -//! - Iter it.2: 3 negative fixtures — self non-structural recursion, -//! mutual cross-family recursion (both fire `non-structural- -//! recursion`), and a loop-bearing fn missing `!Diverge` (fires -//! the existing `undeclared-effect`, no new variant per DD-4). The -//! diagnostic code is the load-bearing assertion, not the surface -//! form. //! - §C4 (b) compile-time-embed: retired 2026-05-14 by milestone //! prelude-decouple; the prelude is now embedded as `prelude.ail` //! in `ailang-surface` and parsed at compile time via @@ -45,15 +37,6 @@ const EXPECTED: &[&str] = &[ "test_mut_var_unsupported_type.ail.json", // Iter mut.4-tidy — lambda-capture-of-mut-var rejection "test_mut_var_captured_by_lambda.ail.json", - // Iter it.1 — recur negative typecheck fixtures - "test_recur_outside_loop.ail.json", - "test_recur_arity_mismatch.ail.json", - "test_recur_type_mismatch.ail.json", - "test_recur_not_in_tail_position.ail.json", - // Iter it.2 — non-structural-recursion negative fixtures - "test_non_structural_recursion.ail.json", - "test_mutual_cross_family.ail.json", - "test_loop_missing_diverge.ail.json", ]; fn examples_dir() -> std::path::PathBuf { diff --git a/crates/ailang-core/tests/design_schema_drift.rs b/crates/ailang-core/tests/design_schema_drift.rs index d5cf2b3..1231549 100644 --- a/crates/ailang-core/tests/design_schema_drift.rs +++ b/crates/ailang-core/tests/design_schema_drift.rs @@ -151,17 +151,6 @@ fn design_md_anchors_every_term_variant() { value: Box::new(Term::Lit { lit: Literal::Unit }), }, ), - ( - r#""t": "loop""#, - Term::Loop { - binders: Vec::new(), - body: Box::new(Term::Lit { lit: Literal::Unit }), - }, - ), - ( - r#""t": "recur""#, - Term::Recur { args: Vec::new() }, - ), ]; for (anchor, term) in exemplars { @@ -183,8 +172,6 @@ fn design_md_anchors_every_term_variant() { Term::ReuseAs { .. } => "reuse-as", Term::Mut { .. } => "mut", Term::Assign { .. } => "assign", - Term::Loop { .. } => "loop", - Term::Recur { .. } => "recur", }; assert!( data_model_section().contains(anchor), @@ -443,3 +430,20 @@ fn data_model_section_is_bounded() { section.len() ); } + +#[test] +fn design_md_documents_the_accumulator_over_iteration_idiom() { + let design = std::fs::read_to_string( + concat!(env!("CARGO_MANIFEST_DIR"), "/../../docs/DESIGN.md"), + ) + .expect("read DESIGN.md"); + assert!( + design.contains("Accumulator-over-iteration shape (documented idiom, not an enforced rule)"), + "the F1/F4 documented-idiom note must not be silently dropped from DESIGN.md" + ); + assert!( + design.contains("examples/mut_counter.ail is the reference") + || design.contains("`examples/mut_counter.ail` is the reference"), + "the F1/F4 note must keep pointing at the canonical fallback fixture" + ); +} diff --git a/crates/ailang-core/tests/schema_coverage.rs b/crates/ailang-core/tests/schema_coverage.rs index 25cc4cb..fcc7d13 100644 --- a/crates/ailang-core/tests/schema_coverage.rs +++ b/crates/ailang-core/tests/schema_coverage.rs @@ -49,8 +49,6 @@ enum VariantTag { TermReuseAs, TermMut, TermAssign, - TermLoop, - TermRecur, // Pattern PatternWild, PatternVar, @@ -98,8 +96,6 @@ const EXPECTED_VARIANTS: &[VariantTag] = &[ VariantTag::TermReuseAs, VariantTag::TermMut, VariantTag::TermAssign, - VariantTag::TermLoop, - VariantTag::TermRecur, VariantTag::PatternWild, VariantTag::PatternVar, VariantTag::PatternLit, @@ -248,20 +244,6 @@ fn visit_term(t: &Term, observed: &mut HashSet) { observed.insert(VariantTag::TermAssign); visit_term(value, observed); } - Term::Loop { binders, body } => { - observed.insert(VariantTag::TermLoop); - for b in binders { - visit_type(&b.ty, observed); - visit_term(&b.init, observed); - } - visit_term(body, observed); - } - Term::Recur { args } => { - observed.insert(VariantTag::TermRecur); - for a in args { - visit_term(a, observed); - } - } } } diff --git a/crates/ailang-core/tests/spec_drift.rs b/crates/ailang-core/tests/spec_drift.rs index b1a01bd..a7d1371 100644 --- a/crates/ailang-core/tests/spec_drift.rs +++ b/crates/ailang-core/tests/spec_drift.rs @@ -128,17 +128,6 @@ fn spec_mentions_every_term_variant() { value: Box::new(Term::Lit { lit: Literal::Unit }), }, ), - ( - "(loop", - Term::Loop { - binders: Vec::new(), - body: Box::new(Term::Lit { lit: Literal::Unit }), - }, - ), - ( - "(recur", - Term::Recur { args: Vec::new() }, - ), ]; for (anchor, term) in exemplars { @@ -162,8 +151,6 @@ fn spec_mentions_every_term_variant() { Term::ReuseAs { .. } => "reuse-as", Term::Mut { .. } => "mut", Term::Assign { .. } => "assign", - Term::Loop { .. } => "loop", - Term::Recur { .. } => "recur", }; assert!( FORM_A_SPEC.contains(anchor), diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs index 76bfc60..baa3f39 100644 --- a/crates/ailang-prose/src/lib.rs +++ b/crates/ailang-prose/src/lib.rs @@ -935,37 +935,6 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, ow out.push_str(" := "); write_term(out, value, level, owning_module); } - Term::Loop { binders, body } => { - // Iter it.1: prose-side minimal-correctness rendering for - // the `(loop ...)` head, mirroring the `mut` block shape - // above. The prose surface for loops is not yet fully - // designed; a follow-on prose iter refines it once the - // LLM-author signal arrives. - out.push_str("loop {\n"); - for b in binders { - indent(out, level + 1); - out.push_str("var "); - out.push_str(&b.name); - out.push_str(" = "); - write_term(out, &b.init, level + 1, owning_module); - out.push_str(";\n"); - } - indent(out, level + 1); - write_term(out, body, level + 1, owning_module); - out.push('\n'); - indent(out, level); - out.push('}'); - } - Term::Recur { args } => { - out.push_str("recur("); - for (i, a) in args.iter().enumerate() { - if i > 0 { - out.push_str(", "); - } - write_term(out, a, level, owning_module); - } - out.push(')'); - } } } @@ -1164,26 +1133,6 @@ fn count_free_var(name: &str, t: &Term) -> usize { let n_use = if assign_name == name { 1 } else { 0 }; n_use + count_free_var(name, value) } - // Iter it.1: a loop binder named `name` shadows the outer - // binding for both later binder inits and the body, exactly - // like `Term::Mut`. - Term::Loop { binders, body } => { - let mut total = 0usize; - let mut shadowed = false; - for b in binders { - if !shadowed { - total += count_free_var(name, &b.init); - } - if b.name == name { - shadowed = true; - } - } - if !shadowed { - total += count_free_var(name, body); - } - total - } - Term::Recur { args } => args.iter().map(|a| count_free_var(name, a)).sum(), } } @@ -1336,39 +1285,6 @@ fn subst_var_with_term(t: &Term, name: &str, replacement: &Term) -> Term { name: assign_name.clone(), value: Box::new(subst_var_with_term(value, name, replacement)), }, - Term::Loop { binders, body } => { - let mut shadowed = false; - let new_binders: Vec = binders - .iter() - .map(|b| { - let init = if shadowed { - (*b.init).clone() - } else { - subst_var_with_term(&b.init, name, replacement) - }; - if b.name == name { - shadowed = true; - } - ailang_core::ast::LoopBinder { - name: b.name.clone(), - ty: b.ty.clone(), - init: Box::new(init), - } - }) - .collect(); - let body_rw = if shadowed { - (**body).clone() - } else { - subst_var_with_term(body, name, replacement) - }; - Term::Loop { - binders: new_binders, - body: Box::new(body_rw), - } - } - Term::Recur { args } => Term::Recur { - args: args.iter().map(|a| subst_var_with_term(a, name, replacement)).collect(), - }, } } @@ -2185,43 +2101,6 @@ mod tests { assert_eq!(render_term(&t), "tail not(x)"); } - /// Iter it.1: prose-projection lockstep for `Term::Loop` / - /// `Term::Recur`. The property protected: the prose renderer - /// projects a loop's binders + body and a recur's args without - /// dropping or reordering them (free-var / subst arms are - /// exercised by the existing prose suite). Prose is a one-way - /// projection (no Form-B parser exists — see CLAUDE.md), so an - /// AST-equality round-trip is not expressible; this render - /// assertion is the feasible lockstep, using the same - /// `render_term` harness the neighbouring render tests use. - #[test] - fn loop_and_recur_project_to_prose() { - let t = Term::Loop { - binders: vec![ailang_core::ast::LoopBinder { - name: "i".into(), - ty: ailang_core::ast::Type::Con { - name: "Int".into(), - args: vec![], - }, - init: Box::new(Term::Lit { - lit: ailang_core::ast::Literal::Int { value: 0 }, - }), - }], - body: Box::new(Term::Recur { - args: vec![ivar("i")], - }), - }; - let rendered = render_term(&t); - assert!( - rendered.contains("loop {") && rendered.contains("var i = 0"), - "loop head not projected, got:\n{rendered}" - ); - assert!( - rendered.contains("recur(i)"), - "recur not projected, got:\n{rendered}" - ); - } - // ---- Polish 4: long doc-string wrap ---- #[test] diff --git a/crates/ailang-surface/src/parse.rs b/crates/ailang-surface/src/parse.rs index 09c0c0d..6d4a593 100644 --- a/crates/ailang-surface/src/parse.rs +++ b/crates/ailang-surface/src/parse.rs @@ -40,7 +40,7 @@ //! | app-term | tail-app-term | match-term | ctor-term //! | do-term | tail-do-term | seq-term | lam-term | if-term //! | let-term | let-rec-term | clone-term | reuse-as-term -//! | mut-term | assign-term | loop-term | recur-term +//! | mut-term | assign-term //! var-ref ::= ident ; reserved: true/false → bool-lit //! int-lit ::= integer ; numeric atom //! str-lit ::= string ; string atom @@ -68,10 +68,8 @@ //! clone-term ::= "(" "clone" term ")" ; Iter 18c.1 //! reuse-as-term ::= "(" "reuse-as" term term ")" ; Iter 18d.1 //! mut-term ::= "(" "mut" var-decl* term+ ")" ; Iter mut.1 -//! var-decl ::= "(" "var" ident type term ")" ; legal only inside mut-term / loop-term +//! var-decl ::= "(" "var" ident type term ")" ; legal only inside mut-term //! assign-term ::= "(" "assign" ident term ")" ; Iter mut.1; legal only inside mut-term -//! loop-term ::= "(" "loop" "(" var-decl* ")" term+ ")" ; Iter it.1 -//! recur-term ::= "(" "recur" term* ")" ; Iter it.1; tail-position-only in loop //! //! pattern ::= pat-var | pat-ctor | pat-lit | pat-wild //! pat-var ::= ident @@ -1214,8 +1212,6 @@ impl<'a> Parser<'a> { "reuse-as" => self.parse_reuse_as(), "mut" => self.parse_mut(), "assign" => self.parse_assign(), - "loop" => self.parse_loop(), - "recur" => self.parse_recur(), other => { let pos = self.peek().map(|t| t.span.start).unwrap_or(0); Err(ParseError::Production { @@ -1224,7 +1220,7 @@ impl<'a> Parser<'a> { "unknown term head `{other}`; expected one of \ `app`, `tail-app`, `lam`, `let`, `let-rec`, `if`, `match`, `do`, \ `tail-do`, `seq`, `term-ctor`, `clone`, `reuse-as`, `mut`, \ - `assign`, `loop`, `recur`, `lit-unit`" + `assign`, `lit-unit`" ), pos, }) @@ -1646,80 +1642,6 @@ impl<'a> Parser<'a> { }) } - /// Iter it.1: `(loop ((var NAME TYPE INIT)*) BODY-TERM+)` — named - /// loop head. The binder list is an explicit parenthesised group - /// holding zero or more `(var NAME TYPE INIT)` entries (same entry - /// shape `parse_mut` reads); the trailing ≥ 1 body terms are - /// right-folded into `Term::Seq` exactly as `parse_mut` does. The - /// recur arity / type / tail-position rules are enforced at - /// typecheck (it.1 Task 5); the parser accepts the shape. - fn parse_loop(&mut self) -> Result { - let head_pos = self.peek().map(|t| t.span.start).unwrap_or(0); - self.expect_lparen("loop-term")?; - self.expect_keyword("loop")?; - - // The binder list is an explicit parenthesised group of - // (var NAME TYPE INIT) entries. - self.expect_lparen("loop-binder-list")?; - let mut binders: Vec = Vec::new(); - while matches!(self.peek_head_ident(), Some("var")) { - self.expect_lparen("loop-binder")?; - self.expect_keyword("var")?; - let name = self.expect_ident("loop-binder-name")?; - let ty = self.parse_type()?; - let init = self.parse_term()?; - self.expect_rparen("loop-binder")?; - binders.push(ailang_core::ast::LoopBinder { - name, - ty, - init: Box::new(init), - }); - } - self.expect_rparen("loop-binder-list")?; - - // Then read ≥ 1 trailing body terms, right-folded into Seq. - let mut body_stmts: Vec = Vec::new(); - while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) { - body_stmts.push(self.parse_term()?); - } - if body_stmts.is_empty() { - return Err(ParseError::Production { - production: "loop-term", - message: "(loop ...) requires at least one body expression after the binder list" - .into(), - pos: head_pos, - }); - } - self.expect_rparen("loop-term")?; - - let mut body = body_stmts.pop().expect("non-empty after the check above"); - while let Some(s) = body_stmts.pop() { - body = Term::Seq { - lhs: Box::new(s), - rhs: Box::new(body), - }; - } - Ok(Term::Loop { - binders, - body: Box::new(body), - }) - } - - /// Iter it.1: `(recur TERM*)` — backward jump to the lexically - /// nearest enclosing `(loop ...)`. The parser accepts any arg - /// count; the enclosing-loop / arity / type / tail-position rules - /// are enforced at typecheck (it.1 Task 5). - fn parse_recur(&mut self) -> Result { - self.expect_lparen("recur-term")?; - self.expect_keyword("recur")?; - let mut args: Vec = Vec::new(); - while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) { - args.push(self.parse_term()?); - } - self.expect_rparen("recur-term")?; - Ok(Term::Recur { args }) - } - // ---- patterns ------------------------------------------------------- fn parse_pattern(&mut self) -> Result { @@ -2661,29 +2583,4 @@ mod tests { "diagnostic should mention missing body, got: {msg}" ); } - - /// Iter it.1: `(loop ((var i Int 0)) (recur i))` parses to a - /// `Term::Loop` with one binder and a `Term::Recur` body. The - /// binder list is explicitly parenthesised (unlike `mut`). - #[test] - fn parses_loop_with_one_binder_and_recur_body() { - let src = "(loop ((var i (con Int) 0)) (recur i))"; - let t = parse_term(src).expect("loop parses"); - match t { - Term::Loop { binders, body } => { - assert_eq!(binders.len(), 1); - assert_eq!(binders[0].name, "i"); - assert!(matches!(*body, Term::Recur { .. })); - } - other => panic!("expected Term::Loop, got {other:?}"), - } - } - - /// Iter it.1: `(recur)` with no args parses to an empty-args - /// `Term::Recur` (arity/scope validity is a typecheck concern). - #[test] - fn parses_recur_zero_args() { - let t = parse_term("(recur)").expect("recur parses"); - assert!(matches!(t, Term::Recur { args } if args.is_empty())); - } } diff --git a/crates/ailang-surface/src/print.rs b/crates/ailang-surface/src/print.rs index 39bd7ef..82eb166 100644 --- a/crates/ailang-surface/src/print.rs +++ b/crates/ailang-surface/src/print.rs @@ -594,54 +594,6 @@ fn write_term(out: &mut String, t: &Term, level: usize) { write_term(out, value, level); out.push(')'); } - Term::Loop { binders, body } => { - // Iter it.1: print as - // `(loop ((var NAME TYPE INIT)*) STMT* FINAL_EXPR)` - // The binder list is explicitly parenthesised (unlike - // `mut`); the body's `Term::Seq` right-spine is walked the - // same way the `Term::Mut` arm above walks it. - out.push_str("(loop ("); - for (k, b) in binders.iter().enumerate() { - if k > 0 { - out.push(' '); - } - out.push_str("(var "); - out.push_str(&b.name); - out.push(' '); - write_type(out, &b.ty); - out.push(' '); - write_term(out, &b.init, level); - out.push(')'); - } - out.push(')'); - let mut cursor: &Term = body; - loop { - match cursor { - Term::Seq { lhs, rhs } => { - out.push(' '); - write_term(out, lhs, level); - cursor = rhs; - } - other => { - out.push(' '); - write_term(out, other, level); - break; - } - } - } - out.push(')'); - } - Term::Recur { args } => { - // Iter it.1: print as `(recur ARG*)`. Legal only in tail - // position of an enclosing `Term::Loop` body; the - // typechecker (it.1 Task 5) enforces that rule. - out.push_str("(recur"); - for a in args { - out.push(' '); - write_term(out, a, level); - } - out.push(')'); - } } } diff --git a/docs/DESIGN.md b/docs/DESIGN.md index cd6f2cb..89d4ec6 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -102,12 +102,17 @@ A proposed feature ships only if all three hold: the bug class is structurally impossible rather than merely discouraged. A documentation note is not a reshape; the discriminator is whether the wrong code fails to typecheck, not - whether a guideline advises against it. The canonical worked - example is the iteration story: a bare `while` over mutable state - passes 1 and 2 yet fails 3 (it reinstates iterated-mutable-state - reasoning); structural recursion over an acyclic ADT and a named - loop/recur point pass all three (the bug class is closed by - construction, not by advice). + whether a guideline advises against it. Worked example: a bare + `while` over mutable state would pass clauses 1 and 2 yet fail + clause 3 (it reinstates iterated-mutable-state reasoning the pure + core exists to remove); a hypothetical "all repetition is either + structurally-decreasing recursion over an acyclic ADT or an + explicit named loop" iteration story would, *if it could be built + without a documented-unenforced precondition*, pass all three — + and the fact that the 2026-05 attempt could not (it forced a + silent-divergence precondition; see + `docs/specs/2026-05-16-iteration-discipline-revert.md`) is itself + the clause-3 mechanism working as intended. This is the positive complement to the CLAUDE.md rule that implementation effort is not a rationale: cost is not a reason *for* a @@ -164,16 +169,8 @@ Advantages: The default is total, pure functions. Effects are declared as a set in the function type: `(Int) -> Int ![IO]`. The effect set is row-polymorphic -(`![IO | r]`). Two effects are wired up: `IO` (observable side effects, -raised by `do`-operations), and `Diverge` (non-termination). As of iter -it.2 (2026-05-15) `Diverge` is no longer nominal: it is the effect carried -by any function whose body contains a `loop` (or that calls a -`Diverge`-declaring function), surfaced through the existing -declared-vs-raised reconciliation (an undeclared `Diverge` is the existing -`UndeclaredEffect`, no new diagnostic). Structural recursion is pure and -total and carries no effect — the author who wants a `!Diverge`-free -signature is structurally pulled toward structural recursion and pays -`!Diverge` only when genuinely writing an unbounded `loop`. +(`![IO | r]`). In the MVP only the effects `IO` and `Diverge` (for infinite +loops) are wired up. This is the most important LLM property: when I read a function, I can trust its signature without reading the body. @@ -2418,22 +2415,6 @@ are real surface forms. { "t": "assign", "name": "", "value": Term } - -// Iter it.1: named loop head. `binders` declares one or more -// lexically-scoped, typed, initialised binders (initialised in -// order); `body` is a single Term in scope of all binders. `recur` -// re-enters the lexically nearest enclosing loop, rebinding the -// binders positionally; it must be in tail position of that loop's -// body. The loop's static type is `body`'s static type. -{ "t": "loop", - "binders": [ { "name": "", "type": Type, "init": Term }, ... ], - "body": Term } - -// Iter it.1: backward jump to the lexically nearest enclosing loop; -// tail-position-only; binds that loop's binders. The `args` array is -// always present in canonical JSON (even when empty). -{ "t": "recur", - "args": [ Term, ... ] } ``` In the MVP, `do` is only a direct call to a built-in effect op (no @@ -2449,23 +2430,6 @@ mut-var into a lambda body is rejected at typecheck via `CheckError::MutVarCapturedByLambda` (iter mut.4-tidy). See `docs/specs/2026-05-15-mut-local.md`. -`loop`/`recur` are additive as of iter it.1 (2026-05-15): they -parse, print, prose-project, round-trip, typecheck (binder typing, -recur arity/type unification, recur tail-position) and codegen -(loop-header block with one phi per binder, `recur` as a back-edge -`br`) without removing or modifying the existing `tail-app`/`tail-do` -paths. As of iter it.2 (2026-05-15) the structural-recursion -guardedness restriction and the `Diverge` effect are in effect: -a non-structural recursion-by-call is the compile error -`NonStructuralRecursion` (directing the author to `(loop …)` / -`recur`), and any fn whose body contains a `Term::Loop` (or calls a -`Diverge`-declaring callee) must declare `!Diverge` in its effect -row — structural recursion stays pure, total, and effect-free. A -transitional grandfather exempts still-`tail: true`-marked recursive -calls so the corpus type-checks unchanged through it.2. -`tail-app`/`tail-do` are retired in it.3. See -`docs/specs/2026-05-15-iteration-discipline.md`. - **`Literal`**: ```jsonc @@ -2917,6 +2881,8 @@ What **is** supported (and used as the smoke test for the pipeline): effect), and introduce composable transducers (`Stateful a b` + `pipe`). Spec: `docs/specs/2026-05-15-mut-local.md`. +**Accumulator-over-iteration shape (documented idiom, not an enforced rule).** `mut`/`var`/`assign` removes friction from *straight-line* and *cascade-of-if* accumulators, but does **not** by itself express the "one running total updated once per loop iteration" shape: a `var` cannot be captured into a lambda (the seal) and there is no loop construct in the language. Until a future iteration-totality milestone lands (gated behind `Nat`/refinement types — see the deferred roadmap entry), the canonical pattern for the per-iteration accumulator is a tail-recursive helper that threads the running total as an explicit parameter; `examples/mut_counter.ail` is the reference. This is a documented authoring idiom, not a typecheck-enforced constraint — wrong code here does not fail to compile, it is merely less ergonomic, which is exactly why this is documentation and not a language rule. + Pipeline regression smoke tests: - `examples/sum.ail.json` → prints 55 (recursion, arithmetic). diff --git a/docs/journals/2026-05-16-iter-revert.md b/docs/journals/2026-05-16-iter-revert.md new file mode 100644 index 0000000..6bddafd --- /dev/null +++ b/docs/journals/2026-05-16-iter-revert.md @@ -0,0 +1,174 @@ +# iter revert — Iteration-discipline milestone surgical forward revert + +**Date:** 2026-05-16 +**Started from:** abf00131c10ff9287b419439c565480c96fa861b +**Status:** DONE +**Tasks completed:** 11 of 11 + +## Summary + +The Iteration-discipline milestone (it.1 `96db54d` + it.2 `a4be1e5`) +is fully backed out by a single forward iteration, with `1ff7e81` +(the last commit before milestone-start `9973546`) as the per-region +byte oracle. `main` was never rewound — every restore is a forward +working-tree edit, net-new it.1/it.2 surface is `rm`'d, DESIGN.md is +hunk-edited in place (clause 3 / criterion section KEPT, never +wholesale-restored). Feature-acceptance clause 3 and the F3 todo are +retained; the clause-3 worked example is de-claimed from "shipped" to +hypothetical-illustration form (in DESIGN.md and brainstorm SKILL.md +in lockstep); one honest F1/F4 documentation note is added (the only +net addition) and guarded by a doc-presence test. The correctness +gate (Task 11) proved compiler behaviour **pristine**: all 164 +surviving `1ff7e81`-era fixtures `ail check`/`ail run` byte-identical +to their pre-milestone behaviour; `cargo test --workspace` 600/0; +zero residual it.1/it.2 production surface. AILang's iteration story +is exactly the pre-`9973546` state (structural / tail recursion; +`tail-app` intact); the genuine total-recursion ambition is preserved +on the roadmap as a deferred P2 milestone sequenced behind a future +`Nat`/refinement-types milestone. + +## Per-task notes + +- revert.1: AST node family + drift anchors + DESIGN.md §Data-model — + removed `Term::Loop`/`Term::Recur`/`struct LoopBinder` + 2 serde + units (ast.rs byte-identical to oracle); loop/recur exemplars + + match arms removed from design_schema_drift.rs / spec_drift.rs / + schema_coverage.rs (byte-identical); DESIGN.md §Data-model + loop/recur JSON + it.1/it.2 prose removed (region byte-identical). +- revert.2: `CheckError` surface — 5 variants + doc comments, 5 + `code()` arms, 3 dedicated `ctx()` arms deleted; `_ =>` catch-all + preserved; diagnostic.rs confirmed genuine no-op. +- revert.3: it.2 guardedness pass + Diverge-injection — STOP-gate + cleared (all 6 named helpers it.2-net-new at oracle → all delete, + no ambiguity). Removed the entire 687-line guardedness cluster + (verify_structural_recursion, term_contains_loop, adt_families, + referenced_con_names, mutual_structural_group, adt_param_positions, + RecCall, TypeUnionFind, MutualGroup, et al.) **plus** the + transitively-it.2 `module_fns` plumbing through + check_module/check_def/check_fn signatures (oracle proved net-new; + resolved via the plan's Oracle convention + recon-by-name mandate — + see Concerns). 3 Diverge-injection sites restored byte-identical; + lib.rs `"Diverge"` count 0 == oracle. +- revert.4: it.1 check surface — synth Loop/Recur arms + + verify_loop_body deleted; loop_stack param + ~30 threaded calls + 9 + local decls removed; verify_tail_positions survives, it.1 arms + removed, byte-identical to oracle; substitute_rigids_in_term + + post-mono name arms cleaned. Result: + `crates/ailang-check/src/lib.rs` FULLY byte-identical to `1ff7e81`. +- revert.5: 9 remaining walker files (lift/mono/linearity/uniqueness/ + reuse_shape/pre_desugar_validation/builtins + core desugar/ + workspace) restored to oracle, all byte-identical; pre-restore diff + classification proved every hunk it.1/it.2-only. +- revert.6: surface + prose + form-A grammar — parse.rs/print.rs/ + prose lib.rs/form_a.md restored to oracle byte-identical; each + touched only by 96db54d (it.1) since 1ff7e81; surface+prose build + clean. +- revert.7: codegen — lib.rs/escape.rs/lambda.rs + ail/main.rs + restored to oracle byte-identical; `block_terminated = true` count + == 8 == oracle (it.1 parallel setter gone; the 4 tail-driven + 4 + control-flow setters survive). `cargo build --workspace` clean + (first full-build gate, lockstep clustering worked as designed). +- revert.8: STOP-gate re-verify cleared (live `git diff --stat` + matched plan's net-new/modified/absent classification exactly). + Deleted 2 pin files + 16 fixtures + bench/it3-oracle via plain + `rm` (no git-index touch). 2 RC fixtures restored byte-identical. + e2e.rs + codegen_import_map_fallback_pin.rs + carve_out_inventory.rs + restored byte-identical (carve = "Twelve carve-outs", last entry + test_mut_var_captured_by_lambda.ail.json). it.{1,2,3} stats json + KEPT. cargo test --workspace 599/0. +- revert.9: DESIGN.md Decision 3 → 1ff7e81 placeholder (byte-identical, + hunk-only); clause-3 worked example de-claimed to hypothetical form + (criterion section + clause-3 discriminator KEPT); brainstorm + SKILL.md de-claimed in lockstep; F1/F4 note added verbatim; + doc-presence test added verbatim, PASSES. +- revert.10: roadmap Iteration-discipline [~] block + blocking-fork + sub-section removed; deferred "Iteration-totality story" entry + added verbatim at top of P2 (per plan + spec sequencing); F3 + + Stateful-islands untouched; superseded header prepended to the old + spec; Step-4 STOP-check clean (no residual A1 amendment). +- revert.11 (correctness gate): 1ff7e81 ref compiler built in + throwaway worktree; 164-fixture check/run oracle captured; + post-revert compiler diffed byte-for-byte — fail=0, ZERO DRIFT, + behaviour PRISTINE. cargo test --workspace 600/0. Residual + it.1/it.2 production-surface grep clean. Worktree removed; main + HEAD never moved. + +## Concerns + +- revert.3: the plan's Task-3 file-map enumerated the guardedness + helpers + call site but did NOT explicitly list the `module_fns` + signature threading through check_module/check_def/check_fn. The + `1ff7e81` oracle unambiguously proved that threading it.2-net-new; + leaving it would have been dead it.2 surface referencing deleted + helpers. Resolved correctly via the plan's own "Oracle convention" + + "re-locate by symbol name, oracle is authority on every byte" + mandate + the spec §Data-flow ("restored to pure pre-it.1 role"). + This is the recon-map-drifts-but-oracle-is-authority mechanism + working as designed, not a plan defect — no bounce. Flagged so the + Boss is aware the plan file-map under-enumerated one signature + edge; the end-state is verified correct (lib.rs byte-identical to + oracle). +- revert.9: the plan's Task-9 Step-6 single-line grep heuristic + (`grep -c 'clauses 1 and 2 yet fail clause 3' ...`) returned 0 + because the verbatim-applied replacement text line-wraps ("yet + fail\n clause 3"). The substantive acceptance criterion + (clause-3 block retained, only de-claimed) is positively verified + multiline + by the intact `## Feature-acceptance criterion` section + and "criterion 3 is the discriminator" sentence. Not a defect; + flagged so the Boss does not misread the heuristic. + +## Known debt + +(none — the revert is byte-pristine against `1ff7e81` for all +production surface; behaviour is byte-identical over the surviving +corpus.) + +## Blocked detail + +(none — DONE.) + +## Files touched + +90 working-tree paths (Boss commits all as one cohesive revert iter): + +- Deleted (59): `crates/ailang-check/tests/loop_recur_pin.rs`, + `crates/ailang-check/tests/structural_recursion_pin.rs`; 16 it.1/it.2 + fixtures under `examples/` (loop_*.ail, struct_rec_*.ail, + test_recur_*.ail.json, test_loop_missing_diverge / test_mutual_cross_family + / test_non_structural_recursion .ail.json); `bench/it3-oracle/` + (MANIFEST.tsv + 40 .out). +- Modified — source revert to 1ff7e81 (byte-identical): + `crates/ailang-core/src/ast.rs`, `desugar.rs`, `workspace.rs`; + `crates/ailang-check/src/lib.rs`, `lift.rs`, `mono.rs`, + `linearity.rs`, `uniqueness.rs`, `reuse_shape.rs`, + `pre_desugar_validation.rs`, `builtins.rs`; + `crates/ailang-codegen/src/lib.rs`, `escape.rs`, `lambda.rs`; + `crates/ail/src/main.rs`; `crates/ailang-surface/src/parse.rs`, + `print.rs`; `crates/ailang-prose/src/lib.rs`; + `crates/ailang-core/specs/form_a.md`. +- Modified — tests revert to 1ff7e81 (byte-identical): + `crates/ailang-core/tests/spec_drift.rs`, `schema_coverage.rs`, + `carve_out_inventory.rs`; `crates/ail/tests/e2e.rs`, + `codegen_import_map_fallback_pin.rs`. +- Modified — net-add / hunk-edit: + `crates/ailang-core/tests/design_schema_drift.rs` (loop/recur + anchors removed + new doc-presence test added), + `docs/DESIGN.md` (Decision 3 placeholder + clause-3 de-claim + + F1/F4 note; hunk-edited, clause 3 kept), `docs/roadmap.md` + (Iteration-discipline block removed, deferred P2 entry added), + `docs/specs/2026-05-15-iteration-discipline.md` (superseded + header), `skills/brainstorm/SKILL.md` (worked-example de-claim). +- Modified — fixtures restored to 1ff7e81: + `examples/rc_pin_recurse_implicit.ail`, + `examples/rc_let_alias_implicit_param.ail`. +- KEPT (no-op, Boss decision): + `bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json`. + +E2E coverage: none (revert iteration — the Task-11 behavioural- +equivalence sweep over all 164 surviving fixtures is a stronger +correctness proof than new E2E; the doc-presence test guards the +only net-new artefact). + +## Stats + +bench/orchestrator-stats/2026-05-16-iter-revert.json diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index d81a606..c5f2a02 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -78,3 +78,4 @@ - 2026-05-15 — iter it.1: iteration-discipline milestone (1 of 3) — `Term::Loop` / `Term::Recur` / `LoopBinder` added as strictly-additive first-class AST nodes end-to-end: Form-A `parse_loop`/`parse_recur` + print + prose render/free-var/subst lockstep + canonical-JSON serde/round-trip + schema/spec-drift/schema-coverage/carve-out lockstep (13→17) + typecheck (binder typing + recur arity/type unification via `loop_stack: &mut Vec>` threaded exactly as mut.2's `mut_scope_stack`; recur-tail-position via a new private `verify_loop_body`, `verify_tail_positions` public signature unchanged) + codegen (loop-header block, one phi per binder, recur back-edge `br` with a NEW parallel `block_terminated` setter, lambda-boundary `loop_frames` save/restore mirroring mut.3). Four new `CheckError` variants `Recur{OutsideLoop,ArityMismatch,TypeMismatch,NotInTailPosition}` (bracket-`[code]`-free Display per the F2 convention). Strictly additive verified — zero deletions touch `tail-app`/`tail-do`, `verify_tail_positions`' tail-app role, or the seven existing codegen `block_terminated` sites (the 32 within-iter deletions are exclusively DD-3 stub-then-fill replacements). `Term::Recur` synth returns a fresh metavar (resolves the plan's flagged `Type::unit()` open risk: recur appears in `if` branches that must unify with the sibling type). `loop_counter.ail`→`55`, `loop_in_lambda_e2e.ail`→`49`, four negatives fire exact codes, `tail-app` fixtures byte-identical, zero IR/prose snapshot drift; `cargo test --workspace` green. Two mut.1-class plan-pseudo-vs-reality substitutions recorded (prose round-trip asserting AST-equality is impossible — no Form-B parser by design; the diagnostic.rs doc-list premise was false) → 2026-05-15-iter-it.1.md - 2026-05-15 — iter it.2: iteration-discipline milestone (2 of 3) — structural-recursion guardedness checker + first real `Diverge` effect, strictly additive (nothing `tail`-related removed; that is it.3). New whole-body pass `verify_structural_recursion` runs as a sibling of `verify_tail_positions` in `check_fn`'s post-synth region (DD-1): the `smaller`-set algorithm with implicit candidate-position inference + unconstrained accumulator positions (DD-2 — foldl-shape accumulator classifies as structural recursion, pure+total), self/mutual identification with an inline ADT-family connected-components union-find (DD-3), and the it.2-only `tail==false` grandfather. `CheckError::NonStructuralRecursion {callee,arg}` (bracket-`[code]`-free Display per F2). `term_contains_loop` (stops at `Term::Lam` boundaries, DD-4) injects `"Diverge"` into the raised effect set so the existing `UndeclaredEffect` machinery enforces it with no new diagnostic variant; lam-arrow + `Term::LetRec` sub-effect sites wired (loop behind a lam edge carries `!Diverge` on the lam's arrow, propagating via the free callee-effect path, not leaking to the enclosing fn — exactly as `!IO` scopes). DESIGN.md Decision 3 + §Data-model hook synced present-tense. Four it.1 loop fixtures gained `!Diverge`. Two spec-premise boundary defects surfaced and resolved inside the task's invariants (corpus clean, check not weakened): (§1) the spec's "21 tail-app fixtures" grandfather premise under-counts the corpus — no-ADT-candidate counter recursions (~18, e.g. `build_tree(depth:Int)`) have no structural position to verify and are deferred to it.3 migration; (§2) two RC-regression fixtures (`rc_pin_recurse_implicit`, `rc_let_alias_implicit_param`) hold an ADT param constant while decrementing an Int — genuinely non-structural, joined the spec's transitional `tail-app` grandfather exactly as the other 20 corpus fixtures do (their RC==GC regression guards verified still green; the regression lives in the unchanged `pin`/`pin_aliased` bodies). Both recorded as corrected it.3 corpus-migration scope. `cargo test --workspace` 622 green / 0 red; all 9 acceptance pins non-vacuous (negatives `.contains(code)`); struct_rec_sum→15, loop_needs_diverge→55, the it.1 55/49 e2e still green → 2026-05-15-iter-it.2.md - 2026-05-15 — iter it.3 (BLOCKED, bounce-back): destructive terminal iteration of iteration-discipline. Task 1 (non-destructive: pre-migration oracle + the spec-delegated class-(b) live sweep) ran complete — 40 recursive corpus fixtures classified + oracled under `bench/it3-oracle/`; zero production code changed; HEAD clean at c992eb9. The mandated Task-1.3 sweep surfaced a **fundamental milestone-design flaw**, not a migration nuisance: 6 fixtures contain `build(d: Int) = if d==0 then Leaf else Node(1, build(d-1), build(d-1))` — a terminating, maximally-LLM-natural, **non-structural (Int param, no ADT-candidate) non-tail BRANCHING (double) recursion** that the milestone's totality dichotomy ("structural-over-ADT OR loop/recur, else error") makes **inexpressible**: not ADT-structural, and not `recur`-able (branching ≠ single tail back-edge). Post-it.3 it is a hard `NonStructuralRecursion` with no expressible alternative — the milestone as-specified would fail its own feature-acceptance criterion (clause 1: the LLM reaches for `build(d-1),build(d-1)`; clause 2: the milestone would *remove* expressivity). The orchestrator correctly refused a 4th plan-patch and bounced (`feedback_spec_over_plan_patches`). Boss verdict: the totality story overlooked a second canonical total-by-construction scheme — well-founded recursion on a strictly-decreasing non-negative Int measure. Resolution requires a new additive iteration **it.2b** (widen the it.2 guardedness checker to accept Int-bounded recursion incl. branching) BEFORE it.3 re-dispatches; the purity sub-fork (Int≠Nat: total only for non-negative entry) touches the user-co-designed purity pillar → user design decision, recommended option A1 (accept with a documented non-negative-entry obligation, analogous to array-bounds). Notify sent; loop stopped. The RC-RSS/18g.1 load-bearing risk (it.3 Task 5.5/5b) was NOT reached and must NOT be treated as resolved by the milestone-close audit → 2026-05-15-iter-it.3.md +- 2026-05-16 — iter revert: Iteration-discipline milestone (it.1 `96db54d` + it.2 `a4be1e5`) fully backed out by one **forward** iteration (`main` sacrosanct — never rewound; `1ff7e81`, the pre-`9973546` commit, is the per-region byte oracle). Root cause: the milestone was an over-escalation of fieldtest finding F1 (a `[friction]` item whose own minimal recommendation was a DESIGN.md note); its totality dichotomy made the maximally-LLM-natural `build(d:Int)=Node(1,build(d-1),build(d-1))` inexpressible (it.3 BLOCKED), and the only in-thesis escape (A1/it.2b) conceded the language's first documented-unenforced totality precondition — a purity-pillar dilution the user rejected. `Term::Loop`/`Term::Recur`/`LoopBinder`, the `verify_structural_recursion` guardedness pass + `term_contains_loop` + `Diverge`-injection + the transitively-it.2 `module_fns` plumbing, the five `Recur*`/`NonStructuralRecursion` `CheckError` variants (+ `code()` + 3 dedicated `ctx()` arms), the it.1 codegen loop-header/phi/back-edge + parallel `block_terminated` setter, and all walker arms are removed — `crates/ailang-check/src/lib.rs` and every reverted source/test file byte-identical to `1ff7e81`. Surgical keeps: feature-acceptance **clause 3** (DESIGN.md + brainstorm SKILL.md, worked example de-claimed "shipped"→hypothetical) and the F3 P2 todo. Sole net addition: an honest F1/F4 documented-idiom note (tail-recursive accumulator fallback; `examples/mut_counter.ail`) guarded by a doc-presence test. 16 it.1/it.2 fixtures + 2 pin files + `bench/it3-oracle/` deleted; 2 RC fixtures restored to `1ff7e81`; `bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json` kept (historical record). Roadmap: Iteration-discipline block + blocking-fork section removed; the genuine total-Int-recursion ambition preserved as a deferred P2 milestone sequenced behind a future `Nat`/refinement-types milestone (not abandoned — correctly sequenced). Correctness gate PRISTINE: 164 surviving `1ff7e81`-era fixtures `ail check`/`ail run` byte-identical to pre-milestone behaviour (1ff7e81 worktree reference compiler, zero drift); `cargo test --workspace` 600/0; zero residual it.1/it.2 production surface. The old it.* journals/plans + the superseded-headered `2026-05-15-iteration-discipline.md` stay as historical record → 2026-05-16-iter-revert.md diff --git a/docs/roadmap.md b/docs/roadmap.md index e1c093f..0c18a4c 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -40,143 +40,6 @@ clean. Pick the next milestone from P2.)_ ## P1 — Next -- [~] **\[milestone\]** Iteration discipline — structural recursion + - named `loop`/`recur`; recursion-by-call restricted; `tail-app` - retired. Spec `docs/specs/2026-05-15-iteration-discipline.md` - (approved fda9b78; scope-corrected 2018178/10a0595). **Status - 2026-05-15: it.1 SHIPPED (96db54d — loop/recur additive), it.2 - SHIPPED (a4be1e5 — guardedness checker + first real Diverge - effect), it.3 BLOCKED on a surfaced fundamental design fork (see - "The blocking fork" below — needs a user design decision + a new - iteration it.2b before it.3 can re-dispatch).** The iteration - story of the language, decided in principle 2026-05-15. Two - constructs survive, one is removed: - - **Structural recursion stays — and becomes total-by-construction.** - A recursive call is permitted iff it is structurally guarded: - each recursive call is on a constructor-smaller component of an - algebraic argument. Decision 10 already guarantees ADTs are - acyclic, so a structurally-guarded recursion terminates *by the - invariant the language already holds* — permitting it costs - nothing on the provability pillar and it stays locally checkable. - This is the most LLM-natural correct pattern (tree / AST / JSON / - list `match`-and-recurse, saturated in every FP corpus) and must - not be amputated. - - **All other repetition must go through a named `(loop ...)` head + - `recur`.** `recur` is the single explicit backward jump; it - targets a lexically-enclosing named loop, never an implicit fn - head (Clojure permits the implicit form — AILang does not, for - the same no-outward-inference reason that motivated explicit - `tail-app`). Accumulator loops, counted iteration, streaming, - state machines — none are structurally decreasing, so all are - forced into the explicit named-loop form. - - **`tail-app` is retired.** `Term::App { tail: bool }` and the - `musttail`-lowering surface go away: a call is either structural - recursion (a plain call, checked total) or it is `loop`/`recur` - (the only loop). No marked-tail-call concept survives. - - **Motivation.** Discharges fieldtest finding F1 — the most - consequential mut-local finding: mut-local's own motivation - ("removes friction from accumulators that today need tail-recursive - helpers") was structurally unmet, because without a loop the only - iteration mechanism remained the very tail-rec helper. `loop`/`recur` - closes that honestly without introducing an imperative construct - (it is pure: no mutable loop variable, no effect, composes into pure - contexts freely). It also closes the residual "forgot to mark tail" - trap *completely* — a recursive call that is not structurally - guarded is a compile error that names itself, not a silent - stack-overflow. And it unifies with Decision 10: acyclic values - *and* an acyclic implicit call graph; the only cycles anywhere in a - program are explicit, named, typed `loop` points. Both surviving - constructs pass all three feature-acceptance clauses including the - 2026-05-15 clause 3 (structural recursion and named loop/recur are - LLM-natural *and* their bug class is closed by construction; a bare - `while` is exactly what clause 3 rejects). - - **Original open spec questions — RESOLVED in it.2 (a4be1e5).** - (1) *mutual* structural recursion → the conservative same-ADT-family - rule (connected-components union-find over the type-reference - graph; admits tree/forest, even/odd-over-Nat, mutual JSON; a - general size-measure ordering stays out of scope). (2) the - `foldl`-shaped accumulator-carrying structural walk → **counts as - structural recursion** (plain, pure, total — only the structural - argument must decrease; accumulator positions are unconstrained). - Both shipped and pinned. - - **The blocking fork (it.3-surfaced 2026-05-15 — needs a USER - design decision; touches the purity pillar the user co-designed).** - The milestone's totality thesis recognised exactly ONE - total-by-construction recursion scheme: structural-over-an-acyclic- - ADT (Decision 10). The it.3 mandated corpus sweep proved this is - *incomplete*. Six corpus fixtures contain the single most - LLM-natural tree-builder shape: - `build(d: Int) = if d==0 then Leaf else Node(1, build(d-1), build(d-1))`. - It is provably terminating, but: **not** ADT-structural (`d` is - `Int`, no constructor-smaller component) and **not** `loop`/`recur`- - able (it is *branching/double* recursion; `recur` is a single - tail-position back-edge — a balanced-tree build is not a tail - loop; the only `loop` form is a hand-rolled explicit-stack - worklist, which no LLM writes). So the milestone *as-specified* - makes a trivially-total, maximally-natural function - **inexpressible** — failing its own feature-acceptance criterion - (clause 1: the LLM reaches for `build(d-1),build(d-1)`; clause 2: - the milestone would *remove* expressivity). This is a real - design-thesis gap, not a migration nuisance: there is a SECOND - canonical total-by-construction scheme the design overlooked — - **well-founded recursion on a strictly-decreasing non-negative - integer measure** (`f(0)=base; f(n)=…f(n-1)…`, branching allowed). - - **Decision the user must make** (it trades against the purity - pillar — Int ≠ ℕ; AILang has no `Nat`/refinement types, so - Int-bounded recursion is total only for *non-negative entry*): - - **A1 (RECOMMENDED).** Make the totality story a *trichotomy*: - ADT-structural | Int-bounded-well-founded | explicit `loop`/`recur`. - Accept Int-bounded recursion (recursive call on `p - ` - with a non-recursing base guard, branching allowed) as a - *second total-by-construction class*, with one documented - obligation: non-negative entry (a negative seed diverges — the - same precondition class as array-bounds the language already - lives with). Restores the entire `f(n-1)` recursion family (the - second-most-common shape in any corpus); keeps all 6 fixtures - verbatim; the trichotomy is *more* complete, not less principled. - Rationale is the language's own gate: a milestone that makes - `build(d)` inexpressible cannot pass the feature-acceptance - criterion. *Why this is a user call:* it concedes "total by - construction, sign nothing" → "total by construction modulo one - documented non-negative-entry obligation" — a dilution of a - purity pillar the user personally weighted in the original - Socratic design dialogue. - - **A2.** Introduce a `Nat` type; accept Int-bounded recursion - only on `Nat` — preserves zero-precondition purity, but `Nat` - is its own sub-milestone and an LLM writes `depth: Int` unless - the prelude makes `Nat` the natural default (clause-1 friction). - - **A3 / B / C (not recommended).** Strict-dichotomy + - explicit-worklist (fails clause 1 — no LLM hand-rolls a stack - for tree-build); a narrow carve-out predicate (the patch smell); - reshaping the LLM-natural fixtures (forbidden — - `feedback_dont_adapt_tests_to_bugs`). - - **If A1 (or A2): new iteration it.2b** — additive widening of the - it.2 guardedness checker to also accept Int-bounded (incl. - branching) recursion as total; no removal. After it.2b the 6 - fixtures check clean with zero migration; it.3 then re-dispatches - from c992eb9 (the `bench/it3-oracle/` 40-fixture behavioural - oracle is preserved and reused; nothing in it.3 was destructive). - The it.3 RC-RSS/18g.1 load-bearing risk (Task 5.5/5b) is still - UNTESTED — must not be treated as resolved by the milestone-close - audit. - - **Relation to Stateful islands.** This entry owns the iteration - story and *supersedes* the "while-loops legal" scope bullet of the - Stateful-islands milestone below. The genuinely-escaping - mutable-state path (`ref a` / `MutArray a` / `Stateful a b` / - `pipe`) is unaffected and stays in Stateful-islands. - - - context: spec `docs/specs/2026-05-15-iteration-discipline.md`; - per-iter journals 2026-05-15-iter-it.1 (shipped), -it.2 - (shipped), -it.3 (BLOCKED — the design fork above). Next action - is a USER decision on the blocking fork (A1 recommended), then - iteration it.2b, then it.3 re-dispatch from c992eb9. - - [x] **\[milestone\]** Heap-`Str` ABI — runtime infrastructure for malloc-backed, refcounted `Str` values alongside the existing static `@.str_*` globals. Today the `Str` path is static-only @@ -213,6 +76,23 @@ clean. Pick the next milestone from P2.)_ ## P2 — Medium-term +- [ ] **\[milestone\]** Iteration-totality story — structural + + Int-bounded total recursion with *enforced* non-negativity. + AILang's iteration story stays as-is (structural / tail recursion; + `tail-app` intact). The genuine ambition — make `f(n-1)`-family + recursion (incl. branching tree builders) total *by construction* + with the non-negative-entry precondition **enforced**, not merely + documented — is deferred here because doing it without a purity- + pillar concession requires refinement/`Nat` type machinery the + language has not built (Decision 4 keeps refinements opaque, no + SMT). Not abandoned; correctly sequenced after the type machinery. + - depends on: a future `Nat`/refinement-types milestone (no spec + yet). + - context: `docs/specs/2026-05-16-iteration-discipline-revert.md` + (why the 2026-05 attempt was reverted) and + `docs/journals/2026-05-15-iter-it.3.md` (the branching-builder + counter-example that surfaced the gap). + - [x] **\[milestone\]** Retire `io/print_int` / `io/print_bool` / `io/print_float` effect-ops + migrate example corpus to `print`. Shipped 2026-05-14 as iter rpe.1. diff --git a/docs/specs/2026-05-15-iteration-discipline.md b/docs/specs/2026-05-15-iteration-discipline.md index e039d17..da904c0 100644 --- a/docs/specs/2026-05-15-iteration-discipline.md +++ b/docs/specs/2026-05-15-iteration-discipline.md @@ -1,3 +1,11 @@ +> **SUPERSEDED 2026-05-16 by +> `docs/specs/2026-05-16-iteration-discipline-revert.md`.** This +> milestone was reverted in full (it.1 + it.2 backed out forward; +> it.3 never ran). It is retained as a historical record of the +> attempt and the design-thesis gap it surfaced; it is **not** the +> current iteration-story design. Do not plan or implement from this +> file. + # Iteration discipline — Design Spec **Date:** 2026-05-15 diff --git a/examples/loop_counter.ail b/examples/loop_counter.ail deleted file mode 100644 index 6dabf37..0000000 --- a/examples/loop_counter.ail +++ /dev/null @@ -1,12 +0,0 @@ -(module loop_counter - - (fn main - (doc "Iter it.1 — sum 1..10 via an accumulator loop. Iter it.2: loop-bearing ⇒ !Diverge added (D2). Expected stdout: 55.") - (type (fn-type (params) (ret (con Unit)) (effects IO Diverge))) - (params) - (body - (app print - (loop ((var acc (con Int) 0) (var i (con Int) 1)) - (if (app > i 10) - acc - (recur (app + acc i) (app + i 1)))))))) diff --git a/examples/loop_in_lambda_e2e.ail b/examples/loop_in_lambda_e2e.ail deleted file mode 100644 index 369f6e8..0000000 --- a/examples/loop_in_lambda_e2e.ail +++ /dev/null @@ -1,30 +0,0 @@ -(module loop_in_lambda_e2e - - (fn apply - (doc "apply a fn-of-Int to an Int. Iter it.2: the supplied closure is loop-bearing, so its arrow carries !Diverge — the higher-order param type and apply's own effect row must reflect that (effects are part of the function type).") - (type (fn-type (params (fn-type (params (con Int)) (ret (con Int)) (effects Diverge)) (con Int)) (ret (con Int)) (effects Diverge))) - (params f x) - (body (app f x))) - - (fn main - (doc "Iter it.1 — a loop inside a lambda body, invoked via a closure. The lambda computes x*x by summing x exactly x times through an accumulator loop; apply 7 prints 49. Codegen-soundness gate for the lambda-boundary loop_frames save/restore. Iter it.2: !Diverge propagates out through apply (callee-effect propagation).") - (type (fn-type (params) (ret (con Unit)) (effects IO Diverge))) - (params) - (body - (app print - (app apply - ; Iter it.2: the loop lives in THIS lambda's body, so the - ; lambda's arrow carries !Diverge (DD-4 lam boundary). The - ; loop does not leak Diverge to `main` — `main`'s body does - ; not syntactically contain the loop (it stops at the lam - ; edge, exactly as !IO does). - (lam - (params (typed x (con Int))) - (ret (con Int)) - (effects Diverge) - (body - (loop ((var acc (con Int) 0) (var k (con Int) 0)) - (if (app == k x) - acc - (recur (app + acc x) (app + k 1)))))) - 7))))) diff --git a/examples/loop_needs_diverge.ail b/examples/loop_needs_diverge.ail deleted file mode 100644 index 22317b3..0000000 --- a/examples/loop_needs_diverge.ail +++ /dev/null @@ -1,18 +0,0 @@ -; Iter it.2 positive (DD-4 / D2): a fn whose body contains a -; `(loop …)` must declare `!Diverge`. This one does — its effect row -; carries `Diverge` (and `IO`, since it `print`s the result), so the -; existing declared-vs-raised reconciliation accepts it. Modelled on -; `loop_counter.ail` (it.1) with `Diverge` added to the effect row. - -(module loop_needs_diverge - - (fn main - (doc "Sum 1..10 via an accumulator loop; loop-bearing ⇒ !Diverge. Expected stdout: 55.") - (type (fn-type (params) (ret (con Unit)) (effects IO Diverge))) - (params) - (body - (app print - (loop ((var acc (con Int) 0) (var i (con Int) 1)) - (if (app > i 10) - acc - (recur (app + acc i) (app + i 1)))))))) diff --git a/examples/loop_nested_in_lambda.ail b/examples/loop_nested_in_lambda.ail deleted file mode 100644 index 6a77411..0000000 --- a/examples/loop_nested_in_lambda.ail +++ /dev/null @@ -1,16 +0,0 @@ -(module loop_nested_in_lambda - - (fn make_adder - (doc "Iter it.1 — a loop inside a lambda body (lambda-boundary analogue). Iter it.2: the returned closure is loop-bearing, so its arrow carries !Diverge (DD-4 lam boundary); make_adder's return type reflects that. make_adder's own body does not contain the loop (it stops at the lam edge), so make_adder itself stays effect-free.") - (type (fn-type (params (con Int)) (ret (fn-type (params (con Int)) (ret (con Int)) (effects Diverge))))) - (params base) - (body - (lam - (params (typed x (con Int))) - (ret (con Int)) - (effects Diverge) - (body - (loop ((var acc (con Int) base) (var k (con Int) 0)) - (if (app == k x) - acc - (recur (app + acc 1) (app + k 1))))))))) diff --git a/examples/loop_smoke.ail b/examples/loop_smoke.ail deleted file mode 100644 index 832fdc2..0000000 --- a/examples/loop_smoke.ail +++ /dev/null @@ -1,11 +0,0 @@ -(module loop_smoke - - (fn count_to - (doc "Iter it.1 — single counted loop; counts i up to n and returns n. Iter it.2: loop-bearing ⇒ !Diverge (D2).") - (type (fn-type (params (con Int)) (ret (con Int)) (effects Diverge))) - (params n) - (body - (loop ((var i (con Int) 0)) - (if (app == i n) - i - (recur (app + i 1))))))) diff --git a/examples/rc_let_alias_implicit_param.ail b/examples/rc_let_alias_implicit_param.ail index 20ec358..56a3e10 100644 --- a/examples/rc_let_alias_implicit_param.ail +++ b/examples/rc_let_alias_implicit_param.ail @@ -59,14 +59,6 @@ (case (pat-ctor TLeaf) 0) (case (pat-ctor TNode v l r) 1))))) - ; Iter it.2: integer-counter recursion holding the ADT param `t` - ; constant — non-structural by the it.2 guardedness check (D2). The - ; recursive call is in tail position, so it joins the transitional - ; `tail-app` grandfather (spec it.2 "Transitional grandfather") as - ; the rest of the corpus does until it.3 migrates such recursions - ; to `(loop …)`. The 18g let-alias-mode regression this fixture - ; guards lives in `pin_aliased`'s match arm-close, unaffected by - ; this tail marking. (fn loop (type (fn-type @@ -77,7 +69,7 @@ (if (app == n 0) 0 (let _v (app pin_aliased t) - (tail-app loop (app - n 1) t))))) + (app loop (app - n 1) t))))) (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) diff --git a/examples/rc_pin_recurse_implicit.ail b/examples/rc_pin_recurse_implicit.ail index 7044c1a..15f84cc 100644 --- a/examples/rc_pin_recurse_implicit.ail +++ b/examples/rc_pin_recurse_implicit.ail @@ -38,14 +38,6 @@ (case (pat-ctor TLeaf) 0) (case (pat-ctor TNode v l r) 1)))) - ; Iter it.2: this is integer-counter recursion holding the ADT - ; param `t` constant — non-structural by the it.2 guardedness - ; check (D2). The recursive call is in tail position, so it joins - ; the transitional `tail-app` grandfather (spec it.2 "Transitional - ; grandfather") exactly as the rest of the corpus does until it.3 - ; migrates such recursions to `(loop …)`. The 18d.4 regression this - ; fixture guards lives in `pin`'s match arm-close, unaffected by - ; this tail marking. (fn loop (type (fn-type (params (con Int) (con Tree)) (ret (con Int)))) (params n t) @@ -53,7 +45,7 @@ (if (app == n 0) 0 (let _v (app pin t) - (tail-app loop (app - n 1) t))))) + (app loop (app - n 1) t))))) (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) diff --git a/examples/struct_rec_foldl_sum.ail b/examples/struct_rec_foldl_sum.ail deleted file mode 100644 index fd7dfa8..0000000 --- a/examples/struct_rec_foldl_sum.ail +++ /dev/null @@ -1,26 +0,0 @@ -; Iter it.2 positive (spec D1): foldl-shape accumulator. `go` recurses -; on the Cons-tail `t` at position 0 (structurally guarded) while -; threading an unconstrained accumulator `acc` at position 1. The -; accumulator position is never examined by the guardedness check, so -; this classifies as structural recursion: pure, total, Diverge-free, -; with NO `tail-app` marker. This is the single most LLM-natural -; iteration shape and must stay structural (spec D1). - -(module struct_rec_foldl_sum - - (data IntList - (ctor INil) - (ctor ICons (con Int) (con IntList))) - - (fn go - (doc "Sum via a foldl-shape accumulator; structural on the tail.") - (type - (fn-type - (params (con IntList) (con Int)) - (ret (con Int)))) - (params xs acc) - (body - (match xs - (case (pat-ctor INil) acc) - (case (pat-ctor ICons h t) - (app go t (app + acc h))))))) diff --git a/examples/struct_rec_list_len.ail b/examples/struct_rec_list_len.ail deleted file mode 100644 index 99caff8..0000000 --- a/examples/struct_rec_list_len.ail +++ /dev/null @@ -1,24 +0,0 @@ -; Iter it.2 positive: structural list length. `len` recurses on the -; Cons-tail `t` (a constructor sub-component of `xs`) via a plain, -; non-tail `(app len t)`. Structurally guarded at position 0, pure, -; total, Diverge-free. No `tail-app` marker — this is the structural -; recursion form the it.2 guardedness check must accept on its own. - -(module struct_rec_list_len - - (data IntList - (ctor INil) - (ctor ICons (con Int) (con IntList))) - - (fn len - (doc "Length of an IntList via structural recursion on the tail.") - (type - (fn-type - (params (con IntList)) - (ret (con Int)))) - (params xs) - (body - (match xs - (case (pat-ctor INil) 0) - (case (pat-ctor ICons h t) - (app + 1 (app len t))))))) diff --git a/examples/struct_rec_sum_e2e.ail b/examples/struct_rec_sum_e2e.ail deleted file mode 100644 index 94ea5fb..0000000 --- a/examples/struct_rec_sum_e2e.ail +++ /dev/null @@ -1,41 +0,0 @@ -; Iter it.2 Phase-3 e2e: an it.2-clean structural recursion that -; actually RUNS. `sum` recurses on the Cons-tail `t` via a plain, -; non-tail `(app sum t)` — structurally guarded ⇒ the it.2 check -; classifies it pure + total, so it carries NO `!Diverge` and uses -; NO `tail-app` marker. This proves the structural-recursion -; classification is behaviourally sound end-to-end (the "total" -; verdict is not just a typecheck assertion): build [1,2,3,4,5], -; sum it structurally, print 15. - -(module struct_rec_sum_e2e - - (data IntList - (ctor INil) - (ctor ICons (con Int) (con IntList))) - - (fn sum - (doc "Structural sum: plain non-tail recursion on the Cons tail. No !Diverge, no tail-app.") - (type - (fn-type - (params (con IntList)) - (ret (con Int)))) - (params xs) - (body - (match xs - (case (pat-ctor INil) 0) - (case (pat-ctor ICons h t) - (app + h (app sum t)))))) - - (fn main - (doc "Build [1,2,3,4,5] and print its structural sum. Expected stdout: 15.") - (type (fn-type (params) (ret (con Unit)) (effects IO))) - (params) - (body - (app print - (app sum - (term-ctor IntList ICons 1 - (term-ctor IntList ICons 2 - (term-ctor IntList ICons 3 - (term-ctor IntList ICons 4 - (term-ctor IntList ICons 5 - (term-ctor IntList INil))))))))))) diff --git a/examples/struct_rec_tree_forest.ail b/examples/struct_rec_tree_forest.ail deleted file mode 100644 index 7d67052..0000000 --- a/examples/struct_rec_tree_forest.ail +++ /dev/null @@ -1,43 +0,0 @@ -; Iter it.2 positive (spec D1, DD-3): mutual structural recursion -; over one ADT family. `Tree` references `Forest` (the `Node` field) -; and `Forest` references `Tree` and `Forest` (the `Cons` fields), so -; the union-find of the ADT type-reference graph puts {Tree, Forest} -; in a single connected component. `tree_size` recurses into -; `forest_size` on the `Node`-bound `f` (structurally smaller); each -; `forest_size` self/cross call passes a `Cons`-bound sub-component. -; The whole mutual group is structural: pure, total, Diverge-free, -; no `tail-app` markers. - -(module struct_rec_tree_forest - - (data Tree - (ctor Node (con Int) (con Forest))) - - (data Forest - (ctor FNil) - (ctor FCons (con Tree) (con Forest))) - - (fn tree_size - (doc "Node count of a tree; recurses into forest_size on the Node forest.") - (type - (fn-type - (params (con Tree)) - (ret (con Int)))) - (params tr) - (body - (match tr - (case (pat-ctor Node v f) - (app + 1 (app forest_size f)))))) - - (fn forest_size - (doc "Node count of a forest; mutual with tree_size, self on the tail.") - (type - (fn-type - (params (con Forest)) - (ret (con Int)))) - (params fo) - (body - (match fo - (case (pat-ctor FNil) 0) - (case (pat-ctor FCons t rest) - (app + (app tree_size t) (app forest_size rest))))))) diff --git a/examples/test_loop_missing_diverge.ail.json b/examples/test_loop_missing_diverge.ail.json deleted file mode 100644 index 82ecbf4..0000000 --- a/examples/test_loop_missing_diverge.ail.json +++ /dev/null @@ -1 +0,0 @@ -{"defs":[{"body":{"args":[{"binders":[{"init":{"lit":{"kind":"int","value":0},"t":"lit"},"name":"acc","type":{"k":"con","name":"Int"}},{"init":{"lit":{"kind":"int","value":1},"t":"lit"},"name":"i","type":{"k":"con","name":"Int"}}],"body":{"cond":{"args":[{"name":"i","t":"var"},{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":">","t":"var"},"t":"app"},"else":{"args":[{"args":[{"name":"acc","t":"var"},{"name":"i","t":"var"}],"fn":{"name":"+","t":"var"},"t":"app"},{"args":[{"name":"i","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"}],"t":"recur"},"t":"if","then":{"name":"acc","t":"var"}},"t":"loop"}],"fn":{"name":"print","t":"var"},"t":"app"},"doc":"Loop-bearing fn that omits !Diverge from its effect row — must fire undeclared-effect.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"test_loop_missing_diverge","schema":"ailang/v0"} diff --git a/examples/test_mutual_cross_family.ail.json b/examples/test_mutual_cross_family.ail.json deleted file mode 100644 index 70a0b76..0000000 --- a/examples/test_mutual_cross_family.ail.json +++ /dev/null @@ -1 +0,0 @@ -{"defs":[{"ctors":[{"fields":[],"name":"LNil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"MyList"}],"name":"LCons"}],"kind":"type","name":"MyList"},{"ctors":[{"fields":[],"name":"TLeaf"},{"fields":[{"k":"con","name":"MyTree"},{"k":"con","name":"MyTree"}],"name":"TBranch"}],"kind":"type","name":"MyTree"},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"LNil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"args":[{"name":"t","t":"var"}],"fn":{"name":"mk_tree","t":"var"},"t":"app"}],"fn":{"name":"g","t":"var"},"t":"app"}],"fn":{"name":"+","t":"var"},"t":"app"},"pat":{"ctor":"LCons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"f recurses into g passing a List sub-component, but g's structural param is an unrelated Tree family.","kind":"fn","name":"f","params":["xs"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"MyList"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[],"ctor":"TLeaf","t":"ctor","type":"MyTree"},"kind":"fn","name":"mk_tree","params":["xs"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"MyList"}],"ret":{"k":"con","name":"MyTree"}}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"TLeaf","fields":[],"p":"ctor"}},{"body":{"args":[{"args":[{"name":"l","t":"var"}],"fn":{"name":"g","t":"var"},"t":"app"},{"args":[{"args":[],"ctor":"LNil","t":"ctor","type":"MyList"}],"fn":{"name":"f","t":"var"},"t":"app"}],"fn":{"name":"+","t":"var"},"t":"app"},"pat":{"ctor":"TBranch","fields":[{"name":"l","p":"var"},{"name":"r","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"tr","t":"var"},"t":"match"},"doc":"g recurses into f, but its own structural param is a Tree (different ADT family).","kind":"fn","name":"g","params":["tr"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"MyTree"}],"ret":{"k":"con","name":"Int"}}}],"imports":[],"name":"test_mutual_cross_family","schema":"ailang/v0"} diff --git a/examples/test_non_structural_recursion.ail.json b/examples/test_non_structural_recursion.ail.json deleted file mode 100644 index bb3d534..0000000 --- a/examples/test_non_structural_recursion.ail.json +++ /dev/null @@ -1 +0,0 @@ -{"defs":[{"ctors":[{"fields":[],"name":"INil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"ICons"}],"kind":"type","name":"IntList"},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"INil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"name":"xs","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"}],"fn":{"name":"+","t":"var"},"t":"app"},"pat":{"ctor":"ICons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Non-structural: recurses on the SAME xs, not a sub-component. Not tail-marked.","kind":"fn","name":"f","params":["xs"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Int"}}}],"imports":[],"name":"test_non_structural_recursion","schema":"ailang/v0"} diff --git a/examples/test_recur_arity_mismatch.ail.json b/examples/test_recur_arity_mismatch.ail.json deleted file mode 100644 index 603dbb8..0000000 --- a/examples/test_recur_arity_mismatch.ail.json +++ /dev/null @@ -1,60 +0,0 @@ -{ - "schema": "ailang/v0", - "name": "test_recur_arity_mismatch", - "imports": [], - "defs": [ - { - "kind": "fn", - "name": "main", - "type": { - "k": "fn", - "params": [], - "ret": { - "k": "con", - "name": "Int" - }, - "effects": [] - }, - "params": [], - "doc": "Iter it.1: recur passing 2 args to a 1-binder loop fires recur-arity-mismatch.", - "body": { - "t": "loop", - "binders": [ - { - "name": "i", - "type": { - "k": "con", - "name": "Int" - }, - "init": { - "t": "lit", - "lit": { - "kind": "int", - "value": 0 - } - } - } - ], - "body": { - "t": "recur", - "args": [ - { - "t": "lit", - "lit": { - "kind": "int", - "value": 1 - } - }, - { - "t": "lit", - "lit": { - "kind": "int", - "value": 2 - } - } - ] - } - } - } - ] -} diff --git a/examples/test_recur_not_in_tail_position.ail.json b/examples/test_recur_not_in_tail_position.ail.json deleted file mode 100644 index f41600e..0000000 --- a/examples/test_recur_not_in_tail_position.ail.json +++ /dev/null @@ -1,60 +0,0 @@ -{ - "schema": "ailang/v0", - "name": "test_recur_not_in_tail_position", - "imports": [], - "defs": [ - { - "kind": "fn", - "name": "main", - "type": { - "k": "fn", - "params": [], - "ret": { - "k": "con", - "name": "Int" - }, - "effects": [] - }, - "params": [], - "doc": "Iter it.1: recur in the lhs of a seq (non-tail) fires recur-not-in-tail-position.", - "body": { - "t": "loop", - "binders": [ - { - "name": "i", - "type": { - "k": "con", - "name": "Int" - }, - "init": { - "t": "lit", - "lit": { - "kind": "int", - "value": 0 - } - } - } - ], - "body": { - "t": "seq", - "lhs": { - "t": "recur", - "args": [ - { - "t": "var", - "name": "i" - } - ] - }, - "rhs": { - "t": "lit", - "lit": { - "kind": "int", - "value": 0 - } - } - } - } - } - ] -} diff --git a/examples/test_recur_outside_loop.ail.json b/examples/test_recur_outside_loop.ail.json deleted file mode 100644 index 63c27f2..0000000 --- a/examples/test_recur_outside_loop.ail.json +++ /dev/null @@ -1,34 +0,0 @@ -{ - "schema": "ailang/v0", - "name": "test_recur_outside_loop", - "imports": [], - "defs": [ - { - "kind": "fn", - "name": "main", - "type": { - "k": "fn", - "params": [], - "ret": { - "k": "con", - "name": "Int" - }, - "effects": [] - }, - "params": [], - "doc": "Iter it.1: a recur with no enclosing loop fires recur-outside-loop.", - "body": { - "t": "recur", - "args": [ - { - "t": "lit", - "lit": { - "kind": "int", - "value": 1 - } - } - ] - } - } - ] -} diff --git a/examples/test_recur_type_mismatch.ail.json b/examples/test_recur_type_mismatch.ail.json deleted file mode 100644 index 7b1c471..0000000 --- a/examples/test_recur_type_mismatch.ail.json +++ /dev/null @@ -1,53 +0,0 @@ -{ - "schema": "ailang/v0", - "name": "test_recur_type_mismatch", - "imports": [], - "defs": [ - { - "kind": "fn", - "name": "main", - "type": { - "k": "fn", - "params": [], - "ret": { - "k": "con", - "name": "Int" - }, - "effects": [] - }, - "params": [], - "doc": "Iter it.1: recur passing a Bool to an Int binder fires recur-type-mismatch.", - "body": { - "t": "loop", - "binders": [ - { - "name": "i", - "type": { - "k": "con", - "name": "Int" - }, - "init": { - "t": "lit", - "lit": { - "kind": "int", - "value": 0 - } - } - } - ], - "body": { - "t": "recur", - "args": [ - { - "t": "lit", - "lit": { - "kind": "bool", - "value": true - } - } - ] - } - } - } - ] -} diff --git a/skills/brainstorm/SKILL.md b/skills/brainstorm/SKILL.md index 40853f2..03de1c5 100644 --- a/skills/brainstorm/SKILL.md +++ b/skills/brainstorm/SKILL.md @@ -104,7 +104,7 @@ A feature ships only if all three hold: Aesthetic appeal does not count. Human ergonomics do not count. If the answer to any of the three is "I'm not sure", the feature is probably not ready. The full criterion (with the canonical worked -example — the iteration story) lives in `docs/DESIGN.md` +example — see the criterion text) lives in `docs/DESIGN.md` ("Feature-acceptance criterion"); this skill is the gate that applies it during spec writing.