1 {-
    2     Haskell version of ...
    3 
    4 ! Text of rule base for Boyer benchmark !
    5 
    6 ! Started by Tony Kitto on 6th April 1988                                  !
    7 ! Changes Log                                                              !
    8 ! 07-04-88 ADK Corrected errors in rules
    9 ! 08-04-88 ADK Modified "or" rule to remove extra final (f) of book definition
   10 
   11 Haskell version:
   12 
   13     23-06-93 JSM initial version
   14 
   15 -}
   16 
   17 module Rulebasetext (rules) where
   18 
   19 rules :: [String]
   20 
   21 -- Rule base extracted from Gabriel pages 118 to 126
   22 
   23 rules = [
   24              "(equal (compile form)\
   25                     \(reverse (codegen (optimize form) (nil) ) ) )",
   26              "(equal (eqp x y)\
   27                     \(equal (fix x)\
   28                            \(fix y) ) )",
   29              "(equal (greaterp x y)\
   30                     \(lessp y x) )",
   31              "(equal (lesseqp x y)\
   32                     \(not (lessp y x) ) )",
   33              "(equal (greatereqp x y)\
   34                     \(not (lessp y x) ) )",
   35              "(equal (boolean x)\
   36                     \(or (equal x (t) )\
   37                         \(equal x (f) ) )",
   38              "(equal (iff x y)\
   39                     \(and (implies x y)\
   40                          \(implies y x) ) )",
   41              "(equal (even1 x)\
   42                     \(if (zerop x)\
   43                         \(t)\
   44                         \(odd (1- x) ) ) )",
   45              "(equal (countps- l pred)\
   46                     \(countps-loop l pred (zero) ) )",
   47              "(equal (fact- i)\
   48                     \(fact-loop i 1) )",
   49 
   50              "(equal (reverse- x)\
   51                     \(reverse-loop x (nil) ) )",
   52              "(equal (divides x y)\
   53                     \(zerop (remainder y x) ) )",
   54              "(equal (assume-true var alist)\
   55                     \(cons (cons var (t) )\
   56                      \alist) )",
   57              "(equal (assume-false var alist)\
   58                     \(cons (cons var (f) )\
   59                           \alist) )",
   60              "(equal (tautology-checker x)\
   61                     \(tautologyp (normalize x)\
   62                                 \(nil) ) )",
   63              "(equal (falsify x)\
   64                     \(falsify1 (normalize x)\
   65                               \(nil) ) )",
   66              "(equal (prime x)\
   67                     \(and (not (zerop x))\
   68                          \(not (equal x (add1 (zero) ) ) )\
   69                          \(prime1 x (1- x) ) ) )",
   70              "(equal (and p q)\
   71                     \(if p (if q (t) (f) ) (f) ) )",
   72              "(equal (or p q)\
   73                     \(if p (t) (if q (t) (f) ) ) )", -- book has extra (f)
   74              "(equal (not p)\
   75                     \(if p (f) (t) ) )",
   76 
   77              "(equal (implies p q)\
   78                     \(if p (if q (t) (f) ) (t) ) )",
   79              "(equal (fix x)\
   80                     \(if (numberp x) x (zero) ) )",
   81              "(equal (if (if a b c) d e)\
   82                     \(if a (if b d e) (if c d e) ) )",
   83              "(equal (zerop x)\
   84                     \(or (equal x (zero) )\
   85                         \(not (numberp x) ) ) )",
   86              "(equal (plus (plus x y) z )\
   87                     \(plus x (plus y z) ) )",
   88              "(equal (equal (plus a b) (zero ) )\
   89                     \(and (zerop a) (zerop b) ) )",
   90              "(equal (difference x x)\
   91                     \(zero) )",
   92              "(equal (equal (plus a b) (plus a c) )\
   93                     \(equal (fix b) (fix c) ) )",
   94              "(equal (equal (zero) (difference x y) )\
   95                     \(not (lessp y x) ) )",
   96              "(equal (equal x (difference x y) )\
   97                     \(and (numberp x)\
   98                          \(or (equal x (zero) )\
   99                              \(zerop y) ) ) )",
  100 
  101              "(equal (meaning (plus-tree (append x y) ) a)\
  102                     \(plus (meaning (plus-tree x) a)\
  103                           \(meaning (plus-tree y) a) ) )",
  104              "(equal (meaning (plus-tree (plus-fringe x) ) a)\
  105                     \(fix (meaning x a) ) )",
  106              "(equal (append (append x y) z)\
  107                     \(append x (append y z) ) )",
  108              "(equal (reverse (append a b) )\
  109                     \(append (reverse b) (reverse a) ) )",
  110              "(equal (times x (plus y z) )\
  111                     \(plus (times x y)\
  112                           \(times x z) ) )",
  113              "(equal (times (times x y) z)\
  114                     \(times x (times y z) ) )",
  115              "(equal (equal (times x y) (zero) )\
  116                     \(or (zerop x)\
  117                         \(zerop y) ) )",
  118              "(equal (exec (append x y)\
  119                            \pds envrn)\
  120                     \(exec y (exec x pds envrn)\
  121                           \envrn) )",
  122              "(equal (mc-flatten x y)\
  123                     \(append (flatten x)\
  124                            \y) )",
  125              "(equal (member x (append a b) )\
  126                     \(or (member x a)\
  127                         \(member x b) ) )",
  128 
  129              "(equal (member x (reverse y) )\
  130                     \(member x y) )",
  131              "(equal (length (reverse x) )\
  132                     \(length x) )",
  133              "(equal (member a (intersect b c) )\
  134                     \(and (member a b)\
  135                          \(member a c) ) )",
  136              "(equal (nth (zero)\
  137                           \i)\
  138                     \(zero) )",
  139              "(equal (exp i (plus j k) )\
  140                     \(times (exp i j)\
  141                            \(exp i k) ) )",
  142              "(equal (exp i (times j k) )\
  143                     \(exp (exp i j)\
  144                          \k) )",
  145              "(equal (reverse-loop x y)\
  146                     \(append (reverse x)\
  147                             \y) )",
  148              "(equal (reverse-loop x (nil) )\
  149                     \(reverse x) )",
  150              "(equal (count-list z (sort-lp x y) )\
  151                     \(plus (count-list z x)\
  152                           \(count-list z y) ) )",
  153              "(equal (equal (append a b)\
  154                            \(append a c) )\
  155                     \(equal b c) )",
  156 
  157              "(equal (plus (remainder x y)\
  158                           \(times y (quotient x y) ) )\
  159                     \(fix x) )",
  160              "(equal (power-eval (big-plus1 l i base)\
  161                                 \base)\
  162                     \(plus (power-eval l base)\
  163                           \i) )",
  164              "(equal (power-eval (big-plus x y i base)\
  165                                 \base)\
  166                     \(plus i (plus (power-eval x base)\
  167                                   \(power-eval y base) ) ) )",
  168              "(equal (remainder y 1)\
  169                     \(zero) )",
  170              "(equal (lessp (remainder x y)\
  171                            \y)\
  172                     \(not (zerop y) ) )",
  173              "(equal (remainder x x)\
  174                     \(zero) )",
  175              "(equal (lessp (quotient i j)\
  176                            \i)\
  177                     \(and (not (zerop i) )\
  178                          \(or (zerop j)\
  179                              \(not (equal j 1) ) ) ) )",
  180              "(equal (lessp (remainder x y)\
  181                            \x)\
  182                     \(and (not (zerop y) )\
  183                          \(not (zerop x) )\
  184                          \(not (lessp x y) ) ) )",
  185              "(equal (power-eval (power-rep i base)\
  186                                 \base)\
  187                     \(fix i) )",
  188              "(equal (power-eval (big-plus (power-rep i base)\
  189                                           \(power-rep j base)\
  190                                           \(zero)\
  191                                           \base)\
  192                                  \base)\
  193                     \(plus i j) )",
  194 
  195              "(equal (gcd x y)\
  196                     \(gcd y x) )",
  197              "(equal (nth (append a b)\
  198                          \i)\
  199                     \(append (nth a i)\
  200                             \(nth b (difference i (length a) ) ) ) )",
  201              "(equal (difference (plus x y)\
  202                                 \x)\
  203                     \(fix y) )",
  204              "(equal (difference (plus y x)\
  205                                 \x)\
  206                     \(fix y) )",
  207              "(equal (difference (plus x y)\
  208                                 \(plus x z) )\
  209                     \(difference y z) )",
  210              "(equal (times x (difference c w) )\
  211                     \(difference (times c x)\
  212                                 \(times w x) ) )",
  213              "(equal (remainder (times x z)\
  214                                \z)\
  215                     \(zero) )",
  216              "(equal (difference (plus b (plus a c) )\
  217                                 \a)\
  218                     \(plus b c) )",
  219              "(equal (difference (add1 (plus y z)\
  220                                 \z)\
  221                     \(add1 y) )",
  222              "(equal (lessp (plus x y)\
  223                            \(plus x z ) )\
  224                     \(lessp y z) )",
  225 
  226              "(equal (lessp (times x z)\
  227                            \(times y z) )\
  228                     \(and (not (zerop z) )\
  229                          \(lessp x y) ) )",
  230              "(equal (lessp y (plus x y) )\
  231                     \(not (zerop x) ) )",
  232              "(equal (gcd (times x z)\
  233                          \(times y z) )\
  234                     \(times z (gcd x y) ) )",
  235              "(equal (value (normalize x)\
  236                            \a)\
  237                     \(value x a) )",
  238              "(equal (equal (flatten x)\
  239                            \(cons y (nil) ) )\
  240                     \(and (nlistp x)\
  241                          \(equal x y) ) )",
  242              "(equal (listp (gopher x) )\
  243                     \(listp x) )",
  244              "(equal (samefringe x y)\
  245                     \(equal (flatten x)\
  246                            \(flatten y) ) )",
  247              "(equal (equal (greatest-factor x y)\
  248                            \(zero) )\
  249                     \(and (or (zerop y)\
  250                              \(equal y 1) )\
  251                          \(equal x (zero) ) ) )",
  252              "(equal (equal (greatest-factor x y)\
  253                            \1)\
  254                     \(equal x 1) )",
  255              "(equal (numberp (greatest-factor x y) )\
  256                     \(not (and (or (zerop y)\
  257                                   \(equal y 1) )\
  258                               \(not (numberp x) ) ) ) )",
  259 
  260              "(equal (times-list (append x y) )\
  261                     \(times (times-list x)\
  262                            \(times-list y) ) )",
  263              "(equal (prime-list (append x y) )\
  264                     \(and (prime-list x)\
  265                          \(prime-list y) ) )",
  266              "(equal (equal z (times w z) )\
  267                     \(and (numberp z)\
  268                          \(or (equal z (zero) )\
  269                              \(equal w 1) ) ) )",
  270              "(equal (greatereqpr x y)\
  271                     \(not (lessp x y) ) )",
  272              "(equal (equal x (times x y) )\
  273                     \(or (equal x (zero) )\
  274                         \(and (numberp x)\
  275                              \(equal y 1) ) ) )",
  276              "(equal (remainder (times y x)\
  277                                \y)\
  278                     \(zero) )",
  279              "(equal (equal (times a b)\
  280                            \1)\
  281                     \(and (not (equal a (zero) ) )\
  282                          \(not (equal b (zero) ) )\
  283                          \(numberp a)\
  284                          \(numberp b)\
  285                          \(equal (1- a)\
  286                                 \(zero) )\
  287                          \(equal (1- b)\
  288                                 \(zero) ) ) )",
  289              "(equal (lessp (length (delete x l) )\
  290                            \(length l) )\
  291                     \(member x l) )",
  292              "(equal (sort2 (delete x l) )\
  293                     \(delete x (sort2 l) ) )",
  294              "(equal (dsort x)\
  295                     \(sort2 x) )",
  296 
  297              "(equal (length\
  298                      \(cons \
  299                       \x1\
  300                       \(cons \
  301                        \x2\
  302                        \(cons \
  303                         \x3\
  304                         \(cons \
  305                          \x4\
  306                          \(cons \
  307                           \x5\
  308                           \(cons x6 x7) ) ) ) ) ) )\
  309                     \(plus 6 (length x7) ) )",
  310              "(equal (difference (add1 (add1 x) )\
  311                                 \2)\
  312                     \(fix x) )",
  313              "(equal (quotient (plus x (plus x y) )\
  314                               \2)\
  315                     \(plus x (quotient y 2) ) )",
  316              "(equal (sigma (zero)\
  317                            \i)\
  318                     \(quotient (times i (add1 i) )\
  319                               \2) )",
  320              "(equal (plus x (add1 y) )\
  321                     \(if (numberp y)\
  322                         \(add1 (plus x y) )\
  323                         \(add1 x) ) )",
  324              "(equal (equal (difference x y)\
  325                            \(difference z y) )\
  326                     \(if (lessp x y)\
  327                         \(not (lessp y z) )\
  328                         \(if (lessp z y)\
  329                             \(not (lessp y x) )\
  330                             \(equal (fix x)\
  331                                    \(fix z) ) ) ) )",
  332              "(equal (meaning (plus-tree (delete x y) )\
  333                              \a)\
  334                     \(if (member x y)\
  335                         \(difference (meaning (plus-tree y)\
  336                                              \a)\
  337                                     \(meaning x a) )\
  338                         \(meaning (plus-tree y)\
  339                                  \a) ) )",
  340              "(equal (times x (add1 y) )\
  341                     \(if (numberp y)\
  342                         \(plus x (times x y) )\
  343                         \(fix x) ) )",
  344              "(equal (nth (nil)\
  345                          \i)\
  346                     \(if (zerop i)\
  347                         \(nil)\
  348                         \(zero) ) )",
  349              "(equal (last (append a b) )\
  350                     \(if (listp b)\
  351                         \(last b)\
  352                         \(if (listp a)\
  353                             \(cons (car (last a) )\
  354                                  \b)\
  355                             \b) ) )",
  356 
  357              "(equal (equal (lessp x y)\
  358                            \z)\
  359                     \(if (lessp x y)\
  360                         \(equal t z)\
  361                         \(equal f z) ) )",
  362              "(equal (assignment x (append a b) )\
  363                     \(if (assignedp x a)\
  364                         \(assignment x a)\
  365                         \(assignment x b) ) )",
  366              "(equal (car (gopher x) )\
  367                     \(if (listp x)\
  368                        \(car (flatten x) )\
  369                         \(zero) ) )",
  370              "(equal (flatten (cdr (gopher x) ) )\
  371                     \(if (listp x)\
  372                         \(cdr (flatten x) )\
  373                         \(cons (zero)\
  374                               \(nil) ) ) )",
  375              "(equal (quotient (times y x)\
  376                               \y)\
  377                     \(if (zerop y)\
  378                         \(zero)\
  379                         \(fix x) ) )",
  380              "(equal (get j (set i val mem) )\
  381                     \(if (eqp j i)\
  382                         \val\
  383                         \(get j mem) ) )"]
  384