From ee5807d73cb4455954c614bc2b90509761689265 Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 7 May 2026 20:05:45 +0200 Subject: [PATCH] =?UTF-8?q?Iter=2015h=20=E2=80=94=20std=5Flist=20extension?= =?UTF-8?q?:=20take,=20drop?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the two canonical prefix-slicing combinators to std_list. First fns in std_list to combine `if` + Int arithmetic + recursive ADT pattern in one body. take : forall a. (Int, List) -> List — first n elements (or all of xs if shorter than n). drop : forall a. (Int, List) -> List — list with first n elements removed (Nil if n >= length). Both use `(if (<= n 0) ...)` as the base-case guard since literal sub-patterns inside Ctor patterns aren't yet supported (queued as 16c — would let take/drop collapse the if into the match). examples/std_list_more_demo: builds [1, 2, 3, 4, 5] once and exercises take/drop at n=0, n=mid, n=overflow on each. Expected output 0, 3, 5, 5, 3, 0 (one per line). Tests: 95/95 (e2e went from 35 to 36). std_list grew from 10 to 12 combinators; total stdlib 5 modules / 29 combinators. No new compiler bug surfaced. Pre-existing std_list defs are byte-identical (verified via diff on .ailx and round-trip on .ail.json), so the five downstream importers (std_list_demo, std_list_stress, std_either_list, std_either_list_demo, list_map_poly) need no regeneration. --- crates/ail/tests/e2e.rs | 15 ++++++ docs/JOURNAL.md | 74 ++++++++++++++++++++++++++++ examples/std_list.ail.json | 2 +- examples/std_list.ailx | 34 ++++++++++++- examples/std_list_more_demo.ail.json | 1 + examples/std_list_more_demo.ailx | 32 ++++++++++++ 6 files changed, 156 insertions(+), 2 deletions(-) create mode 100644 examples/std_list_more_demo.ail.json create mode 100644 examples/std_list_more_demo.ailx diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index ddbcdb2..f1193f5 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -417,6 +417,21 @@ fn std_either_list_demo() { assert_eq!(lines, vec!["2", "3", "2", "3"]); } +/// Iter 15h: `std_list.take` and `std_list.drop` end-to-end. Both are +/// index-driven recursive ADT-pattern fns — the first `std_list` +/// combinators that pair `if (<= n 0)` Int-arithmetic guards with a +/// recursive Cons/Nil match. Property protected: the `if` base-case +/// guard wraps a `match` whose recursive arm bodies use `(- n 1)` and +/// re-enter through `app` — a shape no other `std_list` fn has so +/// far. Six checks pin all three boundary regimes (n=0, 0length) on each combinator. Expected stdout: 0, 3, 5, 5, 3, 0. +#[test] +fn std_list_more_demo() { + let stdout = build_and_run("std_list_more_demo.ail.json"); + let lines: Vec<&str> = stdout.lines().collect(); + assert_eq!(lines, vec!["0", "3", "5", "5", "3", "0"]); +} + /// Guards `ail diff`: a modified body changes the hash of `sum`, while /// `main` stays unchanged. Expects exit code 1, `changed` contains exactly /// `sum`, `unchanged` contains `main`, `added`/`removed` empty. diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index ba332c6..16902cb 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -3042,3 +3042,77 @@ not change observable behaviour for any prior fixture. **Queue update.** 15g-aux done. Unchanged: 16b (local recursive let), 16c (Lit-in-Ctor patterns), 17a (per-fn arena, gated on user discussion of memory management). + +--- + +## Iter 15h — std_list extension: take, drop + +**Goal.** Extend `std_list` with the two index-driven prefix +combinators `take` and `drop`. They are the first `std_list` fns to +combine `if` + Int arithmetic + recursive ADT pattern in a single +body — every previous `std_list` fn was either a fold/HOF +(fold_left, fold_right, length, map, filter, reverse) or a pure +match-on-Cons (head, tail, append, is_empty). 15h closes the +canonical-prefix-slicing gap and dogfoods the `if (<= n 0)` + +`(- n 1)` interaction inside a recursive Cons-pattern body. + +**What shipped.** + +- `examples/std_list.ailx` — `take` and `drop` appended after + `filter`. All ten pre-existing defs byte-identical (verified via + `cargo run -p ail -- check` on every downstream importer: + `std_list_demo`, `std_list_stress`, `std_either_list`, + `std_either_list_demo`, `list_map_poly`). Both new fns are + `forall (vars a). (Int, List) -> List`. `take` is + constructor-blocked recursive (`Cons h (take (n-1) t)`); `drop` + is direct recursive (the recursive call is the arm body, no + Cons wrap), so the `match` arm is in tail position relative to + the `if`'s `else` branch — but neither call site is marked + `tail-app` because the surrounding `if` is not the fn's + immediate body. Conservative; matches the rest of `std_list`'s + marking discipline. +- `examples/std_list_more_demo.ailx` — six prints exercising both + combinators at all three boundary regimes (n=0, 0length). Reuses `std_list_demo`'s `(const xs)` idiom for the + canonical `[1, 2, 3, 4, 5]`. Output: `0 / 3 / 5 / 5 / 3 / 0`. +- `crates/ail/tests/e2e.rs::std_list_more_demo` (e2e count + 35 → 36). + +**`(if (<= n 0) ...)` as the base-case guard.** Both fns gate the +recursion on the int counter at the top of the body, _outside_ the +match. The dual-arm `(case (pat-ctor Cons h t) ...)` then handles +only the n>0 path — so the n=0 branch never re-enters the match, +and the recursive call is reached only when the list is non-empty +and n is still positive. This is a deliberate workaround for the +absence of literal sub-patterns inside Ctor patterns: a +hypothetical `(case (pat-ctor Cons _ _) (case-when (== n 0) ...))` +or matching `n` against `0` directly is queued as 16c. With 16c +landed, both fns could collapse the `if` into the match. + +**No new compiler bug surfaced.** The `if` + Int-arithmetic + +recursive ADT pattern shape is the first instance for `std_list` +in particular but not new for the compiler — `gc_stress` and +`std_list_stress` already exercised `(if (== n 0) ...)` with +`(- n 1)` recursion at the top level. `<=` on `Int` and the +forall-`a` instantiation through the `match` cleanly reused the +same monomorphisation paths. Round-trip `render | parse` stays +canonical for both new files. + +**Tests: 95/95.** + +- e2e: 36 (was 35, +1 for `std_list_more_demo`). +- All other crates unchanged. + +**Cumulative state, post-15h.** + +- Stdlib: 5 modules (`std_maybe`, `std_list`, `std_either`, + `std_pair`, `std_either_list`); **29** combinators total + (27 + 2). All four primary `std_list` operations — length, map, + filter, take/drop — are now present, plus the head/tail/append/ + reverse/is_empty/fold_left/fold_right surface from 15b. +- Compiler bugs surfaced and fixed in dogfood since 14a: 5/5 + (unchanged from 15g-aux). + +**Queue update.** 15h done. Remaining: 16b (local recursive let), +16c (Lit-in-Ctor patterns — would simplify `take`/`drop`), 17a +(per-fn arena, gated on user discussion). diff --git a/examples/std_list.ail.json b/examples/std_list.ail.json index 7a30393..51d1c86 100644 --- a/examples/std_list.ail.json +++ b/examples/std_list.ail.json @@ -1 +1 @@ -{"defs":[{"ctors":[{"fields":[],"name":"Nil"},{"fields":[{"k":"var","name":"a"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"name":"Cons"}],"doc":"Polymorphic singly-linked list: Nil or Cons>.","kind":"type","name":"List","vars":["a"]},{"body":{"arms":[{"body":{"name":"acc","t":"var"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"f","t":"var"},{"args":[{"name":"acc","t":"var"},{"name":"h","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"},{"name":"t","t":"var"}],"fn":{"name":"fold_left","t":"var"},"t":"app","tail":true},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Tail-recursive left fold. The recursive call is in tail position and is marked.","kind":"fn","name":"fold_left","params":["f","acc","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"b"},{"k":"var","name":"a"}],"ret":{"k":"var","name":"b"}},{"k":"var","name":"b"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"k":"var","name":"b"}},"k":"forall","vars":["a","b"]}},{"body":{"arms":[{"body":{"name":"acc","t":"var"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"name":"f","t":"var"},{"name":"acc","t":"var"},{"name":"t","t":"var"}],"fn":{"name":"fold_right","t":"var"},"t":"app"}],"fn":{"name":"f","t":"var"},"t":"app"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Right fold. Constructor-blocked: the recursive call is the second arg of f, NOT a tail position.","kind":"fn","name":"fold_right","params":["f","acc","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"ret":{"k":"var","name":"b"}},{"k":"var","name":"b"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"k":"var","name":"b"}},"k":"forall","vars":["a","b"]}},{"body":{"args":[{"body":{"args":[{"name":"c","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"},"effects":[],"paramTypes":[{"k":"con","name":"Int"},{"k":"var","name":"a"}],"params":["c","_"],"retType":{"k":"con","name":"Int"},"t":"lam"},{"lit":{"kind":"int","value":0},"t":"lit"},{"name":"xs","t":"var"}],"fn":{"name":"fold_left","t":"var"},"t":"app"},"doc":"Length via fold_left. The accumulating lambda ignores the element and increments the counter.","kind":"fn","name":"length","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"k":"con","name":"Int"}},"k":"forall","vars":["a"]}},{"body":{"args":[{"body":{"args":[{"name":"h","t":"var"},{"name":"acc","t":"var"}],"ctor":"Cons","t":"ctor","type":"List"},"effects":[],"paramTypes":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"},{"k":"var","name":"a"}],"params":["acc","h"],"retType":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"},"t":"lam"},{"args":[],"ctor":"Nil","t":"ctor","type":"List"},{"name":"xs","t":"var"}],"fn":{"name":"fold_left","t":"var"},"t":"app"},"doc":"Reverse via fold_left with a flipping accumulator. Tail-recursive by virtue of the fold_left call.","kind":"fn","name":"reverse","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"lit":{"kind":"bool","value":true},"t":"lit"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"lit":{"kind":"bool","value":false},"t":"lit"},"pat":{"ctor":"Cons","fields":[{"p":"wild"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"True iff the list is Nil.","kind":"fn","name":"is_empty","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"k":"con","name":"Bool"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"args":[],"ctor":"Nothing","t":"ctor","type":"std_maybe.Maybe"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"}],"ctor":"Just","t":"ctor","type":"std_maybe.Maybe"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Returns Just of the first element, or Nothing for an empty list. Cross-module Maybe.","kind":"fn","name":"head","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"std_maybe.Maybe"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"args":[],"ctor":"Nothing","t":"ctor","type":"std_maybe.Maybe"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"t","t":"var"}],"ctor":"Just","t":"ctor","type":"std_maybe.Maybe"},"pat":{"ctor":"Cons","fields":[{"p":"wild"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Returns Just> of the tail, or Nothing for an empty list.","kind":"fn","name":"tail","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"k":"con","name":"std_maybe.Maybe"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"name":"ys","t":"var"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"name":"t","t":"var"},{"name":"ys","t":"var"}],"fn":{"name":"append","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"List"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Concatenate two lists. Constructor-blocked recursion: the recursive call is inside Cons, NOT a tail.","kind":"fn","name":"append","params":["xs","ys"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"List"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"args":[{"name":"h","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"},{"args":[{"name":"f","t":"var"},{"name":"t","t":"var"}],"fn":{"name":"map","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"List"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Polymorphic map. Constructor-blocked recursion.","kind":"fn","name":"map","params":["f","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"a"}],"ret":{"k":"var","name":"b"}},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"b"}],"k":"con","name":"List"}},"k":"forall","vars":["a","b"]}},{"body":{"arms":[{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"List"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"cond":{"args":[{"name":"h","t":"var"}],"fn":{"name":"p","t":"var"},"t":"app"},"else":{"args":[{"name":"p","t":"var"},{"name":"t","t":"var"}],"fn":{"name":"filter","t":"var"},"t":"app"},"t":"if","then":{"args":[{"name":"h","t":"var"},{"args":[{"name":"p","t":"var"},{"name":"t","t":"var"}],"fn":{"name":"filter","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"List"}},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Keep elements where p is true. Constructor-blocked when p holds; non-tail recursive call when p is false.","kind":"fn","name":"filter","params":["p","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"a"}],"ret":{"k":"con","name":"Bool"}},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}},"k":"forall","vars":["a"]}}],"imports":[{"module":"std_maybe"}],"name":"std_list","schema":"ailang/v0"} \ No newline at end of file +{"defs":[{"ctors":[{"fields":[],"name":"Nil"},{"fields":[{"k":"var","name":"a"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"name":"Cons"}],"doc":"Polymorphic singly-linked list: Nil or Cons>.","kind":"type","name":"List","vars":["a"]},{"body":{"arms":[{"body":{"name":"acc","t":"var"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"f","t":"var"},{"args":[{"name":"acc","t":"var"},{"name":"h","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"},{"name":"t","t":"var"}],"fn":{"name":"fold_left","t":"var"},"t":"app","tail":true},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Tail-recursive left fold. The recursive call is in tail position and is marked.","kind":"fn","name":"fold_left","params":["f","acc","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"b"},{"k":"var","name":"a"}],"ret":{"k":"var","name":"b"}},{"k":"var","name":"b"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"k":"var","name":"b"}},"k":"forall","vars":["a","b"]}},{"body":{"arms":[{"body":{"name":"acc","t":"var"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"name":"f","t":"var"},{"name":"acc","t":"var"},{"name":"t","t":"var"}],"fn":{"name":"fold_right","t":"var"},"t":"app"}],"fn":{"name":"f","t":"var"},"t":"app"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Right fold. Constructor-blocked: the recursive call is the second arg of f, NOT a tail position.","kind":"fn","name":"fold_right","params":["f","acc","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"ret":{"k":"var","name":"b"}},{"k":"var","name":"b"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"k":"var","name":"b"}},"k":"forall","vars":["a","b"]}},{"body":{"args":[{"body":{"args":[{"name":"c","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"},"effects":[],"paramTypes":[{"k":"con","name":"Int"},{"k":"var","name":"a"}],"params":["c","_"],"retType":{"k":"con","name":"Int"},"t":"lam"},{"lit":{"kind":"int","value":0},"t":"lit"},{"name":"xs","t":"var"}],"fn":{"name":"fold_left","t":"var"},"t":"app"},"doc":"Length via fold_left. The accumulating lambda ignores the element and increments the counter.","kind":"fn","name":"length","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"k":"con","name":"Int"}},"k":"forall","vars":["a"]}},{"body":{"args":[{"body":{"args":[{"name":"h","t":"var"},{"name":"acc","t":"var"}],"ctor":"Cons","t":"ctor","type":"List"},"effects":[],"paramTypes":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"},{"k":"var","name":"a"}],"params":["acc","h"],"retType":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"},"t":"lam"},{"args":[],"ctor":"Nil","t":"ctor","type":"List"},{"name":"xs","t":"var"}],"fn":{"name":"fold_left","t":"var"},"t":"app"},"doc":"Reverse via fold_left with a flipping accumulator. Tail-recursive by virtue of the fold_left call.","kind":"fn","name":"reverse","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"lit":{"kind":"bool","value":true},"t":"lit"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"lit":{"kind":"bool","value":false},"t":"lit"},"pat":{"ctor":"Cons","fields":[{"p":"wild"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"True iff the list is Nil.","kind":"fn","name":"is_empty","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"k":"con","name":"Bool"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"args":[],"ctor":"Nothing","t":"ctor","type":"std_maybe.Maybe"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"}],"ctor":"Just","t":"ctor","type":"std_maybe.Maybe"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Returns Just of the first element, or Nothing for an empty list. Cross-module Maybe.","kind":"fn","name":"head","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"std_maybe.Maybe"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"args":[],"ctor":"Nothing","t":"ctor","type":"std_maybe.Maybe"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"t","t":"var"}],"ctor":"Just","t":"ctor","type":"std_maybe.Maybe"},"pat":{"ctor":"Cons","fields":[{"p":"wild"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Returns Just> of the tail, or Nothing for an empty list.","kind":"fn","name":"tail","params":["xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"k":"con","name":"std_maybe.Maybe"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"name":"ys","t":"var"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"name":"t","t":"var"},{"name":"ys","t":"var"}],"fn":{"name":"append","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"List"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Concatenate two lists. Constructor-blocked recursion: the recursive call is inside Cons, NOT a tail.","kind":"fn","name":"append","params":["xs","ys"],"type":{"body":{"effects":[],"k":"fn","params":[{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}},"k":"forall","vars":["a"]}},{"body":{"arms":[{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"List"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"args":[{"name":"h","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"},{"args":[{"name":"f","t":"var"},{"name":"t","t":"var"}],"fn":{"name":"map","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"List"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Polymorphic map. Constructor-blocked recursion.","kind":"fn","name":"map","params":["f","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"a"}],"ret":{"k":"var","name":"b"}},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"b"}],"k":"con","name":"List"}},"k":"forall","vars":["a","b"]}},{"body":{"arms":[{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"List"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"cond":{"args":[{"name":"h","t":"var"}],"fn":{"name":"p","t":"var"},"t":"app"},"else":{"args":[{"name":"p","t":"var"},{"name":"t","t":"var"}],"fn":{"name":"filter","t":"var"},"t":"app"},"t":"if","then":{"args":[{"name":"h","t":"var"},{"args":[{"name":"p","t":"var"},{"name":"t","t":"var"}],"fn":{"name":"filter","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"List"}},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Keep elements where p is true. Constructor-blocked when p holds; non-tail recursive call when p is false.","kind":"fn","name":"filter","params":["p","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"var","name":"a"}],"ret":{"k":"con","name":"Bool"}},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}},"k":"forall","vars":["a"]}},{"body":{"cond":{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"<=","t":"var"},"t":"app"},"else":{"arms":[{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"List"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"name":"h","t":"var"},{"args":[{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"},{"name":"t","t":"var"}],"fn":{"name":"take","t":"var"},"t":"app"}],"ctor":"Cons","t":"ctor","type":"List"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"t":"if","then":{"args":[],"ctor":"Nil","t":"ctor","type":"List"}},"doc":"First n elements of xs (or all of xs if it has fewer than n).","kind":"fn","name":"take","params":["n","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}},"k":"forall","vars":["a"]}},{"body":{"cond":{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"<=","t":"var"},"t":"app"},"else":{"arms":[{"body":{"args":[],"ctor":"Nil","t":"ctor","type":"List"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"args":[{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"},{"name":"t","t":"var"}],"fn":{"name":"drop","t":"var"},"t":"app"},"pat":{"ctor":"Cons","fields":[{"p":"wild"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"t":"if","then":{"name":"xs","t":"var"}},"doc":"All elements of xs after the first n (or Nil if xs has fewer than n elements).","kind":"fn","name":"drop","params":["n","xs"],"type":{"body":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"},{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}],"ret":{"args":[{"k":"var","name":"a"}],"k":"con","name":"List"}},"k":"forall","vars":["a"]}}],"imports":[{"module":"std_maybe"}],"name":"std_list","schema":"ailang/v0"} \ No newline at end of file diff --git a/examples/std_list.ailx b/examples/std_list.ailx index 6c326c9..aa025e6 100644 --- a/examples/std_list.ailx +++ b/examples/std_list.ailx @@ -161,4 +161,36 @@ (case (pat-ctor Cons h t) (if (app p h) (term-ctor List Cons h (app filter p t)) - (app filter p t))))))) + (app filter p t)))))) + + (fn take + (doc "First n elements of xs (or all of xs if it has fewer than n).") + (type + (forall (vars a) + (fn-type + (params (con Int) (con List a)) + (ret (con List a))))) + (params n xs) + (body + (if (app <= n 0) + (term-ctor List Nil) + (match xs + (case (pat-ctor Nil) (term-ctor List Nil)) + (case (pat-ctor Cons h t) + (term-ctor List Cons h (app take (app - n 1) t))))))) + + (fn drop + (doc "All elements of xs after the first n (or Nil if xs has fewer than n elements).") + (type + (forall (vars a) + (fn-type + (params (con Int) (con List a)) + (ret (con List a))))) + (params n xs) + (body + (if (app <= n 0) + xs + (match xs + (case (pat-ctor Nil) (term-ctor List Nil)) + (case (pat-ctor Cons _ t) + (app drop (app - n 1) t))))))) diff --git a/examples/std_list_more_demo.ail.json b/examples/std_list_more_demo.ail.json new file mode 100644 index 0000000..3e4c9a3 --- /dev/null +++ b/examples/std_list_more_demo.ail.json @@ -0,0 +1 @@ +{"defs":[{"doc":"The canonical [1, 2, 3, 4, 5] used across all checks.","kind":"const","name":"xs","type":{"args":[{"k":"con","name":"Int"}],"k":"con","name":"std_list.List"},"value":{"args":[{"lit":{"kind":"int","value":1},"t":"lit"},{"args":[{"lit":{"kind":"int","value":2},"t":"lit"},{"args":[{"lit":{"kind":"int","value":3},"t":"lit"},{"args":[{"lit":{"kind":"int","value":4},"t":"lit"},{"args":[{"lit":{"kind":"int","value":5},"t":"lit"},{"args":[],"ctor":"Nil","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}],"ctor":"Cons","t":"ctor","type":"std_list.List"}},{"body":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":0},"t":"lit"},{"name":"xs","t":"var"}],"fn":{"name":"std_list.take","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":3},"t":"lit"},{"name":"xs","t":"var"}],"fn":{"name":"std_list.take","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":100},"t":"lit"},{"name":"xs","t":"var"}],"fn":{"name":"std_list.take","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":0},"t":"lit"},{"name":"xs","t":"var"}],"fn":{"name":"std_list.drop","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":2},"t":"lit"},{"name":"xs","t":"var"}],"fn":{"name":"std_list.drop","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":100},"t":"lit"},{"name":"xs","t":"var"}],"fn":{"name":"std_list.drop","t":"var"},"t":"app"}],"fn":{"name":"std_list.length","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"doc":"Expected output (one per line): 0, 3, 5, 5, 3, 0.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[{"module":"std_list"}],"name":"std_list_more_demo","schema":"ailang/v0"} \ No newline at end of file diff --git a/examples/std_list_more_demo.ailx b/examples/std_list_more_demo.ailx new file mode 100644 index 0000000..9820d95 --- /dev/null +++ b/examples/std_list_more_demo.ailx @@ -0,0 +1,32 @@ +; Iter 15h — demo for the new std_list combinators `take` and `drop`. +; Uses a top-level `(const xs)` for the canonical [1, 2, 3, 4, 5] — +; pure ctor expression, so a const is fine (same idiom as +; std_list_demo). Six checks pin both n=0, 0length +; boundaries on each combinator. + +(module std_list_more_demo + + (import std_list) + + (const xs + (doc "The canonical [1, 2, 3, 4, 5] used across all checks.") + (type (con std_list.List (con Int))) + (body + (term-ctor std_list.List Cons 1 + (term-ctor std_list.List Cons 2 + (term-ctor std_list.List Cons 3 + (term-ctor std_list.List Cons 4 + (term-ctor std_list.List Cons 5 + (term-ctor std_list.List Nil)))))))) + + (fn main + (doc "Expected output (one per line): 0, 3, 5, 5, 3, 0.") + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (seq (do io/print_int (app std_list.length (app std_list.take 0 xs))) + (seq (do io/print_int (app std_list.length (app std_list.take 3 xs))) + (seq (do io/print_int (app std_list.length (app std_list.take 100 xs))) + (seq (do io/print_int (app std_list.length (app std_list.drop 0 xs))) + (seq (do io/print_int (app std_list.length (app std_list.drop 2 xs))) + (do io/print_int (app std_list.length (app std_list.drop 100 xs)))))))))))