"Copyright (c) 2015, Mark Tarver\n\nAll rights reserved.\n\nRedistribution and use in source and binary forms, with or without\nmodification, are permitted provided that the following conditions are met:\n1. Redistributions of source code must retain the above copyright\n   notice, this list of conditions and the following disclaimer.\n2. Redistributions in binary form must reproduce the above copyright\n   notice, this list of conditions and the following disclaimer in the\n   documentation and/or other materials provided with the distribution.\n3. The name of Mark Tarver may not be used to endorse or promote products\n   derived from this software without specific prior written permission.\n\nTHIS SOFTWARE IS PROVIDED BY Mark Tarver ''AS IS'' AND ANY\nEXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED\nWARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE\nDISCLAIMED. IN NO EVENT SHALL Mark Tarver BE LIABLE FOR ANY\nDIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES\n(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;\nLOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND\nON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT\n(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS\nSOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
(begin (register-function-arity (quote shen.typecheck) 2) (define (kl:shen.typecheck V3528 V3529) (let ((Curry (kl:shen.curry V3528))) (let ((ProcessN (kl:shen.start-new-prolog-process))) (let ((Type (kl:shen.insert-prolog-variables (kl:shen.demodulate (kl:shen.curry-type V3529)) ProcessN))) (let ((Continuation (lambda () (kl:return Type ProcessN (quote shen.void))))) (kl:shen.t* (cons Curry (cons (quote :) (cons Type (quote ())))) (quote ()) ProcessN Continuation)))))) (quote shen.typecheck))
(begin (register-function-arity (quote shen.curry) 1) (define (kl:shen.curry V3531) (cond ((and (pair? V3531) (assert-boolean (kl:shen.special? (car V3531)))) (cons (car V3531) (kl:map (lambda (Y) (kl:shen.curry Y)) (cdr V3531)))) ((and (pair? V3531) (and (pair? (cdr V3531)) (assert-boolean (kl:shen.extraspecial? (car V3531))))) V3531) ((and (pair? V3531) (and (eq? (quote type) (car V3531)) (and (pair? (cdr V3531)) (and (pair? (cdr (cdr V3531))) (null? (cdr (cdr (cdr V3531)))))))) (cons (quote type) (cons (kl:shen.curry (car (cdr V3531))) (cdr (cdr V3531))))) ((and (pair? V3531) (and (pair? (cdr V3531)) (pair? (cdr (cdr V3531))))) (kl:shen.curry (cons (cons (car V3531) (cons (car (cdr V3531)) (quote ()))) (cdr (cdr V3531))))) ((and (pair? V3531) (and (pair? (cdr V3531)) (null? (cdr (cdr V3531))))) (cons (kl:shen.curry (car V3531)) (cons (kl:shen.curry (car (cdr V3531))) (quote ())))) (#t V3531))) (quote shen.curry))
(begin (register-function-arity (quote shen.special?) 1) (define (kl:shen.special? V3533) (kl:element? V3533 (kl:value (quote shen.*special*)))) (quote shen.special?))
(begin (register-function-arity (quote shen.extraspecial?) 1) (define (kl:shen.extraspecial? V3535) (kl:element? V3535 (kl:value (quote shen.*extraspecial*)))) (quote shen.extraspecial?))
(begin (register-function-arity (quote shen.t*) 4) (define (kl:shen.t* V3540 V3541 V3542 V3543) (let ((Throwcontrol (kl:shen.catchpoint))) (kl:shen.cutpoint Throwcontrol (let ((Case (let ((Error (kl:shen.newpv V3542))) (begin (kl:shen.incinfs) (kl:fwhen (kl:shen.maxinfexceeded?) V3542 (lambda () (kl:bind Error (kl:shen.errormaxinfs) V3542 V3543))))))) (if (kl:= Case #f) (let ((Case (let ((V3520 (kl:shen.lazyderef V3540 V3542))) (if (eq? (quote fail) V3520) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3542 (lambda () (kl:shen.prolog-failure V3542 V3543)))) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3521 (kl:shen.lazyderef V3540 V3542))) (if (pair? V3521) (let ((X (car V3521))) (let ((V3522 (kl:shen.lazyderef (cdr V3521) V3542))) (if (pair? V3522) (let ((V3523 (kl:shen.lazyderef (car V3522) V3542))) (if (eq? (quote :) V3523) (let ((V3524 (kl:shen.lazyderef (cdr V3522) V3542))) (if (pair? V3524) (let ((A (car V3524))) (let ((V3525 (kl:shen.lazyderef (cdr V3524) V3542))) (if (null? V3525) (begin (kl:shen.incinfs) (kl:fwhen (kl:shen.type-theory-enabled?) V3542 (lambda () (kl:cut Throwcontrol V3542 (lambda () (kl:shen.th* X A V3541 V3542 V3543)))))) #f))) #f)) #f)) #f))) #f)))) (if (kl:= Case #f) (let ((Datatypes (kl:shen.newpv V3542))) (begin (kl:shen.incinfs) (kl:shen.show V3540 V3541 V3542 (lambda () (kl:bind Datatypes (kl:value (quote shen.*datatypes*)) V3542 (lambda () (kl:shen.udefs* V3540 V3541 Datatypes V3542 V3543))))))) Case)) Case)) Case))))) (quote shen.t*))
(begin (register-function-arity (quote shen.type-theory-enabled?) 0) (define (kl:shen.type-theory-enabled?) (kl:value (quote shen.*shen-type-theory-enabled?*))) (quote shen.type-theory-enabled?))
(begin (register-function-arity (quote enable-type-theory) 1) (define (kl:enable-type-theory V3549) (cond ((eq? (quote +) V3549) (kl:set (quote shen.*shen-type-theory-enabled?*) #t)) ((eq? (quote -) V3549) (kl:set (quote shen.*shen-type-theory-enabled?*) #f)) (#t (simple-error "enable-type-theory expects a + or a -\n")))) (quote enable-type-theory))
(begin (register-function-arity (quote shen.prolog-failure) 2) (define (kl:shen.prolog-failure V3560 V3561) #f) (quote shen.prolog-failure))
(begin (register-function-arity (quote shen.maxinfexceeded?) 0) (define (kl:shen.maxinfexceeded?) (> (kl:inferences) (kl:value (quote shen.*maxinferences*)))) (quote shen.maxinfexceeded?))
(begin (register-function-arity (quote shen.errormaxinfs) 0) (define (kl:shen.errormaxinfs) (simple-error "maximum inferences exceeded~%")) (quote shen.errormaxinfs))
(begin (register-function-arity (quote shen.udefs*) 5) (define (kl:shen.udefs* V3567 V3568 V3569 V3570 V3571) (let ((Case (let ((V3516 (kl:shen.lazyderef V3569 V3570))) (if (pair? V3516) (let ((D (car V3516))) (begin (kl:shen.incinfs) (kl:call (cons D (cons V3567 (cons V3568 (quote ())))) V3570 V3571))) #f)))) (if (kl:= Case #f) (let ((V3517 (kl:shen.lazyderef V3569 V3570))) (if (pair? V3517) (let ((Ds (cdr V3517))) (begin (kl:shen.incinfs) (kl:shen.udefs* V3567 V3568 Ds V3570 V3571))) #f)) Case))) (quote shen.udefs*))
(begin (register-function-arity (quote shen.th*) 5) (define (kl:shen.th* V3577 V3578 V3579 V3580 V3581) (let ((Throwcontrol (kl:shen.catchpoint))) (kl:shen.cutpoint Throwcontrol (let ((Case (begin (kl:shen.incinfs) (kl:shen.show (cons V3577 (cons (quote :) (cons V3578 (quote ())))) V3579 V3580 (lambda () (kl:fwhen #f V3580 V3581)))))) (if (kl:= Case #f) (let ((Case (let ((F (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:fwhen (kl:shen.typedf? (kl:shen.lazyderef V3577 V3580)) V3580 (lambda () (kl:bind F (kl:shen.sigf (kl:shen.lazyderef V3577 V3580)) V3580 (lambda () (kl:call (cons F (cons V3578 (quote ()))) V3580 V3581))))))))) (if (kl:= Case #f) (let ((Case (begin (kl:shen.incinfs) (kl:shen.base V3577 V3578 V3580 V3581)))) (if (kl:= Case #f) (let ((Case (begin (kl:shen.incinfs) (kl:shen.by_hypothesis V3577 V3578 V3579 V3580 V3581)))) (if (kl:= Case #f) (let ((Case (let ((V3412 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3412) (let ((F (car V3412))) (let ((V3413 (kl:shen.lazyderef (cdr V3412) V3580))) (if (null? V3413) (begin (kl:shen.incinfs) (kl:shen.th* F (cons (quote -->) (cons V3578 (quote ()))) V3579 V3580 V3581)) #f))) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3414 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3414) (let ((F (car V3414))) (let ((V3415 (kl:shen.lazyderef (cdr V3414) V3580))) (if (pair? V3415) (let ((X (car V3415))) (let ((V3416 (kl:shen.lazyderef (cdr V3415) V3580))) (if (null? V3416) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:shen.th* F (cons B (cons (quote -->) (cons V3578 (quote ())))) V3579 V3580 (lambda () (kl:shen.th* X B V3579 V3580 V3581))))) #f))) #f))) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3417 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3417) (let ((V3418 (kl:shen.lazyderef (car V3417) V3580))) (if (eq? (quote cons) V3418) (let ((V3419 (kl:shen.lazyderef (cdr V3417) V3580))) (if (pair? V3419) (let ((X (car V3419))) (let ((V3420 (kl:shen.lazyderef (cdr V3419) V3580))) (if (pair? V3420) (let ((Y (car V3420))) (let ((V3421 (kl:shen.lazyderef (cdr V3420) V3580))) (if (null? V3421) (let ((V3422 (kl:shen.lazyderef V3578 V3580))) (if (pair? V3422) (let ((V3423 (kl:shen.lazyderef (car V3422) V3580))) (if (eq? (quote list) V3423) (let ((V3424 (kl:shen.lazyderef (cdr V3422) V3580))) (if (pair? V3424) (let ((A (car V3424))) (let ((V3425 (kl:shen.lazyderef (cdr V3424) V3580))) (if (null? V3425) (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote list) (cons A (quote ()))) V3579 V3580 V3581)))) (if (kl:shen.pvar? V3425) (begin (kl:shen.bindv V3425 (quote ()) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote list) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3425 V3580) Result))) #f)))) (if (kl:shen.pvar? V3424) (let ((A (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3424 (cons A (quote ())) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote list) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3424 V3580) Result)))) #f))) (if (kl:shen.pvar? V3423) (begin (kl:shen.bindv V3423 (quote list) V3580) (let ((Result (let ((V3426 (kl:shen.lazyderef (cdr V3422) V3580))) (if (pair? V3426) (let ((A (car V3426))) (let ((V3427 (kl:shen.lazyderef (cdr V3426) V3580))) (if (null? V3427) (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote list) (cons A (quote ()))) V3579 V3580 V3581)))) (if (kl:shen.pvar? V3427) (begin (kl:shen.bindv V3427 (quote ()) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote list) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3427 V3580) Result))) #f)))) (if (kl:shen.pvar? V3426) (let ((A (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3426 (cons A (quote ())) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote list) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3426 V3580) Result)))) #f))))) (begin (kl:shen.unbindv V3423 V3580) Result))) #f))) (if (kl:shen.pvar? V3422) (let ((A (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3422 (cons (quote list) (cons A (quote ()))) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote list) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3422 V3580) Result)))) #f))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3428 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3428) (let ((V3429 (kl:shen.lazyderef (car V3428) V3580))) (if (eq? (quote _scheme_at_p) V3429) (let ((V3430 (kl:shen.lazyderef (cdr V3428) V3580))) (if (pair? V3430) (let ((X (car V3430))) (let ((V3431 (kl:shen.lazyderef (cdr V3430) V3580))) (if (pair? V3431) (let ((Y (car V3431))) (let ((V3432 (kl:shen.lazyderef (cdr V3431) V3580))) (if (null? V3432) (let ((V3433 (kl:shen.lazyderef V3578 V3580))) (if (pair? V3433) (let ((A (car V3433))) (let ((V3434 (kl:shen.lazyderef (cdr V3433) V3580))) (if (pair? V3434) (let ((V3435 (kl:shen.lazyderef (car V3434) V3580))) (if (eq? (quote *) V3435) (let ((V3436 (kl:shen.lazyderef (cdr V3434) V3580))) (if (pair? V3436) (let ((B (car V3436))) (let ((V3437 (kl:shen.lazyderef (cdr V3436) V3580))) (if (null? V3437) (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y B V3579 V3580 V3581)))) (if (kl:shen.pvar? V3437) (begin (kl:shen.bindv V3437 (quote ()) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y B V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3437 V3580) Result))) #f)))) (if (kl:shen.pvar? V3436) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3436 (cons B (quote ())) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y B V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3436 V3580) Result)))) #f))) (if (kl:shen.pvar? V3435) (begin (kl:shen.bindv V3435 (quote *) V3580) (let ((Result (let ((V3438 (kl:shen.lazyderef (cdr V3434) V3580))) (if (pair? V3438) (let ((B (car V3438))) (let ((V3439 (kl:shen.lazyderef (cdr V3438) V3580))) (if (null? V3439) (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y B V3579 V3580 V3581)))) (if (kl:shen.pvar? V3439) (begin (kl:shen.bindv V3439 (quote ()) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y B V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3439 V3580) Result))) #f)))) (if (kl:shen.pvar? V3438) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3438 (cons B (quote ())) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y B V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3438 V3580) Result)))) #f))))) (begin (kl:shen.unbindv V3435 V3580) Result))) #f))) (if (kl:shen.pvar? V3434) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3434 (cons (quote *) (cons B (quote ()))) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y B V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3434 V3580) Result)))) #f)))) (if (kl:shen.pvar? V3433) (let ((A (kl:shen.newpv V3580))) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3433 (cons A (cons (quote *) (cons B (quote ())))) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y B V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3433 V3580) Result))))) #f))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3440 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3440) (let ((V3441 (kl:shen.lazyderef (car V3440) V3580))) (if (eq? (quote _scheme_at_v) V3441) (let ((V3442 (kl:shen.lazyderef (cdr V3440) V3580))) (if (pair? V3442) (let ((X (car V3442))) (let ((V3443 (kl:shen.lazyderef (cdr V3442) V3580))) (if (pair? V3443) (let ((Y (car V3443))) (let ((V3444 (kl:shen.lazyderef (cdr V3443) V3580))) (if (null? V3444) (let ((V3445 (kl:shen.lazyderef V3578 V3580))) (if (pair? V3445) (let ((V3446 (kl:shen.lazyderef (car V3445) V3580))) (if (eq? (quote vector) V3446) (let ((V3447 (kl:shen.lazyderef (cdr V3445) V3580))) (if (pair? V3447) (let ((A (car V3447))) (let ((V3448 (kl:shen.lazyderef (cdr V3447) V3580))) (if (null? V3448) (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote vector) (cons A (quote ()))) V3579 V3580 V3581)))) (if (kl:shen.pvar? V3448) (begin (kl:shen.bindv V3448 (quote ()) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote vector) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3448 V3580) Result))) #f)))) (if (kl:shen.pvar? V3447) (let ((A (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3447 (cons A (quote ())) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote vector) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3447 V3580) Result)))) #f))) (if (kl:shen.pvar? V3446) (begin (kl:shen.bindv V3446 (quote vector) V3580) (let ((Result (let ((V3449 (kl:shen.lazyderef (cdr V3445) V3580))) (if (pair? V3449) (let ((A (car V3449))) (let ((V3450 (kl:shen.lazyderef (cdr V3449) V3580))) (if (null? V3450) (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote vector) (cons A (quote ()))) V3579 V3580 V3581)))) (if (kl:shen.pvar? V3450) (begin (kl:shen.bindv V3450 (quote ()) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote vector) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3450 V3580) Result))) #f)))) (if (kl:shen.pvar? V3449) (let ((A (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3449 (cons A (quote ())) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote vector) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3449 V3580) Result)))) #f))))) (begin (kl:shen.unbindv V3446 V3580) Result))) #f))) (if (kl:shen.pvar? V3445) (let ((A (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3445 (cons (quote vector) (cons A (quote ()))) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X A V3579 V3580 (lambda () (kl:shen.th* Y (cons (quote vector) (cons A (quote ()))) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3445 V3580) Result)))) #f))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3451 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3451) (let ((V3452 (kl:shen.lazyderef (car V3451) V3580))) (if (eq? (quote _scheme_at_s) V3452) (let ((V3453 (kl:shen.lazyderef (cdr V3451) V3580))) (if (pair? V3453) (let ((X (car V3453))) (let ((V3454 (kl:shen.lazyderef (cdr V3453) V3580))) (if (pair? V3454) (let ((Y (car V3454))) (let ((V3455 (kl:shen.lazyderef (cdr V3454) V3580))) (if (null? V3455) (let ((V3456 (kl:shen.lazyderef V3578 V3580))) (if (eq? (quote string) V3456) (begin (kl:shen.incinfs) (kl:shen.th* X (quote string) V3579 V3580 (lambda () (kl:shen.th* Y (quote string) V3579 V3580 V3581)))) (if (kl:shen.pvar? V3456) (begin (kl:shen.bindv V3456 (quote string) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:shen.th* X (quote string) V3579 V3580 (lambda () (kl:shen.th* Y (quote string) V3579 V3580 V3581)))))) (begin (kl:shen.unbindv V3456 V3580) Result))) #f))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3457 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3457) (let ((V3458 (kl:shen.lazyderef (car V3457) V3580))) (if (eq? (quote lambda) V3458) (let ((V3459 (kl:shen.lazyderef (cdr V3457) V3580))) (if (pair? V3459) (let ((X (car V3459))) (let ((V3460 (kl:shen.lazyderef (cdr V3459) V3580))) (if (pair? V3460) (let ((Y (car V3460))) (let ((V3461 (kl:shen.lazyderef (cdr V3460) V3580))) (if (null? V3461) (let ((V3462 (kl:shen.lazyderef V3578 V3580))) (if (pair? V3462) (let ((A (car V3462))) (let ((V3463 (kl:shen.lazyderef (cdr V3462) V3580))) (if (pair? V3463) (let ((V3464 (kl:shen.lazyderef (car V3463) V3580))) (if (eq? (quote -->) V3464) (let ((V3465 (kl:shen.lazyderef (cdr V3463) V3580))) (if (pair? V3465) (let ((B (car V3465))) (let ((V3466 (kl:shen.lazyderef (cdr V3465) V3580))) (if (null? V3466) (let ((Z (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind Z (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Y V3580)) V3580 (lambda () (kl:shen.th* Z B (cons (cons X&& (cons (quote :) (cons A (quote ())))) V3579) V3580 V3581)))))))))) (if (kl:shen.pvar? V3466) (begin (kl:shen.bindv V3466 (quote ()) V3580) (let ((Result (let ((Z (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind Z (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Y V3580)) V3580 (lambda () (kl:shen.th* Z B (cons (cons X&& (cons (quote :) (cons A (quote ())))) V3579) V3580 V3581)))))))))))) (begin (kl:shen.unbindv V3466 V3580) Result))) #f)))) (if (kl:shen.pvar? V3465) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3465 (cons B (quote ())) V3580) (let ((Result (let ((Z (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind Z (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Y V3580)) V3580 (lambda () (kl:shen.th* Z B (cons (cons X&& (cons (quote :) (cons A (quote ())))) V3579) V3580 V3581)))))))))))) (begin (kl:shen.unbindv V3465 V3580) Result)))) #f))) (if (kl:shen.pvar? V3464) (begin (kl:shen.bindv V3464 (quote -->) V3580) (let ((Result (let ((V3467 (kl:shen.lazyderef (cdr V3463) V3580))) (if (pair? V3467) (let ((B (car V3467))) (let ((V3468 (kl:shen.lazyderef (cdr V3467) V3580))) (if (null? V3468) (let ((Z (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind Z (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Y V3580)) V3580 (lambda () (kl:shen.th* Z B (cons (cons X&& (cons (quote :) (cons A (quote ())))) V3579) V3580 V3581)))))))))) (if (kl:shen.pvar? V3468) (begin (kl:shen.bindv V3468 (quote ()) V3580) (let ((Result (let ((Z (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind Z (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Y V3580)) V3580 (lambda () (kl:shen.th* Z B (cons (cons X&& (cons (quote :) (cons A (quote ())))) V3579) V3580 V3581)))))))))))) (begin (kl:shen.unbindv V3468 V3580) Result))) #f)))) (if (kl:shen.pvar? V3467) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3467 (cons B (quote ())) V3580) (let ((Result (let ((Z (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind Z (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Y V3580)) V3580 (lambda () (kl:shen.th* Z B (cons (cons X&& (cons (quote :) (cons A (quote ())))) V3579) V3580 V3581)))))))))))) (begin (kl:shen.unbindv V3467 V3580) Result)))) #f))))) (begin (kl:shen.unbindv V3464 V3580) Result))) #f))) (if (kl:shen.pvar? V3463) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3463 (cons (quote -->) (cons B (quote ()))) V3580) (let ((Result (let ((Z (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind Z (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Y V3580)) V3580 (lambda () (kl:shen.th* Z B (cons (cons X&& (cons (quote :) (cons A (quote ())))) V3579) V3580 V3581)))))))))))) (begin (kl:shen.unbindv V3463 V3580) Result)))) #f)))) (if (kl:shen.pvar? V3462) (let ((A (kl:shen.newpv V3580))) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3462 (cons A (cons (quote -->) (cons B (quote ())))) V3580) (let ((Result (let ((Z (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind Z (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Y V3580)) V3580 (lambda () (kl:shen.th* Z B (cons (cons X&& (cons (quote :) (cons A (quote ())))) V3579) V3580 V3581)))))))))))) (begin (kl:shen.unbindv V3462 V3580) Result))))) #f))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3469 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3469) (let ((V3470 (kl:shen.lazyderef (car V3469) V3580))) (if (eq? (quote let) V3470) (let ((V3471 (kl:shen.lazyderef (cdr V3469) V3580))) (if (pair? V3471) (let ((X (car V3471))) (let ((V3472 (kl:shen.lazyderef (cdr V3471) V3580))) (if (pair? V3472) (let ((Y (car V3472))) (let ((V3473 (kl:shen.lazyderef (cdr V3472) V3580))) (if (pair? V3473) (let ((Z (car V3473))) (let ((V3474 (kl:shen.lazyderef (cdr V3473) V3580))) (if (null? V3474) (let ((W (kl:shen.newpv V3580))) (let ((X&& (kl:shen.newpv V3580))) (let ((B (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:shen.th* Y B V3579 V3580 (lambda () (kl:bind X&& (kl:shen.placeholder) V3580 (lambda () (kl:bind W (kl:shen.ebr (kl:shen.lazyderef X&& V3580) (kl:shen.lazyderef X V3580) (kl:shen.lazyderef Z V3580)) V3580 (lambda () (kl:shen.th* W V3578 (cons (cons X&& (cons (quote :) (cons B (quote ())))) V3579) V3580 V3581))))))))))) #f))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3475 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3475) (let ((V3476 (kl:shen.lazyderef (car V3475) V3580))) (if (eq? (quote open) V3476) (let ((V3477 (kl:shen.lazyderef (cdr V3475) V3580))) (if (pair? V3477) (let ((FileName (car V3477))) (let ((V3478 (kl:shen.lazyderef (cdr V3477) V3580))) (if (pair? V3478) (let ((Direction3408 (car V3478))) (let ((V3479 (kl:shen.lazyderef (cdr V3478) V3580))) (if (null? V3479) (let ((V3480 (kl:shen.lazyderef V3578 V3580))) (if (pair? V3480) (let ((V3481 (kl:shen.lazyderef (car V3480) V3580))) (if (eq? (quote stream) V3481) (let ((V3482 (kl:shen.lazyderef (cdr V3480) V3580))) (if (pair? V3482) (let ((Direction (car V3482))) (let ((V3483 (kl:shen.lazyderef (cdr V3482) V3580))) (if (null? V3483) (begin (kl:shen.incinfs) (kl:unify! Direction Direction3408 V3580 (lambda () (kl:cut Throwcontrol V3580 (lambda () (kl:fwhen (kl:element? (kl:shen.lazyderef Direction V3580) (cons (quote in) (cons (quote out) (quote ())))) V3580 (lambda () (kl:shen.th* FileName (quote string) V3579 V3580 V3581)))))))) (if (kl:shen.pvar? V3483) (begin (kl:shen.bindv V3483 (quote ()) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:unify! Direction Direction3408 V3580 (lambda () (kl:cut Throwcontrol V3580 (lambda () (kl:fwhen (kl:element? (kl:shen.lazyderef Direction V3580) (cons (quote in) (cons (quote out) (quote ())))) V3580 (lambda () (kl:shen.th* FileName (quote string) V3579 V3580 V3581)))))))))) (begin (kl:shen.unbindv V3483 V3580) Result))) #f)))) (if (kl:shen.pvar? V3482) (let ((Direction (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3482 (cons Direction (quote ())) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:unify! Direction Direction3408 V3580 (lambda () (kl:cut Throwcontrol V3580 (lambda () (kl:fwhen (kl:element? (kl:shen.lazyderef Direction V3580) (cons (quote in) (cons (quote out) (quote ())))) V3580 (lambda () (kl:shen.th* FileName (quote string) V3579 V3580 V3581)))))))))) (begin (kl:shen.unbindv V3482 V3580) Result)))) #f))) (if (kl:shen.pvar? V3481) (begin (kl:shen.bindv V3481 (quote stream) V3580) (let ((Result (let ((V3484 (kl:shen.lazyderef (cdr V3480) V3580))) (if (pair? V3484) (let ((Direction (car V3484))) (let ((V3485 (kl:shen.lazyderef (cdr V3484) V3580))) (if (null? V3485) (begin (kl:shen.incinfs) (kl:unify! Direction Direction3408 V3580 (lambda () (kl:cut Throwcontrol V3580 (lambda () (kl:fwhen (kl:element? (kl:shen.lazyderef Direction V3580) (cons (quote in) (cons (quote out) (quote ())))) V3580 (lambda () (kl:shen.th* FileName (quote string) V3579 V3580 V3581)))))))) (if (kl:shen.pvar? V3485) (begin (kl:shen.bindv V3485 (quote ()) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:unify! Direction Direction3408 V3580 (lambda () (kl:cut Throwcontrol V3580 (lambda () (kl:fwhen (kl:element? (kl:shen.lazyderef Direction V3580) (cons (quote in) (cons (quote out) (quote ())))) V3580 (lambda () (kl:shen.th* FileName (quote string) V3579 V3580 V3581)))))))))) (begin (kl:shen.unbindv V3485 V3580) Result))) #f)))) (if (kl:shen.pvar? V3484) (let ((Direction (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3484 (cons Direction (quote ())) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:unify! Direction Direction3408 V3580 (lambda () (kl:cut Throwcontrol V3580 (lambda () (kl:fwhen (kl:element? (kl:shen.lazyderef Direction V3580) (cons (quote in) (cons (quote out) (quote ())))) V3580 (lambda () (kl:shen.th* FileName (quote string) V3579 V3580 V3581)))))))))) (begin (kl:shen.unbindv V3484 V3580) Result)))) #f))))) (begin (kl:shen.unbindv V3481 V3580) Result))) #f))) (if (kl:shen.pvar? V3480) (let ((Direction (kl:shen.newpv V3580))) (begin (kl:shen.bindv V3480 (cons (quote stream) (cons Direction (quote ()))) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:unify! Direction Direction3408 V3580 (lambda () (kl:cut Throwcontrol V3580 (lambda () (kl:fwhen (kl:element? (kl:shen.lazyderef Direction V3580) (cons (quote in) (cons (quote out) (quote ())))) V3580 (lambda () (kl:shen.th* FileName (quote string) V3579 V3580 V3581)))))))))) (begin (kl:shen.unbindv V3480 V3580) Result)))) #f))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3486 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3486) (let ((V3487 (kl:shen.lazyderef (car V3486) V3580))) (if (eq? (quote type) V3487) (let ((V3488 (kl:shen.lazyderef (cdr V3486) V3580))) (if (pair? V3488) (let ((X (car V3488))) (let ((V3489 (kl:shen.lazyderef (cdr V3488) V3580))) (if (pair? V3489) (let ((A (car V3489))) (let ((V3490 (kl:shen.lazyderef (cdr V3489) V3580))) (if (null? V3490) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:unify A V3578 V3580 (lambda () (kl:shen.th* X A V3579 V3580 V3581)))))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3491 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3491) (let ((V3492 (kl:shen.lazyderef (car V3491) V3580))) (if (eq? (quote input+) V3492) (let ((V3493 (kl:shen.lazyderef (cdr V3491) V3580))) (if (pair? V3493) (let ((A (car V3493))) (let ((V3494 (kl:shen.lazyderef (cdr V3493) V3580))) (if (pair? V3494) (let ((Stream (car V3494))) (let ((V3495 (kl:shen.lazyderef (cdr V3494) V3580))) (if (null? V3495) (let ((C (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:bind C (kl:shen.demodulate (kl:shen.lazyderef A V3580)) V3580 (lambda () (kl:unify V3578 C V3580 (lambda () (kl:shen.th* Stream (cons (quote stream) (cons (quote in) (quote ()))) V3579 V3580 V3581))))))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3496 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3496) (let ((V3497 (kl:shen.lazyderef (car V3496) V3580))) (if (eq? (quote set) V3497) (let ((V3498 (kl:shen.lazyderef (cdr V3496) V3580))) (if (pair? V3498) (let ((Var (car V3498))) (let ((V3499 (kl:shen.lazyderef (cdr V3498) V3580))) (if (pair? V3499) (let ((Val (car V3499))) (let ((V3500 (kl:shen.lazyderef (cdr V3499) V3580))) (if (null? V3500) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:shen.th* Var (quote symbol) V3579 V3580 (lambda () (kl:cut Throwcontrol V3580 (lambda () (kl:shen.th* (cons (quote value) (cons Var (quote ()))) V3578 V3579 V3580 (lambda () (kl:shen.th* Val V3578 V3579 V3580 V3581)))))))))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((NewHyp (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:shen.t*-hyps V3579 NewHyp V3580 (lambda () (kl:shen.th* V3577 V3578 NewHyp V3580 V3581))))))) (if (kl:= Case #f) (let ((Case (let ((V3501 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3501) (let ((V3502 (kl:shen.lazyderef (car V3501) V3580))) (if (eq? (quote define) V3502) (let ((V3503 (kl:shen.lazyderef (cdr V3501) V3580))) (if (pair? V3503) (let ((F (car V3503))) (let ((X (cdr V3503))) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 (lambda () (kl:shen.t*-def (cons (quote define) (cons F X)) V3578 V3579 V3580 V3581)))))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3504 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3504) (let ((V3505 (kl:shen.lazyderef (car V3504) V3580))) (if (eq? (quote defmacro) V3505) (let ((V3506 (kl:shen.lazyderef V3578 V3580))) (if (eq? (quote unit) V3506) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 V3581)) (if (kl:shen.pvar? V3506) (begin (kl:shen.bindv V3506 (quote unit) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3580 V3581)))) (begin (kl:shen.unbindv V3506 V3580) Result))) #f))) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3507 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3507) (let ((V3508 (kl:shen.lazyderef (car V3507) V3580))) (if (eq? (quote shen.process-datatype) V3508) (let ((V3509 (kl:shen.lazyderef V3578 V3580))) (if (eq? (quote symbol) V3509) (begin (kl:shen.incinfs) (kl:thaw V3581)) (if (kl:shen.pvar? V3509) (begin (kl:shen.bindv V3509 (quote symbol) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:thaw V3581)))) (begin (kl:shen.unbindv V3509 V3580) Result))) #f))) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3510 (kl:shen.lazyderef V3577 V3580))) (if (pair? V3510) (let ((V3511 (kl:shen.lazyderef (car V3510) V3580))) (if (eq? (quote shen.synonyms-help) V3511) (let ((V3512 (kl:shen.lazyderef V3578 V3580))) (if (eq? (quote symbol) V3512) (begin (kl:shen.incinfs) (kl:thaw V3581)) (if (kl:shen.pvar? V3512) (begin (kl:shen.bindv V3512 (quote symbol) V3580) (let ((Result (begin (kl:shen.incinfs) (kl:thaw V3581)))) (begin (kl:shen.unbindv V3512 V3580) Result))) #f))) #f)) #f)))) (if (kl:= Case #f) (let ((Datatypes (kl:shen.newpv V3580))) (begin (kl:shen.incinfs) (kl:bind Datatypes (kl:value (quote shen.*datatypes*)) V3580 (lambda () (kl:shen.udefs* (cons V3577 (cons (quote :) (cons V3578 (quote ())))) 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))))) (quote shen.th*))
(begin (register-function-arity (quote shen.t*-hyps) 4) (define (kl:shen.t*-hyps V3586 V3587 V3588 V3589) (let ((Case (let ((V3323 (kl:shen.lazyderef V3586 V3588))) (if (pair? V3323) (let ((V3324 (kl:shen.lazyderef (car V3323) V3588))) (if (pair? V3324) (let ((V3325 (kl:shen.lazyderef (car V3324) V3588))) (if (pair? V3325) (let ((V3326 (kl:shen.lazyderef (car V3325) V3588))) (if (eq? (quote cons) V3326) (let ((V3327 (kl:shen.lazyderef (cdr V3325) V3588))) (if (pair? V3327) (let ((X (car V3327))) (let ((V3328 (kl:shen.lazyderef (cdr V3327) V3588))) (if (pair? V3328) (let ((Y (car V3328))) (let ((V3329 (kl:shen.lazyderef (cdr V3328) V3588))) (if (null? V3329) (let ((V3330 (kl:shen.lazyderef (cdr V3324) V3588))) (if (pair? V3330) (let ((V3331 (kl:shen.lazyderef (car V3330) V3588))) (if (eq? (quote :) V3331) (let ((V3332 (kl:shen.lazyderef (cdr V3330) V3588))) (if (pair? V3332) (let ((V3333 (kl:shen.lazyderef (car V3332) V3588))) (if (pair? V3333) (let ((V3334 (kl:shen.lazyderef (car V3333) V3588))) (if (eq? (quote list) V3334) (let ((V3335 (kl:shen.lazyderef (cdr V3333) V3588))) (if (pair? V3335) (let ((A (car V3335))) (let ((V3336 (kl:shen.lazyderef (cdr V3335) V3588))) (if (null? V3336) (let ((V3337 (kl:shen.lazyderef (cdr V3332) V3588))) (if (null? V3337) (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3337) (begin (kl:shen.bindv V3337 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3337 V3588) Result))) #f))) (if (kl:shen.pvar? V3336) (begin (kl:shen.bindv V3336 (quote ()) V3588) (let ((Result (let ((V3338 (kl:shen.lazyderef (cdr V3332) V3588))) (if (null? V3338) (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3338) (begin (kl:shen.bindv V3338 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3338 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3336 V3588) Result))) #f)))) (if (kl:shen.pvar? V3335) (let ((A (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3335 (cons A (quote ())) V3588) (let ((Result (let ((V3339 (kl:shen.lazyderef (cdr V3332) V3588))) (if (null? V3339) (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3339) (begin (kl:shen.bindv V3339 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3339 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3335 V3588) Result)))) #f))) (if (kl:shen.pvar? V3334) (begin (kl:shen.bindv V3334 (quote list) V3588) (let ((Result (let ((V3340 (kl:shen.lazyderef (cdr V3333) V3588))) (if (pair? V3340) (let ((A (car V3340))) (let ((V3341 (kl:shen.lazyderef (cdr V3340) V3588))) (if (null? V3341) (let ((V3342 (kl:shen.lazyderef (cdr V3332) V3588))) (if (null? V3342) (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3342) (begin (kl:shen.bindv V3342 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3342 V3588) Result))) #f))) (if (kl:shen.pvar? V3341) (begin (kl:shen.bindv V3341 (quote ()) V3588) (let ((Result (let ((V3343 (kl:shen.lazyderef (cdr V3332) V3588))) (if (null? V3343) (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3343) (begin (kl:shen.bindv V3343 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3343 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3341 V3588) Result))) #f)))) (if (kl:shen.pvar? V3340) (let ((A (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3340 (cons A (quote ())) V3588) (let ((Result (let ((V3344 (kl:shen.lazyderef (cdr V3332) V3588))) (if (null? V3344) (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3344) (begin (kl:shen.bindv V3344 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3344 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3340 V3588) Result)))) #f))))) (begin (kl:shen.unbindv V3334 V3588) Result))) #f))) (if (kl:shen.pvar? V3333) (let ((A (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3333 (cons (quote list) (cons A (quote ()))) V3588) (let ((Result (let ((V3345 (kl:shen.lazyderef (cdr V3332) V3588))) (if (null? V3345) (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3345) (begin (kl:shen.bindv V3345 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3323))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote list) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3345 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3333 V3588) Result)))) #f))) #f)) #f)) #f)) #f))) #f))) #f)) #f)) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3346 (kl:shen.lazyderef V3586 V3588))) (if (pair? V3346) (let ((V3347 (kl:shen.lazyderef (car V3346) V3588))) (if (pair? V3347) (let ((V3348 (kl:shen.lazyderef (car V3347) V3588))) (if (pair? V3348) (let ((V3349 (kl:shen.lazyderef (car V3348) V3588))) (if (eq? (quote _scheme_at_p) V3349) (let ((V3350 (kl:shen.lazyderef (cdr V3348) V3588))) (if (pair? V3350) (let ((X (car V3350))) (let ((V3351 (kl:shen.lazyderef (cdr V3350) V3588))) (if (pair? V3351) (let ((Y (car V3351))) (let ((V3352 (kl:shen.lazyderef (cdr V3351) V3588))) (if (null? V3352) (let ((V3353 (kl:shen.lazyderef (cdr V3347) V3588))) (if (pair? V3353) (let ((V3354 (kl:shen.lazyderef (car V3353) V3588))) (if (eq? (quote :) V3354) (let ((V3355 (kl:shen.lazyderef (cdr V3353) V3588))) (if (pair? V3355) (let ((V3356 (kl:shen.lazyderef (car V3355) V3588))) (if (pair? V3356) (let ((A (car V3356))) (let ((V3357 (kl:shen.lazyderef (cdr V3356) V3588))) (if (pair? V3357) (let ((V3358 (kl:shen.lazyderef (car V3357) V3588))) (if (eq? (quote *) V3358) (let ((V3359 (kl:shen.lazyderef (cdr V3357) V3588))) (if (pair? V3359) (let ((B (car V3359))) (let ((V3360 (kl:shen.lazyderef (cdr V3359) V3588))) (if (null? V3360) (let ((V3361 (kl:shen.lazyderef (cdr V3355) V3588))) (if (null? V3361) (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3361) (begin (kl:shen.bindv V3361 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3361 V3588) Result))) #f))) (if (kl:shen.pvar? V3360) (begin (kl:shen.bindv V3360 (quote ()) V3588) (let ((Result (let ((V3362 (kl:shen.lazyderef (cdr V3355) V3588))) (if (null? V3362) (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3362) (begin (kl:shen.bindv V3362 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3362 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3360 V3588) Result))) #f)))) (if (kl:shen.pvar? V3359) (let ((B (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3359 (cons B (quote ())) V3588) (let ((Result (let ((V3363 (kl:shen.lazyderef (cdr V3355) V3588))) (if (null? V3363) (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3363) (begin (kl:shen.bindv V3363 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3363 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3359 V3588) Result)))) #f))) (if (kl:shen.pvar? V3358) (begin (kl:shen.bindv V3358 (quote *) V3588) (let ((Result (let ((V3364 (kl:shen.lazyderef (cdr V3357) V3588))) (if (pair? V3364) (let ((B (car V3364))) (let ((V3365 (kl:shen.lazyderef (cdr V3364) V3588))) (if (null? V3365) (let ((V3366 (kl:shen.lazyderef (cdr V3355) V3588))) (if (null? V3366) (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3366) (begin (kl:shen.bindv V3366 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3366 V3588) Result))) #f))) (if (kl:shen.pvar? V3365) (begin (kl:shen.bindv V3365 (quote ()) V3588) (let ((Result (let ((V3367 (kl:shen.lazyderef (cdr V3355) V3588))) (if (null? V3367) (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3367) (begin (kl:shen.bindv V3367 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3367 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3365 V3588) Result))) #f)))) (if (kl:shen.pvar? V3364) (let ((B (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3364 (cons B (quote ())) V3588) (let ((Result (let ((V3368 (kl:shen.lazyderef (cdr V3355) V3588))) (if (null? V3368) (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3368) (begin (kl:shen.bindv V3368 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3368 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3364 V3588) Result)))) #f))))) (begin (kl:shen.unbindv V3358 V3588) Result))) #f))) (if (kl:shen.pvar? V3357) (let ((B (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3357 (cons (quote *) (cons B (quote ()))) V3588) (let ((Result (let ((V3369 (kl:shen.lazyderef (cdr V3355) V3588))) (if (null? V3369) (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3369) (begin (kl:shen.bindv V3369 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3369 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3357 V3588) Result)))) #f)))) (if (kl:shen.pvar? V3356) (let ((A (kl:shen.newpv V3588))) (let ((B (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3356 (cons A (cons (quote *) (cons B (quote ())))) V3588) (let ((Result (let ((V3370 (kl:shen.lazyderef (cdr V3355) V3588))) (if (null? V3370) (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3370) (begin (kl:shen.bindv V3370 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3346))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (kl:shen.lazyderef B V3588) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3370 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3356 V3588) Result))))) #f))) #f)) #f)) #f)) #f))) #f))) #f)) #f)) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3371 (kl:shen.lazyderef V3586 V3588))) (if (pair? V3371) (let ((V3372 (kl:shen.lazyderef (car V3371) V3588))) (if (pair? V3372) (let ((V3373 (kl:shen.lazyderef (car V3372) V3588))) (if (pair? V3373) (let ((V3374 (kl:shen.lazyderef (car V3373) V3588))) (if (eq? (quote _scheme_at_v) V3374) (let ((V3375 (kl:shen.lazyderef (cdr V3373) V3588))) (if (pair? V3375) (let ((X (car V3375))) (let ((V3376 (kl:shen.lazyderef (cdr V3375) V3588))) (if (pair? V3376) (let ((Y (car V3376))) (let ((V3377 (kl:shen.lazyderef (cdr V3376) V3588))) (if (null? V3377) (let ((V3378 (kl:shen.lazyderef (cdr V3372) V3588))) (if (pair? V3378) (let ((V3379 (kl:shen.lazyderef (car V3378) V3588))) (if (eq? (quote :) V3379) (let ((V3380 (kl:shen.lazyderef (cdr V3378) V3588))) (if (pair? V3380) (let ((V3381 (kl:shen.lazyderef (car V3380) V3588))) (if (pair? V3381) (let ((V3382 (kl:shen.lazyderef (car V3381) V3588))) (if (eq? (quote vector) V3382) (let ((V3383 (kl:shen.lazyderef (cdr V3381) V3588))) (if (pair? V3383) (let ((A (car V3383))) (let ((V3384 (kl:shen.lazyderef (cdr V3383) V3588))) (if (null? V3384) (let ((V3385 (kl:shen.lazyderef (cdr V3380) V3588))) (if (null? V3385) (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3385) (begin (kl:shen.bindv V3385 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3385 V3588) Result))) #f))) (if (kl:shen.pvar? V3384) (begin (kl:shen.bindv V3384 (quote ()) V3588) (let ((Result (let ((V3386 (kl:shen.lazyderef (cdr V3380) V3588))) (if (null? V3386) (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3386) (begin (kl:shen.bindv V3386 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3386 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3384 V3588) Result))) #f)))) (if (kl:shen.pvar? V3383) (let ((A (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3383 (cons A (quote ())) V3588) (let ((Result (let ((V3387 (kl:shen.lazyderef (cdr V3380) V3588))) (if (null? V3387) (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3387) (begin (kl:shen.bindv V3387 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3387 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3383 V3588) Result)))) #f))) (if (kl:shen.pvar? V3382) (begin (kl:shen.bindv V3382 (quote vector) V3588) (let ((Result (let ((V3388 (kl:shen.lazyderef (cdr V3381) V3588))) (if (pair? V3388) (let ((A (car V3388))) (let ((V3389 (kl:shen.lazyderef (cdr V3388) V3588))) (if (null? V3389) (let ((V3390 (kl:shen.lazyderef (cdr V3380) V3588))) (if (null? V3390) (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3390) (begin (kl:shen.bindv V3390 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3390 V3588) Result))) #f))) (if (kl:shen.pvar? V3389) (begin (kl:shen.bindv V3389 (quote ()) V3588) (let ((Result (let ((V3391 (kl:shen.lazyderef (cdr V3380) V3588))) (if (null? V3391) (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3391) (begin (kl:shen.bindv V3391 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3391 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3389 V3588) Result))) #f)))) (if (kl:shen.pvar? V3388) (let ((A (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3388 (cons A (quote ())) V3588) (let ((Result (let ((V3392 (kl:shen.lazyderef (cdr V3380) V3588))) (if (null? V3392) (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3392) (begin (kl:shen.bindv V3392 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3392 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3388 V3588) Result)))) #f))))) (begin (kl:shen.unbindv V3382 V3588) Result))) #f))) (if (kl:shen.pvar? V3381) (let ((A (kl:shen.newpv V3588))) (begin (kl:shen.bindv V3381 (cons (quote vector) (cons A (quote ()))) V3588) (let ((Result (let ((V3393 (kl:shen.lazyderef (cdr V3380) V3588))) (if (null? V3393) (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3393) (begin (kl:shen.bindv V3393 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3371))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (kl:shen.lazyderef A V3588) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (cons (quote vector) (cons (kl:shen.lazyderef A V3588) (quote ()))) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3393 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3381 V3588) Result)))) #f))) #f)) #f)) #f)) #f))) #f))) #f)) #f)) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3394 (kl:shen.lazyderef V3586 V3588))) (if (pair? V3394) (let ((V3395 (kl:shen.lazyderef (car V3394) V3588))) (if (pair? V3395) (let ((V3396 (kl:shen.lazyderef (car V3395) V3588))) (if (pair? V3396) (let ((V3397 (kl:shen.lazyderef (car V3396) V3588))) (if (eq? (quote _scheme_at_s) V3397) (let ((V3398 (kl:shen.lazyderef (cdr V3396) V3588))) (if (pair? V3398) (let ((X (car V3398))) (let ((V3399 (kl:shen.lazyderef (cdr V3398) V3588))) (if (pair? V3399) (let ((Y (car V3399))) (let ((V3400 (kl:shen.lazyderef (cdr V3399) V3588))) (if (null? V3400) (let ((V3401 (kl:shen.lazyderef (cdr V3395) V3588))) (if (pair? V3401) (let ((V3402 (kl:shen.lazyderef (car V3401) V3588))) (if (eq? (quote :) V3402) (let ((V3403 (kl:shen.lazyderef (cdr V3401) V3588))) (if (pair? V3403) (let ((V3404 (kl:shen.lazyderef (car V3403) V3588))) (if (eq? (quote string) V3404) (let ((V3405 (kl:shen.lazyderef (cdr V3403) V3588))) (if (null? V3405) (let ((Hyp (cdr V3394))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (quote string) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (quote string) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3405) (begin (kl:shen.bindv V3405 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3394))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (quote string) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (quote string) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3405 V3588) Result))) #f))) (if (kl:shen.pvar? V3404) (begin (kl:shen.bindv V3404 (quote string) V3588) (let ((Result (let ((V3406 (kl:shen.lazyderef (cdr V3403) V3588))) (if (null? V3406) (let ((Hyp (cdr V3394))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (quote string) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (quote string) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))) (if (kl:shen.pvar? V3406) (begin (kl:shen.bindv V3406 (quote ()) V3588) (let ((Result (let ((Hyp (cdr V3394))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (cons (kl:shen.lazyderef X V3588) (cons (quote :) (cons (quote string) (quote ())))) (cons (cons (kl:shen.lazyderef Y V3588) (cons (quote :) (cons (quote string) (quote ())))) (kl:shen.lazyderef Hyp V3588))) V3588 V3589))))) (begin (kl:shen.unbindv V3406 V3588) Result))) #f))))) (begin (kl:shen.unbindv V3404 V3588) Result))) #f))) #f)) #f)) #f)) #f))) #f))) #f)) #f)) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((V3407 (kl:shen.lazyderef V3586 V3588))) (if (pair? V3407) (let ((X (car V3407))) (let ((Hyp (cdr V3407))) (let ((NewHyps (kl:shen.newpv V3588))) (begin (kl:shen.incinfs) (kl:bind V3587 (cons (kl:shen.lazyderef X V3588) (kl:shen.lazyderef NewHyps V3588)) V3588 (lambda () (kl:shen.t*-hyps Hyp NewHyps V3588 V3589))))))) #f)) Case)) Case)) Case)) Case))) (quote shen.t*-hyps))
(begin (register-function-arity (quote shen.show) 4) (define (kl:shen.show V3606 V3607 V3608 V3609) (cond ((assert-boolean (kl:value (quote shen.*spy*))) (begin (kl:shen.line) (begin (kl:shen.show-p (kl:shen.deref V3606 V3608)) (begin (kl:nl 1) (begin (kl:nl 1) (begin (kl:shen.show-assumptions (kl:shen.deref V3607 V3608) 1) (begin (kl:shen.prhush "\n> " (kl:stoutput)) (begin (kl:shen.pause-for-user) (kl:thaw V3609))))))))) (#t (kl:thaw V3609)))) (quote shen.show))
(begin (register-function-arity (quote shen.line) 0) (define (kl:shen.line) (let ((Infs (kl:inferences))) (kl:shen.prhush (string-append "____________________________________________________________ " (kl:shen.app Infs (string-append " inference" (kl:shen.app (if (kl:= 1 Infs) "" "s") " \n?- " (quote shen.a))) (quote shen.a))) (kl:stoutput)))) (quote shen.line))
(begin (register-function-arity (quote shen.show-p) 1) (define (kl:shen.show-p V3611) (cond ((and (pair? V3611) (and (pair? (cdr V3611)) (and (eq? (quote :) (car (cdr V3611))) (and (pair? (cdr (cdr V3611))) (null? (cdr (cdr (cdr V3611)))))))) (kl:shen.prhush (kl:shen.app (car V3611) (string-append " : " (kl:shen.app (car (cdr (cdr V3611))) "" (quote shen.r))) (quote shen.r)) (kl:stoutput))) (#t (kl:shen.prhush (kl:shen.app V3611 "" (quote shen.r)) (kl:stoutput))))) (quote shen.show-p))
(begin (register-function-arity (quote shen.show-assumptions) 2) (define (kl:shen.show-assumptions V3616 V3617) (cond ((null? V3616) (quote shen.skip)) ((pair? V3616) (begin (kl:shen.prhush (kl:shen.app V3617 ". " (quote shen.a)) (kl:stoutput)) (begin (kl:shen.show-p (car V3616)) (begin (kl:nl 1) (kl:shen.show-assumptions (cdr V3616) (+ V3617 1)))))) (#t (kl:shen.f_error (quote shen.show-assumptions))))) (quote shen.show-assumptions))
(begin (register-function-arity (quote shen.pause-for-user) 0) (define (kl:shen.pause-for-user) (let ((Byte (kl:read-byte (kl:stinput)))) (if (kl:= Byte 94) (simple-error "input aborted\n") (kl:nl 1)))) (quote shen.pause-for-user))
(begin (register-function-arity (quote shen.typedf?) 1) (define (kl:shen.typedf? V3619) (pair? (kl:assoc V3619 (kl:value (quote shen.*signedfuncs*))))) (quote shen.typedf?))
(begin (register-function-arity (quote shen.sigf) 1) (define (kl:shen.sigf V3621) (kl:concat (quote shen.type-signature-of-) V3621)) (quote shen.sigf))
(begin (register-function-arity (quote shen.placeholder) 0) (define (kl:shen.placeholder) (kl:gensym (quote &&))) (quote shen.placeholder))
(begin (register-function-arity (quote shen.base) 4) (define (kl:shen.base V3626 V3627 V3628 V3629) (let ((Case (let ((V3310 (kl:shen.lazyderef V3627 V3628))) (if (eq? (quote number) V3310) (begin (kl:shen.incinfs) (kl:fwhen (number? (kl:shen.lazyderef V3626 V3628)) V3628 V3629)) (if (kl:shen.pvar? V3310) (begin (kl:shen.bindv V3310 (quote number) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:fwhen (number? (kl:shen.lazyderef V3626 V3628)) V3628 V3629)))) (begin (kl:shen.unbindv V3310 V3628) Result))) #f))))) (if (kl:= Case #f) (let ((Case (let ((V3311 (kl:shen.lazyderef V3627 V3628))) (if (eq? (quote boolean) V3311) (begin (kl:shen.incinfs) (kl:fwhen (kl:boolean? (kl:shen.lazyderef V3626 V3628)) V3628 V3629)) (if (kl:shen.pvar? V3311) (begin (kl:shen.bindv V3311 (quote boolean) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:fwhen (kl:boolean? (kl:shen.lazyderef V3626 V3628)) V3628 V3629)))) (begin (kl:shen.unbindv V3311 V3628) Result))) #f))))) (if (kl:= Case #f) (let ((Case (let ((V3312 (kl:shen.lazyderef V3627 V3628))) (if (eq? (quote string) V3312) (begin (kl:shen.incinfs) (kl:fwhen (string? (kl:shen.lazyderef V3626 V3628)) V3628 V3629)) (if (kl:shen.pvar? V3312) (begin (kl:shen.bindv V3312 (quote string) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:fwhen (string? (kl:shen.lazyderef V3626 V3628)) V3628 V3629)))) (begin (kl:shen.unbindv V3312 V3628) Result))) #f))))) (if (kl:= Case #f) (let ((Case (let ((V3313 (kl:shen.lazyderef V3627 V3628))) (if (eq? (quote symbol) V3313) (begin (kl:shen.incinfs) (kl:fwhen (symbol? (kl:shen.lazyderef V3626 V3628)) V3628 (lambda () (kl:fwhen (kl:not (kl:shen.ue? (kl:shen.lazyderef V3626 V3628))) V3628 V3629)))) (if (kl:shen.pvar? V3313) (begin (kl:shen.bindv V3313 (quote symbol) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:fwhen (symbol? (kl:shen.lazyderef V3626 V3628)) V3628 (lambda () (kl:fwhen (kl:not (kl:shen.ue? (kl:shen.lazyderef V3626 V3628))) V3628 V3629)))))) (begin (kl:shen.unbindv V3313 V3628) Result))) #f))))) (if (kl:= Case #f) (let ((V3314 (kl:shen.lazyderef V3626 V3628))) (if (null? V3314) (let ((V3315 (kl:shen.lazyderef V3627 V3628))) (if (pair? V3315) (let ((V3316 (kl:shen.lazyderef (car V3315) V3628))) (if (eq? (quote list) V3316) (let ((V3317 (kl:shen.lazyderef (cdr V3315) V3628))) (if (pair? V3317) (let ((A (car V3317))) (let ((V3318 (kl:shen.lazyderef (cdr V3317) V3628))) (if (null? V3318) (begin (kl:shen.incinfs) (kl:thaw V3629)) (if (kl:shen.pvar? V3318) (begin (kl:shen.bindv V3318 (quote ()) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:thaw V3629)))) (begin (kl:shen.unbindv V3318 V3628) Result))) #f)))) (if (kl:shen.pvar? V3317) (let ((A (kl:shen.newpv V3628))) (begin (kl:shen.bindv V3317 (cons A (quote ())) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:thaw V3629)))) (begin (kl:shen.unbindv V3317 V3628) Result)))) #f))) (if (kl:shen.pvar? V3316) (begin (kl:shen.bindv V3316 (quote list) V3628) (let ((Result (let ((V3319 (kl:shen.lazyderef (cdr V3315) V3628))) (if (pair? V3319) (let ((A (car V3319))) (let ((V3320 (kl:shen.lazyderef (cdr V3319) V3628))) (if (null? V3320) (begin (kl:shen.incinfs) (kl:thaw V3629)) (if (kl:shen.pvar? V3320) (begin (kl:shen.bindv V3320 (quote ()) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:thaw V3629)))) (begin (kl:shen.unbindv V3320 V3628) Result))) #f)))) (if (kl:shen.pvar? V3319) (let ((A (kl:shen.newpv V3628))) (begin (kl:shen.bindv V3319 (cons A (quote ())) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:thaw V3629)))) (begin (kl:shen.unbindv V3319 V3628) Result)))) #f))))) (begin (kl:shen.unbindv V3316 V3628) Result))) #f))) (if (kl:shen.pvar? V3315) (let ((A (kl:shen.newpv V3628))) (begin (kl:shen.bindv V3315 (cons (quote list) (cons A (quote ()))) V3628) (let ((Result (begin (kl:shen.incinfs) (kl:thaw V3629)))) (begin (kl:shen.unbindv V3315 V3628) Result)))) #f))) #f)) Case)) Case)) Case)) Case))) (quote shen.base))
(begin (register-function-arity (quote shen.by_hypothesis) 5) (define (kl:shen.by_hypothesis V3635 V3636 V3637 V3638 V3639) (let ((Case (let ((V3301 (kl:shen.lazyderef V3637 V3638))) (if (pair? V3301) (let ((V3302 (kl:shen.lazyderef (car V3301) V3638))) (if (pair? V3302) (let ((Y (car V3302))) (let ((V3303 (kl:shen.lazyderef (cdr V3302) V3638))) (if (pair? V3303) (let ((V3304 (kl:shen.lazyderef (car V3303) V3638))) (if (eq? (quote :) V3304) (let ((V3305 (kl:shen.lazyderef (cdr V3303) V3638))) (if (pair? V3305) (let ((B (car V3305))) (let ((V3306 (kl:shen.lazyderef (cdr V3305) V3638))) (if (null? V3306) (begin (kl:shen.incinfs) (kl:identical V3635 Y V3638 (lambda () (kl:unify! V3636 B V3638 V3639)))) #f))) #f)) #f)) #f))) #f)) #f)))) (if (kl:= Case #f) (let ((V3307 (kl:shen.lazyderef V3637 V3638))) (if (pair? V3307) (let ((Hyp (cdr V3307))) (begin (kl:shen.incinfs) (kl:shen.by_hypothesis V3635 V3636 Hyp V3638 V3639))) #f)) Case))) (quote shen.by_hypothesis))
(begin (register-function-arity (quote shen.t*-def) 5) (define (kl:shen.t*-def V3645 V3646 V3647 V3648 V3649) (let ((V3295 (kl:shen.lazyderef V3645 V3648))) (if (pair? V3295) (let ((V3296 (kl:shen.lazyderef (car V3295) V3648))) (if (eq? (quote define) V3296) (let ((V3297 (kl:shen.lazyderef (cdr V3295) V3648))) (if (pair? V3297) (let ((F (car V3297))) (let ((X (cdr V3297))) (let ((Y (kl:shen.newpv V3648))) (let ((E (kl:shen.newpv V3648))) (begin (kl:shen.incinfs) (kl:shen.t*-defh (kl:compile (lambda (Y) (kl:shen.<sig+rules> Y)) X (lambda (E) (if (pair? E) (simple-error (string-append "parse error here: " (kl:shen.app E "\n" (quote shen.s)))) (simple-error "parse error\n")))) F V3646 V3647 V3648 V3649)))))) #f)) #f)) #f))) (quote shen.t*-def))
(begin (register-function-arity (quote shen.t*-defh) 6) (define (kl:shen.t*-defh V3656 V3657 V3658 V3659 V3660 V3661) (let ((V3291 (kl:shen.lazyderef V3656 V3660))) (if (pair? V3291) (let ((Sig (car V3291))) (let ((Rules (cdr V3291))) (begin (kl:shen.incinfs) (kl:shen.t*-defhh Sig (kl:shen.ue-sig Sig) V3657 V3658 V3659 Rules V3660 V3661)))) #f))) (quote shen.t*-defh))
(begin (register-function-arity (quote shen.t*-defhh) 8) (define (kl:shen.t*-defhh V3670 V3671 V3672 V3673 V3674 V3675 V3676 V3677) (begin (kl:shen.incinfs) (kl:shen.t*-rules V3675 V3671 1 V3672 (cons (cons V3672 (cons (quote :) (cons V3671 (quote ())))) V3674) V3676 (lambda () (kl:shen.memo V3672 V3670 V3673 V3676 V3677))))) (quote shen.t*-defhh))
(begin (register-function-arity (quote shen.memo) 5) (define (kl:shen.memo V3683 V3684 V3685 V3686 V3687) (let ((Jnk (kl:shen.newpv V3686))) (begin (kl:shen.incinfs) (kl:unify! V3685 V3684 V3686 (lambda () (kl:bind Jnk (kl:declare (kl:shen.lazyderef V3683 V3686) (kl:shen.lazyderef V3685 V3686)) V3686 V3687)))))) (quote shen.memo))
(begin (register-function-arity (quote shen.<sig+rules>) 1) (define (kl:shen.<sig+rules> V3689) (let ((Parse_shen.<signature> (kl:shen.<signature> V3689))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<signature>)) (let ((Parse_shen.<non-ll-rules> (kl:shen.<non-ll-rules> Parse_shen.<signature>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<non-ll-rules>)) (kl:shen.pair (car Parse_shen.<non-ll-rules>) (cons (kl:shen.hdtl Parse_shen.<signature>) (kl:shen.hdtl Parse_shen.<non-ll-rules>))) (quote shen.fail!))) (quote shen.fail!)))) (quote shen.<sig+rules>))
(begin (register-function-arity (quote shen.<non-ll-rules>) 1) (define (kl:shen.<non-ll-rules> V3691) (let ((YaccParse (let ((Parse_shen.<rule> (kl:shen.<rule> V3691))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<rule>)) (let ((Parse_shen.<non-ll-rules> (kl:shen.<non-ll-rules> Parse_shen.<rule>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<non-ll-rules>)) (kl:shen.pair (car Parse_shen.<non-ll-rules>) (cons (kl:shen.hdtl Parse_shen.<rule>) (kl:shen.hdtl Parse_shen.<non-ll-rules>))) (quote shen.fail!))) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_shen.<rule> (kl:shen.<rule> V3691))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<rule>)) (kl:shen.pair (car Parse_shen.<rule>) (cons (kl:shen.hdtl Parse_shen.<rule>) (quote ()))) (quote shen.fail!))) YaccParse))) (quote shen.<non-ll-rules>))
(begin (register-function-arity (quote shen.ue) 1) (define (kl:shen.ue V3693) (cond ((and (pair? V3693) (and (pair? (cdr V3693)) (and (null? (cdr (cdr V3693))) (eq? (car V3693) (quote protect))))) V3693) ((pair? V3693) (kl:map (lambda (Z) (kl:shen.ue Z)) V3693)) ((kl:variable? V3693) (kl:concat (quote &&) V3693)) (#t V3693))) (quote shen.ue))
(begin (register-function-arity (quote shen.ue-sig) 1) (define (kl:shen.ue-sig V3695) (cond ((pair? V3695) (kl:map (lambda (Z) (kl:shen.ue-sig Z)) V3695)) ((kl:variable? V3695) (kl:concat (quote &&&) V3695)) (#t V3695))) (quote shen.ue-sig))
(begin (register-function-arity (quote shen.ues) 1) (define (kl:shen.ues V3701) (cond ((assert-boolean (kl:shen.ue? V3701)) (cons V3701 (quote ()))) ((pair? V3701) (kl:union (kl:shen.ues (car V3701)) (kl:shen.ues (cdr V3701)))) (#t (quote ())))) (quote shen.ues))
(begin (register-function-arity (quote shen.ue?) 1) (define (kl:shen.ue? V3703) (and (assert-boolean (symbol? V3703)) (assert-boolean (kl:shen.ue-h? (kl:str V3703))))) (quote shen.ue?))
(begin (register-function-arity (quote shen.ue-h?) 1) (define (kl:shen.ue-h? V3711) (cond ((and (assert-boolean (kl:shen.+string? V3711)) (and (equal? "&" (make-string 1 (string-ref V3711 0))) (and (assert-boolean (kl:shen.+string? (kl:tlstr V3711))) (equal? "&" (make-string 1 (string-ref (kl:tlstr V3711) 0)))))) #t) (#t #f))) (quote shen.ue-h?))
(begin (register-function-arity (quote shen.t*-rules) 7) (define (kl:shen.t*-rules V3719 V3720 V3721 V3722 V3723 V3724 V3725) (let ((Throwcontrol (kl:shen.catchpoint))) (kl:shen.cutpoint Throwcontrol (let ((Case (let ((V3275 (kl:shen.lazyderef V3719 V3724))) (if (null? V3275) (begin (kl:shen.incinfs) (kl:thaw V3725)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3276 (kl:shen.lazyderef V3719 V3724))) (if (pair? V3276) (let ((Rule (car V3276))) (let ((Rules (cdr V3276))) (begin (kl:shen.incinfs) (kl:shen.t*-rule (kl:shen.ue Rule) V3720 V3723 V3724 (lambda () (kl:cut Throwcontrol V3724 (lambda () (kl:shen.t*-rules Rules V3720 (+ V3721 1) V3722 V3723 V3724 V3725)))))))) #f)))) (if (kl:= Case #f) (let ((Err (kl:shen.newpv V3724))) (begin (kl:shen.incinfs) (kl:bind Err (simple-error (string-append "type error in rule " (kl:shen.app (kl:shen.lazyderef V3721 V3724) (string-append " of " (kl:shen.app (kl:shen.lazyderef V3722 V3724) "" (quote shen.a))) (quote shen.a)))) V3724 V3725))) Case)) Case))))) (quote shen.t*-rules))
(begin (register-function-arity (quote shen.t*-rule) 5) (define (kl:shen.t*-rule V3731 V3732 V3733 V3734 V3735) (let ((Throwcontrol (kl:shen.catchpoint))) (kl:shen.cutpoint Throwcontrol (let ((V3267 (kl:shen.lazyderef V3731 V3734))) (if (pair? V3267) (let ((Patterns (car V3267))) (let ((V3268 (kl:shen.lazyderef (cdr V3267) V3734))) (if (pair? V3268) (let ((Action (car V3268))) (let ((V3269 (kl:shen.lazyderef (cdr V3268) V3734))) (if (null? V3269) (let ((NewHyps (kl:shen.newpv V3734))) (begin (kl:shen.incinfs) (kl:shen.newhyps (kl:shen.placeholders Patterns) V3733 NewHyps V3734 (lambda () (kl:shen.t*-patterns Patterns V3732 NewHyps V3734 (lambda () (kl:cut Throwcontrol V3734 (lambda () (kl:shen.t*-action (kl:shen.curry (kl:shen.ue Action)) (kl:shen.result-type Patterns V3732) (kl:shen.patthyps Patterns V3732 V3733) V3734 V3735))))))))) #f))) #f))) #f))))) (quote shen.t*-rule))
(begin (register-function-arity (quote shen.placeholders) 1) (define (kl:shen.placeholders V3741) (cond ((assert-boolean (kl:shen.ue? V3741)) (cons V3741 (quote ()))) ((pair? V3741) (kl:union (kl:shen.placeholders (car V3741)) (kl:shen.placeholders (cdr V3741)))) (#t (quote ())))) (quote shen.placeholders))
(begin (register-function-arity (quote shen.newhyps) 5) (define (kl:shen.newhyps V3747 V3748 V3749 V3750 V3751) (let ((Case (let ((V3254 (kl:shen.lazyderef V3747 V3750))) (if (null? V3254) (begin (kl:shen.incinfs) (kl:unify! V3749 V3748 V3750 V3751)) #f)))) (if (kl:= Case #f) (let ((V3255 (kl:shen.lazyderef V3747 V3750))) (if (pair? V3255) (let ((V3250 (car V3255))) (let ((Vs (cdr V3255))) (let ((V3256 (kl:shen.lazyderef V3749 V3750))) (if (pair? V3256) (let ((V3257 (kl:shen.lazyderef (car V3256) V3750))) (if (pair? V3257) (let ((V (car V3257))) (let ((V3258 (kl:shen.lazyderef (cdr V3257) V3750))) (if (pair? V3258) (let ((V3259 (kl:shen.lazyderef (car V3258) V3750))) (if (eq? (quote :) V3259) (let ((V3260 (kl:shen.lazyderef (cdr V3258) V3750))) (if (pair? V3260) (let ((A (car V3260))) (let ((V3261 (kl:shen.lazyderef (cdr V3260) V3750))) (if (null? V3261) (let ((NewHyp (cdr V3256))) (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (if (kl:shen.pvar? V3261) (begin (kl:shen.bindv V3261 (quote ()) V3750) (let ((Result (let ((NewHyp (cdr V3256))) (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751))))))) (begin (kl:shen.unbindv V3261 V3750) Result))) #f)))) (if (kl:shen.pvar? V3260) (let ((A (kl:shen.newpv V3750))) (begin (kl:shen.bindv V3260 (cons A (quote ())) V3750) (let ((Result (let ((NewHyp (cdr V3256))) (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751))))))) (begin (kl:shen.unbindv V3260 V3750) Result)))) #f))) (if (kl:shen.pvar? V3259) (begin (kl:shen.bindv V3259 (quote :) V3750) (let ((Result (let ((V3262 (kl:shen.lazyderef (cdr V3258) V3750))) (if (pair? V3262) (let ((A (car V3262))) (let ((V3263 (kl:shen.lazyderef (cdr V3262) V3750))) (if (null? V3263) (let ((NewHyp (cdr V3256))) (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751))))) (if (kl:shen.pvar? V3263) (begin (kl:shen.bindv V3263 (quote ()) V3750) (let ((Result (let ((NewHyp (cdr V3256))) (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751))))))) (begin (kl:shen.unbindv V3263 V3750) Result))) #f)))) (if (kl:shen.pvar? V3262) (let ((A (kl:shen.newpv V3750))) (begin (kl:shen.bindv V3262 (cons A (quote ())) V3750) (let ((Result (let ((NewHyp (cdr V3256))) (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751))))))) (begin (kl:shen.unbindv V3262 V3750) Result)))) #f))))) (begin (kl:shen.unbindv V3259 V3750) Result))) #f))) (if (kl:shen.pvar? V3258) (let ((A (kl:shen.newpv V3750))) (begin (kl:shen.bindv V3258 (cons (quote :) (cons A (quote ()))) V3750) (let ((Result (let ((NewHyp (cdr V3256))) (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751))))))) (begin (kl:shen.unbindv V3258 V3750) Result)))) #f)))) (if (kl:shen.pvar? V3257) (let ((V (kl:shen.newpv V3750))) (let ((A (kl:shen.newpv V3750))) (begin (kl:shen.bindv V3257 (cons V (cons (quote :) (cons A (quote ())))) V3750) (let ((Result (let ((NewHyp (cdr V3256))) (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751))))))) (begin (kl:shen.unbindv V3257 V3750) Result))))) #f))) (if (kl:shen.pvar? V3256) (let ((V (kl:shen.newpv V3750))) (let ((A (kl:shen.newpv V3750))) (let ((NewHyp (kl:shen.newpv V3750))) (begin (kl:shen.bindv V3256 (cons (cons V (cons (quote :) (cons A (quote ())))) NewHyp) V3750) (let ((Result (begin (kl:shen.incinfs) (kl:unify! V V3250 V3750 (lambda () (kl:shen.newhyps Vs V3748 NewHyp V3750 V3751)))))) (begin (kl:shen.unbindv V3256 V3750) Result)))))) #f))))) #f)) Case))) (quote shen.newhyps))
(begin (register-function-arity (quote shen.patthyps) 3) (define (kl:shen.patthyps V3757 V3758 V3759) (cond ((null? V3757) V3759) ((and (pair? V3757) (and (pair? V3758) (and (pair? (cdr V3758)) (and (eq? (quote -->) (car (cdr V3758))) (and (pair? (cdr (cdr V3758))) (null? (cdr (cdr (cdr V3758))))))))) (kl:adjoin (cons (car V3757) (cons (quote :) (cons (car V3758) (quote ())))) (kl:shen.patthyps (cdr V3757) (car (cdr (cdr V3758))) V3759))) (#t (kl:shen.f_error (quote shen.patthyps))))) (quote shen.patthyps))
(begin (register-function-arity (quote shen.result-type) 2) (define (kl:shen.result-type V3766 V3767) (cond ((and (null? V3766) (and (pair? V3767) (and (eq? (quote -->) (car V3767)) (and (pair? (cdr V3767)) (null? (cdr (cdr V3767))))))) (car (cdr V3767))) ((null? V3766) V3767) ((and (pair? V3766) (and (pair? V3767) (and (pair? (cdr V3767)) (and (eq? (quote -->) (car (cdr V3767))) (and (pair? (cdr (cdr V3767))) (null? (cdr (cdr (cdr V3767))))))))) (kl:shen.result-type (cdr V3766) (car (cdr (cdr V3767))))) (#t (kl:shen.f_error (quote shen.result-type))))) (quote shen.result-type))
(begin (register-function-arity (quote shen.t*-patterns) 5) (define (kl:shen.t*-patterns V3773 V3774 V3775 V3776 V3777) (let ((Case (let ((V3242 (kl:shen.lazyderef V3773 V3776))) (if (null? V3242) (begin (kl:shen.incinfs) (kl:thaw V3777)) #f)))) (if (kl:= Case #f) (let ((V3243 (kl:shen.lazyderef V3773 V3776))) (if (pair? V3243) (let ((Pattern (car V3243))) (let ((Patterns (cdr V3243))) (let ((V3244 (kl:shen.lazyderef V3774 V3776))) (if (pair? V3244) (let ((A (car V3244))) (let ((V3245 (kl:shen.lazyderef (cdr V3244) V3776))) (if (pair? V3245) (let ((V3246 (kl:shen.lazyderef (car V3245) V3776))) (if (eq? (quote -->) V3246) (let ((V3247 (kl:shen.lazyderef (cdr V3245) V3776))) (if (pair? V3247) (let ((B (car V3247))) (let ((V3248 (kl:shen.lazyderef (cdr V3247) V3776))) (if (null? V3248) (begin (kl:shen.incinfs) (kl:shen.t* (cons Pattern (cons (quote :) (cons A (quote ())))) V3775 V3776 (lambda () (kl:shen.t*-patterns Patterns B V3775 V3776 V3777)))) #f))) #f)) #f)) #f))) #f)))) #f)) Case))) (quote shen.t*-patterns))
(begin (register-function-arity (quote shen.t*-action) 5) (define (kl:shen.t*-action V3783 V3784 V3785 V3786 V3787) (let ((Throwcontrol (kl:shen.catchpoint))) (kl:shen.cutpoint Throwcontrol (let ((Case (let ((V3219 (kl:shen.lazyderef V3783 V3786))) (if (pair? V3219) (let ((V3220 (kl:shen.lazyderef (car V3219) V3786))) (if (eq? (quote where) V3220) (let ((V3221 (kl:shen.lazyderef (cdr V3219) V3786))) (if (pair? V3221) (let ((P (car V3221))) (let ((V3222 (kl:shen.lazyderef (cdr V3221) V3786))) (if (pair? V3222) (let ((Action (car V3222))) (let ((V3223 (kl:shen.lazyderef (cdr V3222) V3786))) (if (null? V3223) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3786 (lambda () (kl:shen.t* (cons P (cons (quote :) (cons (quote boolean) (quote ())))) V3785 V3786 (lambda () (kl:cut Throwcontrol V3786 (lambda () (kl:shen.t*-action Action V3784 (cons (cons P (cons (quote :) (cons (quote verified) (quote ())))) V3785) V3786 V3787)))))))) #f))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3224 (kl:shen.lazyderef V3783 V3786))) (if (pair? V3224) (let ((V3225 (kl:shen.lazyderef (car V3224) V3786))) (if (eq? (quote shen.choicepoint!) V3225) (let ((V3226 (kl:shen.lazyderef (cdr V3224) V3786))) (if (pair? V3226) (let ((V3227 (kl:shen.lazyderef (car V3226) V3786))) (if (pair? V3227) (let ((V3228 (kl:shen.lazyderef (car V3227) V3786))) (if (pair? V3228) (let ((V3229 (kl:shen.lazyderef (car V3228) V3786))) (if (eq? (quote fail-if) V3229) (let ((V3230 (kl:shen.lazyderef (cdr V3228) V3786))) (if (pair? V3230) (let ((F (car V3230))) (let ((V3231 (kl:shen.lazyderef (cdr V3230) V3786))) (if (null? V3231) (let ((V3232 (kl:shen.lazyderef (cdr V3227) V3786))) (if (pair? V3232) (let ((Action (car V3232))) (let ((V3233 (kl:shen.lazyderef (cdr V3232) V3786))) (if (null? V3233) (let ((V3234 (kl:shen.lazyderef (cdr V3226) V3786))) (if (null? V3234) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3786 (lambda () (kl:shen.t*-action (cons (quote where) (cons (cons (quote not) (cons (cons F (cons Action (quote ()))) (quote ()))) (cons Action (quote ())))) V3784 V3785 V3786 V3787)))) #f)) #f))) #f)) #f))) #f)) #f)) #f)) #f)) #f)) #f)) #f)))) (if (kl:= Case #f) (let ((Case (let ((V3235 (kl:shen.lazyderef V3783 V3786))) (if (pair? V3235) (let ((V3236 (kl:shen.lazyderef (car V3235) V3786))) (if (eq? (quote shen.choicepoint!) V3236) (let ((V3237 (kl:shen.lazyderef (cdr V3235) V3786))) (if (pair? V3237) (let ((Action (car V3237))) (let ((V3238 (kl:shen.lazyderef (cdr V3237) V3786))) (if (null? V3238) (begin (kl:shen.incinfs) (kl:cut Throwcontrol V3786 (lambda () (kl:shen.t*-action (cons (quote where) (cons (cons (quote not) (cons (cons (cons (quote =) (cons Action (quote ()))) (cons (cons (quote fail) (quote ())) (quote ()))) (quote ()))) (cons Action (quote ())))) V3784 V3785 V3786 V3787)))) #f))) #f)) #f)) #f)))) (if (kl:= Case #f) (begin (kl:shen.incinfs) (kl:shen.t* (cons V3783 (cons (quote :) (cons V3784 (quote ())))) V3785 V3786 V3787)) Case)) Case)) Case))))) (quote shen.t*-action))
(begin (register-function-arity (quote findall) 5) (define (kl:findall V3793 V3794 V3795 V3796 V3797) (let ((B (kl:shen.newpv V3796))) (let ((A (kl:shen.newpv V3796))) (begin (kl:shen.incinfs) (kl:bind A (kl:gensym (quote shen.a)) V3796 (lambda () (kl:bind B (kl:set (kl:shen.lazyderef A V3796) (quote ())) V3796 (lambda () (kl:shen.findallhelp V3793 V3794 V3795 A V3796 V3797))))))))) (quote findall))
(begin (register-function-arity (quote shen.findallhelp) 6) (define (kl:shen.findallhelp V3804 V3805 V3806 V3807 V3808 V3809) (let ((Case (begin (kl:shen.incinfs) (kl:call V3805 V3808 (lambda () (kl:shen.remember V3807 V3804 V3808 (lambda () (kl:fwhen #f V3808 V3809)))))))) (if (kl:= Case #f) (begin (kl:shen.incinfs) (kl:bind V3806 (kl:value (kl:shen.lazyderef V3807 V3808)) V3808 V3809)) Case))) (quote shen.findallhelp))
(begin (register-function-arity (quote shen.remember) 4) (define (kl:shen.remember V3814 V3815 V3816 V3817) (let ((B (kl:shen.newpv V3816))) (begin (kl:shen.incinfs) (kl:bind B (kl:set (kl:shen.deref V3814 V3816) (cons (kl:shen.deref V3815 V3816) (kl:value (kl:shen.deref V3814 V3816)))) V3816 V3817)))) (quote shen.remember))