1structure c_outputLib :> c_outputLib = 2struct 3 4(* 5quietdec := true; 6loadPath := 7 (concat Globals.HOLDIR "/examples/dev/sw") :: 8 (concat Globals.HOLDIR "/examples/elliptic/arm") :: 9 (concat Globals.HOLDIR "/examples/elliptic/spec") :: 10 (concat Globals.HOLDIR "/examples/elliptic/sep") :: 11 (concat Globals.HOLDIR "/examples/elliptic/swsep") :: 12 !loadPath; 13 14show_assums := true; 15map load ["wordsLib"]; 16*) 17 18open HolKernel Parse boolSyntax Drule Rewrite wordsTheory wordsLib; 19 20(* 21quietdec := false; 22*) 23 24 25val word_type = Type `:word32` 26 27fun get_word_type_arity t n = 28 let 29 val (fname, l) = dest_type t; 30 in 31 if (fname = "prod") then ( 32 if (el 1 l = word_type) then 33 get_word_type_arity (el 2 l) (n+1) 34 else 35 (~1) 36 ) else ( 37 if (t = word_type) then (n+1) else (~1) 38 ) 39 end 40 41 42fun get_word_fun_arity t = 43 let 44 val (fname, l) = dest_type t 45 in 46 if (fname = "fun") then 47 let 48 val a1 = get_word_type_arity (el 1 l) 0; 49 val a2 = get_word_type_arity (el 2 l) 0; 50 in 51 (a1, a2) 52 end 53 else 54 (0, get_word_type_arity t 0) 55 end 56 57fun add_consts t set = 58 if (numSyntax.is_numeral t) then set 59 else if (is_const t) then 60 (if ( 61 (same_const let_tm t) orelse 62 (same_const conditional t) 63 )then 64 set 65 else 66 (HOLset.add (set, t))) 67 else if (is_abs t) then 68 add_consts (#2 (dest_abs t)) set 69 else if (pairSyntax.is_pair t) then 70 let 71 val (t1, t2) = pairSyntax.dest_pair t 72 val set = add_consts t1 set; 73 val set = add_consts t2 set; 74 in 75 set 76 end 77 else if (is_eq t) then 78 let 79 val (t1, t2) = dest_eq t; 80 val set = add_consts t1 set; 81 val set = add_consts t2 set; 82 in 83 set 84 end 85 else if (pairLib.is_pabs t) then 86 let 87 val (_, t) = pairLib.dest_pabs t; 88 val set = add_consts t set; 89 in 90 set 91 end 92 else if (is_comb t) then 93 let 94 val (t1, t2) = dest_comb t; 95 val set = add_consts t1 set; 96 val set = add_consts t2 set; 97 in 98 set 99 end 100 else set; 101 102val known_consts_list = [ 103 Term `($+):word32->word32->word32`, 104 Term `($-):word32->word32->word32`, 105 Term `($*):word32->word32->word32`, 106 Term `($>>>):word32->num->word32`, 107 Term `($&&):word32->word32->word32`, 108 Term `($!!):word32->word32->word32`, 109 Term `($??):word32->word32->word32`, 110 Term `($=):word32->word32->bool`, 111 Term `($<):word32->word32->bool`, 112 Term `($<+):word32->word32->bool`, 113 Term `($/\):bool->bool->bool`, 114 Term `($\/):bool->bool->bool`, 115 Term `($~):bool->bool`, 116 Term `n2w:num->word32` 117]; 118 119val known_consts_set = HOLset.addList (Term.empty_tmset, known_consts_list) 120 121 122fun get_unknown_consts tL = 123 let 124 val c_set = foldl (fn (t, s) => add_consts t s) Term.empty_tmset tL; 125 in 126 HOLset.difference (c_set,known_consts_set) 127 end; 128 129 130fun indent_block l = 131 map (fn s => (" "^s)) l 132 133exception SYNTAX_EXCEPTION; 134fun syntax_error c m = 135 if c then 136 let 137 val _ = print ("!! "^m^"\n"); 138 in 139 raise SYNTAX_EXCEPTION 140 end 141 else 142 () 143 144val max_used_word_type = ref 1; 145fun get_word_type n = 146 let 147 val _ = if (n > !max_used_word_type) then 148 (max_used_word_type := n) else () 149 in 150 if (n = 1) then "word32" else 151 ("word32_"^Int.toString n) 152 end 153fun get_signed_word_type () = "s_"^(get_word_type 1); 154 155fun c_get_word_type n = 156 if (n = 1) then ["typedef unsigned int "^(get_word_type n)^";"] else 157 let 158 val name = get_word_type n; 159 val word_type_1 = get_word_type 1; 160 val decl = "typedef struct "^name^"_tag {" 161 val acc_list = List.tabulate (n, fn n => (word_type_1^" e"^(Int.toString (n+1))^";")) 162 val end_line = "} "^name^";" 163 in 164 [decl]@(indent_block acc_list)@[end_line] 165 end 166 167fun c_get_signed_word_type () = 168 ["typedef signed int "^(get_signed_word_type ())^";"] 169 170val temp_var_count = ref 0; 171fun get_new_temp_var () = 172 let 173 val _ = (temp_var_count := !temp_var_count + 1); 174 in 175 "temp_"^Int.toString (!temp_var_count) 176 end; 177 178 179 180fun translate_fun f argL = 181 if (same_const f wordsSyntax.word_add_tm) then 182 ([], "("^(hd (el 1 argL))^" + "^(hd (el 2 argL))^")") 183 else if (same_const f wordsSyntax.word_sub_tm) then 184 ([], "("^(hd (el 1 argL))^" - "^(hd (el 2 argL))^")") 185 else if (same_const f wordsSyntax.word_and_tm) then 186 ([], "("^(hd (el 1 argL))^" & "^(hd (el 2 argL))^")") 187 else if (same_const f wordsSyntax.word_or_tm) then 188 ([], "("^(hd (el 1 argL))^" | "^(hd (el 2 argL))^")") 189 else if (same_const f wordsSyntax.word_xor_tm) then 190 ([], "("^(hd (el 1 argL))^" ^ "^(hd (el 2 argL))^")") 191 else if (same_const f wordsSyntax.word_lsr_tm) then 192 ([], "("^(hd (el 1 argL))^" >> "^(hd (el 2 argL))^")") 193 else 194 let 195 val argL' = if argL = [] then [] else el 1 argL; 196 val (f_name, f_type) = dest_const f; 197 val (arg_n, res_n) = get_word_fun_arity (f_type); 198 val _ = syntax_error (not (arg_n = length argL') orelse 199 (res_n <= 0) 200 ) ("Unknown function '"^f_name^"'!") 201 val args_string = String.concat (commafy argL'); 202 in 203 ([], f_name^"("^args_string^")") 204 end 205 206 207(* 208 val (exp, n) = (true_exp, 1); 209*) 210 211fun translate_exp exp n = 212 let 213 fun translate_bool_exp exp = 214 if (exp = T) then ([], "1") 215 else if (exp = F) then ([], "0") 216 else if (is_neg exp) then 217 let 218 val exp' = dest_neg exp; 219 val (inst, exp_s) = translate_bool_exp exp'; 220 in 221 (inst, "(!"^exp_s^")") 222 end 223 else if (is_conj exp) then 224 let 225 val (exp1, exp2) = dest_conj exp; 226 val (inst1, exp_s1) = translate_bool_exp exp1; val (inst2, exp_s2) = translate_bool_exp exp2; 227 in 228 (inst1@inst2, "("^exp_s1^" && "^exp_s2^")") 229 end 230 else if (is_disj exp) then 231 let 232 val (exp1, exp2) = dest_disj exp; 233 val (inst1, exp_s1) = translate_bool_exp exp1; val (inst2, exp_s2) = translate_bool_exp exp2; 234 in 235 (inst1@inst2, "("^exp_s1^" || "^exp_s2^")") 236 end 237 else if (is_comb exp) then 238 let 239 val (f, args) = strip_comb exp; 240 val _ = syntax_error ((not (length args = 2)) orelse 241 ((not (all (fn arg => (type_of arg = word_type)) args)))) 242 ("Unknown boolean function '"^(term_to_string exp)^"'!"); 243 val (signed, operator) = 244 if (same_const f boolSyntax.equality) then 245 (false, "==") 246 else if (f = ``($<+):word32->word32->bool``) then 247 (false, "<") 248 else if (f = ``($<):word32->word32->bool``) then 249 (true, "<") 250 else 251 (syntax_error true ("Unknown boolean function '"^(term_to_string exp)^"'!"); (false, "")); 252 253 val (inst1, arg1) = translate_exp (el 1 args) 1; 254 val (inst2, arg2) = translate_exp (el 2 args) 1; 255 256 val signed' = if signed then ("("^(get_signed_word_type ())^") ") else ""; 257 258 in 259 (inst1@inst2, "("^signed'^(hd arg1)^" "^operator^" "^signed'^(hd arg2)^")") 260 end 261 else (syntax_error true "Unknown boolean expression!"; ([], "")); 262 263 fun translate_exp_bool exp n = 264 if (type_of exp = bool) then 265 let 266 val (instL, s) = translate_bool_exp exp 267 in 268 (instL, [s]) 269 end 270 else 271 translate_exp exp n 272 273 fun translate_args arg = 274 if (numLib.is_numeral arg) then 275 ([], [term_to_string arg]) 276 else 277 let 278 val (args_n, res_n) = 279 get_word_fun_arity (type_of arg); 280 val _ = syntax_error ((not (args_n = 0)) orelse 281 (res_n <= 0)) 282 ("Invalid argument '" ^ (term_to_string arg) ^"' in term '"^(term_to_string exp)^"'!"); 283 in 284 translate_exp arg res_n 285 end 286 287 fun data_assingment var_name argL = 288 if ((length argL) = 1) then 289 ([var_name^" = "^(hd argL)^";"]) 290 else 291 map (fn (n,e) => var_name^".e"^(Int.toString n)^" = "^e^";") (enumerate 1 argL) 292 293 in 294 if ((wordsSyntax.is_n2w exp) orelse 295 (numLib.is_numeral exp)) then 296 ([], [Int.toString(numSyntax.int_of_term (rand exp))]) 297 else if (is_var exp) then 298 let 299 val var_name = #1 (dest_var exp); 300 val expL = if (n = 1) then [var_name] else 301 (List.tabulate (n, fn n => var_name^".e"^(Int.toString (n+1)))) 302 in 303 ([], expL) 304 end 305 else if (is_cond exp) then 306 let 307 val (cond_exp, true_exp, false_exp) = dest_cond exp; 308 val temp_var = get_new_temp_var (); 309 val a = get_word_type_arity (type_of exp) 0; 310 val _ = syntax_error (not ((n = 1) orelse (n = a))) 311 "Wrong arrity of condition!"; 312 val temp_type = get_word_type a; 313 val decl = temp_type^" "^temp_var^";"; 314 315 val (cond_inst, cond_exp') = translate_bool_exp cond_exp; 316 val (true_inst, true_exp') = translate_exp true_exp a; 317 val (false_inst, false_exp') = translate_exp false_exp a; 318 319 val if_1 = "if ("^cond_exp'^") {" 320 val if_1e = data_assingment temp_var true_exp'; 321 val if_2 = "} else {" 322 val if_2e = data_assingment temp_var false_exp'; 323 val if_3 = "}"; 324 325 val expL = if (n=1) then [temp_var] else 326 (List.tabulate (n, fn n => temp_var^".e"^(Int.toString (n+1)))) 327 in 328 (cond_inst@[decl]@([if_1]@(indent_block (true_inst@if_1e))@[if_2]@ 329 (indent_block (false_inst@if_2e))@[if_3]), 330 expL) 331 end 332 else if (pairLib.is_pair exp) then 333 let 334 val expL = pairLib.strip_pair exp; 335 val expL' = map translate_args expL 336 val (args_insts, args_exp) = unzip expL'; 337 val args_insts = List.concat args_insts; 338 val args_exp = List.concat args_exp; 339 val _ = syntax_error ((not (length (args_exp) = n)) andalso 340 (not (n = 1))) 341 "Invalid arity!"; 342 in 343 (args_insts, args_exp) 344 end 345 else if (is_let exp) then 346 let 347 val (body, rhs) = dest_let exp; 348 val (lhs, body) = pairLib.dest_pabs body; 349 val lhsL = pairLib.strip_pair lhs; 350 val lhsL' = map (fn t => #1 (dest_var t)) lhsL; 351 val (pre, rhsL) = translate_exp_bool rhs (length lhsL); 352 val assignments = map (fn (s1, s2) => (s1^" = "^s2^";")) (zip lhsL' rhsL); 353 val (x, exp_s) = translate_exp body n; 354 in 355 (pre@assignments@x, exp_s) 356 end 357 else if ((is_comb exp) orelse (is_const exp)) then 358 let 359 val (f, args) = strip_comb exp; 360 val args_exp = map translate_args args; 361 val (args_insts, args_exp) = unzip args_exp; 362 val args_insts = List.concat args_insts; 363 val (fun_insts, fun_exp) = translate_fun f args_exp; 364 val (extra_insts, expL) = if (n = 1) then ([], [fun_exp]) else 365 let 366 val temp_var = get_new_temp_var (); 367 val a = get_word_type_arity (type_of exp) 0; 368 val temp_type = get_word_type a; 369 val decl = temp_type^" "^temp_var^";"; 370 val assignment = temp_var ^ " = "^fun_exp^";" 371 val expL = (List.tabulate (n, fn n => temp_var^".e"^(Int.toString (n+1)))) 372 in 373 ([decl,assignment], expL) 374 end 375 in 376 (args_insts@fun_insts@extra_insts, expL) 377 end 378 else 379 let 380 val _ = syntax_error true ("Unknown expression '"^(term_to_string exp)^"'!") 381 in 382 ([], ["ERROR"]) 383 end 384 end; 385 386fun print_insts l = 387let 388 val _ = print "\n\n"; 389 val _ = map (fn s => print (s^"\n")) l 390 val _ = print "\n\n"; 391in 392 () 393end 394 395 396 397fun std_bvars stem tm = 398 let 399 open Lib 400 fun num2name i = stem^Lib.int_to_string i 401 val nameStrm = Lib.mk_istream (fn x => x+1) 0 num2name 402 fun next_name () = state(next nameStrm) 403 fun trav M = 404 if is_comb M then 405 let val (M1,M2) = dest_comb M 406 val M1' = trav M1 407 val M2' = trav M2 408 in mk_comb(M1',M2') 409 end else 410 if is_abs M then 411 let val (v,N) = dest_abs(rename_bvar (next_name()) M) 412 in mk_abs(v,trav N) 413 end 414 else M 415 in 416 trav tm 417 end; 418 419fun STD_BVARS_CONV stem tm = 420 let val tm' = std_bvars stem tm 421 in Thm.ALPHA tm tm' 422 end; 423 424fun is_valid_c_indentifier s = 425 all (fn c => not (c = #"'")) (String.explode s) 426 427fun dest_fun_def def = 428 let 429 val def_term = concl (SPEC_ALL def); 430 val (fun_const, args) = strip_comb (lhs def_term); 431 val body = rhs def_term; 432 val (fun_name, fun_type) = dest_const fun_const 433 val (arg_n, return_n) = get_word_fun_arity fun_type; 434 val _ = syntax_error ((return_n <= 0) orelse (arg_n < 0) orelse 435 (length args > 1)) 436 ("The function '"^fun_name^"' is not a function on 32-bit words!"); 437 val args_fv = FVL args Term.empty_varset 438 val body_fv = FVL [body] Term.empty_varset 439 val _ = syntax_error (not (HOLset.isSubset (args_fv, body_fv))) 440 ("There are free variables in the definition of '"^ 441 fun_name^"'!") 442 val body_av = HOLset.addList (Term.empty_varset, Term.all_vars body); 443 val body_bv = HOLset.difference (body_av, body_fv); 444 val body_bv_list = HOLset.listItems body_bv; 445 446 val args_list = if (args=[]) then [] else (pairLib.strip_pair (hd args)); 447 in 448 (def_term, args_list, body_bv_list, body, fun_name, arg_n, return_n) 449 end; 450 451 452fun normalise_fun_def def force = 453 let 454 val (def_term, args_list, body_bv_list, body, fun_name, arg_n, return_n) = dest_fun_def def; 455 456 val valid_bv = all (fn v => is_valid_c_indentifier (#1 (dest_var v))) body_bv_list; 457 val def = SPEC_ALL def; 458 val def' = if (force orelse not valid_bv) then 459 Conv.CONV_RULE (Conv.RHS_CONV (STD_BVARS_CONV "v")) def 460 else def 461 462 val valid_args = all (fn v => is_valid_c_indentifier (#1 (dest_var v))) args_list; 463 464 val def'' = if (force orelse not valid_args) then 465 let 466 val ren = enumerate 1 args_list; 467 val ren' = map (fn (n, t) => 468 ({redex=t, residue = mk_var ("a"^(Int.toString n), word_type)})) ren; 469 in 470 Thm.INST ren' def' 471 end 472 else def' 473 in 474 def'' 475 end 476 477 478fun translate_fun_to_c def = 479 let 480 val _ = temp_var_count := 0; 481 val def = normalise_fun_def def false; 482 val (def_term, args_list, body_bv_list, body, fun_name, arg_n, return_n) = dest_fun_def def; 483 val def_string = "/* "^(term_to_string def_term)^ " */"; 484 485 val word_type_string = get_word_type 1; 486 val args_string_list = map (fn arg => 487 word_type_string^ " "^(#1 (dest_var arg))) args_list; 488 val args_string = String.concat (commafy args_string_list); 489 val fun_sig = get_word_type (return_n) ^ " "^fun_name^ " ("^args_string^")"; 490 val var_decl = map (fn v => 491 let 492 val (var_name, var_type) = dest_var v; 493 val var_type_string = if (var_type = bool) then "bool" else 494 let 495 val arity = get_word_type_arity var_type 0 496 val _ = syntax_error (arity <= 0) ("Variable '"^var_name^"' is not of type bool or a word type!"); 497 in 498 get_word_type arity 499 end 500 in 501 (var_type_string ^ " " ^ var_name ^ ";") 502 end) body_bv_list 503 val (body_inst, body_exp) = translate_exp body 1 504 val return_inst = "return "^(hd body_exp)^";"; 505 val instL = [def_string,fun_sig^" {"]@(indent_block (var_decl @ body_inst @ [return_inst]))@["}"] 506 in 507 (fun_sig^";", instL) 508 end 509 510 511fun create_tests testL = 512 let 513 val _ = temp_var_count := 0; 514 515 fun create_f_test (f, tests) = 516 let 517 val (f_name, f_type) = dest_const f; 518 val (args_n, res_n) = get_word_fun_arity f_type; 519 val res_var = get_new_temp_var (); 520 521 val decl_ret = (get_word_type res_n)^" "^res_var^";"; 522 fun create_single_test (arg, res) = 523 let 524 val args = pairLib.strip_pair arg; 525 val args_string = map (fn t => 526 Arbnum.toString (numLib.dest_numeral (rand t))) args; 527 val args_s = String.concat (commafy args_string) 528 val fun_call = res_var^" = "^f_name^"("^args_s^");" 529 530 val ress = pairLib.strip_pair res; 531 val ress_string = map (fn t => 532 Arbnum.toString (numLib.dest_numeral (rand t))) ress; 533 534 val conditionL = if (res_n = 1) then 535 ["("^res_var^" == "^(hd ress_string)^")"] 536 else 537 (List.tabulate (res_n, (fn n => 538 "("^res_var^".e"^(Int.toString (n+1))^ 539 " == "^(el (n+1) ress_string) ^")"))) 540 val condition = foldl (fn (s1, s2) => s1 ^ " & "^s2) "1" conditionL; 541 542 543 val error_message = "Test of '"^f_name^"("^args_s^")' failed!\n"; 544 val res_words = if (res_n) = 1 then [res_var] else 545 (List.tabulate (res_n, (fn n => 546 res_var^".e"^(Int.toString (n+1))))); 547 val print_results = map (fn s=>"printf(\"- %ud\\n\", "^s^"); ") res_words; 548 549 val error_inst = "if (! ("^condition^")) { printf(\""^(String.toCString error_message)^"\"); "^(String.concat print_results)^"};" 550 in 551 [fun_call,error_inst] 552 end 553 554 val test_insts = map create_single_test tests 555 in 556 decl_ret::(List.concat test_insts)@[""] 557 end; 558 559 val all_tests = List.concat (map create_f_test testL) 560 in 561 ["void auto_tests() {"]@(indent_block all_tests)@["}"] 562 end 563 564 565fun create_main main_fun = 566let 567 val (f_name, f_type) = dest_const main_fun; 568 val (args_n, res_n) = get_word_fun_arity f_type; 569 val decl_ret = (get_word_type res_n)^" res;"; 570 val word_type_string = get_word_type 1; 571 val args_list = List.tabulate (args_n, fn n => 572 ("a"^(Int.toString (n+1)))) 573 val decl_args = map (fn s => 574 (word_type_string^" "^s^";")) args_list; 575 val f_string = f_name^"("^(String.concat (commafy args_list))^")"; 576 val print_fun = "printf(\""^f_string^"\\n\");" 577 578 val read_args = map (fn s => 579 ("printf(\""^s^": \"); if (scanf(\"%ud\", &"^s^") == 0) exit(0);")) args_list 580 val execution = "res = "^f_string^";" 581 582 val res_words = if (res_n) = 1 then ["res"] else 583 (List.tabulate (res_n, (fn n => 584 "res.e"^(Int.toString (n+1))))); 585 val print_results = map (fn s=>"printf(\"- %ud\\n\", "^s^");") res_words; 586 val print_space = "printf(\"\\n\\n\");" 587 588 val body = [print_fun]@read_args@[execution,print_space]@print_results@[print_space] 589 590 val run_auto_tests = ["auto_tests();", "", ""]; 591 val body' = run_auto_tests@decl_args@[decl_ret]@["","while (1) {"]@ 592 (indent_block body)@["}"] 593in 594 ["main () {"]@(indent_block body')@["}"] 595end; 596 597 598 599 600 601fun translate_to_c dirname filename defs rewrites main_fun tests = 602 let 603 val defs' = (map (SPEC_ALL o (REWRITE_RULE rewrites)) defs) 604 fun extract_fun_const def = (#1 (strip_comb (lhs (concl (SPEC_ALL def))))) 605 val defined_funs = map extract_fun_const defs'; 606 val defs'' = zip (map dest_const defined_funs) defs'; 607 val defs'' = Listsort.sort (fn (((s1, _), _), ((s2, _),_)) => String.compare (s1, s2)) defs''; 608 609 (*check for undefined functions*) 610 val defined_funs_set = HOLset.addList (Term.empty_tmset, defined_funs); 611 val _ = if (not (HOLset.member (defined_funs_set, main_fun))) then 612 (print "The main function is not in the list of definitions!\n";fail()) else (); 613 614 val unknown_consts = get_unknown_consts (map concl defs'); 615 val unknown_consts = HOLset.difference (unknown_consts, defined_funs_set); 616 val unknown_consts_list = HOLset.listItems unknown_consts; 617 val _ = if (unknown_consts_list = []) then () else 618 let 619 val _ = print "The following constants are unkown to the C-export function. Please add additional definitions or rewrites:\n"; 620 val _ = map (fn t => (print " - ";print_term t;print "\n")) unknown_consts_list 621 in 622 fail() 623 end 624 625 val _ = max_used_word_type := 1; 626 val (fun_decl, fun_defs) = unzip (map (fn (_, def) => translate_fun_to_c def) defs''); 627 628(* val def = #2 (el 1 defs''); 629 translate_fun_to_c def; 630*) 631 632 val fun_defs = List.concat (map (fn l => l@["","",""]) fun_defs); 633 634 val word_type_defs = (c_get_signed_word_type()):: (List.tabulate ((!max_used_word_type), fn n => c_get_word_type (n+1))); 635 val word_type_defs = List.concat (map (fn l => l@[""]) word_type_defs); 636 637 val auto_test = create_tests tests; 638 val main_fun_def = create_main main_fun; 639 val spaces = ["",""]; 640 641 642 (*write header file*) 643 val file_name_header = filename^".h"; 644 val file_name_header_guard = filename^"_H"; 645 646 val file_st = TextIO.openOut(dirname^file_name_header); 647 val _ = map (fn s => TextIO.output(file_st, s^"\n")) 648 (["#ifndef "^file_name_header_guard, "#define "^file_name_header_guard, ""]@word_type_defs@spaces@fun_decl@["","#endif"]); 649 val _ = TextIO.output(file_st, "\n\n"); 650 val _ = TextIO.flushOut file_st; 651 val _ = TextIO.closeOut file_st; 652 653 (*write fun_defs*) 654 val inits = ["#include <stdio.h>", 655 "#include \""^file_name_header^"\""]; 656 val file_name_c = filename^".c"; 657 val file_st = TextIO.openOut(dirname^file_name_c); 658 val _ = map (fn s => TextIO.output(file_st, s^"\n")) 659 (inits@spaces@fun_defs); 660 val _ = TextIO.output(file_st, "\n\n"); 661 val _ = TextIO.flushOut file_st; 662 val _ = TextIO.closeOut file_st; 663 664 665 (*write test*) 666 val file_name_test = filename^"-test.c"; 667 val file_st = TextIO.openOut(dirname^file_name_test); 668 val _ = map (fn s => TextIO.output(file_st, s^"\n")) 669 (inits@spaces@auto_test@spaces@main_fun_def); 670 val _ = TextIO.output(file_st, "\n\n"); 671 val _ = TextIO.flushOut file_st; 672 val _ = TextIO.closeOut file_st; 673 in 674 () 675 end 676 677val r = Random.newgen (); 678 679fun generate_word max = 680 let 681 val n = if (max = 0) then 682 let 683 val l = Random.rangelist (0, 65536) (2, r); 684 val n1 = Arbnum.fromInt (el 1 l); 685 val n2 = Arbnum.* (Arbnum.fromInt (el 2 l), Arbnum.fromInt 65536); 686 val n = Arbnum.+ (n1, n2); 687 in 688 n 689 end 690 else 691 Arbnum.fromInt (Random.range (0, max) r) 692 in 693 mk_comb (Term `n2w:num->word32`, numSyntax.mk_numeral n) 694 end; 695 696fun generate_word_pair n max = 697 let 698 val wL = List.tabulate (n, fn n => generate_word max); 699 in 700 pairSyntax.list_mk_pair wL 701 end; 702 703fun generate_word_pair_list n max m = 704 List.tabulate (m, fn x => generate_word_pair n max); 705 706end; 707