;; 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))))))

(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))))))))

(define
  sumo
  (fn
    (l total)
    (conde
      ((nullo l) (== total 0))
      ((fresh (a d rest-sum) (conso a d l) (sumo d rest-sum) (pluso-i a rest-sum total))))))

(define
  producto
  (fn
    (l total)
    (conde
      ((nullo l) (== total 1))
      ((fresh (a d rest-prod) (conso a d l) (producto d rest-prod) (*o-i a rest-prod total))))))

(define
  lengtho-i
  (fn
    (l n)
    (conde
      ((nullo l) (== n 0))
      ((fresh (a d n-1) (conso a d l) (lengtho-i d n-1) (pluso-i 1 n-1 n))))))

(define
  enumerate-from-i
  (fn
    (start l result)
    (conde
      ((nullo l) (nullo result))
      ((fresh (a d r-rest start-prime) (conso a d l) (conso (list start a) r-rest result) (pluso-i 1 start start-prime) (enumerate-from-i start-prime d r-rest))))))

(define enumerate-i (fn (l result) (enumerate-from-i 0 l result)))

(define
  counto
  (fn
    (x l n)
    (conde
      ((nullo l) (== n 0))
      ((fresh (a d n-rest) (conso a d l) (conde ((== a x) (counto x d n-rest) (pluso-i 1 n-rest n)) ((nafc (== a x)) (counto x d n))))))))

(define
  mk-arith-prog
  (fn
    (start step len)
    (cond
      ((= len 0) (list))
      (:else (cons start (mk-arith-prog (+ start step) step (- len 1)))))))

(define
  arith-progo
  (fn
    (start step len result)
    (project (start step len) (== result (mk-arith-prog start step len)))))