shen/release/k_lambda/sequent.kl in shen-ruby-0.4.0 vs shen/release/k_lambda/sequent.kl in shen-ruby-0.4.1

- old
+ new

@@ -45,112 +45,112 @@ * * * For an explication of this license see www.shenlanguage.org/license.htm which * * explains this license in full. * * * ***************************************************************************************** -"(defun shen.datatype-error (V1585) (cond ((and (cons? V1585) (and (cons? (tl V1585)) (= () (tl (tl V1585))))) (simple-error (cn "datatype syntax error here: +"(defun shen.datatype-error (V1591) (cond ((and (cons? V1591) (and (cons? (tl V1591)) (= () (tl (tl V1591))))) (simple-error (cn "datatype syntax error here: - " (shen.app (shen.next-50 50 (hd V1585)) " + " (shen.app (shen.next-50 50 (hd V1591)) " " shen.a)))) (true (shen.sys-error shen.datatype-error)))) -(defun shen.<datatype-rules> (V1590) (let Result (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1590) (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> V1590) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) +(defun shen.<datatype-rules> (V1596) (let Result (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1596) (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> V1596) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) -(defun shen.<datatype-rule> (V1595) (let Result (let Parse_shen.<side-conditions> (shen.<side-conditions> V1595) (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> V1595) (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> (V1601) (let Result (let Parse_shen.<side-conditions> (shen.<side-conditions> V1601) (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> V1601) (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> (V1600) (let Result (let Parse_shen.<side-condition> (shen.<side-condition> V1600) (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> V1600) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) +(defun shen.<side-conditions> (V1606) (let Result (let Parse_shen.<side-condition> (shen.<side-condition> V1606) (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> V1606) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) -(defun shen.<side-condition> (V1605) (let Result (if (and (cons? (hd V1605)) (= if (hd (hd V1605)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1605)) (shen.hdtl V1605))) (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 V1605)) (= let (hd (hd V1605)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1605)) (shen.hdtl V1605))) (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> (V1611) (let Result (if (and (cons? (hd V1611)) (= if (hd (hd V1611)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1611)) (shen.hdtl V1611))) (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 V1611)) (= let (hd (hd V1611)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1611)) (shen.hdtl V1611))) (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?> (V1610) (let Result (if (cons? (hd V1610)) (let Parse_X (hd (hd V1610)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1610)) (shen.hdtl V1610))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<variable?> (V1616) (let Result (if (cons? (hd V1616)) (let Parse_X (hd (hd V1616)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1616)) (shen.hdtl V1616))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.<expr> (V1615) (let Result (if (cons? (hd V1615)) (let Parse_X (hd (hd V1615)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1615)) (shen.hdtl V1615))) (shen.remove-bar Parse_X)) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<expr> (V1621) (let Result (if (cons? (hd V1621)) (let Parse_X (hd (hd V1621)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1621)) (shen.hdtl V1621))) (shen.remove-bar Parse_X)) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.remove-bar (V1616) (cond ((and (cons? V1616) (and (cons? (tl V1616)) (and (cons? (tl (tl V1616))) (and (= () (tl (tl (tl V1616)))) (= (hd (tl V1616)) bar!))))) (cons (hd V1616) (hd (tl (tl V1616))))) ((cons? V1616) (cons (shen.remove-bar (hd V1616)) (shen.remove-bar (tl V1616)))) (true V1616))) +(defun shen.remove-bar (V1622) (cond ((and (cons? V1622) (and (cons? (tl V1622)) (and (cons? (tl (tl V1622))) (and (= () (tl (tl (tl V1622)))) (= (hd (tl V1622)) bar!))))) (cons (hd V1622) (hd (tl (tl V1622))))) ((cons? V1622) (cons (shen.remove-bar (hd V1622)) (shen.remove-bar (tl V1622)))) (true V1622))) -(defun shen.<premises> (V1621) (let Result (let Parse_shen.<premise> (shen.<premise> V1621) (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> V1621) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) +(defun shen.<premises> (V1627) (let Result (let Parse_shen.<premise> (shen.<premise> V1627) (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> V1627) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result))) -(defun shen.<semicolon-symbol> (V1626) (let Result (if (cons? (hd V1626)) (let Parse_X (hd (hd V1626)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1626)) (shen.hdtl V1626))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<semicolon-symbol> (V1632) (let Result (if (cons? (hd V1632)) (let Parse_X (hd (hd V1632)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1632)) (shen.hdtl V1632))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.<premise> (V1631) (let Result (if (and (cons? (hd V1631)) (= ! (hd (hd V1631)))) (shen.pair (hd (shen.pair (tl (hd V1631)) (shen.hdtl V1631))) !) (fail)) (if (= Result (fail)) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1631) (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> V1631) (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> (V1637) (let Result (if (and (cons? (hd V1637)) (= ! (hd (hd V1637)))) (shen.pair (hd (shen.pair (tl (hd V1637)) (shen.hdtl V1637))) !) (fail)) (if (= Result (fail)) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1637) (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> V1637) (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> (V1636) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1636) (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> V1636) (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> (V1642) (let Result (let Parse_shen.<formulae> (shen.<formulae> V1642) (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> V1642) (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 (V1637 V1638) (@p V1637 V1638)) +(defun shen.sequent (V1643 V1644) (@p V1643 V1644)) -(defun shen.<formulae> (V1643) (let Result (let Parse_shen.<formula> (shen.<formula> V1643) (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> V1643) (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> V1643) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result))) +(defun shen.<formulae> (V1649) (let Result (let Parse_shen.<formula> (shen.<formula> V1649) (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> V1649) (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> V1649) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) (if (= Result (fail)) (fail) Result)) Result)) Result))) -(defun shen.<comma-symbol> (V1648) (let Result (if (cons? (hd V1648)) (let Parse_X (hd (hd V1648)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1648)) (shen.hdtl V1648))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<comma-symbol> (V1654) (let Result (if (cons? (hd V1654)) (let Parse_X (hd (hd V1654)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1654)) (shen.hdtl V1654))) shen.skip) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.<formula> (V1653) (let Result (let Parse_shen.<expr> (shen.<expr> V1653) (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.normalise-type (shen.hdtl Parse_shen.<type>)) ())))) (fail))) (fail)) (fail))) (if (= Result (fail)) (let Result (let Parse_shen.<expr> (shen.<expr> V1653) (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> (V1659) (let Result (let Parse_shen.<expr> (shen.<expr> V1659) (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> V1659) (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> (V1658) (let Result (let Parse_shen.<expr> (shen.<expr> V1658) (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> (V1664) (let Result (let Parse_shen.<expr> (shen.<expr> V1664) (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> (V1663) (let Result (if (cons? (hd V1663)) (let Parse_X (hd (hd V1663)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1663)) (shen.hdtl V1663))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<doubleunderline> (V1669) (let Result (if (cons? (hd V1669)) (let Parse_X (hd (hd V1669)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1669)) (shen.hdtl V1669))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.<singleunderline> (V1668) (let Result (if (cons? (hd V1668)) (let Parse_X (hd (hd V1668)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1668)) (shen.hdtl V1668))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) +(defun shen.<singleunderline> (V1674) (let Result (if (cons? (hd V1674)) (let Parse_X (hd (hd V1674)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1674)) (shen.hdtl V1674))) Parse_X) (fail))) (fail)) (if (= Result (fail)) (fail) Result))) -(defun shen.singleunderline? (V1669) (and (symbol? V1669) (shen.sh? (str V1669)))) +(defun shen.singleunderline? (V1675) (and (symbol? V1675) (shen.sh? (str V1675)))) -(defun shen.sh? (V1670) (cond ((= "_" V1670) true) (true (and (= (pos V1670 0) "_") (shen.sh? (tlstr V1670)))))) +(defun shen.sh? (V1676) (cond ((= "_" V1676) true) (true (and (= (pos V1676 0) "_") (shen.sh? (tlstr V1676)))))) -(defun shen.doubleunderline? (V1671) (and (symbol? V1671) (shen.dh? (str V1671)))) +(defun shen.doubleunderline? (V1677) (and (symbol? V1677) (shen.dh? (str V1677)))) -(defun shen.dh? (V1672) (cond ((= "=" V1672) true) (true (and (= (pos V1672 0) "=") (shen.dh? (tlstr V1672)))))) +(defun shen.dh? (V1678) (cond ((= "=" V1678) true) (true (and (= (pos V1678 0) "=") (shen.dh? (tlstr V1678)))))) -(defun shen.process-datatype (V1673 V1674) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1673 V1674)))) +(defun shen.process-datatype (V1679 V1680) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1679 V1680)))) -(defun shen.remember-datatype (V1679) (cond ((cons? V1679) (do (set shen.*datatypes* (adjoin (hd V1679) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1679) (value shen.*alldatatypes*))) (hd V1679)))) (true (shen.sys-error shen.remember-datatype)))) +(defun shen.remember-datatype (V1685) (cond ((cons? V1685) (do (set shen.*datatypes* (adjoin (hd V1685) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1685) (value shen.*alldatatypes*))) (hd V1685)))) (true (shen.sys-error shen.remember-datatype)))) -(defun shen.rules->horn-clauses (V1682 V1683) (cond ((= () V1683) ()) ((and (cons? V1683) (and (tuple? (hd V1683)) (= shen.single (fst (hd V1683))))) (cons (shen.rule->horn-clause V1682 (snd (hd V1683))) (shen.rules->horn-clauses V1682 (tl V1683)))) ((and (cons? V1683) (and (tuple? (hd V1683)) (= shen.double (fst (hd V1683))))) (shen.rules->horn-clauses V1682 (append (shen.double->singles (snd (hd V1683))) (tl V1683)))) (true (shen.sys-error shen.rules->horn-clauses)))) +(defun shen.rules->horn-clauses (V1688 V1689) (cond ((= () V1689) ()) ((and (cons? V1689) (and (tuple? (hd V1689)) (= shen.single (fst (hd V1689))))) (cons (shen.rule->horn-clause V1688 (snd (hd V1689))) (shen.rules->horn-clauses V1688 (tl V1689)))) ((and (cons? V1689) (and (tuple? (hd V1689)) (= shen.double (fst (hd V1689))))) (shen.rules->horn-clauses V1688 (append (shen.double->singles (snd (hd V1689))) (tl V1689)))) (true (shen.sys-error shen.rules->horn-clauses)))) -(defun shen.double->singles (V1684) (cons (shen.right-rule V1684) (cons (shen.left-rule V1684) ()))) +(defun shen.double->singles (V1690) (cons (shen.right-rule V1690) (cons (shen.left-rule V1690) ()))) -(defun shen.right-rule (V1685) (@p shen.single V1685)) +(defun shen.right-rule (V1691) (@p shen.single V1691)) -(defun shen.left-rule (V1686) (cond ((and (cons? V1686) (and (cons? (tl V1686)) (and (cons? (tl (tl V1686))) (and (tuple? (hd (tl (tl V1686)))) (and (= () (fst (hd (tl (tl V1686))))) (= () (tl (tl (tl V1686))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1686)))) ()) Q) (let NewPremises (cons (@p (map shen.right->left (hd (tl V1686))) Q) ()) (@p shen.single (cons (hd V1686) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.sys-error shen.left-rule)))) +(defun shen.left-rule (V1692) (cond ((and (cons? V1692) (and (cons? (tl V1692)) (and (cons? (tl (tl V1692))) (and (tuple? (hd (tl (tl V1692)))) (and (= () (fst (hd (tl (tl V1692))))) (= () (tl (tl (tl V1692))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1692)))) ()) Q) (let NewPremises (cons (@p (map shen.right->left (hd (tl V1692))) Q) ()) (@p shen.single (cons (hd V1692) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.sys-error shen.left-rule)))) -(defun shen.right->left (V1691) (cond ((and (tuple? V1691) (= () (fst V1691))) (snd V1691)) (true (simple-error "syntax error with ========== +(defun shen.right->left (V1697) (cond ((and (tuple? V1697) (= () (fst V1697))) (snd V1697)) (true (simple-error "syntax error with ========== ")))) -(defun shen.rule->horn-clause (V1692 V1693) (cond ((and (cons? V1693) (and (cons? (tl V1693)) (and (cons? (tl (tl V1693))) (and (tuple? (hd (tl (tl V1693)))) (= () (tl (tl (tl V1693)))))))) (cons (shen.rule->horn-clause-head V1692 (snd (hd (tl (tl V1693))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1693) (hd (tl V1693)) (fst (hd (tl (tl V1693))))) ())))) (true (shen.sys-error shen.rule->horn-clause)))) +(defun shen.rule->horn-clause (V1698 V1699) (cond ((and (cons? V1699) (and (cons? (tl V1699)) (and (cons? (tl (tl V1699))) (and (tuple? (hd (tl (tl V1699)))) (= () (tl (tl (tl V1699)))))))) (cons (shen.rule->horn-clause-head V1698 (snd (hd (tl (tl V1699))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1699) (hd (tl V1699)) (fst (hd (tl (tl V1699))))) ())))) (true (shen.sys-error shen.rule->horn-clause)))) -(defun shen.rule->horn-clause-head (V1694 V1695) (cons V1694 (cons (shen.mode-ify V1695) (cons Context_1957 ())))) +(defun shen.rule->horn-clause-head (V1700 V1701) (cons V1700 (cons (shen.mode-ify V1701) (cons Context_1957 ())))) -(defun shen.mode-ify (V1696) (cond ((and (cons? V1696) (and (cons? (tl V1696)) (and (= : (hd (tl V1696))) (and (cons? (tl (tl V1696))) (= () (tl (tl (tl V1696)))))))) (cons mode (cons (cons (hd V1696) (cons : (cons (cons mode (cons (hd (tl (tl V1696))) (cons + ()))) ()))) (cons - ())))) (true V1696))) +(defun shen.mode-ify (V1702) (cond ((and (cons? V1702) (and (cons? (tl V1702)) (and (= : (hd (tl V1702))) (and (cons? (tl (tl V1702))) (= () (tl (tl (tl V1702)))))))) (cons mode (cons (cons (hd V1702) (cons : (cons (cons mode (cons (hd (tl (tl V1702))) (cons + ()))) ()))) (cons - ())))) (true V1702))) -(defun shen.rule->horn-clause-body (V1697 V1698 V1699) (let Variables (map shen.extract_vars V1699) (let Predicates (map (lambda X (gensym shen.cl)) V1699) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1699 Variables) (let SideLiterals (shen.construct-side-literals V1697) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1699))) V1698) (append SearchLiterals (append SideLiterals PremissLiterals))))))))) +(defun shen.rule->horn-clause-body (V1703 V1704 V1705) (let Variables (map shen.extract_vars V1705) (let Predicates (map (lambda X (gensym shen.cl)) V1705) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1705 Variables) (let SideLiterals (shen.construct-side-literals V1703) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1705))) V1704) (append SearchLiterals (append SideLiterals PremissLiterals))))))))) -(defun shen.construct-search-literals (V1704 V1705 V1706 V1707) (cond ((and (= () V1704) (= () V1705)) ()) (true (shen.csl-help V1704 V1705 V1706 V1707)))) +(defun shen.construct-search-literals (V1710 V1711 V1712 V1713) (cond ((and (= () V1710) (= () V1711)) ()) (true (shen.csl-help V1710 V1711 V1712 V1713)))) -(defun shen.csl-help (V1710 V1711 V1712 V1713) (cond ((and (= () V1710) (= () V1711)) (cons (cons bind (cons ContextOut_1957 (cons V1712 ()))) ())) ((and (cons? V1710) (cons? V1711)) (cons (cons (hd V1710) (cons V1712 (cons V1713 (hd V1711)))) (shen.csl-help (tl V1710) (tl V1711) V1713 (gensym Context)))) (true (shen.sys-error shen.csl-help)))) +(defun shen.csl-help (V1716 V1717 V1718 V1719) (cond ((and (= () V1716) (= () V1717)) (cons (cons bind (cons ContextOut_1957 (cons V1718 ()))) ())) ((and (cons? V1716) (cons? V1717)) (cons (cons (hd V1716) (cons V1718 (cons V1719 (hd V1717)))) (shen.csl-help (tl V1716) (tl V1717) V1719 (gensym Context)))) (true (shen.sys-error shen.csl-help)))) -(defun shen.construct-search-clauses (V1714 V1715 V1716) (cond ((and (= () V1714) (and (= () V1715) (= () V1716))) shen.skip) ((and (cons? V1714) (and (cons? V1715) (cons? V1716))) (do (shen.construct-search-clause (hd V1714) (hd V1715) (hd V1716)) (shen.construct-search-clauses (tl V1714) (tl V1715) (tl V1716)))) (true (shen.sys-error shen.construct-search-clauses)))) +(defun shen.construct-search-clauses (V1720 V1721 V1722) (cond ((and (= () V1720) (and (= () V1721) (= () V1722))) shen.skip) ((and (cons? V1720) (and (cons? V1721) (cons? V1722))) (do (shen.construct-search-clause (hd V1720) (hd V1721) (hd V1722)) (shen.construct-search-clauses (tl V1720) (tl V1721) (tl V1722)))) (true (shen.sys-error shen.construct-search-clauses)))) -(defun shen.construct-search-clause (V1717 V1718 V1719) (shen.s-prolog (cons (shen.construct-base-search-clause V1717 V1718 V1719) (cons (shen.construct-recursive-search-clause V1717 V1718 V1719) ())))) +(defun shen.construct-search-clause (V1723 V1724 V1725) (shen.s-prolog (cons (shen.construct-base-search-clause V1723 V1724 V1725) (cons (shen.construct-recursive-search-clause V1723 V1724 V1725) ())))) -(defun shen.construct-base-search-clause (V1720 V1721 V1722) (cons (cons V1720 (cons (cons (shen.mode-ify V1721) In_1957) (cons In_1957 V1722))) (cons :- (cons () ())))) +(defun shen.construct-base-search-clause (V1726 V1727 V1728) (cons (cons V1726 (cons (cons (shen.mode-ify V1727) In_1957) (cons In_1957 V1728))) (cons :- (cons () ())))) -(defun shen.construct-recursive-search-clause (V1723 V1724 V1725) (cons (cons V1723 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1725))) (cons :- (cons (cons (cons V1723 (cons Assumptions_1957 (cons Out_1957 V1725))) ()) ())))) +(defun shen.construct-recursive-search-clause (V1729 V1730 V1731) (cons (cons V1729 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1731))) (cons :- (cons (cons (cons V1729 (cons Assumptions_1957 (cons Out_1957 V1731))) ()) ())))) -(defun shen.construct-side-literals (V1730) (cond ((= () V1730) ()) ((and (cons? V1730) (and (cons? (hd V1730)) (and (= if (hd (hd V1730))) (and (cons? (tl (hd V1730))) (= () (tl (tl (hd V1730)))))))) (cons (cons when (tl (hd V1730))) (shen.construct-side-literals (tl V1730)))) ((and (cons? V1730) (and (cons? (hd V1730)) (and (= let (hd (hd V1730))) (and (cons? (tl (hd V1730))) (and (cons? (tl (tl (hd V1730)))) (= () (tl (tl (tl (hd V1730)))))))))) (cons (cons is (tl (hd V1730))) (shen.construct-side-literals (tl V1730)))) ((cons? V1730) (shen.construct-side-literals (tl V1730))) (true (shen.sys-error shen.construct-side-literals)))) +(defun shen.construct-side-literals (V1736) (cond ((= () V1736) ()) ((and (cons? V1736) (and (cons? (hd V1736)) (and (= if (hd (hd V1736))) (and (cons? (tl (hd V1736))) (= () (tl (tl (hd V1736)))))))) (cons (cons when (tl (hd V1736))) (shen.construct-side-literals (tl V1736)))) ((and (cons? V1736) (and (cons? (hd V1736)) (and (= let (hd (hd V1736))) (and (cons? (tl (hd V1736))) (and (cons? (tl (tl (hd V1736)))) (= () (tl (tl (tl (hd V1736)))))))))) (cons (cons is (tl (hd V1736))) (shen.construct-side-literals (tl V1736)))) ((cons? V1736) (shen.construct-side-literals (tl V1736))) (true (shen.sys-error shen.construct-side-literals)))) -(defun shen.construct-premiss-literal (V1735 V1736) (cond ((tuple? V1735) (cons shen.t* (cons (shen.recursive_cons_form (snd V1735)) (cons (shen.construct-context V1736 (fst V1735)) ())))) ((= ! V1735) (cons cut (cons Throwcontrol ()))) (true (shen.sys-error shen.construct-premiss-literal)))) +(defun shen.construct-premiss-literal (V1741 V1742) (cond ((tuple? V1741) (cons shen.t* (cons (shen.recursive_cons_form (snd V1741)) (cons (shen.construct-context V1742 (fst V1741)) ())))) ((= ! V1741) (cons cut (cons Throwcontrol ()))) (true (shen.sys-error shen.construct-premiss-literal)))) -(defun shen.construct-context (V1737 V1738) (cond ((and (= true V1737) (= () V1738)) Context_1957) ((and (= false V1737) (= () V1738)) ContextOut_1957) ((cons? V1738) (cons cons (cons (shen.recursive_cons_form (hd V1738)) (cons (shen.construct-context V1737 (tl V1738)) ())))) (true (shen.sys-error shen.construct-context)))) +(defun shen.construct-context (V1743 V1744) (cond ((and (= true V1743) (= () V1744)) Context_1957) ((and (= false V1743) (= () V1744)) ContextOut_1957) ((cons? V1744) (cons cons (cons (shen.recursive_cons_form (hd V1744)) (cons (shen.construct-context V1743 (tl V1744)) ())))) (true (shen.sys-error shen.construct-context)))) -(defun shen.recursive_cons_form (V1739) (cond ((cons? V1739) (cons cons (cons (shen.recursive_cons_form (hd V1739)) (cons (shen.recursive_cons_form (tl V1739)) ())))) (true V1739))) +(defun shen.recursive_cons_form (V1745) (cond ((cons? V1745) (cons cons (cons (shen.recursive_cons_form (hd V1745)) (cons (shen.recursive_cons_form (tl V1745)) ())))) (true V1745))) -(defun preclude (V1740) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1740)) (value shen.*datatypes*))) +(defun preclude (V1746) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1746)) (value shen.*datatypes*))) -(defun include (V1741) (let ValidTypes (intersection V1741 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*)))) +(defun include (V1747) (let ValidTypes (intersection V1747 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*)))) -(defun preclude-all-but (V1742) (preclude (difference (value shen.*alldatatypes*) V1742))) +(defun preclude-all-but (V1748) (preclude (difference (value shen.*alldatatypes*) V1748))) -(defun include-all-but (V1743) (include (difference (value shen.*alldatatypes*) V1743))) +(defun include-all-but (V1749) (include (difference (value shen.*alldatatypes*) V1749))) -(defun shen.synonyms-help (V1748) (cond ((= () V1748) synonyms) ((and (cons? V1748) (cons? (tl V1748))) (do (shen.pushnew (cons (hd V1748) (hd (tl V1748))) shen.*synonyms*) (shen.synonyms-help (tl (tl V1748))))) (true (simple-error (cn "odd number of synonyms +(defun shen.synonyms-help (V1754) (cond ((= () V1754) synonyms) ((and (cons? V1754) (cons? (tl V1754))) (do (shen.pushnew (cons (hd V1754) (shen.curry-type (hd (tl V1754)))) shen.*synonyms*) (shen.synonyms-help (tl (tl V1754))))) (true (simple-error (cn "odd number of synonyms " ""))))) -(defun shen.pushnew (V1749 V1750) (if (element? V1749 (value V1750)) (value V1750) (set V1750 (cons V1749 (value V1750))))) +(defun shen.pushnew (V1755 V1756) (if (element? V1755 (value V1756)) (value V1756) (set V1756 (cons V1755 (value V1756)))))