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