Changeset 1223


Ignore:
Timestamp:
Sep 16, 2011, 5:15:35 PM (8 years ago)
Author:
mulligan
Message:

changes

Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1221 r1223  
    2525  mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …).
    2626
    27 (*
    2827definition ertl_internal_function ≝
    29  λglobals. joint_internal_function globals … (ertl_sem_params_ globals).
    30 *)
     28  λglobals. joint_internal_function globals … (ertl_sem_params_ globals).
    3129
    3230definition ertl_program ≝ λglobals. joint_program globals … (ertl_sem_params_ globals).
  • src/ERTL/build.ma

    r1187 r1223  
    22include "utilities/Interference.ma".
    33
     4axiom graph : Type[0].
     5axiom create: ∀globals: list ident. ertl_internal_function globals → graph.
     6
     7record build_properties: Type[1] ≝
     8{
     9  lookup: graph → register → vertex
     10}.
     11
     12(*
    413definition build ≝
    514  λglobals: list ident.
     
    5968    〈liveafter, graph〉.
    6069  [*: @lattice_bottom ] (* XXX: matita bug here! *)
    61 qed.
     70qed. *)
  • src/ERTL/liveness.ma

    r1185 r1223  
    11include "ASM/Util.ma".
    22include "ERTL/ERTL.ma".
    3 
    4 definition list_set_union ≝
    5   λA: Type[0].
    6   λeq_a: A → A → bool.
    7   λl: list A.
    8   λr: list A.
    9     nub_by A eq_a (l @ r).
    10 
    11 definition list_set_add ≝
    12   λA: Type[0].
    13   λeq_a: A → A → bool.
    14   λa: A.
    15   λs: list A.
    16     nub_by A eq_a (a :: s).
    17 
    18 definition list_set_diff ≝
    19   λA: Type[0].
    20   λeq_a: A → A → bool.
    21   λl: list A.
    22   λr: list A.
    23     filter A (λx. member A eq_a x r) l.
    24 
    25 definition list_set_equal ≝
    26   λA: Type[0].
    27   λeq_a: A → A → bool.
    28   λl: list A.
    29   λr: list A.
    30     foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
    31 
    32 definition list_set_member ≝ member.
    33 
    34 definition list_set_fold ≝ foldr.
     3include "utilities/adt/set_adt.ma".
    354
    365definition statement_successors ≝
     
    4110    match seq with
    4211    [ joint_instr_cond acc_a_reg lbl_true ⇒
    43         list_set_add ? (eq_identifier ?) lbl_true [ l ]
    44     | _ ⇒ [ l ]
     12        set_insert … lbl_true (set_singleton … l)
     13    | _ ⇒ set_singleton … l
    4514    ]
    4615  | joint_st_extension ext ⇒
    4716    match ext with
    48     [ ertl_st_ext_new_frame l ⇒ [ l ]
    49     | ertl_st_ext_del_frame l ⇒ [ l ]
    50     | ertl_st_ext_frame_size r l ⇒ [ l ]
    51     ]
    52   | joint_st_goto l ⇒ [ l ]
    53   | joint_st_return ⇒ [ ]
    54   ].
    55 
    56 definition register_lattice ≝ (list register) × (list Register).
     17    [ ertl_st_ext_new_frame l ⇒ set_singleton … l
     18    | ertl_st_ext_del_frame l ⇒ set_singleton … l
     19    | ertl_st_ext_frame_size r l ⇒ set_singleton … l
     20    ]
     21  | joint_st_goto l ⇒ set_singleton … l
     22  | joint_st_return ⇒ set_empty …
     23  ].
     24
     25definition register_lattice ≝ (set register) × (set Register).
    5726definition lattice_property ≝ register_lattice.
    58 definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
     27definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
    5928definition lattice_psingleton: register → register_lattice ≝
    6029  λr.
    61     〈[ r ], [ ]〉.
     30    〈set_singleton … r, set_empty …〉.
    6231definition lattice_hsingleton: Register → register_lattice ≝
    6332  λr.
    64     〈[ ], [ r ]〉.
     33    〈set_empty …, set_singleton … r〉.
    6534
    6635definition lattice_join: register_lattice → register_lattice → register_lattice ≝
     
    6938  let 〈lp, lh〉 ≝ left in
    7039  let 〈rp, rh〉 ≝ right in
    71     〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.
     40    〈set_union … lp rp, set_union … lh rh〉.
    7241
    7342definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
     
    7645  let 〈lp, lh〉 ≝ left in
    7746  let 〈rp, rh〉 ≝ right in
    78     〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.
     47    〈set_diff … lp rp, set_diff … lh rh〉.
    7948
    8049definition lattice_equal: register_lattice → register_lattice → bool ≝
     
    8352  let 〈lp, lh〉 ≝ left in
    8453  let 〈rp, rh〉 ≝ right in
    85     andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).
     54    andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).
    8655
    8756definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
     
    10271definition property ≝
    10372  mk_lattice_property_sig
    104     ((list register) × (list Register))
     73    ((set register) × (set Register))
    10574    lattice_property
    10675    lattice_bottom
     
    134103    | joint_instr_load r _ _ ⇒ lattice_psingleton r
    135104    (* Potentially destroys all caller-save hardware registers. *)
    136     | joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉
     105    | joint_instr_call_id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    137106    | joint_instr_comment c ⇒ lattice_bottom
    138107    | joint_instr_cond r lbl_true ⇒ lattice_bottom
     
    158127  ].
    159128
    160 definition list_set_of_list ≝
    161   λrl.
    162     foldr ? ? (list_set_add Register eq_Register) rl [ ].
    163 
    164 definition list_set_of_list2 ≝
    165   let f ≝ λset. λr. list_set_add Register eq_Register r set in
    166     foldl ? ? f [ ].
    167 
    168 definition ret_regs ≝ list_set_of_list RegisterRets.
     129definition ret_regs ≝ set_from_list … RegisterRets.
    169130
    170131definition used ≝
     
    190151    | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    191152    (* Reads the hardware registers that are used to pass parameters. *)
    192     | joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉
     153    | joint_instr_call_id _ nparams ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    193154    | joint_instr_comment c ⇒ lattice_bottom
    194155    | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
     
    205166      ]
    206167    ]
    207   | joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     168  | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    208169  | joint_st_goto l ⇒ lattice_bottom
    209170  | joint_st_extension ext ⇒
     
    224185    match seq with
    225186    [ joint_instr_op2 op2 acc_a r ⇒
    226       if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
    227          list_set_member Register eq_Register RegisterCarry hliveafter then
     187      if set_member … (eq_identifier …) acc_a pliveafter ∨
     188         set_member … eq_Register RegisterCarry hliveafter then
    228189        None ?
    229190      else
     
    232193    | joint_instr_set_carry ⇒ None ?
    233194    | joint_instr_opaccs opaccs r1 r2 ⇒
    234       if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    235          list_set_member register (eq_identifier ?) r2 pliveafter ∨
    236          list_set_member Register eq_Register RegisterCarry hliveafter then
     195      if set_member … (eq_identifier …) r1 pliveafter ∨
     196         set_member … (eq_identifier …) r2 pliveafter ∨
     197         set_member … eq_Register RegisterCarry hliveafter then
    237198        None ?
    238199      else
    239200        Some ? l
    240201    | joint_instr_op1 op1 r ⇒
    241       if list_set_member register (eq_identifier ?) r pliveafter ∨
    242          list_set_member Register eq_Register RegisterCarry hliveafter then
     202      if set_member … (eq_identifier …) r pliveafter ∨
     203         set_member … eq_Register RegisterCarry hliveafter then
    243204        None ?
    244205      else
     
    246207    | joint_instr_pop r ⇒ None ?
    247208    | joint_instr_int r _ ⇒
    248       if list_set_member register (eq_identifier ?) r pliveafter ∨
    249          list_set_member Register eq_Register RegisterCarry hliveafter then
     209      if set_member … (eq_identifier …) r pliveafter ∨
     210         set_member … eq_Register RegisterCarry hliveafter then
    250211        None ?
    251212      else
    252213        Some ? l
    253214    | joint_instr_address _ _ r1 r2 ⇒
    254       if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    255          list_set_member register (eq_identifier ?) r2 pliveafter ∨
    256          list_set_member Register eq_Register RegisterCarry hliveafter then
     215      if set_member … (eq_identifier …) r1 pliveafter ∨
     216         set_member … (eq_identifier …) r2 pliveafter ∨
     217         set_member … eq_Register RegisterCarry hliveafter then
    257218        None ?
    258219      else
    259220        Some ? l
    260221    | joint_instr_load acc_a dpl dph ⇒
    261       if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
    262          list_set_member Register eq_Register RegisterCarry hliveafter then
     222      if set_member ? (eq_identifier …) acc_a pliveafter ∨
     223         set_member … eq_Register RegisterCarry hliveafter then
    263224        None ?
    264225      else
     
    275236      match r1 with
    276237      [ pseudo p1 ⇒
    277         if list_set_member register (eq_identifier ?) p1 pliveafter ∨
    278            list_set_member Register eq_Register RegisterCarry hliveafter then
     238        if set_member … (eq_identifier …) p1 pliveafter ∨
     239           set_member … eq_Register RegisterCarry hliveafter then
    279240          None ?
    280241        else
    281242          Some ? l
    282243      | hardware h1 ⇒
    283         if list_set_member Register eq_Register h1 hliveafter then
     244        if set_member … eq_Register h1 hliveafter then
    284245          None ?
    285246        else
     
    294255    | ertl_st_ext_del_frame l ⇒ None ?
    295256    | ertl_st_ext_frame_size r l ⇒
    296       if list_set_member register (eq_identifier ?) r pliveafter ∨
    297         list_set_member Register eq_Register RegisterCarry hliveafter then
     257      if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
     258         set_member ? eq_Register RegisterCarry hliveafter then
    298259        None ?
    299260      else
     
    319280definition livebefore ≝
    320281  λglobals: list ident.
    321   λint_fun.
     282  λint_fun: ertl_internal_function globals.
    322283  λlabel.
    323284  λliveafter: valuation.
    324   match lookup ? ? (ertl_if_graph globals int_fun) label with
     285  match lookup ? ? (joint_if_graph … int_fun) label with
    325286  [ None      ⇒ ?
    326287  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
     
    330291
    331292definition liveafter ≝
    332   λglobals.
    333   λint_fun.
    334   λlivebefore.
     293  λglobals: list ident.
     294  λint_fun: ertl_internal_function globals.
     295  λlivebefore: label → ?.
    335296  λlabel.
    336297  λliveafter: valuation.
    337   match lookup … (ertl_if_graph globals int_fun) label with
     298  match lookup … (joint_if_graph … int_fun) label with
    338299  [ None      ⇒ ?
    339   | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice.
     300  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
    340301      lattice_join (livebefore successor liveafter) accu)
    341       lattice_bottom (statement_successors globals stmt)
     302      (statement_successors globals stmt) lattice_bottom
    342303  ].
    343304  cases not_implemented (* XXX *)
  • src/utilities/Interference.ma

    r1219 r1223  
    22include "basics/list.ma".
    33include "common/Graphs.ma".
     4include "common/Order.ma".
    45include "common/Registers.ma".
    56
     
    1011include "utilities/adt/register_table.ma".
    1112
    12 definition vertex_set ≝ set vertex.
     13(* definition vertex_set ≝ set vertex. *)
    1314definition vertex_priority_set ≝ priority_set vertex.
    1415definition vertex_set_table ≝ set_table vertex (set vertex).
     
    1819record graph: Type[0] ≝
    1920{
    20   ig_regmap     : register_table;
    21   ig_ivv        : vertex_set_table;
    22   ig_ivh        : Register_set_table;
    23   ig_pvv        : vertex_set;
    24   ig_pvh        : Register_set;
    25   ig_degree     : vertex_priority_set;
    26   ig_nmr        : vertex_priority_set
     21  g_regmap     : register_table;
     22  g_ivv        : vertex_set_table;
     23  g_ivh        : Register_set_table;
     24  g_pvv        : vertex_set_table;
     25  g_pvh        : Register_set_table;
     26  g_degree     : vertex_priority_set;
     27  g_nmr        : vertex_priority_set
    2728}.
    2829
     
    3031  λgraph.
    3132  λivv: vertex_set_table.
    32     let regmap ≝ ig_regmap graph in
    33     let ivh    ≝ ig_ivh graph in
    34     let pvv    ≝ ig_pvv graph in
    35     let pvh    ≝ ig_pvh graph in
    36     let degree ≝ ig_degree graph in
    37     let nmr    ≝ ig_nmr graph in
     33    let regmap ≝ g_regmap graph in
     34    let ivh    ≝ g_ivh graph in
     35    let pvv    ≝ g_pvv graph in
     36    let pvh    ≝ g_pvh graph in
     37    let degree ≝ g_degree graph in
     38    let nmr    ≝ g_nmr graph in
    3839      mk_graph
    3940        regmap ivv ivh pvv pvh degree nmr.
     
    4243  λgraph.
    4344  λivh: Register_set_table.
    44     let regmap ≝ ig_regmap graph in
    45     let ivv    ≝ ig_ivv graph in
    46     let pvv    ≝ ig_pvv graph in
    47     let pvh    ≝ ig_pvh graph in
    48     let degree ≝ ig_degree graph in
    49     let nmr    ≝ ig_nmr graph in
     45    let regmap ≝ g_regmap graph in
     46    let ivv    ≝ g_ivv graph in
     47    let pvv    ≝ g_pvv graph in
     48    let pvh    ≝ g_pvh graph in
     49    let degree ≝ g_degree graph in
     50    let nmr    ≝ g_nmr graph in
    5051      mk_graph
    5152        regmap ivv ivh pvv pvh degree nmr.
     
    5455  λgraph.
    5556  λdegree: vertex_priority_set.
    56     let regmap ≝ ig_regmap graph in
    57     let ivv    ≝ ig_ivv graph in
    58     let ivh    ≝ ig_ivh graph in
    59     let pvv    ≝ ig_pvv graph in
    60     let pvh    ≝ ig_pvh graph in
    61     let nmr    ≝ ig_nmr graph in
     57    let regmap ≝ g_regmap graph in
     58    let ivv    ≝ g_ivv graph in
     59    let ivh    ≝ g_ivh graph in
     60    let pvv    ≝ g_pvv graph in
     61    let pvh    ≝ g_pvh graph in
     62    let nmr    ≝ g_nmr graph in
    6263      mk_graph
    6364        regmap ivv ivh pvv pvh degree nmr.
     
    6667  λgraph.
    6768  λnmr: vertex_priority_set.
    68     let regmap ≝ ig_regmap graph in
    69     let ivv    ≝ ig_ivv graph in
    70     let ivh    ≝ ig_ivh graph in
    71     let pvv    ≝ ig_pvv graph in
    72     let pvh    ≝ ig_pvh graph in
    73     let degree ≝ ig_degree graph in
     69    let regmap ≝ g_regmap graph in
     70    let ivv    ≝ g_ivv graph in
     71    let ivh    ≝ g_ivh graph in
     72    let pvv    ≝ g_pvv graph in
     73    let pvh    ≝ g_pvh graph in
     74    let degree ≝ g_degree graph in
    7475      mk_graph
    7576        regmap ivv ivh pvv pvh degree nmr.
     
    7879  λgraph: graph.
    7980  λv: vertex.
    80     set_tbl_find … v (ig_ivv graph).
     81    set_tbl_find … v (g_ivv graph).
    8182
    8283definition sg_existsvv ≝
     
    8687  match sg_neighboursv graph v2 with
    8788  [ None       ⇒ false (* XXX: ok? *)
    88   | Some neigh ⇒ set_member ? v1 neigh
     89  | Some neigh ⇒ set_member ? eq_nat v1 neigh
    8990  ].
    9091
     
    9293  λgraph.
    9394  λv.
    94     set_tbl_find ? ? v (ig_ivh graph).
     95    set_tbl_find ? ? v (g_ivh graph).
    9596
    9697definition sg_existsvh ≝
     
    100101  match sg_neighboursh graph v with
    101102  [ None       ⇒ false (* XXX: ok? *)
    102   | Some neigh ⇒ set_member ? h neigh
     103  | Some neigh ⇒ set_member ? eq_Register h neigh
    103104  ].
    104105
     
    118119  λgraph: graph.
    119120    let union ≝ λkey: vertex. set_union ? in
    120     set_tbl_fold vertex ? ? union (ig_ivh graph) (set_empty Register).
     121    set_tbl_fold vertex ? ? union (g_ivh graph) (set_empty Register).
    121122
    122123axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)
     
    126127  λv1.
    127128  λv2.
    128     set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (ig_ivv graph)).
     129    set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (g_ivv graph)).
    129130
    130131definition sg_mkvv ≝
     
    143144  λv1.
    144145  λv2.
    145     set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (ig_ivv graph)).
     146    set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (g_ivv graph)).
    146147
    147148definition sg_rmvvifx ≝
     
    158159  λv.
    159160  λh.
    160     set_ivh graph (set_tbl_update … v (set_insert … h) (ig_ivh graph)).
     161    set_ivh graph (set_tbl_update … v (set_insert … h) (g_ivh graph)).
    161162
    162163definition sg_mkvh ≝
     
    173174  λv.
    174175  λh.
    175     set_ivh graph (set_tbl_update … v (set_remove … h) (ig_ivh graph)).
     176    set_ivh graph (set_tbl_update … v (set_remove … h) (g_ivh graph)).
    176177
    177178definition sg_rmvhifx ≝
     
    250251  let graph ≝ sg_mkvvi graph v1 v2 in
    251252  let graph ≝ sg_rmvvifx graph v1 v2 in
    252   let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (ig_degree graph)) in
    253   let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (ig_nmr graph)) in
     253  let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (g_degree graph)) in
     254  let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (g_nmr graph)) in
    254255    set_degree (set_nmr graph nmr') degree'.
    255256
     
    259260  λv2.
    260261  let graph ≝ sg_rmvv graph v1 v2 in
    261   let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (ig_degree graph)) in
    262   let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (ig_nmr graph)) in
     262  let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (g_degree graph)) in
     263  let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (g_nmr graph)) in
    263264    set_degree (set_nmr graph nmr') degree'.
    264265
     
    269270  let graph ≝ sg_mkvhi graph v h in
    270271  let graph ≝ sg_rmvhifx graph v h in
    271   let degree ≝ pset_increment ? v (repr 1) (ig_degree graph) in
    272   let nmr ≝ pset_incrementifx ? v (repr 1) (ig_nmr graph) in
     272  let degree ≝ pset_increment ? v (repr 1) (g_degree graph) in
     273  let nmr ≝ pset_incrementifx ? v (repr 1) (g_nmr graph) in
    273274    set_degree (set_nmr graph nmr) degree.
    274275
     
    278279  λh.
    279280  let graph ≝ sg_rmvh graph v h in
    280   let degree ≝ pset_increment ? v (neg (repr 1)) (ig_degree graph) in
    281   let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (ig_nmr graph) in
     281  let degree ≝ pset_increment ? v (neg (repr 1)) (g_degree graph) in
     282  let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (g_nmr graph) in
    282283    set_degree (set_nmr graph nmr) degree.
    283284
     
    299300  λv.
    300301    if pref_nmr graph v then
    301       let nmr' ≝ pset_remove ? v (ig_nmr graph) in
     302      let nmr' ≝ pset_remove ? v (g_nmr graph) in
    302303        set_nmr graph nmr'
    303304    else
     
    330331  λv.
    331332  if pref_nmr graph v then
    332     match pset_lookup ? v (ig_degree graph) with
     333    match pset_lookup ? v (g_degree graph) with
    333334    [ None ⇒ graph (* XXX: ok? *)
    334335    | Some pref ⇒
    335       let nmr ≝ pset_insert ? v pref (ig_nmr graph) in
     336      let nmr ≝ pset_insert ? v pref (g_nmr graph) in
    336337        set_nmr graph nmr
    337338    ]
     
    355356  let graph ≝ pref_rmcheck graph v in
    356357    graph.
     358   
     359definition ig_ipp ≝ sg_neighboursv.
     360definition ig_iph ≝ sg_neighboursh.
     361definition ig_ppp ≝ sg_neighboursv.
     362definition ig_pph ≝ sg_neighboursh.
     363definition ig_degree ≝ λgraph. λv. pset_lookup ? v (g_degree graph).
     364definition ig_lowest ≝ λgraph. pset_lowest ? (g_degree graph).
     365definition ig_lowest_non_move_related ≝ λgraph. pset_lowest ? (g_nmr graph).
     366definition ig_fold ≝ λA: Type[0]. λf: vertex → A → A. λgraph. λaccu.
     367  rt_fold … (λv. λ_. λaccu. f v accu) (g_regmap graph) accu.
     368
     369definition ig_minimum: ∀a: Type[0]. (a → a → order) → (vertex → a) → graph → option vertex ≝
     370  λa: Type[0].
     371  λcompare: a → a → order.
     372  λf: vertex → a.
     373  λgraph.
     374  let folded ≝ ig_fold … (λw. λaccu.
     375    let dw ≝ f w in
     376      match accu with
     377      [ None      ⇒ Some … 〈dw, w〉
     378      | Some dv_v ⇒
     379        let 〈dv, v〉 ≝ dv_v in
     380          match compare dw dv with
     381          [ order_lt ⇒ Some … 〈dw, w〉
     382          | _        ⇒ accu
     383          ]
     384      ]) graph (None …)
     385  in
     386    match folded with
     387    [ None          ⇒ None …
     388    | Some ignore_v ⇒
     389      let 〈ignore, v〉 ≝ ignore_v in
     390        Some … v
     391    ].
     392   
     393definition ig_ppedge ≝ vertex × vertex.
     394
     395definition ig_pppick ≝ λgraph. λp. set_tbl_pick … (g_pvv graph) p.
     396
     397definition ig_phedge ≝ vertex × Register.
     398
     399definition ig_phpick ≝ λgraph. λp. set_tbl_pick … (g_pvh graph) p.
    357400
    358401definition ig_create ≝
     
    365408        〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs
    366409  in
    367       mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_empty …)
    368       (set_empty …) priority'' priority''.
    369 
    370 
    371 
     410      mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_tbl_empty …)
     411      (set_tbl_empty …) priority'' priority''.
     412definition ig_lookup ≝ λgraph. λr. rt_backward r (g_regmap graph).
     413definition ig_registers ≝ λgraph. λv. rt_forward v (g_regmap graph).
    372414definition ig_mkipp ≝
    373   λset_impl.
    374   λgraph: interference_graph set_impl.
     415  λgraph.
    375416  λregs1.
    376417  λregs2.
    377     set_fold … (ig_Reg_set … graph) (λr1. λgraph.
    378       let v1 ≝ lookup … graph r1 in
    379         set_fold … (ig_Reg_set … graph) (λr2. λgraph.
    380           ig_mkvv …
    381 
    382 let mkipp graph regs1 regs2 =
    383   Register.Set.fold (fun r1 graph ->
    384     let v1 = lookup graph r1 in
    385     Register.Set.fold (fun r2 graph ->
    386       interference#mkvv graph v1 (lookup graph r2)
    387     ) regs2 graph
    388   ) regs1 graph
    389 
    390 axiom ig_mkiph: graph → list register → list Register →
    391   graph.
    392 
    393 definition ig_mki: graph → (list register) × (list Register) →
    394   (list register) × (list Register) → graph ≝
     418    set_fold … (λr1. λgraph.
     419      let v1 ≝ ig_lookup graph r1 in
     420        set_fold … (λr2. λgraph.
     421          sg_mkvv graph v1 (ig_lookup graph r2)
     422        ) regs2 graph
     423    ) regs1 graph.
     424definition ig_mkiph ≝
     425  λgraph.
     426  λregs.
     427  λhwregs.
     428    set_fold … (λr. λgraph.
     429      let v ≝ ig_lookup graph r in
     430        set_fold … (λh. λgraph.
     431          sg_mkvh graph v h
     432        ) hwregs graph
     433    ) regs graph.
     434definition ig_mki ≝
    395435  λgraph.
    396436  λregs1_hwregs1.
    397437  λregs2_hwregs2.
    398     let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
    399     let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
    400     let graph ≝ ig_mkipp graph regs1 regs2 in
    401     let graph ≝ ig_mkiph graph regs1 hwregs2 in
    402     let graph ≝ ig_mkiph graph regs2 hwregs1 in
    403       graph.
     438  let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
     439  let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
     440  let graph ≝ ig_mkipp graph regs1 regs2 in
     441  let graph ≝ ig_mkiph graph regs1 hwregs2 in
     442  let graph ≝ ig_mkiph graph regs2 hwregs1 in
     443    graph.
     444definition ig_mkppp ≝
     445  λgraph.
     446  λr1.
     447  λr2.
     448  let v1 ≝ ig_lookup graph r1 in
     449  let v2 ≝ ig_lookup graph r2 in
     450  let graph ≝ sg_mkvv graph v1 v2 in
     451    graph.
     452definition ig_mkpph ≝
     453  λgraph.
     454  λr.
     455  λh.
     456  let v ≝ ig_lookup graph r in
     457  let graph ≝ sg_mkvh graph v h in
     458    graph.
     459(*   
     460(* XXX: precondition:
     461  x \not\eq y
     462  existsvv graph x y == false i.e. coalesce interfering edges *)
     463definition ig_coalesce ≝
     464  λgraph.
     465  λx.
     466  λy.
     467  let graph ≝ sg_coalesce graph x y in
     468
     469let coalesce graph x y =
     470
     471  assert (x <> y); (* attempt to coalesce one vertex with itself *)
     472  assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *)
     473
     474  (* Perform coalescing in the two subgraphs. *)
     475
     476  let graph = interference#coalesce graph x y in
     477  let graph = preference#coalesce graph x y in
     478
     479  (* Remove [x] from all tables. *)
     480
     481  {
     482    graph with
     483    regmap = RegMap.coalesce x y graph.regmap;
     484    ivh = Vertex.Map.remove x graph.ivh;
     485    pvh = Vertex.Map.remove x graph.pvh;
     486    degree = PrioritySet.remove x graph.degree;
     487    nmr = PrioritySet.remove x graph.nmr;
     488  }
    404489 
    405490axiom ig_mkppp: interference_graph → register → register → interference_graph.
     
    427512definition ig_phedge ≝ vertex × Register.
    428513axiom ig_phpick: interference_graph → (ig_phedge → bool) → option ig_phedge.
     514*)
  • src/utilities/adt/priority_set_adt.ma

    r1218 r1223  
    44include "common/Integers.ma".
    55
    6 include "utilities/adt/ordering.ma".
    76include "ASM/Util.ma".
    87
  • src/utilities/adt/register_table.ma

    r1211 r1223  
    11include "ASM/I8051.ma".
    22include "common/Registers.ma".
    3 include "utilities/adt/ordering.ma".
    43include "utilities/adt/set_adt.ma".
    54
    65definition vertex ≝ nat. (* XXX: int in o'caml *)
    76
     7(*
    88axiom Register_ordered: ordered Register.
    99axiom register_ordered: ordered register.
    1010axiom vertex_ordered: ordered vertex.
     11*)
    1112
    1213axiom register_table: Type[0].
    1314 
    1415axiom rt_empty : register_table.
     16
     17axiom rt_insert: vertex → set Register → register_table → register_table.
    1518 
    1619axiom rt_forward : vertex → register_table → set Register.
  • src/utilities/adt/set_adt.ma

    r1218 r1223  
    33include "arithmetics/nat.ma".
    44include "ASM/Util.ma".
    5 
    6 include "utilities/adt/ordering.ma".
    75
    86axiom set: Type[0] → Type[0].
     
    1311axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type.
    1412axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type.
    15 axiom set_member: ∀elt_type. elt_type → set elt_type → bool.
     13axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool.
    1614axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool.
    1715axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool.
    1816axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type.
    19 axiom set_equal: ∀elt_type. set elt_type → set elt_type → bool.
    2017axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a.
    2118axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type  → a → a.
     19axiom set_equal: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
     20  set elt_type → set elt_type → bool.
     21
     22(* XXX: define in terms of primitives *)
     23axiom set_diff: ∀elt_type: Type[0]. set elt_type → set elt_type → set elt_type.
    2224
    2325definition set_is_empty ≝
     
    4749definition set_subset ≝
    4850  λelt_type: Type[0].
     51  λeq      : elt_type → elt_type → bool.
    4952  λleft    : set elt_type.
    5053  λright   : set elt_type.
    51     set_forall elt_type (λelt. set_member elt_type elt right) left.
     54    set_forall elt_type (λelt. set_member elt_type eq elt right) left.
    5255
    5356definition set_subseteq ≝
    5457  λelt_type: Type[0].
     58  λeq      : elt_type → elt_type → bool.
    5559  λleft    : set elt_type.
    5660  λright   : set elt_type.
    57     set_equal elt_type left right ∧ (set_subset elt_type left right).
     61    set_equal elt_type eq left right ∧ (set_subset elt_type eq left right).
    5862
    5963definition set_union ≝
     
    6569definition set_intersection ≝
    6670  λelt_type: Type[0].
     71  λeq      : elt_type → elt_type → bool.
    6772  λleft    : set elt_type.
    6873  λright   : set elt_type.
    69     set_filter elt_type (λelt. set_member elt_type elt right) left.
     74    set_filter elt_type (λelt. set_member elt_type eq elt right) left.
  • src/utilities/adt/set_table_adt.ma

    r1218 r1223  
    33include "utilities/adt/set_adt.ma".
    44include "utilities/adt/table_adt.ma".
    5 include "utilities/adt/ordering.ma".
    65
    76axiom set_table: Type[0] → Type[0] → Type[0].
     
    2221                      → set_table key_type a -> b -> b.
    2322axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
    24                       (key_type → a → bool) → option (key_type × a).
     23                      ((key_type × a) → bool) → option (key_type × a).
    2524
    2625
  • src/utilities/adt/table_adt.ma

    r1218 r1223  
    55include "arithmetics/nat.ma".
    66
    7 include "utilities/adt/ordering.ma".
    87include "utilities/adt/equal.ma".
    98
Note: See TracChangeset for help on using the changeset viewer.