;;; C311 miniKanren Interpreter

(load "mk.scm")
(load "mkneverequalo.scm")
(load "mkdefs.scm")

;;; --- represents code you must fill in
(define --- '---)

;;; The interpreter

(define eval-expo
  (lambda (expr env out)
    (conde
      ((exists (n)
         (== `(intc ,n) expr)
         ---))
      ((exists (b)
         (== `(boolc ,b) expr)
         ---))
      ((exists (id body)
         (== `(lambda (,id) ,body) expr)
         ---))
      ((exists (x)
         (== `(var ,x) expr)
         ---))
      ((exists (x res n)
         (== `(zero? ,x) expr)
         ---))
      ((exists (x n n-1)
         (== `(sub1 ,x) expr)
         ---))
      ((exists (x1 x2 n m p)
         (== `(* ,x1 ,x2) expr)
         ---))
      ((exists (test conseq alt b)
         (== `(if ,test ,conseq ,alt) expr)
         ---))
      ((exists (rator rand id body res env^ env^^)
         (== `(app ,rator ,rand) expr)
         ---)))))


;;; Environment relations

(define base-envo
  (lambda (env)
    ---))

(define extend-envo
  (lambda (x v env env^)
    ---))

(define apply-envo
  (lambda (env x val)
    ---))



;;; Tests

(define-syntax test
  (syntax-rules ()
    ((_ title tested-expression expected-result)
     (let* ((expected expected-result)
            (produced tested-expression))
       (if (equal? expected produced)
           (printf "~s works!\n" title)
           (error
             'test
             "Failed ~s: ~a~%Expected: ~a~%Computed: ~a"
             title 'tested-expression expected produced))))))

(define parse
  (lambda (e)
    (cond
      [(symbol? e) `(var ,e)]
      [(number? e) `(intc ,(build-num e))]
      [(boolean? e) `(boolc ,e)]
      [else
	(case (car e)
	  [(sub1) `(sub1 ,(parse (cadr e)))]
	  [(+) `(+ ,(parse (cadr e)) ,(parse (caddr e)))]
	  [(*) `(* ,(parse (cadr e)) ,(parse (caddr e)))]
	  [(car) `(car ,(parse (cadr e)))]
	  [(cdr) `(cdr ,(parse (cadr e)))]
	  [(cons) `(cons ,(parse (cadr e)) ,(parse (caddr e)))]
	  [(fix) `(fix ,(parse (cadr e)))]
	  [(zero?) `(zero? ,(parse (cadr e)))]
	  [(if) `(if ,(parse (cadr e)) ,(parse (caddr e)) ,(parse (cadddr e)))]
	  [(lambda) `(lambda ,(cadr e) ,(parse (caddr e)))]
	  [else `(app ,(parse (car e)) ,(parse (cadr e)))])])))

(test "int"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo (parse '5) env q)))
  (list `(int ,(build-num 5))))

(test "bool-1"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo (parse '#t) env q)))
  (list `(bool #t)))

(test "bool-2"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo (parse '#f) env q)))
  (list `(bool #f)))

(test "zero?-1"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '(zero? 0))
       env
       q)))
    '((bool #t)))

(test "zero?-2"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '(zero? 1))
       env
       q)))
    '((bool #f)))

(test "sub1-1"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '(sub1 0))
       env
       q)))
    '())

(test "sub1-2"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '(sub1 1))
       env
       q)))
    '((int ())))

(test "*"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '(* 5 4))
       env
       q)))
    (list `(int ,(build-num 20))))

(test "if-1"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '(if #t 3 4))
       env
       q)))
    (list `(int ,(build-num 3))))

(test "if-2"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '(if #f 3 4))
       env
       q)))
    (list `(int ,(build-num 4))))

(test "lambda"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '(lambda (x) (* x x)))
       env
       q)))
    '((closure x (* (var x) (var x)) ())))

(test "app-0"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '((lambda (x) 5)  4))
       env
       q)))
  '((int (1 0 1))))

(test "app-1"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       (parse '((lambda (x) (* x x))  4))
       env
       q)))
    (list `(int ,(build-num 16))))

