1loadPath := (concat Globals.HOLDIR "/examples/dev/sw") ::
2            !loadPath;
3
4use (concat Globals.HOLDIR "/examples/dev/sw/compiler");
5
6show_assums := true
7(*---------------------------------------------------------------------------*)
8(*   Simple examples involving function calls                                *)
9(*---------------------------------------------------------------------------*)
10
11val def1 = Define `f1 (x:word32) = x + x + 1w`;
12val spec1 = pp_compile def1 true;
13
14val def2 = Define `f2 x = x * f1 x`;
15val spec2 = pp_compile def2 false;
16
17
18val def3 = Define `f3 x = x + f2 x`;
19val spec3 = pp_compile def3 false;
20
21val def4 = Define `f4(x:word32,y,z) = x + y + y + z`;
22val spec4 = pp_compile def4 false;
23
24val def5 = Define `f5(x:word32,y) = y + (f4 (x, f2 y, y)) + x`;
25val spec5 = pp_compile def5 false;
26
27
28val def6 = Define `f6(x:word32,y) =
29        let a = if (x >= y) then f2 y else x in
30        (y + (f4 (x, a, y)) + x)`;
31
32val spec6_pre = pp_compile def6 false;
33
34(* set_goal___spec_assums  spec6_pre*)
35val spec6 = prove___spec_assums spec6_pre
36(
37REWRITE_TAC[FUN_EQ_THM] THEN
38Cases_on `x` THEN
39SIMP_TAC std_ss [def6, def4, def2, def1, FUN_EQ_THM, LET_THM] THEN
40Cases_on `q >= r` THEN (
41        ASM_SIMP_TAC std_ss [WORD_ADD_ASSOC]
42))
43
44
45val def7 = Define `f7(x:word32,y) =
46        let a = y + (2w * x) in
47        let b = 5w in
48        let c = if (a <= b) then (f2 a) + b else b in
49        let d = f4 (c, c, a) in
50        (x + d + b)`;
51
52val spec7 = pp_compile def7 false;
53
54
55