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