(loader '((title |boyer.lo|)))
(loader'((fentry check-boyer subr0)
(entry check-boyer subr0)
(mov 't a2)
(mov '(test-boyer 1) a1)
(jmp check-value)
))
(loader'((fentry meter-boyer subr0)
(entry meter-boyer subr0)
(mov 'boyer a2)
(mov '(boyer) a1)
(jmp perform-meter)
))
(loader'((fentry test-boyer subr1)
(entry test-boyer subr1)
(cabne a1 '1 104)
(bra boyer)
103
(push a1)
(call boyer)
(pop a1)
104
(sobgez a1 103)
(mov 't a1)
(return)
))
(defvar unify-subst nil)
(defvar temp-temp nil)
(loader'((entry add-lemma subr1)
(bfcons a1 101)
(cabne (car a1) 'equal 101)
(mov (cdr a1) a4)
(bfcons (car a4) 101)
(mov (cdr a1) a4)
(mov (car a4) a4)
(push (car a4))
(push 'lemmas)
(push a1)
(mov (cdr a1) a1)
(mov (car a1) a1)
(mov 'lemmas a2)
(mov (car a1) a1)
(jcall get)
(mov a1 a2)
(pop a1)
(jcall cons)
(mov (& 0) a3)
(mov a1 a2)
(mov (& 1) a1)
(adjstk '2)
(jmp putprop)
101
(mov nil a3)
(mov a1 a2)
(mov '"%ADD-LEMMA did not like the term:" a1)
(jmp error)
))
(loader'((entry add-lemma-lst subr1)
(push a1)
(bfnil a1 101)
(mov 't a1)
(adjstk '1)
(return)
101
(mov (car a1) a1)
(call add-lemma)
(mov (& 0) a1)
(mov (cdr a1) a1)
(adjstk '1)
(bra add-lemma-lst)
))
(loader'((entry apply-subst subr2)
(push a2)
(btcons a2 101)
(push a2)
(mov a1 a2)
(pop a1)
(jcall assq)
(mov a1 (cvalq temp-temp))
(btnil a1 103)
(mov (cdr a1) a1)
(adjstk '1)
(return)
103
(mov (& 0) a1)
(adjstk '1)
(return)
101
(push (car a2))
(mov (cdr a2) a2)
(call apply-subst-lst)
(mov a1 a2)
(pop a1)
(adjstk '1)
(jmp cons)
))
(loader'((entry apply-subst-lst subr2)
(push a2)
(push a1)
(bfnil a2 101)
(mov nil a1)
(adjstk '2)
(return)
101
(mov (car a2) a2)
(call apply-subst)
(push a1)
(mov (& 2) a2)
(mov (cdr a2) a2)
(mov (& 1) a1)
(call apply-subst-lst)
(mov a1 a2)
(pop a1)
(adjstk '2)
(jmp cons)
))
(loader'((entry falsep subr2)
(push a2)
(push a1)
(mov '(f) a2)
(jcall equal)
(bfnil a1 101)
(mov (& 1) a2)
(mov (& 0) a1)
(adjstk '2)
(jmp member)
101
(adjstk '2)
(return)
))
(loader'((entry one-way-unify subr2)
(mov nil (cvalq unify-subst))
(bra one-way-unify1)
))
(loader'((entry one-way-unify1 subr2)
(push a2)
(push a1)
(btcons a2 101)
(push a2)
(mov (cvalq unify-subst) a2)
(pop a1)
(jcall assq)
(mov a1 (cvalq temp-temp))
(btnil a1 103)
(mov (cdr a1) a2)
(mov (& 0) a1)
(adjstk '2)
(jmp equal)
103
(mov (& 0) a2)
(mov (& 1) a1)
(jcall cons)
(mov (cvalq unify-subst) a2)
(jcall cons)
(mov a1 (cvalq unify-subst))
(mov 't a1)
(adjstk '2)
(return)
101
(btcons a1 105)
(mov nil a1)
(adjstk '2)
(return)
105
(cabne (car a1) (car a2) 107)
(mov (cdr a2) a2)
(mov (cdr a1) a1)
(adjstk '2)
(bra one-way-unify1-lst)
107
(mov nil a1)
(adjstk '2)
(return)
))
(loader'((entry one-way-unify1-lst subr2)
(push a2)
(push a1)
(bfnil a1 101)
(mov 't a1)
(adjstk '2)
(return)
101
(mov (car a2) a2)
(mov (car a1) a1)
(call one-way-unify1)
(btnil a1 103)
(mov (& 0) a1)
(mov (& 1) a2)
(mov (cdr a2) a2)
(mov (cdr a1) a1)
(adjstk '2)
(bra one-way-unify1-lst)
103
(mov nil a1)
(adjstk '2)
(return)
))
(loader'((entry rewrite subr1)
(push a1)
(btcons a1 101)
(adjstk '1)
(return)
101
(push (car a1))
(mov (cdr a1) a1)
(call rewrite-args)
(mov a1 a2)
(pop a1)
(jcall cons)
(push a1)
(mov (& 1) a1)
(mov 'lemmas a2)
(mov (car a1) a1)
(jcall get)
(mov a1 a2)
(pop a1)
(adjstk '1)
(bra rewrite-with-lemmas)
))
(loader'((entry rewrite-args subr1)
(push a1)
(bfnil a1 101)
(mov nil a1)
(adjstk '1)
(return)
101
(mov (car a1) a1)
(call rewrite)
(push a1)
(mov (& 1) a1)
(mov (cdr a1) a1)
(call rewrite-args)
(mov a1 a2)
(pop a1)
(adjstk '1)
(jmp cons)
))
(loader'((entry rewrite-with-lemmas subr2)
(push a2)
(push a1)
(bfnil a2 101)
(adjstk '2)
(return)
101
(mov (car a2) a2)
(mov (cdr a2) a2)
(mov (car a2) a2)
(call one-way-unify)
(btnil a1 103)
(mov (& 1) a2)
(mov (car a2) a2)
(mov (cdr a2) a2)
(mov (cdr a2) a2)
(mov (car a2) a2)
(mov (cvalq unify-subst) a1)
(call apply-subst)
(adjstk '2)
(bra rewrite)
103
(mov (& 1) a2)
(mov (cdr a2) a2)
(mov (& 0) a1)
(adjstk '2)
(bra rewrite-with-lemmas)
))
(loader'((fentry boyer-setup subr0)
(entry boyer-setup subr0)
(mov '((equal (compile form) (reverse (codegen (optimize form) (nil)))) (equal (eqp x y) (equal (fix x) (fix y))) (equal (greaterp x y) (lessp y x)) (equal (lesseqp x y) (not (lessp y x))) (equal (greatereqp x y) (not (lessp x y))) (equal (boolean x) (or (equal x (t)) (equal x (f)))) (equal (iff x y) (and (implies x y) (implies y x))) (equal (even1 x) (if (zerop x) (t) (odd (1- x)))) (equal (countps- l pred) (countps-loop l pred (zero))) (equal (fact- i) (fact-loop i 1)) (equal (reverse- x) (reverse-loop x (nil))) (equal (divides x y) (zerop (remainder y x))) (equal (assume-true var alist) (cons (cons var (t)) alist)) (equal (assume-false var alist) (cons (cons var (f)) alist)) (equal (tautology-checker x) (tautologyp (normalize x) (nil))) (equal (falsify x) (falsify1 (normalize x) (nil))) (equal (prime x) (and (not (zerop x)) (not (equal x (add1 (zero)))) (prime1 x (1- x)))) (equal (and p q) (if p (if q (t) (f)) (f))) (equal (or p q) (if p (t) (if q (t) (f)) (f))) (equal (not p) (if p (f) (t))) (equal (implies p q) (if p (if q (t) (f)) (t))) (equal (fix x) (if (numberp x) x (zero))) (equal (if (if a b c) d e) (if a (if b d e) (if c d e))) (equal (zerop x) (or (equal x (zero)) (not (numberp x)))) (equal (plus (plus x y) z) (plus x (plus y z))) (equal (equal (plus a b) (zero)) (and (zerop a) (zerop b))) (equal (difference x x) (zero)) (equal (equal (plus a b) (plus a c)) (equal (fix b) (fix c))) (equal (equal (zero) (difference x y)) (not (lessp y x))) (equal (equal x (difference x y)) (and (numberp x) (or (equal x (zero)) (zerop y)))) (equal (meaning (plus-tree (append x y)) a) (plus (meaning (plus-tree x) a) (meaning (plus-tree y) a))) (equal (meaning (plus-tree (plus-fringe x)) a) (fix (meaning x a))) (equal (append (append x y) z) (append x (append y z))) (equal (reverse (append a b)) (append (reverse b) (reverse a))) (equal (times x (plus y z)) (plus (times x y) (times x z))) (equal (times (times x y) z) (times x (times y z))) (equal (equal (times x y) (zero)) (or (zerop x) (zerop y))) (equal (exec (append x y) pds envrn) (exec y (exec x pds envrn) envrn)) (equal (mc-flatten x y) (append (flatten x) y)) (equal (member x (append a b)) (or (member x a) (member x b))) (equal (member x (reverse y)) (member x y)) (equal (length (reverse x)) (length x)) (equal (member z (intersect b c)) (and (member a b) (member a c))) (equal (nth (zero) i) (zero)) (equal (exp i (plus j k)) (times (exp i h) (exp i k))) (equal (exp i (times j k)) (exp (exp i j) k)) (equal (reverse-loop x y) (append (reverse x) y)) (equal (count-list z (sort-lp x y)) (plus (count-list z x) (count-list z y))) (equal (equal (append a b) (append a c)) (equal b c)) (equal (plus (remainder x y) (times y (quotient x y))) (fix x)) (equal (power-eval (big-plus1 l i base) base) (plus (power-eval l base) i)) (equal (power-eval (big-plus x y i base) base) (plus i (plus (power-eval x base) (power-eval y base)))) (equal (remainder y 1) (zero)) (equal (lessp (quotient i j) i) (and (not (zerop i)) (or (zerop j) (not (equal j 1))))) (equal (lessp (remainder x y) x) (and (not (zerop y)) (not (zerop x)) (not (lessp x y)))) (equal (power-eval (power-rep i base) base) (fix i)) (equal (power-eval (big-plus (power-rep i base) (power-rep j base) (zero) base) base) (plus i j)) (equal (gcd x y) (gcd y x)) (equal (nth (append a b) i) (append (nth a i) (nth b (difference i (length a))))) (equal (difference (plus x y) x) (fix y)) (equal (difference (plus y x) x) (fix y)) (equal (difference (plus x y) (plus x z)) (difference y z)) (equal (times x (difference c w)) (difference (times c x) (times w x))) (equal (remainder (times x z) z) (zero)) (equal (difference (add1 (plus y z)) z) (add1 y)) (equal (lessp (plus x y) (plus x z)) (lessp y z)) (equal (lessp (times x z) (times y z)) (and (not (zerop z)) (lessp x y))) (equal (lessp y (plus x y)) (not (zerop x))) (equal (gcd (times x z) (times y z)) (times z (gcd x y))) (equal (value (normalize x) a) (value x a)) (equal (equal (flatten x) (cons y (nil))) (and (nlistp x) (equal x y))) (equal (listp (gopher x)) (listp x)) (equal (samefringe x y) (equal (flatten x) (flatten y))) (equal (equal (greatest-factor x y) (zero)) (and (or (zerop y) (equal y 1)) (equal x (zero)))) (equal (equal (greatest-factor x y) 1) (equal x 1)) (equal (numberp (greatest-factor x y)) (not (and (or (zerop y) (equal y 1)) (not (numberp x))))) (equal (times-list (append x y)) (times (times-list x) (times-list y))) (equal (prime-list (append x y)) (and (prime-list x) (prime-list y))) (equal (equal z (times w z)) (and (numberp z) (or (equal z (zero)) (equal w 1)))) (equal (greatereqpr x y) (not (lessp x y))) (equal (equal x (times x y)) (or (equal x (zero)) (and (numberp x) (equal y 1)))) (equal (remainder (times y x) y) (zero)) (equal (equal (times a b) 1) (and (not (equal a (zero))) (not (equal b (zero))) (numberp a) (numberp b) (equal (1- a) (zero)) (equal (1- b) (zero)))) (equal (lessp (length (delete x l)) (length l)) (member x l)) (equal (sort2 (delete x l)) (delete x (sort2 l))) (equal (dsort x) (sort2 x)) (equal (length (cons x1 (cons x2 (cons x3 (cons x4 (cons x5 (cons x6 x7))))))) (plus 6 (length x7))) (equal (difference (add1 (add1 x)) 2) (fix x)) (equal (quotient (plus x (plus x y)) 2) (plus x (quotient y 2))) (equal (sigma (zero) i) (quotient (times i (add1 i)) 2)) (equal (plus x (add1 y)) (if (numberp y) (add1 (plus x y)) (add1 x))) (equal (equal (difference x y) (difference z y)) (if (lessp x y) (not (lessp y z)) (if (lessp z y) (not (lessp y x)) (equal (fix x) (fix z))))) (equal (meaning (plus-tree (delete x y)) a) (if (member x y) (difference (meaning (plus-tree y) a) (meaning x a)) (meaning (plus-tree y) a))) (equal (times x (add1 y)) (if (numberp y) (plus x (times x y)) (fix x))) (equal (nth (nil) i) (if (zerop i) (nil) (zero))) (equal (last (append a b)) (if (listp b) (last b) (if (listp a) (cons (car (last a)) b) b))) (equal (equal (lessp x y) z) (if (lessp x y) (equal t z) (equal f z))) (equal (assignment x (append a b)) (if (assignedp x a) (assignment x a) (assignment x b))) (equal (car (gopher x)) (if (listp x) (car (flatten x)) (zero))) (equal (flatten (cdr (gopher x))) (if (listp x) (cdr (flatten x)) (cons (zero) (nil)))) (equal (quotient (times y x) y) (if (zerop y) (zero) (fix x))) (equal (get j (set i val mem)) (if (eqp j i) val (get j mem)))) a1)
(bra add-lemma-lst)
))
(loader'((entry tautologyp subr3)
(push a3)
(push a2)
(push a1)
(call truep)
(btnil a1 101)
(mov 't a1)
(adjstk '3)
(return)
101
(mov (& 2) a2)
(mov (& 0) a1)
(call falsep)
(btnil a1 103)
(mov nil a1)
(adjstk '3)
(return)
103
(btcons (& 0) 105)
(mov nil a1)
(adjstk '3)
(return)
105
(mov (& 0) a4)
(cabne (car a4) 'if 107)
(mov (cdr a4) a1)
(mov (& 1) a2)
(mov (car a1) a1)
(call truep)
(btnil a1 109)
(mov (& 0) a1)
(mov (cdr a1) a1)
(mov (cdr a1) a1)
(mov (& 2) a3)
(mov (& 1) a2)
(mov (car a1) a1)
(adjstk '3)
(bra tautologyp)
109
(mov (& 0) a1)
(mov (cdr a1) a1)
(mov (& 2) a2)
(mov (car a1) a1)
(call falsep)
(btnil a1 111)
(mov (& 0) a1)
(mov (cdr a1) a1)
(mov (cdr a1) a1)
(mov (cdr a1) a1)
(mov (& 2) a3)
(mov (& 1) a2)
(mov (car a1) a1)
(adjstk '3)
(bra tautologyp)
111
(mov (& 0) a1)
(mov (cdr a1) a1)
(mov (cdr a1) a1)
(push (car a1))
(mov (& 1) a1)
(mov (cdr a1) a1)
(mov (& 2) a2)
(mov (car a1) a1)
(jcall cons)
(mov (& 3) a3)
(mov a1 a2)
(pop a1)
(call tautologyp)
(btnil a1 113)
(mov (& 0) a1)
(mov (cdr a1) a1)
(mov (cdr a1) a1)
(mov (cdr a1) a1)
(push (car a1))
(mov (& 1) a1)
(mov (cdr a1) a1)
(mov (& 3) a2)
(mov (car a1) a1)
(jcall cons)
(mov a1 a3)
(mov (& 2) a2)
(pop a1)
(adjstk '3)
(bra tautologyp)
113
(adjstk '3)
(return)
107
(mov nil a1)
(adjstk '3)
(return)
))
(loader'((entry tautp subr1)
(call rewrite)
(mov nil a3)
(mov nil a2)
(bra tautologyp)
))
(loader'((entry boyer subr0)
(mov '(implies (and (implies x y) (and (implies y z) (and (implies z u) (implies u w)))) (implies x w)) a2)
(mov '((x f (plus (plus a b) (plus c (zero)))) (y f (times (times a b) (plus c d))) (z f (reverse (append (append a b) (nil)))) (u equal (plus a b) (difference x y)) (w lessp (remainder a b) (member a (length b)))) a1)
(call apply-subst)
(bra tautp)
))
(loader'((entry truep subr2)
(push a2)
(push a1)
(mov '(t) a2)
(jcall equal)
(bfnil a1 101)
(mov (& 1) a2)
(mov (& 0) a1)
(adjstk '2)
(jmp member)
101
(adjstk '2)
(return)
))
(boyer-setup)
(loader '((end)))