working/0.1/annotatedIR.sml

39       fun printtree(SC(s1,s2,info),d) =
41         | printtree(CJ((exp1,rop,exp2),s1,s2,info),d) =
44         | printtree(TR((exp1,rop,exp2),s,info),d) =
47         | printtree(CALL(fname,pre,body,post,info),d) =
51                 let val ir' = SC (pre, SC (body, post, info), info)
61         | printtree(BLK(stmL, info),d) =
272                 val info = {fspec = DECIDE(Term`T`), ins = ins, outs = ins, context = []}
273                 val r_ir_1 = SC(r_ir,rec_args_pass_ir, info)
279                                         b_ir, info)
309    fun rm_dummy_inst (SC(ir1,ir2,info)) =
310          SC (rm_dummy_inst ir1, rm_dummy_inst ir2, info)
311     |  rm_dummy_inst (TR(cond,ir2,info)) =
312          TR(cond, rm_dummy_inst ir2, info)
313     |  rm_dummy_inst (CJ(cond,ir1,ir2,info)) =
314          CJ(cond, rm_dummy_inst ir1, rm_dummy_inst ir2, info)
317     | rm_dummy_inst (CALL (fname,pre,body,post,info)) =
318          CALL (fname, rm_dummy_inst pre, rm_dummy_inst body, rm_dummy_inst post, info)
319     | rm_dummy_inst (BLK (instL, info)) =
320          BLK (List.filter (not o is_dummy_inst) instL,info)
342        fun merge_stm (SC(STM s1, STM s2, info)) =
343              BLK (s1 @ s2, info)
344         |  merge_stm (SC(STM s1, BLK(s2,_), info)) =
345              BLK (s1 @ s2, info)
346         |  merge_stm (SC(BLK(s1,_), STM s2, info)) =
347              BLK (s1 @ s2, info)
348         |  merge_stm (SC(BLK(s1,_), BLK(s2,_), info)) =
349              BLK (s1 @ s2, info)
350         |  merge_stm (SC(STM [], s2, info)) =
352         |  merge_stm (SC(s1, STM [], info)) =
354         |  merge_stm (SC(BLK([],_), s2, info)) =
356         |  merge_stm (SC(s1, BLK([],_), info)) =
358         |  merge_stm (SC(s1,s2,info)) =
359              SC (merge_stm s1, merge_stm s2, info)
360         |  merge_stm (TR(cond, body, info)) =
361              TR(cond, merge_stm body, info)
362         |  merge_stm (CJ(cond, s1, s2, info)) =
363              CJ(cond, merge_stm s1, merge_stm s2, info)
382    fun get_annt (BLK (stmL,info)) = info
383     |  get_annt (SC(s1,s2,info)) = info
384     |  get_annt (CJ(cond,s1,s2,info)) = info
385     |  get_annt (TR(cond,s,info)) = info
386     |  get_annt (CALL(fname,pre,body,post,info)) = info
402    fun apply_to_info (BLK (stmL,info)) f =  BLK (stmL, f info)
403     |  apply_to_info (SC(s1,s2,info)) f = SC(s1, s2, f info)
404     |  apply_to_info (CJ(cond,s1,s2,info)) f = CJ(cond, s1, s2, f info)
405     |  apply_to_info (TR(cond,s,info)) f = TR(cond, s, f info)
406     |  apply_to_info (CALL(fname,pre,body,post,info)) f = CALL(fname, pre, body, post, f info)
417    fun get_modified_regs (SC(ir1,ir2,info)) =
419     |  get_modified_regs (TR(cond,ir,info)) =
421     |  get_modified_regs (CJ(cond,ir1,ir2,info)) =
423     |  get_modified_regs (CALL(fname,pre,body,post,info)) =
424          List.map (fn (REG r) => r | _ => ~1) (List.filter (fn (REG r) => true | _ => false) (pair2list (#outs info)))
427     |  get_modified_regs (BLK (l,info)) =
445                    (BLK (stmL, info)) =>
447                 |  (SC (s1,s2,info)) =>
449                 |  (CJ (cond,s1,s2,info)) =>
451                 |  (TR (cond,s,info)) =>
452                        TR(cond, adjust_ins s info, info)
453                 |  (CALL (fname,pre,body,post,info)) =>
454                        CALL(fname, pre, body, post, info)
475     |  back_trace (STM stmL) info =
476           back_trace (BLK (stmL,init_info)) info
509     |  back_trace (TR (cond, body, info)) (outer_info as {outs = outer_outs, context = contextL, ...}) =
511               val extra_outs = args_diff (PAIR (outer_outs, list2pair contextL), #outs info)
512               val info' = replace_context info (pair2list extra_outs);
513               val body' = adjust_ins body info'
515               TR(cond, body', info')
519     |  back_trace (CALL (fname, pre, body, post, info)) (outer_info as {outs = outer_outs, context = contextL, fspec = fout_spec, ...}) =
521               val extra_outs = args_diff (PAIR (outer_outs, list2pair contextL), #outs info)
523               CALL (fname, pre, BLK ([], info), post, replace_ins outer_info (#ins info))
541           val info =  {ins = ins, outs = outs, context = [], fspec = thm_t}
543           extract_outputs (back_trace ir info)
550   fun match_ins_outs (SC(s1,s2,info)) =
557               SC(ir1,ir2,info)
562                  info)
565    |  match_ins_outs (ir as (CALL (fname, pre, body, post, info))) =
567           val ((pre_ins,post_outs),(outer_ins,outer_outs)) = ((#ins (get_annt pre), #outs (get_annt post)), (#ins info, #outs info))
571                             BLK ([], {ins = post_outs, outs = outer_outs, context = #context info, fspec = thm_t}),
572                             replace_ins info pre_ins)
576               SC (BLK([], {ins = outer_ins, outs = pre_ins, context = #context info, fspec = thm_t}),
578                   info)