working/0.1/annotatedIR.sml

39       fun printtree(SC(s1,s2,info),d) =
40             (indent d; sayln "SC("; printtree(s1,d+2); sayln ","; printtree(s2,d+2); say ")")
41         | printtree(CJ((exp1,rop,exp2),s1,s2,info),d) =
43                        printtree(s1,d+2); sayln ","; printtree(s2,d+2); say ")")
328        fun is_ir_equal (SC(s1,s2,_)) (SC(s3,s4,_)) =
329              is_ir_equal s1 s3 andalso is_ir_equal s2 s4
332         |  is_ir_equal (CJ(cond1,s1,s2,_)) (CJ(cond2,s3,s4,_)) =
333              cond1 = cond2 andalso is_ir_equal s1 s3 andalso is_ir_equal s2 s4
334         |  is_ir_equal (BLK(s1,_)) (BLK(s2,_)) =
335              List.all (op =) (zip s1 s2)
336         |  is_ir_equal (STM s1) (STM s2) =
337              List.all (op =) (zip s1 s2)
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)) =
351              merge_stm s2
354         |  merge_stm (SC(BLK([],_), s2, info)) =
355              merge_stm s2
358         |  merge_stm (SC(s1,s2,info)) =
359              SC (merge_stm s1, merge_stm s2, info)
362         |  merge_stm (CJ(cond, s1, s2, info)) =
363              CJ(cond, merge_stm s1, merge_stm s2, info)
383     |  get_annt (SC(s1,s2,info)) = info
384     |  get_annt (CJ(cond,s1,s2,info)) = 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)
447                 |  (SC (s1,s2,info)) =>
448                        SC (adjust_ins s1 outer_info, s2, outer_info)
449                 |  (CJ (cond,s1,s2,info)) =>
450                        CJ (cond, adjust_ins s1 outer_info, adjust_ins s2 outer_info, outer_info)
478     |  back_trace (SC(s1,s2,inner_info)) (outer_info as {outs = outer_outs, context = contextL, ...}) =
480               val s2' = back_trace s2 outer_info
481               val (s1_info, s2_info) = (get_annt s1, get_annt s2');
482               val s2'' = if S.isSubset (pair2set (#ins s2_info), pair2set (#outs s1_info))
483                          then adjust_ins s2' (replace_ins s2_info (#outs s1_info))
484                          else s2';
485               val s2_info = get_annt s2'';
489               SC(s1',s2'', {ins = #ins s1_info, outs = #outs s2_info, fspec = thm_t, context = contextL})
492     |  back_trace (CJ(cond, s1, s2, inner_info)) (outer_info as {outs = outer_outs, context = contextL, ...}) =
500               val s2' = back_trace s2 outer_info
501               val ({ins = ins1, outs = outs1, ...}, {ins = ins2, outs = outs2, ...}) = (get_annt s1', get_annt s2');
503                       (* union of the variables in the condition and the inputs of the s1' and s2' *)
506               CJ(cond, adjust_ins s1' info_0, adjust_ins s2' info_0, info_0)
550   fun match_ins_outs (SC(s1,s2,info)) =
552           val (ir1,ir2) = (match_ins_outs s1, match_ins_outs s2);