Ignore:
Timestamp:
Sep 28, 2011, 11:50:32 PM (9 years ago)
Author:
sacerdot
Message:

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Interference.ma

    r1241 r1282  
    2525
    2626axiom build: ∀valuation. coloured_graph valuation.
    27 
    28 (*
    29 (* definition vertex_set ≝ set vertex. *)
    30 definition vertex_priority_set ≝ priority_set vertex.
    31 definition vertex_set_table ≝ set_table vertex (set vertex).
    32 definition vertex_set ≝ set vertex.
    33 definition Register_set_table ≝ set_table vertex (set Register).
    34 definition Register_set ≝ set Register.
    35 *)
    36 
    37 (*
    38 record graph: Type[0] ≝
    39 {
    40   g_regmap     : register_table;
    41   g_ivv        : vertex_set_table;
    42   g_ivh        : Register_set_table;
    43   g_pvv        : vertex_set_table;
    44   g_pvh        : Register_set_table;
    45   g_degree     : vertex_priority_set;
    46   g_nmr        : vertex_priority_set
    47 }.
    48 
    49 definition set_ivv ≝
    50   λgraph.
    51   λivv: vertex_set_table.
    52     let regmap ≝ g_regmap graph in
    53     let ivh    ≝ g_ivh graph in
    54     let pvv    ≝ g_pvv graph in
    55     let pvh    ≝ g_pvh graph in
    56     let degree ≝ g_degree graph in
    57     let nmr    ≝ g_nmr graph in
    58       mk_graph
    59         regmap ivv ivh pvv pvh degree nmr.
    60 
    61 definition set_ivh ≝
    62   λgraph.
    63   λivh: Register_set_table.
    64     let regmap ≝ g_regmap graph in
    65     let ivv    ≝ g_ivv graph in
    66     let pvv    ≝ g_pvv graph in
    67     let pvh    ≝ g_pvh graph in
    68     let degree ≝ g_degree graph in
    69     let nmr    ≝ g_nmr graph in
    70       mk_graph
    71         regmap ivv ivh pvv pvh degree nmr.
    72 
    73 definition set_degree ≝
    74   λgraph.
    75   λdegree: vertex_priority_set.
    76     let regmap ≝ g_regmap graph in
    77     let ivv    ≝ g_ivv graph in
    78     let ivh    ≝ g_ivh graph in
    79     let pvv    ≝ g_pvv graph in
    80     let pvh    ≝ g_pvh graph in
    81     let nmr    ≝ g_nmr graph in
    82       mk_graph
    83         regmap ivv ivh pvv pvh degree nmr.
    84 
    85 definition set_nmr ≝
    86   λgraph.
    87   λnmr: vertex_priority_set.
    88     let regmap ≝ g_regmap graph in
    89     let ivv    ≝ g_ivv graph in
    90     let ivh    ≝ g_ivh graph in
    91     let pvv    ≝ g_pvv graph in
    92     let pvh    ≝ g_pvh graph in
    93     let degree ≝ g_degree graph in
    94       mk_graph
    95         regmap ivv ivh pvv pvh degree nmr.
    96 
    97 definition sg_neighboursv ≝
    98   λgraph: graph.
    99   λv: vertex.
    100     set_tbl_find … v (g_ivv graph).
    101 
    102 definition sg_existsvv ≝
    103   λgraph.
    104   λv1.
    105   λv2.
    106   match sg_neighboursv graph v2 with
    107   [ None       ⇒ false (* XXX: ok? *)
    108   | Some neigh ⇒ set_member ? eq_nat v1 neigh
    109   ].
    110 
    111 definition sg_neighboursh ≝
    112   λgraph.
    113   λv.
    114     set_tbl_find ? ? v (g_ivh graph).
    115 
    116 definition sg_existsvh ≝
    117   λgraph.
    118   λv.
    119   λh.
    120   match sg_neighboursh graph v with
    121   [ None       ⇒ false (* XXX: ok? *)
    122   | Some neigh ⇒ set_member ? eq_Register h neigh
    123   ].
    124 
    125 definition sg_degree ≝
    126   λgraph.
    127   λv.
    128   match sg_neighboursv graph v with
    129   [ None ⇒ None ?
    130   | Some neigh ⇒
    131     match sg_neighboursh graph v with
    132     [ None ⇒ None ?
    133     | Some neigh' ⇒ Some ? ((set_size … neigh) + (set_size … neigh'))
    134     ]
    135   ].
    136    
    137 definition sg_hwregs ≝
    138   λgraph: graph.
    139     let union ≝ λkey: vertex. set_union ? in
    140     set_tbl_fold vertex ? ? union (g_ivh graph) (set_empty Register).
    141 
    142 axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)
    143 
    144 definition sg_mkvvi ≝
    145   λgraph.
    146   λv1.
    147   λv2.
    148     set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (g_ivv graph)).
    149 
    150 definition sg_mkvv ≝
    151   λgraph.
    152   λv1.
    153   λv2.
    154     if eq_nat v1 v2 then
    155       graph
    156     else if sg_existsvv graph v1 v2 then
    157       graph
    158     else
    159       sg_mkvvi graph v1 v2.
    160 
    161 definition sg_rmvv ≝
    162   λgraph.
    163   λv1.
    164   λv2.
    165     set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (g_ivv graph)).
    166 
    167 definition sg_rmvvifx ≝
    168   λgraph.
    169   λv1.
    170   λv2.
    171   if sg_existsvv graph v1 v2 then
    172     sg_rmvv graph v1 v2
    173   else
    174     graph.
    175 
    176 definition sg_mkvhi ≝
    177   λgraph.
    178   λv.
    179   λh.
    180     set_ivh graph (set_tbl_update … v (set_insert … h) (g_ivh graph)).
    181 
    182 definition sg_mkvh ≝
    183   λgraph.
    184   λv.
    185   λh.
    186   if sg_existsvh graph v h then
    187     graph
    188   else
    189     sg_mkvhi graph v h.
    190 
    191 definition sg_rmvh ≝
    192   λgraph.
    193   λv.
    194   λh.
    195     set_ivh graph (set_tbl_update … v (set_remove … h) (g_ivh graph)).
    196 
    197 definition sg_rmvhifx ≝
    198   λgraph.
    199   λv.
    200   λh.
    201     if sg_existsvh graph v h then
    202       sg_rmvh graph v h
    203     else
    204       graph.
    205 
    206 definition sg_coalesce ≝
    207   λg.
    208   λx.
    209   λy.
    210   match sg_neighboursv g x with
    211   [ None       ⇒ None ?
    212   | Some neigh ⇒
    213     let graph ≝ set_fold ? graph (λw. λg.
    214       sg_mkvv (sg_rmvv g x w) y w) neigh g
    215     in
    216     match sg_neighboursh g x with
    217     [ None ⇒ None ?
    218     | Some neigh ⇒
    219       let graph ≝ set_fold ? ? (λh. λg.
    220         sg_mkvh (sg_rmvh g x h) y h) neigh g
    221       in
    222         Some … graph
    223     ]
    224   ].
    225 
    226 definition sg_coalesceh ≝
    227   λg.
    228   λx.
    229   λh.
    230   match sg_neighboursv g x with
    231   [ None       ⇒ None ?
    232   | Some neigh ⇒
    233     let graph ≝ set_fold ? graph (λw. λg.
    234       sg_mkvh (sg_rmvv g x w) w h) neigh g
    235     in
    236     match sg_neighboursh g x with
    237     [ None ⇒ None ?
    238     | Some neigh ⇒
    239       let graph ≝ set_fold ? ? (λk. λg.
    240         sg_rmvh graph x k) neigh g
    241       in
    242         Some … graph
    243     ]
    244   ].
    245 
    246 definition sg_remove ≝
    247   λg.
    248   λx.
    249   match sg_neighboursv g x with
    250   [ None ⇒ None ?
    251   | Some neigh ⇒
    252     let graph ≝
    253       set_fold … (λw. λgraph.
    254         sg_rmvv graph x w) neigh g
    255     in
    256     match sg_neighboursh graph x with
    257     [ None ⇒ None ?
    258     | Some neigh ⇒
    259       let graph ≝ set_fold … (λh. λg.
    260         sg_rmvh g x h) neigh graph
    261       in
    262         Some ? graph
    263     ]
    264   ].
    265 
    266 definition ig_mkvvi ≝
    267   λgraph.
    268   λv1.
    269   λv2.
    270   let graph ≝ sg_mkvvi graph v1 v2 in
    271   let graph ≝ sg_rmvvifx graph v1 v2 in
    272   let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (g_degree graph)) in
    273   let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (g_nmr graph)) in
    274     set_degree (set_nmr graph nmr') degree'.
    275 
    276 definition ig_rmvv ≝
    277   λgraph.
    278   λv1.
    279   λv2.
    280   let graph ≝ sg_rmvv graph v1 v2 in
    281   let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (g_degree graph)) in
    282   let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (g_nmr graph)) in
    283     set_degree (set_nmr graph nmr') degree'.
    284 
    285 definition ig_mkvhi ≝
    286   λgraph.
    287   λv.
    288   λh.
    289   let graph ≝ sg_mkvhi graph v h in
    290   let graph ≝ sg_rmvhifx graph v h in
    291   let degree ≝ pset_increment ? v (repr 1) (g_degree graph) in
    292   let nmr ≝ pset_incrementifx ? v (repr 1) (g_nmr graph) in
    293     set_degree (set_nmr graph nmr) degree.
    294 
    295 definition ig_rmvh ≝
    296   λgraph.
    297   λv.
    298   λh.
    299   let graph ≝ sg_rmvh graph v h in
    300   let degree ≝ pset_increment ? v (neg (repr 1)) (g_degree graph) in
    301   let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (g_nmr graph) in
    302     set_degree (set_nmr graph nmr) degree.
    303 
    304 definition pref_nmr ≝
    305   λgraph.
    306   λv.
    307   match sg_neighboursv graph v with
    308   [ None       ⇒ false (* XXX: ok? *)
    309   | Some neigh ⇒
    310     match sg_neighboursh graph v with
    311     [ None        ⇒ false
    312     | Some neigh' ⇒
    313       andb (set_is_empty ? neigh) (set_is_empty ? neigh')
    314     ]
    315   ].
    316 
    317 definition pref_mkcheck ≝
    318   λgraph.
    319   λv.
    320     if pref_nmr graph v then
    321       let nmr' ≝ pset_remove ? v (g_nmr graph) in
    322         set_nmr graph nmr'
    323     else
    324       graph.
    325 
    326 definition pref_mkvvi ≝
    327   λgraph.
    328   λv1.
    329   λv2.
    330     if sg_existsvv graph v1 v2 then
    331       graph
    332     else
    333       let graph ≝ pref_mkcheck graph v1 in
    334       let graph ≝ pref_mkcheck graph v2 in
    335         sg_mkvvi graph v1 v2.
    336 
    337 definition pref_mkvhi ≝
    338   λgraph.
    339   λv.
    340   λh.
    341   if sg_existsvh graph v h then
    342     graph
    343   else
    344     let graph ≝ pref_mkcheck graph v in
    345       sg_mkvhi graph v h.
    346 
    347 (* XXX: look at this carefully *)
    348 definition pref_rmcheck ≝
    349   λgraph.
    350   λv.
    351   if pref_nmr graph v then
    352     match pset_lookup ? v (g_degree graph) with
    353     [ None ⇒ graph (* XXX: ok? *)
    354     | Some pref ⇒
    355       let nmr ≝ pset_insert ? v pref (g_nmr graph) in
    356         set_nmr graph nmr
    357     ]
    358   else
    359     graph.
    360 
    361 definition pref_rmvv ≝
    362   λgraph.
    363   λv1.
    364   λv2.
    365   let graph ≝ sg_rmvv graph v1 v2 in
    366   let graph ≝ pref_rmcheck graph v1 in
    367   let graph ≝ pref_rmcheck graph v2 in
    368     graph.
    369 
    370 definition pref_rmvh ≝
    371   λgraph.
    372   λv.
    373   λh.
    374   let graph ≝ sg_rmvh graph v h in
    375   let graph ≝ pref_rmcheck graph v in
    376     graph.
    377    
    378 definition ig_ipp ≝ sg_neighboursv.
    379 definition ig_iph ≝ sg_neighboursh.
    380 definition ig_ppp ≝ sg_neighboursv.
    381 definition ig_pph ≝ sg_neighboursh.
    382 definition ig_degree ≝ λgraph. λv. pset_lookup ? v (g_degree graph).
    383 definition ig_lowest ≝ λgraph. pset_lowest ? (g_degree graph).
    384 definition ig_lowest_non_move_related ≝ λgraph. pset_lowest ? (g_nmr graph).
    385 definition ig_fold ≝ λA: Type[0]. λf: vertex → A → A. λgraph. λaccu.
    386   rt_fold … (λv. λ_. λaccu. f v accu) (g_regmap graph) accu.
    387 
    388 definition ig_minimum: ∀a: Type[0]. (a → a → order) → (vertex → a) → graph → option vertex ≝
    389   λa: Type[0].
    390   λcompare: a → a → order.
    391   λf: vertex → a.
    392   λgraph.
    393   let folded ≝ ig_fold … (λw. λaccu.
    394     let dw ≝ f w in
    395       match accu with
    396       [ None      ⇒ Some … 〈dw, w〉
    397       | Some dv_v ⇒
    398         let 〈dv, v〉 ≝ dv_v in
    399           match compare dw dv with
    400           [ order_lt ⇒ Some … 〈dw, w〉
    401           | _        ⇒ accu
    402           ]
    403       ]) graph (None …)
    404   in
    405     match folded with
    406     [ None          ⇒ None …
    407     | Some ignore_v ⇒
    408       let 〈ignore, v〉 ≝ ignore_v in
    409         Some … v
    410     ].
    411    
    412 definition ig_ppedge ≝ vertex × vertex.
    413 
    414 definition ig_pppick ≝ λgraph. λp. set_tbl_pick … (g_pvv graph) p.
    415 
    416 definition ig_phedge ≝ vertex × Register.
    417 
    418 definition ig_phpick ≝ λgraph. λp. set_tbl_pick … (g_pvh graph) p.
    419 
    420 definition ig_create ≝
    421   λregs.
    422   let 〈ignore_int, table'', priority''〉 ≝
    423     foldr … (λr. λv_table_priority'.
    424       let 〈v, table', priority'〉 ≝ v_table_priority' in
    425       let table'' ≝ rt_add r v table' in
    426       let priority'' ≝ pset_insert ? v 0 priority' in
    427         〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs
    428   in
    429       mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_tbl_empty …)
    430       (set_tbl_empty …) priority'' priority''.
    431 definition ig_lookup ≝ λgraph. λr. rt_backward r (g_regmap graph).
    432 definition ig_registers ≝ λgraph. λv. rt_forward v (g_regmap graph).
    433 definition ig_mkipp ≝
    434   λgraph.
    435   λregs1.
    436   λregs2.
    437     set_fold … (λr1. λgraph.
    438       let v1 ≝ ig_lookup graph r1 in
    439         set_fold … (λr2. λgraph.
    440           sg_mkvv graph v1 (ig_lookup graph r2)
    441         ) regs2 graph
    442     ) regs1 graph.
    443 definition ig_mkiph ≝
    444   λgraph.
    445   λregs.
    446   λhwregs.
    447     set_fold … (λr. λgraph.
    448       let v ≝ ig_lookup graph r in
    449         set_fold … (λh. λgraph.
    450           sg_mkvh graph v h
    451         ) hwregs graph
    452     ) regs graph.
    453 definition ig_mki ≝
    454   λgraph.
    455   λregs1_hwregs1.
    456   λregs2_hwregs2.
    457   let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
    458   let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
    459   let graph ≝ ig_mkipp graph regs1 regs2 in
    460   let graph ≝ ig_mkiph graph regs1 hwregs2 in
    461   let graph ≝ ig_mkiph graph regs2 hwregs1 in
    462     graph.
    463 definition ig_mkppp ≝
    464   λgraph.
    465   λr1.
    466   λr2.
    467   let v1 ≝ ig_lookup graph r1 in
    468   let v2 ≝ ig_lookup graph r2 in
    469   let graph ≝ sg_mkvv graph v1 v2 in
    470     graph.
    471 definition ig_mkpph ≝
    472   λgraph.
    473   λr.
    474   λh.
    475   let v ≝ ig_lookup graph r in
    476   let graph ≝ sg_mkvh graph v h in
    477     graph.
    478 (*   
    479 (* XXX: precondition:
    480   x \not\eq y
    481   existsvv graph x y == false i.e. coalesce interfering edges *)
    482 definition ig_coalesce ≝
    483   λgraph.
    484   λx.
    485   λy.
    486   let graph ≝ sg_coalesce graph x y in
    487 
    488 let coalesce graph x y =
    489 
    490   assert (x <> y); (* attempt to coalesce one vertex with itself *)
    491   assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *)
    492 
    493   (* Perform coalescing in the two subgraphs. *)
    494 
    495   let graph = interference#coalesce graph x y in
    496   let graph = preference#coalesce graph x y in
    497 
    498   (* Remove [x] from all tables. *)
    499 
    500   {
    501     graph with
    502     regmap = RegMap.coalesce x y graph.regmap;
    503     ivh = Vertex.Map.remove x graph.ivh;
    504     pvh = Vertex.Map.remove x graph.pvh;
    505     degree = PrioritySet.remove x graph.degree;
    506     nmr = PrioritySet.remove x graph.nmr;
    507   }
    508 
    509 axiom ig_mkppp: graph → register → register → graph.
    510 axiom ig_mkpph: graph → register → Register → graph.
    511 axiom ig_coalesce: graph → vertex → vertex → graph.
    512 axiom ig_coalesceh: graph → vertex → Register → graph.
    513 axiom ig_remove: graph → vertex → graph.
    514 axiom ig_freeze: graph → vertex → graph.
    515 axiom ig_restrict: graph → (vertex → bool) → graph.
    516 axiom ig_droph: graph → graph.
    517 axiom ig_lookup: graph → register → vertex.
    518 axiom ig_registers: graph → vertex → list register.
    519 axiom ig_degree: graph → vertex → nat.
    520 axiom ig_lowest: graph → option (vertex × nat).
    521 axiom ig_lowest_non_move_related: graph → option (vertex × nat).
    522 axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
    523   graph → option vertex.
    524 axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → graph → A → A.
    525 axiom ig_ipp: graph → vertex → vertex_set.
    526 axiom ig_iph: graph → vertex → list Register.
    527 axiom ig_ppp: graph → vertex → vertex_set.
    528 axiom ig_pph: graph → vertex → list Register.
    529 definition ig_ppedge ≝ vertex × vertex.
    530 axiom ig_pppick: graph → (ig_ppedge → bool) → option ig_ppedge.
    531 definition ig_phedge ≝ vertex × Register.
    532 axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
    533 *)
    534 *)
Note: See TracChangeset for help on using the changeset viewer.