1(* 2quietdec := true; 3loadPath := 4 (concat Globals.HOLDIR "/examples/dev/sw") :: 5 (concat Globals.HOLDIR "/examples/elliptic/arm") :: 6 (concat Globals.HOLDIR "/examples/elliptic/spec") :: 7 (concat Globals.HOLDIR "/examples/elliptic/sep") :: 8 (concat Globals.HOLDIR "/examples/elliptic/swsep") :: 9 (concat Globals.HOLDIR "/examples/elliptic/c_output") :: 10 !loadPath; 11 12map load ["elliptic_exampleTheory", "c_outputLib"]; 13show_assums := true; 14*) 15 16open HolKernel Parse boolLib bossLib; 17open ellipticTheory; 18open elliptic_exampleTheory; 19open wordsTheory; 20open wordsLib; 21open c_outputLib; 22 23(* 24quietdec := false; 25*) 26 27 28 29val defs = [ex1_field_neg_alt, ex1_field_add_alt, ex1_field_sub_alt, 30 ex1_field_mult_aux_alt, ex1_field_mult_alt, ex1_field_exp_aux_alt, 31 ex1_field_exp_alt, ex1_field_inv_alt, ex1_field_div_alt, 32 ex1_curve_neg_alt, ex1_curve_double_alt, ex1_curve_add_alt, 33 ex1_curve_mult_aux_alt, ex1_curve_mult_alt]; 34val rewrites = []; 35 36 37fun precompile_tests conv (f, tests) = 38 let 39 fun eval_test a = 40 (a, rhs (concl (conv (mk_comb (f, a))))) 41 in 42 (f, map (fn x => (print_term (mk_comb (f, x)); print "\n"; eval_test x)) tests) 43 end 44 45val testArgs_1 = generate_word_pair_list 1 1000 5; 46val testArgs_2 = generate_word_pair_list 2 1000 3; 47val tests_1 = (map (fn f => (f, testArgs_1)) [``ex1_field_neg``]); 48val tests_2 = (map (fn f => (f, testArgs_2)) [``ex1_field_add``, 49 ``ex1_field_sub``]); 50val tests = tests_1 @ tests_2; 51val testsL = map (precompile_tests EVAL) tests 52 53val _ = translate_to_c (concat Globals.HOLDIR "/examples/elliptic/c_output/") "defs" defs rewrites ``ex1_field_neg`` testsL 54