"Copyright (c) 2015, Mark Tarver

All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright
   notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
   notice, this list of conditions and the following disclaimer in the
   documentation and/or other materials provided with the distribution.
3. The name of Mark Tarver may not be used to endorse or promote products
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY Mark Tarver ''AS IS'' AND ANY
EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL Mark Tarver BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."

(defun shen.typecheck (V3528 V3529) (let Curry (shen.curry V3528) (let ProcessN (shen.start-new-prolog-process) (let Type (shen.insert-prolog-variables (shen.demodulate (shen.curry-type V3529)) ProcessN) (let Continuation (freeze (return Type ProcessN shen.void)) (shen.t* (cons Curry (cons : (cons Type ()))) () ProcessN Continuation))))))

(defun shen.curry (V3531) (cond ((and (cons? V3531) (shen.special? (hd V3531))) (cons (hd V3531) (map (lambda Y (shen.curry Y)) (tl V3531)))) ((and (cons? V3531) (and (cons? (tl V3531)) (shen.extraspecial? (hd V3531)))) V3531) ((and (cons? V3531) (and (= type (hd V3531)) (and (cons? (tl V3531)) (and (cons? (tl (tl V3531))) (= () (tl (tl (tl V3531)))))))) (cons type (cons (shen.curry (hd (tl V3531))) (tl (tl V3531))))) ((and (cons? V3531) (and (cons? (tl V3531)) (cons? (tl (tl V3531))))) (shen.curry (cons (cons (hd V3531) (cons (hd (tl V3531)) ())) (tl (tl V3531))))) ((and (cons? V3531) (and (cons? (tl V3531)) (= () (tl (tl V3531))))) (cons (shen.curry (hd V3531)) (cons (shen.curry (hd (tl V3531))) ()))) (true V3531)))

(defun shen.special? (V3533) (element? V3533 (value shen.*special*)))

(defun shen.extraspecial? (V3535) (element? V3535 (value shen.*extraspecial*)))

(defun shen.t* (V3540 V3541 V3542 V3543) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let Error (shen.newpv V3542) (do (shen.incinfs) (fwhen (shen.maxinfexceeded?) V3542 (freeze (bind Error (shen.errormaxinfs) V3542 V3543))))) (if (= Case false) (let Case (let V3520 (shen.lazyderef V3540 V3542) (if (= fail V3520) (do (shen.incinfs) (cut Throwcontrol V3542 (freeze (shen.prolog-failure V3542 V3543)))) false)) (if (= Case false) (let Case (let V3521 (shen.lazyderef V3540 V3542) (if (cons? V3521) (let X (hd V3521) (let V3522 (shen.lazyderef (tl V3521) V3542) (if (cons? V3522) (let V3523 (shen.lazyderef (hd V3522) V3542) (if (= : V3523) (let V3524 (shen.lazyderef (tl V3522) V3542) (if (cons? V3524) (let A (hd V3524) (let V3525 (shen.lazyderef (tl V3524) V3542) (if (= () V3525) (do (shen.incinfs) (fwhen (shen.type-theory-enabled?) V3542 (freeze (cut Throwcontrol V3542 (freeze (shen.th* X A V3541 V3542 V3543)))))) false))) false)) false)) false))) false)) (if (= Case false) (let Datatypes (shen.newpv V3542) (do (shen.incinfs) (shen.show V3540 V3541 V3542 (freeze (bind Datatypes (value shen.*datatypes*) V3542 (freeze (shen.udefs* V3540 V3541 Datatypes V3542 V3543))))))) Case)) Case)) Case)))))

(defun shen.type-theory-enabled? () (value shen.*shen-type-theory-enabled?*))

