; Equivalent to example/houses.adb


(define (value bin)
  (cond
    ((null? bin) 0)
    ((zero? (car bin)) (* 2 (value (cdr bin))))
    (#t (+ 1 (* 2 (value (cdr bin)))))))


(define (do-unique x li)
  (fresh (h t)
    (caro li h)
    (cdro li t)
    (conde
      ((<o x h))
      ((<o h x)))
    (conde
      ((== t '()))
      ((do-unique x t)))))


(define (unique li)
  (fresh (h t)
    (caro li h)
    (cdro li t)
    (conde
      ((== t '()))
      ((do-unique h t) (unique t)))))


(define (within-range v l h)
  (conde
    ((<=o l v) (<=o v h))
    (fail)))


(define (doors-from a d b)
  (conde
    ((pluso a d b))
    ((minuso a d b))))


(define (houses a1 a2 b1 b2 c1 c2 d1 d2)
  (conde
    ((within-range a1 (build-num 3) (build-num 8))
     (within-range a2 (build-num 2) (build-num 8))
     (within-range b1 (build-num 6) (build-num 8))
     (within-range b2 (build-num 4) (build-num 7))
     (within-range c1 (build-num 5) (build-num 8))
     (within-range c2 (build-num 2) (build-num 8))
     (within-range d1 (build-num 1) (build-num 3))
     (within-range d2 (build-num 5) (build-num 7))

     (unique `(,a1 ,a2 ,b1 ,b2 ,c1 ,c2 ,d1 ,d2))

     (doors-from a1 (build-num 1) a2)
     (doors-from b1 (build-num 2) b2)
     (doors-from c1 (build-num 3) c2)
     (doors-from d1 (build-num 4) d2)

     (<o b2 c1))
    (fail)))


(define (run-houses args)
  (let*
      ((s (run 1 (h)
          (fresh (s t u v w x y z)
            (== h `(,s ,t ,u ,v ,w ,x ,y ,z))
            (houses s t u v w x y z))))
       (r (car s)))
    (begin
      (display (string-append "Allison: "  (number->string (value (list-ref r 0))))) (newline)
      (display (string-append "Adrienne: " (number->string (value (list-ref r 1))))) (newline)
      (display (string-append "Belinda: "  (number->string (value (list-ref r 2))))) (newline)
      (display (string-append "Benito: "   (number->string (value (list-ref r 3))))) (newline)
      (display (string-append "Cheri: "    (number->string (value (list-ref r 4))))) (newline)
      (display (string-append "Crawford: " (number->string (value (list-ref r 5))))) (newline)
      (display (string-append "Daryl: "    (number->string (value (list-ref r 6))))) (newline)
      (display (string-append "Don: "      (number->string (value (list-ref r 7))))) (newline))))