mk: appendo3 — 3-list append
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 23s
Composes two appendos: (appendo a b mid) ∧ (appendo mid c r). Runs forward (concatenate three known lists) and backward (recover any of the three from the other two and the result). 5 new tests, 491/491 cumulative.
This commit is contained in:
@@ -42,6 +42,12 @@
|
|||||||
;; --- membero ---
|
;; --- membero ---
|
||||||
;; (membero x l) — x appears (at least once) in l.
|
;; (membero x l) — x appears (at least once) in l.
|
||||||
|
|
||||||
|
(define
|
||||||
|
appendo3
|
||||||
|
(fn
|
||||||
|
(l1 l2 l3 result)
|
||||||
|
(fresh (l12) (appendo l1 l2 l12) (appendo l12 l3 result))))
|
||||||
|
|
||||||
(define
|
(define
|
||||||
membero
|
membero
|
||||||
(fn
|
(fn
|
||||||
@@ -82,8 +88,8 @@
|
|||||||
((nullo l) (== result acc))
|
((nullo l) (== result acc))
|
||||||
((fresh (a d acc-prime) (conso a d l) (conso a acc acc-prime) (rev-acco d acc-prime result))))))
|
((fresh (a d acc-prime) (conso a d l) (conso a acc acc-prime) (rev-acco d acc-prime result))))))
|
||||||
|
|
||||||
(define rev-2o (fn (l result) (rev-acco l (list) result)))
|
|
||||||
|
|
||||||
|
(define rev-2o (fn (l result) (rev-acco l (list) result)))
|
||||||
|
|
||||||
(define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev))))
|
(define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev))))
|
||||||
|
|
||||||
|
|||||||
49
lib/minikanren/tests/appendo3.sx
Normal file
49
lib/minikanren/tests/appendo3.sx
Normal file
@@ -0,0 +1,49 @@
|
|||||||
|
;; lib/minikanren/tests/appendo3.sx — 3-list append.
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-forward"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo3
|
||||||
|
(list 1 2)
|
||||||
|
(list 3 4)
|
||||||
|
(list 5 6)
|
||||||
|
q))
|
||||||
|
(list
|
||||||
|
(list 1 2 3 4 5 6)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-empty-everything"
|
||||||
|
(run* q (appendo3 (list) (list) (list) q))
|
||||||
|
(list (list)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-recover-middle"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo3
|
||||||
|
(list 1 2)
|
||||||
|
q
|
||||||
|
(list 5 6)
|
||||||
|
(list 1 2 3 4 5 6)))
|
||||||
|
(list (list 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-empty-middle"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo3
|
||||||
|
(list 1 2)
|
||||||
|
(list)
|
||||||
|
(list 3 4)
|
||||||
|
q))
|
||||||
|
(list (list 1 2 3 4)))
|
||||||
|
|
||||||
|
(mk-test
|
||||||
|
"appendo3-empty-first-and-last"
|
||||||
|
(run*
|
||||||
|
q
|
||||||
|
(appendo3 (list) (list 1 2 3) (list) q))
|
||||||
|
(list (list 1 2 3)))
|
||||||
|
|
||||||
|
(mk-tests-run!)
|
||||||
@@ -173,6 +173,7 @@ _(none yet)_
|
|||||||
|
|
||||||
_Newest first._
|
_Newest first._
|
||||||
|
|
||||||
|
- **2026-05-08** — **appendo3**: 3-list append via two appendos. (appendo3 a b c r) is (appendo a b mid) ∧ (appendo mid c r). Recovers any of the three lists given the other two and the result. 5 new tests, 491/491 cumulative.
|
||||||
- **2026-05-08** — **lengtho-i**: integer-indexed length (intarith). Empty list -> 0; recurse with pluso-i. Drop-in fast replacement for Peano lengtho when the count fits in a host integer. 5 new tests, 486/486 cumulative.
|
- **2026-05-08** — **lengtho-i**: integer-indexed length (intarith). Empty list -> 0; recurse with pluso-i. Drop-in fast replacement for Peano lengtho when the count fits in a host integer. 5 new tests, 486/486 cumulative.
|
||||||
- **2026-05-08** — **sumo + producto (intarith)**: fold a list of ground integers to its sum or product. Empty list -> identity (0 / 1). Recurse via pluso-i / *o-i. 9 new tests, 481/481 cumulative.
|
- **2026-05-08** — **sumo + producto (intarith)**: fold a list of ground integers to its sum or product. Empty list -> identity (0 / 1). Recurse via pluso-i / *o-i. 9 new tests, 481/481 cumulative.
|
||||||
- **2026-05-08** — **mino + maxo (intarith)**: find the minimum/maximum of a non-empty list of ground integers. Two conde clauses each: singleton (return the element) / multi (compare head against recursive min/max of tail). 9 new tests, 472/472 cumulative.
|
- **2026-05-08** — **mino + maxo (intarith)**: find the minimum/maximum of a non-empty list of ground integers. Two conde clauses each: singleton (return the element) / multi (compare head against recursive min/max of tail). 9 new tests, 472/472 cumulative.
|
||||||
|
|||||||
Reference in New Issue
Block a user