giles
c4b6f1fa0f
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 25s
Three conde clauses: empty list / singleton list / two-or-more (where the first two satisfy lteo-i and the rest is recursively sorted). Uses ground-only integer comparison (intarith), so the input list must walk to ground integers. 7 new tests, 463/463 cumulative.
80 lines
1.7 KiB
Plaintext
80 lines
1.7 KiB
Plaintext
;; lib/minikanren/intarith.sx — fast integer arithmetic via project.
|
|
;;
|
|
;; These are ground-only escapes into host arithmetic. They run at native
|
|
;; speed (host ints) but require their arguments to walk to actual numbers
|
|
;; — they are not relational the way `pluso` (Peano) is. Use them when
|
|
;; the puzzle size makes Peano impractical.
|
|
;;
|
|
;; Naming: `-i` suffix marks "integer-only" goals.
|
|
|
|
(define
|
|
pluso-i
|
|
(fn
|
|
(a b c)
|
|
(project
|
|
(a b)
|
|
(if (and (number? a) (number? b)) (== c (+ a b)) fail))))
|
|
|
|
(define
|
|
minuso-i
|
|
(fn
|
|
(a b c)
|
|
(project
|
|
(a b)
|
|
(if (and (number? a) (number? b)) (== c (- a b)) fail))))
|
|
|
|
(define
|
|
*o-i
|
|
(fn
|
|
(a b c)
|
|
(project
|
|
(a b)
|
|
(if (and (number? a) (number? b)) (== c (* a b)) fail))))
|
|
|
|
(define
|
|
lto-i
|
|
(fn
|
|
(a b)
|
|
(project
|
|
(a b)
|
|
(if (and (number? a) (and (number? b) (< a b))) succeed fail))))
|
|
|
|
(define
|
|
lteo-i
|
|
(fn
|
|
(a b)
|
|
(project
|
|
(a b)
|
|
(if (and (number? a) (and (number? b) (<= a b))) succeed fail))))
|
|
|
|
(define
|
|
neqo-i
|
|
(fn
|
|
(a b)
|
|
(project
|
|
(a b)
|
|
(if (and (number? a) (and (number? b) (not (= a b)))) succeed fail))))
|
|
|
|
(define numbero (fn (x) (project (x) (if (number? x) succeed fail))))
|
|
|
|
(define stringo (fn (x) (project (x) (if (string? x) succeed fail))))
|
|
|
|
(define symbolo (fn (x) (project (x) (if (symbol? x) succeed fail))))
|
|
|
|
(define
|
|
even-i
|
|
(fn (n) (project (n) (if (and (number? n) (even? n)) succeed fail))))
|
|
|
|
(define
|
|
odd-i
|
|
(fn (n) (project (n) (if (and (number? n) (odd? n)) succeed fail))))
|
|
|
|
(define
|
|
sortedo
|
|
(fn
|
|
(l)
|
|
(conde
|
|
((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))))))
|