;;; C311 Spring 2008
;;; miniKanren Type Inferencer

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

(define unparse
  (lambda (e)
    (if (var? e) e
      (case (car e)
	[(sub1) `(sub1 ,(unparse (cadr e)))]
	[(+) `(+ ,(unparse (cadr e)) ,(unparse (caddr e)))]
	[(*) `(* ,(unparse (cadr e)) ,(unparse (caddr e)))]
	[(car) `(car ,(unparse (cadr e)))]
	[(cdr) `(cdr ,(unparse (cadr e)))]
	[(cons) `(cons ,(unparse (cadr e)) ,(unparse (caddr e)))]
	[(var) e]
	[(intc) e]
	[(boolc) e]
	[(fix) `(fix ,(unparse (cadr e)))]
	[(zero?) `(zero? ,(unparse (cadr e)))]
	[(if) `(if ,(unparse (cadr e))
		 ,(unparse (caddr e))
		 ,(unparse (cadddr e)))]
	[(lambda) `(lambda ,(cadr e) ,(unparse (caddr e)))]
	[(app) `(,(unparse (cadr e)) ,(unparse (caddr e)))]))))


(define == ==-check)


(define fix
  (lambda (f)
    (letrec ([g (lambda (x) ((f g) x))])
      g)))


(define !-int
  (lambda (gamma exp type)
    (exists (n)
      (== `(intc ,n) exp)
      (== 'int type))))

(define !-bool
  (lambda (gamma exp type)
    (exists (b)
      (== `(boolc ,b) exp)
      (== 'bool type))))

(define !-zero?
  (lambda (gamma exp type)
    (exists (n)
      (== `(zero? ,n) exp)
      (== 'bool type)
      (!- gamma n 'int))))

(define !-if
  (lambda (gamma exp type)
    (exists (test conseq alt)
      (== `(if ,test ,conseq ,alt) exp)
      (!- gamma test 'bool)
      (!- gamma conseq type)
      (!- gamma alt type))))

(define !-fix
  (lambda (gamma exp type)
    (exists (rand)
      (== `(fix ,rand) exp)
      (!- gamma rand `(-> ,type ,type)))))

(define !-var
  (lambda (gamma exp type)
    (exists (x)
      (== `(var ,x) exp)
      (lookup x gamma type))))

(define !-lambda
  (lambda (gamma exp type)
    (exists (x b tx tb gamma^)
      (== `(lambda (,x) ,b) exp)
      (== `(-> ,tx ,tb) type)
      (extend-env x tx gamma gamma^)
      (!- gamma^ b tb))))

(define !-app
  (lambda (gamma exp type)
    (exists (rator rand tn tb)
      (== `(app ,rator ,rand) exp)
      (== tb type)
      (!- gamma rator `(-> ,tn ,tb))
      (!- gamma rand tn))))

(define !-
  (lambda (gamma exp type)
    (exists (n m b test tn tb rator rand gamma^)
      (conde
        ((!-int gamma exp type))
        ((!-bool gamma exp type))
        ((!-fix gamma exp type))
        ((!-zero? gamma exp type))        
        ((!-var gamma exp type))
        ((!-lambda gamma exp type))        
        ((!-app gamma exp type))        
        ((!-if gamma exp type))))))

(define extend-env
  (lambda (x tx gamma gamma^)
    (== `((,x . ,tx) . ,gamma) gamma^)))

(define lookup
  (lambda (x gamma type)
    ---))


(test "1"
  (run* (q) (!- '() '(intc 17) q))
  '(int))

(test "2"
  (run* (q) (!- '() '(zero? (intc 24)) q))
  '(bool))

(test "3"
  (run* (q) (!- '() '(zero? (sub1 (intc 24))) q))
  '(bool))

(test "4"
  (run* (q)
    (!- '() '(zero? (sub1 (+ (intc 18) (+ (intc 24) (intc 50))))) q))
  '(bool))

(test "5"
  (run* (q)
    (!- '() (parse '(lambda (n) (if (zero? n) n n))) q))
  ' ((-> int int)))

(test "6"
  (run* (q)
    (!- '() (parse '((lambda (n) (zero? n)) 5)) q))  
  '(bool))

(test "7"
  (run* (q)
    (!- '() '(if (zero? (intc 24)) (intc 3) (intc 4)) q))
  '(int))

(test "8"
  (run* (q)
    (!- '() '(if (zero? (intc 24)) (zero? (intc 3)) (zero? (intc 4))) q))
  '(bool))

(test "9"
  (run* (q)
    (!- '() '(lambda (x) (+ (var x) (intc 5))) q))
  '((-> int int)))

(test "10"
  (run* (q)
    (!- '() '(lambda (a) (lambda (x) (+ (var x) (var a)))) q))
  '((-> int (-> int int))))

(test "11"
  (run* (q)
    (!- '() (parse '(lambda (f)
                      (lambda (x)
                        ((f x) x))))
      q))
  '((->
     (-> _.0 (-> _.0 _.1))
     (-> _.0 _.1))))

(test "12"
  (run* (q)
    (!- '() (parse '(+ 4 (* 5 (sub1 6)))) q))
  '(int))

(test "13"
  (run 1 (q)
    (exists (t)
      (!- '() (parse '(lambda (f) (f f))) t)))
  '())

(test "14"
  (run* (q)
    (!- '() (parse '((fix (lambda (!)
                            (lambda (n)
                              (if (zero? n)
                                  1
                                  (* (! (sub1 n)) n))))) 5))
        q))
  '(int))

(test "15"
  (run* (q)
    (!- '() (parse '(cons 5 4)) q))
  '((pair int int)))

(test "16"
  (run* (q)
    (!- '() (parse '(cdr (cons 5 4))) q))
  '(int))

(test "17"
  (run* (q)
    (!- '() (parse '(car (cons (cons 3 4) #t))) q))
  '((pair int int)))

(test "18"
  (run* (q)
    (!- '() (parse '(car (cdr (cons (cons 3 4) (cons #t #f))))) q))
  '(bool))

(test "19"
  (run* (q)
    (!- '() (parse '(cons (cons 3 (cons 5 #t)) (cons #f (cons (cons #t #f) 4)))) q))
  '((pair (pair int (pair int bool)) (pair bool (pair (pair bool bool) int)))))

(test "20"
  (run* (q)
    (!- '() (parse '((lambda (l) (car (cdr (cdr l)))) (cons 5 (cons 6 (cons 7 8))))) q))
  '(int))

(test "21"
  (run* (q)
    (!- '() (parse '((fix (lambda (sum)
                            (lambda (n)
                              (if (zero? n)
                                  0
                                  (+ n (sum (sub1 n)))))))
                     10))
        q))
  '(int))

(test "22"
  (run* (q)
    (!- '() '(app
              (fix
                (lambda (sum)
                  (lambda (n)
                    (if (if (zero? (var n)) (boolc #t) (boolc #f))
                        (intc 0)
                        (+ (var n) (app (var sum) (sub1 (var n))))))))
              (intc 10))
        q))
  '(int))

(test "23"
  (run* (q) 
    (!- '() (parse
              '((fix
                  (car
                    (cons
                      (lambda (sum)
                        (lambda (n)
                          (+ n (sum (sub1 (* n n))))))
                      (cdr (cons 3 4)))))
                10))
        q))
  '(int))

(test "24"
  (let ([v (run 20 (q)
             (exists (lam a b)
               (!- '() `(app (,lam (,a) ,b) (intc 5)) 'int)
               (== `(,lam (,a) ,b) q)))])
    (pretty-print v)
    (length v))
  20)

(test "25"
  (let ([v (run 30 (q)
             (!- '() q 'int))])
    (pretty-print v)
    (length v))
  30)

(test "26"
  (let ([v (run 30 (q)
             (!- '() q '(-> int int)))])
    (pretty-print v)
    (length v))
  30)

(test "27"
  (let ([v (run 30 (q)
             (!- '() q '(-> bool int)))])
    (pretty-print v)
    (length v))
  30)

(test "28"
  (let ([v (run 30 (q)
             (!- '() q '(-> int (-> int int))))])
    (pretty-print v)
    (length v))
  30)

(test "29"
  (let ([v (run 100 (q)
             (exists (e t)
               (!- '() e t)
               (== `(,e ,t) q)))])
    (pretty-print v)
    (length v))
  100)

(test "30"
  (let ([v (run 100 (q)
             (exists (g e t)
               (!- g e t)
               (== `(,g ,e ,t) q)))])
    (pretty-print v)
    (length v))
  100)

(test "31"
  (length
    (run 100 (q)
      (exists (g v)
        (!- g `(var ,v) 'int)
        (== `(,g ,v) q))))
  100)