1structure inline :> inline = 2struct 3 4open HolKernel Parse boolLib bossLib NormalTheory Normal 5 pairLib pairSyntax PairRules basic; 6 7 8(*---------------------------------------------------------------------------*) 9(* Inline Expansion *) 10(* Replace calls to small functions with their bodies *) 11(*---------------------------------------------------------------------------*) 12 13val threshold = ref 10; 14 15fun size tm = 16 if is_let tm then 17 let val (v,M,N) = dest_plet tm 18 in size M + size N end 19 else if is_pabs tm then 20 size (#2 (dest_pabs tm)) 21 else if is_cond tm then 22 let val (J,M,N) = dest_cond tm 23 in size M + size N + 1 end 24 else if is_pair tm then 25 let val (M,N) = dest_pair tm 26 in size M + size N end 27 else 1 28 29(*---------------------------------------------------------------------------*) 30(* Inline Expansion small anonymous functions defined in the body *) 31(*---------------------------------------------------------------------------*) 32 33fun identify_small_fun tm = 34 let 35 fun trav t = 36 if is_let t then 37 let val (v,M,N) = dest_plet t 38 val M' = if is_pabs M andalso size M < !threshold then 39 mk_comb (inst [alpha |-> type_of M] (Term `fun`), M) 40 else trav M 41 in mk_plet (v, M', trav N) 42 end 43 else t 44 in 45 trav tm 46 end; 47 48fun once_expand_anonymous def = 49 let 50 val t0 = rhs (concl (SPEC_ALL def)) 51 val t1 = identify_small_fun t0 52 val lem0 = REFL t1 53 val lem1 = CONV_RULE (LHS_CONV (REWRITE_CONV [fun_ID])) lem0 54 val thm1 = ONCE_REWRITE_RULE [lem1] def 55 val thm2 = (PBETA_RULE o SIMP_RULE bool_ss [INLINE_EXPAND]) thm1 56 in 57 thm2 58 end 59 60fun expand_anonymous def = 61 let 62 fun expand th = 63 let val th' = once_expand_anonymous th 64 in 65 if concl th' = concl th then th' 66 else expand th' 67 end 68 handle e => th (* Unchanged *) 69 in 70 expand def 71 end 72 73(*---------------------------------------------------------------------------*) 74(* Inline Expand small named functions *) 75(* Retrieve pre-defined functions stored in the environment *) 76(*---------------------------------------------------------------------------*) 77 78val unroll_limit = ref 3; 79 80fun mk_inline_rules env = 81 let fun unroll defth = 82 let val (name,body) = dest_eq (concl defth) 83 in if occurs_in name body 84 then PBETA_RULE (* unroll the function *) 85 (CONV_RULE (RHS_CONV 86 (REWRITE_CONV 87 [Ntimes defth (!unroll_limit)])) defth) 88 else 89 defth 90 end 91 in 92 List.map (unroll o abs_fun) env 93 end 94 95fun expand_named env def = 96 let 97 val rules = mk_inline_rules env 98 val thm1 = (PBETA_RULE o ONCE_REWRITE_RULE rules) def (* inline expansion *) 99 in 100 thm1 101 end 102 103 104(*---------------------------------------------------------------------------*) 105(* Optimization on Normal Forms: *) 106(* 1. SSA forms *) 107(* 2. Inline expansion *) 108(* 3. Simplification of let-expressions (atom_let, flatten_let, useless_let*) 109(* 4. Constant folding *) 110(* 5. Beta-reduction (a special case of constant folding) *) 111(*---------------------------------------------------------------------------*) 112 113fun optimize th = 114 let val lem1 = SIMP_RULE arith_ss [] th (* constant folding *) 115 val lem2 = beta_reduction lem1 (* beta_reduction *) 116 in 117 if concl lem2 = concl th then lem2 118 else optimize lem2 119 end 120 121fun optimize_norm env def = 122 let 123 val th1 = SSA_RULE def 124 val th2 = expand_anonymous th1 125 val th3 = expand_named env th2 126 val th4 = optimize th3 127 val th5 = SIMP_RULE bool_ss [FLATTEN_LET] th4 128 val th6 = beta_reduction th5 129 in 130 th6 131 end 132 133end (* struct *) 134