(test "app-2"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	(parse '((lambda (n) (zero? n)) 7))
	env
	q)))
  '((bool #f)))

(test "app-3"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	(parse '((lambda (n) (zero? n)) (sub1 1)))
	env
	q)))
  '((bool #t)))

(define fact-5
  '(app (lambda (f)
          (app (app (var f) (var f)) (intc (1 0 1))))
        (lambda (f)
          (lambda (n)
            (if (zero? (var n))
                (intc (1))
                (* (var n) (app (app (var f) (var f)) (sub1 (var n)))))))))

(test "fact-5"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo fact-5 env q)))
  (list `(int ,(build-num 120))))

(test "generate"
  (length (run 20 (q)
    (exists (exp env out)
      (eval-expo exp env out)
      (== `(,exp ,env ,out) q))))
  20)

(test "six"
  (length (run 50 (q)
    (exists (env)
      (base-envo env)
      (eval-expo q env `(int ,(build-num 6))))))
   50)

(test "fact-5-reverse"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var f)) (intc ,q)))
	   (lambda (f)
	     (lambda (n)
	       (if (zero? (var n))
		 (intc (1))
		 (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== '(1 1) q)))
  '((1 1)))

(test "fact-5-reverse-2"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var f)) ,q))
	   (lambda (f)
	     (lambda (n)
	       (if (zero? (var n))
		 (intc (1))
		 (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== '(intc (1 1)) q)))
  '((intc (1 1))))

(test "fact-5-reverse-3"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var ,q)) (intc (1 1))))
	   (lambda (f)
	     (lambda (n)
	       (if (zero? (var n))
		 (intc (1))
		 (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== 'f q)))
  '(f))

(test "fact-5-reverse-4"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var f)) (intc (1 1))))
	   (lambda (f)
	     (lambda (n)
	       (if (zero? (var n))
		 (intc ,q)
		 (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== '(1) q)))
  '((1)))

(test "fact-5-reverse-5"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var f)) (intc (1 1))))
	   (lambda (f)
	     (lambda (n)
	       (if (zero? (var ,q))
		 (intc (1))
		 (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== 'n q)))
  '(n))

(test "fact-5-reverse-6"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var f)) (intc (1 1))))
	   (lambda (f)
	     (lambda (n)
	       (if (zero? ,q)
		 (intc (1))
		 (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== '(var n) q)))
  '((var n)))

(test "fact-5-reverse-7"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var f)) (intc (1 1))))
	   (lambda (f)
	     (lambda (n)
	       (if ,q
		 (intc (1))
		 (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== '(zero? (var n)) q)))
  '((zero? (var n))))

(test "fact-5-reverse-8"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var f)) (intc (1 1))))
	   (lambda (f)
	     (lambda (n)
	       (if (zero? (var n))
		 (intc (1))
		 (* (var n) (app (app (var f) ,q) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== `(var f) q)))
  '((var f)))

(test "fact-5-reverse-9"
  (run 1 (q)
    (exists (env)
      (base-envo env)
      (eval-expo
	`(app (lambda (f)
		(app (app (var f) (var f)) (intc (1 1))))
	   (lambda (f)
	     (lambda (n)
	       (if (zero? (var n))
		 (intc (1))
		 (* ,q (app (app (var f) (var f)) (sub1 (var n))))))))
	env
	`(int ,(build-num 6)))
      (== `(var n) q)))
  '((var n)))

(test "almost-fact"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       `(app (lambda (f)
               (app (app (var f) (var f)) (intc (1 1))))
             (lambda (f)
               (lambda (n)
                 (if (zero? (intc ()))
                     (intc (1))
                     (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
       env
       q)))
  '((int (1))))

(test "almost-fact-2"
  (run* (q)
    (exists (env)
      (base-envo env)
      (eval-expo
       `(app (lambda (f)
               (app (app (var f) (var f)) (intc (1 1))))
             (lambda (f)
               (lambda (n)
                 (if (boolc #t)
                     (intc (1))
                     (* (var n) (app (app (var f) (var f)) (sub1 (var n))))))))
       env
       q)))
  '((int (1))))