Annotated code from Steve

gistfile1.rkt

#lang racket
(require "miniKanren/mk.rkt")

; changed name of goal to be more descriptive
(define (key-not-boundo key env)
  (conde
   [(== '() env)] ; swapped conde clauses to make the non-recursive
                  ; clause come first; not necessary, but could
                  ; improve efficiency
   [(fresh (k v rest)
      (== `((,k . ,v) . ,rest) env)
      (=/= k key)
      (key-not-boundo key rest))]))

(define (get-varo key env val)
  (fresh (k v rest)
    (== `((,k . ,v) . ,rest) env)
    (conde
     [(== k key)
      (== v val)]
     [(=/= k key) ; better have this test to prevent multiple bindings
                  ; for the same variable.
      (get-varo key rest val)])))

(define (ando a b r)
  (conde
   [(== a #t) (== b #t) (== r #t)]
   [(== a #f) (== b #t) (== r #f)]
   [(== a #t) (== b #f) (== r #f)]
   [(== a #f) (== b #f) (== r #f)]))

(define (oro a b r)
  (conde
   [(== a #t) (== b #t) (== r #t)]
   [(== a #f) (== b #t) (== r #t)]
   [(== a #t) (== b #f) (== r #t)]
   [(== a #f) (== b #f) (== r #f)]))

(define (noto x v)
  (conde
   [(== x #t) (== v #f)]
   [(== x #f) (== v #t)]))

(define (boolo b)
  (conde
   [(== b #t)]
   [(== b #f)]))

(define (expressiono exp env-in env-out val)
  (conde
   [(boolo exp)
    (== env-in env-out)
    (== exp val)]
   [(symbolo exp) ; consolidated symbolo clauses
    (conde
      [;; unifications should come before
       ;; recursive/potentially divergent goals
       ;;
       ;; no need for the 'v' variable
       (== env-out `((,exp . ,val) . ,env-in))
       (key-not-boundo exp env-in)]
      [(== env-in env-out) ;; unifications should come before
                           ;; recursive/potentially divergent goals
       (get-varo exp env-in val)])]
   [(fresh (e v) ;; moved NOT clause before AND and OR, since it has
                 ;; only one recursive call.  Not necessary, but could
                 ;; improve efficiency
      (== `(NOT ,e) exp)
      (noto v val) ;; moved noto about recursion
      (expressiono e env-in env-out v))]
   [(fresh (e1 e2 v1 v2 env*)
      (== `(AND ,e1 ,e2) exp)
      (ando v1 v2 val) ;; moved ando above recursive calls, since ando
                       ;; can succeed only a finite number of times
      (expressiono e1 env-in env* v1)
      (expressiono e2 env* env-out v2))]
   [(fresh (e1 e2 v1 v2 env*)
      (== `(OR ,e1 ,e2) exp)
      (oro v1 v2 val) ;; moved oro above recursions
      (expressiono e1 env-in env* v1)
      (expressiono e2 env* env-out v2))]))

(define (assertiono a env-in env-out)
  (conde
   [(fresh (e1 e2 v1 v2 env*)
      ;; Moved IFF clause above IF, since there is the same number of
      ;; recursive calls, but IFF clause doesn't have the conde.
      ;; Npt strictly necessary, but could improve efficiency.
      (== `(IFF ,e1 ,e2) a)
      (== v1 v2) ;; moved unification above recursive calls
      ;;
      ;; Actually, could use just a single 'v' variable rather than
      ;; 'v1' and 'v2' (which also would get rid of the call to ==)
      (expressiono e1 env-in env* v1)
      (expressiono e2 env* env-out v2))]
   [(fresh (e1 e2 v1 v2 env*)
      (== `(IF ,e1 ,e2) a)
      ;; moved conde above recursive calls, since the conde produces
      ;; finitely many answers
      (conde
        [(== #t v1) (== #t v2)]
        [(== #f v1) (== #t v2)]
        [(== #f v1) (== #f v2)])
      (expressiono e1 env-in env* v1)
      (expressiono e2 env* env-out v2))]))

(define (eval-manyo as env-in env-out)
  (conde
   [(== `() as) ;; moved base case clause above recursive call, for
                ;; efficiency
    (== env-in env-out)]
   [(fresh (f r env* v)
      (== (cons f r) as)
      (assertiono f env-in env*)
      (eval-manyo r env* env-out))]))

(define (evaluate-assertions . assertions)
  (run* (q)
    (eval-manyo assertions `() q)))

(module+ test (require rackunit)
  (check-equal? (run* (q) (oro #t #f q))
                `(#t))
  (check-equal? (run* (q) (ando #t #f q))
                `(#f))
  (check-equal? (run* (q) (ando #t #t q))
                `(#t))
  (check-equal? (run* (q) (noto #t q))
                `(#f))
  (check-equal? (run* (q) (expressiono `foo `() q #t))
                `(((foo . #t))))
  (check-equal? (run* (q) (expressiono #t `() `() q))
                `(#t))
  (check-equal? (run* (q) (fresh (a) (expressiono `foo `((foo . #f)) a q)))
                `(#f))
  (check-equal? (run* (q) (fresh (a) (expressiono `foo `((foo . #f)) a q)))
                `(#f))
  (check-equal? (run* (q) (fresh (a) (expressiono `(AND foo #t) `((foo . #f)) a q)))
                `(#f))
  (check-equal? (run* (q) (fresh (a) (expressiono `(AND foo #t) `((foo . ,q)) a #f)))
                `(#f))
  (check-equal? (run* (q) (expressiono `(AND foo #t) `() q #f))
                `(((foo . #f))))
  (check-equal? (run* (q) (expressiono `(AND foo (NOT bar)) `((bar . #t)) q #t))
                `())
  (check-equal? (run* (q) (assertiono `(IF #t #t) `() `()))
                `(_.0))
  (check-equal? (run 1 (q) (assertiono `(IF #t ,q) `() `()))
                `(#t))
  (check-equal? (run 2 (q) (assertiono `(IF #f ,q) `() `()))
                `(#t #f))
  (check-equal? (run 1 (q) (eval-manyo `((IF a b) (IF b c) (IFF a #t)) `() q))
                `(((c . #t) (b . #t) (a . #t))))
  
  )