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