mk: rembero / assoco / nth-o — more list relations
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 54s
rembero (remove-first) uses nafc to gate the skip-element clause so the result is well-defined on ground lists. assoco is alist lookup — runs forward (key -> value) and backward (find keys with a given value). nth-o uses Peano-encoded indices into a list, mirroring lengtho. 13 new tests, 266/266 cumulative.
This commit is contained in:
@@ -96,3 +96,31 @@
|
||||
(flatteno t tf)
|
||||
(appendo hf tf flat)))
|
||||
((nafc (nullo tree)) (nafc (pairo tree)) (== flat (list tree))))))
|
||||
|
||||
|
||||
(define
|
||||
rembero
|
||||
(fn
|
||||
(x l out)
|
||||
(conde
|
||||
((nullo l) (nullo out))
|
||||
((fresh (a d) (conso a d l) (== a x) (== out d)))
|
||||
((fresh (a d res) (conso a d l) (nafc (== a x)) (conso a res out) (rembero x d res))))))
|
||||
|
||||
(define
|
||||
assoco
|
||||
(fn
|
||||
(key pairs val)
|
||||
(fresh
|
||||
(rest)
|
||||
(conde
|
||||
((conso (list key val) rest pairs))
|
||||
((fresh (other) (conso other rest pairs) (assoco key rest val)))))))
|
||||
|
||||
(define
|
||||
nth-o
|
||||
(fn
|
||||
(n l elem)
|
||||
(conde
|
||||
((== n :z) (fresh (d) (conso elem d l)))
|
||||
((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (nth-o n-1 d elem))))))
|
||||
|
||||
Reference in New Issue
Block a user