1open HolKernel Parse boolLib bossLib; 2open blastLib testutils 3 4(* 5 fun die s = (print (s ^ "\n"); raise ERR "" "") 6*) 7 8val _ = set_trace "Unicode" 0 9val _ = set_trace "print blast counterexamples" 0 10val _ = set_trace "bit blast" 0 11 12val ERR = mk_HOL_ERR "selftest" 13 14val prs = StringCvt.padRight #" " 15fun trunc w t = let 16 val s = Lib.with_flag (Globals.linewidth, 10000) term_to_string t 17in 18 if size s >= w then String.extract (s, 0, SOME (w - 5)) ^ " ... " 19 else prs w s 20end 21 22val _ = tprint "Parsing :bool[32] list" 23val ty1 = listSyntax.mk_list_type (wordsSyntax.mk_int_word_type 32) 24val ty2 = Parse.Type`:bool[32] list` handle HOL_ERR _ => alpha 25val _ = if Type.compare(ty1,ty2) = EQUAL then OK() 26 else die "FAILED!" 27 28val _ = tprint "Parsing :('a + 'b)[32]" 29val ty1 = fcpSyntax.mk_cart_type 30 (sumSyntax.mk_sum(alpha,beta), 31 fcpSyntax.mk_int_numeric_type 32); 32val ty2 = Parse.Type`:('a + 'b)[32]` 33val _ = if Type.compare(ty1,ty2) = EQUAL then OK() 34 else die "FAILED" 35 36val _ = tprint "Printing :('a + 'b)[32]" 37val _ = if type_to_string ty2 = ":('a + 'b)[32]" then OK() 38 else die "FAILED" 39 40val _ = tprint "Parsing abbreviated word types" 41val u8 = fcpSyntax.mk_cart_type(bool, fcpSyntax.mk_int_numeric_type 8) 42val _ = type_abbrev("u8", u8) 43val _ = if Type.compare(Parse.Type`:u8`, u8) <> EQUAL then die "FAILED!" 44 else OK() 45val _ = tprint "Printing abbreviated word types" 46val _ = if type_to_string u8 = ":u8" then OK() else die "FAILED!" 47 48val _ = tprint "Parsing Datatype with bool-array type" 49val _ = (Datatype`mytype = mytype_con (bool[3])`; OK()) handle HOL_ERR _ => die "FAILED" 50 51fun test (c:conv) tm = let 52 val rt = Timer.startRealTimer () 53 val res = Lib.total c tm 54 val elapsed = Timer.checkRealTimer rt 55in 56 TextIO.print (trunc 65 tm ^ Time.toString elapsed); 57 case res of 58 NONE => die "FAILED!" 59 | _ => print "\n" 60end 61 62fun test_fail orig (c:conv) tm = let 63 val res = (c tm; SOME "should fail!") 64 handle HolSatLib.SAT_cex _ => SOME "unexpected counterexample!" 65 | HOL_ERR {origin_function,...} => 66 if origin_function = orig then 67 NONE 68 else 69 SOME ("unexpected exception from " ^ origin_function) 70in 71 tprint ("Expecting failure: " ^ trunc 46 tm); 72 case res of 73 NONE => OK() 74 | SOME s => die s 75end 76 77fun test_counter (c:conv) tm = let 78 val res = (c tm; SOME "should fail!") 79 handle HolSatLib.SAT_cex thm => 80 if Lib.can Drule.EQF_ELIM thm then 81 NONE 82 else 83 SOME "bad counterexample" 84 | HOL_ERR {origin_function,...} => 85 SOME ("unexpected exception from " ^ origin_function) 86in 87 tprint ("Counterexample: " ^ trunc 49 tm); 88 case res of 89 NONE => OK() 90 | SOME s => die s 91end 92 93local 94 fun test_conv (conv: conv) tm = 95 let 96 val (t, expected) = boolSyntax.dest_eq tm 97 val s = fst (boolSyntax.dest_strip_comb t) 98 val s = case String.tokens (Lib.equal #"$") s of 99 [_, s] => s 100 | _ => die "FAILED\n Couldn't get name." 101 val _ = tprint s 102 val th = conv t handle _ => die "FAILED - exception raised" 103 val r = rhs (concl th) handle HOL_ERR _ => die "FAILED - no RHS" 104 in 105 if aconv r expected then OK() 106 else die ("FAILED\n Got ``" ^ term_to_string r ^ "``") 107 end 108 val quote_to_term_list = 109 fn [QUOTE s] => 110 List.mapPartial (fn s => if List.all Char.isSpace (String.explode s) 111 then NONE 112 else SOME (Parse.Term [QUOTE s])) 113 (String.tokens (Lib.equal #"\n") s) 114 | _ => raise ERR "" "" 115in 116 fun qtest_conv conv q = List.app (test_conv conv) (quote_to_term_list q) 117end 118 119val blast_true = test blastLib.BBLAST_PROVE 120val blast_fail = test_fail "BBLAST_PROVE" blastLib.BBLAST_PROVE 121val blast_counter = test_counter blastLib.BBLAST_PROVE 122val srw_true = test (simpLib.SIMP_PROVE (srw_ss()) []) 123 124(* start tests *) 125val _ = print "\nblastLib tests\n\n" 126val tt = Timer.startRealTimer () 127 128(* Fail (false) *) 129val _ = blast_fail ``?x. x <+ 0w : word8`` 130val _ = blast_fail ``?x y. !z. (x + y = 0w : word8) /\ P z`` 131val _ = blast_fail ``?x: word8. 3w > 4w : word4`` 132val _ = blast_fail ``x + x = x :'a word`` 133 134(* Fail, can't solve *) 135val _ = blast_fail ``?x. !y. x <=+ y : word8`` 136val _ = blast_fail ``!y. ?x. x <=+ y : word8`` 137val _ = blast_fail ``?x. x <=+ y : word8`` 138val _ = blast_fail ``(!x:word8 y:word8. word_msb x = word_msb y) ==> 139 (x <+ y = x < y : word8)`` 140 141(* Counterexamples *) 142val _ = blast_counter ``!x. x <+ 0w : word8`` 143val _ = blast_counter ``!x. x >=+ 2w : word8`` 144val _ = blast_counter ``!y. x <=+ y : word8`` 145val _ = blast_counter ``(x = 1w) \/ (x = 2w : word2)`` 146val _ = blast_counter ``x = y : word2`` 147val _ = blast_counter ``x + x = x : word8`` 148val _ = blast_counter ``x <+ y = x < y : word8`` 149val _ = blast_counter ``(8w * a + b && 7w) >> 3 = a && (-1w >> 3) : word8`` 150 151val _ = blast_true ``!x. x >=+ 2w \/ x <+ 2w : word8`` 152val _ = blast_true ``?x. x <+ 2w : word8`` 153val _ = blast_true ``?x. !y:word8. (y <> y + 1w) /\ x <+ 2w : word8`` 154val _ = blast_true ``?x y. x + y = 12w : word8`` 155val _ = blast_true ``?x. x + x = x : word8`` 156val _ = blast_true ``?x y. !z. (x + y = 0w : word8) /\ (z \/ ~z)`` 157val _ = blast_true ``?x. x <=+ 0w : word8`` 158val _ = blast_true ``!w:word8. ~word_lsb (w << 2)`` 159val _ = blast_true ``?w:word8. word_lsb w`` 160val _ = blast_true ``?x y z. (x + y <+ z + 1w : word8)`` 161val _ = blast_true ``?z y x. (x + y <+ z + 1w : word8)`` 162val _ = blast_true ``?z x y. (x + y <+ z + 1w : word8)`` 163val _ = blast_true ``?x. x`` 164val _ = blast_true ``?x y. x \/ y`` 165val _ = blast_true ``?y x. x \/ y`` 166val _ = blast_true ``!x y. (word_msb x = word_msb y) ==> 167 (x <+ y = x < y : word8)`` 168val _ = blast_true ``?x y. (word_msb x = word_msb y) ==> 169 (x <+ y = x < y : word8)`` 170val _ = blast_true ``!x. x <+ 1w ==> (x + x = x : word8)`` 171val _ = blast_true ``?x. x <+ 1w ==> (x + x = x : word8)`` 172val _ = blast_true ``?x: word8. 3w < 4w : word4`` 173val _ = blast_true ``?x y. x + y = y + x : word8`` 174val _ = blast_true ``?x:word8 y:word8. T`` 175val _ = blast_true ``?x:word8. !y:word8. T`` 176val _ = blast_true ``!x:word8. ?y:word8. T`` 177val _ = blast_true ``((w2w a - w2w b) : 33 word ' 32) = (a <+ b : word32)`` 178 179val _ = blast_true 180 ``(v ?? w = 0w:word8) = (v = w)`` 181 182val _ = blast_true 183 ``(1 >< 0) (w2w (x:word30) << 2 + w:word32) : word2 = (1 >< 0) w`` 184 185val _ = blast_true 186 ``(1 >< 0) ((w2w (x:word30) << 2) : word32) = 0w :word2`` 187 188val _ = blast_true 189 ``(x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w)`` 190 191val _ = blast_true 192 ``(31 >< 2) (w2w (x:word30) << 2 + y:word32) = x + (31 >< 2) y`` 193 194val _ = blast_true 195 ``(31 >< 2) (w2w (a:word30) << 2 + 0w:word32) = a`` 196 197val _ = blast_true 198 ``(31 >< 2) (w2w (a:word30) << 2 + 1w:word32) = a`` 199 200val _ = blast_true 201 ``(31 >< 2) (w2w (a:word30) << 2 + 2w:word32) = a`` 202 203val _ = blast_true 204 ``(31 >< 2) (w2w (a:word30) << 2 + 3w:word32) = a`` 205 206val _ = blast_true 207 ``(x && 3w = 0w:word32) ==> (w2w ((31 >< 2) x : word30) << 2 = x)`` 208 209val _ = blast_true 210 ``w2w (v + w:word30) << 2 = (w2w v << 2 + w2w w << 2) : word32`` 211 212val _ = blast_true 213 ``w2w (-w : word30) << 2 = -(w2w w << 2) : word32`` 214 215val _ = blast_true 216 ``w2w (v - w:word30) << 2 = (w2w v << 2 - w2w w << 2) : word32`` 217 218val _ = blast_true 219 ``w2w (p + 1w:word30) << 2 = w2w p << 2 + 4w:word32`` 220 221val _ = blast_true 222 ``(w2w a << 2 = 0w:word32) = (a = 0w:word30)`` 223 224val _ = blast_true 225 ``(w2w (a:word30) << 2 && 1w = 0w:word32)`` 226 227val _ = blast_true 228 ``(w2w (a:word30) << 2 && 2w = 0w:word32)`` 229 230val _ = blast_true 231 ``(w2w (a:word30) << 2 && 3w = 0w:word32)`` 232 233val _ = blast_true 234 ``(w2w (a:word30) << 2 = (w2w b << 2):word32) = (a = b)`` 235 236val _ = blast_true 237 ``(w2w (a:word30) << 2 + 1w : word32 = w2w b << 2 + 1w) = (a = b)`` 238 239val _ = blast_true 240 ``(w2w (a:word30) << 2 + 2w : word32 = w2w b << 2 + 2w) = (a = b)`` 241 242val _ = blast_true 243 ``(w2w (a:word30) << 2 + 3w : word32 = w2w b << 2 + 3w) = (a = b)`` 244 245val _ = blast_true 246 ``~(w2w (a:word30) << 2 + 1w : word32 = w2w (b:word30) << 2 + 2w)`` 247 248val _ = blast_true 249 ``~(w2w (a:word30) << 2 + 1w : word32 = w2w (b:word30) << 2 + 3w)`` 250 251val _ = blast_true 252 ``~(w2w (a:word30) << 2 + 2w : word32 = w2w (b:word30) << 2 + 3w)`` 253 254val _ = blast_true 255 ``(w2w (x:word30) << 2) + 4w:word32 = w2w (x + 1w) << 2`` 256 257val _ = blast_true 258 ``(w2w (x:word30) << 2) + 8w:word32 = w2w (x + 2w) << 2`` 259 260val _ = blast_true 261 ``(w2w (x:word30) << 2) + 40w:word32 = w2w (x + 10w) << 2`` 262 263val _ = blast_true 264 ``(w2w (x:word30) << 2) - 4w:word32 = w2w (x - 1w) << 2`` 265 266val _ = blast_true 267 ``(w2w (x:word30) << 2) - 8w:word32 = w2w (x - 2w) << 2`` 268 269val _ = blast_true 270 ``(w2w (x:word30) << 2) - 40w:word32 = w2w (x - 10w) << 2`` 271 272val _ = blast_true 273 ``(-x && 3w = 0w:word32) = (x && 3w = 0w)`` 274 275val _ = blast_true 276 ``(x && 3w = 0w) ==> (x && 1w = 0w:word32)`` 277 278val _ = blast_true 279 ``(x && 3w = 0w) ==> ~(x + 1w && 1w = 0w:word32)`` 280 281val _ = blast_true 282 ``(x && 3w = 0w) ==> (x + 1w && 3w = 1w:word32)`` 283 284val _ = blast_true 285 ``(x && 3w = 0w) ==> (x + 2w && 3w = 2w:word32)`` 286 287val _ = blast_true 288 ``(x && 3w = 0w) ==> (x + 3w && 3w = 3w:word32)`` 289 290val _ = blast_true 291 ``(x && 3w = 0w) /\ (y && 3w = 0w) ==> ((x + y) && 3w = 0w:word32)`` 292 293val _ = blast_true 294 ``(x && 3w = 0w) /\ (y && 3w = 0w) ==> ((x - y) && 3w = 0w:word32)`` 295 296val _ = blast_true 297 ``((a + 4w * x) && 3w = 0w:word32) = (a && 3w = 0w)`` 298 299val _ = blast_true 300 ``((4w * x + a) && 3w = 0w:word32) = (a && 3w = 0w)`` 301 302val _ = blast_true 303 ``((a + x * 4w) && 3w = 0w:word32) = (a && 3w = 0w)`` 304 305val _ = blast_true 306 ``((x * 4w + a) && 3w = 0w:word32) = (a && 3w = 0w)`` 307 308val _ = blast_true 309 ``((a + 4w) && 3w = 0w:word32) = (a && 3w = 0w)`` 310 311val _ = blast_true 312 ``((4w + a) && 3w = 0w:word32) = (a && 3w = 0w)`` 313 314val _ = blast_true 315 ``(a && 3w = 0w:word32) ==> ~((a + 1w) && 3w = 0w)`` 316 317val _ = blast_true 318 ``(a && 3w = 0w:word32) ==> ~((a + 2w) && 3w = 0w)`` 319 320val _ = blast_true 321 ``(a && 3w = 0w:word32) ==> ~((a + 3w) && 3w = 0w)`` 322 323val _ = blast_true 324 ``(x && 3w = 0w:word32) = ~(x ' 0) /\ ~(x ' 1)`` 325 326val _ = blast_true 327 ``((x || y) && 3w = 0w:word32) = (x && 3w = 0w) /\ (y && 3w = 0w)`` 328 329val _ = blast_true 330 ``(w2w (x:word30) << 2) :word32 <=+ (w2w (y:word30) << 2) = x <=+ y`` 331 332val _ = blast_true 333 ``(w2w (x:word30) << 2) :word32 <+ (w2w (y:word30) << 2) = x <+ y`` 334 335val _ = blast_true 336 ``((x:word32) && 3w = 0w) /\ ~(x + 4w = 0w) ==> x <+ x + 4w`` 337 338val _ = blast_true 339 ``((x:word32) && 3w = 0w) ==> 340 (((x + y) && 3w = 0w) = ((y:word32) && 3w = 0w))`` 341 342val _ = blast_true 343 ``((x:word32) && 3w = 0w) ==> 344 (((x - y) && 3w = 0w) = ((y:word32) && 3w = 0w))`` 345 346val _ = blast_true 347 ``((x:word32) && 3w = 0w) ==> 348 (((y - x) && 3w = 0w) = ((y:word32) && 3w = 0w))`` 349 350val _ = blast_true 351 ``((x:word32) && 3w = 0w) ==> 352 (((y + x) && 3w = 0w) = ((y:word32) && 3w = 0w))`` 353 354val _ = blast_true 355 ``((x - 4w:word32) && 3w = 0w) = ((x:word32) && 3w = 0w)`` 356 357val _ = blast_true 358 ``((x - 4w * a:word32) && 3w = 0w) = ((x:word32) && 3w = 0w)`` 359 360val _ = blast_true 361 ``((66 >< 0) :bool[67] -> bool[128]) 362 ((((0 >< 0) :bool[unit] -> bool[67]) 363 ~(((65 >< 65) :bool[66] -> bool[unit]) w)) << 65 + 364 (((64 >< 0) :bool[66] -> bool[67]) w) + 0x40000000000000000w) = 365 (((0 >< 0) :bool[unit] -> bool[128]) 366 ~(((65 >< 65) :bool[66] -> bool[unit]) w)) << 65 + 367 (((64 >< 0) :bool[66] -> bool[128]) w) + 0x40000000000000000w`` 368 369val _ = blast_true 370 ``!w. (sw2sw :bool[32] -> bool[64]) w = 371 ((w2w :bool[32] -> bool[64]) 372 ((w2w :bool[16] -> bool[32]) 373 (((15 >< 0) :bool[32] -> bool[16]) w))) + 374 ((sw2sw :bool[16] -> bool[64]) 375 ((w2w :bool[32] -> bool[16]) (w >>> 16))) << 16`` 376 377val _ = blast_true 378 ``!(w: 18 word). 379 (sw2sw w): 32 word = 380 w2w ((16 >< 0) w: 17 word) + 0xfffe0000w + 381 ((0 >< 0) (~(17 >< 17) w:bool [unit]) << 17):32 word`` 382 383val _ = blast_true 384 ``!w:word32. ~word_lsb (w << 2)`` 385 386val _ = blast_true 387 ``!w:word32. ~word_msb (w >>> 2)`` 388 389val _ = blast_true 390 ``!w:word32. word_lsb (w >> 2 #<< 2) = word_msb w`` 391 392val _ = blast_true 393 ``!w:word32. w ' 3 ==> (word_bit 4 ((3 --- 1) w))`` 394 395val _ = blast_true 396 ``!w:word16. word_reverse (word_reverse w) = w`` 397 398val _ = blast_true 399 ``!a b:word8. word_reverse a || word_reverse b = word_reverse (a || b)`` 400 401val _ = blast_true 402 ``(4 >< 1) (bit_field_insert 4 1 (a:word4) (b:word32) + w2w (-a) << 1) = 403 0w:word4`` 404 405val _ = blast_true 406 ``!a b:word8. 407 ~(a ' 3) /\ ~(b ' 3) ==> 408 (((7 >< 4) a + ((7 >< 4) b) : word4) @@ (w2w b + w2w a :word4) = a + b)`` 409 410val _ = blast_true 411 ``~a ' 7 ==> 412 ((31 >< 24) 413 (word_replicate 4 (a:word8) + word_replicate 4 (a:word8) :word32) = 414 2w * a)`` 415 416val _ = blast_true 417 ``!a:word8. a <+ 4w ==> a <+ 8w`` 418 419val _ = blast_true 420 ``!a:word8. a <+ 4w ==> (a + a) <+ 8w`` 421 422val _ = blast_true 423 ``!a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w`` 424 425val _ = blast_true 426 ``w ' 3 ==> (reduce_or (w:word8) <> 0w)`` 427 428val _ = blast_true 429 ``(reduce_or (w:word8) && reduce_or (v:word8)) = 430 ~(reduce_and (~w) || reduce_and (~v))`` 431 432val _ = blast_true 433 ``(0w:word32 = 0xFFFFFFFFw * sw2sw (x :word8)) ==> 434 ~(x ' 1 <=> ~(x ' 0))`` 435 436val _ = blast_true 437 ``if (0w :bool[16]) = (x :bool[16]) && (1024w :bool[16]) then 438 ~(if (0w :bool[16]) = x && (1024w :bool[16]) then 439 $= (((0 :num) >< (0 :num)) (1w :bool[unit]) :bool[unit]) 440 else 441 $= (((0 :num) >< (0 :num)) (0w :bool[unit]) :bool[unit])) (1w 442 :bool[unit]) ==> 443 ((1w :bool[unit]) = ~(1w :bool[unit])) 444 else 445 ~(if (0w :bool[16]) = x && (1024w :bool[16]) then 446 $= (((0 :num) >< (0 :num)) (1w :bool[unit]) :bool[unit]) 447 else 448 $= (((0 :num) >< (0 :num)) (0w :bool[unit]) :bool[unit])) (1w 449 :bool[unit]) ==> 450 ((1w :bool[unit]) = ~(0w :bool[unit]))`` 451 452val _ = blast_true 453 ``SND (word_rrx (T,v:word32)) = v >>> 1 || 0x80000000w`` 454 455val _ = blast_true 456 ``(a:word2) <+ b /\ b <+ c /\ c <+ d ==> (3w * d = 1w)`` 457 458val _ = blast_true 459 ``(m:word8) <+ 4w /\ n <+ 4w ==> (((w <<~ m) <<~ n) = w <<~ (m + n))`` 460 461val _ = blast_true 462 ``(w #<<~ m) #>>~ n = w #<<~ (m - n) : word8`` 463 464val _ = blast_true 465 ``w <+ 10w /\ s <+ 3w ==> w <<~ (s + 1w) <+ 73w : word16`` 466 467val _ = blast_true 468 ``w >>>~ v <=+ w : word16`` 469 470val _ = blast_true 471 ``~word_msb w ==> w >>~ v <= w : word16`` 472 473val _ = blast_true 474 ``w2w (a * b : word4) = 0xFw && (w2w a * w2w b) : word8`` 475 476val _ = blast_true 477 ``(1w <<~ a) * b = b <<~ a : 6 word`` 478 479val _ = blast_true 480 ``a <+ 10w /\ b <+ 10w ==> (a * b <=+ 81w : word8)`` 481 482val _ = blast_true 483 ``(a + x + c + d - e + 0w = c + -(g - x)) = (-e = -(g + d + a))`` 484 485val _ = blast_true 486 ``a << 2 + b = b + a * 4w`` 487 488val _ = blast_true 489 ``(-a * (b + c) + b = -a * b) = (-a * c = -b)`` 490 491val _ = blast_true 492 ``(a + 4w = b + 2w) = (a + 2w = b)`` 493 494val _ = blast_true 495 ``(a + 4w = b - 2w) = (a + 6w = b)`` 496 497val _ = blast_true 498 ``(-a = -b) = (a = b)`` 499 500val _ = blast_true 501 ``(a + 4w = b) = (b + 4w = a : word3)`` 502 503val _ = blast_true 504 ``(x + b * 4w + c * 4w = q + e * 4w - r : word3) = 505 (4w * b + 4w * c + 4w * e + x + r = q)`` 506 507val _ = print "\nsimplifier tests\n\n" 508 509val _ = srw_true 510 ``0x20000000w || 0w || w : word32 = w || 0x20000000w`` 511 512val _ = srw_true 513 ``32w && w && 0w = 0w : word32`` 514 515val _ = srw_true 516 ``15w && a || (a ?? -1w) = word_T: word4`` 517 518val () = print "\nWORD_GROUND_CONV tests\n\n" 519 520val () = qtest_conv wordsLib.WORD_GROUND_CONV 521 `BIT_SET 2 5 = {2; 4} 522 add_with_carry (12w:word8, 11w, T) = (24w,F,F) 523 bit_count (0b101101w: word8) = 4 524 bit_count_upto 3 (0b101101w: word8) = 2 525 concat_word_list [1w; 2w: word8] = 513w: word16 526 l2w 10 [1; 2] : word16 = 21w 527 reduce_and (0xFw: word4) = 1w 528 reduce_nand (0xFw: word4) = 0w 529 reduce_nor (0xFw: word4) = 0w 530 reduce_or (0xFw: word4) = 1w 531 reduce_or (0xFw: word4) = 1w 532 reduce_or (0xFw: word4) = 1w 533 s2w 16 UNHEX "F0" : word8 = 240w 534 saturate_add 12w 4w : word4 = 15w 535 saturate_mul 12w 4w : word4 = 15w 536 saturate_n2w 18 : word4 = 15w 537 saturate_sub 3w 10w : word4 = 0w 538 saturate_w2w (18w: word8) : word4 = 15w 539 sw2sw (15w: word4) : word8 = 255w 540 w2l 2 (0b1011w: word4) = [1; 1; 0; 1] 541 w2n (3w: word4) = 3 542 w2s 16 HEX (0xF0w: word8) = "F0" 543 w2w (15w: word4) : word8 = 15w 544 word_1comp (14w: word4) = 1w 545 word_2comp (14w: word4) = 2w 546 word_H: word8 = 127w 547 word_L: word8 = 128w 548 word_T: word8 = 255w 549 word_abs (255w: word8) = 1w 550 word_add 3w 4w : word8 = 7w 551 word_and 3w 5w : word8 = 1w 552 word_asr_bv 254w 1w : word8 = 255w 553 word_asr 254w 1 : word8 = 255w 554 word_bit 2 (0b101w: word4) = T 555 word_bits 3 2 (0b10101w: word8) = 1w 556 word_compare 3w (4w: word4) = 0w 557 word_concat (3w: word4) (4w: word4) = 52w: word8 558 word_div 8w 2w = 4w : word8 559 word_extract 7 4 (0xF0w: word8) = 15w : word4 560 word_from_bin_list [1; 0; 1; 1] = 0b1101w: word4 561 word_from_bin_string "1011" = 0b1011w: word4 562 word_from_dec_list [9; 8] = 89w: word8 563 word_from_dec_string "89" = 89w: word8 564 word_from_hex_list [10; 11] = 0xBAw: word8 565 word_from_hex_string "BA" = 0xBAw: word8 566 word_from_oct_list [7] = 7w: word8 567 word_from_oct_string "7" = 7w: word8 568 word_ge (3w: word4) 2w = T 569 word_gt (3w: word4) 2w = T 570 word_hi (3w: word4) 2w = T 571 word_hs (3w: word4) 2w = T 572 word_join (3w: word4) (4w: word4) = 52w: (4 + 4) word 573 word_le (3w: word4) 2w = F 574 word_lo (3w: word4) 2w = F 575 word_ls (3w: word4) 2w = F 576 word_lt (3w: word4) 2w = F 577 word_len (3w: word4) = 4 578 word_log2 (3w: word4) = 1w 579 word_lsb (3w: word4) = T 580 word_lsl_bv 254w 1w : word8 = 252w 581 word_lsl 254w 1 : word8 = 252w 582 word_lsr_bv 254w 1w : word8 = 127w 583 word_lsr 254w 1 : word8 = 127w 584 word_max (3w: word4) 2w = 3w 585 word_min (3w: word4) 2w = 2w 586 word_mod (3w: word4) 2w = 1w 587 word_msb (3w: word4) = F 588 word_mul (3w: word4) 2w = 6w 589 word_nand (3w: word4) 2w = 13w 590 word_nor (3w: word4) 2w = 12w 591 word_or (3w: word4) 2w = 3w 592 word_quot 8w 2w = 4w : word8 593 word_replicate 2 (15w: word4) = 0xFFw: word8 594 word_rem (3w: word4) 2w = 1w 595 word_reverse (0b1011w: word4) = 0b1101w 596 word_rol_bv 254w 1w : word8 = 253w 597 word_rol 254w 1 : word8 = 253w 598 word_ror_bv 254w 1w : word8 = 127w 599 word_ror 254w 1 : word8 = 127w 600 word_rrx (T, 254w : word8) = (F, 255w) 601 word_sign_extend 4 (0xFw: word16) = 0xFFFFw 602 word_signed_bits 7 4 (0xE0w: word16) = 0xFFFEw 603 word_slice 7 4 (0xEFw: word16) = 0xE0w 604 word_smax (3w: word4) 2w = 3w 605 word_smin (3w: word4) 2w = 2w 606 word_sub 3w 4w : word8 = 255w 607 word_to_bin_list (0b1011w: word4) = [1; 1; 0; 1] 608 word_to_bin_string (0b1011w: word4) = "1011" 609 word_to_dec_list (1234w: word16) = [4; 3; 2; 1] 610 word_to_dec_string (1234w: word16) = "1234" 611 word_to_hex_list (0x1234w: word16) = [4; 3; 2; 1] 612 word_to_hex_string (0x1234w: word16) = "1234" 613 word_to_oct_list (34w: word16) = [2; 4] 614 word_to_oct_string (34w: word16) = "42" 615 word_xnor 3w 5w : word8 = 249w 616 word_xor 3w 5w : word8 = 6w 617 ` 618 619val elapsed = Timer.checkRealTimer tt 620 621val _ = print ("\nTotal time: " ^ Lib.time_to_string elapsed ^ "\n"); 622 623val _ = OS.Process.exit OS.Process.success 624