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