(define-record lv (name) ())
(define lv make-lv)

(define residualize
  (letrec
      ([resid
         (lambda (x env)
           (cond
             [(lv? x) (artificial-name/env-pair x env)]
             [(constant? x) `(,x ,env)]
             [(pair? x)
              (let ((s/e (resid (car x) env)))
                (let ((s^/e^ (resid (cdr x) (cadr s/e))))
                  `(,(cons (car s/e) (car s^/e^))
                    ,(cadr s^/e^))))]
             [else (error 'resid "Invalid term: ~s" x)]))])
    (lambda (x)
      (car (resid x '())))))

(define artificial-name/env-pair
  (lambda (lv env)
    (cond
      [(assq lv env) =>
       (lambda (pr)
         `(,(artificial-name (lv-name lv) (cdr pr))
           ,env))]
      [(assq/name (lv-name lv) env) =>
       (lambda (pr)
         (let ((c (+ (cdr pr) 1)))
           `(,(artificial-name (lv-name lv) c)
             ,(cons `(,lv . ,c) env))))]
      [else
        `(,(artificial-name (lv-name lv) 0)
          ,(cons `(,lv . 0) env))])))

(define artificial-name
  (lambda (name c)
    (string->symbol (format "~s.~s" name c))))

(define assq/name
  (lambda (name env)
    (cond
      [(null? env) #f]
      [(eq? (lv-name (caar env)) name) (car env)]
      [else (assq/name name (cdr env))])))

(define subst-in
  (lambda (t s)
    (cond
      [(lv? t) (apply-subst s t)]
      [(constant? t) t]
      [else (cons (subst-in (car t) s) (subst-in (cdr t) s))])))

(define apply-subst
  (lambda (s id)
    (cond
      [(null? s) id]
      [(eq? (car s) 'unit-subst)
       (let ((t (cadr s)) (u (caddr s)))
         (if (eqv? id t) u id))]
      [(eq? (car s) 'compose-subst)
       (let ((old (cadr s)) (new (caddr s)))
         (let ((old (apply-subst old id)))
           (subst-in old new)))])))

(define compose-subst
  (lambda (old new)
    (cond
      [(null? old) new]
      [(null? new) old]
      [else `(compose-subst ,old ,new)])))

(define unit-subst
  (lambda (t u)
    `(unit-subst ,t ,u)))

(define empty-subst '())

(define flatten-subst
  (lambda (s)
    (cond
      [(null? s) '()]
      [(eq? (car s) 'unit-subst)
       (let ((t (cadr s)) (u (caddr s)))
         `((,t == ,u)))]
      [(eq? (car s) 'compose-subst)
       (let ((old (cadr s)) (new (caddr s)))
         (let ((old (flatten-subst old))
               (new (flatten-subst new)))
           (append old new)))])))

(define constant?
  (let ((v (void)))
    (lambda (x)
      (or (string? x) (number? x) (char? x) (boolean? x)
          (null? x) (symbol? x) (procedure? x) (vector? x)
          (eq? v x)))))

(define unify
  (lambda (t u subst)
    (if (and (list? t) (list? u) (not (= (length t) (length u))))
        (error 'unify "Lengths not equal:~n ~s~n ~s" t u))
    (cond
      [(unify* t u)
       =>
       (lambda (new-subst)
         (compose-subst subst new-subst))]
      [else #f])))

(define unify*
  (lambda (t u)
    (cond
      [(and (lv? t) (lv? u))
       (if (eqv? t u) empty-subst (unit-subst t u))]
      [(lv? t)
       (if (occurs? t u) #f (unit-subst t u))]
      [(lv? u)
       (if (occurs? u t) #f (unit-subst u t))]
      [(and (constant? t) (constant? u))
       (if (equal? t u) empty-subst #f)]
      [(or (constant? t) (constant? u)) #f]
      [(unify* (car t) (car u)) =>
       (lambda (s-car)
	 (cond
	   [(unify* (subst-in (cdr t) s-car) (subst-in (cdr u) s-car)) =>
	    (lambda (s-cdr) (compose-subst s-car s-cdr))]
	   [else #f]))]
      [else #f])))

(define occurs?  ;;; not used in Prolog
  (lambda (x t)
    (cond
      [(lv? t) (eqv? x t)]
      [(constant? t) #f]
      [else (or (occurs? x (car t)) (occurs? x (cdr t)))])))

(define-syntax let-lv
  (syntax-rules ()
    [(let-lv (name ...) body0 body1 ...)
     (let ((name (lv 'name)) ...)
       body0 body1 ...)]))

(define sx
  (let-lv (r v w x u)
    (residualize
      (flatten-subst
        (unify* `(,r (,v (,w ,x) 8)) `(,r (,u (abc ,u) ,x)))))))

(define sy
  (let-lv (x y)
    (residualize
      (flatten-subst
        (unify* `(p (f a) (g ,x)) `(p ,x ,y))))))

(define sz
  (let-lv (x y z)
    (residualize
      (flatten-subst
        (unify* `(p a ,x (h (g ,z))) `(p ,z (h ,y) (h ,y)))))))

(define sa ;; uses "occurs check"
  (let-lv (x y)
    (cond
      [(unify* `(p ,x ,x) `(p ,y (f ,y))) =>
       (lambda (subst)
         (residualize
           (flatten-subst subst)))]
      [else #f])))

;;;; This is what is in the paper.

(define disjoin-empty
  (lambda (cutk)
    (lambda (goal)
      (lambda (sk)
        (lambda (subst)
          (cutk))))))

(define disjoin-cons
  (lambda (disjunct disjunct*)
    (lambda (cutk)
      (lambda (goal)
        (lambda (sk)
          (lambda (subst)
            ((((disjunct sk) goal) subst)
             (lambda ()
               ((((disjunct* cutk) goal) sk) subst)))))))))

(define-syntax lambda*
  (syntax-rules ()
    [(_ () body0 body1 ...) (begin body0 body1 ...)]
    [(_ (formal0 formal1 ...) body0 body1 ...)
     (lambda (formal0)
       (lambda* (formal1 ...) body0 body1 ...))]))

(define-syntax trace-lambda*
  (syntax-rules ()
    [(_ name () body0 body1 ...) (begin body0 body1 ...)]
    [(_ name (formal0 formal1 ...) body0 body1 ...)
     (trace-lambda name (formal0)
       (trace-lambda* name (formal1 ...) body0 body1 ...))]))

(define disjoin-empty
  (lambda* (cutk goal sk subst)
    (cutk)))

(define disjoin-cons
  (lambda (disjunct disjunct*)
    (lambda* (cutk goal sk subst)
      ((((disjunct sk) goal) subst)
       (lambda () ((((disjunct* cutk) goal) sk) subst))))))

(define-syntax disjoin
  (syntax-rules ()
    [(_) disjoin-empty]
    [(_ disjunct0 disjunct1 ...)
     (disjoin-cons disjunct0 (disjoin disjunct1 ...))]))

(define-syntax relation
  (syntax-rules ()
    [(_ (formal ...) body)
     (lambda (formal ...)
       (lambda* (ant* sk subst cutk)
         ((((body cutk) `(,(subst-in formal subst) ...))
           (ant* sk)) subst)))]))

(define-syntax trace-relation
  (syntax-rules ()
    [(_ name (formal ...) body)
     (trace-lambda name (formal ...)
       (lambda* (ant* sk subst cutk)
         ((((body cutk) `(,(subst-in formal subst) ...))
           (ant* sk)) subst)))]))

(define father
  (relation (dad child)
    (disjoin
      (fact 'john 'sam)
      (fact 'sam 'pete)
      (fact 'pete 'sal))))

(define fact
  (lambda term
    (lambda* (sk goal entering-subst next-disjunctk)
      (cond
        [(unify term goal entering-subst) =>
         (lambda (exiting-subst)
           ((sk exiting-subst) next-disjunctk))]
        [else (next-disjunctk)]))))

(define axiom (lambda (sk) sk))

(define initial-sk
  (lambda* (subst fk)
    (cons subst fk)))

(define initial-cutk (lambda () '()))

(define query
  (lambda (result)
    ((((result axiom) initial-sk) empty-subst) initial-cutk)))

(define father
  (relation (dad child)
    (disjoin
      (fact 'john 'sam)
      (fact 'sam 'pete)
      (fact 'pete 'sal)
      (fact 'pete 'pat))))

(define stream-prefix
  (lambda (n strm)
    (if (null? strm) '()
      (cons (car strm)
        (if (zero? n) '()
          (stream-prefix (- n 1) ((cdr strm))))))))

(define solver
  (lambda (n result term)
    (map (lambda (subst)
           (residualize
             (subst-in term subst)))
      (stream-prefix (- n 1) (query result)))))

(define solve
  (lambda (n guide/goal)
    (solver n (apply (car guide/goal) (cdr guide/goal)) (cdr guide/goal))))

(define grandpa-sam
  (relation (grandchild)
    (disjoin
      (let-lv (grandchild parent)
        ((to-show grandchild)
         ((father 'sam parent) ((father parent grandchild) axiom)))))))

(define-syntax to-show
  (syntax-rules ()
    [(to-show a0 ...)
     (let ((fact-ready (fact a0 ...)))
       (lambda* (ant* sk)
         (fact-ready (ant* sk))))]))

(define-syntax conjoin
  (syntax-rules ()
    [(_) axiom]
    [(_ conjunct0 conjunct1 ...)
     (conjunct0 (conjoin conjunct1 ...))]))

(define fail (relation () (disjoin)))

(define grandpa-maker
  (lambda (grandad)
    (relation (grandchild)
      (disjoin
        (let-lv (parent grandchild)
          ((to-show grandchild)
           (conjoin
             (father grandad parent)
             (father parent grandchild))))))))

(define grandpa-maker
  (lambda (guide grandad)
    (relation (grandchild)
      (disjoin
        (let-lv (grandchild parent)
          ((to-show grandchild)
           (conjoin
             (guide grandad parent)
             (guide parent grandchild))))))))

(define grandpa
  (relation (grandad grandchild)
    (disjoin
      (let-lv (grandad grandchild parent)
        ((to-show grandad grandchild)
         (conjoin
           (father grandad parent)
           (father parent grandchild)))))))

(define father
  (relation (dad child)
    (disjoin
      (fact 'john 'sam)
      (fact 'sam 'pete)
      (fact 'sam 'polly)
      (fact 'pete 'sal)
      (fact 'pete 'pat))))

(define mother
  (relation (mom child)
    (disjoin
      (fact 'polly 'betty)
      (fact 'polly 'david))))

(define grandpa
  (relation (grandad grandchild)
    (disjoin
      (let-lv (grandad grandchild parent)
        ((to-show grandad grandchild)
         (conjoin
           (father grandad parent)
           (father parent grandchild))))
      (let-lv (grandad grandchild parent)
        ((to-show grandad grandchild)
         (conjoin
           (father grandad parent)
           (mother parent grandchild)))))))

(define grandpa
  (relation (grandad grandchild)
    (lambda (cutk)
      ((disjoin
         (let-lv (grandad grandchild parent)
           ((to-show grandad grandchild)
            (conjoin
              (father grandad parent)
              (father parent grandchild)
              (! cutk))))
         (let-lv (grandad grandchild parent)
           ((to-show grandad grandchild)
            (conjoin
              (father grandad parent)
              (mother parent grandchild)))))
       cutk))))

(define !
  (lambda (exiting-cutk)
    (lambda* (ant* sk subst cutk)
      (((ant* sk) subst) exiting-cutk))))

(define grandpa
  (relation (grandad grandchild)
    (lambda (cutk)
      ((disjoin
         (let-lv (grandad grandchild parent)
           ((to-show grandad grandchild)
            (conjoin
              (father grandad parent)
              (! cutk)
              (father parent grandchild))))
         (let-lv (grandad grandchild parent)
           ((to-show grandad grandchild)
            (conjoin
              (father grandad parent)
              (mother parent grandchild)))))
       cutk))))

(define grandpa
  (relation (grandad grandchild)
    (lambda (cutk)
      ((disjoin
         (let-lv (grandad grandchild parent)
           ((to-show grandad grandchild)
            (conjoin
              (! cutk)
              (father grandad parent)
              (father parent grandchild))))
         (let-lv (grandad grandchild parent)
           ((to-show grandad grandchild)
            (conjoin
              (father grandad parent)
              (mother parent grandchild)))))
       cutk))))

(define !fail
  (lambda (exiting-cutk)
    (lambda* (ant* sk subst cutk)
      (exiting-cutk))))

(define grandpa
  (relation (grandad grandchild)
    (disjoin
      (let-lv (grandad grandchild parent)
        ((to-show grandad grandchild)
         (conjoin
           (father grandad parent)
           (starts-with-p? parent)
           (father parent grandchild)))))))

(define starts-with-p?
  (lambda (x)
    (lambda* (ant* sk subst cutk)
      (let ((x (subst-in x subst)))
        (if (lv? x)
            (error 'starts-with-p? "Variable found: ~s." x))
        (if (not (symbol? x))
            (error 'starts-with-p? "Non-symbol found: ~s." x))
        (let ([char (string-ref (symbol->string x) 0)])
          (if (string=? (string char) "p")
              (((ant* sk) subst) cutk)
              (cutk)))))))

(define pred
  (lambda (p)
    (let ([p-nocheck (pred-nocheck p)])
      (lambda args
        (lambda* (ant* sk subst cutk)
          (let ((args (subst-in args subst)))
            (approve-apply 'pred p args)
            (((((p-nocheck args) ant*) sk) subst) cutk)))))))

(define pred-nocheck
  (lambda (p)
    (lambda args
      (lambda* (ant* sk subst cutk)
        (if (apply p args) (((ant* sk) subst) cutk) (cutk))))))

(define fun
  (lambda (f)
    (lambda args
      (lambda* (ant* sk subst cutk)
        (let ((args (subst-in (rotate-right args) subst)))
          (approve-apply 'fun f (cdr args))
          (cond
            [(unify (apply f (cdr args)) (car args) subst)
             => (lambda (exiting-subst)
                  (((ant* sk) exiting-subst) cutk))]
            [else (cutk)]))))))

(define approve-apply
  (lambda (name proc args)
    (if (not (procedure? proc))
      (error name "Non-procedure found: ~s" proc))
    (if (ormap lv? args)
      (error name "Variable found: ~s" args))
    (write 'approved)
    (newline)))

(define starts-with-p?
  (pred
    (lambda (x)
      (and
        (symbol? x)
        (string=? (string (string-ref (symbol->string x) 0)) "p")))))

(define rotate-right
  (lambda (ls)
    (cond
      [(null? (cdr ls)) (cons (car ls) '())]
      [else (let ([rcdr (rotate-right (cdr ls))])
              (cons (car rcdr) (cons (car ls) (cdr rcdr))))])))

(define fails
  (lambda (result)
    (lambda* (ant* sk subst cutk)
      ((((result ant*)
         (lambda* (subst fk) (cutk)))
        subst)
       (lambda () (((ant* sk) subst) cutk))))))

(define instantiated
  (lambda (x)
    (lambda* (ant* sk subst cutk)
      (let ((x (subst-in x subst)))
        (if (not (lv? x))
          (((ant* sk) subst) cutk)
          (cutk))))))

(define grandpa
  (relation (grandad grandchild)
    (disjoin
      (let-lv (grandad grandchild parent)
        ((to-show grandad grandchild)
         (conjoin
           (instantiated parent)
           (father grandad parent)
           (fails (starts-with-p? parent))
           (father parent grandchild)))))))

(define view-goal
  (lambda (name goal)
    (lambda* (ant* sk subst cutk)
      (pretty-print
        (residualize `(,name . ,(subst-in goal subst))))
      (((ant* sk) subst) cutk))))

(define grandpa
  (relation (grandad grandchild)
    (lambda (cutk)
      (lambda (goal)
        (((disjoin
            (let-lv (grandad grandchild parent)
              ((to-show grandad grandchild)
               (conjoin
                 (father grandad parent)
                 (view-goal 'grandpa goal)
                 (father parent grandchild)))))
          cutk)
         goal)))))

(define view-subst
  (lambda (name)
    (lambda* (ant* sk subst cutk)
      (write (subst-in name subst))
      (newline)
      (pretty-print (residualize (flatten-subst subst)))
      (newline)
      (((ant* sk) subst) cutk))))

(define grandpa
  (relation (grandad grandchild)
    (disjoin
      (let-lv (grandad grandchild parent)
        ((to-show grandad grandchild)
         (conjoin
           (father grandad parent)
           (father parent grandchild)
           (view-subst grandchild)))))))

(define father
  (relation (dad child)
    (disjoin
      (fact 'john 'sam)
      (fact 'john 'harry)
      (fact 'harry 'carl)
      (fact 'sam 'pete)
      (fact 'sam 'polly)
      (fact 'sam 'leon)
      (fact 'pete 'sal)
      (fact 'pete 'pat))))

(define ancestor
  (relation (old young)
    (disjoin
      (let-lv (old young not-so-old)
        ((to-show old young)
         (conjoin (father old young))))
      (let-lv (old young not-so-old)
        ((to-show old young)
         (conjoin
           (father old not-so-old)
           (ancestor not-so-old young)))))))

(define ancestor
  (relation (old young)
    (let-lv (old young not-so-old)
      (disjoin
        ((to-show old young)
         (conjoin (father old young)))
        ((to-show old young)
         (conjoin
           (father old not-so-old)
           (ancestor not-so-old young)))))))

(define common-ancestor
  (relation (young-a young-b old)
    (let-lv (young-a young-b old)
      (disjoin
        ((to-show young-a young-b old)
         (conjoin
           (ancestor old young-a)
           (ancestor old young-b)))))))

(define younger-ancestor
  (relation (young-a young-b old not-so-old)
    (let-lv (young-a young-b old not-so-old)
      (disjoin
        ((to-show young-a young-b old not-so-old)
         (conjoin
           (common-ancestor young-a young-b not-so-old)
           (ancestor old not-so-old)))))))

(define youngest-common-ancestor
  (relation (young-a young-b not-so-old)
    (let-lv (young-a young-b not-so-old old)
      (disjoin
        ((to-show young-a young-b not-so-old)
         (conjoin
           (common-ancestor young-a young-b not-so-old)
           (fails
             (younger-ancestor young-a young-b not-so-old old))))))))

(define concat
  (lambda (ls1 ls2)
    (cond
      [(null? ls1) ls2]
      [else (cons (car ls1) (concat (cdr ls1) ls2))])))

(define concat
  (relation (xs ys zs)
    (disjoin
      (let-lv (xs) (fact '() xs xs))
      (let-lv (x xs ys zs)
        ((to-show `(,x . ,xs) ys `(,x . ,zs))
         (conjoin (concat xs ys zs)))))))

(define solution
  (lambda (guide/goal)
    (let ((ls (solve 1 guide/goal)))
      (if (null? ls) #f (car ls)))))

(define disjoin-base
  (lambda (rel)
    (lambda* (cutk goal sk subst)
      (((((apply rel goal) axiom) sk) subst) cutk))))

(define-syntax disjoin+
  (syntax-rules ()
    [(_ rel) (disjoin-base rel)]
    [(_ more disjunct0 disjunct1 ...)
     (disjoin-cons disjunct0 (disjoin+ more disjunct1 ...))]))

(define !-1 fail)
(define !-
  (relation (g x t)
    (let-lv (g x)
      (lambda (cutk)      
        ((disjoin+ !-1
           ((to-show g x "int")
            (conjoin ((pred integer?) x) (! cutk)))
           ((to-show g x "bool")
            (conjoin ((pred boolean?) x) (! cutk))))
         cutk)))))

(define !-2 fail)
(define !-1
  (relation (g exp t)
    (lambda (cutk)
      (let-lv (g x y)
        ((disjoin+ !-2
           ((to-show g `(zero? ,x) "bool")
            (conjoin (! cutk) (!- g x "int")))
           ((to-show g `(sub1 ,x) "int")
            (conjoin (! cutk) (!- g x "int")))
           ((to-show g `(+ ,x ,y) "int")
            (conjoin (! cutk) (!- g x "int") (!- g y "int"))))
         cutk)))))

(define !-3 fail)
(define !-2
  (relation (g exp t)
    (lambda (cutk)
      (let-lv (g t test conseq alt)
        ((disjoin+ !-3
           ((to-show g `(if ,test ,conseq ,alt) t)
            (conjoin (! cutk)
              (!- g test "bool") (!- g conseq t) (!- g alt t))))
         cutk)))))

(define !-4 fail)
(define !-3
  (relation (g v t)
    (let-lv (g v t)
      (lambda (cutk)
        ((disjoin+ !-4
           ((to-show g v t)
            (conjoin ((pred symbol?) v) (! cutk) (env g v t))))
         cutk)))))

(define more-env fail)
(define env
  (relation (g v t)
    (lambda (cutk)
      (let-lv (g v t w type-w)
        ((disjoin+ more-env
           ((to-show `(non-generic ,v ,t ,g) v t)
            (conjoin (! cutk)))
           ((to-show `(non-generic ,v ,t ,g) v type-w)
            (conjoin (unequal? t type-w) (!fail cutk)))
           ((to-show `(non-generic ,w ,type-w ,g) v t)
            (conjoin (! cutk) (unequal? w v) (env g v t))))
         cutk)))))

(define unequal?
  (let-lv (x y)
    (relation (a b)
      (disjoin
        ((to-show x x)
         (conjoin (fail)))
        ((to-show x y)
         (conjoin (fails (fail))))))))

(define !-5 fail)
(define !-4
  (relation (g exp t)
    (lambda (cutk)
      (let-lv (g t v body type-v)
        ((disjoin+ !-5
           ((to-show g `(lambda (,v) ,body) `("->" ,type-v ,t))
            (conjoin (! cutk)
              (!- `(non-generic ,v ,type-v ,g) body t))))
         cutk)))))

(define !-6 fail)
(define !-5
  (relation (g exp t)
    (lambda (cutk)
      (let-lv (g t rand v body t-rand rator)
        ((disjoin+ !-6
           ((to-show g `(fix ,rand) t)
            (conjoin (! cutk) (!- g rand `("->" ,t ,t))))
           ((to-show g `(let ((,v ,rand)) ,body) t)
            (conjoin (! cutk)
              (!- g rand t-rand)
              (!- `(generic ,v ,t-rand ,g) body t)))
           ((to-show g `(,rator ,rand) t)
            (conjoin (! cutk)
              (!- g rator `("->" ,t-rand ,t))
              (!- g rand t-rand))))
         cutk)))))

(define fix
  (lambda (e)
    (e (lambda (z) ((fix e) z)))))

(define more-env
  (relation (g v t)
    (let-lv (g v t targ tresult notv nott)
      (lambda (cutk)
        ((disjoin
           ((to-show `(generic ,v ("->" ,targ ,tresult) ,g) v t)
            (conjoin
              (instantiate `("->" ,targ ,tresult) t)
              (! cutk)))
           ((to-show `(generic ,notv ,nott ,g) v t)
            (conjoin (unequal? notv v) (env g v t))))
         cutk)))))

(define instantiate
  (relation (te1 te2)
    (let-lv (te1 te2 varmap)
      (disjoin
        ((to-show te1 te2)
         (conjoin
           (instantiate-raw te1 te2 varmap)
           (fix-varmap varmap)))))))

(define instantiate-raw
  (relation (te1 te2 varmap)
    (lambda (cutk)
      ((disjoin
         (let-lv (te1 te2)
           ((to-show te1 te2 `[(,te1 . ,te2)])
            (conjoin
              (fails (instantiated te1))
              (! cutk))))
         (let-lv (varmap targ1 tresult1 t1 targ2 tresult2 t2)
           ((to-show
              `("->" ,targ1 ,tresult1) `("->" ,targ2 ,tresult2) varmap)
            (conjoin
              (instantiate-raw targ1 targ2 t1)
              (instantiate-raw tresult1 tresult2 t2)
              (concat t1 t2 varmap)
              (! cutk))))
         (fact "int" "int" '())
         (fact "bool" "bool" '()))
       cutk))))

(define fix-varmap
  (relation (varmap)
    (disjoin
      (fact '())
      (let-lv (x y)
        ((to-show `(,x . ,y))
         (conjoin (fix-varmap-one x y) (fix-varmap y)))))))

(define fix-varmap-one
  (relation (x y)
    (lambda (cutk)
      ((disjoin 
         (let-lv (x) (fact x '()))
         (let-lv (x y x1 y1 rest)
           ((to-show `(,x1 . ,y1) `[(,x . ,y) . ,rest])
            (conjoin
              ((pred-nocheck eq?) x1 x)
              (make-equal y1 y)
              (fix-varmap-one `(,x1 . ,y1) rest)
              (! cutk))))
         (let-lv (p other rest)
           ((to-show p `(,other . ,rest))
            (conjoin (fix-varmap-one p rest)))))
       cutk))))

(define make-equal
  (let-lv (x)
    (relation (a b)
      (disjoin
        (fact x x)))))

(define !-
  (relation (g exp t)
    (let-lv (g t x y z tx)
      (lambda (cutk)
        (let ([! (! cutk)])
          ((disjoin
             ((to-show g `(var ,x) t)
              (conjoin ! (env g x t)))
             ((to-show g `(intc ,x) "int")
              (conjoin !))
             ((to-show g `(boolc ,x) "bool")
              (conjoin !))
             ((to-show g `(zero? ,x) "bool")
              (conjoin ! (!- g x "int")))
             ((to-show g `(sub1 ,x) "int")
              (conjoin ! (!- g x "int")))
             ((to-show g `(+ ,x ,y) "int")
              (conjoin ! (!- g x "int") (!- g y "int")))
             ((to-show g `(if ,x ,y ,z) t)
              (conjoin ! (!- g x "bool") (!- g y t) (!- g z t)))
             ((to-show g `(lambda (,x) ,y) `("->" ,tx ,t))
              (conjoin ! (!- `(non-generic ,x ,tx ,g) y t)))
             ((to-show g `(app ,x ,y) t)
              (conjoin ! (!- g x `("->" ,tx ,t)) (!- g y tx)))
             ((to-show g `(fix ,x) t)
              (conjoin ! (!- g x `("->" ,t ,t))))
             ((to-show g `(let ((,x ,y)) ,z) t)
              (conjoin ! (!- g y tx) (!- `(generic ,x ,tx ,g) z t))))
           cutk))))))

(define test-working
  (lambda ()
    (solution
    (let-lv (g ?)
      `(,!-
         ,g
         (let ((f (lambda (x) (var x))))
           (if (app (var f) (zero? (intc 5)))
             (+ (app (var f) (intc 4)) (intc 8))
             (+ (app (var f) (intc 3)) (intc 7))))
         ,?)))))

(define easy-test
  (lambda ()
    (solve 20 (let-lv (x y) `(,ancestor ,x ,y)))))

(pretty-print (easy-test))
(newline)

(pretty-print (test-working))
(newline)