shen/release/k_lambda/sequent.kl in shen-ruby-0.6.0 vs shen/release/k_lambda/sequent.kl in shen-ruby-0.7.0

- old
+ new

@@ -45,116 +45,116 @@ * * * For an explication of this license see www.shenlanguage.org/license.htm which * * explains this license in full. * * * ***************************************************************************************** -"(defun shen.datatype-error (V1612) (cond ((and (cons? V1612) (and (cons? (tl V1612)) (= () (tl (tl V1612))))) (simple-error (cn "datatype syntax error here: +"(defun shen.datatype-error (V1632) (cond ((and (cons? V1632) (and (cons? (tl V1632)) (= () (tl (tl V1632))))) (simple-error (cn "datatype syntax error here: - " (shen.app (shen.next-50 50 (hd V1612)) " + " (shen.app (shen.next-50 50 (hd V1632)) " " shen.a)))) (true (shen.sys-error shen.datatype-error)))) -(defun shen.<datatype-rules> (V1617) (let Result (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1617) (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> V1617) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) +(defun shen.<datatype-rules> (V1637) (let Result (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1637) (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> V1637) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) -(defun shen.<datatype-rule> (V1622) (let Result (let Parse_shen.<side-conditions> (shen.<side-conditions> V1622) (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> V1622) (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.<datatype-rule> (V1642) (let Result (let Parse_shen.<side-conditions> (shen.<side-conditions> V1642) (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> V1642) (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> (V1627) (let Result (let Parse_shen.<side-condition> (shen.<side-condition> V1627) (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> V1627) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) +(defun shen.<side-conditions> (V1647) (let Result (let Parse_shen.<side-condition> (shen.<side-condition> V1647) (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> V1647) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) -(defun shen.<side-condition> (V1632) (let Result (if (and (cons? (hd V1632)) (= if (hd (hd V1632)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1632)) (shen.hdtl V1632))) (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 V1632)) (= let (hd (hd V1632)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1632)) (shen.hdtl V1632))) (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.<side-condition> (V1652) (let Result (if (and (cons? (hd V1652)) (= if (hd (hd V1652)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1652)) (shen.hdtl V1652))) (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 V1652)) (= let (hd (hd V1652)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1652)) (shen.hdtl V1652))) (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?> (V1637) (let Result (if (cons? (hd V1637)) (let Parse_X (hd (hd V1637)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1637)) (shen.hdtl V1637))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<variable?> (V1657) (let Result (if (cons? (hd V1657)) (let Parse_X (hd (hd V1657)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1657)) (shen.hdtl V1657))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.<expr> (V1642) (let Result (if (cons? (hd V1642)) (let Parse_X (hd (hd V1642)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1642)) (shen.hdtl V1642))) (shen.remove-bar Parse_X)) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<expr> (V1662) (let Result (if (cons? (hd V1662)) (let Parse_X (hd (hd V1662)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1662)) (shen.hdtl V1662))) (shen.remove-bar Parse_X)) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.remove-bar (V1643) (cond ((and (cons? V1643) (and (cons? (tl V1643)) (and (cons? (tl (tl V1643))) (and (= () (tl (tl (tl V1643)))) (= (hd (tl V1643)) bar!))))) (cons (hd V1643) (hd (tl (tl V1643))))) ((cons? V1643) (cons (shen.remove-bar (hd V1643)) (shen.remove-bar (tl V1643)))) (true V1643))) +(defun shen.remove-bar (V1663) (cond ((and (cons? V1663) (and (cons? (tl V1663)) (and (cons? (tl (tl V1663))) (and (= () (tl (tl (tl V1663)))) (= (hd (tl V1663)) bar!))))) (cons (hd V1663) (hd (tl (tl V1663))))) ((cons? V1663) (cons (shen.remove-bar (hd V1663)) (shen.remove-bar (tl V1663)))) (true V1663))) -(defun shen.<premises> (V1648) (let Result (let Parse_shen.<premise> (shen.<premise> V1648) (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> V1648) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) +(defun shen.<premises> (V1668) (let Result (let Parse_shen.<premise> (shen.<premise> V1668) (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> V1668) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) -(defun shen.<semicolon-symbol> (V1653) (let Result (if (cons? (hd V1653)) (let Parse_X (hd (hd V1653)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1653)) (shen.hdtl V1653))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<semicolon-symbol> (V1673) (let Result (if (cons? (hd V1673)) (let Parse_X (hd (hd V1673)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1673)) (shen.hdtl V1673))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.<premise> (V1658) (let Result (if (and (cons? (hd V1658)) (= ! (hd (hd V1658)))) (shen.pair (hd (shen.pair (tl (hd V1658)) (shen.hdtl V1658))) !) (fail)) (if (= Result (fail)) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1658) (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> V1658) (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.<premise> (V1678) (let Result (if (and (cons? (hd V1678)) (= ! (hd (hd V1678)))) (shen.pair (hd (shen.pair (tl (hd V1678)) (shen.hdtl V1678))) !) (fail)) (if (= Result (fail)) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1678) (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> V1678) (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> (V1663) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1663) (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> V1663) (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.<conclusion> (V1683) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1683) (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> V1683) (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 (V1664 V1665) (@p V1664 V1665)) +(defun shen.sequent (V1684 V1685) (@p V1684 V1685)) -(defun shen.<formulae> (V1670) (let Result (let Parse_shen.<formula> (shen.<formula> V1670) (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> V1670) (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> V1670) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result))) +(defun shen.<formulae> (V1690) (let Result (let Parse_shen.<formula> (shen.<formula> V1690) (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> V1690) (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> V1690) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result))) -(defun shen.<comma-symbol> (V1675) (let Result (if (cons? (hd V1675)) (let Parse_X (hd (hd V1675)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1675)) (shen.hdtl V1675))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<comma-symbol> (V1695) (let Result (if (cons? (hd V1695)) (let Parse_X (hd (hd V1695)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1695)) (shen.hdtl V1695))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.<formula> (V1680) (let Result (let Parse_shen.<expr> (shen.<expr> V1680) (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> V1680) (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.<formula> (V1700) (let Result (let Parse_shen.<expr> (shen.<expr> V1700) (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> V1700) (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> (V1685) (let Result (let Parse_shen.<expr> (shen.<expr> V1685) (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.<type> (V1705) (let Result (let Parse_shen.<expr> (shen.<expr> V1705) (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> (V1690) (let Result (if (cons? (hd V1690)) (let Parse_X (hd (hd V1690)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1690)) (shen.hdtl V1690))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<doubleunderline> (V1710) (let Result (if (cons? (hd V1710)) (let Parse_X (hd (hd V1710)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1710)) (shen.hdtl V1710))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.<singleunderline> (V1695) (let Result (if (cons? (hd V1695)) (let Parse_X (hd (hd V1695)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1695)) (shen.hdtl V1695))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<singleunderline> (V1715) (let Result (if (cons? (hd V1715)) (let Parse_X (hd (hd V1715)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1715)) (shen.hdtl V1715))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.singleunderline? (V1696) (and (symbol? V1696) (shen.sh? (str V1696)))) +(defun shen.singleunderline? (V1716) (and (symbol? V1716) (shen.sh? (str V1716)))) -(defun shen.sh? (V1697) (cond ((= "_" V1697) true) (true (and (= (pos V1697 0) "_") (shen.sh? (tlstr V1697)))))) +(defun shen.sh? (V1717) (cond ((= "_" V1717) true) (true (and (= (pos V1717 0) "_") (shen.sh? (tlstr V1717)))))) -(defun shen.doubleunderline? (V1698) (and (symbol? V1698) (shen.dh? (str V1698)))) +(defun shen.doubleunderline? (V1718) (and (symbol? V1718) (shen.dh? (str V1718)))) -(defun shen.dh? (V1699) (cond ((= "=" V1699) true) (true (and (= (pos V1699 0) "=") (shen.dh? (tlstr V1699)))))) +(defun shen.dh? (V1719) (cond ((= "=" V1719) true) (true (and (= (pos V1719 0) "=") (shen.dh? (tlstr V1719)))))) -(defun shen.process-datatype (V1700 V1701) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1700 V1701)))) +(defun shen.process-datatype (V1720 V1721) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1720 V1721)))) -(defun shen.remember-datatype (V1706) (cond ((cons? V1706) (do (set shen.*datatypes* (adjoin (hd V1706) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1706) (value shen.*alldatatypes*))) (hd V1706)))) (true (shen.sys-error shen.remember-datatype)))) +(defun shen.remember-datatype (V1726) (cond ((cons? V1726) (do (set shen.*datatypes* (adjoin (hd V1726) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1726) (value shen.*alldatatypes*))) (hd V1726)))) (true (shen.sys-error shen.remember-datatype)))) -(defun shen.rules->horn-clauses (V1709 V1710) (cond ((= () V1710) ()) ((and (cons? V1710) (and (tuple? (hd V1710)) (= shen.single (fst (hd V1710))))) (cons (shen.rule->horn-clause V1709 (snd (hd V1710))) (shen.rules->horn-clauses V1709 (tl V1710)))) ((and (cons? V1710) (and (tuple? (hd V1710)) (= shen.double (fst (hd V1710))))) (shen.rules->horn-clauses V1709 (append (shen.double->singles (snd (hd V1710))) (tl V1710)))) (true (shen.sys-error shen.rules->horn-clauses)))) +(defun shen.rules->horn-clauses (V1729 V1730) (cond ((= () V1730) ()) ((and (cons? V1730) (and (tuple? (hd V1730)) (= shen.single (fst (hd V1730))))) (cons (shen.rule->horn-clause V1729 (snd (hd V1730))) (shen.rules->horn-clauses V1729 (tl V1730)))) ((and (cons? V1730) (and (tuple? (hd V1730)) (= shen.double (fst (hd V1730))))) (shen.rules->horn-clauses V1729 (append (shen.double->singles (snd (hd V1730))) (tl V1730)))) (true (shen.sys-error shen.rules->horn-clauses)))) -(defun shen.double->singles (V1711) (cons (shen.right-rule V1711) (cons (shen.left-rule V1711) ()))) +(defun shen.double->singles (V1731) (cons (shen.right-rule V1731) (cons (shen.left-rule V1731) ()))) -(defun shen.right-rule (V1712) (@p shen.single V1712)) +(defun shen.right-rule (V1732) (@p shen.single V1732)) -(defun shen.left-rule (V1713) (cond ((and (cons? V1713) (and (cons? (tl V1713)) (and (cons? (tl (tl V1713))) (and (tuple? (hd (tl (tl V1713)))) (and (= () (fst (hd (tl (tl V1713))))) (= () (tl (tl (tl V1713))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1713)))) ()) Q) (let NewPremises (cons (@p (map shen.right->left (hd (tl V1713))) Q) ()) (@p shen.single (cons (hd V1713) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.sys-error shen.left-rule)))) +(defun shen.left-rule (V1733) (cond ((and (cons? V1733) (and (cons? (tl V1733)) (and (cons? (tl (tl V1733))) (and (tuple? (hd (tl (tl V1733)))) (and (= () (fst (hd (tl (tl V1733))))) (= () (tl (tl (tl V1733))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1733)))) ()) Q) (let NewPremises (cons (@p (map shen.right->left (hd (tl V1733))) Q) ()) (@p shen.single (cons (hd V1733) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.sys-error shen.left-rule)))) -(defun shen.right->left (V1718) (cond ((and (tuple? V1718) (= () (fst V1718))) (snd V1718)) (true (simple-error "syntax error with ========== +(defun shen.right->left (V1738) (cond ((and (tuple? V1738) (= () (fst V1738))) (snd V1738)) (true (simple-error "syntax error with ========== ")))) -(defun shen.rule->horn-clause (V1719 V1720) (cond ((and (cons? V1720) (and (cons? (tl V1720)) (and (cons? (tl (tl V1720))) (and (tuple? (hd (tl (tl V1720)))) (= () (tl (tl (tl V1720)))))))) (cons (shen.rule->horn-clause-head V1719 (snd (hd (tl (tl V1720))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1720) (hd (tl V1720)) (fst (hd (tl (tl V1720))))) ())))) (true (shen.sys-error shen.rule->horn-clause)))) +(defun shen.rule->horn-clause (V1739 V1740) (cond ((and (cons? V1740) (and (cons? (tl V1740)) (and (cons? (tl (tl V1740))) (and (tuple? (hd (tl (tl V1740)))) (= () (tl (tl (tl V1740)))))))) (cons (shen.rule->horn-clause-head V1739 (snd (hd (tl (tl V1740))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1740) (hd (tl V1740)) (fst (hd (tl (tl V1740))))) ())))) (true (shen.sys-error shen.rule->horn-clause)))) -(defun shen.rule->horn-clause-head (V1721 V1722) (cons V1721 (cons (shen.mode-ify V1722) (cons Context_1957 ())))) +(defun shen.rule->horn-clause-head (V1741 V1742) (cons V1741 (cons (shen.mode-ify V1742) (cons Context_1957 ())))) -(defun shen.mode-ify (V1723) (cond ((and (cons? V1723) (and (cons? (tl V1723)) (and (= : (hd (tl V1723))) (and (cons? (tl (tl V1723))) (= () (tl (tl (tl V1723)))))))) (cons mode (cons (cons (hd V1723) (cons : (cons (cons mode (cons (hd (tl (tl V1723))) (cons + ()))) ()))) (cons - ())))) (true V1723))) +(defun shen.mode-ify (V1743) (cond ((and (cons? V1743) (and (cons? (tl V1743)) (and (= : (hd (tl V1743))) (and (cons? (tl (tl V1743))) (= () (tl (tl (tl V1743)))))))) (cons mode (cons (cons (hd V1743) (cons : (cons (cons mode (cons (hd (tl (tl V1743))) (cons + ()))) ()))) (cons - ())))) (true V1743))) -(defun shen.rule->horn-clause-body (V1724 V1725 V1726) (let Variables (map shen.extract_vars V1726) (let Predicates (map (lambda X (gensym shen.cl)) V1726) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1726 Variables) (let SideLiterals (shen.construct-side-literals V1724) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1726))) V1725) (append SearchLiterals (append SideLiterals PremissLiterals))))))))) +(defun shen.rule->horn-clause-body (V1744 V1745 V1746) (let Variables (map shen.extract_vars V1746) (let Predicates (map (lambda X (gensym shen.cl)) V1746) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1746 Variables) (let SideLiterals (shen.construct-side-literals V1744) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1746))) V1745) (append SearchLiterals (append SideLiterals PremissLiterals))))))))) -(defun shen.construct-search-literals (V1731 V1732 V1733 V1734) (cond ((and (= () V1731) (= () V1732)) ()) (true (shen.csl-help V1731 V1732 V1733 V1734)))) +(defun shen.construct-search-literals (V1751 V1752 V1753 V1754) (cond ((and (= () V1751) (= () V1752)) ()) (true (shen.csl-help V1751 V1752 V1753 V1754)))) -(defun shen.csl-help (V1737 V1738 V1739 V1740) (cond ((and (= () V1737) (= () V1738)) (cons (cons bind (cons ContextOut_1957 (cons V1739 ()))) ())) ((and (cons? V1737) (cons? V1738)) (cons (cons (hd V1737) (cons V1739 (cons V1740 (hd V1738)))) (shen.csl-help (tl V1737) (tl V1738) V1740 (gensym Context)))) (true (shen.sys-error shen.csl-help)))) +(defun shen.csl-help (V1757 V1758 V1759 V1760) (cond ((and (= () V1757) (= () V1758)) (cons (cons bind (cons ContextOut_1957 (cons V1759 ()))) ())) ((and (cons? V1757) (cons? V1758)) (cons (cons (hd V1757) (cons V1759 (cons V1760 (hd V1758)))) (shen.csl-help (tl V1757) (tl V1758) V1760 (gensym Context)))) (true (shen.sys-error shen.csl-help)))) -(defun shen.construct-search-clauses (V1741 V1742 V1743) (cond ((and (= () V1741) (and (= () V1742) (= () V1743))) shen.skip) ((and (cons? V1741) (and (cons? V1742) (cons? V1743))) (do (shen.construct-search-clause (hd V1741) (hd V1742) (hd V1743)) (shen.construct-search-clauses (tl V1741) (tl V1742) (tl V1743)))) (true (shen.sys-error shen.construct-search-clauses)))) +(defun shen.construct-search-clauses (V1761 V1762 V1763) (cond ((and (= () V1761) (and (= () V1762) (= () V1763))) shen.skip) ((and (cons? V1761) (and (cons? V1762) (cons? V1763))) (do (shen.construct-search-clause (hd V1761) (hd V1762) (hd V1763)) (shen.construct-search-clauses (tl V1761) (tl V1762) (tl V1763)))) (true (shen.sys-error shen.construct-search-clauses)))) -(defun shen.construct-search-clause (V1744 V1745 V1746) (shen.s-prolog (cons (shen.construct-base-search-clause V1744 V1745 V1746) (cons (shen.construct-recursive-search-clause V1744 V1745 V1746) ())))) +(defun shen.construct-search-clause (V1764 V1765 V1766) (shen.s-prolog (cons (shen.construct-base-search-clause V1764 V1765 V1766) (cons (shen.construct-recursive-search-clause V1764 V1765 V1766) ())))) -(defun shen.construct-base-search-clause (V1747 V1748 V1749) (cons (cons V1747 (cons (cons (shen.mode-ify V1748) In_1957) (cons In_1957 V1749))) (cons :- (cons () ())))) +(defun shen.construct-base-search-clause (V1767 V1768 V1769) (cons (cons V1767 (cons (cons (shen.mode-ify V1768) In_1957) (cons In_1957 V1769))) (cons :- (cons () ())))) -(defun shen.construct-recursive-search-clause (V1750 V1751 V1752) (cons (cons V1750 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1752))) (cons :- (cons (cons (cons V1750 (cons Assumptions_1957 (cons Out_1957 V1752))) ()) ())))) +(defun shen.construct-recursive-search-clause (V1770 V1771 V1772) (cons (cons V1770 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1772))) (cons :- (cons (cons (cons V1770 (cons Assumptions_1957 (cons Out_1957 V1772))) ()) ())))) -(defun shen.construct-side-literals (V1757) (cond ((= () V1757) ()) ((and (cons? V1757) (and (cons? (hd V1757)) (and (= if (hd (hd V1757))) (and (cons? (tl (hd V1757))) (= () (tl (tl (hd V1757)))))))) (cons (cons when (tl (hd V1757))) (shen.construct-side-literals (tl V1757)))) ((and (cons? V1757) (and (cons? (hd V1757)) (and (= let (hd (hd V1757))) (and (cons? (tl (hd V1757))) (and (cons? (tl (tl (hd V1757)))) (= () (tl (tl (tl (hd V1757)))))))))) (cons (cons is (tl (hd V1757))) (shen.construct-side-literals (tl V1757)))) ((cons? V1757) (shen.construct-side-literals (tl V1757))) (true (shen.sys-error shen.construct-side-literals)))) +(defun shen.construct-side-literals (V1777) (cond ((= () V1777) ()) ((and (cons? V1777) (and (cons? (hd V1777)) (and (= if (hd (hd V1777))) (and (cons? (tl (hd V1777))) (= () (tl (tl (hd V1777)))))))) (cons (cons when (tl (hd V1777))) (shen.construct-side-literals (tl V1777)))) ((and (cons? V1777) (and (cons? (hd V1777)) (and (= let (hd (hd V1777))) (and (cons? (tl (hd V1777))) (and (cons? (tl (tl (hd V1777)))) (= () (tl (tl (tl (hd V1777)))))))))) (cons (cons is (tl (hd V1777))) (shen.construct-side-literals (tl V1777)))) ((cons? V1777) (shen.construct-side-literals (tl V1777))) (true (shen.sys-error shen.construct-side-literals)))) -(defun shen.construct-premiss-literal (V1762 V1763) (cond ((tuple? V1762) (cons shen.t* (cons (shen.recursive_cons_form (snd V1762)) (cons (shen.construct-context V1763 (fst V1762)) ())))) ((= ! V1762) (cons cut (cons Throwcontrol ()))) (true (shen.sys-error shen.construct-premiss-literal)))) +(defun shen.construct-premiss-literal (V1782 V1783) (cond ((tuple? V1782) (cons shen.t* (cons (shen.recursive_cons_form (snd V1782)) (cons (shen.construct-context V1783 (fst V1782)) ())))) ((= ! V1782) (cons cut (cons Throwcontrol ()))) (true (shen.sys-error shen.construct-premiss-literal)))) -(defun shen.construct-context (V1764 V1765) (cond ((and (= true V1764) (= () V1765)) Context_1957) ((and (= false V1764) (= () V1765)) ContextOut_1957) ((cons? V1765) (cons cons (cons (shen.recursive_cons_form (hd V1765)) (cons (shen.construct-context V1764 (tl V1765)) ())))) (true (shen.sys-error shen.construct-context)))) +(defun shen.construct-context (V1784 V1785) (cond ((and (= true V1784) (= () V1785)) Context_1957) ((and (= false V1784) (= () V1785)) ContextOut_1957) ((cons? V1785) (cons cons (cons (shen.recursive_cons_form (hd V1785)) (cons (shen.construct-context V1784 (tl V1785)) ())))) (true (shen.sys-error shen.construct-context)))) -(defun shen.recursive_cons_form (V1766) (cond ((cons? V1766) (cons cons (cons (shen.recursive_cons_form (hd V1766)) (cons (shen.recursive_cons_form (tl V1766)) ())))) (true V1766))) +(defun shen.recursive_cons_form (V1786) (cond ((cons? V1786) (cons cons (cons (shen.recursive_cons_form (hd V1786)) (cons (shen.recursive_cons_form (tl V1786)) ())))) (true V1786))) -(defun preclude (V1767) (shen.preclude-h (map shen.intern-type V1767))) +(defun preclude (V1787) (shen.preclude-h (map shen.intern-type V1787))) -(defun shen.preclude-h (V1768) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1768)) (value shen.*datatypes*))) +(defun shen.preclude-h (V1788) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1788)) (value shen.*datatypes*))) -(defun include (V1769) (shen.include-h (map shen.intern-type V1769))) +(defun include (V1789) (shen.include-h (map shen.intern-type V1789))) -(defun shen.include-h (V1770) (let ValidTypes (intersection V1770 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*)))) +(defun shen.include-h (V1790) (let ValidTypes (intersection V1790 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*)))) -(defun preclude-all-but (V1771) (shen.preclude-h (difference (value shen.*alldatatypes*) (map shen.intern-type V1771)))) +(defun preclude-all-but (V1791) (shen.preclude-h (difference (value shen.*alldatatypes*) (map shen.intern-type V1791)))) -(defun include-all-but (V1772) (shen.include-h (difference (value shen.*alldatatypes*) (map shen.intern-type V1772)))) +(defun include-all-but (V1792) (shen.include-h (difference (value shen.*alldatatypes*) (map shen.intern-type V1792)))) -(defun shen.synonyms-help (V1777) (cond ((= () V1777) synonyms) ((and (cons? V1777) (cons? (tl V1777))) (do (shen.pushnew (cons (hd V1777) (shen.curry-type (hd (tl V1777)))) shen.*synonyms*) (shen.synonyms-help (tl (tl V1777))))) (true (simple-error (cn "odd number of synonyms +(defun shen.synonyms-help (V1797) (cond ((= () V1797) synonyms) ((and (cons? V1797) (cons? (tl V1797))) (do (shen.pushnew (cons (hd V1797) (shen.curry-type (hd (tl V1797)))) shen.*synonyms*) (shen.synonyms-help (tl (tl V1797))))) (true (simple-error (cn "odd number of synonyms " ""))))) -(defun shen.pushnew (V1778 V1779) (if (element? V1778 (value V1779)) (value V1779) (set V1779 (cons V1778 (value V1779))))) +(defun shen.pushnew (V1798 V1799) (if (element? V1798 (value V1799)) (value V1799) (set V1799 (cons V1798 (value V1799)))))