Changeset 1208


Ignore:
Timestamp:
Sep 13, 2011, 4:33:10 PM (8 years ago)
Author:
mulligan
Message:

added adts for sets, tables and priority sets in order to make life easier when working on the interference graph code

Location:
src/utilities
Files:
6 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Interference.ma

    r1196 r1208  
    33include "common/Graphs.ma".
    44include "common/Registers.ma".
    5 include "utilities/RegisterSet.ma".
     5
     6include "utilities/adt/table_adt.ma".
     7include "utilities/adt/priority_set_adt.ma".
     8include "utilities/adt/set_adt.ma".
    69
    710definition vertex ≝ nat. (* XXX: int in o'caml *)
     
    1720axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
    1821
    19 definition interference_graph ≝ graph label.
     22axiom ordered_vertex: ordered vertex.
     23axiom ordered_register: ordered register.
     24axiom ordered_Register: ordered Register.
    2025
    21 definition ig_create: ∀rs. rs_set rs → interference_graph ≝
    22   let 〈ignore_int, regmap, degree〉 ≝
    23     rs_fold rs (λr. λv_regmap_degree.
    24       let 〈v, regmap, degree〉 ≝ v_regmap_degree in
    25         〈v + 1, (r, v)::regmap,
     26record interference_graph: Type[1] ≝
     27{
     28  ig_reg_table  : table_adt register vertex ordered_register;
     29  ig_vertex_set : set_adt vertex ordered_vertex;
     30  ig_vertex_pset: priority_set_adt vertex ordered_vertex;
     31  ig_Reg_set    : set_adt Register ordered_Register;
     32  ig_regmap     : table … ig_reg_table register vertex;
     33  ig_ivv        : set … ig_vertex_set vertex;
     34  ig_ivh        : set … ig_Reg_set Register;
     35  ig_pvv        : set … ig_vertex_set vertex;
     36  ig_pvh        : set … ig_Reg_set Register;
     37  ig_degree     : priority_set … ig_vertex_pset vertex;
     38  ig_nmr        : priority_set … ig_vertex_pset vertex
     39}.
    2640
     41definition ig_create ≝
     42  λreg_table  : table_adt register vertex ordered_register.
     43  λvertex_set : set_adt vertex ordered_vertex.
     44  λvertex_pset: priority_set_adt vertex ordered_vertex.
     45  λReg_set    : set_adt Register ordered_Register.
     46  λregs.
     47  let 〈ignore_int, table'', priority''〉 ≝
     48    foldr … (λr. λv_table_priority'.
     49      let 〈v, table', priority'〉 ≝ v_table_priority' in
     50      let table'' ≝ insert … reg_table r v table' in
     51      let priority'' ≝ insert … vertex_pset v 0 priority' in
     52        〈v + 1, table'', priority''〉) 〈0, empty …, empty …〉 regs
     53  in
     54    mk_interference_graph
     55      reg_table vertex_set vertex_pset Reg_set
     56      table'' [ ] [ ] [ ] [ ] priority'' priority''.
    2757
     58definition ig_mkipp: interference_graph → list register → list register →
     59  interference_graph ≝
     60  λgraph.
     61  λregs1.
     62  λregs2.
     63    foldr … (λr. λgraph.
     64      let v1 ≝ lookup
    2865
     66let mkipp graph regs1 regs2 =
     67  Register.Set.fold (fun r1 graph ->
     68    let v1 = lookup graph r1 in
     69    Register.Set.fold (fun r2 graph ->
     70      interference#mkvv graph v1 (lookup graph r2)
     71    ) regs2 graph
     72  ) regs1 graph
    2973
    30 let create regs =
    31   let (_ : int), regmap, degree =
    32     Register.Set.fold (fun r (v, regmap, degree) ->
    33       v+1,
    34       RegMap.add r v regmap,
    35       PrioritySet.add v 0 degree
    36     ) regs (0, RegMap.empty, PrioritySet.empty)
    37   in
    38   {
    39     regmap = regmap;
    40     ivv = Vertex.Map.empty;
    41     ivh = Vertex.Map.empty;
    42     pvv = Vertex.Map.empty;
    43     pvh = Vertex.Map.empty;
    44     degree = degree;
    45     nmr = degree
    46   }
    47 
    48 
    49 axiom ig_mki: interference_graph → (list register) × (list Register) →
    50   (list register) × (list Register) → interference_graph.
    5174axiom ig_mkiph: interference_graph → list register → list Register →
    5275  interference_graph.
     76
     77definition ig_mki: interference_graph → (list register) × (list Register) →
     78  (list register) × (list Register) → interference_graph ≝
     79  λgraph.
     80  λregs1_hwregs1.
     81  λregs2_hwregs2.
     82    let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
     83    let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
     84    let graph ≝ ig_mkipp graph regs1 regs2 in
     85    let graph ≝ ig_mkiph graph regs1 hwregs2 in
     86    let graph ≝ ig_mkiph graph regs2 hwregs1 in
     87      graph.
     88 
    5389axiom ig_mkppp: interference_graph → register → register → interference_graph.
    5490axiom ig_mkpph: interference_graph → register → Register → interference_graph.
Note: See TracChangeset for help on using the changeset viewer.