runold.scm

(define old-lisp-program "
DEFINE ((
(THEOREM (LAMBDA (S) (TH1 NIL NIL (CADR S) (CADDR S))))

(TH1 (LAMBDA (A1 A2 A C) (COND ((NULL A)
        (TH2 A1 A2 NIL NIL C)) (T
        (OR (MEMBER (CAR A) C) (COND ((ATOM (CAR A))
        (TH1 (COND ((MEMBER (CAR A) A1) A1)
        (T (CONS (CAR A) A1))) A2 (CDR A) C))
        (T (TH1 A1 (COND ((MEMBER (CAR A) A2) A2)
        (T (CONS (CAR A) A2))) (CDR A) C))))))))

(TH2 (LAMBDA (A1 A2 C1 C2 C) (COND
        ((NULL C) (TH A1 A2 C1 C2))
        ((ATOM (CAR C)) (TH2 A1 A2 (COND
        ((MEMBER (CAR C) C1) C1) (T
        (CONS (CAR C) C1))) C2 (CDR C)))
        (T (TH2 A1 A2 C1 (COND ((MEMBER
        (CAR C) C2) C2) (T (CONS (CAR C) C2)))
        (CDR C))))))

(TH (LAMBDA (A1 A2 C1 C2) (COND ((NULL A2) (AND (NOT (NULL C2))
        (THR (CAR C2) A1 A2 C1 (CDR C2)))) (T (THL (CAR A2) A1 (CDR A2)
        C1 C2)))))

(THL (LAMBDA (U A1 A2 C1 C2) (COND
        ((EQ (CAR U) (QUOTE NOT)) (TH1R (CADR U) A1 A2 C1 C2))
        ((EQ (CAR U) (QUOTE AND)) (TH2L (CDR U) A1 A2 C1 C2))
        ((EQ (CAR U) (QUOTE OR)) (AND (TH1L (CADR U) A1 A2 C1 C2)
        (TH1L (CADDR U) A1 A2 C1 C2) ))
        ((EQ (CAR U) (QUOTE IMPLIES)) (AND (TH1L (CADDR U) A1 A2 C1
        C2) (TH1R (CADR U) A1 A2 C1 C2) ))
        ((EQ (CAR U) (QUOTE EQUIV)) (AND (TH2L (CDR U) A1 A2 C1 C2)
        (TH2R (CDR U) A1 A2 C1 C2) ))
        (T (ERROR (LIST (QUOTE THL) U A1 A2 C1 C2)))
        )))

(THR (LAMBDA (U A1 A2 C1 C2) (COND
        ((EQ (CAR U) (QUOTE NOT)) (TH1L (CADR U) A1 A2 C1 C2))
        ((EQ (CAR U) (QUOTE AND)) (AND (TH1R (CADR U) A1 A2 C1 C2)
        (TH1R (CADDR U) A1 A2 C1 C2) ))
        ((EQ (CAR U) (QUOTE OR)) (TH2R (CDR U) A1 A2 C1 C2))
        ((EQ (CAR U) (QUOTE IMPLIES)) (TH11 (CADR U) (CADDR U)
         A1 A2 C1 C2))
        ((EQ (CAR U) (QUOTE EQUIV)) (AND (TH11 (CADR U) (CADDR U)
        A1 A2 C1 C2) (TH11 (CADDR U) (CADR U) A1 A2 C1 C2) ))
        (T (ERROR (LIST (QUOTE THR) U A1 A2 C1 C2)))
        )))

(TH1L (LAMBDA (V A1 A2 C1 C2) (COND
        ((ATOM V) (OR (MEMBER V C1)
        (TH (CONS V A1) A2 C1 C2) ))
        (T (OR (MEMBER V C2) (TH A1 (CONS V A2) C1 C2) ))
        )))

(TH1R (LAMBDA (V A1 A2 C1 C2) (COND
        ((ATOM V) (OR (MEMBER V A1)
        (TH A1 A2 (CONS V C1) C2) ))
        (T (OR (MEMBER V A2) (TH A1 A2 C1 (CONS V C2))))
        )))

(TH2L (LAMBDA (V A1 A2 C1 C2) (COND
        ((ATOM (CAR V)) (OR (MEMBER (CAR V) C1)
        (TH1L (CADR V) (CONS (CAR V) A1) A2 C1 C2)))
        (T (OR (MEMBER (CAR V) C2) (TH1L (CADR V) A1 (CONS (CAR V)
        A2) C1 C2)))
        )))

(TH2R (LAMBDA (V A1 A2 C1 C2) (COND
        ((ATOM (CAR V)) (OR (MEMBER (CAR V) A1)
        (TH1R (CADR V) A1 A2 (CONS (CAR V) C1) C2)))
        (T (OR (MEMBER (CAR V) A2) (TH1R (CADR V) A1 A2 C1
        (CONS (CAR V) C2))))
        )))

(TH11 (LAMBDA (VI V2 A1 A2 C1 C2) (COND
        ((ATOM VI) (OR (MEMBER VI C1) (TH1R V2 (CONS VI A1) A2 C1
        C2)))
        (T (OR (MEMBER VI C2) (TH1R V2 A1 (CONS VI A2) C1 C2)))
        )))
))

THEOREM
((ARROW (P) ((OR P Q))))

THEOREM
((ARROW ((OR A (NOT B))) ((IMPLIES (AND P Q) (EQUIV P Q))) ))
")

(define eq eq?)
(define (atom x) (not (pair? x)))
(define null null?)
(define nil '())
(define t #t)

(read-enable 'case-insensitive)

(with-input-from-string old-lisp-program
  (lambda ()
    (let loop ()
      (let* ((command (read))
             (args (read)))
        (cond ((eof-object? args)
               (values))
              ((eq? command 'define)
               (for-each (lambda (definition)
                           (eval `(define . ,definition) (current-module)))
                         (car args))
               (loop))
              (else
               (display `(,command (quote . ,args)))
               (display " => ")
               (display (eval `(,command (quote . ,args)) (current-module)))
               (newline)
               (loop)))))))

;;; Outputs:
;; (theorem (quote (arrow (p) ((or p q))))) => (p)
;; (theorem (quote (arrow ((or a (not b))) ((implies (and p q) (equiv p q)))))) => (p)