Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
4 edited
3 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/utilities/Interference.ma

    r1153 r1197  
    33include "common/Graphs.ma".
    44include "common/Registers.ma".
     5include "utilities/RegisterSet.ma".
     6
     7definition vertex ≝ nat. (* XXX: int in o'caml *)
     8
     9(* vertex sets *)
     10axiom vertex_set: Type[0].
     11axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
     12axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
     13axiom vs_subset: vertex_set → vertex_set → bool.
     14
     15(* vertex maps *)
     16axiom vertex_map: Type[0] → Type[0].
     17axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
    518
    619definition interference_graph ≝ graph label.
    7 axiom vertex: Type[0].
    8 axiom vertex_set: Type[0].
    9 axiom vertex_map: Type[0].
    1020
    11 axiom ig_create: list register → interference_graph.
     21definition 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,
     26
     27
     28
     29
     30let 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
    1249axiom ig_mki: interference_graph → (list register) × (list Register) →
    1350  (list register) × (list Register) → interference_graph.
     
    3067  interference_graph → option vertex.
    3168axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → interference_graph → A → A.
    32 axiom ig_ipp: interference_graph → vertex → list vertex.
     69axiom ig_ipp: interference_graph → vertex → vertex_set.
    3370axiom ig_iph: interference_graph → vertex → list Register.
    34 axiom ig_ppp: interference_graph → vertex → list vertex.
     71axiom ig_ppp: interference_graph → vertex → vertex_set.
    3572axiom ig_pph: interference_graph → vertex → list Register.
    3673definition ig_ppedge ≝ vertex × vertex.
  • Deliverables/D3.3/id-lookup-branch/utilities/RegisterSet.ma

    r1075 r1197  
    1111  rs_exists: Register → rs_set → bool;
    1212  rs_union: rs_set → rs_set → rs_set;
     13  rs_subset: rs_set → rs_set → bool;
    1314  rs_to_list: rs_set → list Register;
    1415  rs_from_list: list Register → rs_set
     
    4546  λs: list Register.
    4647    nub_by ? eq_Register (r @ s).
     48
     49definition rs_list_set_subset ≝
     50  λr: list Register.
     51  λs: list Register.
     52    forall … (λx. member … eq_Register x s) r.
    4753 
    4854definition rs_list_set_from_list ≝
     
    5561                  rs_list_set_insert rs_list_set_exists
    5662                  rs_list_set_union
     63                  rs_list_set_subset
    5764                  (λx. x) rs_list_set_from_list.
  • Deliverables/D3.3/id-lookup-branch/utilities/lists.ma

    r1105 r1197  
    9797| #h #t #IH #l2 normalize //
    9898] qed.
     99
     100let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
     101match l with
     102[ nil ⇒ None B
     103| cons h t ⇒
     104    match f h with
     105    [ None ⇒ find A B f t
     106    | Some b ⇒ Some B b
     107    ]
     108].
Note: See TracChangeset for help on using the changeset viewer.