((module tak racket
   (provide/contract
    (tak (-> number? number? number? (-> number? number?) number?)))
   (define (tak x y z k)
     (if (not (< y x))
       (k z)
       (tak
        (- x 1)
        y
        z
        (lambda (v1)
          (tak
           (- y 1)
           z
           x
           (lambda (v2) (tak (- z 1) x y (lambda (v3) (tak v1 v2 v3 k))))))))))
 (module nums racket (provide/contract (a number?) (b number?) (c number?)))
 (require 'tak 'nums)
 (tak a b c (lambda (x) x)))


=====================================================================

((module tak racket
   (provide/contract
    (tak (-> number? number? number? (-> number? number?) number?)))
   (define (tak x y z k)
     (if (not (< y x))
       (k z)
       (tak
        (- x 1)
        y
        z
        (lambda (v1)
          (tak
           (- y 1)
           z
           x
           (lambda (v2) (tak (- z 1) x y (lambda (v3) (tak v1 v2 v3 k))))))))))
 (module nums racket (provide/contract (a number?) (b number?) (c number?)))
 (module concolic racket
   (provide/contract (concolic-main (-> any/c)))
   (require 'tak 'nums)
   (define (concolic-main) (tak a b c (lambda (x) x)))))


=====================================================================

((module mtak racket
   (provide/contract
    (tak
     (->
      (flat int?)
      (->
       (flat int?)
       (-> (flat int?) (-> (-> (flat int?) (flat int?)) (flat int?)))))))
   (define tak
     (λ tak
       (x)
       (λ unused
         (y)
         (λ unused
           (z)
           (λ unused
             (k)
             (((if (not (< y x))) (k z))
              ((((tak (- x 1)) y) z)
               (λ unused
                 (v1)
                 ((((tak (- y 1)) z) x)
                  (λ unused
                    (v2)
                    ((((tak (- z 1)) x) y)
                     (λ unused (v3) ((((tak v1) v2) v3) k))))))))))))))
 (module mnums racket
   (provide/contract (a (flat int?)) (b (flat int?)) (c (flat int?))))
 (module concolic racket
   (provide/contract (concolic-main (-> (flat bool?) any/c)))
   (require (submod ".." mtak) (submod ".." mnums))
   (define concolic-main
     (λ concolic-main (unused) ((((tak a) b) c) (λ unused (x) x))))))


=====================================================================

(let ((mtak@tak
       (λ tak
         (x)
         (λ unused
           (y)
           (λ unused
             (z)
             (λ unused
               (k)
               (((if (not (< y x))) (k z))
                ((((tak (- x 1)) y) z)
                 (λ unused
                   (v1)
                   ((((tak (- y 1)) z) x)
                    (λ unused
                      (v2)
                      ((((tak (- z 1)) x) y)
                       (λ unused (v3) ((((tak v1) v2) v3) k))))))))))))))
  (let ((concolic@mtak@tak
         (contract
          (->
           (flat int?)
           (->
            (flat int?)
            (-> (flat int?) (-> (-> (flat int?) (flat int?)) (flat int?)))))
          mtak@tak
          mtak
          concolic)))
    (let ((concolic@mnums@a (contract (flat int?) mnums@a mnums concolic))
          (concolic@mnums@b (contract (flat int?) mnums@b mnums concolic))
          (concolic@mnums@c (contract (flat int?) mnums@c mnums concolic)))
      (let ((concolic@concolic-main
             (λ concolic-main
               (unused)
               ((((concolic@mtak@tak concolic@mnums@a) concolic@mnums@b)
                 concolic@mnums@c)
                (λ unused (x) x)))))
        (concolic@concolic-main (• Xarg))))))