"********************************************************************************** * 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 (V1639) (cond ((and (cons? V1639) (and (cons? (tl V1639)) (= () (tl (tl V1639))))) (simple-error (cn "datatype syntax error here: " (shen.app (shen.next-50 50 (hd V1639)) " " shen.a)))) (true (shen.sys-error shen.datatype-error)))) (defun shen. (V1644) (let Result (let Parse_shen. (shen. V1644) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (cons (shen.hdtl Parse_shen.) (shen.hdtl Parse_shen.))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_ ( V1644) (if (not (= (fail) Parse_)) (shen.pair (hd Parse_) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) (defun shen. (V1649) (let Result (let Parse_shen. (shen. V1649) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (shen.sequent shen.single (cons (shen.hdtl Parse_shen.) (cons (shen.hdtl Parse_shen.) (cons (shen.hdtl Parse_shen.) ()))))) (fail))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_shen. (shen. V1649) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (shen.sequent shen.double (cons (shen.hdtl Parse_shen.) (cons (shen.hdtl Parse_shen.) (cons (shen.hdtl Parse_shen.) ()))))) (fail))) (fail))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)) Result))) (defun shen. (V1654) (let Result (let Parse_shen. (shen. V1654) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (cons (shen.hdtl Parse_shen.) (shen.hdtl Parse_shen.))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_ ( V1654) (if (not (= (fail) Parse_)) (shen.pair (hd Parse_) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) (defun shen. (V1659) (let Result (if (and (cons? (hd V1659)) (= if (hd (hd V1659)))) (let Parse_shen. (shen. (shen.pair (tl (hd V1659)) (shen.hdtl V1659))) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (cons if (cons (shen.hdtl Parse_shen.) ()))) (fail))) (fail)) (if (= Result (fail)) (let Result (if (and (cons? (hd V1659)) (= let (hd (hd V1659)))) (let Parse_shen. (shen. (shen.pair (tl (hd V1659)) (shen.hdtl V1659))) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (cons let (cons (shen.hdtl Parse_shen.) (cons (shen.hdtl Parse_shen.) ())))) (fail))) (fail))) (fail)) (if (= Result (fail)) (fail) Result)) Result))) (defun shen. (V1664) (let Result (if (cons? (hd V1664)) (let Parse_X (hd (hd V1664)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1664)) (shen.hdtl V1664))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) (defun shen. (V1669) (let Result (if (cons? (hd V1669)) (let Parse_X (hd (hd V1669)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1669)) (shen.hdtl V1669))) (shen.remove-bar Parse_X)) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) (defun shen.remove-bar (V1670) (cond ((and (cons? V1670) (and (cons? (tl V1670)) (and (cons? (tl (tl V1670))) (and (= () (tl (tl (tl V1670)))) (= (hd (tl V1670)) bar!))))) (cons (hd V1670) (hd (tl (tl V1670))))) ((cons? V1670) (cons (shen.remove-bar (hd V1670)) (shen.remove-bar (tl V1670)))) (true V1670))) (defun shen. (V1675) (let Result (let Parse_shen. (shen. V1675) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (cons (shen.hdtl Parse_shen.) (shen.hdtl Parse_shen.))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_ ( V1675) (if (not (= (fail) Parse_)) (shen.pair (hd Parse_) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) (defun shen. (V1680) (let Result (if (cons? (hd V1680)) (let Parse_X (hd (hd V1680)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1680)) (shen.hdtl V1680))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) (defun shen. (V1685) (let Result (if (and (cons? (hd V1685)) (= ! (hd (hd V1685)))) (shen.pair (hd (shen.pair (tl (hd V1685)) (shen.hdtl V1685))) !) (fail)) (if (= Result (fail)) (let Result (let Parse_shen. (shen. V1685) (if (not (= (fail) Parse_shen.)) (if (and (cons? (hd Parse_shen.)) (= >> (hd (hd Parse_shen.)))) (let Parse_shen. (shen. (shen.pair (tl (hd Parse_shen.)) (shen.hdtl Parse_shen.))) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (shen.sequent (shen.hdtl Parse_shen.) (shen.hdtl Parse_shen.))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen. (shen. V1685) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (shen.sequent () (shen.hdtl Parse_shen.))) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result))) (defun shen. (V1690) (let Result (let Parse_shen. (shen. V1690) (if (not (= (fail) Parse_shen.)) (if (and (cons? (hd Parse_shen.)) (= >> (hd (hd Parse_shen.)))) (let Parse_shen. (shen. (shen.pair (tl (hd Parse_shen.)) (shen.hdtl Parse_shen.))) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (shen.sequent (shen.hdtl Parse_shen.) (shen.hdtl Parse_shen.))) (fail))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen. (shen. V1690) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (shen.sequent () (shen.hdtl Parse_shen.))) (fail))) (fail))) (if (= Result (fail)) (fail) Result)) Result))) (defun shen.sequent (V1691 V1692) (@p V1691 V1692)) (defun shen. (V1697) (let Result (let Parse_shen. (shen. V1697) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (let Parse_shen. (shen. Parse_shen.) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (cons (shen.hdtl Parse_shen.) (shen.hdtl Parse_shen.))) (fail))) (fail))) (fail))) (if (= Result (fail)) (let Result (let Parse_shen. (shen. V1697) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (cons (shen.hdtl Parse_shen.) ())) (fail))) (if (= Result (fail)) (let Result (let Parse_ ( V1697) (if (not (= (fail) Parse_)) (shen.pair (hd Parse_) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result))) (defun shen. (V1702) (let Result (if (cons? (hd V1702)) (let Parse_X (hd (hd V1702)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1702)) (shen.hdtl V1702))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) (defun shen. (V1707) (let Result (let Parse_shen. (shen. V1707) (if (not (= (fail) Parse_shen.)) (if (and (cons? (hd Parse_shen.)) (= : (hd (hd Parse_shen.)))) (let Parse_shen. (shen. (shen.pair (tl (hd Parse_shen.)) (shen.hdtl Parse_shen.))) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (cons (shen.curry (shen.hdtl Parse_shen.)) (cons : (cons (shen.demodulate (shen.hdtl Parse_shen.)) ())))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen. (shen. V1707) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (shen.hdtl Parse_shen.)) (fail))) (if (= Result (fail)) (fail) Result)) Result))) (defun shen. (V1712) (let Result (let Parse_shen. (shen. V1712) (if (not (= (fail) Parse_shen.)) (shen.pair (hd Parse_shen.) (shen.curry-type (shen.hdtl Parse_shen.))) (fail))) (if (= Result (fail)) (fail) Result))) (defun shen. (V1717) (let Result (if (cons? (hd V1717)) (let Parse_X (hd (hd V1717)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1717)) (shen.hdtl V1717))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) (defun shen. (V1722) (let Result (if (cons? (hd V1722)) (let Parse_X (hd (hd V1722)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1722)) (shen.hdtl V1722))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) (defun shen.singleunderline? (V1723) (and (symbol? V1723) (shen.sh? (str V1723)))) (defun shen.sh? (V1724) (cond ((= "_" V1724) true) (true (and (= (pos V1724 0) "_") (shen.sh? (tlstr V1724)))))) (defun shen.doubleunderline? (V1725) (and (symbol? V1725) (shen.dh? (str V1725)))) (defun shen.dh? (V1726) (cond ((= "=" V1726) true) (true (and (= (pos V1726 0) "=") (shen.dh? (tlstr V1726)))))) (defun shen.process-datatype (V1727 V1728) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1727 V1728)))) (defun shen.remember-datatype (V1733) (cond ((cons? V1733) (do (set shen.*datatypes* (adjoin (hd V1733) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1733) (value shen.*alldatatypes*))) (hd V1733)))) (true (shen.sys-error shen.remember-datatype)))) (defun shen.rules->horn-clauses (V1736 V1737) (cond ((= () V1737) ()) ((and (cons? V1737) (and (tuple? (hd V1737)) (= shen.single (fst (hd V1737))))) (cons (shen.rule->horn-clause V1736 (snd (hd V1737))) (shen.rules->horn-clauses V1736 (tl V1737)))) ((and (cons? V1737) (and (tuple? (hd V1737)) (= shen.double (fst (hd V1737))))) (shen.rules->horn-clauses V1736 (append (shen.double->singles (snd (hd V1737))) (tl V1737)))) (true (shen.sys-error shen.rules->horn-clauses)))) (defun shen.double->singles (V1738) (cons (shen.right-rule V1738) (cons (shen.left-rule V1738) ()))) (defun shen.right-rule (V1739) (@p shen.single V1739)) (defun shen.left-rule (V1740) (cond ((and (cons? V1740) (and (cons? (tl V1740)) (and (cons? (tl (tl V1740))) (and (tuple? (hd (tl (tl V1740)))) (and (= () (fst (hd (tl (tl V1740))))) (= () (tl (tl (tl V1740))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1740)))) ()) Q) (let NewPremises (cons (@p (map shen.right->left (hd (tl V1740))) Q) ()) (@p shen.single (cons (hd V1740) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.sys-error shen.left-rule)))) (defun shen.right->left (V1745) (cond ((and (tuple? V1745) (= () (fst V1745))) (snd V1745)) (true (simple-error "syntax error with ========== ")))) (defun shen.rule->horn-clause (V1746 V1747) (cond ((and (cons? V1747) (and (cons? (tl V1747)) (and (cons? (tl (tl V1747))) (and (tuple? (hd (tl (tl V1747)))) (= () (tl (tl (tl V1747)))))))) (cons (shen.rule->horn-clause-head V1746 (snd (hd (tl (tl V1747))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1747) (hd (tl V1747)) (fst (hd (tl (tl V1747))))) ())))) (true (shen.sys-error shen.rule->horn-clause)))) (defun shen.rule->horn-clause-head (V1748 V1749) (cons V1748 (cons (shen.mode-ify V1749) (cons Context_1957 ())))) (defun shen.mode-ify (V1750) (cond ((and (cons? V1750) (and (cons? (tl V1750)) (and (= : (hd (tl V1750))) (and (cons? (tl (tl V1750))) (= () (tl (tl (tl V1750)))))))) (cons mode (cons (cons (hd V1750) (cons : (cons (cons mode (cons (hd (tl (tl V1750))) (cons + ()))) ()))) (cons - ())))) (true V1750))) (defun shen.rule->horn-clause-body (V1751 V1752 V1753) (let Variables (map shen.extract_vars V1753) (let Predicates (map (lambda X (gensym shen.cl)) V1753) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1753 Variables) (let SideLiterals (shen.construct-side-literals V1751) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1753))) V1752) (append SearchLiterals (append SideLiterals PremissLiterals))))))))) (defun shen.construct-search-literals (V1758 V1759 V1760 V1761) (cond ((and (= () V1758) (= () V1759)) ()) (true (shen.csl-help V1758 V1759 V1760 V1761)))) (defun shen.csl-help (V1764 V1765 V1766 V1767) (cond ((and (= () V1764) (= () V1765)) (cons (cons bind (cons ContextOut_1957 (cons V1766 ()))) ())) ((and (cons? V1764) (cons? V1765)) (cons (cons (hd V1764) (cons V1766 (cons V1767 (hd V1765)))) (shen.csl-help (tl V1764) (tl V1765) V1767 (gensym Context)))) (true (shen.sys-error shen.csl-help)))) (defun shen.construct-search-clauses (V1768 V1769 V1770) (cond ((and (= () V1768) (and (= () V1769) (= () V1770))) shen.skip) ((and (cons? V1768) (and (cons? V1769) (cons? V1770))) (do (shen.construct-search-clause (hd V1768) (hd V1769) (hd V1770)) (shen.construct-search-clauses (tl V1768) (tl V1769) (tl V1770)))) (true (shen.sys-error shen.construct-search-clauses)))) (defun shen.construct-search-clause (V1771 V1772 V1773) (shen.s-prolog (cons (shen.construct-base-search-clause V1771 V1772 V1773) (cons (shen.construct-recursive-search-clause V1771 V1772 V1773) ())))) (defun shen.construct-base-search-clause (V1774 V1775 V1776) (cons (cons V1774 (cons (cons (shen.mode-ify V1775) In_1957) (cons In_1957 V1776))) (cons :- (cons () ())))) (defun shen.construct-recursive-search-clause (V1777 V1778 V1779) (cons (cons V1777 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1779))) (cons :- (cons (cons (cons V1777 (cons Assumptions_1957 (cons Out_1957 V1779))) ()) ())))) (defun shen.construct-side-literals (V1784) (cond ((= () V1784) ()) ((and (cons? V1784) (and (cons? (hd V1784)) (and (= if (hd (hd V1784))) (and (cons? (tl (hd V1784))) (= () (tl (tl (hd V1784)))))))) (cons (cons when (tl (hd V1784))) (shen.construct-side-literals (tl V1784)))) ((and (cons? V1784) (and (cons? (hd V1784)) (and (= let (hd (hd V1784))) (and (cons? (tl (hd V1784))) (and (cons? (tl (tl (hd V1784)))) (= () (tl (tl (tl (hd V1784)))))))))) (cons (cons is (tl (hd V1784))) (shen.construct-side-literals (tl V1784)))) ((cons? V1784) (shen.construct-side-literals (tl V1784))) (true (shen.sys-error shen.construct-side-literals)))) (defun shen.construct-premiss-literal (V1789 V1790) (cond ((tuple? V1789) (cons shen.t* (cons (shen.recursive_cons_form (snd V1789)) (cons (shen.construct-context V1790 (fst V1789)) ())))) ((= ! V1789) (cons cut (cons Throwcontrol ()))) (true (shen.sys-error shen.construct-premiss-literal)))) (defun shen.construct-context (V1791 V1792) (cond ((and (= true V1791) (= () V1792)) Context_1957) ((and (= false V1791) (= () V1792)) ContextOut_1957) ((cons? V1792) (cons cons (cons (shen.recursive_cons_form (hd V1792)) (cons (shen.construct-context V1791 (tl V1792)) ())))) (true (shen.sys-error shen.construct-context)))) (defun shen.recursive_cons_form (V1793) (cond ((cons? V1793) (cons cons (cons (shen.recursive_cons_form (hd V1793)) (cons (shen.recursive_cons_form (tl V1793)) ())))) (true V1793))) (defun preclude (V1794) (shen.preclude-h (map shen.intern-type V1794))) (defun shen.preclude-h (V1795) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1795)) (value shen.*datatypes*))) (defun include (V1796) (shen.include-h (map shen.intern-type V1796))) (defun shen.include-h (V1797) (let ValidTypes (intersection V1797 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*)))) (defun preclude-all-but (V1798) (shen.preclude-h (difference (value shen.*alldatatypes*) (map shen.intern-type V1798)))) (defun include-all-but (V1799) (shen.include-h (difference (value shen.*alldatatypes*) (map shen.intern-type V1799)))) (defun shen.synonyms-help (V1804) (cond ((= () V1804) synonyms) ((and (cons? V1804) (cons? (tl V1804))) (do (shen.pushnew (cons (hd V1804) (shen.curry-type (hd (tl V1804)))) shen.*synonyms*) (shen.synonyms-help (tl (tl V1804))))) (true (simple-error (cn "odd number of synonyms " ""))))) (defun shen.pushnew (V1805 V1806) (if (element? V1805 (value V1806)) (value V1806) (set V1806 (cons V1805 (value V1806)))))