mk: foldl-o — relational left fold
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 33s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 33s
Complement to foldr-o. The combiner relation has signature
(acc head new-acc) — accumulator first.
Examples:
(foldl-o pluso-i (list 1 2 3 4 5) 0 q) -> (15)
(foldl-o *o-i (list 1 2 3 4) 1 q) -> (24)
(foldl-o (fn (acc x r) (conso x acc r)) ; flipped conso
(list 1 2 3 4) (list) q) -> ((4 3 2 1)) ; reverse
5 new tests, 510/510 cumulative.
This commit is contained in:
@@ -64,6 +64,14 @@
|
||||
((nullo l) (== result acc))
|
||||
((fresh (a d r-rest) (conso a d l) (foldr-o rel d acc r-rest) (rel a r-rest result))))))
|
||||
|
||||
(define
|
||||
foldl-o
|
||||
(fn
|
||||
(rel l acc result)
|
||||
(conde
|
||||
((nullo l) (== result acc))
|
||||
((fresh (a d new-acc) (conso a d l) (rel acc a new-acc) (foldl-o rel d new-acc result))))))
|
||||
|
||||
(define
|
||||
membero
|
||||
(fn
|
||||
@@ -80,6 +88,7 @@
|
||||
((nullo l))
|
||||
((fresh (a d) (conso a d l) (nafc (== a x)) (not-membero x d))))))
|
||||
|
||||
|
||||
(define
|
||||
subseto
|
||||
(fn
|
||||
@@ -88,7 +97,6 @@
|
||||
((nullo l1))
|
||||
((fresh (a d) (conso a d l1) (membero a l2) (subseto d l2))))))
|
||||
|
||||
|
||||
(define
|
||||
reverseo
|
||||
(fn
|
||||
|
||||
Reference in New Issue
Block a user