#lang racket
(require "mk.rkt")

(define apply-Go
  (lambda (G e t)
    (fresh (a G^)
      (== `(,a . ,G^) G)
      (fresh (aa da)
        (== `(,aa . ,da) a)
        (conde
          ((== aa e) (== da t))
          ((=/= aa e) (apply-Go G^ e t)))))))

(define !-
  (lambda (G e t)
    (conde
      ((numbero e) (== 'Nat t))
      ((== t 'Bool)
       (conde
         ((== #t e))
         ((== #f e))))
      ((fresh (e1)
              (== `(zero? ,e1) e)
              (== 'Bool t)
              (!- G e1 'Nat)))
      ((fresh (e1)
              (== `(not ,e1) e)
              (== 'Bool t)
              (!- G e1 'Bool)))
      ((fresh (e1)
              (== `(sub1 ,e1) e)
              (== 'Nat t)
              (!- G e1 'Nat)))
      ((fresh (x)
             (== `(car ,x) e)
             (fresh (ta td)
                    (== ta t) 
                    (!- G x `(pairof ,ta ,td)))))
      ((fresh (x)
             (== `(cdr ,x) e)
             (fresh (ta td)
                    (== td t) 
                    (!- G x `(pairof ,ta ,td)))))
      ((fresh (ne1 ne2)
         (== `(+ ,ne1 ,ne2) e)
         (== 'Nat t)
         (!- G ne1 'Nat)
         (!- G ne2 'Nat)))
      ((fresh (ne1 ne2)
         (== `(* ,ne1 ,ne2) e)
         (== 'Nat t)
         (!- G ne1 'Nat)
         (!- G ne2 'Nat)))
      ((fresh (a d)
              (== `(cons ,a ,d) e)
              (fresh (ta td)
                     (== `(pairof ,ta ,td) t)
                     (!- G a ta)
                     (!- G d td))))
      ((fresh (teste anse elsee)
        (== `(if ,teste ,anse ,elsee) e)
        (!- G teste 'Bool)
        (!- G anse t)
        (!- G elsee t)))
      ((symbolo e) (apply-Go G e t))
      ((fresh (x b)
         (== `(lambda (,x) ,b) e)
         (symbolo x)
         (fresh (tx tb)          
           (== `(,tx -> ,tb) t)
           (!- `((,x . ,tx) . ,G) b tb))))
       ((fresh (x val b)
               (== `(let ((,x ,val)) ,b) e) 
               (symbolo x)
               (fresh (te)
                      ;(!- G val `(,ta -> ,td))
                      (!- G val te)
                      (!- `((,x . ,te) . ,G) b t)
                      ;(== tt t)
                      ))) 
       ((fresh (x b)
               (== `(fix (lambda (,x) ,b)) e)
               (symbolo x)
               (fresh (tt)
                      (== tt t)
                      (!- `((,x . ,tt) . ,G) b tt))))
       ((fresh (e1 arg)
         (== `(,e1 ,arg) e)
         (fresh (targ)
           (!- G e1 `(,targ -> ,t))
           (!- G arg targ)))))))