(defun enable-type-theory (V3549) (cond ((= + V3549) (set shen.*shen-type-theory-enabled?* true)) ((= - V3549) (set shen.*shen-type-theory-enabled?* false)) (true (simple-error "enable-type-theory expects a + or a -
"))))

(defun shen.prolog-failure (V3560 V3561) false)

(defun shen.maxinfexceeded? () (> (inferences) (value shen.*maxinferences*)))

(defun shen.errormaxinfs () (simple-error "maximum inferences exceeded~%"))

(defun shen.udefs* (V3567 V3568 V3569 V3570 V3571) (let Case (let V3516 (shen.lazyderef V3569 V3570) (if (cons? V3516) (let D (hd V3516) (do (shen.incinfs) (call (cons D (cons V3567 (cons V3568 ()))) V3570 V3571))) false)) (if (= Case false) (let V3517 (shen.lazyderef V3569 V3570) (if (cons? V3517) (let Ds (tl V3517) (do (shen.incinfs) (shen.udefs* V3567 V3568 Ds V3570 V3571))) false)) Case)))

(defun shen.th* (V3577 V3578 V3579 V3580 V3581) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (do (shen.incinfs) (shen.show (cons V3577 (cons : (cons V3578 ()))) V3579 V3580 (freeze (fwhen false V3580 V3581)))) (if (= Case false) (let Case (let F (shen.newpv V3580) (do (shen.incinfs) (fwhen (shen.typedf? (shen.lazyderef V3577 V3580)) V3580 (freeze (bind F (shen.sigf (shen.lazyderef V3577 V3580)) V3580 (freeze (call (cons F (cons V3578 ())) V3580 V3581))))))) (if (= Case false) (let Case (do (shen.incinfs) (shen.base V3577 V3578 V3580 V3581)) (if (= Case false) (let Case (do (shen.incinfs) (shen.by_hypothesis V3577 V3578 V3579 V3580 V3581)) (if (= Case false) (let Case (let V3412 (shen.lazyderef V3577 V3580) (if (cons? V3412) (let F (hd V3412) (let V3413 (shen.lazyderef (tl V3412) V3580) (if (= () V3413) (do (shen.incinfs) (shen.th* F (cons --> (cons V3578 ())) V3579 V3580 V3581)) false))) false)) (if (= Case false) (let Case (let V3414 (shen.lazyderef V3577 V3580) (if (cons? V3414) (let F (hd V3414) (let V3415 (shen.lazyderef (tl V3414) V3580) (if (cons? V3415) (let X (hd V3415) (let V3416 (shen.lazyderef (tl V3415) V3580) (if (= () V3416) (let B (shen.newpv V3580) (do (shen.incinfs) (shen.th* F (cons B (cons --> (cons V3578 ()))) V3579 V3580 (freeze (shen.th* X B V3579 V3580 V3581))))) false))) false))) false)) (if (= Case false) (let Case (let V3417 (shen.lazyderef V3577 V3580) (if (cons? V3417) (let V3418 (shen.lazyderef (hd V3417) V3580) (if (= cons V3418) (let V3419 (shen.lazyderef (tl V3417) V3580) (if (cons? V3419) (let X (hd V3419) (let V3420 (shen.lazyderef (tl V3419) V3580) (if (cons? V3420) (let Y (hd V3420) (let V3421 (shen.lazyderef (tl V3420) V3580) (if (= () V3421) (let V3422 (shen.lazyderef V3578 V3580) (if (cons? V3422) (let V3423 (shen.lazyderef (hd V3422) V3580) (if (= list V3423) (let V3424 (shen.lazyderef (tl V3422) V3580) (if (cons? V3424) (let A (hd V3424) (let V3425 (shen.lazyderef (tl V3424) V3580) (if (= () V3425) (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons list (cons A ())) V3579 V3580 V3581)))) (if (shen.pvar? V3425) (do (shen.bindv V3425 () V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons list (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3425 V3580) Result))) false)))) (if (shen.pvar? V3424) (let A (shen.newpv V3580) (do (shen.bindv V3424 (cons A ()) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons list (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3424 V3580) Result)))) false))) (if (shen.pvar? V3423) (do (shen.bindv V3423 list V3580) (let Result (let V3426 (shen.lazyderef (tl V3422) V3580) (if (cons? V3426) (let A (hd V3426) (let V3427 (shen.lazyderef (tl V3426) V3580) (if (= () V3427) (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons list (cons A ())) V3579 V3580 V3581)))) (if (shen.pvar? V3427) (do (shen.bindv V3427 () V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons list (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3427 V3580) Result))) false)))) (if (shen.pvar? V3426) (let A (shen.newpv V3580) (do (shen.bindv V3426 (cons A ()) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons list (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3426 V3580) Result)))) false))) (do (shen.unbindv V3423 V3580) Result))) false))) (if (shen.pvar? V3422) (let A (shen.newpv V3580) (do (shen.bindv V3422 (cons list (cons A ())) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons list (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3422 V3580) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3428 (shen.lazyderef V3577 V3580) (if (cons? V3428) (let V3429 (shen.lazyderef (hd V3428) V3580) (if (= @p V3429) (let V3430 (shen.lazyderef (tl V3428) V3580) (if (cons? V3430) (let X (hd V3430) (let V3431 (shen.lazyderef (tl V3430) V3580) (if (cons? V3431) (let Y (hd V3431) (let V3432 (shen.lazyderef (tl V3431) V3580) (if (= () V3432) (let V3433 (shen.lazyderef V3578 V3580) (if (cons? V3433) (let A (hd V3433) (let V3434 (shen.lazyderef (tl V3433) V3580) (if (cons? V3434) (let V3435 (shen.lazyderef (hd V3434) V3580) (if (= * V3435) (let V3436 (shen.lazyderef (tl V3434) V3580) (if (cons? V3436) (let B (hd V3436) (let V3437 (shen.lazyderef (tl V3436) V3580) (if (= () V3437) (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y B V3579 V3580 V3581)))) (if (shen.pvar? V3437) (do (shen.bindv V3437 () V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y B V3579 V3580 V3581)))) (do (shen.unbindv V3437 V3580) Result))) false)))) (if (shen.pvar? V3436) (let B (shen.newpv V3580) (do (shen.bindv V3436 (cons B ()) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y B V3579 V3580 V3581)))) (do (shen.unbindv V3436 V3580) Result)))) false))) (if (shen.pvar? V3435) (do (shen.bindv V3435 * V3580) (let Result (let V3438 (shen.lazyderef (tl V3434) V3580) (if (cons? V3438) (let B (hd V3438) (let V3439 (shen.lazyderef (tl V3438) V3580) (if (= () V3439) (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y B V3579 V3580 V3581)))) (if (shen.pvar? V3439) (do (shen.bindv V3439 () V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y B V3579 V3580 V3581)))) (do (shen.unbindv V3439 V3580) Result))) false)))) (if (shen.pvar? V3438) (let B (shen.newpv V3580) (do (shen.bindv V3438 (cons B ()) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y B V3579 V3580 V3581)))) (do (shen.unbindv V3438 V3580) Result)))) false))) (do (shen.unbindv V3435 V3580) Result))) false))) (if (shen.pvar? V3434) (let B (shen.newpv V3580) (do (shen.bindv V3434 (cons * (cons B ())) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y B V3579 V3580 V3581)))) (do (shen.unbindv V3434 V3580) Result)))) false)))) (if (shen.pvar? V3433) (let A (shen.newpv V3580) (let B (shen.newpv V3580) (do (shen.bindv V3433 (cons A (cons * (cons B ()))) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y B V3579 V3580 V3581)))) (do (shen.unbindv V3433 V3580) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3440 (shen.lazyderef V3577 V3580) (if (cons? V3440) (let V3441 (shen.lazyderef (hd V3440) V3580) (if (= @v V3441) (let V3442 (shen.lazyderef (tl V3440) V3580) (if (cons? V3442) (let X (hd V3442) (let V3443 (shen.lazyderef (tl V3442) V3580) (if (cons? V3443) (let Y (hd V3443) (let V3444 (shen.lazyderef (tl V3443) V3580) (if (= () V3444) (let V3445 (shen.lazyderef V3578 V3580) (if (cons? V3445) (let V3446 (shen.lazyderef (hd V3445) V3580) (if (= vector V3446) (let V3447 (shen.lazyderef (tl V3445) V3580) (if (cons? V3447) (let A (hd V3447) (let V3448 (shen.lazyderef (tl V3447) V3580) (if (= () V3448) (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons vector (cons A ())) V3579 V3580 V3581)))) (if (shen.pvar? V3448) (do (shen.bindv V3448 () V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons vector (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3448 V3580) Result))) false)))) (if (shen.pvar? V3447) (let A (shen.newpv V3580) (do (shen.bindv V3447 (cons A ()) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons vector (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3447 V3580) Result)))) false))) (if (shen.pvar? V3446) (do (shen.bindv V3446 vector V3580) (let Result (let V3449 (shen.lazyderef (tl V3445) V3580) (if (cons? V3449) (let A (hd V3449) (let V3450 (shen.lazyderef (tl V3449) V3580) (if (= () V3450) (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons vector (cons A ())) V3579 V3580 V3581)))) (if (shen.pvar? V3450) (do (shen.bindv V3450 () V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons vector (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3450 V3580) Result))) false)))) (if (shen.pvar? V3449) (let A (shen.newpv V3580) (do (shen.bindv V3449 (cons A ()) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons vector (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3449 V3580) Result)))) false))) (do (shen.unbindv V3446 V3580) Result))) false))) (if (shen.pvar? V3445) (let A (shen.newpv V3580) (do (shen.bindv V3445 (cons vector (cons A ())) V3580) (let Result (do (shen.incinfs) (shen.th* X A V3579 V3580 (freeze (shen.th* Y (cons vector (cons A ())) V3579 V3580 V3581)))) (do (shen.unbindv V3445 V3580) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3451 (shen.lazyderef V3577 V3580) (if (cons? V3451) (let V3452 (shen.lazyderef (hd V3451) V3580) (if (= @s V3452) (let V3453 (shen.lazyderef (tl V3451) V3580) (if (cons? V3453) (let X (hd V3453) (let V3454 (shen.lazyderef (tl V3453) V3580) (if (cons? V3454) (let Y (hd V3454) (let V3455 (shen.lazyderef (tl V3454) V3580) (if (= () V3455) (let V3456 (shen.lazyderef V3578 V3580) (if (= string V3456) (do (shen.incinfs) (shen.th* X string V3579 V3580 (freeze (shen.th* Y string V3579 V3580 V3581)))) (if (shen.pvar? V3456) (do (shen.bindv V3456 string V3580) (let Result (do (shen.incinfs) (shen.th* X string V3579 V3580 (freeze (shen.th* Y string V3579 V3580 V3581)))) (do (shen.unbindv V3456 V3580) Result))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3457 (shen.lazyderef V3577 V3580) (if (cons? V3457) (let V3458 (shen.lazyderef (hd V3457) V3580) (if (= lambda V3458) (let V3459 (shen.lazyderef (tl V3457) V3580) (if (cons? V3459) (let X (hd V3459) (let V3460 (shen.lazyderef (tl V3459) V3580) (if (cons? V3460) (let Y (hd V3460) (let V3461 (shen.lazyderef (tl V3460) V3580) (if (= () V3461) (let V3462 (shen.lazyderef V3578 V3580) (if (cons? V3462) (let A (hd V3462) (let V3463 (shen.lazyderef (tl V3462) V3580) (if (cons? V3463) (let V3464 (shen.lazyderef (hd V3463) V3580) (if (= --> V3464) (let V3465 (shen.lazyderef (tl V3463) V3580) (if (cons? V3465) (let B (hd V3465) (let V3466 (shen.lazyderef (tl V3465) V3580) (if (= () V3466) (let Z (shen.newpv V3580) (let X&& (shen.newpv V3580) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Y V3580)) V3580 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V3579) V3580 V3581)))))))))) (if (shen.pvar? V3466) (do (shen.bindv V3466 () V3580) (let Result (let Z (shen.newpv V3580) (let X&& (shen.newpv V3580) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Y V3580)) V3580 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V3579) V3580 V3581)))))))))) (do (shen.unbindv V3466 V3580) Result))) false)))) (if (shen.pvar? V3465) (let B (shen.newpv V3580) (do (shen.bindv V3465 (cons B ()) V3580) (let Result (let Z (shen.newpv V3580) (let X&& (shen.newpv V3580) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Y V3580)) V3580 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V3579) V3580 V3581)))))))))) (do (shen.unbindv V3465 V3580) Result)))) false))) (if (shen.pvar? V3464) (do (shen.bindv V3464 --> V3580) (let Result (let V3467 (shen.lazyderef (tl V3463) V3580) (if (cons? V3467) (let B (hd V3467) (let V3468 (shen.lazyderef (tl V3467) V3580) (if (= () V3468) (let Z (shen.newpv V3580) (let X&& (shen.newpv V3580) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Y V3580)) V3580 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V3579) V3580 V3581)))))))))) (if (shen.pvar? V3468) (do (shen.bindv V3468 () V3580) (let Result (let Z (shen.newpv V3580) (let X&& (shen.newpv V3580) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Y V3580)) V3580 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V3579) V3580 V3581)))))))))) (do (shen.unbindv V3468 V3580) Result))) false)))) (if (shen.pvar? V3467) (let B (shen.newpv V3580) (do (shen.bindv V3467 (cons B ()) V3580) (let Result (let Z (shen.newpv V3580) (let X&& (shen.newpv V3580) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Y V3580)) V3580 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V3579) V3580 V3581)))))))))) (do (shen.unbindv V3467 V3580) Result)))) false))) (do (shen.unbindv V3464 V3580) Result))) false))) (if (shen.pvar? V3463) (let B (shen.newpv V3580) (do (shen.bindv V3463 (cons --> (cons B ())) V3580) (let Result (let Z (shen.newpv V3580) (let X&& (shen.newpv V3580) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Y V3580)) V3580 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V3579) V3580 V3581)))))))))) (do (shen.unbindv V3463 V3580) Result)))) false)))) (if (shen.pvar? V3462) (let A (shen.newpv V3580) (let B (shen.newpv V3580) (do (shen.bindv V3462 (cons A (cons --> (cons B ()))) V3580) (let Result (let Z (shen.newpv V3580) (let X&& (shen.newpv V3580) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Y V3580)) V3580 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V3579) V3580 V3581)))))))))) (do (shen.unbindv V3462 V3580) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3469 (shen.lazyderef V3577 V3580) (if (cons? V3469) (let V3470 (shen.lazyderef (hd V3469) V3580) (if (= let V3470) (let V3471 (shen.lazyderef (tl V3469) V3580) (if (cons? V3471) (let X (hd V3471) (let V3472 (shen.lazyderef (tl V3471) V3580) (if (cons? V3472) (let Y (hd V3472) (let V3473 (shen.lazyderef (tl V3472) V3580) (if (cons? V3473) (let Z (hd V3473) (let V3474 (shen.lazyderef (tl V3473) V3580) (if (= () V3474) (let W (shen.newpv V3580) (let X&& (shen.newpv V3580) (let B (shen.newpv V3580) (do (shen.incinfs) (shen.th* Y B V3579 V3580 (freeze (bind X&& (shen.placeholder) V3580 (freeze (bind W (shen.ebr (shen.lazyderef X&& V3580) (shen.lazyderef X V3580) (shen.lazyderef Z V3580)) V3580 (freeze (shen.th* W V3578 (cons (cons X&& (cons : (cons B ()))) V3579) V3580 V3581))))))))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3475 (shen.lazyderef V3577 V3580) (if (cons? V3475) (let V3476 (shen.lazyderef (hd V3475) V3580) (if (= open V3476) (let V3477 (shen.lazyderef (tl V3475) V3580) (if (cons? V3477) (let FileName (hd V3477) (let V3478 (shen.lazyderef (tl V3477) V3580) (if (cons? V3478) (let Direction3408 (hd V3478) (let V3479 (shen.lazyderef (tl V3478) V3580) (if (= () V3479) (let V3480 (shen.lazyderef V3578 V3580) (if (cons? V3480) (let V3481 (shen.lazyderef (hd V3480) V3580) (if (= stream V3481) (let V3482 (shen.lazyderef (tl V3480) V3580) (if (cons? V3482) (let Direction (hd V3482) (let V3483 (shen.lazyderef (tl V3482) V3580) (if (= () V3483) (do (shen.incinfs) (unify! Direction Direction3408 V3580 (freeze (cut Throwcontrol V3580 (freeze (fwhen (element? (shen.lazyderef Direction V3580) (cons in (cons out ()))) V3580 (freeze (shen.th* FileName string V3579 V3580 V3581)))))))) (if (shen.pvar? V3483) (do (shen.bindv V3483 () V3580) (let Result (do (shen.incinfs) (unify! Direction Direction3408 V3580 (freeze (cut Throwcontrol V3580 (freeze (fwhen (element? (shen.lazyderef Direction V3580) (cons in (cons out ()))) V3580 (freeze (shen.th* FileName string V3579 V3580 V3581)))))))) (do (shen.unbindv V3483 V3580) Result))) false)))) (if (shen.pvar? V3482) (let Direction (shen.newpv V3580) (do (shen.bindv V3482 (cons Direction ()) V3580) (let Result (do (shen.incinfs) (unify! Direction Direction3408 V3580 (freeze (cut Throwcontrol V3580 (freeze (fwhen (element? (shen.lazyderef Direction V3580) (cons in (cons out ()))) V3580 (freeze (shen.th* FileName string V3579 V3580 V3581)))))))) (do (shen.unbindv V3482 V3580) Result)))) false))) (if (shen.pvar? V3481) (do (shen.bindv V3481 stream V3580) (let Result (let V3484 (shen.lazyderef (tl V3480) V3580) (if (cons? V3484) (let Direction (hd V3484) (let V3485 (shen.lazyderef (tl V3484) V3580) (if (= () V3485) (do (shen.incinfs) (unify! Direction Direction3408 V3580 (freeze (cut Throwcontrol V3580 (freeze (fwhen (element? (shen.lazyderef Direction V3580) (cons in (cons out ()))) V3580 (freeze (shen.th* FileName string V3579 V3580 V3581)))))))) (if (shen.pvar? V3485) (do (shen.bindv V3485 () V3580) (let Result (do (shen.incinfs) (unify! Direction Direction3408 V3580 (freeze (cut Throwcontrol V3580 (freeze (fwhen (element? (shen.lazyderef Direction V3580) (cons in (cons out ()))) V3580 (freeze (shen.th* FileName string V3579 V3580 V3581)))))))) (do (shen.unbindv V3485 V3580) Result))) false)))) (if (shen.pvar? V3484) (let Direction (shen.newpv V3580) (do (shen.bindv V3484 (cons Direction ()) V3580) (let Result (do (shen.incinfs) (unify! Direction Direction3408 V3580 (freeze (cut Throwcontrol V3580 (freeze (fwhen (element? (shen.lazyderef Direction V3580) (cons in (cons out ()))) V3580 (freeze (shen.th* FileName string V3579 V3580 V3581)))))))) (do (shen.unbindv V3484 V3580) Result)))) false))) (do (shen.unbindv V3481 V3580) Result))) false))) (if (shen.pvar? V3480) (let Direction (shen.newpv V3580) (do (shen.bindv V3480 (cons stream (cons Direction ())) V3580) (let Result (do (shen.incinfs) (unify! Direction Direction3408 V3580 (freeze (cut Throwcontrol V3580 (freeze (fwhen (element? (shen.lazyderef Direction V3580) (cons in (cons out ()))) V3580 (freeze (shen.th* FileName string V3579 V3580 V3581)))))))) (do (shen.unbindv V3480 V3580) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3486 (shen.lazyderef V3577 V3580) (if (cons? V3486) (let V3487 (shen.lazyderef (hd V3486) V3580) (if (= type V3487) (let V3488 (shen.lazyderef (tl V3486) V3580) (if (cons? V3488) (let X (hd V3488) (let V3489 (shen.lazyderef (tl V3488) V3580) (if (cons? V3489) (let A (hd V3489) (let V3490 (shen.lazyderef (tl V3489) V3580) (if (= () V3490) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (unify A V3578 V3580 (freeze (shen.th* X A V3579 V3580 V3581)))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3491 (shen.lazyderef V3577 V3580) (if (cons? V3491) (let V3492 (shen.lazyderef (hd V3491) V3580) (if (= input+ V3492) (let V3493 (shen.lazyderef (tl V3491) V3580) (if (cons? V3493) (let A (hd V3493) (let V3494 (shen.lazyderef (tl V3493) V3580) (if (cons? V3494) (let Stream (hd V3494) (let V3495 (shen.lazyderef (tl V3494) V3580) (if (= () V3495) (let C (shen.newpv V3580) (do (shen.incinfs) (bind C (shen.demodulate (shen.lazyderef A V3580)) V3580 (freeze (unify V3578 C V3580 (freeze (shen.th* Stream (cons stream (cons in ())) V3579 V3580 V3581))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3496 (shen.lazyderef V3577 V3580) (if (cons? V3496) (let V3497 (shen.lazyderef (hd V3496) V3580) (if (= set V3497) (let V3498 (shen.lazyderef (tl V3496) V3580) (if (cons? V3498) (let Var (hd V3498) (let V3499 (shen.lazyderef (tl V3498) V3580) (if (cons? V3499) (let Val (hd V3499) (let V3500 (shen.lazyderef (tl V3499) V3580) (if (= () V3500) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (shen.th* Var symbol V3579 V3580 (freeze (cut Throwcontrol V3580 (freeze (shen.th* (cons value (cons Var ())) V3578 V3579 V3580 (freeze (shen.th* Val V3578 V3579 V3580 V3581)))))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let NewHyp (shen.newpv V3580) (do (shen.incinfs) (shen.t*-hyps V3579 NewHyp V3580 (freeze (shen.th* V3577 V3578 NewHyp V3580 V3581))))) (if (= Case false) (let Case (let V3501 (shen.lazyderef V3577 V3580) (if (cons? V3501) (let V3502 (shen.lazyderef (hd V3501) V3580) (if (= define V3502) (let V3503 (shen.lazyderef (tl V3501) V3580) (if (cons? V3503) (let F (hd V3503) (let X (tl V3503) (do (shen.incinfs) (cut Throwcontrol V3580 (freeze (shen.t*-def (cons define (cons F X)) V3578 V3579 V3580 V3581)))))) false)) false)) false)) (if (= Case false) (let Case (let V3504 (shen.lazyderef V3577 V3580) (if (cons? V3504) (let V3505 (shen.lazyderef (hd V3504) V3580) (if (= defmacro V3505) (let V3506 (shen.lazyderef V3578 V3580) (if (= unit V3506) (do (shen.incinfs) (cut Throwcontrol V3580 V3581)) (if (shen.pvar? V3506) (do (shen.bindv V3506 unit V3580) (let Result (do (shen.incinfs) (cut Throwcontrol V3580 V3581)) (do (shen.unbindv V3506 V3580) Result))) false))) false)) false)) (if (= Case false) (let Case (let V3507 (shen.lazyderef V3577 V3580) (if (cons? V3507) (let V3508 (shen.lazyderef (hd V3507) V3580) (if (= shen.process-datatype V3508) (let V3509 (shen.lazyderef V3578 V3580) (if (= symbol V3509) (do (shen.incinfs) (thaw V3581)) (if (shen.pvar? V3509) (do (shen.bindv V3509 symbol V3580) (let Result (do (shen.incinfs) (thaw V3581)) (do (shen.unbindv V3509 V3580) Result))) false))) false)) false)) (if (= Case false) (let Case (let V3510 (shen.lazyderef V3577 V3580) (if (cons? V3510) (let V3511 (shen.lazyderef (hd V3510) V3580) (if (= shen.synonyms-help V3511) (let V3512 (shen.lazyderef V3578 V3580) (if (= symbol V3512) (do (shen.incinfs) (thaw V3581)) (if (shen.pvar? V3512) (do (shen.bindv V3512 symbol V3580) (let Result (do (shen.incinfs) (thaw V3581)) (do (shen.unbindv V3512 V3580) Result))) false))) false)) false)) (if (= Case false) (let Datatypes (shen.newpv V3580) (do (shen.incinfs) (bind Datatypes (value shen.*datatypes*) V3580 (freeze (shen.udefs* (cons V3577 (cons : (cons V3578 ()))) V3579 Datatypes V3580 V3581))))) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)) Case)))))

(defun shen.t*-hyps (V3586 V3587 V3588 V3589) (let Case (let V3323 (shen.lazyderef V3586 V3588) (if (cons? V3323) (let V3324 (shen.lazyderef (hd V3323) V3588) (if (cons? V3324) (let V3325 (shen.lazyderef (hd V3324) V3588) (if (cons? V3325) (let V3326 (shen.lazyderef (hd V3325) V3588) (if (= cons V3326) (let V3327 (shen.lazyderef (tl V3325) V3588) (if (cons? V3327) (let X (hd V3327) (let V3328 (shen.lazyderef (tl V3327) V3588) (if (cons? V3328) (let Y (hd V3328) (let V3329 (shen.lazyderef (tl V3328) V3588) (if (= () V3329) (let V3330 (shen.lazyderef (tl V3324) V3588) (if (cons? V3330) (let V3331 (shen.lazyderef (hd V3330) V3588) (if (= : V3331) (let V3332 (shen.lazyderef (tl V3330) V3588) (if (cons? V3332) (let V3333 (shen.lazyderef (hd V3332) V3588) (if (cons? V3333) (let V3334 (shen.lazyderef (hd V3333) V3588) (if (= list V3334) (let V3335 (shen.lazyderef (tl V3333) V3588) (if (cons? V3335) (let A (hd V3335) (let V3336 (shen.lazyderef (tl V3335) V3588) (if (= () V3336) (let V3337 (shen.lazyderef (tl V3332) V3588) (if (= () V3337) (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3337) (do (shen.bindv V3337 () V3588) (let Result (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3337 V3588) Result))) false))) (if (shen.pvar? V3336) (do (shen.bindv V3336 () V3588) (let Result (let V3338 (shen.lazyderef (tl V3332) V3588) (if (= () V3338) (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3338) (do (shen.bindv V3338 () V3588) (let Result (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3338 V3588) Result))) false))) (do (shen.unbindv V3336 V3588) Result))) false)))) (if (shen.pvar? V3335) (let A (shen.newpv V3588) (do (shen.bindv V3335 (cons A ()) V3588) (let Result (let V3339 (shen.lazyderef (tl V3332) V3588) (if (= () V3339) (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3339) (do (shen.bindv V3339 () V3588) (let Result (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3339 V3588) Result))) false))) (do (shen.unbindv V3335 V3588) Result)))) false))) (if (shen.pvar? V3334) (do (shen.bindv V3334 list V3588) (let Result (let V3340 (shen.lazyderef (tl V3333) V3588) (if (cons? V3340) (let A (hd V3340) (let V3341 (shen.lazyderef (tl V3340) V3588) (if (= () V3341) (let V3342 (shen.lazyderef (tl V3332) V3588) (if (= () V3342) (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3342) (do (shen.bindv V3342 () V3588) (let Result (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3342 V3588) Result))) false))) (if (shen.pvar? V3341) (do (shen.bindv V3341 () V3588) (let Result (let V3343 (shen.lazyderef (tl V3332) V3588) (if (= () V3343) (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3343) (do (shen.bindv V3343 () V3588) (let Result (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3343 V3588) Result))) false))) (do (shen.unbindv V3341 V3588) Result))) false)))) (if (shen.pvar? V3340) (let A (shen.newpv V3588) (do (shen.bindv V3340 (cons A ()) V3588) (let Result (let V3344 (shen.lazyderef (tl V3332) V3588) (if (= () V3344) (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3344) (do (shen.bindv V3344 () V3588) (let Result (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3344 V3588) Result))) false))) (do (shen.unbindv V3340 V3588) Result)))) false))) (do (shen.unbindv V3334 V3588) Result))) false))) (if (shen.pvar? V3333) (let A (shen.newpv V3588) (do (shen.bindv V3333 (cons list (cons A ())) V3588) (let Result (let V3345 (shen.lazyderef (tl V3332) V3588) (if (= () V3345) (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3345) (do (shen.bindv V3345 () V3588) (let Result (let Hyp (tl V3323) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons list (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3345 V3588) Result))) false))) (do (shen.unbindv V3333 V3588) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V3346 (shen.lazyderef V3586 V3588) (if (cons? V3346) (let V3347 (shen.lazyderef (hd V3346) V3588) (if (cons? V3347) (let V3348 (shen.lazyderef (hd V3347) V3588) (if (cons? V3348) (let V3349 (shen.lazyderef (hd V3348) V3588) (if (= @p V3349) (let V3350 (shen.lazyderef (tl V3348) V3588) (if (cons? V3350) (let X (hd V3350) (let V3351 (shen.lazyderef (tl V3350) V3588) (if (cons? V3351) (let Y (hd V3351) (let V3352 (shen.lazyderef (tl V3351) V3588) (if (= () V3352) (let V3353 (shen.lazyderef (tl V3347) V3588) (if (cons? V3353) (let V3354 (shen.lazyderef (hd V3353) V3588) (if (= : V3354) (let V3355 (shen.lazyderef (tl V3353) V3588) (if (cons? V3355) (let V3356 (shen.lazyderef (hd V3355) V3588) (if (cons? V3356) (let A (hd V3356) (let V3357 (shen.lazyderef (tl V3356) V3588) (if (cons? V3357) (let V3358 (shen.lazyderef (hd V3357) V3588) (if (= * V3358) (let V3359 (shen.lazyderef (tl V3357) V3588) (if (cons? V3359) (let B (hd V3359) (let V3360 (shen.lazyderef (tl V3359) V3588) (if (= () V3360) (let V3361 (shen.lazyderef (tl V3355) V3588) (if (= () V3361) (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3361) (do (shen.bindv V3361 () V3588) (let Result (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3361 V3588) Result))) false))) (if (shen.pvar? V3360) (do (shen.bindv V3360 () V3588) (let Result (let V3362 (shen.lazyderef (tl V3355) V3588) (if (= () V3362) (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3362) (do (shen.bindv V3362 () V3588) (let Result (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3362 V3588) Result))) false))) (do (shen.unbindv V3360 V3588) Result))) false)))) (if (shen.pvar? V3359) (let B (shen.newpv V3588) (do (shen.bindv V3359 (cons B ()) V3588) (let Result (let V3363 (shen.lazyderef (tl V3355) V3588) (if (= () V3363) (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3363) (do (shen.bindv V3363 () V3588) (let Result (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3363 V3588) Result))) false))) (do (shen.unbindv V3359 V3588) Result)))) false))) (if (shen.pvar? V3358) (do (shen.bindv V3358 * V3588) (let Result (let V3364 (shen.lazyderef (tl V3357) V3588) (if (cons? V3364) (let B (hd V3364) (let V3365 (shen.lazyderef (tl V3364) V3588) (if (= () V3365) (let V3366 (shen.lazyderef (tl V3355) V3588) (if (= () V3366) (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3366) (do (shen.bindv V3366 () V3588) (let Result (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3366 V3588) Result))) false))) (if (shen.pvar? V3365) (do (shen.bindv V3365 () V3588) (let Result (let V3367 (shen.lazyderef (tl V3355) V3588) (if (= () V3367) (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3367) (do (shen.bindv V3367 () V3588) (let Result (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3367 V3588) Result))) false))) (do (shen.unbindv V3365 V3588) Result))) false)))) (if (shen.pvar? V3364) (let B (shen.newpv V3588) (do (shen.bindv V3364 (cons B ()) V3588) (let Result (let V3368 (shen.lazyderef (tl V3355) V3588) (if (= () V3368) (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3368) (do (shen.bindv V3368 () V3588) (let Result (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3368 V3588) Result))) false))) (do (shen.unbindv V3364 V3588) Result)))) false))) (do (shen.unbindv V3358 V3588) Result))) false))) (if (shen.pvar? V3357) (let B (shen.newpv V3588) (do (shen.bindv V3357 (cons * (cons B ())) V3588) (let Result (let V3369 (shen.lazyderef (tl V3355) V3588) (if (= () V3369) (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3369) (do (shen.bindv V3369 () V3588) (let Result (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3369 V3588) Result))) false))) (do (shen.unbindv V3357 V3588) Result)))) false)))) (if (shen.pvar? V3356) (let A (shen.newpv V3588) (let B (shen.newpv V3588) (do (shen.bindv V3356 (cons A (cons * (cons B ()))) V3588) (let Result (let V3370 (shen.lazyderef (tl V3355) V3588) (if (= () V3370) (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3370) (do (shen.bindv V3370 () V3588) (let Result (let Hyp (tl V3346) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (shen.lazyderef B V3588) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3370 V3588) Result))) false))) (do (shen.unbindv V3356 V3588) Result))))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V3371 (shen.lazyderef V3586 V3588) (if (cons? V3371) (let V3372 (shen.lazyderef (hd V3371) V3588) (if (cons? V3372) (let V3373 (shen.lazyderef (hd V3372) V3588) (if (cons? V3373) (let V3374 (shen.lazyderef (hd V3373) V3588) (if (= @v V3374) (let V3375 (shen.lazyderef (tl V3373) V3588) (if (cons? V3375) (let X (hd V3375) (let V3376 (shen.lazyderef (tl V3375) V3588) (if (cons? V3376) (let Y (hd V3376) (let V3377 (shen.lazyderef (tl V3376) V3588) (if (= () V3377) (let V3378 (shen.lazyderef (tl V3372) V3588) (if (cons? V3378) (let V3379 (shen.lazyderef (hd V3378) V3588) (if (= : V3379) (let V3380 (shen.lazyderef (tl V3378) V3588) (if (cons? V3380) (let V3381 (shen.lazyderef (hd V3380) V3588) (if (cons? V3381) (let V3382 (shen.lazyderef (hd V3381) V3588) (if (= vector V3382) (let V3383 (shen.lazyderef (tl V3381) V3588) (if (cons? V3383) (let A (hd V3383) (let V3384 (shen.lazyderef (tl V3383) V3588) (if (= () V3384) (let V3385 (shen.lazyderef (tl V3380) V3588) (if (= () V3385) (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3385) (do (shen.bindv V3385 () V3588) (let Result (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3385 V3588) Result))) false))) (if (shen.pvar? V3384) (do (shen.bindv V3384 () V3588) (let Result (let V3386 (shen.lazyderef (tl V3380) V3588) (if (= () V3386) (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3386) (do (shen.bindv V3386 () V3588) (let Result (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3386 V3588) Result))) false))) (do (shen.unbindv V3384 V3588) Result))) false)))) (if (shen.pvar? V3383) (let A (shen.newpv V3588) (do (shen.bindv V3383 (cons A ()) V3588) (let Result (let V3387 (shen.lazyderef (tl V3380) V3588) (if (= () V3387) (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3387) (do (shen.bindv V3387 () V3588) (let Result (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3387 V3588) Result))) false))) (do (shen.unbindv V3383 V3588) Result)))) false))) (if (shen.pvar? V3382) (do (shen.bindv V3382 vector V3588) (let Result (let V3388 (shen.lazyderef (tl V3381) V3588) (if (cons? V3388) (let A (hd V3388) (let V3389 (shen.lazyderef (tl V3388) V3588) (if (= () V3389) (let V3390 (shen.lazyderef (tl V3380) V3588) (if (= () V3390) (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3390) (do (shen.bindv V3390 () V3588) (let Result (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3390 V3588) Result))) false))) (if (shen.pvar? V3389) (do (shen.bindv V3389 () V3588) (let Result (let V3391 (shen.lazyderef (tl V3380) V3588) (if (= () V3391) (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3391) (do (shen.bindv V3391 () V3588) (let Result (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3391 V3588) Result))) false))) (do (shen.unbindv V3389 V3588) Result))) false)))) (if (shen.pvar? V3388) (let A (shen.newpv V3588) (do (shen.bindv V3388 (cons A ()) V3588) (let Result (let V3392 (shen.lazyderef (tl V3380) V3588) (if (= () V3392) (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3392) (do (shen.bindv V3392 () V3588) (let Result (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3392 V3588) Result))) false))) (do (shen.unbindv V3388 V3588) Result)))) false))) (do (shen.unbindv V3382 V3588) Result))) false))) (if (shen.pvar? V3381) (let A (shen.newpv V3588) (do (shen.bindv V3381 (cons vector (cons A ())) V3588) (let Result (let V3393 (shen.lazyderef (tl V3380) V3588) (if (= () V3393) (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3393) (do (shen.bindv V3393 () V3588) (let Result (let Hyp (tl V3371) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons (shen.lazyderef A V3588) ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons (cons vector (cons (shen.lazyderef A V3588) ())) ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3393 V3588) Result))) false))) (do (shen.unbindv V3381 V3588) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V3394 (shen.lazyderef V3586 V3588) (if (cons? V3394) (let V3395 (shen.lazyderef (hd V3394) V3588) (if (cons? V3395) (let V3396 (shen.lazyderef (hd V3395) V3588) (if (cons? V3396) (let V3397 (shen.lazyderef (hd V3396) V3588) (if (= @s V3397) (let V3398 (shen.lazyderef (tl V3396) V3588) (if (cons? V3398) (let X (hd V3398) (let V3399 (shen.lazyderef (tl V3398) V3588) (if (cons? V3399) (let Y (hd V3399) (let V3400 (shen.lazyderef (tl V3399) V3588) (if (= () V3400) (let V3401 (shen.lazyderef (tl V3395) V3588) (if (cons? V3401) (let V3402 (shen.lazyderef (hd V3401) V3588) (if (= : V3402) (let V3403 (shen.lazyderef (tl V3401) V3588) (if (cons? V3403) (let V3404 (shen.lazyderef (hd V3403) V3588) (if (= string V3404) (let V3405 (shen.lazyderef (tl V3403) V3588) (if (= () V3405) (let Hyp (tl V3394) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons string ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3405) (do (shen.bindv V3405 () V3588) (let Result (let Hyp (tl V3394) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons string ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3405 V3588) Result))) false))) (if (shen.pvar? V3404) (do (shen.bindv V3404 string V3588) (let Result (let V3406 (shen.lazyderef (tl V3403) V3588) (if (= () V3406) (let Hyp (tl V3394) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons string ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (if (shen.pvar? V3406) (do (shen.bindv V3406 () V3588) (let Result (let Hyp (tl V3394) (do (shen.incinfs) (bind V3587 (cons (cons (shen.lazyderef X V3588) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V3588) (cons : (cons string ()))) (shen.lazyderef Hyp V3588))) V3588 V3589))) (do (shen.unbindv V3406 V3588) Result))) false))) (do (shen.unbindv V3404 V3588) Result))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let V3407 (shen.lazyderef V3586 V3588) (if (cons? V3407) (let X (hd V3407) (let Hyp (tl V3407) (let NewHyps (shen.newpv V3588) (do (shen.incinfs) (bind V3587 (cons (shen.lazyderef X V3588) (shen.lazyderef NewHyps V3588)) V3588 (freeze (shen.t*-hyps Hyp NewHyps V3588 V3589))))))) false)) Case)) Case)) Case)) Case)))

(defun shen.show (V3606 V3607 V3608 V3609) (cond ((value shen.*spy*) (do (shen.line) (do (shen.show-p (shen.deref V3606 V3608)) (do (nl 1) (do (nl 1) (do (shen.show-assumptions (shen.deref V3607 V3608) 1) (do (shen.prhush "
> " (stoutput)) (do (shen.pause-for-user) (thaw V3609))))))))) (true (thaw V3609))))

(defun shen.line () (let Infs (inferences) (shen.prhush (cn "____________________________________________________________ " (shen.app Infs (cn " inference" (shen.app (if (= 1 Infs) "" "s") " 
?- " shen.a)) shen.a)) (stoutput))))

(defun shen.show-p (V3611) (cond ((and (cons? V3611) (and (cons? (tl V3611)) (and (= : (hd (tl V3611))) (and (cons? (tl (tl V3611))) (= () (tl (tl (tl V3611)))))))) (shen.prhush (shen.app (hd V3611) (cn " : " (shen.app (hd (tl (tl V3611))) "" shen.r)) shen.r) (stoutput))) (true (shen.prhush (shen.app V3611 "" shen.r) (stoutput)))))

(defun shen.show-assumptions (V3616 V3617) (cond ((= () V3616) shen.skip) ((cons? V3616) (do (shen.prhush (shen.app V3617 ". " shen.a) (stoutput)) (do (shen.show-p (hd V3616)) (do (nl 1) (shen.show-assumptions (tl V3616) (+ V3617 1)))))) (true (shen.f_error shen.show-assumptions))))

(defun shen.pause-for-user () (let Byte (read-byte (stinput)) (if (= Byte 94) (simple-error "input aborted
") (nl 1))))

(defun shen.typedf? (V3619) (cons? (assoc V3619 (value shen.*signedfuncs*))))

(defun shen.sigf (V3621) (concat shen.type-signature-of- V3621))

(defun shen.placeholder () (gensym &&))

(defun shen.base (V3626 V3627 V3628 V3629) (let Case (let V3310 (shen.lazyderef V3627 V3628) (if (= number V3310) (do (shen.incinfs) (fwhen (number? (shen.lazyderef V3626 V3628)) V3628 V3629)) (if (shen.pvar? V3310) (do (shen.bindv V3310 number V3628) (let Result (do (shen.incinfs) (fwhen (number? (shen.lazyderef V3626 V3628)) V3628 V3629)) (do (shen.unbindv V3310 V3628) Result))) false))) (if (= Case false) (let Case (let V3311 (shen.lazyderef V3627 V3628) (if (= boolean V3311) (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V3626 V3628)) V3628 V3629)) (if (shen.pvar? V3311) (do (shen.bindv V3311 boolean V3628) (let Result (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V3626 V3628)) V3628 V3629)) (do (shen.unbindv V3311 V3628) Result))) false))) (if (= Case false) (let Case (let V3312 (shen.lazyderef V3627 V3628) (if (= string V3312) (do (shen.incinfs) (fwhen (string? (shen.lazyderef V3626 V3628)) V3628 V3629)) (if (shen.pvar? V3312) (do (shen.bindv V3312 string V3628) (let Result (do (shen.incinfs) (fwhen (string? (shen.lazyderef V3626 V3628)) V3628 V3629)) (do (shen.unbindv V3312 V3628) Result))) false))) (if (= Case false) (let Case (let V3313 (shen.lazyderef V3627 V3628) (if (= symbol V3313) (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V3626 V3628)) V3628 (freeze (fwhen (not (shen.ue? (shen.lazyderef V3626 V3628))) V3628 V3629)))) (if (shen.pvar? V3313) (do (shen.bindv V3313 symbol V3628) (let Result (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V3626 V3628)) V3628 (freeze (fwhen (not (shen.ue? (shen.lazyderef V3626 V3628))) V3628 V3629)))) (do (shen.unbindv V3313 V3628) Result))) false))) (if (= Case false) (let V3314 (shen.lazyderef V3626 V3628) (if (= () V3314) (let V3315 (shen.lazyderef V3627 V3628) (if (cons? V3315) (let V3316 (shen.lazyderef (hd V3315) V3628) (if (= list V3316) (let V3317 (shen.lazyderef (tl V3315) V3628) (if (cons? V3317) (let A (hd V3317) (let V3318 (shen.lazyderef (tl V3317) V3628) (if (= () V3318) (do (shen.incinfs) (thaw V3629)) (if (shen.pvar? V3318) (do (shen.bindv V3318 () V3628) (let Result (do (shen.incinfs) (thaw V3629)) (do (shen.unbindv V3318 V3628) Result))) false)))) (if (shen.pvar? V3317) (let A (shen.newpv V3628) (do (shen.bindv V3317 (cons A ()) V3628) (let Result (do (shen.incinfs) (thaw V3629)) (do (shen.unbindv V3317 V3628) Result)))) false))) (if (shen.pvar? V3316) (do (shen.bindv V3316 list V3628) (let Result (let V3319 (shen.lazyderef (tl V3315) V3628) (if (cons? V3319) (let A (hd V3319) (let V3320 (shen.lazyderef (tl V3319) V3628) (if (= () V3320) (do (shen.incinfs) (thaw V3629)) (if (shen.pvar? V3320) (do (shen.bindv V3320 () V3628) (let Result (do (shen.incinfs) (thaw V3629)) (do (shen.unbindv V3320 V3628) Result))) false)))) (if (shen.pvar? V3319) (let A (shen.newpv V3628) (do (shen.bindv V3319 (cons A ()) V3628) (let Result (do (shen.incinfs) (thaw V3629)) (do (shen.unbindv V3319 V3628) Result)))) false))) (do (shen.unbindv V3316 V3628) Result))) false))) (if (shen.pvar? V3315) (let A (shen.newpv V3628) (do (shen.bindv V3315 (cons list (cons A ())) V3628) (let Result (do (shen.incinfs) (thaw V3629)) (do (shen.unbindv V3315 V3628) Result)))) false))) false)) Case)) Case)) Case)) Case)))

(defun shen.by_hypothesis (V3635 V3636 V3637 V3638 V3639) (let Case (let V3301 (shen.lazyderef V3637 V3638) (if (cons? V3301) (let V3302 (shen.lazyderef (hd V3301) V3638) (if (cons? V3302) (let Y (hd V3302) (let V3303 (shen.lazyderef (tl V3302) V3638) (if (cons? V3303) (let V3304 (shen.lazyderef (hd V3303) V3638) (if (= : V3304) (let V3305 (shen.lazyderef (tl V3303) V3638) (if (cons? V3305) (let B (hd V3305) (let V3306 (shen.lazyderef (tl V3305) V3638) (if (= () V3306) (do (shen.incinfs) (identical V3635 Y V3638 (freeze (unify! V3636 B V3638 V3639)))) false))) false)) false)) false))) false)) false)) (if (= Case false) (let V3307 (shen.lazyderef V3637 V3638) (if (cons? V3307) (let Hyp (tl V3307) (do (shen.incinfs) (shen.by_hypothesis V3635 V3636 Hyp V3638 V3639))) false)) Case)))

(defun shen.t*-def (V3645 V3646 V3647 V3648 V3649) (let V3295 (shen.lazyderef V3645 V3648) (if (cons? V3295) (let V3296 (shen.lazyderef (hd V3295) V3648) (if (= define V3296) (let V3297 (shen.lazyderef (tl V3295) V3648) (if (cons? V3297) (let F (hd V3297) (let X (tl V3297) (let Y (shen.newpv V3648) (let E (shen.newpv V3648) (do (shen.incinfs) (shen.t*-defh (compile (lambda Y (shen.<sig+rules> Y)) X (lambda E (if (cons? E) (simple-error (cn "parse error here: " (shen.app E "
" shen.s))) (simple-error "parse error
")))) F V3646 V3647 V3648 V3649)))))) false)) false)) false)))

(defun shen.t*-defh (V3656 V3657 V3658 V3659 V3660 V3661) (let V3291 (shen.lazyderef V3656 V3660) (if (cons? V3291) (let Sig (hd V3291) (let Rules (tl V3291) (do (shen.incinfs) (shen.t*-defhh Sig (shen.ue-sig Sig) V3657 V3658 V3659 Rules V3660 V3661)))) false)))

(defun shen.t*-defhh (V3670 V3671 V3672 V3673 V3674 V3675 V3676 V3677) (do (shen.incinfs) (shen.t*-rules V3675 V3671 1 V3672 (cons (cons V3672 (cons : (cons V3671 ()))) V3674) V3676 (freeze (shen.memo V3672 V3670 V3673 V3676 V3677)))))

(defun shen.memo (V3683 V3684 V3685 V3686 V3687) (let Jnk (shen.newpv V3686) (do (shen.incinfs) (unify! V3685 V3684 V3686 (freeze (bind Jnk (declare (shen.lazyderef V3683 V3686) (shen.lazyderef V3685 V3686)) V3686 V3687))))))

(defun shen.<sig+rules> (V3689) (let Parse_shen.<signature> (shen.<signature> V3689) (if (not (= (fail) Parse_shen.<signature>)) (let Parse_shen.<non-ll-rules> (shen.<non-ll-rules> Parse_shen.<signature>) (if (not (= (fail) Parse_shen.<non-ll-rules>)) (shen.pair (hd Parse_shen.<non-ll-rules>) (cons (shen.hdtl Parse_shen.<signature>) (shen.hdtl Parse_shen.<non-ll-rules>))) (fail))) (fail))))

(defun shen.<non-ll-rules> (V3691) (let YaccParse (let Parse_shen.<rule> (shen.<rule> V3691) (if (not (= (fail) Parse_shen.<rule>)) (let Parse_shen.<non-ll-rules> (shen.<non-ll-rules> Parse_shen.<rule>) (if (not (= (fail) Parse_shen.<non-ll-rules>)) (shen.pair (hd Parse_shen.<non-ll-rules>) (cons (shen.hdtl Parse_shen.<rule>) (shen.hdtl Parse_shen.<non-ll-rules>))) (fail))) (fail))) (if (= YaccParse (fail)) (let Parse_shen.<rule> (shen.<rule> V3691) (if (not (= (fail) Parse_shen.<rule>)) (shen.pair (hd Parse_shen.<rule>) (cons (shen.hdtl Parse_shen.<rule>) ())) (fail))) YaccParse)))

(defun shen.ue (V3693) (cond ((and (cons? V3693) (and (cons? (tl V3693)) (and (= () (tl (tl V3693))) (= (hd V3693) protect)))) V3693) ((cons? V3693) (map (lambda Z (shen.ue Z)) V3693)) ((variable? V3693) (concat && V3693)) (true V3693)))

(defun shen.ue-sig (V3695) (cond ((cons? V3695) (map (lambda Z (shen.ue-sig Z)) V3695)) ((variable? V3695) (concat &&& V3695)) (true V3695)))

(defun shen.ues (V3701) (cond ((shen.ue? V3701) (cons V3701 ())) ((cons? V3701) (union (shen.ues (hd V3701)) (shen.ues (tl V3701)))) (true ())))

(defun shen.ue? (V3703) (and (symbol? V3703) (shen.ue-h? (str V3703))))

(defun shen.ue-h? (V3711) (cond ((and (shen.+string? V3711) (and (= "&" (pos V3711 0)) (and (shen.+string? (tlstr V3711)) (= "&" (pos (tlstr V3711) 0))))) true) (true false)))

(defun shen.t*-rules (V3719 V3720 V3721 V3722 V3723 V3724 V3725) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V3275 (shen.lazyderef V3719 V3724) (if (= () V3275) (do (shen.incinfs) (thaw V3725)) false)) (if (= Case false) (let Case (let V3276 (shen.lazyderef V3719 V3724) (if (cons? V3276) (let Rule (hd V3276) (let Rules (tl V3276) (do (shen.incinfs) (shen.t*-rule (shen.ue Rule) V3720 V3723 V3724 (freeze (cut Throwcontrol V3724 (freeze (shen.t*-rules Rules V3720 (+ V3721 1) V3722 V3723 V3724 V3725)))))))) false)) (if (= Case false) (let Err (shen.newpv V3724) (do (shen.incinfs) (bind Err (simple-error (cn "type error in rule " (shen.app (shen.lazyderef V3721 V3724) (cn " of " (shen.app (shen.lazyderef V3722 V3724) "" shen.a)) shen.a))) V3724 V3725))) Case)) Case)))))

(defun shen.t*-rule (V3731 V3732 V3733 V3734 V3735) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let V3267 (shen.lazyderef V3731 V3734) (if (cons? V3267) (let Patterns (hd V3267) (let V3268 (shen.lazyderef (tl V3267) V3734) (if (cons? V3268) (let Action (hd V3268) (let V3269 (shen.lazyderef (tl V3268) V3734) (if (= () V3269) (let NewHyps (shen.newpv V3734) (do (shen.incinfs) (shen.newhyps (shen.placeholders Patterns) V3733 NewHyps V3734 (freeze (shen.t*-patterns Patterns V3732 NewHyps V3734 (freeze (cut Throwcontrol V3734 (freeze (shen.t*-action (shen.curry (shen.ue Action)) (shen.result-type Patterns V3732) (shen.patthyps Patterns V3732 V3733) V3734 V3735))))))))) false))) false))) false)))))

(defun shen.placeholders (V3741) (cond ((shen.ue? V3741) (cons V3741 ())) ((cons? V3741) (union (shen.placeholders (hd V3741)) (shen.placeholders (tl V3741)))) (true ())))

(defun shen.newhyps (V3747 V3748 V3749 V3750 V3751) (let Case (let V3254 (shen.lazyderef V3747 V3750) (if (= () V3254) (do (shen.incinfs) (unify! V3749 V3748 V3750 V3751)) false)) (if (= Case false) (let V3255 (shen.lazyderef V3747 V3750) (if (cons? V3255) (let V3250 (hd V3255) (let Vs (tl V3255) (let V3256 (shen.lazyderef V3749 V3750) (if (cons? V3256) (let V3257 (shen.lazyderef (hd V3256) V3750) (if (cons? V3257) (let V (hd V3257) (let V3258 (shen.lazyderef (tl V3257) V3750) (if (cons? V3258) (let V3259 (shen.lazyderef (hd V3258) V3750) (if (= : V3259) (let V3260 (shen.lazyderef (tl V3258) V3750) (if (cons? V3260) (let A (hd V3260) (let V3261 (shen.lazyderef (tl V3260) V3750) (if (= () V3261) (let NewHyp (tl V3256) (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (if (shen.pvar? V3261) (do (shen.bindv V3261 () V3750) (let Result (let NewHyp (tl V3256) (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (do (shen.unbindv V3261 V3750) Result))) false)))) (if (shen.pvar? V3260) (let A (shen.newpv V3750) (do (shen.bindv V3260 (cons A ()) V3750) (let Result (let NewHyp (tl V3256) (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (do (shen.unbindv V3260 V3750) Result)))) false))) (if (shen.pvar? V3259) (do (shen.bindv V3259 : V3750) (let Result (let V3262 (shen.lazyderef (tl V3258) V3750) (if (cons? V3262) (let A (hd V3262) (let V3263 (shen.lazyderef (tl V3262) V3750) (if (= () V3263) (let NewHyp (tl V3256) (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (if (shen.pvar? V3263) (do (shen.bindv V3263 () V3750) (let Result (let NewHyp (tl V3256) (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (do (shen.unbindv V3263 V3750) Result))) false)))) (if (shen.pvar? V3262) (let A (shen.newpv V3750) (do (shen.bindv V3262 (cons A ()) V3750) (let Result (let NewHyp (tl V3256) (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (do (shen.unbindv V3262 V3750) Result)))) false))) (do (shen.unbindv V3259 V3750) Result))) false))) (if (shen.pvar? V3258) (let A (shen.newpv V3750) (do (shen.bindv V3258 (cons : (cons A ())) V3750) (let Result (let NewHyp (tl V3256) (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (do (shen.unbindv V3258 V3750) Result)))) false)))) (if (shen.pvar? V3257) (let V (shen.newpv V3750) (let A (shen.newpv V3750) (do (shen.bindv V3257 (cons V (cons : (cons A ()))) V3750) (let Result (let NewHyp (tl V3256) (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (do (shen.unbindv V3257 V3750) Result))))) false))) (if (shen.pvar? V3256) (let V (shen.newpv V3750) (let A (shen.newpv V3750) (let NewHyp (shen.newpv V3750) (do (shen.bindv V3256 (cons (cons V (cons : (cons A ()))) NewHyp) V3750) (let Result (do (shen.incinfs) (unify! V V3250 V3750 (freeze (shen.newhyps Vs V3748 NewHyp V3750 V3751)))) (do (shen.unbindv V3256 V3750) Result)))))) false))))) false)) Case)))

(defun shen.patthyps (V3757 V3758 V3759) (cond ((= () V3757) V3759) ((and (cons? V3757) (and (cons? V3758) (and (cons? (tl V3758)) (and (= --> (hd (tl V3758))) (and (cons? (tl (tl V3758))) (= () (tl (tl (tl V3758))))))))) (adjoin (cons (hd V3757) (cons : (cons (hd V3758) ()))) (shen.patthyps (tl V3757) (hd (tl (tl V3758))) V3759))) (true (shen.f_error shen.patthyps))))

(defun shen.result-type (V3766 V3767) (cond ((and (= () V3766) (and (cons? V3767) (and (= --> (hd V3767)) (and (cons? (tl V3767)) (= () (tl (tl V3767))))))) (hd (tl V3767))) ((= () V3766) V3767) ((and (cons? V3766) (and (cons? V3767) (and (cons? (tl V3767)) (and (= --> (hd (tl V3767))) (and (cons? (tl (tl V3767))) (= () (tl (tl (tl V3767))))))))) (shen.result-type (tl V3766) (hd (tl (tl V3767))))) (true (shen.f_error shen.result-type))))

(defun shen.t*-patterns (V3773 V3774 V3775 V3776 V3777) (let Case (let V3242 (shen.lazyderef V3773 V3776) (if (= () V3242) (do (shen.incinfs) (thaw V3777)) false)) (if (= Case false) (let V3243 (shen.lazyderef V3773 V3776) (if (cons? V3243) (let Pattern (hd V3243) (let Patterns (tl V3243) (let V3244 (shen.lazyderef V3774 V3776) (if (cons? V3244) (let A (hd V3244) (let V3245 (shen.lazyderef (tl V3244) V3776) (if (cons? V3245) (let V3246 (shen.lazyderef (hd V3245) V3776) (if (= --> V3246) (let V3247 (shen.lazyderef (tl V3245) V3776) (if (cons? V3247) (let B (hd V3247) (let V3248 (shen.lazyderef (tl V3247) V3776) (if (= () V3248) (do (shen.incinfs) (shen.t* (cons Pattern (cons : (cons A ()))) V3775 V3776 (freeze (shen.t*-patterns Patterns B V3775 V3776 V3777)))) false))) false)) false)) false))) false)))) false)) Case)))

(defun shen.t*-action (V3783 V3784 V3785 V3786 V3787) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V3219 (shen.lazyderef V3783 V3786) (if (cons? V3219) (let V3220 (shen.lazyderef (hd V3219) V3786) (if (= where V3220) (let V3221 (shen.lazyderef (tl V3219) V3786) (if (cons? V3221) (let P (hd V3221) (let V3222 (shen.lazyderef (tl V3221) V3786) (if (cons? V3222) (let Action (hd V3222) (let V3223 (shen.lazyderef (tl V3222) V3786) (if (= () V3223) (do (shen.incinfs) (cut Throwcontrol V3786 (freeze (shen.t* (cons P (cons : (cons boolean ()))) V3785 V3786 (freeze (cut Throwcontrol V3786 (freeze (shen.t*-action Action V3784 (cons (cons P (cons : (cons verified ()))) V3785) V3786 V3787)))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V3224 (shen.lazyderef V3783 V3786) (if (cons? V3224) (let V3225 (shen.lazyderef (hd V3224) V3786) (if (= shen.choicepoint! V3225) (let V3226 (shen.lazyderef (tl V3224) V3786) (if (cons? V3226) (let V3227 (shen.lazyderef (hd V3226) V3786) (if (cons? V3227) (let V3228 (shen.lazyderef (hd V3227) V3786) (if (cons? V3228) (let V3229 (shen.lazyderef (hd V3228) V3786) (if (= fail-if V3229) (let V3230 (shen.lazyderef (tl V3228) V3786) (if (cons? V3230) (let F (hd V3230) (let V3231 (shen.lazyderef (tl V3230) V3786) (if (= () V3231) (let V3232 (shen.lazyderef (tl V3227) V3786) (if (cons? V3232) (let Action (hd V3232) (let V3233 (shen.lazyderef (tl V3232) V3786) (if (= () V3233) (let V3234 (shen.lazyderef (tl V3226) V3786) (if (= () V3234) (do (shen.incinfs) (cut Throwcontrol V3786 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons F (cons Action ())) ())) (cons Action ()))) V3784 V3785 V3786 V3787)))) false)) false))) false)) false))) false)) false)) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V3235 (shen.lazyderef V3783 V3786) (if (cons? V3235) (let V3236 (shen.lazyderef (hd V3235) V3786) (if (= shen.choicepoint! V3236) (let V3237 (shen.lazyderef (tl V3235) V3786) (if (cons? V3237) (let Action (hd V3237) (let V3238 (shen.lazyderef (tl V3237) V3786) (if (= () V3238) (do (shen.incinfs) (cut Throwcontrol V3786 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons (cons = (cons Action ())) (cons (cons fail ()) ())) ())) (cons Action ()))) V3784 V3785 V3786 V3787)))) false))) false)) false)) false)) (if (= Case false) (do (shen.incinfs) (shen.t* (cons V3783 (cons : (cons V3784 ()))) V3785 V3786 V3787)) Case)) Case)) Case)))))

(defun findall (V3793 V3794 V3795 V3796 V3797) (let B (shen.newpv V3796) (let A (shen.newpv V3796) (do (shen.incinfs) (bind A (gensym shen.a) V3796 (freeze (bind B (set (shen.lazyderef A V3796) ()) V3796 (freeze (shen.findallhelp V3793 V3794 V3795 A V3796 V3797)))))))))

(defun shen.findallhelp (V3804 V3805 V3806 V3807 V3808 V3809) (let Case (do (shen.incinfs) (call V3805 V3808 (freeze (shen.remember V3807 V3804 V3808 (freeze (fwhen false V3808 V3809)))))) (if (= Case false) (do (shen.incinfs) (bind V3806 (value (shen.lazyderef V3807 V3808)) V3808 V3809)) Case)))

(defun shen.remember (V3814 V3815 V3816 V3817) (let B (shen.newpv V3816) (do (shen.incinfs) (bind B (set (shen.deref V3814 V3816) (cons (shen.deref V3815 V3816) (value (shen.deref V3814 V3816)))) V3816 V3817))))