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