1structure SALGen :> SALGen =
2struct
3
4(* Interactive
5quietdec := true;
6app load ["pairLib","basic", "SALTheory"];
7open pairLib pairSyntax PairRules numSyntax basic SALTheory;
8quietdec := false;
9*)
10
11open HolKernel Parse boolLib pairLib pairSyntax bossLib ;
12open PairRules numSyntax basic SALTheory;
13
14val ERR = mk_HOL_ERR "SALGen";
15
16(* --------------------------------------------------------------------*)
17(* Generate SAL code for a FIL program                                 *)
18(* --------------------------------------------------------------------*)
19
20structure M = Binarymap
21structure S = Binaryset
22val VarType = ref (Type `:word32`) (* numSyntax.num *)
23
24(* --------------------------------------------------------------------*)
25(* Datatypes, Commonly-used variables and functions                    *)
26(* --------------------------------------------------------------------*)
27
28val nop = prim_mk_const{Name="NOP",Thy="SAL"};
29val reduce_tm = prim_mk_const{Name="Reduce",Thy="SAL"};
30val union_tm = prim_mk_const{Name="UNION",Thy="SAL"};
31val asg_tm = prim_mk_const{Name="ASG",Thy="SAL"};
32val ifgoto_tm = prim_mk_const{Name="IFGOTO",Thy="SAL"};
33val goto_tm = prim_mk_const{Name="GOTO",Thy="SAL"};
34
35fun dest_composite ty =
36 case total dest_thy_type ty
37  of SOME {Tyop="COMPOSITE",Thy="SAL",Args=[x]} => x
38   | other => raise ERR "dest_composite" "";
39
40(* --------------------------------------------------------------------*)
41(* Auxiliary functions manipulating labels                             *)
42(* --------------------------------------------------------------------*)
43
44val label_tm = prim_mk_const{Name="L",Thy="SAL"};
45
46fun mk_label i = mk_comb(label_tm, term_of_int i);
47
48val label_index = ref 0;
49
50fun reset_label () = label_index := 0
51fun cur_label() = mk_label (!label_index)
52
53fun next_label () =
54  let val _ = label_index := !label_index + 1;
55  in
56      mk_label (!label_index)
57  end;
58
59(* ---------------------------------------------------------------------*)
60(* Mechanism for mechanical reasoning                                   *)
61(* A specification stores all information about a FIL program including *)
62(* a theorem stating that the SAL code "implements" the FIL program.    *)
63(* The composition of specifications is directed by the syntax of the   *)
64(* program and goes in a bottom-up manner.                              *)
65(* ---------------------------------------------------------------------*)
66
67type spec_type = {body : term, dst : term, entry : term, exit : term, exp : term, thm : thm}
68
69(* Make a basic specification for single assignment instruction *)
70
71fun mk_instr_spec (entry_l,exit_l) (dest,src) =
72  let
73    val ty = type_of dest
74    val value = mk_pair (src, dest)
75    val instr = list_mk_comb (inst [alpha |-> ty] asg_tm, [entry_l, dest, src, exit_l])
76    val s = list_mk_pair [entry_l, instr, exit_l]
77    val spec = list_mk_comb(inst [alpha |-> ty] reduce_tm, [s, value])
78    val spec_thm = prove(spec, SIMP_TAC std_ss [inst_rule])
79  in
80    {entry = entry_l, exit = exit_l, body = instr, thm = spec_thm, exp = src, dst = dest}
81  end
82
83(* Union of two structures (i.e. sequential composition *)
84
85fun mk_union_spec (spec1:spec_type) (spec2:spec_type) =
86  let (*  s1 |+| s2 *)
87      val union_body = list_mk_comb(inst [alpha |-> !VarType] union_tm, [#body spec1, #body spec2])
88      val exp = mk_plet (#dst spec1, #exp spec1,
89                         mk_comb(mk_pabs (#dst spec1, #exp spec2), #dst spec1))
90      val value = mk_pair(exp, #dst spec2)
91      val s = list_mk_pair [#entry spec1, union_body, #exit spec2]
92      val spec = list_mk_comb(inst [alpha |-> !VarType] reduce_tm, [s, value])
93
94      val spec_lem =  prove (spec,   (* set_goal ([], spec) *)
95                       MATCH_MP_TAC seq_rule THEN
96                       EXISTS_TAC (#exit spec1) THEN EXISTS_TAC (#dst spec1) THEN
97                       PBETA_TAC THEN
98                       REWRITE_TAC [#thm spec1, #thm spec2]
99                      )
100     val spec_thm = PBETA_RULE spec_lem
101  in
102     {entry = #entry spec1, exit = #exit spec2, body = union_body, thm = spec_thm, exp = exp, dst = #dst spec2}
103  end
104
105(* --------------------------------------------------------------------*)
106(* Eliminate the deepest "let" expression. It is for optiomization.    *)
107(* --------------------------------------------------------------------*)
108
109val ELIM_DEEP_LET_CONV =
110   let
111     val elim_deep_let_conv = (fn t => (DEPTH_CONV (SIMP_CONV bool_ss [Once LET_THM])) t)
112   in
113     RATOR_CONV elim_deep_let_conv THENC
114     RAND_CONV elim_deep_let_conv
115   end;
116
117(* --------------------------------------------------------------------*)
118(* Compose the specifications in a bottom-up manner.                   *)
119(* --------------------------------------------------------------------*)
120
121(* Generate specification for conditional structures.                  *)
122
123fun mk_cond_spec (entry_l,exit_l) (dest,src) args =
124   let
125       val (J,M1,M2) = dest_cond src
126
127       val args = hd(free_vars J)
128       val c = mk_pabs(args,J)
129       val (l1,l2,l3,l4) = (entry_l,next_label(),next_label(),exit_l)
130       val ifgoto = list_mk_comb(inst [alpha |-> !VarType] ifgoto_tm, [l1, c, l2, l3])
131       val spec1 = gen_code (l2,M1,l4) (args,dest)
132       val spec2 = gen_code (l3,M2,l4) (args,dest)
133
134       val b1 = list_mk_comb(inst [alpha |-> !VarType] union_tm, [ifgoto, #body spec1])
135       val b2 = list_mk_comb(inst [alpha |-> !VarType] union_tm, [b1, #body spec2])
136       val s = list_mk_pair [l1, b2, l4]
137
138       val exp = mk_cond (mk_comb(c,args),
139                          mk_comb(mk_pabs(args, #exp spec1), args),
140                          mk_comb(mk_pabs(args, #exp spec2), args))
141       val value = mk_pair(exp, dest)
142       val spec = list_mk_comb(inst [alpha |-> !VarType] reduce_tm, [s, value])
143
144       val spec_lem =  prove (spec,   (* set_goal ([], spec) *)
145                              MATCH_MP_TAC CONDITIONAL_RULE THEN
146                              PBETA_TAC THEN
147                              REWRITE_TAC [#thm spec1, #thm spec2]
148                              )
149       val spec_thm = PBETA_RULE spec_lem
150       val exp' = mk_cond (J, #exp spec1, #exp spec2)
151
152(*     val t = #1 (dest_pair (List.last (#2 (strip_comb (concl spec_lem1)))))
153       val lem = ELIM_DEEP_LET_CONV t handle _ => REFL t
154       val spec_thm = ONCE_REWRITE_RULE [lem] spec_lem1
155*)
156    in
157       {entry = entry_l, exit = exit_l, body = b2, thm = spec_thm, exp = exp', dst = dest}
158    end
159
160and
161
162(* The composition is syntax directed.             *)
163
164mk_spec (entry_l,exit_l) (dest,src) args =
165    if is_atomic src orelse is_pair src then
166        mk_instr_spec (entry_l,exit_l) (dest,src)
167
168    else if is_cond src then                 (*  t = if P then M else N *)
169        mk_cond_spec (entry_l,exit_l) (dest,src) args
170
171    else if is_comb src then
172      let val (operator, operands) = strip_comb src
173      in
174        if basic.is_binop operator then (* Arith. and Logical Operations *)
175           mk_instr_spec (entry_l,exit_l) (dest,src)
176        else (* Application *)
177           raise Fail "unimplemented SAL code generation for function applications"
178      end
179    else
180       raise Fail "unimplemented for this structure!"
181
182and
183
184(*  Code generation (by producing specifications)       *)
185
186gen_code (entry_l, t, exit_l) (input,output) =
187   if is_atomic t orelse is_pair t then
188       if t = output then    (* no copying is required *)
189            {entry = entry_l, exit = exit_l, body = inst [alpha |-> !VarType] nop, exp = t, dst = t,
190             thm = dummy_rule}
191       else mk_instr_spec (entry_l,exit_l) (output, t)
192
193   else if is_let t then                     (*  exp = LET (\v. N) M  *)
194     let
195         val (v,M,N) = dest_plet t
196         val new_l = next_label()
197         val spec1 = mk_spec (entry_l,new_l) (v,M) input
198         val spec2 = gen_code (new_l, N, exit_l) (#dst spec1, output)
199         val spec3 = if #body spec2 = (inst [alpha |-> !VarType] nop) then
200                         mk_spec (entry_l,exit_l) (v,M) input       (* make sure the exit label is correct *)
201                     else mk_union_spec spec1 spec2
202     in
203         spec3
204     end
205
206   else
207     {entry = entry_l, exit = exit_l, body = t, thm = mk_thm ([],``T``), exp = t, dst = t}
208  ;
209
210(* --------------------------------------------------------------------*)
211(* Fromat SAL programs for printing.                                   *)
212(* --------------------------------------------------------------------*)
213
214val seperator = ref ("\n")   (* " \n " *)
215val indent = "      "
216
217fun format_label l =
218  "l" ^ (term_to_string (#2 (dest_comb l))) handle _ => term_to_string l
219
220fun indent_label l =
221  let val label = format_label(l)
222  in case (size (label)) of
223      2 => label ^ ":   " |
224      3 => label ^ ":  "  |
225      4 => label ^ ": "   |
226      _ => label ^ ":"
227  end
228
229(* Turn a piece of SAL code into a string *)
230
231fun formatSAL code =
232  if is_const code andalso #1 (dest_const code) = "NOP" then ""
233  else if is_atomic code orelse is_pair code then term_to_string code
234  else if is_comb code then
235    let val (operator, xs) = strip_comb code
236        val op_s = #1 (dest_const operator)
237    in
238       if op_s = "UNION" then
239         formatSAL (hd xs) ^ formatSAL (hd (tl xs))
240       else if op_s = "ASG" then
241         let val [entry_l, dest, src, exit_l] = xs
242         in indent_label entry_l ^ term_to_string dest ^ " := " ^ term_to_string src ^
243            "  (goto " ^ format_label exit_l ^ ")" ^ !seperator
244         end
245       else if op_s = "IFGOTO" then
246         let val [entry_l, cond, true_l, false_l] = xs
247         in indent_label entry_l ^ "ifgoto " ^
248             term_to_string (#2 (dest_pabs cond)) ^ " " ^ format_label true_l ^
249              " " ^ format_label false_l ^ !seperator
250         end
251       else if op_s = "GOTO" then
252         let val [entry_l, exit_l] = xs
253         in indent ^ "goto " ^ format_label exit_l ^ !seperator
254         end
255       else
256         term_to_string code
257     end
258  else
259    term_to_string code
260
261(* --------------------------------------------------------------------*)
262(* Pre-processing before code generation                               *)
263(* --------------------------------------------------------------------*)
264
265(* Find the output of an expression      *)
266
267fun find_output t =
268    if is_let t then
269        let val (v,M,N) = dest_plet t
270        in if is_atomic N orelse is_pair N then SOME N
271           else find_output N
272        end
273    else if is_cond t then NONE
274    else if is_pabs t then
275        find_output (#2 (dest_pabs t))
276    else NONE
277
278(* Identify the argument, body and the output of a function *)
279
280fun pre_process def =
281  let
282    val (fname, fbody) = dest_eq (concl (SPEC_ALL def))
283    val fname = if is_comb fname then #1 (dest_comb fname) else fname
284    val (args,body) = dest_pabs fbody handle _ => (#2 (dest_comb fname), fbody)
285
286    val (body, output) =
287      case find_output(body) of
288        SOME x => (body, x) |
289        NONE => (mk_plet(args, body, args), args)
290  in
291    {body = body, input = args, output = output}
292  end
293
294(* --------------------------------------------------------------------*)
295(* Certifing Code Generation                                           *)
296(* --------------------------------------------------------------------*)
297
298val printSAL = print o formatSAL;
299
300fun certified_gen def =
301  let
302    val rs = pre_process def
303    val (sane,var_type) = pre_check(#input rs, #body rs)
304  in
305    if sane then
306      let val _ = (reset_label(); VarType := var_type)
307          val s = gen_code (next_label(), #body rs, next_label()) (#input rs, #output rs)
308      in
309          {code = #body s, thm = #thm s}
310      end
311      handle _ =>
312       ( print("STOP: The source program (FIL) includes structures whose conversion hasn't been implemented!\n");
313         {code = nop, thm = mk_thm ([], Term`T`)}
314       )
315    else
316      ( print("STOP: The source program (FIL) is invalid! (e.g. all variables are not of the same type)\n");
317        {code = nop, thm = mk_thm ([], Term`T`)}
318      )
319  end
320
321(* --------------------------------------------------------------------*)
322
323end (* struct *)
324