shen/release/k_lambda/sequent.kl in shen-ruby-0.10.0 vs shen/release/k_lambda/sequent.kl in shen-ruby-0.11.0
- old
+ new
@@ -1,166 +1,166 @@
-"**********************************************************************************
-* 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.datatype-error (V1686) (cond ((and (cons? V1686) (and (cons? (tl V1686)) (= () (tl (tl V1686))))) (simple-error (cn "datatype syntax error here:
-
- " (shen.app (shen.next-50 50 (hd V1686)) "
-" shen.a)))) (true (shen.sys-error shen.datatype-error))))
-
-(defun shen.<datatype-rules> (V1691) (let Result (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1691) (if (not (= (fail) Parse_shen.<datatype-rule>)) (let Parse_shen.<datatype-rules> (shen.<datatype-rules> Parse_shen.<datatype-rule>) (if (not (= (fail) Parse_shen.<datatype-rules>)) (shen.pair (hd Parse_shen.<datatype-rules>) (cons (shen.hdtl Parse_shen.<datatype-rule>) (shen.hdtl Parse_shen.<datatype-rules>))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_<e> (<e> V1691) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
-
-(defun shen.<datatype-rule> (V1696) (let Result (let Parse_shen.<side-conditions> (shen.<side-conditions> V1696) (if (not (= (fail) Parse_shen.<side-conditions>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<side-conditions>) (if (not (= (fail) Parse_shen.<premises>)) (let Parse_shen.<singleunderline> (shen.<singleunderline> Parse_shen.<premises>) (if (not (= (fail) Parse_shen.<singleunderline>)) (let Parse_shen.<conclusion> (shen.<conclusion> Parse_shen.<singleunderline>) (if (not (= (fail) Parse_shen.<conclusion>)) (shen.pair (hd Parse_shen.<conclusion>) (shen.sequent shen.single (cons (shen.hdtl Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<conclusion>) ()))))) (fail))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<side-conditions> (shen.<side-conditions> V1696) (if (not (= (fail) Parse_shen.<side-conditions>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<side-conditions>) (if (not (= (fail) Parse_shen.<premises>)) (let Parse_shen.<doubleunderline> (shen.<doubleunderline> Parse_shen.<premises>) (if (not (= (fail) Parse_shen.<doubleunderline>)) (let Parse_shen.<conclusion> (shen.<conclusion> Parse_shen.<doubleunderline>) (if (not (= (fail) Parse_shen.<conclusion>)) (shen.pair (hd Parse_shen.<conclusion>) (shen.sequent shen.double (cons (shen.hdtl Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<conclusion>) ()))))) (fail))) (fail))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
-
-(defun shen.<side-conditions> (V1701) (let Result (let Parse_shen.<side-condition> (shen.<side-condition> V1701) (if (not (= (fail) Parse_shen.<side-condition>)) (let Parse_shen.<side-conditions> (shen.<side-conditions> Parse_shen.<side-condition>) (if (not (= (fail) Parse_shen.<side-conditions>)) (shen.pair (hd Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<side-condition>) (shen.hdtl Parse_shen.<side-conditions>))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_<e> (<e> V1701) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
-
-(defun shen.<side-condition> (V1706) (let Result (if (and (cons? (hd V1706)) (= if (hd (hd V1706)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1706)) (shen.hdtl V1706))) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (cons if (cons (shen.hdtl Parse_shen.<expr>) ()))) (fail))) (fail)) (if (= Result (fail)) (let Result (if (and (cons? (hd V1706)) (= let (hd (hd V1706)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1706)) (shen.hdtl V1706))) (if (not (= (fail) Parse_shen.<variable?>)) (let Parse_shen.<expr> (shen.<expr> Parse_shen.<variable?>) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (cons let (cons (shen.hdtl Parse_shen.<variable?>) (cons (shen.hdtl Parse_shen.<expr>) ())))) (fail))) (fail))) (fail)) (if (= Result (fail)) (fail) Result)) Result)))
-
-(defun shen.<variable?> (V1711) (let Result (if (cons? (hd V1711)) (let Parse_X (hd (hd V1711)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1711)) (shen.hdtl V1711))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
-
-(defun shen.<expr> (V1716) (let Result (if (cons? (hd V1716)) (let Parse_X (hd (hd V1716)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1716)) (shen.hdtl V1716))) (shen.remove-bar Parse_X)) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
-
-(defun shen.remove-bar (V1717) (cond ((and (cons? V1717) (and (cons? (tl V1717)) (and (cons? (tl (tl V1717))) (and (= () (tl (tl (tl V1717)))) (= (hd (tl V1717)) bar!))))) (cons (hd V1717) (hd (tl (tl V1717))))) ((cons? V1717) (cons (shen.remove-bar (hd V1717)) (shen.remove-bar (tl V1717)))) (true V1717)))
-
-(defun shen.<premises> (V1722) (let Result (let Parse_shen.<premise> (shen.<premise> V1722) (if (not (= (fail) Parse_shen.<premise>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<premise>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<semicolon-symbol>) (if (not (= (fail) Parse_shen.<premises>)) (shen.pair (hd Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<premise>) (shen.hdtl Parse_shen.<premises>))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_<e> (<e> V1722) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
-
-(defun shen.<semicolon-symbol> (V1727) (let Result (if (cons? (hd V1727)) (let Parse_X (hd (hd V1727)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1727)) (shen.hdtl V1727))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
-
-(defun shen.<premise> (V1732) (let Result (if (and (cons? (hd V1732)) (= ! (hd (hd V1732)))) (shen.pair (hd (shen.pair (tl (hd V1732)) (shen.hdtl V1732))) !) (fail)) (if (= Result (fail)) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1732) (if (not (= (fail) Parse_shen.<formulae>)) (if (and (cons? (hd Parse_shen.<formulae>)) (= >> (hd (hd Parse_shen.<formulae>)))) (let Parse_shen.<formula> (shen.<formula> (shen.pair (tl (hd Parse_shen.<formulae>)) (shen.hdtl Parse_shen.<formulae>))) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (shen.sequent (shen.hdtl Parse_shen.<formulae>) (shen.hdtl Parse_shen.<formula>))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<formula> (shen.<formula> V1732) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (shen.sequent () (shen.hdtl Parse_shen.<formula>))) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result)))
-
-(defun shen.<conclusion> (V1737) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1737) (if (not (= (fail) Parse_shen.<formulae>)) (if (and (cons? (hd Parse_shen.<formulae>)) (= >> (hd (hd Parse_shen.<formulae>)))) (let Parse_shen.<formula> (shen.<formula> (shen.pair (tl (hd Parse_shen.<formulae>)) (shen.hdtl Parse_shen.<formulae>))) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (shen.pair (hd Parse_shen.<semicolon-symbol>) (shen.sequent (shen.hdtl Parse_shen.<formulae>) (shen.hdtl Parse_shen.<formula>))) (fail))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<formula> (shen.<formula> V1737) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (shen.pair (hd Parse_shen.<semicolon-symbol>) (shen.sequent () (shen.hdtl Parse_shen.<formula>))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
-
-(defun shen.sequent (V1738 V1739) (@p V1738 V1739))
-
-(defun shen.<formulae> (V1744) (let Result (let Parse_shen.<formula> (shen.<formula> V1744) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<comma-symbol> (shen.<comma-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<comma-symbol>)) (let Parse_shen.<formulae> (shen.<formulae> Parse_shen.<comma-symbol>) (if (not (= (fail) Parse_shen.<formulae>)) (shen.pair (hd Parse_shen.<formulae>) (cons (shen.hdtl Parse_shen.<formula>) (shen.hdtl Parse_shen.<formulae>))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<formula> (shen.<formula> V1744) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (cons (shen.hdtl Parse_shen.<formula>) ())) (fail))) (if (= Result (fail)) (let Result (let Parse_<e> (<e> V1744) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result)))
-
-(defun shen.<comma-symbol> (V1749) (let Result (if (cons? (hd V1749)) (let Parse_X (hd (hd V1749)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1749)) (shen.hdtl V1749))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
-
-(defun shen.<formula> (V1754) (let Result (let Parse_shen.<expr> (shen.<expr> V1754) (if (not (= (fail) Parse_shen.<expr>)) (if (and (cons? (hd Parse_shen.<expr>)) (= : (hd (hd Parse_shen.<expr>)))) (let Parse_shen.<type> (shen.<type> (shen.pair (tl (hd Parse_shen.<expr>)) (shen.hdtl Parse_shen.<expr>))) (if (not (= (fail) Parse_shen.<type>)) (shen.pair (hd Parse_shen.<type>) (cons (shen.curry (shen.hdtl Parse_shen.<expr>)) (cons : (cons (shen.demodulate (shen.hdtl Parse_shen.<type>)) ())))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<expr> (shen.<expr> V1754) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.hdtl Parse_shen.<expr>)) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
-
-(defun shen.<type> (V1759) (let Result (let Parse_shen.<expr> (shen.<expr> V1759) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.curry-type (shen.hdtl Parse_shen.<expr>))) (fail))) (if (= Result (fail)) (fail) Result)))
-
-(defun shen.<doubleunderline> (V1764) (let Result (if (cons? (hd V1764)) (let Parse_X (hd (hd V1764)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1764)) (shen.hdtl V1764))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
-
-(defun shen.<singleunderline> (V1769) (let Result (if (cons? (hd V1769)) (let Parse_X (hd (hd V1769)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1769)) (shen.hdtl V1769))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
-
-(defun shen.singleunderline? (V1770) (and (symbol? V1770) (shen.sh? (str V1770))))
-
-(defun shen.sh? (V1771) (cond ((= "_" V1771) true) (true (and (= (pos V1771 0) "_") (shen.sh? (tlstr V1771))))))
-
-(defun shen.doubleunderline? (V1772) (and (symbol? V1772) (shen.dh? (str V1772))))
-
-(defun shen.dh? (V1773) (cond ((= "=" V1773) true) (true (and (= (pos V1773 0) "=") (shen.dh? (tlstr V1773))))))
-
-(defun shen.process-datatype (V1774 V1775) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1774 V1775))))
-
-(defun shen.remember-datatype (V1780) (cond ((cons? V1780) (do (set shen.*datatypes* (adjoin (hd V1780) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1780) (value shen.*alldatatypes*))) (hd V1780)))) (true (shen.sys-error shen.remember-datatype))))
-
-(defun shen.rules->horn-clauses (V1783 V1784) (cond ((= () V1784) ()) ((and (cons? V1784) (and (tuple? (hd V1784)) (= shen.single (fst (hd V1784))))) (cons (shen.rule->horn-clause V1783 (snd (hd V1784))) (shen.rules->horn-clauses V1783 (tl V1784)))) ((and (cons? V1784) (and (tuple? (hd V1784)) (= shen.double (fst (hd V1784))))) (shen.rules->horn-clauses V1783 (append (shen.double->singles (snd (hd V1784))) (tl V1784)))) (true (shen.sys-error shen.rules->horn-clauses))))
-
-(defun shen.double->singles (V1785) (cons (shen.right-rule V1785) (cons (shen.left-rule V1785) ())))
-
-(defun shen.right-rule (V1786) (@p shen.single V1786))
-
-(defun shen.left-rule (V1787) (cond ((and (cons? V1787) (and (cons? (tl V1787)) (and (cons? (tl (tl V1787))) (and (tuple? (hd (tl (tl V1787)))) (and (= () (fst (hd (tl (tl V1787))))) (= () (tl (tl (tl V1787))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1787)))) ()) Q) (let NewPremises (cons (@p (map (lambda X1675 (shen.right->left X1675)) (hd (tl V1787))) Q) ()) (@p shen.single (cons (hd V1787) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.sys-error shen.left-rule))))
-
-(defun shen.right->left (V1792) (cond ((and (tuple? V1792) (= () (fst V1792))) (snd V1792)) (true (simple-error "syntax error with ==========
-"))))
-
-(defun shen.rule->horn-clause (V1793 V1794) (cond ((and (cons? V1794) (and (cons? (tl V1794)) (and (cons? (tl (tl V1794))) (and (tuple? (hd (tl (tl V1794)))) (= () (tl (tl (tl V1794)))))))) (cons (shen.rule->horn-clause-head V1793 (snd (hd (tl (tl V1794))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1794) (hd (tl V1794)) (fst (hd (tl (tl V1794))))) ())))) (true (shen.sys-error shen.rule->horn-clause))))
-
-(defun shen.rule->horn-clause-head (V1795 V1796) (cons V1795 (cons (shen.mode-ify V1796) (cons Context_1957 ()))))
-
-(defun shen.mode-ify (V1797) (cond ((and (cons? V1797) (and (cons? (tl V1797)) (and (= : (hd (tl V1797))) (and (cons? (tl (tl V1797))) (= () (tl (tl (tl V1797)))))))) (cons mode (cons (cons (hd V1797) (cons : (cons (cons mode (cons (hd (tl (tl V1797))) (cons + ()))) ()))) (cons - ())))) (true V1797)))
-
-(defun shen.rule->horn-clause-body (V1798 V1799 V1800) (let Variables (map (lambda X1676 (shen.extract_vars X1676)) V1800) (let Predicates (map (lambda X (gensym shen.cl)) V1800) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1800 Variables) (let SideLiterals (shen.construct-side-literals V1798) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1800))) V1799) (append SearchLiterals (append SideLiterals PremissLiterals)))))))))
-
-(defun shen.construct-search-literals (V1805 V1806 V1807 V1808) (cond ((and (= () V1805) (= () V1806)) ()) (true (shen.csl-help V1805 V1806 V1807 V1808))))
-
-(defun shen.csl-help (V1811 V1812 V1813 V1814) (cond ((and (= () V1811) (= () V1812)) (cons (cons bind (cons ContextOut_1957 (cons V1813 ()))) ())) ((and (cons? V1811) (cons? V1812)) (cons (cons (hd V1811) (cons V1813 (cons V1814 (hd V1812)))) (shen.csl-help (tl V1811) (tl V1812) V1814 (gensym Context)))) (true (shen.sys-error shen.csl-help))))
-
-(defun shen.construct-search-clauses (V1815 V1816 V1817) (cond ((and (= () V1815) (and (= () V1816) (= () V1817))) shen.skip) ((and (cons? V1815) (and (cons? V1816) (cons? V1817))) (do (shen.construct-search-clause (hd V1815) (hd V1816) (hd V1817)) (shen.construct-search-clauses (tl V1815) (tl V1816) (tl V1817)))) (true (shen.sys-error shen.construct-search-clauses))))
-
-(defun shen.construct-search-clause (V1818 V1819 V1820) (shen.s-prolog (cons (shen.construct-base-search-clause V1818 V1819 V1820) (cons (shen.construct-recursive-search-clause V1818 V1819 V1820) ()))))
-
-(defun shen.construct-base-search-clause (V1821 V1822 V1823) (cons (cons V1821 (cons (cons (shen.mode-ify V1822) In_1957) (cons In_1957 V1823))) (cons :- (cons () ()))))
-
-(defun shen.construct-recursive-search-clause (V1824 V1825 V1826) (cons (cons V1824 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1826))) (cons :- (cons (cons (cons V1824 (cons Assumptions_1957 (cons Out_1957 V1826))) ()) ()))))
-
-(defun shen.construct-side-literals (V1831) (cond ((= () V1831) ()) ((and (cons? V1831) (and (cons? (hd V1831)) (and (= if (hd (hd V1831))) (and (cons? (tl (hd V1831))) (= () (tl (tl (hd V1831)))))))) (cons (cons when (tl (hd V1831))) (shen.construct-side-literals (tl V1831)))) ((and (cons? V1831) (and (cons? (hd V1831)) (and (= let (hd (hd V1831))) (and (cons? (tl (hd V1831))) (and (cons? (tl (tl (hd V1831)))) (= () (tl (tl (tl (hd V1831)))))))))) (cons (cons is (tl (hd V1831))) (shen.construct-side-literals (tl V1831)))) ((cons? V1831) (shen.construct-side-literals (tl V1831))) (true (shen.sys-error shen.construct-side-literals))))
-
-(defun shen.construct-premiss-literal (V1836 V1837) (cond ((tuple? V1836) (cons shen.t* (cons (shen.recursive_cons_form (snd V1836)) (cons (shen.construct-context V1837 (fst V1836)) ())))) ((= ! V1836) (cons cut (cons Throwcontrol ()))) (true (shen.sys-error shen.construct-premiss-literal))))
-
-(defun shen.construct-context (V1838 V1839) (cond ((and (= true V1838) (= () V1839)) Context_1957) ((and (= false V1838) (= () V1839)) ContextOut_1957) ((cons? V1839) (cons cons (cons (shen.recursive_cons_form (hd V1839)) (cons (shen.construct-context V1838 (tl V1839)) ())))) (true (shen.sys-error shen.construct-context))))
-
-(defun shen.recursive_cons_form (V1840) (cond ((cons? V1840) (cons cons (cons (shen.recursive_cons_form (hd V1840)) (cons (shen.recursive_cons_form (tl V1840)) ())))) (true V1840)))
-
-(defun preclude (V1841) (shen.preclude-h (map (lambda X1677 (shen.intern-type X1677)) V1841)))
-
-(defun shen.preclude-h (V1842) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1842)) (value shen.*datatypes*)))
-
-(defun include (V1843) (shen.include-h (map (lambda X1678 (shen.intern-type X1678)) V1843)))
-
-(defun shen.include-h (V1844) (let ValidTypes (intersection V1844 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*))))
-
-(defun preclude-all-but (V1845) (shen.preclude-h (difference (value shen.*alldatatypes*) (map (lambda X1679 (shen.intern-type X1679)) V1845))))
-
-(defun include-all-but (V1846) (shen.include-h (difference (value shen.*alldatatypes*) (map (lambda X1680 (shen.intern-type X1680)) V1846))))
-
-(defun shen.synonyms-help (V1851) (cond ((= () V1851) (shen.demodulation-function (value shen.*tc*) (mapcan (lambda X1681 (shen.demod-rule X1681)) (value shen.*synonyms*)))) ((and (cons? V1851) (cons? (tl V1851))) (let Vs (difference (shen.extract_vars (hd (tl V1851))) (shen.extract_vars (hd V1851))) (if (empty? Vs) (do (shen.pushnew (cons (hd V1851) (cons (hd (tl V1851)) ())) shen.*synonyms*) (shen.synonyms-help (tl (tl V1851)))) (shen.free_variable_warnings (hd (tl V1851)) Vs)))) (true (simple-error "odd number of synonyms
-"))))
-
-(defun shen.pushnew (V1852 V1853) (if (element? V1852 (value V1853)) (value V1853) (set V1853 (cons V1852 (value V1853)))))
-
-(defun shen.demod-rule (V1854) (cond ((and (cons? V1854) (and (cons? (tl V1854)) (= () (tl (tl V1854))))) (cons (shen.rcons_form (hd V1854)) (cons -> (cons (shen.rcons_form (hd (tl V1854))) ())))) (true (shen.sys-error shen.demod-rule))))
-
-(defun shen.demodulation-function (V1855 V1856) (do (tc -) (do (eval (cons define (cons shen.demod (append V1856 (shen.default-rule))))) (do (if V1855 (tc +) shen.skip) synonyms))))
-
-(defun shen.default-rule () (cons X (cons -> (cons X ()))))
-
-
-
+"**********************************************************************************
+* 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.datatype-error (V1686) (cond ((and (cons? V1686) (and (cons? (tl V1686)) (= () (tl (tl V1686))))) (simple-error (cn "datatype syntax error here:
+
+ " (shen.app (shen.next-50 50 (hd V1686)) "
+" shen.a)))) (true (shen.sys-error shen.datatype-error))))
+
+(defun shen.<datatype-rules> (V1691) (let Result (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1691) (if (not (= (fail) Parse_shen.<datatype-rule>)) (let Parse_shen.<datatype-rules> (shen.<datatype-rules> Parse_shen.<datatype-rule>) (if (not (= (fail) Parse_shen.<datatype-rules>)) (shen.pair (hd Parse_shen.<datatype-rules>) (cons (shen.hdtl Parse_shen.<datatype-rule>) (shen.hdtl Parse_shen.<datatype-rules>))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_<e> (<e> V1691) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
+
+(defun shen.<datatype-rule> (V1696) (let Result (let Parse_shen.<side-conditions> (shen.<side-conditions> V1696) (if (not (= (fail) Parse_shen.<side-conditions>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<side-conditions>) (if (not (= (fail) Parse_shen.<premises>)) (let Parse_shen.<singleunderline> (shen.<singleunderline> Parse_shen.<premises>) (if (not (= (fail) Parse_shen.<singleunderline>)) (let Parse_shen.<conclusion> (shen.<conclusion> Parse_shen.<singleunderline>) (if (not (= (fail) Parse_shen.<conclusion>)) (shen.pair (hd Parse_shen.<conclusion>) (shen.sequent shen.single (cons (shen.hdtl Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<conclusion>) ()))))) (fail))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<side-conditions> (shen.<side-conditions> V1696) (if (not (= (fail) Parse_shen.<side-conditions>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<side-conditions>) (if (not (= (fail) Parse_shen.<premises>)) (let Parse_shen.<doubleunderline> (shen.<doubleunderline> Parse_shen.<premises>) (if (not (= (fail) Parse_shen.<doubleunderline>)) (let Parse_shen.<conclusion> (shen.<conclusion> Parse_shen.<doubleunderline>) (if (not (= (fail) Parse_shen.<conclusion>)) (shen.pair (hd Parse_shen.<conclusion>) (shen.sequent shen.double (cons (shen.hdtl Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<conclusion>) ()))))) (fail))) (fail))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
+
+(defun shen.<side-conditions> (V1701) (let Result (let Parse_shen.<side-condition> (shen.<side-condition> V1701) (if (not (= (fail) Parse_shen.<side-condition>)) (let Parse_shen.<side-conditions> (shen.<side-conditions> Parse_shen.<side-condition>) (if (not (= (fail) Parse_shen.<side-conditions>)) (shen.pair (hd Parse_shen.<side-conditions>) (cons (shen.hdtl Parse_shen.<side-condition>) (shen.hdtl Parse_shen.<side-conditions>))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_<e> (<e> V1701) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
+
+(defun shen.<side-condition> (V1706) (let Result (if (and (cons? (hd V1706)) (= if (hd (hd V1706)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1706)) (shen.hdtl V1706))) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (cons if (cons (shen.hdtl Parse_shen.<expr>) ()))) (fail))) (fail)) (if (= Result (fail)) (let Result (if (and (cons? (hd V1706)) (= let (hd (hd V1706)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1706)) (shen.hdtl V1706))) (if (not (= (fail) Parse_shen.<variable?>)) (let Parse_shen.<expr> (shen.<expr> Parse_shen.<variable?>) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (cons let (cons (shen.hdtl Parse_shen.<variable?>) (cons (shen.hdtl Parse_shen.<expr>) ())))) (fail))) (fail))) (fail)) (if (= Result (fail)) (fail) Result)) Result)))
+
+(defun shen.<variable?> (V1711) (let Result (if (cons? (hd V1711)) (let Parse_X (hd (hd V1711)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1711)) (shen.hdtl V1711))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
+
+(defun shen.<expr> (V1716) (let Result (if (cons? (hd V1716)) (let Parse_X (hd (hd V1716)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1716)) (shen.hdtl V1716))) (shen.remove-bar Parse_X)) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
+
+(defun shen.remove-bar (V1717) (cond ((and (cons? V1717) (and (cons? (tl V1717)) (and (cons? (tl (tl V1717))) (and (= () (tl (tl (tl V1717)))) (= (hd (tl V1717)) bar!))))) (cons (hd V1717) (hd (tl (tl V1717))))) ((cons? V1717) (cons (shen.remove-bar (hd V1717)) (shen.remove-bar (tl V1717)))) (true V1717)))
+
+(defun shen.<premises> (V1722) (let Result (let Parse_shen.<premise> (shen.<premise> V1722) (if (not (= (fail) Parse_shen.<premise>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<premise>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (let Parse_shen.<premises> (shen.<premises> Parse_shen.<semicolon-symbol>) (if (not (= (fail) Parse_shen.<premises>)) (shen.pair (hd Parse_shen.<premises>) (cons (shen.hdtl Parse_shen.<premise>) (shen.hdtl Parse_shen.<premises>))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_<e> (<e> V1722) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
+
+(defun shen.<semicolon-symbol> (V1727) (let Result (if (cons? (hd V1727)) (let Parse_X (hd (hd V1727)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1727)) (shen.hdtl V1727))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
+
+(defun shen.<premise> (V1732) (let Result (if (and (cons? (hd V1732)) (= ! (hd (hd V1732)))) (shen.pair (hd (shen.pair (tl (hd V1732)) (shen.hdtl V1732))) !) (fail)) (if (= Result (fail)) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1732) (if (not (= (fail) Parse_shen.<formulae>)) (if (and (cons? (hd Parse_shen.<formulae>)) (= >> (hd (hd Parse_shen.<formulae>)))) (let Parse_shen.<formula> (shen.<formula> (shen.pair (tl (hd Parse_shen.<formulae>)) (shen.hdtl Parse_shen.<formulae>))) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (shen.sequent (shen.hdtl Parse_shen.<formulae>) (shen.hdtl Parse_shen.<formula>))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<formula> (shen.<formula> V1732) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (shen.sequent () (shen.hdtl Parse_shen.<formula>))) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result)))
+
+(defun shen.<conclusion> (V1737) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1737) (if (not (= (fail) Parse_shen.<formulae>)) (if (and (cons? (hd Parse_shen.<formulae>)) (= >> (hd (hd Parse_shen.<formulae>)))) (let Parse_shen.<formula> (shen.<formula> (shen.pair (tl (hd Parse_shen.<formulae>)) (shen.hdtl Parse_shen.<formulae>))) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (shen.pair (hd Parse_shen.<semicolon-symbol>) (shen.sequent (shen.hdtl Parse_shen.<formulae>) (shen.hdtl Parse_shen.<formula>))) (fail))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<formula> (shen.<formula> V1737) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<semicolon-symbol> (shen.<semicolon-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<semicolon-symbol>)) (shen.pair (hd Parse_shen.<semicolon-symbol>) (shen.sequent () (shen.hdtl Parse_shen.<formula>))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
+
+(defun shen.sequent (V1738 V1739) (@p V1738 V1739))
+
+(defun shen.<formulae> (V1744) (let Result (let Parse_shen.<formula> (shen.<formula> V1744) (if (not (= (fail) Parse_shen.<formula>)) (let Parse_shen.<comma-symbol> (shen.<comma-symbol> Parse_shen.<formula>) (if (not (= (fail) Parse_shen.<comma-symbol>)) (let Parse_shen.<formulae> (shen.<formulae> Parse_shen.<comma-symbol>) (if (not (= (fail) Parse_shen.<formulae>)) (shen.pair (hd Parse_shen.<formulae>) (cons (shen.hdtl Parse_shen.<formula>) (shen.hdtl Parse_shen.<formulae>))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<formula> (shen.<formula> V1744) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (cons (shen.hdtl Parse_shen.<formula>) ())) (fail))) (if (= Result (fail)) (let Result (let Parse_<e> (<e> V1744) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result)))
+
+(defun shen.<comma-symbol> (V1749) (let Result (if (cons? (hd V1749)) (let Parse_X (hd (hd V1749)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1749)) (shen.hdtl V1749))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
+
+(defun shen.<formula> (V1754) (let Result (let Parse_shen.<expr> (shen.<expr> V1754) (if (not (= (fail) Parse_shen.<expr>)) (if (and (cons? (hd Parse_shen.<expr>)) (= : (hd (hd Parse_shen.<expr>)))) (let Parse_shen.<type> (shen.<type> (shen.pair (tl (hd Parse_shen.<expr>)) (shen.hdtl Parse_shen.<expr>))) (if (not (= (fail) Parse_shen.<type>)) (shen.pair (hd Parse_shen.<type>) (cons (shen.curry (shen.hdtl Parse_shen.<expr>)) (cons : (cons (shen.demodulate (shen.hdtl Parse_shen.<type>)) ())))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<expr> (shen.<expr> V1754) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.hdtl Parse_shen.<expr>)) (fail))) (if (= Result (fail)) (fail) Result)) Result)))
+
+(defun shen.<type> (V1759) (let Result (let Parse_shen.<expr> (shen.<expr> V1759) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.curry-type (shen.hdtl Parse_shen.<expr>))) (fail))) (if (= Result (fail)) (fail) Result)))
+
+(defun shen.<doubleunderline> (V1764) (let Result (if (cons? (hd V1764)) (let Parse_X (hd (hd V1764)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1764)) (shen.hdtl V1764))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
+
+(defun shen.<singleunderline> (V1769) (let Result (if (cons? (hd V1769)) (let Parse_X (hd (hd V1769)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1769)) (shen.hdtl V1769))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result)))
+
+(defun shen.singleunderline? (V1770) (and (symbol? V1770) (shen.sh? (str V1770))))
+
+(defun shen.sh? (V1771) (cond ((= "_" V1771) true) (true (and (= (pos V1771 0) "_") (shen.sh? (tlstr V1771))))))
+
+(defun shen.doubleunderline? (V1772) (and (symbol? V1772) (shen.dh? (str V1772))))
+
+(defun shen.dh? (V1773) (cond ((= "=" V1773) true) (true (and (= (pos V1773 0) "=") (shen.dh? (tlstr V1773))))))
+
+(defun shen.process-datatype (V1774 V1775) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1774 V1775))))
+
+(defun shen.remember-datatype (V1780) (cond ((cons? V1780) (do (set shen.*datatypes* (adjoin (hd V1780) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1780) (value shen.*alldatatypes*))) (hd V1780)))) (true (shen.sys-error shen.remember-datatype))))
+
+(defun shen.rules->horn-clauses (V1783 V1784) (cond ((= () V1784) ()) ((and (cons? V1784) (and (tuple? (hd V1784)) (= shen.single (fst (hd V1784))))) (cons (shen.rule->horn-clause V1783 (snd (hd V1784))) (shen.rules->horn-clauses V1783 (tl V1784)))) ((and (cons? V1784) (and (tuple? (hd V1784)) (= shen.double (fst (hd V1784))))) (shen.rules->horn-clauses V1783 (append (shen.double->singles (snd (hd V1784))) (tl V1784)))) (true (shen.sys-error shen.rules->horn-clauses))))
+
+(defun shen.double->singles (V1785) (cons (shen.right-rule V1785) (cons (shen.left-rule V1785) ())))
+
+(defun shen.right-rule (V1786) (@p shen.single V1786))
+
+(defun shen.left-rule (V1787) (cond ((and (cons? V1787) (and (cons? (tl V1787)) (and (cons? (tl (tl V1787))) (and (tuple? (hd (tl (tl V1787)))) (and (= () (fst (hd (tl (tl V1787))))) (= () (tl (tl (tl V1787))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1787)))) ()) Q) (let NewPremises (cons (@p (map (lambda X1675 (shen.right->left X1675)) (hd (tl V1787))) Q) ()) (@p shen.single (cons (hd V1787) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.sys-error shen.left-rule))))
+
+(defun shen.right->left (V1792) (cond ((and (tuple? V1792) (= () (fst V1792))) (snd V1792)) (true (simple-error "syntax error with ==========
+"))))
+
+(defun shen.rule->horn-clause (V1793 V1794) (cond ((and (cons? V1794) (and (cons? (tl V1794)) (and (cons? (tl (tl V1794))) (and (tuple? (hd (tl (tl V1794)))) (= () (tl (tl (tl V1794)))))))) (cons (shen.rule->horn-clause-head V1793 (snd (hd (tl (tl V1794))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1794) (hd (tl V1794)) (fst (hd (tl (tl V1794))))) ())))) (true (shen.sys-error shen.rule->horn-clause))))
+
+(defun shen.rule->horn-clause-head (V1795 V1796) (cons V1795 (cons (shen.mode-ify V1796) (cons Context_1957 ()))))
+
+(defun shen.mode-ify (V1797) (cond ((and (cons? V1797) (and (cons? (tl V1797)) (and (= : (hd (tl V1797))) (and (cons? (tl (tl V1797))) (= () (tl (tl (tl V1797)))))))) (cons mode (cons (cons (hd V1797) (cons : (cons (cons mode (cons (hd (tl (tl V1797))) (cons + ()))) ()))) (cons - ())))) (true V1797)))
+
+(defun shen.rule->horn-clause-body (V1798 V1799 V1800) (let Variables (map (lambda X1676 (shen.extract_vars X1676)) V1800) (let Predicates (map (lambda X (gensym shen.cl)) V1800) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1800 Variables) (let SideLiterals (shen.construct-side-literals V1798) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1800))) V1799) (append SearchLiterals (append SideLiterals PremissLiterals)))))))))
+
+(defun shen.construct-search-literals (V1805 V1806 V1807 V1808) (cond ((and (= () V1805) (= () V1806)) ()) (true (shen.csl-help V1805 V1806 V1807 V1808))))
+
+(defun shen.csl-help (V1811 V1812 V1813 V1814) (cond ((and (= () V1811) (= () V1812)) (cons (cons bind (cons ContextOut_1957 (cons V1813 ()))) ())) ((and (cons? V1811) (cons? V1812)) (cons (cons (hd V1811) (cons V1813 (cons V1814 (hd V1812)))) (shen.csl-help (tl V1811) (tl V1812) V1814 (gensym Context)))) (true (shen.sys-error shen.csl-help))))
+
+(defun shen.construct-search-clauses (V1815 V1816 V1817) (cond ((and (= () V1815) (and (= () V1816) (= () V1817))) shen.skip) ((and (cons? V1815) (and (cons? V1816) (cons? V1817))) (do (shen.construct-search-clause (hd V1815) (hd V1816) (hd V1817)) (shen.construct-search-clauses (tl V1815) (tl V1816) (tl V1817)))) (true (shen.sys-error shen.construct-search-clauses))))
+
+(defun shen.construct-search-clause (V1818 V1819 V1820) (shen.s-prolog (cons (shen.construct-base-search-clause V1818 V1819 V1820) (cons (shen.construct-recursive-search-clause V1818 V1819 V1820) ()))))
+
+(defun shen.construct-base-search-clause (V1821 V1822 V1823) (cons (cons V1821 (cons (cons (shen.mode-ify V1822) In_1957) (cons In_1957 V1823))) (cons :- (cons () ()))))
+
+(defun shen.construct-recursive-search-clause (V1824 V1825 V1826) (cons (cons V1824 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1826))) (cons :- (cons (cons (cons V1824 (cons Assumptions_1957 (cons Out_1957 V1826))) ()) ()))))
+
+(defun shen.construct-side-literals (V1831) (cond ((= () V1831) ()) ((and (cons? V1831) (and (cons? (hd V1831)) (and (= if (hd (hd V1831))) (and (cons? (tl (hd V1831))) (= () (tl (tl (hd V1831)))))))) (cons (cons when (tl (hd V1831))) (shen.construct-side-literals (tl V1831)))) ((and (cons? V1831) (and (cons? (hd V1831)) (and (= let (hd (hd V1831))) (and (cons? (tl (hd V1831))) (and (cons? (tl (tl (hd V1831)))) (= () (tl (tl (tl (hd V1831)))))))))) (cons (cons is (tl (hd V1831))) (shen.construct-side-literals (tl V1831)))) ((cons? V1831) (shen.construct-side-literals (tl V1831))) (true (shen.sys-error shen.construct-side-literals))))
+
+(defun shen.construct-premiss-literal (V1836 V1837) (cond ((tuple? V1836) (cons shen.t* (cons (shen.recursive_cons_form (snd V1836)) (cons (shen.construct-context V1837 (fst V1836)) ())))) ((= ! V1836) (cons cut (cons Throwcontrol ()))) (true (shen.sys-error shen.construct-premiss-literal))))
+
+(defun shen.construct-context (V1838 V1839) (cond ((and (= true V1838) (= () V1839)) Context_1957) ((and (= false V1838) (= () V1839)) ContextOut_1957) ((cons? V1839) (cons cons (cons (shen.recursive_cons_form (hd V1839)) (cons (shen.construct-context V1838 (tl V1839)) ())))) (true (shen.sys-error shen.construct-context))))
+
+(defun shen.recursive_cons_form (V1840) (cond ((cons? V1840) (cons cons (cons (shen.recursive_cons_form (hd V1840)) (cons (shen.recursive_cons_form (tl V1840)) ())))) (true V1840)))
+
+(defun preclude (V1841) (shen.preclude-h (map (lambda X1677 (shen.intern-type X1677)) V1841)))
+
+(defun shen.preclude-h (V1842) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1842)) (value shen.*datatypes*)))
+
+(defun include (V1843) (shen.include-h (map (lambda X1678 (shen.intern-type X1678)) V1843)))
+
+(defun shen.include-h (V1844) (let ValidTypes (intersection V1844 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*))))
+
+(defun preclude-all-but (V1845) (shen.preclude-h (difference (value shen.*alldatatypes*) (map (lambda X1679 (shen.intern-type X1679)) V1845))))
+
+(defun include-all-but (V1846) (shen.include-h (difference (value shen.*alldatatypes*) (map (lambda X1680 (shen.intern-type X1680)) V1846))))
+
+(defun shen.synonyms-help (V1851) (cond ((= () V1851) (shen.demodulation-function (value shen.*tc*) (mapcan (lambda X1681 (shen.demod-rule X1681)) (value shen.*synonyms*)))) ((and (cons? V1851) (cons? (tl V1851))) (let Vs (difference (shen.extract_vars (hd (tl V1851))) (shen.extract_vars (hd V1851))) (if (empty? Vs) (do (shen.pushnew (cons (hd V1851) (cons (hd (tl V1851)) ())) shen.*synonyms*) (shen.synonyms-help (tl (tl V1851)))) (shen.free_variable_warnings (hd (tl V1851)) Vs)))) (true (simple-error "odd number of synonyms
+"))))
+
+(defun shen.pushnew (V1852 V1853) (if (element? V1852 (value V1853)) (value V1853) (set V1853 (cons V1852 (value V1853)))))
+
+(defun shen.demod-rule (V1854) (cond ((and (cons? V1854) (and (cons? (tl V1854)) (= () (tl (tl V1854))))) (cons (shen.rcons_form (hd V1854)) (cons -> (cons (shen.rcons_form (hd (tl V1854))) ())))) (true (shen.sys-error shen.demod-rule))))
+
+(defun shen.demodulation-function (V1855 V1856) (do (tc -) (do (eval (cons define (cons shen.demod (append V1856 (shen.default-rule))))) (do (if V1855 (tc +) shen.skip) synonyms))))
+
+(defun shen.default-rule () (cons X (cons -> (cons X ()))))
+
+
+