shen/release/k_lambda/t-star.kl in shen-ruby-0.10.0 vs shen/release/k_lambda/t-star.kl in shen-ruby-0.11.0
- old
+ new
@@ -1,139 +1,139 @@
-"**********************************************************************************
-* The License *
-* *
-* The user is free to produce commercial applications with the software, to *
-* distribute these applications in source or binary form, and to charge monies *
-* for them as he sees fit and in concordance with the laws of the land subject *
-* to the following license. *
-* *
-* 1. The license applies to all the software and all derived software and *
-* must appear on such. *
-* *
-* 2. It is illegal to distribute the software without this license attached *
-* to it and use of the software implies agreement with the license as such. *
-* It is illegal for anyone who is not the copyright holder to tamper with *
-* or change the license. *
-* *
-* 3. Neither the names of Lambda Associates or the copyright holder may be used *
-* to endorse or promote products built using the software without specific *
-* prior written permission from the copyright holder. *
-* *
-* 4. That possession of this license does not confer on the copyright holder *
-* any special contractual obligation towards the user. That in no event *
-* shall the copyright holder 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, *
-* interruption), however caused and on any theory of liability, whether in *
-* contract, strict liability or tort (including negligence) arising in any *
-* way out of the use of the software, even if advised of the possibility of *
-* such damage. *
-* *
-* 5. It is permitted for the user to change the software, for the purpose of *
-* improving performance, correcting an error, or porting to a new platform, *
-* and distribute the derived version of Shen provided the resulting program *
-* conforms in all respects to the Shen standard and is issued under that *
-* title. The user must make it clear with his distribution that he/she is *
-* the author of the changes and what these changes are and why. *
-* *
-* 6. Derived versions of this software in whatever form are subject to the same *
-* restrictions. In particular it is not permitted to make derived copies of *
-* this software which do not conform to the Shen standard or appear under a *
-* different title. *
-* *
-* It is permitted to distribute versions of Shen which incorporate libraries, *
-* graphics or other facilities which are not part of the Shen standard. *
-* *
-* For an explication of this license see www.shenlanguage.org/license.htm which *
-* explains this license in full. *
-* *
-*****************************************************************************************
-"(defun shen.typecheck (V2790 V2791) (let Curry (shen.curry V2790) (let ProcessN (shen.start-new-prolog-process) (let Type (shen.insert-prolog-variables (shen.demodulate (shen.curry-type V2791)) ProcessN) (let Continuation (freeze (return Type ProcessN shen.void)) (shen.t* (cons Curry (cons : (cons Type ()))) () ProcessN Continuation))))))
-
-(defun shen.curry (V2792) (cond ((and (cons? V2792) (shen.special? (hd V2792))) (cons (hd V2792) (map (lambda X2786 (shen.curry X2786)) (tl V2792)))) ((and (cons? V2792) (and (cons? (tl V2792)) (shen.extraspecial? (hd V2792)))) V2792) ((and (cons? V2792) (and (= type (hd V2792)) (and (cons? (tl V2792)) (and (cons? (tl (tl V2792))) (= () (tl (tl (tl V2792)))))))) (cons type (cons (shen.curry (hd (tl V2792))) (tl (tl V2792))))) ((and (cons? V2792) (and (cons? (tl V2792)) (cons? (tl (tl V2792))))) (shen.curry (cons (cons (hd V2792) (cons (hd (tl V2792)) ())) (tl (tl V2792))))) ((and (cons? V2792) (and (cons? (tl V2792)) (= () (tl (tl V2792))))) (cons (shen.curry (hd V2792)) (cons (shen.curry (hd (tl V2792))) ()))) (true V2792)))
-
-(defun shen.special? (V2793) (element? V2793 (value shen.*special*)))
-
-(defun shen.extraspecial? (V2794) (element? V2794 (value shen.*extraspecial*)))
-
-(defun shen.t* (V2795 V2796 V2797 V2798) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let Error (shen.newpv V2797) (do (shen.incinfs) (fwhen (shen.maxinfexceeded?) V2797 (freeze (bind Error (shen.errormaxinfs) V2797 V2798))))) (if (= Case false) (let Case (let V2780 (shen.lazyderef V2795 V2797) (if (= fail V2780) (do (shen.incinfs) (cut Throwcontrol V2797 (freeze (shen.prolog-failure V2797 V2798)))) false)) (if (= Case false) (let Case (let V2781 (shen.lazyderef V2795 V2797) (if (cons? V2781) (let X (hd V2781) (let V2782 (shen.lazyderef (tl V2781) V2797) (if (cons? V2782) (let V2783 (shen.lazyderef (hd V2782) V2797) (if (= : V2783) (let V2784 (shen.lazyderef (tl V2782) V2797) (if (cons? V2784) (let A (hd V2784) (let V2785 (shen.lazyderef (tl V2784) V2797) (if (= () V2785) (do (shen.incinfs) (fwhen (shen.type-theory-enabled?) V2797 (freeze (cut Throwcontrol V2797 (freeze (shen.th* X A V2796 V2797 V2798)))))) false))) false)) false)) false))) false)) (if (= Case false) (let Datatypes (shen.newpv V2797) (do (shen.incinfs) (shen.show V2795 V2796 V2797 (freeze (bind Datatypes (value shen.*datatypes*) V2797 (freeze (shen.udefs* V2795 V2796 Datatypes V2797 V2798))))))) Case)) Case)) Case)))))
-
-(defun shen.type-theory-enabled? () (value shen.*shen-type-theory-enabled?*))
-
-(defun enable-type-theory (V2803) (cond ((= + V2803) (set shen.*shen-type-theory-enabled?* true)) ((= - V2803) (set shen.*shen-type-theory-enabled?* false)) (true (simple-error "enable-type-theory expects a + or a -
-"))))
-
-(defun shen.prolog-failure (V2812 V2813) false)
-
-(defun shen.maxinfexceeded? () (> (inferences) (value shen.*maxinferences*)))
-
-(defun shen.errormaxinfs () (simple-error "maximum inferences exceeded~%"))
-
-(defun shen.udefs* (V2814 V2815 V2816 V2817 V2818) (let Case (let V2776 (shen.lazyderef V2816 V2817) (if (cons? V2776) (let D (hd V2776) (do (shen.incinfs) (call (cons D (cons V2814 (cons V2815 ()))) V2817 V2818))) false)) (if (= Case false) (let V2777 (shen.lazyderef V2816 V2817) (if (cons? V2777) (let Ds (tl V2777) (do (shen.incinfs) (shen.udefs* V2814 V2815 Ds V2817 V2818))) false)) Case)))
-
-(defun shen.th* (V2819 V2820 V2821 V2822 V2823) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (do (shen.incinfs) (shen.show (cons V2819 (cons : (cons V2820 ()))) V2821 V2822 (freeze (fwhen false V2822 V2823)))) (if (= Case false) (let Case (let F (shen.newpv V2822) (do (shen.incinfs) (fwhen (shen.typedf? (shen.lazyderef V2819 V2822)) V2822 (freeze (bind F (shen.sigf (shen.lazyderef V2819 V2822)) V2822 (freeze (call (cons F (cons V2820 ())) V2822 V2823))))))) (if (= Case false) (let Case (do (shen.incinfs) (shen.base V2819 V2820 V2822 V2823)) (if (= Case false) (let Case (do (shen.incinfs) (shen.by_hypothesis V2819 V2820 V2821 V2822 V2823)) (if (= Case false) (let Case (let V2668 (shen.lazyderef V2819 V2822) (if (cons? V2668) (let F (hd V2668) (let V2669 (shen.lazyderef (tl V2668) V2822) (if (= () V2669) (do (shen.incinfs) (shen.th* F (cons --> (cons V2820 ())) V2821 V2822 V2823)) false))) false)) (if (= Case false) (let Case (let V2670 (shen.lazyderef V2819 V2822) (if (cons? V2670) (let F (hd V2670) (let V2671 (shen.lazyderef (tl V2670) V2822) (if (cons? V2671) (let X (hd V2671) (let V2672 (shen.lazyderef (tl V2671) V2822) (if (= () V2672) (let B (shen.newpv V2822) (do (shen.incinfs) (shen.th* F (cons B (cons --> (cons V2820 ()))) V2821 V2822 (freeze (shen.th* X B V2821 V2822 V2823))))) false))) false))) false)) (if (= Case false) (let Case (let V2673 (shen.lazyderef V2819 V2822) (if (cons? V2673) (let V2674 (shen.lazyderef (hd V2673) V2822) (if (= cons V2674) (let V2675 (shen.lazyderef (tl V2673) V2822) (if (cons? V2675) (let X (hd V2675) (let V2676 (shen.lazyderef (tl V2675) V2822) (if (cons? V2676) (let Y (hd V2676) (let V2677 (shen.lazyderef (tl V2676) V2822) (if (= () V2677) (let V2678 (shen.lazyderef V2820 V2822) (if (cons? V2678) (let V2679 (shen.lazyderef (hd V2678) V2822) (if (= list V2679) (let V2680 (shen.lazyderef (tl V2678) V2822) (if (cons? V2680) (let A (hd V2680) (let V2681 (shen.lazyderef (tl V2680) V2822) (if (= () V2681) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2681) (do (shen.bindv V2681 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2681 V2822) Result))) false)))) (if (shen.pvar? V2680) (let A (shen.newpv V2822) (do (shen.bindv V2680 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2680 V2822) Result)))) false))) (if (shen.pvar? V2679) (do (shen.bindv V2679 list V2822) (let Result (let V2682 (shen.lazyderef (tl V2678) V2822) (if (cons? V2682) (let A (hd V2682) (let V2683 (shen.lazyderef (tl V2682) V2822) (if (= () V2683) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2683) (do (shen.bindv V2683 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2683 V2822) Result))) false)))) (if (shen.pvar? V2682) (let A (shen.newpv V2822) (do (shen.bindv V2682 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2682 V2822) Result)))) false))) (do (shen.unbindv V2679 V2822) Result))) false))) (if (shen.pvar? V2678) (let A (shen.newpv V2822) (do (shen.bindv V2678 (cons list (cons A ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2678 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2684 (shen.lazyderef V2819 V2822) (if (cons? V2684) (let V2685 (shen.lazyderef (hd V2684) V2822) (if (= @p V2685) (let V2686 (shen.lazyderef (tl V2684) V2822) (if (cons? V2686) (let X (hd V2686) (let V2687 (shen.lazyderef (tl V2686) V2822) (if (cons? V2687) (let Y (hd V2687) (let V2688 (shen.lazyderef (tl V2687) V2822) (if (= () V2688) (let V2689 (shen.lazyderef V2820 V2822) (if (cons? V2689) (let A (hd V2689) (let V2690 (shen.lazyderef (tl V2689) V2822) (if (cons? V2690) (let V2691 (shen.lazyderef (hd V2690) V2822) (if (= * V2691) (let V2692 (shen.lazyderef (tl V2690) V2822) (if (cons? V2692) (let B (hd V2692) (let V2693 (shen.lazyderef (tl V2692) V2822) (if (= () V2693) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (if (shen.pvar? V2693) (do (shen.bindv V2693 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2693 V2822) Result))) false)))) (if (shen.pvar? V2692) (let B (shen.newpv V2822) (do (shen.bindv V2692 (cons B ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2692 V2822) Result)))) false))) (if (shen.pvar? V2691) (do (shen.bindv V2691 * V2822) (let Result (let V2694 (shen.lazyderef (tl V2690) V2822) (if (cons? V2694) (let B (hd V2694) (let V2695 (shen.lazyderef (tl V2694) V2822) (if (= () V2695) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (if (shen.pvar? V2695) (do (shen.bindv V2695 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2695 V2822) Result))) false)))) (if (shen.pvar? V2694) (let B (shen.newpv V2822) (do (shen.bindv V2694 (cons B ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2694 V2822) Result)))) false))) (do (shen.unbindv V2691 V2822) Result))) false))) (if (shen.pvar? V2690) (let B (shen.newpv V2822) (do (shen.bindv V2690 (cons * (cons B ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2690 V2822) Result)))) false)))) (if (shen.pvar? V2689) (let A (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.bindv V2689 (cons A (cons * (cons B ()))) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2689 V2822) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2696 (shen.lazyderef V2819 V2822) (if (cons? V2696) (let V2697 (shen.lazyderef (hd V2696) V2822) (if (= @v V2697) (let V2698 (shen.lazyderef (tl V2696) V2822) (if (cons? V2698) (let X (hd V2698) (let V2699 (shen.lazyderef (tl V2698) V2822) (if (cons? V2699) (let Y (hd V2699) (let V2700 (shen.lazyderef (tl V2699) V2822) (if (= () V2700) (let V2701 (shen.lazyderef V2820 V2822) (if (cons? V2701) (let V2702 (shen.lazyderef (hd V2701) V2822) (if (= vector V2702) (let V2703 (shen.lazyderef (tl V2701) V2822) (if (cons? V2703) (let A (hd V2703) (let V2704 (shen.lazyderef (tl V2703) V2822) (if (= () V2704) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2704) (do (shen.bindv V2704 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2704 V2822) Result))) false)))) (if (shen.pvar? V2703) (let A (shen.newpv V2822) (do (shen.bindv V2703 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2703 V2822) Result)))) false))) (if (shen.pvar? V2702) (do (shen.bindv V2702 vector V2822) (let Result (let V2705 (shen.lazyderef (tl V2701) V2822) (if (cons? V2705) (let A (hd V2705) (let V2706 (shen.lazyderef (tl V2705) V2822) (if (= () V2706) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2706) (do (shen.bindv V2706 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2706 V2822) Result))) false)))) (if (shen.pvar? V2705) (let A (shen.newpv V2822) (do (shen.bindv V2705 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2705 V2822) Result)))) false))) (do (shen.unbindv V2702 V2822) Result))) false))) (if (shen.pvar? V2701) (let A (shen.newpv V2822) (do (shen.bindv V2701 (cons vector (cons A ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2701 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2707 (shen.lazyderef V2819 V2822) (if (cons? V2707) (let V2708 (shen.lazyderef (hd V2707) V2822) (if (= @s V2708) (let V2709 (shen.lazyderef (tl V2707) V2822) (if (cons? V2709) (let X (hd V2709) (let V2710 (shen.lazyderef (tl V2709) V2822) (if (cons? V2710) (let Y (hd V2710) (let V2711 (shen.lazyderef (tl V2710) V2822) (if (= () V2711) (let V2712 (shen.lazyderef V2820 V2822) (if (= string V2712) (do (shen.incinfs) (shen.th* X string V2821 V2822 (freeze (shen.th* Y string V2821 V2822 V2823)))) (if (shen.pvar? V2712) (do (shen.bindv V2712 string V2822) (let Result (do (shen.incinfs) (shen.th* X string V2821 V2822 (freeze (shen.th* Y string V2821 V2822 V2823)))) (do (shen.unbindv V2712 V2822) Result))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2713 (shen.lazyderef V2819 V2822) (if (cons? V2713) (let V2714 (shen.lazyderef (hd V2713) V2822) (if (= lambda V2714) (let V2715 (shen.lazyderef (tl V2713) V2822) (if (cons? V2715) (let X (hd V2715) (let V2716 (shen.lazyderef (tl V2715) V2822) (if (cons? V2716) (let Y (hd V2716) (let V2717 (shen.lazyderef (tl V2716) V2822) (if (= () V2717) (let V2718 (shen.lazyderef V2820 V2822) (if (cons? V2718) (let A (hd V2718) (let V2719 (shen.lazyderef (tl V2718) V2822) (if (cons? V2719) (let V2720 (shen.lazyderef (hd V2719) V2822) (if (= --> V2720) (let V2721 (shen.lazyderef (tl V2719) V2822) (if (cons? V2721) (let B (hd V2721) (let V2722 (shen.lazyderef (tl V2721) V2822) (if (= () V2722) (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (if (shen.pvar? V2722) (do (shen.bindv V2722 () V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2722 V2822) Result))) false)))) (if (shen.pvar? V2721) (let B (shen.newpv V2822) (do (shen.bindv V2721 (cons B ()) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2721 V2822) Result)))) false))) (if (shen.pvar? V2720) (do (shen.bindv V2720 --> V2822) (let Result (let V2723 (shen.lazyderef (tl V2719) V2822) (if (cons? V2723) (let B (hd V2723) (let V2724 (shen.lazyderef (tl V2723) V2822) (if (= () V2724) (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (if (shen.pvar? V2724) (do (shen.bindv V2724 () V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2724 V2822) Result))) false)))) (if (shen.pvar? V2723) (let B (shen.newpv V2822) (do (shen.bindv V2723 (cons B ()) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2723 V2822) Result)))) false))) (do (shen.unbindv V2720 V2822) Result))) false))) (if (shen.pvar? V2719) (let B (shen.newpv V2822) (do (shen.bindv V2719 (cons --> (cons B ())) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2719 V2822) Result)))) false)))) (if (shen.pvar? V2718) (let A (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.bindv V2718 (cons A (cons --> (cons B ()))) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2718 V2822) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2725 (shen.lazyderef V2819 V2822) (if (cons? V2725) (let V2726 (shen.lazyderef (hd V2725) V2822) (if (= let V2726) (let V2727 (shen.lazyderef (tl V2725) V2822) (if (cons? V2727) (let X (hd V2727) (let V2728 (shen.lazyderef (tl V2727) V2822) (if (cons? V2728) (let Y (hd V2728) (let V2729 (shen.lazyderef (tl V2728) V2822) (if (cons? V2729) (let Z (hd V2729) (let V2730 (shen.lazyderef (tl V2729) V2822) (if (= () V2730) (let W (shen.newpv V2822) (let X&& (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.incinfs) (shen.th* Y B V2821 V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind W (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Z V2822)) V2822 (freeze (shen.th* W V2820 (cons (cons X&& (cons : (cons B ()))) V2821) V2822 V2823))))))))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2731 (shen.lazyderef V2819 V2822) (if (cons? V2731) (let V2732 (shen.lazyderef (hd V2731) V2822) (if (= open V2732) (let V2733 (shen.lazyderef (tl V2731) V2822) (if (cons? V2733) (let FileName (hd V2733) (let V2734 (shen.lazyderef (tl V2733) V2822) (if (cons? V2734) (let Direction2664 (hd V2734) (let V2735 (shen.lazyderef (tl V2734) V2822) (if (= () V2735) (let V2736 (shen.lazyderef V2820 V2822) (if (cons? V2736) (let V2737 (shen.lazyderef (hd V2736) V2822) (if (= stream V2737) (let V2738 (shen.lazyderef (tl V2736) V2822) (if (cons? V2738) (let Direction (hd V2738) (let V2739 (shen.lazyderef (tl V2738) V2822) (if (= () V2739) (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (if (shen.pvar? V2739) (do (shen.bindv V2739 () V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2739 V2822) Result))) false)))) (if (shen.pvar? V2738) (let Direction (shen.newpv V2822) (do (shen.bindv V2738 (cons Direction ()) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2738 V2822) Result)))) false))) (if (shen.pvar? V2737) (do (shen.bindv V2737 stream V2822) (let Result (let V2740 (shen.lazyderef (tl V2736) V2822) (if (cons? V2740) (let Direction (hd V2740) (let V2741 (shen.lazyderef (tl V2740) V2822) (if (= () V2741) (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (if (shen.pvar? V2741) (do (shen.bindv V2741 () V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2741 V2822) Result))) false)))) (if (shen.pvar? V2740) (let Direction (shen.newpv V2822) (do (shen.bindv V2740 (cons Direction ()) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2740 V2822) Result)))) false))) (do (shen.unbindv V2737 V2822) Result))) false))) (if (shen.pvar? V2736) (let Direction (shen.newpv V2822) (do (shen.bindv V2736 (cons stream (cons Direction ())) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2736 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2742 (shen.lazyderef V2819 V2822) (if (cons? V2742) (let V2743 (shen.lazyderef (hd V2742) V2822) (if (= type V2743) (let V2744 (shen.lazyderef (tl V2742) V2822) (if (cons? V2744) (let X (hd V2744) (let V2745 (shen.lazyderef (tl V2744) V2822) (if (cons? V2745) (let A (hd V2745) (let V2746 (shen.lazyderef (tl V2745) V2822) (if (= () V2746) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (unify A V2820 V2822 (freeze (shen.th* X A V2821 V2822 V2823)))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2747 (shen.lazyderef V2819 V2822) (if (cons? V2747) (let V2748 (shen.lazyderef (hd V2747) V2822) (if (= input+ V2748) (let V2749 (shen.lazyderef (tl V2747) V2822) (if (cons? V2749) (let A (hd V2749) (let V2750 (shen.lazyderef (tl V2749) V2822) (if (cons? V2750) (let Stream (hd V2750) (let V2751 (shen.lazyderef (tl V2750) V2822) (if (= () V2751) (let C (shen.newpv V2822) (do (shen.incinfs) (bind C (shen.demodulate (shen.lazyderef A V2822)) V2822 (freeze (unify V2820 C V2822 (freeze (shen.th* Stream (cons stream (cons in ())) V2821 V2822 V2823))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2752 (shen.lazyderef V2819 V2822) (if (cons? V2752) (let V2753 (shen.lazyderef (hd V2752) V2822) (if (= set V2753) (let V2754 (shen.lazyderef (tl V2752) V2822) (if (cons? V2754) (let Var (hd V2754) (let V2755 (shen.lazyderef (tl V2754) V2822) (if (cons? V2755) (let Val (hd V2755) (let V2756 (shen.lazyderef (tl V2755) V2822) (if (= () V2756) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (shen.th* Var symbol V2821 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* (cons value (cons Var ())) V2820 V2821 V2822 (freeze (shen.th* Val V2820 V2821 V2822 V2823)))))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2757 (shen.lazyderef V2819 V2822) (if (cons? V2757) (let V2758 (shen.lazyderef (hd V2757) V2822) (if (= fail V2758) (let V2759 (shen.lazyderef (tl V2757) V2822) (if (= () V2759) (let V2760 (shen.lazyderef V2820 V2822) (if (= symbol V2760) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2760) (do (shen.bindv V2760 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2760 V2822) Result))) false))) false)) false)) false)) (if (= Case false) (let Case (let NewHyp (shen.newpv V2822) (do (shen.incinfs) (shen.t*-hyps V2821 NewHyp V2822 (freeze (shen.th* V2819 V2820 NewHyp V2822 V2823))))) (if (= Case false) (let Case (let V2761 (shen.lazyderef V2819 V2822) (if (cons? V2761) (let V2762 (shen.lazyderef (hd V2761) V2822) (if (= define V2762) (let V2763 (shen.lazyderef (tl V2761) V2822) (if (cons? V2763) (let F (hd V2763) (let X (tl V2763) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (shen.t*-def (cons define (cons F X)) V2820 V2821 V2822 V2823)))))) false)) false)) false)) (if (= Case false) (let Case (let V2764 (shen.lazyderef V2819 V2822) (if (cons? V2764) (let V2765 (shen.lazyderef (hd V2764) V2822) (if (= defmacro V2765) (let V2766 (shen.lazyderef V2820 V2822) (if (= unit V2766) (do (shen.incinfs) (cut Throwcontrol V2822 V2823)) (if (shen.pvar? V2766) (do (shen.bindv V2766 unit V2822) (let Result (do (shen.incinfs) (cut Throwcontrol V2822 V2823)) (do (shen.unbindv V2766 V2822) Result))) false))) false)) false)) (if (= Case false) (let Case (let V2767 (shen.lazyderef V2819 V2822) (if (cons? V2767) (let V2768 (shen.lazyderef (hd V2767) V2822) (if (= shen.process-datatype V2768) (let V2769 (shen.lazyderef V2820 V2822) (if (= symbol V2769) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2769) (do (shen.bindv V2769 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2769 V2822) Result))) false))) false)) false)) (if (= Case false) (let Case (let V2770 (shen.lazyderef V2819 V2822) (if (cons? V2770) (let V2771 (shen.lazyderef (hd V2770) V2822) (if (= shen.synonyms-help V2771) (let V2772 (shen.lazyderef V2820 V2822) (if (= symbol V2772) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2772) (do (shen.bindv V2772 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2772 V2822) Result))) false))) false)) false)) (if (= Case false) (let Datatypes (shen.newpv V2822) (do (shen.incinfs) (bind Datatypes (value shen.*datatypes*) V2822 (freeze (shen.udefs* (cons V2819 (cons : (cons V2820 ()))) V2821 Datatypes V2822 V2823))))) Case)) 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 (V2824 V2825 V2826 V2827) (let Case (let V2579 (shen.lazyderef V2824 V2826) (if (cons? V2579) (let V2580 (shen.lazyderef (hd V2579) V2826) (if (cons? V2580) (let V2581 (shen.lazyderef (hd V2580) V2826) (if (cons? V2581) (let V2582 (shen.lazyderef (hd V2581) V2826) (if (= cons V2582) (let V2583 (shen.lazyderef (tl V2581) V2826) (if (cons? V2583) (let X (hd V2583) (let V2584 (shen.lazyderef (tl V2583) V2826) (if (cons? V2584) (let Y (hd V2584) (let V2585 (shen.lazyderef (tl V2584) V2826) (if (= () V2585) (let V2586 (shen.lazyderef (tl V2580) V2826) (if (cons? V2586) (let V2587 (shen.lazyderef (hd V2586) V2826) (if (= : V2587) (let V2588 (shen.lazyderef (tl V2586) V2826) (if (cons? V2588) (let V2589 (shen.lazyderef (hd V2588) V2826) (if (cons? V2589) (let V2590 (shen.lazyderef (hd V2589) V2826) (if (= list V2590) (let V2591 (shen.lazyderef (tl V2589) V2826) (if (cons? V2591) (let A (hd V2591) (let V2592 (shen.lazyderef (tl V2591) V2826) (if (= () V2592) (let V2593 (shen.lazyderef (tl V2588) V2826) (if (= () V2593) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2593) (do (shen.bindv V2593 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2593 V2826) Result))) false))) (if (shen.pvar? V2592) (do (shen.bindv V2592 () V2826) (let Result (let V2594 (shen.lazyderef (tl V2588) V2826) (if (= () V2594) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2594) (do (shen.bindv V2594 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2594 V2826) Result))) false))) (do (shen.unbindv V2592 V2826) Result))) false)))) (if (shen.pvar? V2591) (let A (shen.newpv V2826) (do (shen.bindv V2591 (cons A ()) V2826) (let Result (let V2595 (shen.lazyderef (tl V2588) V2826) (if (= () V2595) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2595) (do (shen.bindv V2595 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2595 V2826) Result))) false))) (do (shen.unbindv V2591 V2826) Result)))) false))) (if (shen.pvar? V2590) (do (shen.bindv V2590 list V2826) (let Result (let V2596 (shen.lazyderef (tl V2589) V2826) (if (cons? V2596) (let A (hd V2596) (let V2597 (shen.lazyderef (tl V2596) V2826) (if (= () V2597) (let V2598 (shen.lazyderef (tl V2588) V2826) (if (= () V2598) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2598) (do (shen.bindv V2598 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2598 V2826) Result))) false))) (if (shen.pvar? V2597) (do (shen.bindv V2597 () V2826) (let Result (let V2599 (shen.lazyderef (tl V2588) V2826) (if (= () V2599) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2599) (do (shen.bindv V2599 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2599 V2826) Result))) false))) (do (shen.unbindv V2597 V2826) Result))) false)))) (if (shen.pvar? V2596) (let A (shen.newpv V2826) (do (shen.bindv V2596 (cons A ()) V2826) (let Result (let V2600 (shen.lazyderef (tl V2588) V2826) (if (= () V2600) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2600) (do (shen.bindv V2600 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2600 V2826) Result))) false))) (do (shen.unbindv V2596 V2826) Result)))) false))) (do (shen.unbindv V2590 V2826) Result))) false))) (if (shen.pvar? V2589) (let A (shen.newpv V2826) (do (shen.bindv V2589 (cons list (cons A ())) V2826) (let Result (let V2601 (shen.lazyderef (tl V2588) V2826) (if (= () V2601) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2601) (do (shen.bindv V2601 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2601 V2826) Result))) false))) (do (shen.unbindv V2589 V2826) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2602 (shen.lazyderef V2824 V2826) (if (cons? V2602) (let V2603 (shen.lazyderef (hd V2602) V2826) (if (cons? V2603) (let V2604 (shen.lazyderef (hd V2603) V2826) (if (cons? V2604) (let V2605 (shen.lazyderef (hd V2604) V2826) (if (= @p V2605) (let V2606 (shen.lazyderef (tl V2604) V2826) (if (cons? V2606) (let X (hd V2606) (let V2607 (shen.lazyderef (tl V2606) V2826) (if (cons? V2607) (let Y (hd V2607) (let V2608 (shen.lazyderef (tl V2607) V2826) (if (= () V2608) (let V2609 (shen.lazyderef (tl V2603) V2826) (if (cons? V2609) (let V2610 (shen.lazyderef (hd V2609) V2826) (if (= : V2610) (let V2611 (shen.lazyderef (tl V2609) V2826) (if (cons? V2611) (let V2612 (shen.lazyderef (hd V2611) V2826) (if (cons? V2612) (let A (hd V2612) (let V2613 (shen.lazyderef (tl V2612) V2826) (if (cons? V2613) (let V2614 (shen.lazyderef (hd V2613) V2826) (if (= * V2614) (let V2615 (shen.lazyderef (tl V2613) V2826) (if (cons? V2615) (let B (hd V2615) (let V2616 (shen.lazyderef (tl V2615) V2826) (if (= () V2616) (let V2617 (shen.lazyderef (tl V2611) V2826) (if (= () V2617) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2617) (do (shen.bindv V2617 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2617 V2826) Result))) false))) (if (shen.pvar? V2616) (do (shen.bindv V2616 () V2826) (let Result (let V2618 (shen.lazyderef (tl V2611) V2826) (if (= () V2618) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2618) (do (shen.bindv V2618 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2618 V2826) Result))) false))) (do (shen.unbindv V2616 V2826) Result))) false)))) (if (shen.pvar? V2615) (let B (shen.newpv V2826) (do (shen.bindv V2615 (cons B ()) V2826) (let Result (let V2619 (shen.lazyderef (tl V2611) V2826) (if (= () V2619) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2619) (do (shen.bindv V2619 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2619 V2826) Result))) false))) (do (shen.unbindv V2615 V2826) Result)))) false))) (if (shen.pvar? V2614) (do (shen.bindv V2614 * V2826) (let Result (let V2620 (shen.lazyderef (tl V2613) V2826) (if (cons? V2620) (let B (hd V2620) (let V2621 (shen.lazyderef (tl V2620) V2826) (if (= () V2621) (let V2622 (shen.lazyderef (tl V2611) V2826) (if (= () V2622) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2622) (do (shen.bindv V2622 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2622 V2826) Result))) false))) (if (shen.pvar? V2621) (do (shen.bindv V2621 () V2826) (let Result (let V2623 (shen.lazyderef (tl V2611) V2826) (if (= () V2623) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2623) (do (shen.bindv V2623 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2623 V2826) Result))) false))) (do (shen.unbindv V2621 V2826) Result))) false)))) (if (shen.pvar? V2620) (let B (shen.newpv V2826) (do (shen.bindv V2620 (cons B ()) V2826) (let Result (let V2624 (shen.lazyderef (tl V2611) V2826) (if (= () V2624) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2624) (do (shen.bindv V2624 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2624 V2826) Result))) false))) (do (shen.unbindv V2620 V2826) Result)))) false))) (do (shen.unbindv V2614 V2826) Result))) false))) (if (shen.pvar? V2613) (let B (shen.newpv V2826) (do (shen.bindv V2613 (cons * (cons B ())) V2826) (let Result (let V2625 (shen.lazyderef (tl V2611) V2826) (if (= () V2625) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2625) (do (shen.bindv V2625 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2625 V2826) Result))) false))) (do (shen.unbindv V2613 V2826) Result)))) false)))) (if (shen.pvar? V2612) (let A (shen.newpv V2826) (let B (shen.newpv V2826) (do (shen.bindv V2612 (cons A (cons * (cons B ()))) V2826) (let Result (let V2626 (shen.lazyderef (tl V2611) V2826) (if (= () V2626) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2626) (do (shen.bindv V2626 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2626 V2826) Result))) false))) (do (shen.unbindv V2612 V2826) Result))))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2627 (shen.lazyderef V2824 V2826) (if (cons? V2627) (let V2628 (shen.lazyderef (hd V2627) V2826) (if (cons? V2628) (let V2629 (shen.lazyderef (hd V2628) V2826) (if (cons? V2629) (let V2630 (shen.lazyderef (hd V2629) V2826) (if (= @v V2630) (let V2631 (shen.lazyderef (tl V2629) V2826) (if (cons? V2631) (let X (hd V2631) (let V2632 (shen.lazyderef (tl V2631) V2826) (if (cons? V2632) (let Y (hd V2632) (let V2633 (shen.lazyderef (tl V2632) V2826) (if (= () V2633) (let V2634 (shen.lazyderef (tl V2628) V2826) (if (cons? V2634) (let V2635 (shen.lazyderef (hd V2634) V2826) (if (= : V2635) (let V2636 (shen.lazyderef (tl V2634) V2826) (if (cons? V2636) (let V2637 (shen.lazyderef (hd V2636) V2826) (if (cons? V2637) (let V2638 (shen.lazyderef (hd V2637) V2826) (if (= vector V2638) (let V2639 (shen.lazyderef (tl V2637) V2826) (if (cons? V2639) (let A (hd V2639) (let V2640 (shen.lazyderef (tl V2639) V2826) (if (= () V2640) (let V2641 (shen.lazyderef (tl V2636) V2826) (if (= () V2641) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2641) (do (shen.bindv V2641 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2641 V2826) Result))) false))) (if (shen.pvar? V2640) (do (shen.bindv V2640 () V2826) (let Result (let V2642 (shen.lazyderef (tl V2636) V2826) (if (= () V2642) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2642) (do (shen.bindv V2642 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2642 V2826) Result))) false))) (do (shen.unbindv V2640 V2826) Result))) false)))) (if (shen.pvar? V2639) (let A (shen.newpv V2826) (do (shen.bindv V2639 (cons A ()) V2826) (let Result (let V2643 (shen.lazyderef (tl V2636) V2826) (if (= () V2643) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2643) (do (shen.bindv V2643 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2643 V2826) Result))) false))) (do (shen.unbindv V2639 V2826) Result)))) false))) (if (shen.pvar? V2638) (do (shen.bindv V2638 vector V2826) (let Result (let V2644 (shen.lazyderef (tl V2637) V2826) (if (cons? V2644) (let A (hd V2644) (let V2645 (shen.lazyderef (tl V2644) V2826) (if (= () V2645) (let V2646 (shen.lazyderef (tl V2636) V2826) (if (= () V2646) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2646) (do (shen.bindv V2646 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2646 V2826) Result))) false))) (if (shen.pvar? V2645) (do (shen.bindv V2645 () V2826) (let Result (let V2647 (shen.lazyderef (tl V2636) V2826) (if (= () V2647) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2647) (do (shen.bindv V2647 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2647 V2826) Result))) false))) (do (shen.unbindv V2645 V2826) Result))) false)))) (if (shen.pvar? V2644) (let A (shen.newpv V2826) (do (shen.bindv V2644 (cons A ()) V2826) (let Result (let V2648 (shen.lazyderef (tl V2636) V2826) (if (= () V2648) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2648) (do (shen.bindv V2648 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2648 V2826) Result))) false))) (do (shen.unbindv V2644 V2826) Result)))) false))) (do (shen.unbindv V2638 V2826) Result))) false))) (if (shen.pvar? V2637) (let A (shen.newpv V2826) (do (shen.bindv V2637 (cons vector (cons A ())) V2826) (let Result (let V2649 (shen.lazyderef (tl V2636) V2826) (if (= () V2649) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2649) (do (shen.bindv V2649 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2649 V2826) Result))) false))) (do (shen.unbindv V2637 V2826) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2650 (shen.lazyderef V2824 V2826) (if (cons? V2650) (let V2651 (shen.lazyderef (hd V2650) V2826) (if (cons? V2651) (let V2652 (shen.lazyderef (hd V2651) V2826) (if (cons? V2652) (let V2653 (shen.lazyderef (hd V2652) V2826) (if (= @s V2653) (let V2654 (shen.lazyderef (tl V2652) V2826) (if (cons? V2654) (let X (hd V2654) (let V2655 (shen.lazyderef (tl V2654) V2826) (if (cons? V2655) (let Y (hd V2655) (let V2656 (shen.lazyderef (tl V2655) V2826) (if (= () V2656) (let V2657 (shen.lazyderef (tl V2651) V2826) (if (cons? V2657) (let V2658 (shen.lazyderef (hd V2657) V2826) (if (= : V2658) (let V2659 (shen.lazyderef (tl V2657) V2826) (if (cons? V2659) (let V2660 (shen.lazyderef (hd V2659) V2826) (if (= string V2660) (let V2661 (shen.lazyderef (tl V2659) V2826) (if (= () V2661) (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2661) (do (shen.bindv V2661 () V2826) (let Result (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2661 V2826) Result))) false))) (if (shen.pvar? V2660) (do (shen.bindv V2660 string V2826) (let Result (let V2662 (shen.lazyderef (tl V2659) V2826) (if (= () V2662) (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2662) (do (shen.bindv V2662 () V2826) (let Result (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2662 V2826) Result))) false))) (do (shen.unbindv V2660 V2826) Result))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let V2663 (shen.lazyderef V2824 V2826) (if (cons? V2663) (let X (hd V2663) (let Hyp (tl V2663) (let NewHyps (shen.newpv V2826) (do (shen.incinfs) (bind V2825 (cons (shen.lazyderef X V2826) (shen.lazyderef NewHyps V2826)) V2826 (freeze (shen.t*-hyps Hyp NewHyps V2826 V2827))))))) false)) Case)) Case)) Case)) Case)))
-
-(defun shen.show (V2840 V2841 V2842 V2843) (cond ((value shen.*spy*) (do (shen.line) (do (shen.show-p (shen.deref V2840 V2842)) (do (nl 1) (do (nl 1) (do (shen.show-assumptions (shen.deref V2841 V2842) 1) (do (shen.prhush "
-> " (stoutput)) (do (shen.pause-for-user) (thaw V2843))))))))) (true (thaw V2843))))
-
-(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 (V2844) (cond ((and (cons? V2844) (and (cons? (tl V2844)) (and (= : (hd (tl V2844))) (and (cons? (tl (tl V2844))) (= () (tl (tl (tl V2844)))))))) (shen.prhush (shen.app (hd V2844) (cn " : " (shen.app (hd (tl (tl V2844))) "" shen.r)) shen.r) (stoutput))) (true (shen.prhush (shen.app V2844 "" shen.r) (stoutput)))))
-
-(defun shen.show-assumptions (V2847 V2848) (cond ((= () V2847) shen.skip) ((cons? V2847) (do (shen.prhush (shen.app V2848 ". " shen.a) (stoutput)) (do (shen.show-p (hd V2847)) (do (nl 1) (shen.show-assumptions (tl V2847) (+ V2848 1)))))) (true (shen.sys-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? (V2849) (cons? (assoc V2849 (value shen.*signedfuncs*))))
-
-(defun shen.sigf (V2850) (concat shen.type-signature-of- V2850))
-
-(defun shen.placeholder () (gensym &&))
-
-(defun shen.base (V2851 V2852 V2853 V2854) (let Case (let V2566 (shen.lazyderef V2852 V2853) (if (= number V2566) (do (shen.incinfs) (fwhen (number? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2566) (do (shen.bindv V2566 number V2853) (let Result (do (shen.incinfs) (fwhen (number? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2566 V2853) Result))) false))) (if (= Case false) (let Case (let V2567 (shen.lazyderef V2852 V2853) (if (= boolean V2567) (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2567) (do (shen.bindv V2567 boolean V2853) (let Result (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2567 V2853) Result))) false))) (if (= Case false) (let Case (let V2568 (shen.lazyderef V2852 V2853) (if (= string V2568) (do (shen.incinfs) (fwhen (string? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2568) (do (shen.bindv V2568 string V2853) (let Result (do (shen.incinfs) (fwhen (string? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2568 V2853) Result))) false))) (if (= Case false) (let Case (let V2569 (shen.lazyderef V2852 V2853) (if (= symbol V2569) (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V2851 V2853)) V2853 (freeze (fwhen (not (shen.ue? (shen.lazyderef V2851 V2853))) V2853 V2854)))) (if (shen.pvar? V2569) (do (shen.bindv V2569 symbol V2853) (let Result (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V2851 V2853)) V2853 (freeze (fwhen (not (shen.ue? (shen.lazyderef V2851 V2853))) V2853 V2854)))) (do (shen.unbindv V2569 V2853) Result))) false))) (if (= Case false) (let V2570 (shen.lazyderef V2851 V2853) (if (= () V2570) (let V2571 (shen.lazyderef V2852 V2853) (if (cons? V2571) (let V2572 (shen.lazyderef (hd V2571) V2853) (if (= list V2572) (let V2573 (shen.lazyderef (tl V2571) V2853) (if (cons? V2573) (let A (hd V2573) (let V2574 (shen.lazyderef (tl V2573) V2853) (if (= () V2574) (do (shen.incinfs) (thaw V2854)) (if (shen.pvar? V2574) (do (shen.bindv V2574 () V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2574 V2853) Result))) false)))) (if (shen.pvar? V2573) (let A (shen.newpv V2853) (do (shen.bindv V2573 (cons A ()) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2573 V2853) Result)))) false))) (if (shen.pvar? V2572) (do (shen.bindv V2572 list V2853) (let Result (let V2575 (shen.lazyderef (tl V2571) V2853) (if (cons? V2575) (let A (hd V2575) (let V2576 (shen.lazyderef (tl V2575) V2853) (if (= () V2576) (do (shen.incinfs) (thaw V2854)) (if (shen.pvar? V2576) (do (shen.bindv V2576 () V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2576 V2853) Result))) false)))) (if (shen.pvar? V2575) (let A (shen.newpv V2853) (do (shen.bindv V2575 (cons A ()) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2575 V2853) Result)))) false))) (do (shen.unbindv V2572 V2853) Result))) false))) (if (shen.pvar? V2571) (let A (shen.newpv V2853) (do (shen.bindv V2571 (cons list (cons A ())) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2571 V2853) Result)))) false))) false)) Case)) Case)) Case)) Case)))
-
-(defun shen.by_hypothesis (V2855 V2856 V2857 V2858 V2859) (let Case (let V2557 (shen.lazyderef V2857 V2858) (if (cons? V2557) (let V2558 (shen.lazyderef (hd V2557) V2858) (if (cons? V2558) (let Y (hd V2558) (let V2559 (shen.lazyderef (tl V2558) V2858) (if (cons? V2559) (let V2560 (shen.lazyderef (hd V2559) V2858) (if (= : V2560) (let V2561 (shen.lazyderef (tl V2559) V2858) (if (cons? V2561) (let B (hd V2561) (let V2562 (shen.lazyderef (tl V2561) V2858) (if (= () V2562) (do (shen.incinfs) (identical V2855 Y V2858 (freeze (unify! V2856 B V2858 V2859)))) false))) false)) false)) false))) false)) false)) (if (= Case false) (let V2563 (shen.lazyderef V2857 V2858) (if (cons? V2563) (let Hyp (tl V2563) (do (shen.incinfs) (shen.by_hypothesis V2855 V2856 Hyp V2858 V2859))) false)) Case)))
-
-(defun shen.t*-def (V2860 V2861 V2862 V2863 V2864) (let V2551 (shen.lazyderef V2860 V2863) (if (cons? V2551) (let V2552 (shen.lazyderef (hd V2551) V2863) (if (= define V2552) (let V2553 (shen.lazyderef (tl V2551) V2863) (if (cons? V2553) (let F (hd V2553) (let X (tl V2553) (let E (shen.newpv V2863) (do (shen.incinfs) (shen.t*-defh (compile (lambda X2787 (shen.<sig+rules> X2787)) X (lambda E (if (cons? E) (simple-error (cn "parse error here: " (shen.app E "
-" shen.s))) (simple-error "parse error
-")))) F V2861 V2862 V2863 V2864))))) false)) false)) false)))
-
-(defun shen.t*-defh (V2865 V2866 V2867 V2868 V2869 V2870) (let V2547 (shen.lazyderef V2865 V2869) (if (cons? V2547) (let Sig (hd V2547) (let Rules (tl V2547) (do (shen.incinfs) (shen.t*-defhh Sig (shen.ue-sig Sig) V2866 V2867 V2868 Rules V2869 V2870)))) false)))
-
-(defun shen.t*-defhh (V2871 V2872 V2873 V2874 V2875 V2876 V2877 V2878) (do (shen.incinfs) (shen.t*-rules V2876 V2872 1 V2873 (cons (cons V2873 (cons : (cons V2872 ()))) V2875) V2877 (freeze (shen.memo V2873 V2871 V2874 V2877 V2878)))))
-
-(defun shen.memo (V2879 V2880 V2881 V2882 V2883) (let Jnk (shen.newpv V2882) (do (shen.incinfs) (unify! V2881 V2880 V2882 (freeze (bind Jnk (declare (shen.lazyderef V2879 V2882) (shen.lazyderef V2881 V2882)) V2882 V2883))))))
-
-(defun shen.<sig+rules> (V2888) (let Result (let Parse_shen.<signature> (shen.<signature> V2888) (if (not (= (fail) Parse_shen.<signature>)) (let Parse_shen.<rules> (shen.<rules> Parse_shen.<signature>) (if (not (= (fail) Parse_shen.<rules>)) (shen.pair (hd Parse_shen.<rules>) (cons (shen.hdtl Parse_shen.<signature>) (shen.hdtl Parse_shen.<rules>))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)))
-
-(defun shen.ue (V2889) (cond ((and (cons? V2889) (and (cons? (tl V2889)) (and (= () (tl (tl V2889))) (= (hd V2889) protect)))) V2889) ((cons? V2889) (map (lambda X2788 (shen.ue X2788)) V2889)) ((variable? V2889) (concat && V2889)) (true V2889)))
-
-(defun shen.ue-sig (V2890) (cond ((cons? V2890) (map (lambda X2789 (shen.ue-sig X2789)) V2890)) ((variable? V2890) (concat &&& V2890)) (true V2890)))
-
-(defun shen.ues (V2895) (cond ((shen.ue? V2895) (cons V2895 ())) ((cons? V2895) (union (shen.ues (hd V2895)) (shen.ues (tl V2895)))) (true ())))
-
-(defun shen.ue? (V2896) (and (symbol? V2896) (shen.ue-h? (str V2896))))
-
-(defun shen.ue-h? (V2903) (cond ((and (shen.+string? V2903) (and (= "&" (pos V2903 0)) (and (shen.+string? (tlstr V2903)) (= "&" (pos (tlstr V2903) 0))))) true) (true false)))
-
-(defun shen.t*-rules (V2904 V2905 V2906 V2907 V2908 V2909 V2910) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2522 (shen.lazyderef V2904 V2909) (if (= () V2522) (do (shen.incinfs) (thaw V2910)) false)) (if (= Case false) (let Case (let V2523 (shen.lazyderef V2904 V2909) (if (cons? V2523) (let V2524 (shen.lazyderef (hd V2523) V2909) (if (cons? V2524) (let V2525 (shen.lazyderef (hd V2524) V2909) (if (= () V2525) (let V2526 (shen.lazyderef (tl V2524) V2909) (if (cons? V2526) (let Action (hd V2526) (let V2527 (shen.lazyderef (tl V2526) V2909) (if (= () V2527) (let Rules (tl V2523) (let V2528 (shen.lazyderef V2905 V2909) (if (cons? V2528) (let V2529 (shen.lazyderef (hd V2528) V2909) (if (= --> V2529) (let V2530 (shen.lazyderef (tl V2528) V2909) (if (cons? V2530) (let A (hd V2530) (let V2531 (shen.lazyderef (tl V2530) V2909) (if (= () V2531) (do (shen.incinfs) (shen.t*-rule (cons () (cons (shen.ue Action) ())) A V2908 V2909 (freeze (cut Throwcontrol V2909 (freeze (shen.t*-rules Rules A (+ V2906 1) V2907 V2908 V2909 V2910)))))) false))) false)) false)) false))) false))) false)) false)) false)) false)) (if (= Case false) (let Case (let V2532 (shen.lazyderef V2904 V2909) (if (cons? V2532) (let Rule (hd V2532) (let Rules (tl V2532) (do (shen.incinfs) (shen.t*-rule (shen.ue Rule) V2905 V2908 V2909 (freeze (cut Throwcontrol V2909 (freeze (shen.t*-rules Rules V2905 (+ V2906 1) V2907 V2908 V2909 V2910)))))))) false)) (if (= Case false) (let Err (shen.newpv V2909) (do (shen.incinfs) (bind Err (simple-error (cn "type error in rule " (shen.app (shen.lazyderef V2906 V2909) (cn " of " (shen.app (shen.lazyderef V2907 V2909) "" shen.a)) shen.a))) V2909 V2910))) Case)) Case)) Case)))))
-
-(defun shen.t*-rule (V2911 V2912 V2913 V2914 V2915) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2504 (shen.lazyderef V2911 V2914) (if (cons? V2504) (let V2505 (shen.lazyderef (hd V2504) V2914) (if (= () V2505) (let V2506 (shen.lazyderef (tl V2504) V2914) (if (cons? V2506) (let Action (hd V2506) (let V2507 (shen.lazyderef (tl V2506) V2914) (if (= () V2507) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (shen.t*-action (shen.curry Action) V2912 V2913 V2914 V2915)))) false))) false)) false)) false)) (if (= Case false) (let V2508 (shen.lazyderef V2911 V2914) (if (cons? V2508) (let V2509 (shen.lazyderef (hd V2508) V2914) (if (cons? V2509) (let Pattern (hd V2509) (let Patterns (tl V2509) (let V2510 (shen.lazyderef (tl V2508) V2914) (if (cons? V2510) (let Action (hd V2510) (let V2511 (shen.lazyderef (tl V2510) V2914) (if (= () V2511) (let V2512 (shen.lazyderef V2912 V2914) (if (cons? V2512) (let A (hd V2512) (let V2513 (shen.lazyderef (tl V2512) V2914) (if (cons? V2513) (let V2514 (shen.lazyderef (hd V2513) V2914) (if (= --> V2514) (let V2515 (shen.lazyderef (tl V2513) V2914) (if (cons? V2515) (let B (hd V2515) (let V2516 (shen.lazyderef (tl V2515) V2914) (if (= () V2516) (do (shen.incinfs) (shen.t*-pattern Pattern A V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.t*-rule (cons Patterns (cons Action ())) B (cons (cons Pattern (cons : (cons A ()))) V2913) V2914 V2915)))))) false))) false)) false)) false))) false)) false))) false)))) false)) false)) Case)))))
-
-(defun shen.t*-action (V2916 V2917 V2918 V2919 V2920) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2481 (shen.lazyderef V2916 V2919) (if (cons? V2481) (let V2482 (shen.lazyderef (hd V2481) V2919) (if (= where V2482) (let V2483 (shen.lazyderef (tl V2481) V2919) (if (cons? V2483) (let P (hd V2483) (let V2484 (shen.lazyderef (tl V2483) V2919) (if (cons? V2484) (let Action (hd V2484) (let V2485 (shen.lazyderef (tl V2484) V2919) (if (= () V2485) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t* (cons P (cons : (cons boolean ()))) V2918 V2919 (freeze (cut Throwcontrol V2919 (freeze (shen.t*-action Action V2917 (cons (cons P (cons : (cons verified ()))) V2918) V2919 V2920)))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2486 (shen.lazyderef V2916 V2919) (if (cons? V2486) (let V2487 (shen.lazyderef (hd V2486) V2919) (if (= shen.choicepoint! V2487) (let V2488 (shen.lazyderef (tl V2486) V2919) (if (cons? V2488) (let V2489 (shen.lazyderef (hd V2488) V2919) (if (cons? V2489) (let V2490 (shen.lazyderef (hd V2489) V2919) (if (cons? V2490) (let V2491 (shen.lazyderef (hd V2490) V2919) (if (= fail-if V2491) (let V2492 (shen.lazyderef (tl V2490) V2919) (if (cons? V2492) (let F (hd V2492) (let V2493 (shen.lazyderef (tl V2492) V2919) (if (= () V2493) (let V2494 (shen.lazyderef (tl V2489) V2919) (if (cons? V2494) (let Action (hd V2494) (let V2495 (shen.lazyderef (tl V2494) V2919) (if (= () V2495) (let V2496 (shen.lazyderef (tl V2488) V2919) (if (= () V2496) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons F (cons Action ())) ())) (cons Action ()))) V2917 V2918 V2919 V2920)))) false)) false))) false)) false))) false)) false)) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2497 (shen.lazyderef V2916 V2919) (if (cons? V2497) (let V2498 (shen.lazyderef (hd V2497) V2919) (if (= shen.choicepoint! V2498) (let V2499 (shen.lazyderef (tl V2497) V2919) (if (cons? V2499) (let Action (hd V2499) (let V2500 (shen.lazyderef (tl V2499) V2919) (if (= () V2500) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons (cons = (cons Action ())) (cons (cons fail ()) ())) ())) (cons Action ()))) V2917 V2918 V2919 V2920)))) false))) false)) false)) false)) (if (= Case false) (do (shen.incinfs) (shen.t* (cons V2916 (cons : (cons V2917 ()))) V2918 V2919 V2920)) Case)) Case)) Case)))))
-
-(defun shen.t*-pattern (V2921 V2922 V2923 V2924) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Hyp (shen.newpv V2923) (do (shen.incinfs) (shen.tms->hyp (shen.ues V2921) Hyp V2923 (freeze (cut Throwcontrol V2923 (freeze (shen.t* (cons V2921 (cons : (cons V2922 ()))) Hyp V2923 V2924))))))))))
-
-(defun shen.tms->hyp (V2925 V2926 V2927 V2928) (let Case (let V2465 (shen.lazyderef V2925 V2927) (if (= () V2465) (let V2466 (shen.lazyderef V2926 V2927) (if (= () V2466) (do (shen.incinfs) (thaw V2928)) (if (shen.pvar? V2466) (do (shen.bindv V2466 () V2927) (let Result (do (shen.incinfs) (thaw V2928)) (do (shen.unbindv V2466 V2927) Result))) false))) false)) (if (= Case false) (let V2467 (shen.lazyderef V2925 V2927) (if (cons? V2467) (let Tm2462 (hd V2467) (let Tms (tl V2467) (let V2468 (shen.lazyderef V2926 V2927) (if (cons? V2468) (let V2469 (shen.lazyderef (hd V2468) V2927) (if (cons? V2469) (let Tm (hd V2469) (let V2470 (shen.lazyderef (tl V2469) V2927) (if (cons? V2470) (let V2471 (shen.lazyderef (hd V2470) V2927) (if (= : V2471) (let V2472 (shen.lazyderef (tl V2470) V2927) (if (cons? V2472) (let A (hd V2472) (let V2473 (shen.lazyderef (tl V2472) V2927) (if (= () V2473) (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (if (shen.pvar? V2473) (do (shen.bindv V2473 () V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2473 V2927) Result))) false)))) (if (shen.pvar? V2472) (let A (shen.newpv V2927) (do (shen.bindv V2472 (cons A ()) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2472 V2927) Result)))) false))) (if (shen.pvar? V2471) (do (shen.bindv V2471 : V2927) (let Result (let V2474 (shen.lazyderef (tl V2470) V2927) (if (cons? V2474) (let A (hd V2474) (let V2475 (shen.lazyderef (tl V2474) V2927) (if (= () V2475) (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (if (shen.pvar? V2475) (do (shen.bindv V2475 () V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2475 V2927) Result))) false)))) (if (shen.pvar? V2474) (let A (shen.newpv V2927) (do (shen.bindv V2474 (cons A ()) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2474 V2927) Result)))) false))) (do (shen.unbindv V2471 V2927) Result))) false))) (if (shen.pvar? V2470) (let A (shen.newpv V2927) (do (shen.bindv V2470 (cons : (cons A ())) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2470 V2927) Result)))) false)))) (if (shen.pvar? V2469) (let Tm (shen.newpv V2927) (let A (shen.newpv V2927) (do (shen.bindv V2469 (cons Tm (cons : (cons A ()))) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2469 V2927) Result))))) false))) (if (shen.pvar? V2468) (let Tm (shen.newpv V2927) (let A (shen.newpv V2927) (let Hyp (shen.newpv V2927) (do (shen.bindv V2468 (cons (cons Tm (cons : (cons A ()))) Hyp) V2927) (let Result (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928)))) (do (shen.unbindv V2468 V2927) Result)))))) false))))) false)) Case)))
-
-(defun findall (V2929 V2930 V2931 V2932 V2933) (let B (shen.newpv V2932) (let A (shen.newpv V2932) (do (shen.incinfs) (bind A (gensym shen.a) V2932 (freeze (bind B (set (shen.lazyderef A V2932) ()) V2932 (freeze (shen.findallhelp V2929 V2930 V2931 A V2932 V2933)))))))))
-
-(defun shen.findallhelp (V2934 V2935 V2936 V2937 V2938 V2939) (let Case (do (shen.incinfs) (call V2935 V2938 (freeze (shen.remember V2937 V2934 V2938 (freeze (fwhen false V2938 V2939)))))) (if (= Case false) (do (shen.incinfs) (bind V2936 (value (shen.lazyderef V2937 V2938)) V2938 V2939)) Case)))
-
-(defun shen.remember (V2940 V2941 V2942 V2943) (let B (shen.newpv V2942) (do (shen.incinfs) (bind B (set (shen.deref V2940 V2942) (cons (shen.deref V2941 V2942) (value (shen.deref V2940 V2942)))) V2942 V2943))))
-
-
-
+"**********************************************************************************
+* The License *
+* *
+* The user is free to produce commercial applications with the software, to *
+* distribute these applications in source or binary form, and to charge monies *
+* for them as he sees fit and in concordance with the laws of the land subject *
+* to the following license. *
+* *
+* 1. The license applies to all the software and all derived software and *
+* must appear on such. *
+* *
+* 2. It is illegal to distribute the software without this license attached *
+* to it and use of the software implies agreement with the license as such. *
+* It is illegal for anyone who is not the copyright holder to tamper with *
+* or change the license. *
+* *
+* 3. Neither the names of Lambda Associates or the copyright holder may be used *
+* to endorse or promote products built using the software without specific *
+* prior written permission from the copyright holder. *
+* *
+* 4. That possession of this license does not confer on the copyright holder *
+* any special contractual obligation towards the user. That in no event *
+* shall the copyright holder 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, *
+* interruption), however caused and on any theory of liability, whether in *
+* contract, strict liability or tort (including negligence) arising in any *
+* way out of the use of the software, even if advised of the possibility of *
+* such damage. *
+* *
+* 5. It is permitted for the user to change the software, for the purpose of *
+* improving performance, correcting an error, or porting to a new platform, *
+* and distribute the derived version of Shen provided the resulting program *
+* conforms in all respects to the Shen standard and is issued under that *
+* title. The user must make it clear with his distribution that he/she is *
+* the author of the changes and what these changes are and why. *
+* *
+* 6. Derived versions of this software in whatever form are subject to the same *
+* restrictions. In particular it is not permitted to make derived copies of *
+* this software which do not conform to the Shen standard or appear under a *
+* different title. *
+* *
+* It is permitted to distribute versions of Shen which incorporate libraries, *
+* graphics or other facilities which are not part of the Shen standard. *
+* *
+* For an explication of this license see www.shenlanguage.org/license.htm which *
+* explains this license in full. *
+* *
+*****************************************************************************************
+"(defun shen.typecheck (V2790 V2791) (let Curry (shen.curry V2790) (let ProcessN (shen.start-new-prolog-process) (let Type (shen.insert-prolog-variables (shen.demodulate (shen.curry-type V2791)) ProcessN) (let Continuation (freeze (return Type ProcessN shen.void)) (shen.t* (cons Curry (cons : (cons Type ()))) () ProcessN Continuation))))))
+
+(defun shen.curry (V2792) (cond ((and (cons? V2792) (shen.special? (hd V2792))) (cons (hd V2792) (map (lambda X2786 (shen.curry X2786)) (tl V2792)))) ((and (cons? V2792) (and (cons? (tl V2792)) (shen.extraspecial? (hd V2792)))) V2792) ((and (cons? V2792) (and (= type (hd V2792)) (and (cons? (tl V2792)) (and (cons? (tl (tl V2792))) (= () (tl (tl (tl V2792)))))))) (cons type (cons (shen.curry (hd (tl V2792))) (tl (tl V2792))))) ((and (cons? V2792) (and (cons? (tl V2792)) (cons? (tl (tl V2792))))) (shen.curry (cons (cons (hd V2792) (cons (hd (tl V2792)) ())) (tl (tl V2792))))) ((and (cons? V2792) (and (cons? (tl V2792)) (= () (tl (tl V2792))))) (cons (shen.curry (hd V2792)) (cons (shen.curry (hd (tl V2792))) ()))) (true V2792)))
+
+(defun shen.special? (V2793) (element? V2793 (value shen.*special*)))
+
+(defun shen.extraspecial? (V2794) (element? V2794 (value shen.*extraspecial*)))
+
+(defun shen.t* (V2795 V2796 V2797 V2798) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let Error (shen.newpv V2797) (do (shen.incinfs) (fwhen (shen.maxinfexceeded?) V2797 (freeze (bind Error (shen.errormaxinfs) V2797 V2798))))) (if (= Case false) (let Case (let V2780 (shen.lazyderef V2795 V2797) (if (= fail V2780) (do (shen.incinfs) (cut Throwcontrol V2797 (freeze (shen.prolog-failure V2797 V2798)))) false)) (if (= Case false) (let Case (let V2781 (shen.lazyderef V2795 V2797) (if (cons? V2781) (let X (hd V2781) (let V2782 (shen.lazyderef (tl V2781) V2797) (if (cons? V2782) (let V2783 (shen.lazyderef (hd V2782) V2797) (if (= : V2783) (let V2784 (shen.lazyderef (tl V2782) V2797) (if (cons? V2784) (let A (hd V2784) (let V2785 (shen.lazyderef (tl V2784) V2797) (if (= () V2785) (do (shen.incinfs) (fwhen (shen.type-theory-enabled?) V2797 (freeze (cut Throwcontrol V2797 (freeze (shen.th* X A V2796 V2797 V2798)))))) false))) false)) false)) false))) false)) (if (= Case false) (let Datatypes (shen.newpv V2797) (do (shen.incinfs) (shen.show V2795 V2796 V2797 (freeze (bind Datatypes (value shen.*datatypes*) V2797 (freeze (shen.udefs* V2795 V2796 Datatypes V2797 V2798))))))) Case)) Case)) Case)))))
+
+(defun shen.type-theory-enabled? () (value shen.*shen-type-theory-enabled?*))
+
+(defun enable-type-theory (V2803) (cond ((= + V2803) (set shen.*shen-type-theory-enabled?* true)) ((= - V2803) (set shen.*shen-type-theory-enabled?* false)) (true (simple-error "enable-type-theory expects a + or a -
+"))))
+
+(defun shen.prolog-failure (V2812 V2813) false)
+
+(defun shen.maxinfexceeded? () (> (inferences) (value shen.*maxinferences*)))
+
+(defun shen.errormaxinfs () (simple-error "maximum inferences exceeded~%"))
+
+(defun shen.udefs* (V2814 V2815 V2816 V2817 V2818) (let Case (let V2776 (shen.lazyderef V2816 V2817) (if (cons? V2776) (let D (hd V2776) (do (shen.incinfs) (call (cons D (cons V2814 (cons V2815 ()))) V2817 V2818))) false)) (if (= Case false) (let V2777 (shen.lazyderef V2816 V2817) (if (cons? V2777) (let Ds (tl V2777) (do (shen.incinfs) (shen.udefs* V2814 V2815 Ds V2817 V2818))) false)) Case)))
+
+(defun shen.th* (V2819 V2820 V2821 V2822 V2823) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (do (shen.incinfs) (shen.show (cons V2819 (cons : (cons V2820 ()))) V2821 V2822 (freeze (fwhen false V2822 V2823)))) (if (= Case false) (let Case (let F (shen.newpv V2822) (do (shen.incinfs) (fwhen (shen.typedf? (shen.lazyderef V2819 V2822)) V2822 (freeze (bind F (shen.sigf (shen.lazyderef V2819 V2822)) V2822 (freeze (call (cons F (cons V2820 ())) V2822 V2823))))))) (if (= Case false) (let Case (do (shen.incinfs) (shen.base V2819 V2820 V2822 V2823)) (if (= Case false) (let Case (do (shen.incinfs) (shen.by_hypothesis V2819 V2820 V2821 V2822 V2823)) (if (= Case false) (let Case (let V2668 (shen.lazyderef V2819 V2822) (if (cons? V2668) (let F (hd V2668) (let V2669 (shen.lazyderef (tl V2668) V2822) (if (= () V2669) (do (shen.incinfs) (shen.th* F (cons --> (cons V2820 ())) V2821 V2822 V2823)) false))) false)) (if (= Case false) (let Case (let V2670 (shen.lazyderef V2819 V2822) (if (cons? V2670) (let F (hd V2670) (let V2671 (shen.lazyderef (tl V2670) V2822) (if (cons? V2671) (let X (hd V2671) (let V2672 (shen.lazyderef (tl V2671) V2822) (if (= () V2672) (let B (shen.newpv V2822) (do (shen.incinfs) (shen.th* F (cons B (cons --> (cons V2820 ()))) V2821 V2822 (freeze (shen.th* X B V2821 V2822 V2823))))) false))) false))) false)) (if (= Case false) (let Case (let V2673 (shen.lazyderef V2819 V2822) (if (cons? V2673) (let V2674 (shen.lazyderef (hd V2673) V2822) (if (= cons V2674) (let V2675 (shen.lazyderef (tl V2673) V2822) (if (cons? V2675) (let X (hd V2675) (let V2676 (shen.lazyderef (tl V2675) V2822) (if (cons? V2676) (let Y (hd V2676) (let V2677 (shen.lazyderef (tl V2676) V2822) (if (= () V2677) (let V2678 (shen.lazyderef V2820 V2822) (if (cons? V2678) (let V2679 (shen.lazyderef (hd V2678) V2822) (if (= list V2679) (let V2680 (shen.lazyderef (tl V2678) V2822) (if (cons? V2680) (let A (hd V2680) (let V2681 (shen.lazyderef (tl V2680) V2822) (if (= () V2681) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2681) (do (shen.bindv V2681 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2681 V2822) Result))) false)))) (if (shen.pvar? V2680) (let A (shen.newpv V2822) (do (shen.bindv V2680 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2680 V2822) Result)))) false))) (if (shen.pvar? V2679) (do (shen.bindv V2679 list V2822) (let Result (let V2682 (shen.lazyderef (tl V2678) V2822) (if (cons? V2682) (let A (hd V2682) (let V2683 (shen.lazyderef (tl V2682) V2822) (if (= () V2683) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2683) (do (shen.bindv V2683 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2683 V2822) Result))) false)))) (if (shen.pvar? V2682) (let A (shen.newpv V2822) (do (shen.bindv V2682 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2682 V2822) Result)))) false))) (do (shen.unbindv V2679 V2822) Result))) false))) (if (shen.pvar? V2678) (let A (shen.newpv V2822) (do (shen.bindv V2678 (cons list (cons A ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons list (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2678 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2684 (shen.lazyderef V2819 V2822) (if (cons? V2684) (let V2685 (shen.lazyderef (hd V2684) V2822) (if (= @p V2685) (let V2686 (shen.lazyderef (tl V2684) V2822) (if (cons? V2686) (let X (hd V2686) (let V2687 (shen.lazyderef (tl V2686) V2822) (if (cons? V2687) (let Y (hd V2687) (let V2688 (shen.lazyderef (tl V2687) V2822) (if (= () V2688) (let V2689 (shen.lazyderef V2820 V2822) (if (cons? V2689) (let A (hd V2689) (let V2690 (shen.lazyderef (tl V2689) V2822) (if (cons? V2690) (let V2691 (shen.lazyderef (hd V2690) V2822) (if (= * V2691) (let V2692 (shen.lazyderef (tl V2690) V2822) (if (cons? V2692) (let B (hd V2692) (let V2693 (shen.lazyderef (tl V2692) V2822) (if (= () V2693) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (if (shen.pvar? V2693) (do (shen.bindv V2693 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2693 V2822) Result))) false)))) (if (shen.pvar? V2692) (let B (shen.newpv V2822) (do (shen.bindv V2692 (cons B ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2692 V2822) Result)))) false))) (if (shen.pvar? V2691) (do (shen.bindv V2691 * V2822) (let Result (let V2694 (shen.lazyderef (tl V2690) V2822) (if (cons? V2694) (let B (hd V2694) (let V2695 (shen.lazyderef (tl V2694) V2822) (if (= () V2695) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (if (shen.pvar? V2695) (do (shen.bindv V2695 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2695 V2822) Result))) false)))) (if (shen.pvar? V2694) (let B (shen.newpv V2822) (do (shen.bindv V2694 (cons B ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2694 V2822) Result)))) false))) (do (shen.unbindv V2691 V2822) Result))) false))) (if (shen.pvar? V2690) (let B (shen.newpv V2822) (do (shen.bindv V2690 (cons * (cons B ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2690 V2822) Result)))) false)))) (if (shen.pvar? V2689) (let A (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.bindv V2689 (cons A (cons * (cons B ()))) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y B V2821 V2822 V2823)))) (do (shen.unbindv V2689 V2822) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2696 (shen.lazyderef V2819 V2822) (if (cons? V2696) (let V2697 (shen.lazyderef (hd V2696) V2822) (if (= @v V2697) (let V2698 (shen.lazyderef (tl V2696) V2822) (if (cons? V2698) (let X (hd V2698) (let V2699 (shen.lazyderef (tl V2698) V2822) (if (cons? V2699) (let Y (hd V2699) (let V2700 (shen.lazyderef (tl V2699) V2822) (if (= () V2700) (let V2701 (shen.lazyderef V2820 V2822) (if (cons? V2701) (let V2702 (shen.lazyderef (hd V2701) V2822) (if (= vector V2702) (let V2703 (shen.lazyderef (tl V2701) V2822) (if (cons? V2703) (let A (hd V2703) (let V2704 (shen.lazyderef (tl V2703) V2822) (if (= () V2704) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2704) (do (shen.bindv V2704 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2704 V2822) Result))) false)))) (if (shen.pvar? V2703) (let A (shen.newpv V2822) (do (shen.bindv V2703 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2703 V2822) Result)))) false))) (if (shen.pvar? V2702) (do (shen.bindv V2702 vector V2822) (let Result (let V2705 (shen.lazyderef (tl V2701) V2822) (if (cons? V2705) (let A (hd V2705) (let V2706 (shen.lazyderef (tl V2705) V2822) (if (= () V2706) (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (if (shen.pvar? V2706) (do (shen.bindv V2706 () V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2706 V2822) Result))) false)))) (if (shen.pvar? V2705) (let A (shen.newpv V2822) (do (shen.bindv V2705 (cons A ()) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2705 V2822) Result)))) false))) (do (shen.unbindv V2702 V2822) Result))) false))) (if (shen.pvar? V2701) (let A (shen.newpv V2822) (do (shen.bindv V2701 (cons vector (cons A ())) V2822) (let Result (do (shen.incinfs) (shen.th* X A V2821 V2822 (freeze (shen.th* Y (cons vector (cons A ())) V2821 V2822 V2823)))) (do (shen.unbindv V2701 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2707 (shen.lazyderef V2819 V2822) (if (cons? V2707) (let V2708 (shen.lazyderef (hd V2707) V2822) (if (= @s V2708) (let V2709 (shen.lazyderef (tl V2707) V2822) (if (cons? V2709) (let X (hd V2709) (let V2710 (shen.lazyderef (tl V2709) V2822) (if (cons? V2710) (let Y (hd V2710) (let V2711 (shen.lazyderef (tl V2710) V2822) (if (= () V2711) (let V2712 (shen.lazyderef V2820 V2822) (if (= string V2712) (do (shen.incinfs) (shen.th* X string V2821 V2822 (freeze (shen.th* Y string V2821 V2822 V2823)))) (if (shen.pvar? V2712) (do (shen.bindv V2712 string V2822) (let Result (do (shen.incinfs) (shen.th* X string V2821 V2822 (freeze (shen.th* Y string V2821 V2822 V2823)))) (do (shen.unbindv V2712 V2822) Result))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2713 (shen.lazyderef V2819 V2822) (if (cons? V2713) (let V2714 (shen.lazyderef (hd V2713) V2822) (if (= lambda V2714) (let V2715 (shen.lazyderef (tl V2713) V2822) (if (cons? V2715) (let X (hd V2715) (let V2716 (shen.lazyderef (tl V2715) V2822) (if (cons? V2716) (let Y (hd V2716) (let V2717 (shen.lazyderef (tl V2716) V2822) (if (= () V2717) (let V2718 (shen.lazyderef V2820 V2822) (if (cons? V2718) (let A (hd V2718) (let V2719 (shen.lazyderef (tl V2718) V2822) (if (cons? V2719) (let V2720 (shen.lazyderef (hd V2719) V2822) (if (= --> V2720) (let V2721 (shen.lazyderef (tl V2719) V2822) (if (cons? V2721) (let B (hd V2721) (let V2722 (shen.lazyderef (tl V2721) V2822) (if (= () V2722) (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (if (shen.pvar? V2722) (do (shen.bindv V2722 () V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2722 V2822) Result))) false)))) (if (shen.pvar? V2721) (let B (shen.newpv V2822) (do (shen.bindv V2721 (cons B ()) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2721 V2822) Result)))) false))) (if (shen.pvar? V2720) (do (shen.bindv V2720 --> V2822) (let Result (let V2723 (shen.lazyderef (tl V2719) V2822) (if (cons? V2723) (let B (hd V2723) (let V2724 (shen.lazyderef (tl V2723) V2822) (if (= () V2724) (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (if (shen.pvar? V2724) (do (shen.bindv V2724 () V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2724 V2822) Result))) false)))) (if (shen.pvar? V2723) (let B (shen.newpv V2822) (do (shen.bindv V2723 (cons B ()) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2723 V2822) Result)))) false))) (do (shen.unbindv V2720 V2822) Result))) false))) (if (shen.pvar? V2719) (let B (shen.newpv V2822) (do (shen.bindv V2719 (cons --> (cons B ())) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2719 V2822) Result)))) false)))) (if (shen.pvar? V2718) (let A (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.bindv V2718 (cons A (cons --> (cons B ()))) V2822) (let Result (let Z (shen.newpv V2822) (let X&& (shen.newpv V2822) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind Z (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Y V2822)) V2822 (freeze (shen.th* Z B (cons (cons X&& (cons : (cons A ()))) V2821) V2822 V2823)))))))))) (do (shen.unbindv V2718 V2822) Result))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2725 (shen.lazyderef V2819 V2822) (if (cons? V2725) (let V2726 (shen.lazyderef (hd V2725) V2822) (if (= let V2726) (let V2727 (shen.lazyderef (tl V2725) V2822) (if (cons? V2727) (let X (hd V2727) (let V2728 (shen.lazyderef (tl V2727) V2822) (if (cons? V2728) (let Y (hd V2728) (let V2729 (shen.lazyderef (tl V2728) V2822) (if (cons? V2729) (let Z (hd V2729) (let V2730 (shen.lazyderef (tl V2729) V2822) (if (= () V2730) (let W (shen.newpv V2822) (let X&& (shen.newpv V2822) (let B (shen.newpv V2822) (do (shen.incinfs) (shen.th* Y B V2821 V2822 (freeze (bind X&& (shen.placeholder) V2822 (freeze (bind W (shen.ebr (shen.lazyderef X&& V2822) (shen.lazyderef X V2822) (shen.lazyderef Z V2822)) V2822 (freeze (shen.th* W V2820 (cons (cons X&& (cons : (cons B ()))) V2821) V2822 V2823))))))))))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2731 (shen.lazyderef V2819 V2822) (if (cons? V2731) (let V2732 (shen.lazyderef (hd V2731) V2822) (if (= open V2732) (let V2733 (shen.lazyderef (tl V2731) V2822) (if (cons? V2733) (let FileName (hd V2733) (let V2734 (shen.lazyderef (tl V2733) V2822) (if (cons? V2734) (let Direction2664 (hd V2734) (let V2735 (shen.lazyderef (tl V2734) V2822) (if (= () V2735) (let V2736 (shen.lazyderef V2820 V2822) (if (cons? V2736) (let V2737 (shen.lazyderef (hd V2736) V2822) (if (= stream V2737) (let V2738 (shen.lazyderef (tl V2736) V2822) (if (cons? V2738) (let Direction (hd V2738) (let V2739 (shen.lazyderef (tl V2738) V2822) (if (= () V2739) (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (if (shen.pvar? V2739) (do (shen.bindv V2739 () V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2739 V2822) Result))) false)))) (if (shen.pvar? V2738) (let Direction (shen.newpv V2822) (do (shen.bindv V2738 (cons Direction ()) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2738 V2822) Result)))) false))) (if (shen.pvar? V2737) (do (shen.bindv V2737 stream V2822) (let Result (let V2740 (shen.lazyderef (tl V2736) V2822) (if (cons? V2740) (let Direction (hd V2740) (let V2741 (shen.lazyderef (tl V2740) V2822) (if (= () V2741) (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (if (shen.pvar? V2741) (do (shen.bindv V2741 () V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2741 V2822) Result))) false)))) (if (shen.pvar? V2740) (let Direction (shen.newpv V2822) (do (shen.bindv V2740 (cons Direction ()) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2740 V2822) Result)))) false))) (do (shen.unbindv V2737 V2822) Result))) false))) (if (shen.pvar? V2736) (let Direction (shen.newpv V2822) (do (shen.bindv V2736 (cons stream (cons Direction ())) V2822) (let Result (do (shen.incinfs) (unify! Direction Direction2664 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* FileName string V2821 V2822 V2823)))))) (do (shen.unbindv V2736 V2822) Result)))) false))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2742 (shen.lazyderef V2819 V2822) (if (cons? V2742) (let V2743 (shen.lazyderef (hd V2742) V2822) (if (= type V2743) (let V2744 (shen.lazyderef (tl V2742) V2822) (if (cons? V2744) (let X (hd V2744) (let V2745 (shen.lazyderef (tl V2744) V2822) (if (cons? V2745) (let A (hd V2745) (let V2746 (shen.lazyderef (tl V2745) V2822) (if (= () V2746) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (unify A V2820 V2822 (freeze (shen.th* X A V2821 V2822 V2823)))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2747 (shen.lazyderef V2819 V2822) (if (cons? V2747) (let V2748 (shen.lazyderef (hd V2747) V2822) (if (= input+ V2748) (let V2749 (shen.lazyderef (tl V2747) V2822) (if (cons? V2749) (let A (hd V2749) (let V2750 (shen.lazyderef (tl V2749) V2822) (if (cons? V2750) (let Stream (hd V2750) (let V2751 (shen.lazyderef (tl V2750) V2822) (if (= () V2751) (let C (shen.newpv V2822) (do (shen.incinfs) (bind C (shen.demodulate (shen.lazyderef A V2822)) V2822 (freeze (unify V2820 C V2822 (freeze (shen.th* Stream (cons stream (cons in ())) V2821 V2822 V2823))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2752 (shen.lazyderef V2819 V2822) (if (cons? V2752) (let V2753 (shen.lazyderef (hd V2752) V2822) (if (= set V2753) (let V2754 (shen.lazyderef (tl V2752) V2822) (if (cons? V2754) (let Var (hd V2754) (let V2755 (shen.lazyderef (tl V2754) V2822) (if (cons? V2755) (let Val (hd V2755) (let V2756 (shen.lazyderef (tl V2755) V2822) (if (= () V2756) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (shen.th* Var symbol V2821 V2822 (freeze (cut Throwcontrol V2822 (freeze (shen.th* (cons value (cons Var ())) V2820 V2821 V2822 (freeze (shen.th* Val V2820 V2821 V2822 V2823)))))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2757 (shen.lazyderef V2819 V2822) (if (cons? V2757) (let V2758 (shen.lazyderef (hd V2757) V2822) (if (= fail V2758) (let V2759 (shen.lazyderef (tl V2757) V2822) (if (= () V2759) (let V2760 (shen.lazyderef V2820 V2822) (if (= symbol V2760) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2760) (do (shen.bindv V2760 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2760 V2822) Result))) false))) false)) false)) false)) (if (= Case false) (let Case (let NewHyp (shen.newpv V2822) (do (shen.incinfs) (shen.t*-hyps V2821 NewHyp V2822 (freeze (shen.th* V2819 V2820 NewHyp V2822 V2823))))) (if (= Case false) (let Case (let V2761 (shen.lazyderef V2819 V2822) (if (cons? V2761) (let V2762 (shen.lazyderef (hd V2761) V2822) (if (= define V2762) (let V2763 (shen.lazyderef (tl V2761) V2822) (if (cons? V2763) (let F (hd V2763) (let X (tl V2763) (do (shen.incinfs) (cut Throwcontrol V2822 (freeze (shen.t*-def (cons define (cons F X)) V2820 V2821 V2822 V2823)))))) false)) false)) false)) (if (= Case false) (let Case (let V2764 (shen.lazyderef V2819 V2822) (if (cons? V2764) (let V2765 (shen.lazyderef (hd V2764) V2822) (if (= defmacro V2765) (let V2766 (shen.lazyderef V2820 V2822) (if (= unit V2766) (do (shen.incinfs) (cut Throwcontrol V2822 V2823)) (if (shen.pvar? V2766) (do (shen.bindv V2766 unit V2822) (let Result (do (shen.incinfs) (cut Throwcontrol V2822 V2823)) (do (shen.unbindv V2766 V2822) Result))) false))) false)) false)) (if (= Case false) (let Case (let V2767 (shen.lazyderef V2819 V2822) (if (cons? V2767) (let V2768 (shen.lazyderef (hd V2767) V2822) (if (= shen.process-datatype V2768) (let V2769 (shen.lazyderef V2820 V2822) (if (= symbol V2769) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2769) (do (shen.bindv V2769 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2769 V2822) Result))) false))) false)) false)) (if (= Case false) (let Case (let V2770 (shen.lazyderef V2819 V2822) (if (cons? V2770) (let V2771 (shen.lazyderef (hd V2770) V2822) (if (= shen.synonyms-help V2771) (let V2772 (shen.lazyderef V2820 V2822) (if (= symbol V2772) (do (shen.incinfs) (thaw V2823)) (if (shen.pvar? V2772) (do (shen.bindv V2772 symbol V2822) (let Result (do (shen.incinfs) (thaw V2823)) (do (shen.unbindv V2772 V2822) Result))) false))) false)) false)) (if (= Case false) (let Datatypes (shen.newpv V2822) (do (shen.incinfs) (bind Datatypes (value shen.*datatypes*) V2822 (freeze (shen.udefs* (cons V2819 (cons : (cons V2820 ()))) V2821 Datatypes V2822 V2823))))) Case)) 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 (V2824 V2825 V2826 V2827) (let Case (let V2579 (shen.lazyderef V2824 V2826) (if (cons? V2579) (let V2580 (shen.lazyderef (hd V2579) V2826) (if (cons? V2580) (let V2581 (shen.lazyderef (hd V2580) V2826) (if (cons? V2581) (let V2582 (shen.lazyderef (hd V2581) V2826) (if (= cons V2582) (let V2583 (shen.lazyderef (tl V2581) V2826) (if (cons? V2583) (let X (hd V2583) (let V2584 (shen.lazyderef (tl V2583) V2826) (if (cons? V2584) (let Y (hd V2584) (let V2585 (shen.lazyderef (tl V2584) V2826) (if (= () V2585) (let V2586 (shen.lazyderef (tl V2580) V2826) (if (cons? V2586) (let V2587 (shen.lazyderef (hd V2586) V2826) (if (= : V2587) (let V2588 (shen.lazyderef (tl V2586) V2826) (if (cons? V2588) (let V2589 (shen.lazyderef (hd V2588) V2826) (if (cons? V2589) (let V2590 (shen.lazyderef (hd V2589) V2826) (if (= list V2590) (let V2591 (shen.lazyderef (tl V2589) V2826) (if (cons? V2591) (let A (hd V2591) (let V2592 (shen.lazyderef (tl V2591) V2826) (if (= () V2592) (let V2593 (shen.lazyderef (tl V2588) V2826) (if (= () V2593) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2593) (do (shen.bindv V2593 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2593 V2826) Result))) false))) (if (shen.pvar? V2592) (do (shen.bindv V2592 () V2826) (let Result (let V2594 (shen.lazyderef (tl V2588) V2826) (if (= () V2594) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2594) (do (shen.bindv V2594 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2594 V2826) Result))) false))) (do (shen.unbindv V2592 V2826) Result))) false)))) (if (shen.pvar? V2591) (let A (shen.newpv V2826) (do (shen.bindv V2591 (cons A ()) V2826) (let Result (let V2595 (shen.lazyderef (tl V2588) V2826) (if (= () V2595) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2595) (do (shen.bindv V2595 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2595 V2826) Result))) false))) (do (shen.unbindv V2591 V2826) Result)))) false))) (if (shen.pvar? V2590) (do (shen.bindv V2590 list V2826) (let Result (let V2596 (shen.lazyderef (tl V2589) V2826) (if (cons? V2596) (let A (hd V2596) (let V2597 (shen.lazyderef (tl V2596) V2826) (if (= () V2597) (let V2598 (shen.lazyderef (tl V2588) V2826) (if (= () V2598) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2598) (do (shen.bindv V2598 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2598 V2826) Result))) false))) (if (shen.pvar? V2597) (do (shen.bindv V2597 () V2826) (let Result (let V2599 (shen.lazyderef (tl V2588) V2826) (if (= () V2599) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2599) (do (shen.bindv V2599 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2599 V2826) Result))) false))) (do (shen.unbindv V2597 V2826) Result))) false)))) (if (shen.pvar? V2596) (let A (shen.newpv V2826) (do (shen.bindv V2596 (cons A ()) V2826) (let Result (let V2600 (shen.lazyderef (tl V2588) V2826) (if (= () V2600) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2600) (do (shen.bindv V2600 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2600 V2826) Result))) false))) (do (shen.unbindv V2596 V2826) Result)))) false))) (do (shen.unbindv V2590 V2826) Result))) false))) (if (shen.pvar? V2589) (let A (shen.newpv V2826) (do (shen.bindv V2589 (cons list (cons A ())) V2826) (let Result (let V2601 (shen.lazyderef (tl V2588) V2826) (if (= () V2601) (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2601) (do (shen.bindv V2601 () V2826) (let Result (let Hyp (tl V2579) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons list (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2601 V2826) Result))) false))) (do (shen.unbindv V2589 V2826) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2602 (shen.lazyderef V2824 V2826) (if (cons? V2602) (let V2603 (shen.lazyderef (hd V2602) V2826) (if (cons? V2603) (let V2604 (shen.lazyderef (hd V2603) V2826) (if (cons? V2604) (let V2605 (shen.lazyderef (hd V2604) V2826) (if (= @p V2605) (let V2606 (shen.lazyderef (tl V2604) V2826) (if (cons? V2606) (let X (hd V2606) (let V2607 (shen.lazyderef (tl V2606) V2826) (if (cons? V2607) (let Y (hd V2607) (let V2608 (shen.lazyderef (tl V2607) V2826) (if (= () V2608) (let V2609 (shen.lazyderef (tl V2603) V2826) (if (cons? V2609) (let V2610 (shen.lazyderef (hd V2609) V2826) (if (= : V2610) (let V2611 (shen.lazyderef (tl V2609) V2826) (if (cons? V2611) (let V2612 (shen.lazyderef (hd V2611) V2826) (if (cons? V2612) (let A (hd V2612) (let V2613 (shen.lazyderef (tl V2612) V2826) (if (cons? V2613) (let V2614 (shen.lazyderef (hd V2613) V2826) (if (= * V2614) (let V2615 (shen.lazyderef (tl V2613) V2826) (if (cons? V2615) (let B (hd V2615) (let V2616 (shen.lazyderef (tl V2615) V2826) (if (= () V2616) (let V2617 (shen.lazyderef (tl V2611) V2826) (if (= () V2617) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2617) (do (shen.bindv V2617 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2617 V2826) Result))) false))) (if (shen.pvar? V2616) (do (shen.bindv V2616 () V2826) (let Result (let V2618 (shen.lazyderef (tl V2611) V2826) (if (= () V2618) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2618) (do (shen.bindv V2618 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2618 V2826) Result))) false))) (do (shen.unbindv V2616 V2826) Result))) false)))) (if (shen.pvar? V2615) (let B (shen.newpv V2826) (do (shen.bindv V2615 (cons B ()) V2826) (let Result (let V2619 (shen.lazyderef (tl V2611) V2826) (if (= () V2619) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2619) (do (shen.bindv V2619 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2619 V2826) Result))) false))) (do (shen.unbindv V2615 V2826) Result)))) false))) (if (shen.pvar? V2614) (do (shen.bindv V2614 * V2826) (let Result (let V2620 (shen.lazyderef (tl V2613) V2826) (if (cons? V2620) (let B (hd V2620) (let V2621 (shen.lazyderef (tl V2620) V2826) (if (= () V2621) (let V2622 (shen.lazyderef (tl V2611) V2826) (if (= () V2622) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2622) (do (shen.bindv V2622 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2622 V2826) Result))) false))) (if (shen.pvar? V2621) (do (shen.bindv V2621 () V2826) (let Result (let V2623 (shen.lazyderef (tl V2611) V2826) (if (= () V2623) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2623) (do (shen.bindv V2623 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2623 V2826) Result))) false))) (do (shen.unbindv V2621 V2826) Result))) false)))) (if (shen.pvar? V2620) (let B (shen.newpv V2826) (do (shen.bindv V2620 (cons B ()) V2826) (let Result (let V2624 (shen.lazyderef (tl V2611) V2826) (if (= () V2624) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2624) (do (shen.bindv V2624 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2624 V2826) Result))) false))) (do (shen.unbindv V2620 V2826) Result)))) false))) (do (shen.unbindv V2614 V2826) Result))) false))) (if (shen.pvar? V2613) (let B (shen.newpv V2826) (do (shen.bindv V2613 (cons * (cons B ())) V2826) (let Result (let V2625 (shen.lazyderef (tl V2611) V2826) (if (= () V2625) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2625) (do (shen.bindv V2625 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2625 V2826) Result))) false))) (do (shen.unbindv V2613 V2826) Result)))) false)))) (if (shen.pvar? V2612) (let A (shen.newpv V2826) (let B (shen.newpv V2826) (do (shen.bindv V2612 (cons A (cons * (cons B ()))) V2826) (let Result (let V2626 (shen.lazyderef (tl V2611) V2826) (if (= () V2626) (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2626) (do (shen.bindv V2626 () V2826) (let Result (let Hyp (tl V2602) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (shen.lazyderef B V2826) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2626 V2826) Result))) false))) (do (shen.unbindv V2612 V2826) Result))))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2627 (shen.lazyderef V2824 V2826) (if (cons? V2627) (let V2628 (shen.lazyderef (hd V2627) V2826) (if (cons? V2628) (let V2629 (shen.lazyderef (hd V2628) V2826) (if (cons? V2629) (let V2630 (shen.lazyderef (hd V2629) V2826) (if (= @v V2630) (let V2631 (shen.lazyderef (tl V2629) V2826) (if (cons? V2631) (let X (hd V2631) (let V2632 (shen.lazyderef (tl V2631) V2826) (if (cons? V2632) (let Y (hd V2632) (let V2633 (shen.lazyderef (tl V2632) V2826) (if (= () V2633) (let V2634 (shen.lazyderef (tl V2628) V2826) (if (cons? V2634) (let V2635 (shen.lazyderef (hd V2634) V2826) (if (= : V2635) (let V2636 (shen.lazyderef (tl V2634) V2826) (if (cons? V2636) (let V2637 (shen.lazyderef (hd V2636) V2826) (if (cons? V2637) (let V2638 (shen.lazyderef (hd V2637) V2826) (if (= vector V2638) (let V2639 (shen.lazyderef (tl V2637) V2826) (if (cons? V2639) (let A (hd V2639) (let V2640 (shen.lazyderef (tl V2639) V2826) (if (= () V2640) (let V2641 (shen.lazyderef (tl V2636) V2826) (if (= () V2641) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2641) (do (shen.bindv V2641 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2641 V2826) Result))) false))) (if (shen.pvar? V2640) (do (shen.bindv V2640 () V2826) (let Result (let V2642 (shen.lazyderef (tl V2636) V2826) (if (= () V2642) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2642) (do (shen.bindv V2642 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2642 V2826) Result))) false))) (do (shen.unbindv V2640 V2826) Result))) false)))) (if (shen.pvar? V2639) (let A (shen.newpv V2826) (do (shen.bindv V2639 (cons A ()) V2826) (let Result (let V2643 (shen.lazyderef (tl V2636) V2826) (if (= () V2643) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2643) (do (shen.bindv V2643 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2643 V2826) Result))) false))) (do (shen.unbindv V2639 V2826) Result)))) false))) (if (shen.pvar? V2638) (do (shen.bindv V2638 vector V2826) (let Result (let V2644 (shen.lazyderef (tl V2637) V2826) (if (cons? V2644) (let A (hd V2644) (let V2645 (shen.lazyderef (tl V2644) V2826) (if (= () V2645) (let V2646 (shen.lazyderef (tl V2636) V2826) (if (= () V2646) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2646) (do (shen.bindv V2646 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2646 V2826) Result))) false))) (if (shen.pvar? V2645) (do (shen.bindv V2645 () V2826) (let Result (let V2647 (shen.lazyderef (tl V2636) V2826) (if (= () V2647) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2647) (do (shen.bindv V2647 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2647 V2826) Result))) false))) (do (shen.unbindv V2645 V2826) Result))) false)))) (if (shen.pvar? V2644) (let A (shen.newpv V2826) (do (shen.bindv V2644 (cons A ()) V2826) (let Result (let V2648 (shen.lazyderef (tl V2636) V2826) (if (= () V2648) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2648) (do (shen.bindv V2648 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2648 V2826) Result))) false))) (do (shen.unbindv V2644 V2826) Result)))) false))) (do (shen.unbindv V2638 V2826) Result))) false))) (if (shen.pvar? V2637) (let A (shen.newpv V2826) (do (shen.bindv V2637 (cons vector (cons A ())) V2826) (let Result (let V2649 (shen.lazyderef (tl V2636) V2826) (if (= () V2649) (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2649) (do (shen.bindv V2649 () V2826) (let Result (let Hyp (tl V2627) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons (shen.lazyderef A V2826) ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons (cons vector (cons (shen.lazyderef A V2826) ())) ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2649 V2826) Result))) false))) (do (shen.unbindv V2637 V2826) Result)))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2650 (shen.lazyderef V2824 V2826) (if (cons? V2650) (let V2651 (shen.lazyderef (hd V2650) V2826) (if (cons? V2651) (let V2652 (shen.lazyderef (hd V2651) V2826) (if (cons? V2652) (let V2653 (shen.lazyderef (hd V2652) V2826) (if (= @s V2653) (let V2654 (shen.lazyderef (tl V2652) V2826) (if (cons? V2654) (let X (hd V2654) (let V2655 (shen.lazyderef (tl V2654) V2826) (if (cons? V2655) (let Y (hd V2655) (let V2656 (shen.lazyderef (tl V2655) V2826) (if (= () V2656) (let V2657 (shen.lazyderef (tl V2651) V2826) (if (cons? V2657) (let V2658 (shen.lazyderef (hd V2657) V2826) (if (= : V2658) (let V2659 (shen.lazyderef (tl V2657) V2826) (if (cons? V2659) (let V2660 (shen.lazyderef (hd V2659) V2826) (if (= string V2660) (let V2661 (shen.lazyderef (tl V2659) V2826) (if (= () V2661) (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2661) (do (shen.bindv V2661 () V2826) (let Result (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2661 V2826) Result))) false))) (if (shen.pvar? V2660) (do (shen.bindv V2660 string V2826) (let Result (let V2662 (shen.lazyderef (tl V2659) V2826) (if (= () V2662) (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (if (shen.pvar? V2662) (do (shen.bindv V2662 () V2826) (let Result (let Hyp (tl V2650) (do (shen.incinfs) (bind V2825 (cons (cons (shen.lazyderef X V2826) (cons : (cons string ()))) (cons (cons (shen.lazyderef Y V2826) (cons : (cons string ()))) (shen.lazyderef Hyp V2826))) V2826 V2827))) (do (shen.unbindv V2662 V2826) Result))) false))) (do (shen.unbindv V2660 V2826) Result))) false))) false)) false)) false)) false))) false))) false)) false)) false)) false)) false)) (if (= Case false) (let V2663 (shen.lazyderef V2824 V2826) (if (cons? V2663) (let X (hd V2663) (let Hyp (tl V2663) (let NewHyps (shen.newpv V2826) (do (shen.incinfs) (bind V2825 (cons (shen.lazyderef X V2826) (shen.lazyderef NewHyps V2826)) V2826 (freeze (shen.t*-hyps Hyp NewHyps V2826 V2827))))))) false)) Case)) Case)) Case)) Case)))
+
+(defun shen.show (V2840 V2841 V2842 V2843) (cond ((value shen.*spy*) (do (shen.line) (do (shen.show-p (shen.deref V2840 V2842)) (do (nl 1) (do (nl 1) (do (shen.show-assumptions (shen.deref V2841 V2842) 1) (do (shen.prhush "
+> " (stoutput)) (do (shen.pause-for-user) (thaw V2843))))))))) (true (thaw V2843))))
+
+(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 (V2844) (cond ((and (cons? V2844) (and (cons? (tl V2844)) (and (= : (hd (tl V2844))) (and (cons? (tl (tl V2844))) (= () (tl (tl (tl V2844)))))))) (shen.prhush (shen.app (hd V2844) (cn " : " (shen.app (hd (tl (tl V2844))) "" shen.r)) shen.r) (stoutput))) (true (shen.prhush (shen.app V2844 "" shen.r) (stoutput)))))
+
+(defun shen.show-assumptions (V2847 V2848) (cond ((= () V2847) shen.skip) ((cons? V2847) (do (shen.prhush (shen.app V2848 ". " shen.a) (stoutput)) (do (shen.show-p (hd V2847)) (do (nl 1) (shen.show-assumptions (tl V2847) (+ V2848 1)))))) (true (shen.sys-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? (V2849) (cons? (assoc V2849 (value shen.*signedfuncs*))))
+
+(defun shen.sigf (V2850) (concat shen.type-signature-of- V2850))
+
+(defun shen.placeholder () (gensym &&))
+
+(defun shen.base (V2851 V2852 V2853 V2854) (let Case (let V2566 (shen.lazyderef V2852 V2853) (if (= number V2566) (do (shen.incinfs) (fwhen (number? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2566) (do (shen.bindv V2566 number V2853) (let Result (do (shen.incinfs) (fwhen (number? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2566 V2853) Result))) false))) (if (= Case false) (let Case (let V2567 (shen.lazyderef V2852 V2853) (if (= boolean V2567) (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2567) (do (shen.bindv V2567 boolean V2853) (let Result (do (shen.incinfs) (fwhen (boolean? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2567 V2853) Result))) false))) (if (= Case false) (let Case (let V2568 (shen.lazyderef V2852 V2853) (if (= string V2568) (do (shen.incinfs) (fwhen (string? (shen.lazyderef V2851 V2853)) V2853 V2854)) (if (shen.pvar? V2568) (do (shen.bindv V2568 string V2853) (let Result (do (shen.incinfs) (fwhen (string? (shen.lazyderef V2851 V2853)) V2853 V2854)) (do (shen.unbindv V2568 V2853) Result))) false))) (if (= Case false) (let Case (let V2569 (shen.lazyderef V2852 V2853) (if (= symbol V2569) (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V2851 V2853)) V2853 (freeze (fwhen (not (shen.ue? (shen.lazyderef V2851 V2853))) V2853 V2854)))) (if (shen.pvar? V2569) (do (shen.bindv V2569 symbol V2853) (let Result (do (shen.incinfs) (fwhen (symbol? (shen.lazyderef V2851 V2853)) V2853 (freeze (fwhen (not (shen.ue? (shen.lazyderef V2851 V2853))) V2853 V2854)))) (do (shen.unbindv V2569 V2853) Result))) false))) (if (= Case false) (let V2570 (shen.lazyderef V2851 V2853) (if (= () V2570) (let V2571 (shen.lazyderef V2852 V2853) (if (cons? V2571) (let V2572 (shen.lazyderef (hd V2571) V2853) (if (= list V2572) (let V2573 (shen.lazyderef (tl V2571) V2853) (if (cons? V2573) (let A (hd V2573) (let V2574 (shen.lazyderef (tl V2573) V2853) (if (= () V2574) (do (shen.incinfs) (thaw V2854)) (if (shen.pvar? V2574) (do (shen.bindv V2574 () V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2574 V2853) Result))) false)))) (if (shen.pvar? V2573) (let A (shen.newpv V2853) (do (shen.bindv V2573 (cons A ()) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2573 V2853) Result)))) false))) (if (shen.pvar? V2572) (do (shen.bindv V2572 list V2853) (let Result (let V2575 (shen.lazyderef (tl V2571) V2853) (if (cons? V2575) (let A (hd V2575) (let V2576 (shen.lazyderef (tl V2575) V2853) (if (= () V2576) (do (shen.incinfs) (thaw V2854)) (if (shen.pvar? V2576) (do (shen.bindv V2576 () V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2576 V2853) Result))) false)))) (if (shen.pvar? V2575) (let A (shen.newpv V2853) (do (shen.bindv V2575 (cons A ()) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2575 V2853) Result)))) false))) (do (shen.unbindv V2572 V2853) Result))) false))) (if (shen.pvar? V2571) (let A (shen.newpv V2853) (do (shen.bindv V2571 (cons list (cons A ())) V2853) (let Result (do (shen.incinfs) (thaw V2854)) (do (shen.unbindv V2571 V2853) Result)))) false))) false)) Case)) Case)) Case)) Case)))
+
+(defun shen.by_hypothesis (V2855 V2856 V2857 V2858 V2859) (let Case (let V2557 (shen.lazyderef V2857 V2858) (if (cons? V2557) (let V2558 (shen.lazyderef (hd V2557) V2858) (if (cons? V2558) (let Y (hd V2558) (let V2559 (shen.lazyderef (tl V2558) V2858) (if (cons? V2559) (let V2560 (shen.lazyderef (hd V2559) V2858) (if (= : V2560) (let V2561 (shen.lazyderef (tl V2559) V2858) (if (cons? V2561) (let B (hd V2561) (let V2562 (shen.lazyderef (tl V2561) V2858) (if (= () V2562) (do (shen.incinfs) (identical V2855 Y V2858 (freeze (unify! V2856 B V2858 V2859)))) false))) false)) false)) false))) false)) false)) (if (= Case false) (let V2563 (shen.lazyderef V2857 V2858) (if (cons? V2563) (let Hyp (tl V2563) (do (shen.incinfs) (shen.by_hypothesis V2855 V2856 Hyp V2858 V2859))) false)) Case)))
+
+(defun shen.t*-def (V2860 V2861 V2862 V2863 V2864) (let V2551 (shen.lazyderef V2860 V2863) (if (cons? V2551) (let V2552 (shen.lazyderef (hd V2551) V2863) (if (= define V2552) (let V2553 (shen.lazyderef (tl V2551) V2863) (if (cons? V2553) (let F (hd V2553) (let X (tl V2553) (let E (shen.newpv V2863) (do (shen.incinfs) (shen.t*-defh (compile (lambda X2787 (shen.<sig+rules> X2787)) X (lambda E (if (cons? E) (simple-error (cn "parse error here: " (shen.app E "
+" shen.s))) (simple-error "parse error
+")))) F V2861 V2862 V2863 V2864))))) false)) false)) false)))
+
+(defun shen.t*-defh (V2865 V2866 V2867 V2868 V2869 V2870) (let V2547 (shen.lazyderef V2865 V2869) (if (cons? V2547) (let Sig (hd V2547) (let Rules (tl V2547) (do (shen.incinfs) (shen.t*-defhh Sig (shen.ue-sig Sig) V2866 V2867 V2868 Rules V2869 V2870)))) false)))
+
+(defun shen.t*-defhh (V2871 V2872 V2873 V2874 V2875 V2876 V2877 V2878) (do (shen.incinfs) (shen.t*-rules V2876 V2872 1 V2873 (cons (cons V2873 (cons : (cons V2872 ()))) V2875) V2877 (freeze (shen.memo V2873 V2871 V2874 V2877 V2878)))))
+
+(defun shen.memo (V2879 V2880 V2881 V2882 V2883) (let Jnk (shen.newpv V2882) (do (shen.incinfs) (unify! V2881 V2880 V2882 (freeze (bind Jnk (declare (shen.lazyderef V2879 V2882) (shen.lazyderef V2881 V2882)) V2882 V2883))))))
+
+(defun shen.<sig+rules> (V2888) (let Result (let Parse_shen.<signature> (shen.<signature> V2888) (if (not (= (fail) Parse_shen.<signature>)) (let Parse_shen.<rules> (shen.<rules> Parse_shen.<signature>) (if (not (= (fail) Parse_shen.<rules>)) (shen.pair (hd Parse_shen.<rules>) (cons (shen.hdtl Parse_shen.<signature>) (shen.hdtl Parse_shen.<rules>))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)))
+
+(defun shen.ue (V2889) (cond ((and (cons? V2889) (and (cons? (tl V2889)) (and (= () (tl (tl V2889))) (= (hd V2889) protect)))) V2889) ((cons? V2889) (map (lambda X2788 (shen.ue X2788)) V2889)) ((variable? V2889) (concat && V2889)) (true V2889)))
+
+(defun shen.ue-sig (V2890) (cond ((cons? V2890) (map (lambda X2789 (shen.ue-sig X2789)) V2890)) ((variable? V2890) (concat &&& V2890)) (true V2890)))
+
+(defun shen.ues (V2895) (cond ((shen.ue? V2895) (cons V2895 ())) ((cons? V2895) (union (shen.ues (hd V2895)) (shen.ues (tl V2895)))) (true ())))
+
+(defun shen.ue? (V2896) (and (symbol? V2896) (shen.ue-h? (str V2896))))
+
+(defun shen.ue-h? (V2903) (cond ((and (shen.+string? V2903) (and (= "&" (pos V2903 0)) (and (shen.+string? (tlstr V2903)) (= "&" (pos (tlstr V2903) 0))))) true) (true false)))
+
+(defun shen.t*-rules (V2904 V2905 V2906 V2907 V2908 V2909 V2910) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2522 (shen.lazyderef V2904 V2909) (if (= () V2522) (do (shen.incinfs) (thaw V2910)) false)) (if (= Case false) (let Case (let V2523 (shen.lazyderef V2904 V2909) (if (cons? V2523) (let V2524 (shen.lazyderef (hd V2523) V2909) (if (cons? V2524) (let V2525 (shen.lazyderef (hd V2524) V2909) (if (= () V2525) (let V2526 (shen.lazyderef (tl V2524) V2909) (if (cons? V2526) (let Action (hd V2526) (let V2527 (shen.lazyderef (tl V2526) V2909) (if (= () V2527) (let Rules (tl V2523) (let V2528 (shen.lazyderef V2905 V2909) (if (cons? V2528) (let V2529 (shen.lazyderef (hd V2528) V2909) (if (= --> V2529) (let V2530 (shen.lazyderef (tl V2528) V2909) (if (cons? V2530) (let A (hd V2530) (let V2531 (shen.lazyderef (tl V2530) V2909) (if (= () V2531) (do (shen.incinfs) (shen.t*-rule (cons () (cons (shen.ue Action) ())) A V2908 V2909 (freeze (cut Throwcontrol V2909 (freeze (shen.t*-rules Rules A (+ V2906 1) V2907 V2908 V2909 V2910)))))) false))) false)) false)) false))) false))) false)) false)) false)) false)) (if (= Case false) (let Case (let V2532 (shen.lazyderef V2904 V2909) (if (cons? V2532) (let Rule (hd V2532) (let Rules (tl V2532) (do (shen.incinfs) (shen.t*-rule (shen.ue Rule) V2905 V2908 V2909 (freeze (cut Throwcontrol V2909 (freeze (shen.t*-rules Rules V2905 (+ V2906 1) V2907 V2908 V2909 V2910)))))))) false)) (if (= Case false) (let Err (shen.newpv V2909) (do (shen.incinfs) (bind Err (simple-error (cn "type error in rule " (shen.app (shen.lazyderef V2906 V2909) (cn " of " (shen.app (shen.lazyderef V2907 V2909) "" shen.a)) shen.a))) V2909 V2910))) Case)) Case)) Case)))))
+
+(defun shen.t*-rule (V2911 V2912 V2913 V2914 V2915) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2504 (shen.lazyderef V2911 V2914) (if (cons? V2504) (let V2505 (shen.lazyderef (hd V2504) V2914) (if (= () V2505) (let V2506 (shen.lazyderef (tl V2504) V2914) (if (cons? V2506) (let Action (hd V2506) (let V2507 (shen.lazyderef (tl V2506) V2914) (if (= () V2507) (do (shen.incinfs) (cut Throwcontrol V2914 (freeze (shen.t*-action (shen.curry Action) V2912 V2913 V2914 V2915)))) false))) false)) false)) false)) (if (= Case false) (let V2508 (shen.lazyderef V2911 V2914) (if (cons? V2508) (let V2509 (shen.lazyderef (hd V2508) V2914) (if (cons? V2509) (let Pattern (hd V2509) (let Patterns (tl V2509) (let V2510 (shen.lazyderef (tl V2508) V2914) (if (cons? V2510) (let Action (hd V2510) (let V2511 (shen.lazyderef (tl V2510) V2914) (if (= () V2511) (let V2512 (shen.lazyderef V2912 V2914) (if (cons? V2512) (let A (hd V2512) (let V2513 (shen.lazyderef (tl V2512) V2914) (if (cons? V2513) (let V2514 (shen.lazyderef (hd V2513) V2914) (if (= --> V2514) (let V2515 (shen.lazyderef (tl V2513) V2914) (if (cons? V2515) (let B (hd V2515) (let V2516 (shen.lazyderef (tl V2515) V2914) (if (= () V2516) (do (shen.incinfs) (shen.t*-pattern Pattern A V2914 (freeze (cut Throwcontrol V2914 (freeze (shen.t*-rule (cons Patterns (cons Action ())) B (cons (cons Pattern (cons : (cons A ()))) V2913) V2914 V2915)))))) false))) false)) false)) false))) false)) false))) false)))) false)) false)) Case)))))
+
+(defun shen.t*-action (V2916 V2917 V2918 V2919 V2920) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Case (let V2481 (shen.lazyderef V2916 V2919) (if (cons? V2481) (let V2482 (shen.lazyderef (hd V2481) V2919) (if (= where V2482) (let V2483 (shen.lazyderef (tl V2481) V2919) (if (cons? V2483) (let P (hd V2483) (let V2484 (shen.lazyderef (tl V2483) V2919) (if (cons? V2484) (let Action (hd V2484) (let V2485 (shen.lazyderef (tl V2484) V2919) (if (= () V2485) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t* (cons P (cons : (cons boolean ()))) V2918 V2919 (freeze (cut Throwcontrol V2919 (freeze (shen.t*-action Action V2917 (cons (cons P (cons : (cons verified ()))) V2918) V2919 V2920)))))))) false))) false))) false)) false)) false)) (if (= Case false) (let Case (let V2486 (shen.lazyderef V2916 V2919) (if (cons? V2486) (let V2487 (shen.lazyderef (hd V2486) V2919) (if (= shen.choicepoint! V2487) (let V2488 (shen.lazyderef (tl V2486) V2919) (if (cons? V2488) (let V2489 (shen.lazyderef (hd V2488) V2919) (if (cons? V2489) (let V2490 (shen.lazyderef (hd V2489) V2919) (if (cons? V2490) (let V2491 (shen.lazyderef (hd V2490) V2919) (if (= fail-if V2491) (let V2492 (shen.lazyderef (tl V2490) V2919) (if (cons? V2492) (let F (hd V2492) (let V2493 (shen.lazyderef (tl V2492) V2919) (if (= () V2493) (let V2494 (shen.lazyderef (tl V2489) V2919) (if (cons? V2494) (let Action (hd V2494) (let V2495 (shen.lazyderef (tl V2494) V2919) (if (= () V2495) (let V2496 (shen.lazyderef (tl V2488) V2919) (if (= () V2496) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons F (cons Action ())) ())) (cons Action ()))) V2917 V2918 V2919 V2920)))) false)) false))) false)) false))) false)) false)) false)) false)) false)) false)) false)) (if (= Case false) (let Case (let V2497 (shen.lazyderef V2916 V2919) (if (cons? V2497) (let V2498 (shen.lazyderef (hd V2497) V2919) (if (= shen.choicepoint! V2498) (let V2499 (shen.lazyderef (tl V2497) V2919) (if (cons? V2499) (let Action (hd V2499) (let V2500 (shen.lazyderef (tl V2499) V2919) (if (= () V2500) (do (shen.incinfs) (cut Throwcontrol V2919 (freeze (shen.t*-action (cons where (cons (cons not (cons (cons (cons = (cons Action ())) (cons (cons fail ()) ())) ())) (cons Action ()))) V2917 V2918 V2919 V2920)))) false))) false)) false)) false)) (if (= Case false) (do (shen.incinfs) (shen.t* (cons V2916 (cons : (cons V2917 ()))) V2918 V2919 V2920)) Case)) Case)) Case)))))
+
+(defun shen.t*-pattern (V2921 V2922 V2923 V2924) (let Throwcontrol (shen.catchpoint) (shen.cutpoint Throwcontrol (let Hyp (shen.newpv V2923) (do (shen.incinfs) (shen.tms->hyp (shen.ues V2921) Hyp V2923 (freeze (cut Throwcontrol V2923 (freeze (shen.t* (cons V2921 (cons : (cons V2922 ()))) Hyp V2923 V2924))))))))))
+
+(defun shen.tms->hyp (V2925 V2926 V2927 V2928) (let Case (let V2465 (shen.lazyderef V2925 V2927) (if (= () V2465) (let V2466 (shen.lazyderef V2926 V2927) (if (= () V2466) (do (shen.incinfs) (thaw V2928)) (if (shen.pvar? V2466) (do (shen.bindv V2466 () V2927) (let Result (do (shen.incinfs) (thaw V2928)) (do (shen.unbindv V2466 V2927) Result))) false))) false)) (if (= Case false) (let V2467 (shen.lazyderef V2925 V2927) (if (cons? V2467) (let Tm2462 (hd V2467) (let Tms (tl V2467) (let V2468 (shen.lazyderef V2926 V2927) (if (cons? V2468) (let V2469 (shen.lazyderef (hd V2468) V2927) (if (cons? V2469) (let Tm (hd V2469) (let V2470 (shen.lazyderef (tl V2469) V2927) (if (cons? V2470) (let V2471 (shen.lazyderef (hd V2470) V2927) (if (= : V2471) (let V2472 (shen.lazyderef (tl V2470) V2927) (if (cons? V2472) (let A (hd V2472) (let V2473 (shen.lazyderef (tl V2472) V2927) (if (= () V2473) (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (if (shen.pvar? V2473) (do (shen.bindv V2473 () V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2473 V2927) Result))) false)))) (if (shen.pvar? V2472) (let A (shen.newpv V2927) (do (shen.bindv V2472 (cons A ()) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2472 V2927) Result)))) false))) (if (shen.pvar? V2471) (do (shen.bindv V2471 : V2927) (let Result (let V2474 (shen.lazyderef (tl V2470) V2927) (if (cons? V2474) (let A (hd V2474) (let V2475 (shen.lazyderef (tl V2474) V2927) (if (= () V2475) (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (if (shen.pvar? V2475) (do (shen.bindv V2475 () V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2475 V2927) Result))) false)))) (if (shen.pvar? V2474) (let A (shen.newpv V2927) (do (shen.bindv V2474 (cons A ()) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2474 V2927) Result)))) false))) (do (shen.unbindv V2471 V2927) Result))) false))) (if (shen.pvar? V2470) (let A (shen.newpv V2927) (do (shen.bindv V2470 (cons : (cons A ())) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2470 V2927) Result)))) false)))) (if (shen.pvar? V2469) (let Tm (shen.newpv V2927) (let A (shen.newpv V2927) (do (shen.bindv V2469 (cons Tm (cons : (cons A ()))) V2927) (let Result (let Hyp (tl V2468) (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928))))) (do (shen.unbindv V2469 V2927) Result))))) false))) (if (shen.pvar? V2468) (let Tm (shen.newpv V2927) (let A (shen.newpv V2927) (let Hyp (shen.newpv V2927) (do (shen.bindv V2468 (cons (cons Tm (cons : (cons A ()))) Hyp) V2927) (let Result (do (shen.incinfs) (unify! Tm Tm2462 V2927 (freeze (shen.tms->hyp Tms Hyp V2927 V2928)))) (do (shen.unbindv V2468 V2927) Result)))))) false))))) false)) Case)))
+
+(defun findall (V2929 V2930 V2931 V2932 V2933) (let B (shen.newpv V2932) (let A (shen.newpv V2932) (do (shen.incinfs) (bind A (gensym shen.a) V2932 (freeze (bind B (set (shen.lazyderef A V2932) ()) V2932 (freeze (shen.findallhelp V2929 V2930 V2931 A V2932 V2933)))))))))
+
+(defun shen.findallhelp (V2934 V2935 V2936 V2937 V2938 V2939) (let Case (do (shen.incinfs) (call V2935 V2938 (freeze (shen.remember V2937 V2934 V2938 (freeze (fwhen false V2938 V2939)))))) (if (= Case false) (do (shen.incinfs) (bind V2936 (value (shen.lazyderef V2937 V2938)) V2938 V2939)) Case)))
+
+(defun shen.remember (V2940 V2941 V2942 V2943) (let B (shen.newpv V2942) (do (shen.incinfs) (bind B (set (shen.deref V2940 V2942) (cons (shen.deref V2941 V2942) (value (shen.deref V2940 V2942)))) V2942 V2943))))
+
+
+