Iter 15h — std_list extension: take, drop
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<a>) -> List<a>
— first n elements (or all of xs if shorter than n).
drop : forall a. (Int, List<a>) -> List<a>
— 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.
This commit is contained in:
+33
-1
@@ -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)))))))
|
||||
|
||||
Reference in New Issue
Block a user