Changeset 1211


Ignore:
Timestamp:
Sep 14, 2011, 4:14:59 PM (8 years ago)
Author:
mulligan
Message:

fixed interference file

Location:
src/utilities
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Interference.ma

    r1210 r1211  
    99include "utilities/adt/register_table.ma".
    1010
    11 definition vertex_set ≝ set_adt vertex vertex_ordered.
    12 definition vertex_priority_set ≝ priority_set_adt vertex vertex_ordered.
    13 definition Register_set ≝ set_adt Register Register_ordered.
     11definition vertex_set ≝ set vertex.
     12definition vertex_priority_set ≝ priority_set vertex.
     13definition Register_set ≝ set Register.
    1414
    15 record graph
    16   (set_impl: set_adt … Register Register_ordered): Type[1] ≝
     15record graph: Type[1] ≝
    1716{
    18   ig_reg_table  : register_table_adt set_impl;
    19   ig_vertex_set : vertex_set;
    20   ig_vertex_pset: vertex_priority_set;
    21   ig_Reg_set    : Register_set;
    22   ig_regmap     : register_table set_impl ig_reg_table;
    23   ig_ivv        : set … ig_vertex_set vertex;
    24   ig_ivh        : set … ig_Reg_set Register;
    25   ig_pvv        : set … ig_vertex_set vertex;
    26   ig_pvh        : set … ig_Reg_set Register;
    27   ig_degree     : priority_set … ig_vertex_pset vertex;
    28   ig_nmr        : priority_set … ig_vertex_pset vertex
     17  ig_regmap     : register_table;
     18  ig_ivv        : vertex_set;
     19  ig_ivh        : Register_set;
     20  ig_pvv        : vertex_set;
     21  ig_pvh        : Register_set;
     22  ig_degree     : vertex_priority_set;
     23  ig_nmr        : vertex_priority_set
    2924}.
    3025
    3126definition ig_create ≝
    32   λReg_set_impl: set_adt … Register Register_ordered.
    33   λvertex_set_impl: set_adt … vertex vertex_ordered.
    34   λvertex_priority_set_impl: priority_set_adt … vertex vertex_ordered.
    35   λReg_table_impl: register_table_adt Reg_set_impl.
    3627  λregs.
    3728  let 〈ignore_int, table'', priority''〉 ≝
    3829    foldr … (λr. λv_table_priority'.
    3930      let 〈v, table', priority'〉 ≝ v_table_priority' in
    40       let table'' ≝ rt_add ? Reg_table_impl r v table' in
    41       let priority'' ≝ ps_insert ? ? vertex_priority_set_impl v 0 priority' in
     31      let table'' ≝ rt_add r v table' in
     32      let priority'' ≝ ps_insert ? v 0 priority' in
    4233        〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs
    4334  in
    44       mk_graph Reg_set_impl
    45       Reg_table_impl vertex_set_impl vertex_priority_set_impl
    46       Reg_set_impl table'' (set_empty …) (set_empty …) (set_empty …)
     35      mk_graph table'' (set_empty …) (set_empty …) (set_empty …)
    4736      (set_empty …) priority'' priority''.
    4837
  • src/utilities/adt/register_table.ma

    r1210 r1211  
    2020axiom rt_remove: vertex → register_table → register_table.
    2121
    22 axiom rt_fold: ∀a: Type[0]. (vertex → set … set_impl Register → a → a) →
    23    register_table → a → a;
     22axiom rt_fold: ∀a: Type[0]. (vertex → set Register → a → a) →
     23   register_table → a → a.
    2424
    2525axiom rt_coalesce: vertex → vertex → register_table → register_table.
Note: See TracChangeset for help on using the changeset viewer.