"Copyright (c) 2015, Mark Tarver\n\nAll rights reserved.\n\nRedistribution and use in source and binary forms, with or without\nmodification, are permitted provided that the following conditions are met:\n1. Redistributions of source code must retain the above copyright\n   notice, this list of conditions and the following disclaimer.\n2. Redistributions in binary form must reproduce the above copyright\n   notice, this list of conditions and the following disclaimer in the\n   documentation and/or other materials provided with the distribution.\n3. The name of Mark Tarver may not be used to endorse or promote products\n   derived from this software without specific prior written permission.\n\nTHIS SOFTWARE IS PROVIDED BY Mark Tarver ''AS IS'' AND ANY\nEXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED\nWARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE\nDISCLAIMED. IN NO EVENT SHALL Mark Tarver BE LIABLE FOR ANY\nDIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES\n(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;\nLOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND\nON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT\n(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS\nSOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
(begin (register-function-arity (quote shen.datatype-error) 1) (define (kl:shen.datatype-error V2519) (cond ((and (pair? V2519) (and (pair? (cdr V2519)) (null? (cdr (cdr V2519))))) (simple-error (string-append "datatype syntax error here:\n\n " (kl:shen.app (kl:shen.next-50 50 (car V2519)) "\n" (quote shen.a))))) (#t (kl:shen.f_error (quote shen.datatype-error))))) (quote shen.datatype-error))
(begin (register-function-arity (quote shen.<datatype-rules>) 1) (define (kl:shen.<datatype-rules> V2521) (let ((YaccParse (let ((Parse_shen.<datatype-rule> (kl:shen.<datatype-rule> V2521))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<datatype-rule>)) (let ((Parse_shen.<datatype-rules> (kl:shen.<datatype-rules> Parse_shen.<datatype-rule>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<datatype-rules>)) (kl:shen.pair (car Parse_shen.<datatype-rules>) (cons (kl:shen.hdtl Parse_shen.<datatype-rule>) (kl:shen.hdtl Parse_shen.<datatype-rules>))) (quote shen.fail!))) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_<e> (kl:<e> V2521))) (if (kl:not (eq? (quote shen.fail!) Parse_<e>)) (kl:shen.pair (car Parse_<e>) (quote ())) (quote shen.fail!))) YaccParse))) (quote shen.<datatype-rules>))
(begin (register-function-arity (quote shen.<datatype-rule>) 1) (define (kl:shen.<datatype-rule> V2523) (let ((YaccParse (let ((Parse_shen.<side-conditions> (kl:shen.<side-conditions> V2523))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<side-conditions>)) (let ((Parse_shen.<premises> (kl:shen.<premises> Parse_shen.<side-conditions>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<premises>)) (let ((Parse_shen.<singleunderline> (kl:shen.<singleunderline> Parse_shen.<premises>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<singleunderline>)) (let ((Parse_shen.<conclusion> (kl:shen.<conclusion> Parse_shen.<singleunderline>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<conclusion>)) (kl:shen.pair (car Parse_shen.<conclusion>) (kl:shen.sequent (quote shen.single) (cons (kl:shen.hdtl Parse_shen.<side-conditions>) (cons (kl:shen.hdtl Parse_shen.<premises>) (cons (kl:shen.hdtl Parse_shen.<conclusion>) (quote ())))))) (quote shen.fail!))) (quote shen.fail!))) (quote shen.fail!))) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_shen.<side-conditions> (kl:shen.<side-conditions> V2523))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<side-conditions>)) (let ((Parse_shen.<premises> (kl:shen.<premises> Parse_shen.<side-conditions>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<premises>)) (let ((Parse_shen.<doubleunderline> (kl:shen.<doubleunderline> Parse_shen.<premises>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<doubleunderline>)) (let ((Parse_shen.<conclusion> (kl:shen.<conclusion> Parse_shen.<doubleunderline>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<conclusion>)) (kl:shen.pair (car Parse_shen.<conclusion>) (kl:shen.sequent (quote shen.double) (cons (kl:shen.hdtl Parse_shen.<side-conditions>) (cons (kl:shen.hdtl Parse_shen.<premises>) (cons (kl:shen.hdtl Parse_shen.<conclusion>) (quote ())))))) (quote shen.fail!))) (quote shen.fail!))) (quote shen.fail!))) (quote shen.fail!))) YaccParse))) (quote shen.<datatype-rule>))
(begin (register-function-arity (quote shen.<side-conditions>) 1) (define (kl:shen.<side-conditions> V2525) (let ((YaccParse (let ((Parse_shen.<side-condition> (kl:shen.<side-condition> V2525))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<side-condition>)) (let ((Parse_shen.<side-conditions> (kl:shen.<side-conditions> Parse_shen.<side-condition>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<side-conditions>)) (kl:shen.pair (car Parse_shen.<side-conditions>) (cons (kl:shen.hdtl Parse_shen.<side-condition>) (kl:shen.hdtl Parse_shen.<side-conditions>))) (quote shen.fail!))) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_<e> (kl:<e> V2525))) (if (kl:not (eq? (quote shen.fail!) Parse_<e>)) (kl:shen.pair (car Parse_<e>) (quote ())) (quote shen.fail!))) YaccParse))) (quote shen.<side-conditions>))
(begin (register-function-arity (quote shen.<side-condition>) 1) (define (kl:shen.<side-condition> V2529) (let ((YaccParse (if (and (pair? (car V2529)) (eq? (quote if) (kl:shen.hdhd V2529))) (let ((NewStream2526 (kl:shen.pair (kl:shen.tlhd V2529) (kl:shen.hdtl V2529)))) (let ((Parse_shen.<expr> (kl:shen.<expr> NewStream2526))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<expr>)) (kl:shen.pair (car Parse_shen.<expr>) (cons (quote if) (cons (kl:shen.hdtl Parse_shen.<expr>) (quote ())))) (quote shen.fail!)))) (quote shen.fail!)))) (if (eq? YaccParse (quote shen.fail!)) (if (and (pair? (car V2529)) (eq? (quote let) (kl:shen.hdhd V2529))) (let ((NewStream2527 (kl:shen.pair (kl:shen.tlhd V2529) (kl:shen.hdtl V2529)))) (let ((Parse_shen.<variable?> (kl:shen.<variable?> NewStream2527))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<variable?>)) (let ((Parse_shen.<expr> (kl:shen.<expr> Parse_shen.<variable?>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<expr>)) (kl:shen.pair (car Parse_shen.<expr>) (cons (quote let) (cons (kl:shen.hdtl Parse_shen.<variable?>) (cons (kl:shen.hdtl Parse_shen.<expr>) (quote ()))))) (quote shen.fail!))) (quote shen.fail!)))) (quote shen.fail!)) YaccParse))) (quote shen.<side-condition>))
(begin (register-function-arity (quote shen.<variable?>) 1) (define (kl:shen.<variable?> V2531) (if (pair? (car V2531)) (let ((Parse_X (kl:shen.hdhd V2531))) (if (kl:variable? Parse_X) (kl:shen.pair (car (kl:shen.pair (kl:shen.tlhd V2531) (kl:shen.hdtl V2531))) Parse_X) (quote shen.fail!))) (quote shen.fail!))) (quote shen.<variable?>))
(begin (register-function-arity (quote shen.<expr>) 1) (define (kl:shen.<expr> V2533) (if (pair? (car V2533)) (let ((Parse_X (kl:shen.hdhd V2533))) (if (kl:not (or (kl:element? Parse_X (cons (quote >>) (cons (quote _scheme_sc_) (quote ())))) (or (assert-boolean (kl:shen.singleunderline? Parse_X)) (assert-boolean (kl:shen.doubleunderline? Parse_X))))) (kl:shen.pair (car (kl:shen.pair (kl:shen.tlhd V2533) (kl:shen.hdtl V2533))) (kl:shen.remove-bar Parse_X)) (quote shen.fail!))) (quote shen.fail!))) (quote shen.<expr>))
(begin (register-function-arity (quote shen.remove-bar) 1) (define (kl:shen.remove-bar V2535) (cond ((and (pair? V2535) (and (pair? (cdr V2535)) (and (pair? (cdr (cdr V2535))) (and (null? (cdr (cdr (cdr V2535)))) (eq? (car (cdr V2535)) (quote bar!)))))) (cons (car V2535) (car (cdr (cdr V2535))))) ((pair? V2535) (cons (kl:shen.remove-bar (car V2535)) (kl:shen.remove-bar (cdr V2535)))) (#t V2535))) (quote shen.remove-bar))
(begin (register-function-arity (quote shen.<premises>) 1) (define (kl:shen.<premises> V2537) (let ((YaccParse (let ((Parse_shen.<premise> (kl:shen.<premise> V2537))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<premise>)) (let ((Parse_shen.<semicolon-symbol> (kl:shen.<semicolon-symbol> Parse_shen.<premise>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<semicolon-symbol>)) (let ((Parse_shen.<premises> (kl:shen.<premises> Parse_shen.<semicolon-symbol>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<premises>)) (kl:shen.pair (car Parse_shen.<premises>) (cons (kl:shen.hdtl Parse_shen.<premise>) (kl:shen.hdtl Parse_shen.<premises>))) (quote shen.fail!))) (quote shen.fail!))) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_<e> (kl:<e> V2537))) (if (kl:not (eq? (quote shen.fail!) Parse_<e>)) (kl:shen.pair (car Parse_<e>) (quote ())) (quote shen.fail!))) YaccParse))) (quote shen.<premises>))
(begin (register-function-arity (quote shen.<semicolon-symbol>) 1) (define (kl:shen.<semicolon-symbol> V2539) (if (pair? (car V2539)) (let ((Parse_X (kl:shen.hdhd V2539))) (if (eq? Parse_X (quote _scheme_sc_)) (kl:shen.pair (car (kl:shen.pair (kl:shen.tlhd V2539) (kl:shen.hdtl V2539))) (quote shen.skip)) (quote shen.fail!))) (quote shen.fail!))) (quote shen.<semicolon-symbol>))
(begin (register-function-arity (quote shen.<premise>) 1) (define (kl:shen.<premise> V2543) (let ((YaccParse (if (and (pair? (car V2543)) (eq? (quote !) (kl:shen.hdhd V2543))) (let ((NewStream2540 (kl:shen.pair (kl:shen.tlhd V2543) (kl:shen.hdtl V2543)))) (kl:shen.pair (car NewStream2540) (quote !))) (quote shen.fail!)))) (if (eq? YaccParse (quote shen.fail!)) (let ((YaccParse (let ((Parse_shen.<formulae> (kl:shen.<formulae> V2543))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formulae>)) (if (and (pair? (car Parse_shen.<formulae>)) (eq? (quote >>) (kl:shen.hdhd Parse_shen.<formulae>))) (let ((NewStream2541 (kl:shen.pair (kl:shen.tlhd Parse_shen.<formulae>) (kl:shen.hdtl Parse_shen.<formulae>)))) (let ((Parse_shen.<formula> (kl:shen.<formula> NewStream2541))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formula>)) (kl:shen.pair (car Parse_shen.<formula>) (kl:shen.sequent (kl:shen.hdtl Parse_shen.<formulae>) (kl:shen.hdtl Parse_shen.<formula>))) (quote shen.fail!)))) (quote shen.fail!)) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_shen.<formula> (kl:shen.<formula> V2543))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formula>)) (kl:shen.pair (car Parse_shen.<formula>) (kl:shen.sequent (quote ()) (kl:shen.hdtl Parse_shen.<formula>))) (quote shen.fail!))) YaccParse)) YaccParse))) (quote shen.<premise>))
(begin (register-function-arity (quote shen.<conclusion>) 1) (define (kl:shen.<conclusion> V2546) (let ((YaccParse (let ((Parse_shen.<formulae> (kl:shen.<formulae> V2546))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formulae>)) (if (and (pair? (car Parse_shen.<formulae>)) (eq? (quote >>) (kl:shen.hdhd Parse_shen.<formulae>))) (let ((NewStream2544 (kl:shen.pair (kl:shen.tlhd Parse_shen.<formulae>) (kl:shen.hdtl Parse_shen.<formulae>)))) (let ((Parse_shen.<formula> (kl:shen.<formula> NewStream2544))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formula>)) (let ((Parse_shen.<semicolon-symbol> (kl:shen.<semicolon-symbol> Parse_shen.<formula>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<semicolon-symbol>)) (kl:shen.pair (car Parse_shen.<semicolon-symbol>) (kl:shen.sequent (kl:shen.hdtl Parse_shen.<formulae>) (kl:shen.hdtl Parse_shen.<formula>))) (quote shen.fail!))) (quote shen.fail!)))) (quote shen.fail!)) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_shen.<formula> (kl:shen.<formula> V2546))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formula>)) (let ((Parse_shen.<semicolon-symbol> (kl:shen.<semicolon-symbol> Parse_shen.<formula>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<semicolon-symbol>)) (kl:shen.pair (car Parse_shen.<semicolon-symbol>) (kl:shen.sequent (quote ()) (kl:shen.hdtl Parse_shen.<formula>))) (quote shen.fail!))) (quote shen.fail!))) YaccParse))) (quote shen.<conclusion>))
(begin (register-function-arity (quote shen.sequent) 2) (define (kl:shen.sequent V2549 V2550) (kl:_scheme_at_p V2549 V2550)) (quote shen.sequent))
(begin (register-function-arity (quote shen.<formulae>) 1) (define (kl:shen.<formulae> V2552) (let ((YaccParse (let ((Parse_shen.<formula> (kl:shen.<formula> V2552))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formula>)) (let ((Parse_shen.<comma-symbol> (kl:shen.<comma-symbol> Parse_shen.<formula>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<comma-symbol>)) (let ((Parse_shen.<formulae> (kl:shen.<formulae> Parse_shen.<comma-symbol>))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formulae>)) (kl:shen.pair (car Parse_shen.<formulae>) (cons (kl:shen.hdtl Parse_shen.<formula>) (kl:shen.hdtl Parse_shen.<formulae>))) (quote shen.fail!))) (quote shen.fail!))) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((YaccParse (let ((Parse_shen.<formula> (kl:shen.<formula> V2552))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<formula>)) (kl:shen.pair (car Parse_shen.<formula>) (cons (kl:shen.hdtl Parse_shen.<formula>) (quote ()))) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_<e> (kl:<e> V2552))) (if (kl:not (eq? (quote shen.fail!) Parse_<e>)) (kl:shen.pair (car Parse_<e>) (quote ())) (quote shen.fail!))) YaccParse)) YaccParse))) (quote shen.<formulae>))
(begin (register-function-arity (quote shen.<comma-symbol>) 1) (define (kl:shen.<comma-symbol> V2554) (if (pair? (car V2554)) (let ((Parse_X (kl:shen.hdhd V2554))) (if (kl:= Parse_X (kl:intern ",")) (kl:shen.pair (car (kl:shen.pair (kl:shen.tlhd V2554) (kl:shen.hdtl V2554))) (quote shen.skip)) (quote shen.fail!))) (quote shen.fail!))) (quote shen.<comma-symbol>))
(begin (register-function-arity (quote shen.<formula>) 1) (define (kl:shen.<formula> V2557) (let ((YaccParse (let ((Parse_shen.<expr> (kl:shen.<expr> V2557))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<expr>)) (if (and (pair? (car Parse_shen.<expr>)) (eq? (quote :) (kl:shen.hdhd Parse_shen.<expr>))) (let ((NewStream2555 (kl:shen.pair (kl:shen.tlhd Parse_shen.<expr>) (kl:shen.hdtl Parse_shen.<expr>)))) (let ((Parse_shen.<type> (kl:shen.<type> NewStream2555))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<type>)) (kl:shen.pair (car Parse_shen.<type>) (cons (kl:shen.curry (kl:shen.hdtl Parse_shen.<expr>)) (cons (quote :) (cons (kl:shen.demodulate (kl:shen.hdtl Parse_shen.<type>)) (quote ()))))) (quote shen.fail!)))) (quote shen.fail!)) (quote shen.fail!))))) (if (eq? YaccParse (quote shen.fail!)) (let ((Parse_shen.<expr> (kl:shen.<expr> V2557))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<expr>)) (kl:shen.pair (car Parse_shen.<expr>) (kl:shen.hdtl Parse_shen.<expr>)) (quote shen.fail!))) YaccParse))) (quote shen.<formula>))
(begin (register-function-arity (quote shen.<type>) 1) (define (kl:shen.<type> V2559) (let ((Parse_shen.<expr> (kl:shen.<expr> V2559))) (if (kl:not (eq? (quote shen.fail!) Parse_shen.<expr>)) (kl:shen.pair (car Parse_shen.<expr>) (kl:shen.curry-type (kl:shen.hdtl Parse_shen.<expr>))) (quote shen.fail!)))) (quote shen.<type>))
(begin (register-function-arity (quote shen.<doubleunderline>) 1) (define (kl:shen.<doubleunderline> V2561) (if (pair? (car V2561)) (let ((Parse_X (kl:shen.hdhd V2561))) (if (assert-boolean (kl:shen.doubleunderline? Parse_X)) (kl:shen.pair (car (kl:shen.pair (kl:shen.tlhd V2561) (kl:shen.hdtl V2561))) Parse_X) (quote shen.fail!))) (quote shen.fail!))) (quote shen.<doubleunderline>))
(begin (register-function-arity (quote shen.<singleunderline>) 1) (define (kl:shen.<singleunderline> V2563) (if (pair? (car V2563)) (let ((Parse_X (kl:shen.hdhd V2563))) (if (assert-boolean (kl:shen.singleunderline? Parse_X)) (kl:shen.pair (car (kl:shen.pair (kl:shen.tlhd V2563) (kl:shen.hdtl V2563))) Parse_X) (quote shen.fail!))) (quote shen.fail!))) (quote shen.<singleunderline>))
(begin (register-function-arity (quote shen.singleunderline?) 1) (define (kl:shen.singleunderline? V2565) (and (assert-boolean (symbol? V2565)) (assert-boolean (kl:shen.sh? (kl:str V2565))))) (quote shen.singleunderline?))
(begin (register-function-arity (quote shen.sh?) 1) (define (kl:shen.sh? V2567) (cond ((equal? "_" V2567) #t) (#t (and (equal? (make-string 1 (string-ref V2567 0)) "_") (assert-boolean (kl:shen.sh? (kl:tlstr V2567))))))) (quote shen.sh?))
(begin (register-function-arity (quote shen.doubleunderline?) 1) (define (kl:shen.doubleunderline? V2569) (and (assert-boolean (symbol? V2569)) (assert-boolean (kl:shen.dh? (kl:str V2569))))) (quote shen.doubleunderline?))
(begin (register-function-arity (quote shen.dh?) 1) (define (kl:shen.dh? V2571) (cond ((equal? "=" V2571) #t) (#t (and (equal? (make-string 1 (string-ref V2571 0)) "=") (assert-boolean (kl:shen.dh? (kl:tlstr V2571))))))) (quote shen.dh?))
(begin (register-function-arity (quote shen.process-datatype) 2) (define (kl:shen.process-datatype V2574 V2575) (kl:shen.remember-datatype (kl:shen.s-prolog (kl:shen.rules->horn-clauses V2574 V2575)))) (quote shen.process-datatype))
(begin (register-function-arity (quote shen.remember-datatype) 1) (define (kl:shen.remember-datatype V2581) (cond ((pair? V2581) (begin (kl:set (quote shen.*datatypes*) (kl:adjoin (car V2581) (kl:value (quote shen.*datatypes*)))) (begin (kl:set (quote shen.*alldatatypes*) (kl:adjoin (car V2581) (kl:value (quote shen.*alldatatypes*)))) (car V2581)))) (#t (kl:shen.f_error (quote shen.remember-datatype))))) (quote shen.remember-datatype))
(begin (register-function-arity (quote shen.rules->horn-clauses) 2) (define (kl:shen.rules->horn-clauses V2586 V2587) (cond ((null? V2587) (quote ())) ((and (pair? V2587) (and (kl:tuple? (car V2587)) (eq? (quote shen.single) (kl:fst (car V2587))))) (cons (kl:shen.rule->horn-clause V2586 (kl:snd (car V2587))) (kl:shen.rules->horn-clauses V2586 (cdr V2587)))) ((and (pair? V2587) (and (kl:tuple? (car V2587)) (eq? (quote shen.double) (kl:fst (car V2587))))) (kl:shen.rules->horn-clauses V2586 (kl:append (kl:shen.double->singles (kl:snd (car V2587))) (cdr V2587)))) (#t (kl:shen.f_error (quote shen.rules->horn-clauses))))) (quote shen.rules->horn-clauses))
(begin (register-function-arity (quote shen.double->singles) 1) (define (kl:shen.double->singles V2589) (cons (kl:shen.right-rule V2589) (cons (kl:shen.left-rule V2589) (quote ())))) (quote shen.double->singles))
(begin (register-function-arity (quote shen.right-rule) 1) (define (kl:shen.right-rule V2591) (kl:_scheme_at_p (quote shen.single) V2591)) (quote shen.right-rule))
(begin (register-function-arity (quote shen.left-rule) 1) (define (kl:shen.left-rule V2593) (cond ((and (pair? V2593) (and (pair? (cdr V2593)) (and (pair? (cdr (cdr V2593))) (and (kl:tuple? (car (cdr (cdr V2593)))) (and (null? (kl:fst (car (cdr (cdr V2593))))) (null? (cdr (cdr (cdr V2593))))))))) (let ((Q (kl:gensym (quote Qv)))) (let ((NewConclusion (kl:_scheme_at_p (cons (kl:snd (car (cdr (cdr V2593)))) (quote ())) Q))) (let ((NewPremises (cons (kl:_scheme_at_p (kl:map (lambda (X) (kl:shen.right->left X)) (car (cdr V2593))) Q) (quote ())))) (kl:_scheme_at_p (quote shen.single) (cons (car V2593) (cons NewPremises (cons NewConclusion (quote ()))))))))) (#t (kl:shen.f_error (quote shen.left-rule))))) (quote shen.left-rule))
(begin (register-function-arity (quote shen.right->left) 1) (define (kl:shen.right->left V2599) (cond ((and (kl:tuple? V2599) (null? (kl:fst V2599))) (kl:snd V2599)) (#t (simple-error "syntax error with ==========\n")))) (quote shen.right->left))
(begin (register-function-arity (quote shen.rule->horn-clause) 2) (define (kl:shen.rule->horn-clause V2602 V2603) (cond ((and (pair? V2603) (and (pair? (cdr V2603)) (and (pair? (cdr (cdr V2603))) (and (kl:tuple? (car (cdr (cdr V2603)))) (null? (cdr (cdr (cdr V2603)))))))) (cons (kl:shen.rule->horn-clause-head V2602 (kl:snd (car (cdr (cdr V2603))))) (cons (quote :-) (cons (kl:shen.rule->horn-clause-body (car V2603) (car (cdr V2603)) (kl:fst (car (cdr (cdr V2603))))) (quote ()))))) (#t (kl:shen.f_error (quote shen.rule->horn-clause))))) (quote shen.rule->horn-clause))
(begin (register-function-arity (quote shen.rule->horn-clause-head) 2) (define (kl:shen.rule->horn-clause-head V2606 V2607) (cons V2606 (cons (kl:shen.mode-ify V2607) (cons (quote Context_1957) (quote ()))))) (quote shen.rule->horn-clause-head))
(begin (register-function-arity (quote shen.mode-ify) 1) (define (kl:shen.mode-ify V2609) (cond ((and (pair? V2609) (and (pair? (cdr V2609)) (and (eq? (quote :) (car (cdr V2609))) (and (pair? (cdr (cdr V2609))) (null? (cdr (cdr (cdr V2609)))))))) (cons (quote mode) (cons (cons (car V2609) (cons (quote :) (cons (cons (quote mode) (cons (car (cdr (cdr V2609))) (cons (quote +) (quote ())))) (quote ())))) (cons (quote -) (quote ()))))) (#t V2609))) (quote shen.mode-ify))
(begin (register-function-arity (quote shen.rule->horn-clause-body) 3) (define (kl:shen.rule->horn-clause-body V2613 V2614 V2615) (let ((Variables (kl:map (lambda (X) (kl:shen.extract_vars X)) V2615))) (let ((Predicates (kl:map (lambda (X) (kl:gensym (quote shen.cl))) V2615))) (let ((SearchLiterals (kl:shen.construct-search-literals Predicates Variables (quote Context_1957) (quote Context1_1957)))) (let ((SearchClauses (kl:shen.construct-search-clauses Predicates V2615 Variables))) (let ((SideLiterals (kl:shen.construct-side-literals V2613))) (let ((PremissLiterals (kl:map (lambda (X) (kl:shen.construct-premiss-literal X (kl:empty? V2615))) V2614))) (kl:append SearchLiterals (kl:append SideLiterals PremissLiterals))))))))) (quote shen.rule->horn-clause-body))
(begin (register-function-arity (quote shen.construct-search-literals) 4) (define (kl:shen.construct-search-literals V2624 V2625 V2626 V2627) (cond ((and (null? V2624) (null? V2625)) (quote ())) (#t (kl:shen.csl-help V2624 V2625 V2626 V2627)))) (quote shen.construct-search-literals))
(begin (register-function-arity (quote shen.csl-help) 4) (define (kl:shen.csl-help V2634 V2635 V2636 V2637) (cond ((and (null? V2634) (null? V2635)) (cons (cons (quote bind) (cons (quote ContextOut_1957) (cons V2636 (quote ())))) (quote ()))) ((and (pair? V2634) (pair? V2635)) (cons (cons (car V2634) (cons V2636 (cons V2637 (car V2635)))) (kl:shen.csl-help (cdr V2634) (cdr V2635) V2637 (kl:gensym (quote Context))))) (#t (kl:shen.f_error (quote shen.csl-help))))) (quote shen.csl-help))
(begin (register-function-arity (quote shen.construct-search-clauses) 3) (define (kl:shen.construct-search-clauses V2641 V2642 V2643) (cond ((and (null? V2641) (and (null? V2642) (null? V2643))) (quote shen.skip)) ((and (pair? V2641) (and (pair? V2642) (pair? V2643))) (begin (kl:shen.construct-search-clause (car V2641) (car V2642) (car V2643)) (kl:shen.construct-search-clauses (cdr V2641) (cdr V2642) (cdr V2643)))) (#t (kl:shen.f_error (quote shen.construct-search-clauses))))) (quote shen.construct-search-clauses))
(begin (register-function-arity (quote shen.construct-search-clause) 3) (define (kl:shen.construct-search-clause V2647 V2648 V2649) (kl:shen.s-prolog (cons (kl:shen.construct-base-search-clause V2647 V2648 V2649) (cons (kl:shen.construct-recursive-search-clause V2647 V2648 V2649) (quote ()))))) (quote shen.construct-search-clause))
(begin (register-function-arity (quote shen.construct-base-search-clause) 3) (define (kl:shen.construct-base-search-clause V2653 V2654 V2655) (cons (cons V2653 (cons (cons (kl:shen.mode-ify V2654) (quote In_1957)) (cons (quote In_1957) V2655))) (cons (quote :-) (cons (quote ()) (quote ()))))) (quote shen.construct-base-search-clause))
(begin (register-function-arity (quote shen.construct-recursive-search-clause) 3) (define (kl:shen.construct-recursive-search-clause V2659 V2660 V2661) (cons (cons V2659 (cons (cons (quote Assumption_1957) (quote Assumptions_1957)) (cons (cons (quote Assumption_1957) (quote Out_1957)) V2661))) (cons (quote :-) (cons (cons (cons V2659 (cons (quote Assumptions_1957) (cons (quote Out_1957) V2661))) (quote ())) (quote ()))))) (quote shen.construct-recursive-search-clause))
(begin (register-function-arity (quote shen.construct-side-literals) 1) (define (kl:shen.construct-side-literals V2667) (cond ((null? V2667) (quote ())) ((and (pair? V2667) (and (pair? (car V2667)) (and (eq? (quote if) (car (car V2667))) (and (pair? (cdr (car V2667))) (null? (cdr (cdr (car V2667)))))))) (cons (cons (quote when) (cdr (car V2667))) (kl:shen.construct-side-literals (cdr V2667)))) ((and (pair? V2667) (and (pair? (car V2667)) (and (eq? (quote let) (car (car V2667))) (and (pair? (cdr (car V2667))) (and (pair? (cdr (cdr (car V2667)))) (null? (cdr (cdr (cdr (car V2667)))))))))) (cons (cons (quote is) (cdr (car V2667))) (kl:shen.construct-side-literals (cdr V2667)))) ((pair? V2667) (kl:shen.construct-side-literals (cdr V2667))) (#t (kl:shen.f_error (quote shen.construct-side-literals))))) (quote shen.construct-side-literals))
(begin (register-function-arity (quote shen.construct-premiss-literal) 2) (define (kl:shen.construct-premiss-literal V2674 V2675) (cond ((kl:tuple? V2674) (cons (quote shen.t*) (cons (kl:shen.recursive_cons_form (kl:snd V2674)) (cons (kl:shen.construct-context V2675 (kl:fst V2674)) (quote ()))))) ((eq? (quote !) V2674) (cons (quote cut) (cons (quote Throwcontrol) (quote ())))) (#t (kl:shen.f_error (quote shen.construct-premiss-literal))))) (quote shen.construct-premiss-literal))
(begin (register-function-arity (quote shen.construct-context) 2) (define (kl:shen.construct-context V2678 V2679) (cond ((and (kl:= #t V2678) (null? V2679)) (quote Context_1957)) ((and (kl:= #f V2678) (null? V2679)) (quote ContextOut_1957)) ((pair? V2679) (cons (quote cons) (cons (kl:shen.recursive_cons_form (car V2679)) (cons (kl:shen.construct-context V2678 (cdr V2679)) (quote ()))))) (#t (kl:shen.f_error (quote shen.construct-context))))) (quote shen.construct-context))
(begin (register-function-arity (quote shen.recursive_cons_form) 1) (define (kl:shen.recursive_cons_form V2681) (cond ((pair? V2681) (cons (quote cons) (cons (kl:shen.recursive_cons_form (car V2681)) (cons (kl:shen.recursive_cons_form (cdr V2681)) (quote ()))))) (#t V2681))) (quote shen.recursive_cons_form))
(begin (register-function-arity (quote preclude) 1) (define (kl:preclude V2683) (kl:shen.preclude-h (kl:map (lambda (X) (kl:shen.intern-type X)) V2683))) (quote preclude))
(begin (register-function-arity (quote shen.preclude-h) 1) (define (kl:shen.preclude-h V2685) (let ((FilterDatatypes (kl:set (quote shen.*datatypes*) (kl:difference (kl:value (quote shen.*datatypes*)) V2685)))) (kl:value (quote shen.*datatypes*)))) (quote shen.preclude-h))
(begin (register-function-arity (quote include) 1) (define (kl:include V2687) (kl:shen.include-h (kl:map (lambda (X) (kl:shen.intern-type X)) V2687))) (quote include))
(begin (register-function-arity (quote shen.include-h) 1) (define (kl:shen.include-h V2689) (let ((ValidTypes (kl:intersection V2689 (kl:value (quote shen.*alldatatypes*))))) (let ((NewDatatypes (kl:set (quote shen.*datatypes*) (kl:union ValidTypes (kl:value (quote shen.*datatypes*)))))) (kl:value (quote shen.*datatypes*))))) (quote shen.include-h))
(begin (register-function-arity (quote preclude-all-but) 1) (define (kl:preclude-all-but V2691) (kl:shen.preclude-h (kl:difference (kl:value (quote shen.*alldatatypes*)) (kl:map (lambda (X) (kl:shen.intern-type X)) V2691)))) (quote preclude-all-but))
(begin (register-function-arity (quote include-all-but) 1) (define (kl:include-all-but V2693) (kl:shen.include-h (kl:difference (kl:value (quote shen.*alldatatypes*)) (kl:map (lambda (X) (kl:shen.intern-type X)) V2693)))) (quote include-all-but))
(begin (register-function-arity (quote shen.synonyms-help) 1) (define (kl:shen.synonyms-help V2699) (cond ((null? V2699) (kl:shen.update-demodulation-function (kl:value (quote shen.*tc*)) (kl:mapcan (lambda (X) (kl:shen.demod-rule X)) (kl:value (quote shen.*synonyms*))))) ((and (pair? V2699) (pair? (cdr V2699))) (let ((Vs (kl:difference (kl:shen.extract_vars (car (cdr V2699))) (kl:shen.extract_vars (car V2699))))) (if (kl:empty? Vs) (begin (kl:shen.pushnew (cons (car V2699) (cons (car (cdr V2699)) (quote ()))) (quote shen.*synonyms*)) (kl:shen.synonyms-help (cdr (cdr V2699)))) (kl:shen.free_variable_warnings (car (cdr V2699)) Vs)))) (#t (simple-error "odd number of synonyms\n")))) (quote shen.synonyms-help))
(begin (register-function-arity (quote shen.pushnew) 2) (define (kl:shen.pushnew V2702 V2703) (if (kl:element? V2702 (kl:value V2703)) (kl:value V2703) (kl:set V2703 (cons V2702 (kl:value V2703))))) (quote shen.pushnew))
(begin (register-function-arity (quote shen.demod-rule) 1) (define (kl:shen.demod-rule V2705) (cond ((and (pair? V2705) (and (pair? (cdr V2705)) (null? (cdr (cdr V2705))))) (cons (kl:shen.rcons_form (car V2705)) (cons (quote ->) (cons (kl:shen.rcons_form (car (cdr V2705))) (quote ()))))) (#t (kl:shen.f_error (quote shen.demod-rule))))) (quote shen.demod-rule))
(begin (register-function-arity (quote shen.lambda-of-defun) 1) (define (kl:shen.lambda-of-defun V2711) (cond ((and (pair? V2711) (and (eq? (quote defun) (car V2711)) (and (pair? (cdr V2711)) (and (pair? (cdr (cdr V2711))) (and (pair? (car (cdr (cdr V2711)))) (and (null? (cdr (car (cdr (cdr V2711))))) (and (pair? (cdr (cdr (cdr V2711)))) (null? (cdr (cdr (cdr (cdr V2711)))))))))))) (kl:eval (cons (quote /.) (cons (car (car (cdr (cdr V2711)))) (cdr (cdr (cdr V2711))))))) (#t (kl:shen.f_error (quote shen.lambda-of-defun))))) (quote shen.lambda-of-defun))
(begin (register-function-arity (quote shen.update-demodulation-function) 2) (define (kl:shen.update-demodulation-function V2714 V2715) (begin (kl:tc (quote -)) (begin (kl:set (quote shen.*demodulation-function*) (kl:shen.lambda-of-defun (kl:shen.elim-def (cons (quote define) (cons (quote shen.demod) (kl:append V2715 (kl:shen.default-rule))))))) (begin (if (assert-boolean V2714) (kl:tc (quote +)) (quote shen.skip)) (quote synonyms))))) (quote shen.update-demodulation-function))
(begin (register-function-arity (quote shen.default-rule) 0) (define (kl:shen.default-rule) (cons (quote X) (cons (quote ->) (cons (quote X) (quote ()))))) (quote shen.default-rule))