{-
    Haskell version of ...

! Text of rule base for Boyer benchmark !

! Started by Tony Kitto on 6th April 1988                                  !
! Changes Log                                                              !
! 07-04-88 ADK Corrected errors in rules
! 08-04-88 ADK Modified "or" rule to remove extra final (f) of book definition

Haskell version:

    23-06-93 JSM initial version

-}

module Rulebasetext (rules) where

rules :: [String]

-- Rule base extracted from Gabriel pages 118 to 126

rules = [
             "(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 y x) ) )",
             "(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) ) ) )", -- book has extra (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 a (intersect b c) )\
                    \(and (member a b)\
                         \(member a c) ) )",
             "(equal (nth (zero)\
                          \i)\
                    \(zero) )",
             "(equal (exp i (plus j k) )\
                    \(times (exp i j)\
                           \(exp i k) ) )",
             "(equal (exp i (times j k) )\
                    \(exp (exp i j)\
                         \k) )",
             "(equal (reverse-loop x y)\
                    \(append (reverse x)\
                            \y) )",
             "(equal (reverse-loop x (nil) )\
                    \(reverse x) )",
             "(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 (remainder x y)\
                           \y)\
                    \(not (zerop y) ) )",
             "(equal (remainder x x)\
                    \(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 (plus b (plus a c) )\
                                \a)\
                    \(plus b c) )",
             "(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) ) )"]