shen/release/klambda/sequent.kl in shen-ruby-0.13.0 vs shen/release/klambda/sequent.kl in shen-ruby-0.14.0

- old
+ new

@@ -21,121 +21,121 @@ LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE." -(defun shen.datatype-error (V1329) (cond ((and (cons? V1329) (and (cons? (tl V1329)) (= () (tl (tl V1329))))) (simple-error (cn "datatype syntax error here: +(defun shen.datatype-error (V1370) (cond ((and (cons? V1370) (and (cons? (tl V1370)) (= () (tl (tl V1370))))) (simple-error (cn "datatype syntax error here: - " (shen.app (shen.next-50 50 (hd V1329)) " + " (shen.app (shen.next-50 50 (hd V1370)) " " shen.a)))) (true (shen.f_error shen.datatype-error)))) -(defun shen.<datatype-rules> (V1330) (let YaccParse (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1330) (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 (= YaccParse (fail)) (let Parse_<e> (<e> V1330) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse))) +(defun shen.<datatype-rules> (V1371) (let YaccParse (let Parse_shen.<datatype-rule> (shen.<datatype-rule> V1371) (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 (= YaccParse (fail)) (let Parse_<e> (<e> V1371) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse))) -(defun shen.<datatype-rule> (V1331) (let YaccParse (let Parse_shen.<side-conditions> (shen.<side-conditions> V1331) (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 (= YaccParse (fail)) (let Parse_shen.<side-conditions> (shen.<side-conditions> V1331) (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))) YaccParse))) +(defun shen.<datatype-rule> (V1372) (let YaccParse (let Parse_shen.<side-conditions> (shen.<side-conditions> V1372) (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 (= YaccParse (fail)) (let Parse_shen.<side-conditions> (shen.<side-conditions> V1372) (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))) YaccParse))) -(defun shen.<side-conditions> (V1332) (let YaccParse (let Parse_shen.<side-condition> (shen.<side-condition> V1332) (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 (= YaccParse (fail)) (let Parse_<e> (<e> V1332) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse))) +(defun shen.<side-conditions> (V1373) (let YaccParse (let Parse_shen.<side-condition> (shen.<side-condition> V1373) (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 (= YaccParse (fail)) (let Parse_<e> (<e> V1373) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse))) -(defun shen.<side-condition> (V1333) (let YaccParse (if (and (cons? (hd V1333)) (= if (hd (hd V1333)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1333)) (shen.hdtl V1333))) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (cons if (cons (shen.hdtl Parse_shen.<expr>) ()))) (fail))) (fail)) (if (= YaccParse (fail)) (if (and (cons? (hd V1333)) (= let (hd (hd V1333)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1333)) (shen.hdtl V1333))) (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)) YaccParse))) +(defun shen.<side-condition> (V1374) (let YaccParse (if (and (cons? (hd V1374)) (= if (hd (hd V1374)))) (let Parse_shen.<expr> (shen.<expr> (shen.pair (tl (hd V1374)) (shen.hdtl V1374))) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (cons if (cons (shen.hdtl Parse_shen.<expr>) ()))) (fail))) (fail)) (if (= YaccParse (fail)) (if (and (cons? (hd V1374)) (= let (hd (hd V1374)))) (let Parse_shen.<variable?> (shen.<variable?> (shen.pair (tl (hd V1374)) (shen.hdtl V1374))) (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)) YaccParse))) -(defun shen.<variable?> (V1334) (if (cons? (hd V1334)) (let Parse_X (hd (hd V1334)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1334)) (shen.hdtl V1334))) Parse_X) (fail))) (fail))) +(defun shen.<variable?> (V1375) (if (cons? (hd V1375)) (let Parse_X (hd (hd V1375)) (if (variable? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1375)) (shen.hdtl V1375))) Parse_X) (fail))) (fail))) -(defun shen.<expr> (V1335) (if (cons? (hd V1335)) (let Parse_X (hd (hd V1335)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1335)) (shen.hdtl V1335))) (shen.remove-bar Parse_X)) (fail))) (fail))) +(defun shen.<expr> (V1376) (if (cons? (hd V1376)) (let Parse_X (hd (hd V1376)) (if (not (or (element? Parse_X (cons >> (cons ; ()))) (or (shen.singleunderline? Parse_X) (shen.doubleunderline? Parse_X)))) (shen.pair (hd (shen.pair (tl (hd V1376)) (shen.hdtl V1376))) (shen.remove-bar Parse_X)) (fail))) (fail))) -(defun shen.remove-bar (V1336) (cond ((and (cons? V1336) (and (cons? (tl V1336)) (and (cons? (tl (tl V1336))) (and (= () (tl (tl (tl V1336)))) (= (hd (tl V1336)) bar!))))) (cons (hd V1336) (hd (tl (tl V1336))))) ((cons? V1336) (cons (shen.remove-bar (hd V1336)) (shen.remove-bar (tl V1336)))) (true V1336))) +(defun shen.remove-bar (V1377) (cond ((and (cons? V1377) (and (cons? (tl V1377)) (and (cons? (tl (tl V1377))) (and (= () (tl (tl (tl V1377)))) (= (hd (tl V1377)) bar!))))) (cons (hd V1377) (hd (tl (tl V1377))))) ((cons? V1377) (cons (shen.remove-bar (hd V1377)) (shen.remove-bar (tl V1377)))) (true V1377))) -(defun shen.<premises> (V1337) (let YaccParse (let Parse_shen.<premise> (shen.<premise> V1337) (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 (= YaccParse (fail)) (let Parse_<e> (<e> V1337) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse))) +(defun shen.<premises> (V1378) (let YaccParse (let Parse_shen.<premise> (shen.<premise> V1378) (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 (= YaccParse (fail)) (let Parse_<e> (<e> V1378) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse))) -(defun shen.<semicolon-symbol> (V1338) (if (cons? (hd V1338)) (let Parse_X (hd (hd V1338)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1338)) (shen.hdtl V1338))) shen.skip) (fail))) (fail))) +(defun shen.<semicolon-symbol> (V1379) (if (cons? (hd V1379)) (let Parse_X (hd (hd V1379)) (if (= Parse_X ;) (shen.pair (hd (shen.pair (tl (hd V1379)) (shen.hdtl V1379))) shen.skip) (fail))) (fail))) -(defun shen.<premise> (V1339) (let YaccParse (if (and (cons? (hd V1339)) (= ! (hd (hd V1339)))) (shen.pair (hd (shen.pair (tl (hd V1339)) (shen.hdtl V1339))) !) (fail)) (if (= YaccParse (fail)) (let YaccParse (let Parse_shen.<formulae> (shen.<formulae> V1339) (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 (= YaccParse (fail)) (let Parse_shen.<formula> (shen.<formula> V1339) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (shen.sequent () (shen.hdtl Parse_shen.<formula>))) (fail))) YaccParse)) YaccParse))) +(defun shen.<premise> (V1380) (let YaccParse (if (and (cons? (hd V1380)) (= ! (hd (hd V1380)))) (shen.pair (hd (shen.pair (tl (hd V1380)) (shen.hdtl V1380))) !) (fail)) (if (= YaccParse (fail)) (let YaccParse (let Parse_shen.<formulae> (shen.<formulae> V1380) (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 (= YaccParse (fail)) (let Parse_shen.<formula> (shen.<formula> V1380) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (shen.sequent () (shen.hdtl Parse_shen.<formula>))) (fail))) YaccParse)) YaccParse))) -(defun shen.<conclusion> (V1340) (let YaccParse (let Parse_shen.<formulae> (shen.<formulae> V1340) (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 (= YaccParse (fail)) (let Parse_shen.<formula> (shen.<formula> V1340) (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))) YaccParse))) +(defun shen.<conclusion> (V1381) (let YaccParse (let Parse_shen.<formulae> (shen.<formulae> V1381) (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 (= YaccParse (fail)) (let Parse_shen.<formula> (shen.<formula> V1381) (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))) YaccParse))) -(defun shen.sequent (V1341 V1342) (@p V1341 V1342)) +(defun shen.sequent (V1382 V1383) (@p V1382 V1383)) -(defun shen.<formulae> (V1343) (let YaccParse (let Parse_shen.<formula> (shen.<formula> V1343) (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 (= YaccParse (fail)) (let YaccParse (let Parse_shen.<formula> (shen.<formula> V1343) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (cons (shen.hdtl Parse_shen.<formula>) ())) (fail))) (if (= YaccParse (fail)) (let Parse_<e> (<e> V1343) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)) YaccParse))) +(defun shen.<formulae> (V1384) (let YaccParse (let Parse_shen.<formula> (shen.<formula> V1384) (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 (= YaccParse (fail)) (let YaccParse (let Parse_shen.<formula> (shen.<formula> V1384) (if (not (= (fail) Parse_shen.<formula>)) (shen.pair (hd Parse_shen.<formula>) (cons (shen.hdtl Parse_shen.<formula>) ())) (fail))) (if (= YaccParse (fail)) (let Parse_<e> (<e> V1384) (if (not (= (fail) Parse_<e>)) (shen.pair (hd Parse_<e>) ()) (fail))) YaccParse)) YaccParse))) -(defun shen.<comma-symbol> (V1344) (if (cons? (hd V1344)) (let Parse_X (hd (hd V1344)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1344)) (shen.hdtl V1344))) shen.skip) (fail))) (fail))) +(defun shen.<comma-symbol> (V1385) (if (cons? (hd V1385)) (let Parse_X (hd (hd V1385)) (if (= Parse_X (intern ",")) (shen.pair (hd (shen.pair (tl (hd V1385)) (shen.hdtl V1385))) shen.skip) (fail))) (fail))) -(defun shen.<formula> (V1345) (let YaccParse (let Parse_shen.<expr> (shen.<expr> V1345) (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 (= YaccParse (fail)) (let Parse_shen.<expr> (shen.<expr> V1345) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.hdtl Parse_shen.<expr>)) (fail))) YaccParse))) +(defun shen.<formula> (V1386) (let YaccParse (let Parse_shen.<expr> (shen.<expr> V1386) (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 (= YaccParse (fail)) (let Parse_shen.<expr> (shen.<expr> V1386) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.hdtl Parse_shen.<expr>)) (fail))) YaccParse))) -(defun shen.<type> (V1346) (let Parse_shen.<expr> (shen.<expr> V1346) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.curry-type (shen.hdtl Parse_shen.<expr>))) (fail)))) +(defun shen.<type> (V1387) (let Parse_shen.<expr> (shen.<expr> V1387) (if (not (= (fail) Parse_shen.<expr>)) (shen.pair (hd Parse_shen.<expr>) (shen.curry-type (shen.hdtl Parse_shen.<expr>))) (fail)))) -(defun shen.<doubleunderline> (V1347) (if (cons? (hd V1347)) (let Parse_X (hd (hd V1347)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1347)) (shen.hdtl V1347))) Parse_X) (fail))) (fail))) +(defun shen.<doubleunderline> (V1388) (if (cons? (hd V1388)) (let Parse_X (hd (hd V1388)) (if (shen.doubleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1388)) (shen.hdtl V1388))) Parse_X) (fail))) (fail))) -(defun shen.<singleunderline> (V1348) (if (cons? (hd V1348)) (let Parse_X (hd (hd V1348)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1348)) (shen.hdtl V1348))) Parse_X) (fail))) (fail))) +(defun shen.<singleunderline> (V1389) (if (cons? (hd V1389)) (let Parse_X (hd (hd V1389)) (if (shen.singleunderline? Parse_X) (shen.pair (hd (shen.pair (tl (hd V1389)) (shen.hdtl V1389))) Parse_X) (fail))) (fail))) -(defun shen.singleunderline? (V1349) (and (symbol? V1349) (shen.sh? (str V1349)))) +(defun shen.singleunderline? (V1390) (and (symbol? V1390) (shen.sh? (str V1390)))) -(defun shen.sh? (V1350) (cond ((= "_" V1350) true) (true (and (= (pos V1350 0) "_") (shen.sh? (tlstr V1350)))))) +(defun shen.sh? (V1391) (cond ((= "_" V1391) true) (true (and (= (pos V1391 0) "_") (shen.sh? (tlstr V1391)))))) -(defun shen.doubleunderline? (V1351) (and (symbol? V1351) (shen.dh? (str V1351)))) +(defun shen.doubleunderline? (V1392) (and (symbol? V1392) (shen.dh? (str V1392)))) -(defun shen.dh? (V1352) (cond ((= "=" V1352) true) (true (and (= (pos V1352 0) "=") (shen.dh? (tlstr V1352)))))) +(defun shen.dh? (V1393) (cond ((= "=" V1393) true) (true (and (= (pos V1393 0) "=") (shen.dh? (tlstr V1393)))))) -(defun shen.process-datatype (V1353 V1354) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1353 V1354)))) +(defun shen.process-datatype (V1394 V1395) (shen.remember-datatype (shen.s-prolog (shen.rules->horn-clauses V1394 V1395)))) -(defun shen.remember-datatype (V1359) (cond ((cons? V1359) (do (set shen.*datatypes* (adjoin (hd V1359) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1359) (value shen.*alldatatypes*))) (hd V1359)))) (true (shen.f_error shen.remember-datatype)))) +(defun shen.remember-datatype (V1400) (cond ((cons? V1400) (do (set shen.*datatypes* (adjoin (hd V1400) (value shen.*datatypes*))) (do (set shen.*alldatatypes* (adjoin (hd V1400) (value shen.*alldatatypes*))) (hd V1400)))) (true (shen.f_error shen.remember-datatype)))) -(defun shen.rules->horn-clauses (V1362 V1363) (cond ((= () V1363) ()) ((and (cons? V1363) (and (tuple? (hd V1363)) (= shen.single (fst (hd V1363))))) (cons (shen.rule->horn-clause V1362 (snd (hd V1363))) (shen.rules->horn-clauses V1362 (tl V1363)))) ((and (cons? V1363) (and (tuple? (hd V1363)) (= shen.double (fst (hd V1363))))) (shen.rules->horn-clauses V1362 (append (shen.double->singles (snd (hd V1363))) (tl V1363)))) (true (shen.f_error shen.rules->horn-clauses)))) +(defun shen.rules->horn-clauses (V1403 V1404) (cond ((= () V1404) ()) ((and (cons? V1404) (and (tuple? (hd V1404)) (= shen.single (fst (hd V1404))))) (cons (shen.rule->horn-clause V1403 (snd (hd V1404))) (shen.rules->horn-clauses V1403 (tl V1404)))) ((and (cons? V1404) (and (tuple? (hd V1404)) (= shen.double (fst (hd V1404))))) (shen.rules->horn-clauses V1403 (append (shen.double->singles (snd (hd V1404))) (tl V1404)))) (true (shen.f_error shen.rules->horn-clauses)))) -(defun shen.double->singles (V1364) (cons (shen.right-rule V1364) (cons (shen.left-rule V1364) ()))) +(defun shen.double->singles (V1405) (cons (shen.right-rule V1405) (cons (shen.left-rule V1405) ()))) -(defun shen.right-rule (V1365) (@p shen.single V1365)) +(defun shen.right-rule (V1406) (@p shen.single V1406)) -(defun shen.left-rule (V1366) (cond ((and (cons? V1366) (and (cons? (tl V1366)) (and (cons? (tl (tl V1366))) (and (tuple? (hd (tl (tl V1366)))) (and (= () (fst (hd (tl (tl V1366))))) (= () (tl (tl (tl V1366))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1366)))) ()) Q) (let NewPremises (cons (@p (map shen.right->left (hd (tl V1366))) Q) ()) (@p shen.single (cons (hd V1366) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.f_error shen.left-rule)))) +(defun shen.left-rule (V1407) (cond ((and (cons? V1407) (and (cons? (tl V1407)) (and (cons? (tl (tl V1407))) (and (tuple? (hd (tl (tl V1407)))) (and (= () (fst (hd (tl (tl V1407))))) (= () (tl (tl (tl V1407))))))))) (let Q (gensym Qv) (let NewConclusion (@p (cons (snd (hd (tl (tl V1407)))) ()) Q) (let NewPremises (cons (@p (map (lambda V1359 (shen.right->left V1359)) (hd (tl V1407))) Q) ()) (@p shen.single (cons (hd V1407) (cons NewPremises (cons NewConclusion ())))))))) (true (shen.f_error shen.left-rule)))) -(defun shen.right->left (V1371) (cond ((and (tuple? V1371) (= () (fst V1371))) (snd V1371)) (true (simple-error "syntax error with ========== +(defun shen.right->left (V1412) (cond ((and (tuple? V1412) (= () (fst V1412))) (snd V1412)) (true (simple-error "syntax error with ========== ")))) -(defun shen.rule->horn-clause (V1372 V1373) (cond ((and (cons? V1373) (and (cons? (tl V1373)) (and (cons? (tl (tl V1373))) (and (tuple? (hd (tl (tl V1373)))) (= () (tl (tl (tl V1373)))))))) (cons (shen.rule->horn-clause-head V1372 (snd (hd (tl (tl V1373))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1373) (hd (tl V1373)) (fst (hd (tl (tl V1373))))) ())))) (true (shen.f_error shen.rule->horn-clause)))) +(defun shen.rule->horn-clause (V1413 V1414) (cond ((and (cons? V1414) (and (cons? (tl V1414)) (and (cons? (tl (tl V1414))) (and (tuple? (hd (tl (tl V1414)))) (= () (tl (tl (tl V1414)))))))) (cons (shen.rule->horn-clause-head V1413 (snd (hd (tl (tl V1414))))) (cons :- (cons (shen.rule->horn-clause-body (hd V1414) (hd (tl V1414)) (fst (hd (tl (tl V1414))))) ())))) (true (shen.f_error shen.rule->horn-clause)))) -(defun shen.rule->horn-clause-head (V1374 V1375) (cons V1374 (cons (shen.mode-ify V1375) (cons Context_1957 ())))) +(defun shen.rule->horn-clause-head (V1415 V1416) (cons V1415 (cons (shen.mode-ify V1416) (cons Context_1957 ())))) -(defun shen.mode-ify (V1376) (cond ((and (cons? V1376) (and (cons? (tl V1376)) (and (= : (hd (tl V1376))) (and (cons? (tl (tl V1376))) (= () (tl (tl (tl V1376)))))))) (cons mode (cons (cons (hd V1376) (cons : (cons (cons mode (cons (hd (tl (tl V1376))) (cons + ()))) ()))) (cons - ())))) (true V1376))) +(defun shen.mode-ify (V1417) (cond ((and (cons? V1417) (and (cons? (tl V1417)) (and (= : (hd (tl V1417))) (and (cons? (tl (tl V1417))) (= () (tl (tl (tl V1417)))))))) (cons mode (cons (cons (hd V1417) (cons : (cons (cons mode (cons (hd (tl (tl V1417))) (cons + ()))) ()))) (cons - ())))) (true V1417))) -(defun shen.rule->horn-clause-body (V1377 V1378 V1379) (let Variables (map shen.extract_vars V1379) (let Predicates (map (lambda X (gensym shen.cl)) V1379) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1379 Variables) (let SideLiterals (shen.construct-side-literals V1377) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1379))) V1378) (append SearchLiterals (append SideLiterals PremissLiterals))))))))) +(defun shen.rule->horn-clause-body (V1418 V1419 V1420) (let Variables (map (lambda V1360 (shen.extract_vars V1360)) V1420) (let Predicates (map (lambda X (gensym shen.cl)) V1420) (let SearchLiterals (shen.construct-search-literals Predicates Variables Context_1957 Context1_1957) (let SearchClauses (shen.construct-search-clauses Predicates V1420 Variables) (let SideLiterals (shen.construct-side-literals V1418) (let PremissLiterals (map (lambda X (shen.construct-premiss-literal X (empty? V1420))) V1419) (append SearchLiterals (append SideLiterals PremissLiterals))))))))) -(defun shen.construct-search-literals (V1384 V1385 V1386 V1387) (cond ((and (= () V1384) (= () V1385)) ()) (true (shen.csl-help V1384 V1385 V1386 V1387)))) +(defun shen.construct-search-literals (V1425 V1426 V1427 V1428) (cond ((and (= () V1425) (= () V1426)) ()) (true (shen.csl-help V1425 V1426 V1427 V1428)))) -(defun shen.csl-help (V1390 V1391 V1392 V1393) (cond ((and (= () V1390) (= () V1391)) (cons (cons bind (cons ContextOut_1957 (cons V1392 ()))) ())) ((and (cons? V1390) (cons? V1391)) (cons (cons (hd V1390) (cons V1392 (cons V1393 (hd V1391)))) (shen.csl-help (tl V1390) (tl V1391) V1393 (gensym Context)))) (true (shen.f_error shen.csl-help)))) +(defun shen.csl-help (V1431 V1432 V1433 V1434) (cond ((and (= () V1431) (= () V1432)) (cons (cons bind (cons ContextOut_1957 (cons V1433 ()))) ())) ((and (cons? V1431) (cons? V1432)) (cons (cons (hd V1431) (cons V1433 (cons V1434 (hd V1432)))) (shen.csl-help (tl V1431) (tl V1432) V1434 (gensym Context)))) (true (shen.f_error shen.csl-help)))) -(defun shen.construct-search-clauses (V1394 V1395 V1396) (cond ((and (= () V1394) (and (= () V1395) (= () V1396))) shen.skip) ((and (cons? V1394) (and (cons? V1395) (cons? V1396))) (do (shen.construct-search-clause (hd V1394) (hd V1395) (hd V1396)) (shen.construct-search-clauses (tl V1394) (tl V1395) (tl V1396)))) (true (shen.f_error shen.construct-search-clauses)))) +(defun shen.construct-search-clauses (V1435 V1436 V1437) (cond ((and (= () V1435) (and (= () V1436) (= () V1437))) shen.skip) ((and (cons? V1435) (and (cons? V1436) (cons? V1437))) (do (shen.construct-search-clause (hd V1435) (hd V1436) (hd V1437)) (shen.construct-search-clauses (tl V1435) (tl V1436) (tl V1437)))) (true (shen.f_error shen.construct-search-clauses)))) -(defun shen.construct-search-clause (V1397 V1398 V1399) (shen.s-prolog (cons (shen.construct-base-search-clause V1397 V1398 V1399) (cons (shen.construct-recursive-search-clause V1397 V1398 V1399) ())))) +(defun shen.construct-search-clause (V1438 V1439 V1440) (shen.s-prolog (cons (shen.construct-base-search-clause V1438 V1439 V1440) (cons (shen.construct-recursive-search-clause V1438 V1439 V1440) ())))) -(defun shen.construct-base-search-clause (V1400 V1401 V1402) (cons (cons V1400 (cons (cons (shen.mode-ify V1401) In_1957) (cons In_1957 V1402))) (cons :- (cons () ())))) +(defun shen.construct-base-search-clause (V1441 V1442 V1443) (cons (cons V1441 (cons (cons (shen.mode-ify V1442) In_1957) (cons In_1957 V1443))) (cons :- (cons () ())))) -(defun shen.construct-recursive-search-clause (V1403 V1404 V1405) (cons (cons V1403 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1405))) (cons :- (cons (cons (cons V1403 (cons Assumptions_1957 (cons Out_1957 V1405))) ()) ())))) +(defun shen.construct-recursive-search-clause (V1444 V1445 V1446) (cons (cons V1444 (cons (cons Assumption_1957 Assumptions_1957) (cons (cons Assumption_1957 Out_1957) V1446))) (cons :- (cons (cons (cons V1444 (cons Assumptions_1957 (cons Out_1957 V1446))) ()) ())))) -(defun shen.construct-side-literals (V1410) (cond ((= () V1410) ()) ((and (cons? V1410) (and (cons? (hd V1410)) (and (= if (hd (hd V1410))) (and (cons? (tl (hd V1410))) (= () (tl (tl (hd V1410)))))))) (cons (cons when (tl (hd V1410))) (shen.construct-side-literals (tl V1410)))) ((and (cons? V1410) (and (cons? (hd V1410)) (and (= let (hd (hd V1410))) (and (cons? (tl (hd V1410))) (and (cons? (tl (tl (hd V1410)))) (= () (tl (tl (tl (hd V1410)))))))))) (cons (cons is (tl (hd V1410))) (shen.construct-side-literals (tl V1410)))) ((cons? V1410) (shen.construct-side-literals (tl V1410))) (true (shen.f_error shen.construct-side-literals)))) +(defun shen.construct-side-literals (V1451) (cond ((= () V1451) ()) ((and (cons? V1451) (and (cons? (hd V1451)) (and (= if (hd (hd V1451))) (and (cons? (tl (hd V1451))) (= () (tl (tl (hd V1451)))))))) (cons (cons when (tl (hd V1451))) (shen.construct-side-literals (tl V1451)))) ((and (cons? V1451) (and (cons? (hd V1451)) (and (= let (hd (hd V1451))) (and (cons? (tl (hd V1451))) (and (cons? (tl (tl (hd V1451)))) (= () (tl (tl (tl (hd V1451)))))))))) (cons (cons is (tl (hd V1451))) (shen.construct-side-literals (tl V1451)))) ((cons? V1451) (shen.construct-side-literals (tl V1451))) (true (shen.f_error shen.construct-side-literals)))) -(defun shen.construct-premiss-literal (V1415 V1416) (cond ((tuple? V1415) (cons shen.t* (cons (shen.recursive_cons_form (snd V1415)) (cons (shen.construct-context V1416 (fst V1415)) ())))) ((= ! V1415) (cons cut (cons Throwcontrol ()))) (true (shen.f_error shen.construct-premiss-literal)))) +(defun shen.construct-premiss-literal (V1456 V1457) (cond ((tuple? V1456) (cons shen.t* (cons (shen.recursive_cons_form (snd V1456)) (cons (shen.construct-context V1457 (fst V1456)) ())))) ((= ! V1456) (cons cut (cons Throwcontrol ()))) (true (shen.f_error shen.construct-premiss-literal)))) -(defun shen.construct-context (V1417 V1418) (cond ((and (= true V1417) (= () V1418)) Context_1957) ((and (= false V1417) (= () V1418)) ContextOut_1957) ((cons? V1418) (cons cons (cons (shen.recursive_cons_form (hd V1418)) (cons (shen.construct-context V1417 (tl V1418)) ())))) (true (shen.f_error shen.construct-context)))) +(defun shen.construct-context (V1458 V1459) (cond ((and (= true V1458) (= () V1459)) Context_1957) ((and (= false V1458) (= () V1459)) ContextOut_1957) ((cons? V1459) (cons cons (cons (shen.recursive_cons_form (hd V1459)) (cons (shen.construct-context V1458 (tl V1459)) ())))) (true (shen.f_error shen.construct-context)))) -(defun shen.recursive_cons_form (V1419) (cond ((cons? V1419) (cons cons (cons (shen.recursive_cons_form (hd V1419)) (cons (shen.recursive_cons_form (tl V1419)) ())))) (true V1419))) +(defun shen.recursive_cons_form (V1460) (cond ((cons? V1460) (cons cons (cons (shen.recursive_cons_form (hd V1460)) (cons (shen.recursive_cons_form (tl V1460)) ())))) (true V1460))) -(defun preclude (V1420) (shen.preclude-h (map shen.intern-type V1420))) +(defun preclude (V1461) (shen.preclude-h (map (lambda V1361 (shen.intern-type V1361)) V1461))) -(defun shen.preclude-h (V1421) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1421)) (value shen.*datatypes*))) +(defun shen.preclude-h (V1462) (let FilterDatatypes (set shen.*datatypes* (difference (value shen.*datatypes*) V1462)) (value shen.*datatypes*))) -(defun include (V1422) (shen.include-h (map shen.intern-type V1422))) +(defun include (V1463) (shen.include-h (map (lambda V1362 (shen.intern-type V1362)) V1463))) -(defun shen.include-h (V1423) (let ValidTypes (intersection V1423 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*)))) +(defun shen.include-h (V1464) (let ValidTypes (intersection V1464 (value shen.*alldatatypes*)) (let NewDatatypes (set shen.*datatypes* (union ValidTypes (value shen.*datatypes*))) (value shen.*datatypes*)))) -(defun preclude-all-but (V1424) (shen.preclude-h (difference (value shen.*alldatatypes*) (map shen.intern-type V1424)))) +(defun preclude-all-but (V1465) (shen.preclude-h (difference (value shen.*alldatatypes*) (map (lambda V1363 (shen.intern-type V1363)) V1465)))) -(defun include-all-but (V1425) (shen.include-h (difference (value shen.*alldatatypes*) (map shen.intern-type V1425)))) +(defun include-all-but (V1466) (shen.include-h (difference (value shen.*alldatatypes*) (map (lambda V1364 (shen.intern-type V1364)) V1466)))) -(defun shen.synonyms-help (V1430) (cond ((= () V1430) (shen.demodulation-function (value shen.*tc*) (mapcan shen.demod-rule (value shen.*synonyms*)))) ((and (cons? V1430) (cons? (tl V1430))) (let Vs (difference (shen.extract_vars (hd (tl V1430))) (shen.extract_vars (hd V1430))) (if (empty? Vs) (do (shen.pushnew (cons (hd V1430) (cons (hd (tl V1430)) ())) shen.*synonyms*) (shen.synonyms-help (tl (tl V1430)))) (shen.free_variable_warnings (hd (tl V1430)) Vs)))) (true (simple-error "odd number of synonyms +(defun shen.synonyms-help (V1471) (cond ((= () V1471) (shen.demodulation-function (value shen.*tc*) (mapcan (lambda V1365 (shen.demod-rule V1365)) (value shen.*synonyms*)))) ((and (cons? V1471) (cons? (tl V1471))) (let Vs (difference (shen.extract_vars (hd (tl V1471))) (shen.extract_vars (hd V1471))) (if (empty? Vs) (do (shen.pushnew (cons (hd V1471) (cons (hd (tl V1471)) ())) shen.*synonyms*) (shen.synonyms-help (tl (tl V1471)))) (shen.free_variable_warnings (hd (tl V1471)) Vs)))) (true (simple-error "odd number of synonyms ")))) -(defun shen.pushnew (V1431 V1432) (if (element? V1431 (value V1432)) (value V1432) (set V1432 (cons V1431 (value V1432))))) +(defun shen.pushnew (V1472 V1473) (if (element? V1472 (value V1473)) (value V1473) (set V1473 (cons V1472 (value V1473))))) -(defun shen.demod-rule (V1433) (cond ((and (cons? V1433) (and (cons? (tl V1433)) (= () (tl (tl V1433))))) (cons (shen.rcons_form (hd V1433)) (cons -> (cons (shen.rcons_form (hd (tl V1433))) ())))) (true (shen.f_error shen.demod-rule)))) +(defun shen.demod-rule (V1474) (cond ((and (cons? V1474) (and (cons? (tl V1474)) (= () (tl (tl V1474))))) (cons (shen.rcons_form (hd V1474)) (cons -> (cons (shen.rcons_form (hd (tl V1474))) ())))) (true (shen.f_error shen.demod-rule)))) -(defun shen.demodulation-function (V1434 V1435) (do (tc -) (do (eval (cons define (cons shen.demod (append V1435 (shen.default-rule))))) (do (if V1434 (tc +) shen.skip) synonyms)))) +(defun shen.demodulation-function (V1475 V1476) (do (tc -) (do (eval (cons define (cons shen.demod (append V1476 (shen.default-rule))))) (do (if V1475 (tc +) shen.skip) synonyms)))) (defun shen.default-rule () (cons X (cons -> (cons X ()))))