mk: intarith.sx — ground-only integer arithmetic via project
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic in project. They run at native speed but require their inputs to walk to ground numbers — they are NOT relational the way Peano pluso is. Use them when puzzle size makes Peano impractical (which is most cases beyond toy examples). Composes with relational goals — for instance, (fresh (x) (membero x (1 2 3 4 5)) (lto-i x 3) (== q x)) filters the domain by < 3 and returns (1 2). 18 new tests, 287/287 cumulative.
This commit is contained in:
56
lib/minikanren/intarith.sx
Normal file
56
lib/minikanren/intarith.sx
Normal file
@@ -0,0 +1,56 @@
|
||||
;; 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))))
|
||||
Reference in New Issue
Block a user