mk: mino + maxo — find min/max of a list
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 24s
Two conde clauses each: singleton -> the element; multi -> compare head against the recursive min/max of the tail and pick. Uses lteo-i / lto-i for the comparisons, so the input must be ground integers. mino + maxo can run together: (fresh (mn mx) (mino l mn) (maxo l mx) (== q (list mn mx))) recovers both. 9 new tests, 472/472 cumulative.
This commit is contained in:
@@ -77,3 +77,19 @@
|
||||
((nullo l))
|
||||
((fresh (a) (== l (list a))))
|
||||
((fresh (a b rest mid) (conso a mid l) (conso b rest mid) (lteo-i a b) (sortedo mid))))))
|
||||
|
||||
(define
|
||||
mino
|
||||
(fn
|
||||
(l m)
|
||||
(conde
|
||||
((fresh (a) (== l (list a)) (== m a)))
|
||||
((fresh (a d rest-min) (conso a d l) (mino d rest-min) (conde ((lteo-i a rest-min) (== m a)) ((lto-i rest-min a) (== m rest-min))))))))
|
||||
|
||||
(define
|
||||
maxo
|
||||
(fn
|
||||
(l m)
|
||||
(conde
|
||||
((fresh (a) (== l (list a)) (== m a)))
|
||||
((fresh (a d rest-max) (conso a d l) (maxo d rest-max) (conde ((lteo-i rest-max a) (== m a)) ((lto-i a rest-max) (== m rest-max))))))))
|
||||
|
||||
Reference in New Issue
Block a user