logic.rkt

#lang racket

(provide (all-defined-out))

(define var (lambda (x) (vector x)))
(define var? (lambda (x) (vector? x)))

(define empty-s '())

(define (walk v s)
  (let ((a (and (var? v) (assv v s))))
    (cond
      ((pair? a) (walk (cdr a) s))
      (else v))))

(define (ext-s x v s)
  (cond
    ((occurs? x v s) #f)
    (else (cons `(,x . ,v) s))))

(define (occurs? x v s)
  (let ((v (walk v s)))
    (cond
      ((var? v) (eqv? v x))
      ((pair? v) 
       (or (occurs? x (car v) s)
           (occurs? x (cdr v) s)))
      (else #f))))

(define (unify u v s)
  (let ((u (walk u s)) (v (walk v s)))
    (cond
      ((eqv? u v) s)
      ((var? u) (ext-s u v s))
      ((var? v) (ext-s v u s))
      ((and (pair? u) (pair? v))
       (let ((s (unify (car u) (car v) s)))
         (and s
           (unify (cdr u) (cdr v) s))))
      (else #f))))

(define (== u v)
  (lambda (s)
    (let ((s (unify u v s)))
      (if s `(,s) '()))))

(define succeed
  (lambda (s)
    `(,s)))
 
(define fail
  (lambda (s)
    '()))

(define (disj2 g1 g2)
  (lambda (s)
    (append-inf (g1 s) (g2 s))))

(define (append-inf s-inf t-inf)
  (cond
    ((null? s-inf) t-inf)
    ((pair? s-inf) 
     (cons (car s-inf)
       (append-inf (cdr s-inf) t-inf)))
    (else (lambda () 
            (append-inf t-inf (s-inf))))))

(define (take-inf n s-inf)
  (cond
    ((and n (zero? n)) '())
    ((null? s-inf) '())
    ((pair? s-inf) 
     (cons (car s-inf)
       (take-inf (and n (sub1 n))
         (cdr s-inf))))
    (else (take-inf n (s-inf)))))

(define (conj2 g1 g2)
  (lambda (s)
    (append-map-inf g2 (g1 s))))

(define (append-map-inf g s-inf)
  (cond
    ((null? s-inf) '())
    ((pair? s-inf)
     (append-inf (g (car s-inf))
       (append-map-inf g (cdr s-inf))))
    (else (lambda () 
            (append-map-inf g (s-inf))))))

(define (call/fresh name f)
  (f (var name)))

(define (reify-name n)
  (string->symbol
    (string-append "_"
      (number->string n))))

(define (walk* v s)
  (let ((v (walk v s)))
    (cond
      ((var? v) v)
      ((pair? v)
       (cons
         (walk* (car v) s)
         (walk* (cdr v) s)))
      (else v))))

; 'project' is defined in the frame 10:98 on page 166.
(define-syntax project
  (syntax-rules ()
    ((project (x ...) g ...)
     (lambda (s)
       (let ((x (walk* x s)) ...)
         ((conj g ...) s))))))

(define (reify-s v r)
  (let ((v (walk v r)))
    (cond
      ((var? v)
       (let ((n (length r)))
         (let ((rn (reify-name n)))
           (cons `(,v . ,rn) r))))
      ((pair? v)
       (let ((r (reify-s (car v) r)))
         (reify-s (cdr v) r)))
      (else r))))

(define (reify v)
  (lambda (s)
    (let ((v (walk* v s)))
      (let ((r (reify-s v empty-s)))
        (walk* v r)))))

(define (run-goal n g)
  (take-inf n (g empty-s)))

(define (ifte g1 g2 g3)
  (lambda (s)
    (let loop ((s-inf (g1 s)))
      (cond
        ((null? s-inf) (g3 s))
        ((pair? s-inf)
         (append-map-inf g2 s-inf))
        (else (lambda ()
                (loop (s-inf))))))))

(define (once g)
  (lambda (s)
    (let loop ((s-inf (g s)))
      (cond
        ((null? s-inf) '())
        ((pair? s-inf)
         (cons (car s-inf) '()))
        (else (lambda ()
                (loop (s-inf))))))))


;;; Here are the key parts of Appendix A

(define-syntax disj
  (syntax-rules ()
    ((disj) fail)
    ((disj g) g)
    ((disj g0 g ...) (disj2 g0 (disj g ...)))))

(define-syntax conj
  (syntax-rules ()
    ((conj) succeed)
    ((conj g) g)
    ((conj g0 g ...) (conj2 g0 (conj g ...)))))

(define-syntax defrel
  (syntax-rules ()
    ((defrel (name x ...) g ...)
     (define (name x ...)
       (lambda (s)
         (lambda ()
           ((conj g ...) s)))))))

(define-syntax run
  (syntax-rules ()
    ((run n (x0 x ...) g ...)
     (run n q (fresh (x0 x ...)
                (== `(,x0 ,x ...) q) g ...)))
    ((run n q g ...)
     (let ((q (var 'q)))
       (map (reify q)
         (run-goal n (conj g ...)))))))

(define-syntax run*
  (syntax-rules ()
    ((run* q g ...) (run #f q g ...))))

(define-syntax fresh
  (syntax-rules ()
    ((fresh () g ...) (conj g ...))
    ((fresh (x0 x ...) g ...)
     (call/fresh 'x_0
       (lambda (x0)
         (fresh (x ...) g ...))))))

(define-syntax conde
  (syntax-rules ()
    ((conde (g ...) ...)
     (disj (conj g ...) ...))))

(define-syntax conda
  (syntax-rules ()
    ((conda (g0 g ...)) (conj g0 g ...))
    ((conda (g0 g ...) ln ...)
     (ifte g0 (conj g ...) (conda ln ...)))))

(define-syntax condu
  (syntax-rules ()
    ((condu (g0 g ...) ...)
     (conda ((once g0) g ...) ...))))

;; Arithmitic operations
; Helper definitions from Chapters 2 and 4.
(defrel (nullo x)
  (== '() x))

(defrel (conso a d p)
  (== `(,a . ,d) p))

(defrel (caro p a)
  (fresh (d)
    (== (cons a d) p)))

(defrel (cdro p d)
  (fresh (a)
    (== (cons a d) p)))

(defrel (appendo l t out)
  (conde
    ((nullo l) (== t out))
    ((fresh (a d res)
       (conso a d l)
       (conso a res out)
       (appendo d t res)))))



;;; Here are the key parts of Chapter 7
(defrel (bit-xoro x y r)
  (conde
    ((== 0 x) (== 0 y) (== 0 r))
    ((== 0 x) (== 1 y) (== 1 r))
    ((== 1 x) (== 0 y) (== 1 r))
    ((== 1 x) (== 1 y) (== 0 r))))

(defrel (bit-ando x y r)
  (conde
    ((== 0 x) (== 0 y) (== 0 r))
    ((== 1 x) (== 0 y) (== 0 r))
    ((== 0 x) (== 1 y) (== 0 r))
    ((== 1 x) (== 1 y) (== 1 r))))


(defrel (half-addero x y r c)
  (bit-xoro x y r)
  (bit-ando x y c))

; Alternative definition of 'half-addero' from frame 7:12 on page 87.
#;(defrel (half-addero x y r c)
  (conde
    ((== 0 x) (== 0 y) (== 0 r) (== 0 c))
    ((== 1 x) (== 0 y) (== 1 r) (== 0 c))
    ((== 0 x) (== 1 y) (== 1 r) (== 0 c))
    ((== 1 x) (== 1 y) (== 0 r) (== 1 c))))



; Definition of 'full-addero' from frame 7:15 on page 87.
#;(defrel (full-addero b x y r c)
  (fresh (w xy wz)
    (half-addero x y w xy)
    (half-addero w b r wz)
    (bit-xoro xy wz c)))

; Alternative definition of 'full-addero' from frame 7:15 on page 87.
;
; For performance reasons, we use this explicit table version of
; 'full-addero' (which no longer uses 'half-addero').
(defrel (full-addero b x y r c)
  (conde
    ((== 0 b) (== 0 x) (== 0 y) (== 0 r) (== 0 c))
    ((== 1 b) (== 0 x) (== 0 y) (== 1 r) (== 0 c))
    ((== 0 b) (== 1 x) (== 0 y) (== 1 r) (== 0 c))
    ((== 1 b) (== 1 x) (== 0 y) (== 0 r) (== 1 c))
    ((== 0 b) (== 0 x) (== 1 y) (== 1 r) (== 0 c))
    ((== 1 b) (== 0 x) (== 1 y) (== 0 r) (== 1 c))
    ((== 0 b) (== 1 x) (== 1 y) (== 0 r) (== 1 c))
    ((== 1 b) (== 1 x) (== 1 y) (== 1 r) (== 1 c))))


(define (build-num n)
  (cond
    ((zero? n) '())
    ((even? n)
     (cons 0
       (build-num (quotient n 2))))
    ((odd? n)
     (cons 1
       (build-num (quotient (- n 1) 2))))))

(defrel (poso n)
  (fresh (a d)
    (== `(,a . ,d) n)))

(defrel (>1o n)
  (fresh (a ad dd)
    (== `(,a ,ad . ,dd) n)))

(defrel (addero b n m r)
  (conde
    ((== 0 b) (== '() m) (== n r))
    ((== 0 b) (== '() n) (== m r)
     (poso m))
    ((== 1 b) (== '() m)
     (addero 0 n '(1) r))
    ((== 1 b) (== '() n) (poso m)
     (addero 0 '(1) m r))
    ((== '(1) n) (== '(1) m)
     (fresh (a c)
       (== `(,a ,c) r)
       (full-addero b 1 1 a c)))
    ((== '(1) n) (gen-addero b n m r))
    ((== '(1) m) (>1o n) (>1o r)
     (addero b '(1) n r))
    ((>1o n) (gen-addero b n m r))))

(defrel (gen-addero b n m r)
  (fresh (a c d e x y z)
    (== `(,a . ,x) n)
    (== `(,d . ,y) m) (poso y)
    (== `(,c . ,z) r) (poso z)
    (full-addero b a d c e)
    (addero e x y z)))

(defrel (pluso n m k)
  (addero 0 n m k))

(defrel (minuso n m k)
  (pluso m k n))

;;; Here are the key parts of Chapter 8
(defrel (*o n m p)
  (conde
    ((== '() n) (== '() p))
    ((poso n) (== '() m) (== '() p))  
    ((== '(1) n) (poso m) (== m p))   
    ((>1o n) (== '(1) m) (== n p))
    ((fresh (x z)
       (== `(0 . ,x) n) (poso x)
       (== `(0 . ,z) p) (poso z)
       (>1o m)
       (*o x m z)))
    ((fresh (x y)
       (== `(1 . ,x) n) (poso x)
       (== `(0 . ,y) m) (poso y)
       (*o m n p)))
    ((fresh (x y)
       (== `(1 . ,x) n) (poso x)      
       (== `(1 . ,y) m) (poso y)
       (odd-*o x n m p)))))

(defrel (odd-*o x n m p)
  (fresh (q)
    (bound-*o q p n m)
    (*o x m q)
    (pluso `(0 . ,q) m p)))

(defrel (bound-*o q p n m)
  (conde
    ((== '() q) (poso p))
    ((fresh (a0 a1 a2 a3 x y z)
       (== `(,a0 . ,x) q)
       (== `(,a1 . ,y) p)
       (conde
         ((== '() n)
          (== `(,a2 . ,z) m)
          (bound-*o x y z '()))
         ((== `(,a3 . ,z) n) 
          (bound-*o x y z m)))))))

(defrel (=lo n m)
  (conde
    ((== '() n) (== '() m))
    ((== '(1) n) (== '(1) m))
    ((fresh (a x b y)
       (== `(,a . ,x) n) (poso x)
       (== `(,b . ,y) m) (poso y)
       (=lo x y)))))

(defrel (<lo n m)
  (conde
    ((== '() n) (poso m))
    ((== '(1) n) (>1o m))
    ((fresh (a x b y)
       (== `(,a . ,x) n) (poso x)
       (== `(,b . ,y) m) (poso y)
       (<lo x y)))))

(defrel (<=lo n m)
  (conde
    ((=lo n m))
    ((<lo n m))))

(defrel (<o n m)
  (conde
    ((<lo n m))
    ((=lo n m)
     (fresh (x)
       (poso x)
       (pluso n x m)))))

(defrel (<=o n m)
  (conde
    ((== n m))
    ((<o n m))))

; Flawed definition of '/o' from frame 8:54 on page 118.
#;(defrel (/o n m q r)
  (conde
    ((== '() q) (== n r) (<o n m))
    ((== '(1) q) (== '() r) (== n m)
     (<o r m))      
    ((<o m n) (<o r m)
     (fresh (mq)
       (<=lo mq n)
       (*o m q mq)
       (pluso mq r n)))))

; Flawed definition of '/o' from frame 8:64 on page 120.
#;(defrel (/o n m q r)
  (fresh (mq)
    (<o r m)
    (<=lo mq n)
    (*o m q mq)
    (pluso mq r n)))

(defrel (splito n r l h)
  (conde
    ((== '() n) (== '() h) (== '() l))
    ((fresh (b n^)
       (== `(0 ,b . ,n^) n) (== '() r)
       (== `(,b . ,n^) h) (== '() l)))
    ((fresh (n^)
       (==  `(1 . ,n^) n) (== '() r)
       (== n^ h) (== '(1) l)))
    ((fresh (b n^ a r^)
       (== `(0 ,b . ,n^) n)
       (== `(,a . ,r^) r) (== '() l)
       (splito `(,b . ,n^) r^ '() h)))
    ((fresh (n^ a r^)
       (== `(1 . ,n^) n)
       (== `(,a . ,r^) r) (== '(1) l)
       (splito n^ r^ '() h)))
    ((fresh (b n^ a r^ l^)
       (== `(,b . ,n^) n)
       (== `(,a . ,r^) r)
       (== `(,b . ,l^) l)
       (poso l^)
       (splito n^ r^ l^ h)))))

; Final definition of '/o' from frame 8:81 on page 124.
(defrel (/o n m q r)
  (conde
    ((== '() q) (== r n) (<o n m))
    ((== '(1) q) (=lo m n) (pluso r m n)
     (<o r m))
    ((poso q) (<lo m n) (<o r m)
     (n-wider-than-mo n m q r))))

(defrel (n-wider-than-mo n m q r)
  (fresh (nh nl qh ql)
    (fresh (mql mrql rr rh)
      (splito n r nl nh)
      (splito q r ql qh)
      (conde
        ((== '() nh)
         (== '() qh)
         (minuso nl r mql)
         (*o m ql mql))
        ((poso nh)
         (*o m ql mql)
         (pluso r mql mrql)
         (minuso mrql nl rr)
         (splito rr r '() rh)
         (/o nh m qh rh))))))

(defrel (logo n b q r)
  (conde
    ((== '() q) (<=o n b)
     (pluso r '(1) n))
    ((== '(1) q) (>1o b) (=lo n b)
     (pluso r b n))
    ((== '(1) b) (poso q)
     (pluso r '(1) n))
    ((== '() b) (poso q) (== r n))
    ((== '(0 1) b)
     (fresh (a ad dd)
       (poso dd)
       (== `(,a ,ad . ,dd) n)
       (exp2o n '() q)
       (fresh (s)
         (splito n dd r s))))
    ((<=o '(1 1) b) (<lo b n)
     (base-three-or-moreo n b q r))))

(defrel (exp2o n b q)
  (conde
    ((== '(1) n) (== '() q))
    ((>1o n) (== '(1) q)
     (fresh (s)
       (splito n b s '(1))))
    ((fresh (q1 b2)
       (== `(0 . ,q1) q) (poso q1)
       (<lo b n)
       (appendo b `(1 . ,b) b2)
       (exp2o n b2 q1)))
    ((fresh (q1 nh b2 s)
       (== `(1 . ,q1) q) (poso q1)
       (poso nh)
       (splito n b s nh)
       (appendo b `(1 . ,b) b2)
       (exp2o nh b2 q1)))))

(defrel (base-three-or-moreo n b q r)
  (fresh (bw1 bw nw nw1 ql1 ql s)
    (exp2o b '() bw1)
    (pluso bw1 '(1) bw)
    (<lo q n)
    (fresh (q1 bwq1)
      (pluso q '(1) q1)
      (*o bw q1 bwq1)
      (<o nw1 bwq1))
    (exp2o n '() nw1)
    (pluso nw1 '(1) nw)
    (/o nw bw ql1 s)
    (pluso ql '(1) ql1)
    (<=lo ql q)
    (fresh (bql qh s qdh qd)
      (repeated-mulo b ql bql)
      (/o nw bw1 qh s)
      (pluso ql qdh qh)
      (pluso ql qd q)
      (<=o qd qdh)
      (fresh (bqd bq1 bq)
        (repeated-mulo b qd bqd)
        (*o bql bqd bq)
        (*o b bq bq1)
        (pluso bq r n)
        (<o n bq1)))))

(defrel (repeated-mulo n q nq)
  (conde
    ((poso n) (== '() q) (== '(1) nq))
    ((== '(1) q) (== n nq))
    ((>1o q)
     (fresh (q1 nq1)
       (pluso q1 '(1) q)
       (repeated-mulo n q1 nq1)
       (*o nq1 n nq)))))

(defrel (expo b q n)
  (logo n b q '()))