lambda_calculus/data/list/pair.rs
1//! [Single-pair list](https://en.wikipedia.org/wiki/Church_encoding#One_pair_as_a_list_node)
2
3use crate::combinators::{I, Z};
4use crate::data::boolean::{fls, tru};
5use crate::data::num::church::{is_zero, pred, succ, zero};
6use crate::data::pair::{fst, pair, snd};
7use crate::term::Term::*;
8use crate::term::{abs, app, Term};
9
10/// Produces a `nil`, the last link of a pair-encoded list; equivalent to `boolean::fls`.
11///
12/// NIL ≡ λab.b ≡ λ λ 1 ≡ FALSE
13pub fn nil() -> Term {
14 fls()
15}
16
17/// Applied to a pair-encoded list it determines if it is empty.
18///
19/// IS_NIL ≡ λl.l (λhtd.FALSE) TRUE ≡ λ 1 (λ λ λ FALSE) TRUE
20///
21/// # Example
22/// ```
23/// use lambda_calculus::data::list::pair::is_nil;
24/// use lambda_calculus::*;
25///
26/// assert_eq!(beta(app(is_nil(), vec![].into_pair_list()), NOR, 0), true.into());
27/// assert_eq!(beta(app(is_nil(), vec![1.into_church()].into_pair_list()), NOR, 0), false.into());
28/// ```
29pub fn is_nil() -> Term {
30 abs(app!(Var(1), abs!(3, fls()), tru()))
31}
32
33/// Applied to two terms it returns them contained in a pair-encoded list; equivalent to `pair::pair`.
34///
35/// CONS ≡ λxyz.z x y ≡ λ λ λ 1 3 2 ≡ PAIR
36///
37/// # Example
38/// ```
39/// use lambda_calculus::data::list::pair::{nil, cons};
40/// use lambda_calculus::*;
41///
42/// let list_consed =
43/// app!(
44/// cons(),
45/// 1.into_church(),
46/// app!(
47/// cons(),
48/// 2.into_church(),
49/// app!(
50/// cons(),
51/// 3.into_church(),
52/// nil()
53/// )
54/// )
55/// );
56///
57/// let list_from_vec = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
58///
59/// assert_eq!(beta(list_consed, NOR, 0), list_from_vec);
60/// ```
61pub fn cons() -> Term {
62 pair()
63}
64
65/// Applied to a pair-encoded list it returns its first element; equivalent to `pair::fst`.
66///
67/// HEAD ≡ λp.p TRUE ≡ λ 1 TRUE ≡ FST
68///
69/// # Example
70/// ```
71/// use lambda_calculus::data::list::pair::head;
72/// use lambda_calculus::*;
73///
74/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
75///
76/// assert_eq!(beta(app(head(), list), NOR, 0), 1.into_church());
77/// ```
78pub fn head() -> Term {
79 fst()
80}
81
82/// Applied to a pair-encoded list it returns a new list with all its elements but the first one;
83/// equivalent to `pair::snd`.
84///
85/// TAIL ≡ λp.p FALSE ≡ λ 1 FALSE ≡ SND
86///
87/// # Example
88/// ```
89/// use lambda_calculus::data::list::pair::tail;
90/// use lambda_calculus::*;
91///
92/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
93///
94/// assert_eq!(
95/// beta(app(tail(), list), NOR, 0),
96/// vec![2.into_church(), 3.into_church()].into_pair_list()
97/// );
98/// ```
99pub fn tail() -> Term {
100 snd()
101}
102
103/// Applied to a pair-encoded list it returns its Church-encoded length.
104///
105/// LENGTH ≡ Z (λzal.IS_NIL l (λx.a) (λx.z (SUCC a) (TAIL l)) I) ZERO
106/// ≡ Z (λλλ IS_NIL 1 (λ 3) (λ 4 (SUCC 3) (TAIL 2)) I) ZERO
107///
108/// # Example
109/// ```
110/// use lambda_calculus::data::list::pair::{length, nil};
111/// use lambda_calculus::*;
112///
113/// assert_eq!(
114/// beta(app(length(), nil()), NOR, 0),
115/// 0.into_church()
116/// );
117/// ```
118pub fn length() -> Term {
119 app!(
120 Z(),
121 abs!(
122 3,
123 app!(
124 is_nil(),
125 Var(1),
126 abs(Var(3)),
127 abs(app!(Var(4), app(succ(), Var(3)), app(tail(), Var(2)))),
128 I()
129 )
130 ),
131 zero()
132 )
133}
134
135/// Applied to a Church-encoded number `i` and a pair-encoded list it returns the `i`-th
136/// (zero-indexed) element of the list.
137///
138/// INDEX ≡ λil.HEAD (i TAIL l) ≡ λ λ HEAD (2 TAIL 1)
139///
140/// # Example
141/// ```
142/// use lambda_calculus::data::list::pair::index;
143/// use lambda_calculus::*;
144///
145/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()];
146///
147/// assert_eq!(
148/// beta(app!(index(), 0.into_church(), list.into_pair_list()), NOR, 0),
149/// 1.into_church()
150/// );
151/// ```
152pub fn index() -> Term {
153 abs!(2, app(head(), app!(Var(2), tail(), Var(1))))
154}
155
156/// Reverses a pair-encoded list.
157///
158/// REVERSE ≡ Z (λzal.IS_NIL l (λx.a) (λx.z (CONS (HEAD l) a) (TAIL l) I)) NIL
159/// ≡ Z (λ λ λ IS_NIL 1 (λ 3) (λ 4 (CONS (HEAD 2) 3) (TAIL 2)) I) NIL
160///
161/// # Example
162/// ```
163/// use lambda_calculus::data::list::pair::reverse;
164/// use lambda_calculus::*;
165///
166/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
167///
168/// assert_eq!(
169/// beta(app(reverse(), list), NOR, 0),
170/// vec![3.into_church(), 2.into_church(), 1.into_church()].into_pair_list()
171/// );
172/// ```
173pub fn reverse() -> Term {
174 app!(
175 Z(),
176 abs!(
177 3,
178 app!(
179 is_nil(),
180 Var(1),
181 abs(Var(3)),
182 abs(app!(
183 Var(4),
184 app!(cons(), app(head(), Var(2)), Var(3)),
185 app(tail(), Var(2))
186 )),
187 I()
188 )
189 ),
190 nil()
191 )
192}
193
194/// Applied to a Church-encoded number `n` and `n` `Term`s it creates a pair-encoded list of those
195/// terms.
196///
197/// LIST ≡ λn.n (λfax.f (CONS x a)) REVERSE NIL ≡ λ 1 (λ λ λ 3 (CONS 1 2)) REVERSE NIL
198///
199/// # Example
200/// ```
201/// use lambda_calculus::data::list::pair::list;
202/// use lambda_calculus::*;
203///
204/// assert_eq!(
205/// beta(app!(list(), 3.into_church(), 1.into_church(), 2.into_church(), 3.into_church()), NOR, 0),
206/// vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list()
207/// );
208/// ```
209pub fn list() -> Term {
210 abs(app!(
211 Var(1),
212 abs!(3, app(Var(3), app!(cons(), Var(1), Var(2)))),
213 reverse(),
214 nil()
215 ))
216}
217
218/// Applied to two pair-encoded lists it concatenates them.
219///
220/// APPEND ≡ Z (λzab.IS_NIL a (λx.b) (λx.CONS (HEAD a) (z (TAIL a) b)) I)
221/// ≡ Z (λ λ λ IS_NIL 2 (λ 2) (λ CONS (HEAD 3) (4 (TAIL 3) 2)) I)
222///
223/// # Example
224/// ```
225/// use lambda_calculus::data::list::pair::append;
226/// use lambda_calculus::*;
227///
228/// let list1 = vec![1.into_church(), 2.into_church()].into_pair_list();
229/// let list2 = vec![3.into_church(), 4.into_church()].into_pair_list();
230///
231/// assert_eq!(
232/// beta(app!(append(), list1, list2), NOR, 0),
233/// vec![1.into_church(), 2.into_church(), 3.into_church(), 4.into_church()].into_pair_list()
234/// );
235/// ```
236pub fn append() -> Term {
237 app(
238 Z(),
239 abs!(
240 3,
241 app!(
242 is_nil(),
243 Var(2),
244 abs(Var(2)),
245 abs(app!(
246 cons(),
247 app(head(), Var(3)),
248 app!(Var(4), app(tail(), Var(3)), Var(2))
249 )),
250 I()
251 )
252 ),
253 )
254}
255
256/// Applied to a function and a pair-encoded list it maps the function over it.
257///
258/// MAP ≡ Z (λzfl.IS_NIL l (λx.NIL) (λx.CONS (f (HEAD l)) (z f (TAIL l))) I)
259/// ≡ Z (λ λ λ IS_NIL 1 (λ NIL) (λ CONS (3 (HEAD 2)) (4 3 (TAIL 2))) I)
260///
261/// # Example
262/// ```
263/// use lambda_calculus::data::list::pair::map;
264/// use lambda_calculus::data::num::church::succ;
265/// use lambda_calculus::*;
266///
267/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
268///
269/// assert_eq!(
270/// beta(app!(map(), succ(), list), NOR, 0),
271/// vec![2.into_church(), 3.into_church(), 4.into_church()].into_pair_list()
272/// );
273/// ```
274pub fn map() -> Term {
275 app(
276 Z(),
277 abs!(
278 3,
279 app!(
280 is_nil(),
281 Var(1),
282 abs(nil()),
283 abs(app!(
284 cons(),
285 app(Var(3), app(head(), Var(2))),
286 app!(Var(4), Var(3), app(tail(), Var(2)))
287 )),
288 I()
289 )
290 ),
291 )
292}
293
294/// Applied to a function, a starting value and a pair-encoded list it performs a
295/// [left fold](https://en.wikipedia.org/wiki/Fold_(higher-order_function)#Folds_on_lists)
296/// on the list.
297///
298/// FOLDL ≡ Z (λzfsl.IS_NIL l (λx.s) (λx.z f (f s (HEAD l)) (TAIL l)) I)
299/// ≡ Z (λ λ λ λ IS_NIL 1 (λ 3) (λ 5 4 (4 3 (HEAD 2)) (TAIL 2)) I)
300///
301/// # Example
302/// ```
303/// use lambda_calculus::data::list::pair::foldl;
304/// use lambda_calculus::data::num::church::{add, sub};
305/// use lambda_calculus::*;
306///
307/// let list = || vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
308///
309/// assert_eq!(beta(app!(foldl(), add(), 0.into_church(), list()), NOR, 0), 6.into_church());
310/// assert_eq!(beta(app!(foldl(), sub(), 6.into_church(), list()), NOR, 0), 0.into_church());
311/// ```
312pub fn foldl() -> Term {
313 app(
314 Z(),
315 abs!(
316 4,
317 app!(
318 is_nil(),
319 Var(1),
320 abs(Var(3)),
321 abs(app!(
322 Var(5),
323 Var(4),
324 app!(Var(4), Var(3), app(head(), Var(2))),
325 app(tail(), Var(2))
326 )),
327 I()
328 )
329 ),
330 )
331}
332
333/// Applied to a function, a starting value and a pair-encoded list it performs a
334/// [right fold](https://en.wikipedia.org/wiki/Fold_(higher-order_function)#Folds_on_lists)
335/// on the list.
336///
337/// FOLDR ≡ λfal.Z (λzt.IS_NIL t (λx.a) (λx.f (HEAD t) (z (TAIL t))) I) l
338/// ≡ λ λ λ Z (λ λ IS_NIL 1 (λ 5) (λ 6 (HEAD 2) (3 (TAIL 2))) I) 1
339///
340/// # Example
341/// ```
342/// use lambda_calculus::data::list::pair::foldr;
343/// use lambda_calculus::data::num::church::{add, sub};
344/// use lambda_calculus::*;
345///
346/// let list = || vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
347///
348/// assert_eq!(beta(app!(foldr(), add(), 0.into_church(), list()), NOR, 0), 6.into_church());
349/// assert_eq!(beta(app!(foldr(), sub(), 6.into_church(), list()), NOR, 0), 0.into_church());
350/// ```
351pub fn foldr() -> Term {
352 abs!(
353 3,
354 app!(
355 Z(),
356 abs!(
357 2,
358 app!(
359 is_nil(),
360 Var(1),
361 abs(Var(5)),
362 abs(app!(
363 Var(6),
364 app(head(), Var(2)),
365 app!(Var(3), app(tail(), Var(2)))
366 )),
367 I()
368 )
369 ),
370 Var(1)
371 )
372 )
373}
374
375/// Applied to a predicate and a pair-encoded list it filters the list based on the predicate.
376///
377/// FILTER ≡ Z (λzpl.IS_NIL l (λx.NIL) (λx.p (HEAD l) (CONS (HEAD l)) I (z p (TAIL l))) I)
378/// ≡ Z (λ λ λ IS_NIL 1 (λ NIL) (λ 3 (HEAD 2) (CONS (HEAD 2)) I (4 3 (TAIL 2))) I)
379///
380/// # Example
381/// ```
382/// use lambda_calculus::data::list::pair::filter;
383/// use lambda_calculus::data::num::church::{is_zero, gt};
384/// use lambda_calculus::combinators::C;
385/// use lambda_calculus::*;
386///
387/// let list = || vec![0.into_church(), 1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
388/// let gt_1 = app!(C(), gt(), 1.into_church()); // greater than 1
389///
390/// assert_eq!(
391/// beta(app!(filter(), is_zero(), list()), NOR, 0),
392/// vec![0.into_church()].into_pair_list()
393/// );
394/// assert_eq!(
395/// beta(app!(filter(), gt_1, list()), NOR, 0),
396/// vec![2.into_church(), 3.into_church()].into_pair_list()
397/// );
398/// ```
399pub fn filter() -> Term {
400 app(
401 Z(),
402 abs!(
403 3,
404 app!(
405 is_nil(),
406 Var(1),
407 abs(nil()),
408 abs(app!(
409 Var(3),
410 app(head(), Var(2)),
411 app(cons(), app(head(), Var(2))),
412 I(),
413 app!(Var(4), Var(3), app(tail(), Var(2)))
414 )),
415 I()
416 )
417 ),
418 )
419}
420
421/// Applied to a pair-encoded list it returns the last element.
422///
423/// LAST ≡ Z (λzl.IS_NIL l (λx.NIL) (λx.IS_NIL (TAIL l) (HEAD l) (z (TAIL l))) I)
424/// ≡ Z (λ λ IS_NIL 1 (λ NIL) (λ IS_NIL (TAIL 2) (HEAD 2) (3 (TAIL 2))) I)
425///
426/// # Example
427/// ```
428/// use lambda_calculus::data::list::pair::last;
429/// use lambda_calculus::*;
430///
431/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
432///
433/// assert_eq!(beta(app(last(), list), NOR, 0), 3.into_church());
434/// ```
435pub fn last() -> Term {
436 app(
437 Z(),
438 abs!(
439 2,
440 app!(
441 is_nil(),
442 Var(1),
443 abs(nil()),
444 abs(app!(
445 is_nil(),
446 app(tail(), Var(2)),
447 app(head(), Var(2)),
448 app(Var(3), app(tail(), Var(2)))
449 )),
450 I()
451 )
452 ),
453 )
454}
455
456/// Applied to a pair-encoded list it returns the list without the last element.
457///
458/// INIT ≡ Z (λzl.IS_NIL l (λx.NIL) (λx.IS_NIL (TAIL l) NIL (CONS (HEAD l) (z (TAIL l)))) I)
459/// ≡ Z (λ λ IS_NIL 1 (λ NIL) (λ IS_NIL (TAIL 2) NIL (CONS (HEAD 2) (3 (TAIL 2)))) I)
460///
461/// # Example
462/// ```
463/// use lambda_calculus::data::list::pair::init;
464/// use lambda_calculus::*;
465///
466/// let list1 = vec![1.into_church(), 2.into_church(), 3.into_church()].into_pair_list();
467/// let list2 = vec![1.into_church(), 2.into_church()].into_pair_list();
468///
469/// assert_eq!(beta(app(init(), list1), NOR, 0), list2);
470/// ```
471pub fn init() -> Term {
472 app(
473 Z(),
474 abs!(
475 2,
476 app!(
477 is_nil(),
478 Var(1),
479 abs(nil()),
480 abs(app!(
481 is_nil(),
482 app(tail(), Var(2)),
483 nil(),
484 app!(
485 cons(),
486 app(head(), Var(2)),
487 app(Var(3), app(tail(), Var(2)))
488 )
489 )),
490 I()
491 )
492 ),
493 )
494}
495
496/// Applied to two pair-encoded lists it returns a list of corresponding pairs. If one input list
497/// is shorter, excess elements of the longer list are discarded.
498///
499/// ZIP ≡ Z (λzab.IS_NIL b (λx.NIL) (λx.IS_NIL a NIL (CONS (CONS (HEAD b) (HEAD a)) (z (TAIL b) (TAIL a)))) I)
500/// ≡ Z (λ λ λ IS_NIL 2 (λ NIL) (λ IS_NIL 2 NIL (CONS (CONS (HEAD 3) (HEAD 2)) (4 (TAIL 3) (TAIL 2)))) I)
501///
502/// # Example
503/// ```
504/// use lambda_calculus::data::list::pair::zip;
505/// use lambda_calculus::*;
506///
507/// let list = || vec![0.into_church(), 1.into_church()].into_pair_list();
508/// let pairs = || vec![(0, 0).into_church(), (1, 1).into_church()].into_pair_list();
509///
510/// assert_eq!(beta(app!(zip(), list(), list()), NOR, 0), pairs());
511/// ```
512pub fn zip() -> Term {
513 app(
514 Z(),
515 abs!(
516 3,
517 app!(
518 is_nil(),
519 Var(2),
520 abs(nil()),
521 abs(app!(
522 is_nil(),
523 Var(2),
524 nil(),
525 app!(
526 cons(),
527 app!(cons(), app(head(), Var(3)), app(head(), Var(2))),
528 app!(Var(4), app(tail(), Var(3)), app(tail(), Var(2)))
529 )
530 )),
531 I()
532 )
533 ),
534 )
535}
536
537/// Applied to a function and two pair-encoded lists it applies the function to the corresponding
538/// elements and returns the resulting list. If one input list is shorter, excess elements of the
539/// longer list are discarded.
540///
541/// ZIP_WITH ≡ Z (λzfab.IS_NIL b (λx.NIL) (λx.IS_NIL a NIL (CONS (f (HEAD b) (HEAD a)) (z f (TAIL b) (TAIL a)))) I)
542/// ≡ Z (λ λ λ λ IS_NIL 2 (λ NIL) (λ IS_NIL 2 NIL (CONS (4 (HEAD 3) (HEAD 2)) (5 4 (TAIL 3) (TAIL 2)))) I)
543///
544/// # Example
545/// ```
546/// use lambda_calculus::data::list::pair::zip_with;
547/// use lambda_calculus::data::num::church::add;
548/// use lambda_calculus::*;
549///
550/// let list1 = || vec![2.into_church(), 3.into_church()].into_pair_list();
551/// let list2 = || vec![4.into_church(), 6.into_church()].into_pair_list();
552///
553/// assert_eq!(beta(app!(zip_with(), add(), list1(), list1()), NOR, 0), list2());
554/// ```
555pub fn zip_with() -> Term {
556 app(
557 Z(),
558 abs!(
559 4,
560 app!(
561 is_nil(),
562 Var(2),
563 abs(nil()),
564 abs(app!(
565 is_nil(),
566 Var(2),
567 nil(),
568 app!(
569 cons(),
570 app!(Var(4), app(head(), Var(3)), app(head(), Var(2))),
571 app!(Var(5), Var(4), app(tail(), Var(3)), app(tail(), Var(2)))
572 )
573 )),
574 I()
575 )
576 ),
577 )
578}
579
580/// Applied to a Church-encoded number `n` and a pair-encoded list it returns a new list with the
581/// first `n` elements of the supplied list.
582///
583/// TAKE ≡ Z (λznl.IS_NIL l (λx.NIL) (λx.IS_ZERO n NIL (CONS (HEAD l) (z (PRED n) (TAIL l)))) I)
584/// ≡ Z (λ λ λ IS_NIL 1 (λ NIL) (λ IS_ZERO 3 NIL (CONS (HEAD 2) (4 (PRED 3) (TAIL 2)))) I)
585///
586/// # Example
587/// ```
588/// use lambda_calculus::data::list::pair::take;
589/// use lambda_calculus::*;
590///
591/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()];
592///
593/// assert_eq!(
594/// beta(app!(take(), 2.into_church(), list.into_pair_list()), NOR, 0),
595/// vec![1.into_church(), 2.into_church()].into_pair_list()
596/// );
597/// ```
598pub fn take() -> Term {
599 app!(
600 Z(),
601 abs!(
602 3,
603 app!(
604 is_nil(),
605 Var(1),
606 abs(nil()),
607 abs(app!(
608 is_zero(),
609 Var(3),
610 nil(),
611 app!(
612 cons(),
613 app(head(), Var(2)),
614 app!(Var(4), app(pred(), Var(3)), app(tail(), Var(2)))
615 )
616 )),
617 I()
618 )
619 )
620 )
621}
622
623/// Applied to a predicate function and a pair-encoded list it returns the longest prefix of the
624/// list whose elements all satisfy the predicate function.
625///
626/// TAKE_WHILE ≡ Z (λzfl. IS_NIL l (λx.NIL) (λx.f (HEAD l) (CONS (HEAD l) (z f (TAIL l))) NIL) I)
627/// ≡ Z (λ λ λ IS_NIL 1 (λ NIL) (λ 3 (HEAD 2) (CONS (HEAD 2) (4 3 (TAIL 2))) NIL) I)
628///
629/// # Example
630/// ```
631/// use lambda_calculus::data::list::pair::take_while;
632/// use lambda_calculus::data::num::church::is_zero;
633/// use lambda_calculus::*;
634///
635/// let list1 = vec![0.into_church(), 0.into_church(), 1.into_church()].into_pair_list();
636/// let list2 = vec![0.into_church(), 0.into_church()].into_pair_list();
637///
638/// assert_eq!(beta(app!(take_while(), is_zero(), list1), NOR, 0), list2);
639/// ```
640pub fn take_while() -> Term {
641 app(
642 Z(),
643 abs!(
644 3,
645 app!(
646 is_nil(),
647 Var(1),
648 abs(nil()),
649 abs(app!(
650 Var(3),
651 app(head(), Var(2)),
652 app!(
653 cons(),
654 app(head(), Var(2)),
655 app!(Var(4), Var(3), app(tail(), Var(2)))
656 ),
657 nil()
658 )),
659 I()
660 )
661 ),
662 )
663}
664
665/// Applied to a Church-encoded number `n` and a pair-encoded list it returns a new list without
666/// the first `n` elements of the supplied list.
667///
668/// DROP ≡ Z (λznl.IS_NIL l (λx.NIL) (λx.IS_ZERO n l (z (PRED n) (TAIL l))) I)
669/// ≡ Z (λ λ λ IS_NIL 1 (λ NIL) (λ IS_ZERO 3 2 (4 (PRED 3) (TAIL 2))) I)
670///
671/// # Example
672/// ```
673/// use lambda_calculus::data::list::pair::drop;
674/// use lambda_calculus::*;
675///
676/// let list = vec![1.into_church(), 2.into_church(), 3.into_church()];
677///
678/// assert_eq!(
679/// beta(app!(drop(), 1.into_church(), list.into_pair_list()), NOR, 0),
680/// vec![2.into_church(), 3.into_church()].into_pair_list()
681/// );
682/// ```
683pub fn drop() -> Term {
684 app!(
685 Z(),
686 abs!(
687 3,
688 app!(
689 is_nil(),
690 Var(1),
691 abs(nil()),
692 abs(app!(
693 is_zero(),
694 Var(3),
695 Var(2),
696 app!(Var(4), app(pred(), Var(3)), app(tail(), Var(2)))
697 )),
698 I()
699 )
700 )
701 )
702}
703
704/// Applied to a predicate function and a pair-encoded list it returns a new list without
705/// the prefix of the supplied list whose elements satisfy the predicate function.
706///
707/// DROP_WHILE ≡ Z (λzfl.IS_NIL l (λx.NIL) (λx.f (HEAD l) (z f (TAIL l)) l) I)
708/// ≡ Z (λ λ λ IS_NIL 1 (λ NIL) (λ 3 (HEAD 2) (4 3 (TAIL 2)) 2) I)
709///
710/// # Example
711/// ```
712/// use lambda_calculus::data::list::pair::drop_while;
713/// use lambda_calculus::data::num::church::is_zero;
714/// use lambda_calculus::*;
715///
716/// let list1 = vec![0.into_church(), 0.into_church(), 1.into_church(), 0.into_church()].into_pair_list();
717/// let list2 = vec![1.into_church(), 0.into_church()].into_pair_list();
718///
719/// assert_eq!(beta(app!(drop_while(), is_zero(), list1), NOR, 0), list2);
720/// ```
721pub fn drop_while() -> Term {
722 app(
723 Z(),
724 abs!(
725 3,
726 app!(
727 is_nil(),
728 Var(1),
729 abs(nil()),
730 abs(app!(
731 Var(3),
732 app(head(), Var(2)),
733 app!(Var(4), Var(3), app(tail(), Var(2))),
734 Var(2)
735 )),
736 I()
737 )
738 ),
739 )
740}
741
742/// Applied to a Church-encoded number `n` and an argument, it produces a list containing the
743/// argument repeated `n` times.
744///
745/// REPLICATE ≡ Z (λzny.IS_ZERO n (λx.NIL) (λx.PAIR y (z (PRED n) y)) I)
746/// ≡ Z (λ λ λ IS_ZERO 2 (λ NIL) (λ PAIR 2 (4 (PRED 3) 2)) I)
747///
748/// # Example
749/// ```
750/// use lambda_calculus::data::list::pair::replicate;
751/// use lambda_calculus::*;
752///
753/// let list1 = vec![2.into_church(), 2.into_church(), 2.into_church()].into_pair_list();
754/// let list2 = vec![].into_pair_list();
755///
756/// assert_eq!(beta(app!(replicate(), 3.into_church(), 2.into_church()), NOR, 0), list1);
757/// assert_eq!(beta(app!(replicate(), 0.into_church(), 4.into_church()), NOR, 0), list2);
758/// ```
759pub fn replicate() -> Term {
760 app(
761 Z(),
762 abs!(
763 3,
764 app!(
765 is_zero(),
766 Var(2),
767 abs(nil()),
768 abs(app!(
769 pair(),
770 Var(2),
771 app!(Var(4), app(pred(), Var(3)), Var(2))
772 )),
773 I()
774 )
775 ),
776 )
777}
778
779impl From<Vec<Term>> for Term {
780 fn from(vec: Vec<Term>) -> Term {
781 let mut ret = nil();
782
783 for term in vec.into_iter().rev() {
784 ret = abs(app!(Var(1), term, ret))
785 }
786
787 ret
788 }
789}