Changeset 1210


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

getting rid of typeclass-like records in favour of file-level axioms. much too heavyweight to use effectively

Location:
src/utilities
Files:
2 added
4 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Interference.ma

    r1209 r1210  
    77include "utilities/adt/priority_set_adt.ma".
    88include "utilities/adt/set_adt.ma".
     9include "utilities/adt/register_table.ma".
    910
    10 definition vertex ≝ nat. (* XXX: int in o'caml *)
     11definition vertex_set ≝ set_adt vertex vertex_ordered.
     12definition vertex_priority_set ≝ priority_set_adt vertex vertex_ordered.
     13definition Register_set ≝ set_adt Register Register_ordered.
    1114
    12 (* vertex sets *)
    13 axiom vertex_set: Type[0].
    14 axiom vs_fold: ∀A: Type[0]. (vertex → A → A) → vertex_set → A → A.
    15 axiom vs_filter: (vertex → bool) → vertex_set → vertex_set.
    16 axiom vs_subset: vertex_set → vertex_set → bool.
    17 
    18 (* vertex maps *)
    19 axiom vertex_map: Type[0] → Type[0].
    20 axiom vm_find: ∀A: Type[0]. vertex → vertex_map A → option A.
    21 
    22 axiom ordered_vertex: ordered vertex.
    23 axiom ordered_register: ordered register.
    24 axiom ordered_Register: ordered Register.
    25 
    26 record interference_graph: Type[1] ≝
     15record graph
     16  (set_impl: set_adt … Register Register_ordered): Type[1] ≝
    2717{
    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;
     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;
    3323  ig_ivv        : set … ig_vertex_set vertex;
    3424  ig_ivh        : set … ig_Reg_set Register;
     
    4030
    4131definition 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.
     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.
    4636  λregs.
    4737  let 〈ignore_int, table'', priority''〉 ≝
    4838    foldr … (λr. λv_table_priority'.
    4939      let 〈v, table', priority'〉 ≝ v_table_priority' in
    50       let table'' ≝ tbl_insert … reg_table r v table' in
    51       let priority'' ≝ ps_insert … vertex_pset v 0 priority' in
    52         〈v + 1, table'', priority''〉) 〈0, tbl_empty …, ps_empty …〉 regs
     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
     42        〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs
    5343  in
    54     mk_interference_graph
    55       reg_table vertex_set vertex_pset Reg_set
    56       table'' (set_empty …) (set_empty …) (set_empty …)
     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 …)
    5747      (set_empty …) priority'' priority''.
    5848
    59 definition ig_mkipp: interference_graph → list register → list register →
    60   interference_graph ≝
    61   λgraph.
     49definition neighboursv ≝
     50  λset_impl.
     51  λgraph: graph set_impl.
     52    set_find … (ig_vertex_set … graph) v (getvv set_impl graph).
     53
     54  method neighborsv graph v =
     55    VertexSetMap.find v (self#getvv graph)
     56
     57definition ig_mkipp ≝
     58  λset_impl.
     59  λgraph: interference_graph set_impl.
    6260  λregs1.
    6361  λregs2.
    64     foldr … (λr. λgraph.
    65       let v1 ≝ lookup graph e1 in
     62    set_fold … (ig_Reg_set … graph) (λr1. λgraph.
     63      let v1 ≝ lookup … graph r1 in
     64        set_fold … (ig_Reg_set … graph) (λr2. λgraph.
     65          ig_mkvv …
    6666
    6767let mkipp graph regs1 regs2 =
  • src/utilities/adt/priority_set_adt.ma

    r1208 r1210  
    66include "ASM/Util.ma".
    77
    8 record priority_set_adt
    9   (elt_type: Type[0]) (order: ordered elt_type): Type[1] ≝
    10 {
    11   priority_set: Type[0] → Type[0];
     8axiom priority_set: Type[0] → Type[0].
    129 
    13   ps_empty       : priority_set elt_type;
    14   ps_size        : priority_set elt_type → nat;
     10axiom ps_empty: ∀elt_type. priority_set elt_type.
     11axiom ps_size: ∀elt_type. priority_set elt_type → nat.
    1512 
    16   ps_to_list     : priority_set elt_type → list (elt_type × nat);
     13axiom ps_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).
    1714 
    18   ps_insert      : elt_type → nat → priority_set elt_type → priority_set elt_type;
    19   ps_remove      : elt_type → priority_set elt_type → priority_set elt_type;
    20   ps_lookup      : elt_type → priority_set elt_type → option nat;
     15axiom ps_insert: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
     16axiom ps_remove: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
     17axiom ps_lookup: ∀elt_type. elt_type → priority_set elt_type → option nat.
    2118 
    22   ps_increment   : elt_type → priority_set elt_type → priority_set elt_type;
    23   ps_modify      : elt_type → nat → priority_set elt_type → priority_set elt_type;
    24   ps_lowest      : priority_set elt_type → option (elt_type × nat);
     19axiom ps_increment: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
     20axiom ps_modify: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
     21axiom ps_lowest: ∀elt_type. priority_set elt_type → option (elt_type × nat).
    2522 
    26   ps_equal       : priority_set elt_type → priority_set elt_type → bool;
     23axiom ps_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.
    2724 
    28   ps_map         : ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a;
    29   ps_fold        : ∀a: Type[0]. (elt_type → nat → a → a) → priority_set elt_type
    30                   → a → a 
    31 }.
     25axiom ps_map: ∀elt_type. ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a.
     26axiom ps_fold: ∀elt_type. ∀a: Type[0]. (elt_type → nat → a → a) → priority_set elt_type → a → a.
    3227
    3328definition ps_is_empty ≝
    3429  λelt_type         : Type[0].
    35   λorder            : ordered elt_type.
    36   λpriority_set_adt : priority_set_adt elt_type order.
    37   λpriority_set     : priority_set elt_type order priority_set_adt elt_type.
     30  λpriority_set     : priority_set elt_type.
    3831    ps_size … priority_set = 0.
    3932
    4033definition ps_singleton ≝
    4134  λelt_type        : Type[0].
    42   λorder           : ordered elt_type.
    43   λpriority_set_adt: priority_set_adt elt_type order.
    4435  λelt             : elt_type.
    4536  λpriority        : nat.
    46     ps_insert … elt priority (ps_empty elt_type order priority_set_adt).
     37    ps_insert … elt priority (ps_empty elt_type).
    4738
    4839definition from_list ≝
    4940  λelt_type        : Type[0].
    50   λorder           : ordered elt_type.
    51   λpriority_set_adt: priority_set_adt elt_type order.
    5241  λthe_list        : list (elt_type × nat).
    5342    foldr … (λelt_priority.
    5443      let 〈elt, priority〉 ≝ elt_priority in
    55         ps_insert elt_type order priority_set_adt elt priority)
     44        ps_insert elt_type elt priority)
    5645          (ps_empty …) the_list.
  • src/utilities/adt/set_adt.ma

    r1208 r1210  
    55include "utilities/adt/ordering.ma".
    66
    7 record set_adt
    8   (elt_type: Type[0]) (order: ordered elt_type): Type[1] ≝
    9 {
    10   set        : Type[0] → Type[0];
    11  
    12   set_empty  : set elt_type;
    13   set_size   : set elt_type → nat;
    14  
    15   set_to_list: set elt_type → list elt_type;
    16  
    17   set_insert : elt_type → set elt_type → set elt_type;
    18   set_remove : elt_type → set elt_type → set elt_type;
    19  
    20   set_member : elt_type → set elt_type → bool;
    21  
    22   set_forall : (elt_type → bool) → set elt_type → bool;
    23   set_exists : (elt_type → bool) → set elt_type → bool;
    24   set_filter : (elt_type → bool) → set elt_type → set elt_type;
    25  
    26   set_equal  : set elt_type → set elt_type → bool;
    27  
    28   set_map    : ∀a: Type[0]. (elt_type → a) → set elt_type → set a;
    29   set_fold   : ∀a: Type[0]. (elt_type → a → a) → set elt_type  → a → a
    30 }.
     7axiom set: Type[0] → Type[0].
     8axiom set_empty: ∀elt_type. set elt_type.
     9
     10axiom set_size: ∀elt_type. set elt_type → nat.
     11axiom set_to_list: ∀elt_type. set elt_type → list elt_type.
     12axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type.
     13axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type.
     14axiom set_member: ∀elt_type. elt_type → set elt_type → bool.
     15axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool.
     16axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool.
     17axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type.
     18axiom set_equal: ∀elt_type. set elt_type → set elt_type → bool.
     19axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a.
     20axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type  → a → a.
    3121
    3222definition set_is_empty ≝
    3323  λelt_type: Type[0].
    34   λorder   : ordered elt_type.
    35   λset_adt : set_adt elt_type order.
    36   λset     : set elt_type order set_adt elt_type.
    37     set_size … set = 0.
     24  λset: set elt_type.
     25    set_size elt_type set = 0.
    3826
    3927definition set_singleton ≝
    4028  λelt_type: Type[0].
    41   λorder   : ordered elt_type.
    42   λset_adt : set_adt elt_type order.
    4329  λelt     : elt_type.
    44     set_insert … elt (set_empty elt_type order set_adt).
     30    set_insert elt_type elt (set_empty elt_type).
    4531
    4632definition set_from_list ≝
    4733  λelt_type: Type[0].
    48   λorder   : ordered elt_type.
    49   λset_adt : set_adt elt_type order.
    5034  λthe_list: list elt_type.
    51     foldr … (set_insert elt_type order set_adt) (set_empty …) the_list.
     35    foldr … (set_insert elt_type) (set_empty elt_type) the_list.
    5236
    5337definition set_split ≝
    5438  λelt_type: Type[0].
    55   λorder   : ordered elt_type.
    56   λset_adt : set_adt elt_type order.
    5739  λpred    : elt_type → bool.
    58   λthe_set : set elt_type order set_adt elt_type.
    59   let left  ≝ set_filter elt_type order set_adt pred the_set in
     40  λthe_set : set elt_type.
     41  let left  ≝ set_filter elt_type pred the_set in
    6042  let npred ≝ λx. ¬ (pred x) in
    61   let right ≝ set_filter elt_type order set_adt npred the_set in
     43  let right ≝ set_filter elt_type npred the_set in
    6244    〈left, right〉.
    6345
    6446definition set_subset ≝
    6547  λelt_type: Type[0].
    66   λorder   : ordered elt_type.
    67   λset_adt : set_adt elt_type order.
    68   λleft    : set elt_type order set_adt elt_type.
    69   λright   : set elt_type order set_adt elt_type.
    70     set_forall … (λelt. set_member … elt right) left.
     48  λleft    : set elt_type.
     49  λright   : set elt_type.
     50    set_forall elt_type (λelt. set_member elt_type elt right) left.
    7151
    7252definition set_subseteq ≝
    7353  λelt_type: Type[0].
    74   λorder   : ordered elt_type.
    75   λset_adt : set_adt elt_type order.
    76   λleft    : set elt_type order set_adt elt_type.
    77   λright   : set elt_type order set_adt elt_type.
    78     set_equal … left right ∧ (set_subset elt_type order set_adt left right).
     54  λleft    : set elt_type.
     55  λright   : set elt_type.
     56    set_equal elt_type left right ∧ (set_subset elt_type left right).
    7957
    8058definition set_union ≝
    8159  λelt_type: Type[0].
    82   λorder   : ordered elt_type.
    83   λset_adt : set_adt elt_type order.
    84   λleft    : set elt_type order set_adt elt_type.
    85   λright   : set elt_type order set_adt elt_type.
    86     set_fold … (set_insert elt_type order set_adt) left right.
     60  λleft    : set elt_type.
     61  λright   : set elt_type.
     62    set_fold elt_type (set elt_type) (set_insert elt_type) left right.
    8763
    8864definition set_intersection ≝
    8965  λelt_type: Type[0].
    90   λelt_type: Type[0].
    91   λorder   : ordered elt_type.
    92   λset_adt : set_adt elt_type order.
    93   λleft    : set elt_type order set_adt elt_type.
    94   λright   : set elt_type order set_adt elt_type.
    95     set_filter … (λelt. set_member … elt right) left.
     66  λleft    : set elt_type.
     67  λright   : set elt_type.
     68    set_filter elt_type (λelt. set_member elt_type elt right) left.
  • src/utilities/adt/table_adt.ma

    r1208 r1210  
    1010include "ASM/Util.ma".
    1111
    12 record table_adt
    13   (key_type: Type[0]) (rng_type: Type[0]) (order: ordered key_type): Type[1] ≝
    14 {
    15   table  : Type[0] → Type[0] → Type[0];
     12axiom table: Type[0] → Type[0] → Type[0].
    1613 
    17   tbl_empty  : table key_type rng_type;
    18   tbl_size   : table key_type rng_type → nat;
     14axiom tbl_empty  : ∀key_type, rng_type. table key_type rng_type.
     15axiom tbl_size   : ∀key_type, rng_type. table key_type rng_type → nat.
    1916 
    20   tbl_to_list: table key_type rng_type → list (key_type × rng_type);
     17axiom tbl_to_list: ∀key_type, rng_type. table key_type rng_type → list (key_type × rng_type).
    2118 
    22   tbl_insert : key_type → rng_type → table key_type rng_type → table key_type rng_type;
    23   tbl_remove : key_type → table key_type rng_type → table key_type rng_type;
     19axiom tbl_insert : ∀key_type, rng_type. key_type → rng_type → table key_type rng_type → table key_type rng_type.
     20axiom tbl_remove : ∀key_type, rng_type. key_type → table key_type rng_type → table key_type rng_type.
    2421 
    25   tbl_find   : key_type → table key_type rng_type → option rng_type;
     22axiom tbl_find   : ∀key_type, rng_type. key_type → table key_type rng_type → option rng_type.
     23axiom tbl_update : ∀key_type, rng_type. key_type → (rng_type → rng_type) → table key_type rng_type →
     24                    table key_type rng_type.
    2625 
    27   tbl_forall : (rng_type → bool) → table key_type rng_type → bool;
    28   tbl_exists : (rng_type → bool) → table key_type rng_type → bool;
    29   tbl_filter : (rng_type → bool) → table key_type rng_type → table key_type rng_type;
     26axiom tbl_forall : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → bool.
     27axiom tbl_exists : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → bool.
     28axiom tbl_filter : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → table key_type rng_type.
    3029 
    31   tbl_equal  : equal rng_type → table key_type rng_type
    32              → table key_type rng_type → bool;
     30axiom tbl_equal  : ∀key_type, rng_type. table key_type rng_type
     31                    → table key_type rng_type → bool.
    3332 
    34   tbl_mapi   : ∀a: Type[0]. (key_type → rng_type → a)
    35              → table key_type rng_type → table key_type a;
    36   tbl_map    : ∀a: Type[0]. (rng_type → a) → table key_type rng_type
    37              → table key_type a;
    38   tbl_fold   : ∀a: Type[0]. (key_type → a → a) → table key_type rng_type → a → a
    39 }.
     33axiom tbl_mapi   : ∀key_type, rng_type. ∀a: Type[0]. (key_type → rng_type → a)
     34                   → table key_type rng_type → table key_type a.
     35axiom tbl_map    : ∀key_type, rng_type. ∀a: Type[0]. (rng_type → a) → table key_type rng_type
     36                   → table key_type a.
     37axiom tbl_fold   : ∀key_type, rng_type. ∀a: Type[0]. (key_type → a → a) → table key_type rng_type → a → a.
    4038
    4139definition tbl_is_empty ≝
    4240  λkey_type : Type[0].
    4341  λrng_type : Type[0].
    44   λorder    : ordered key_type.
    45   λtable_adt: table_adt key_type rng_type order.
    46   λtable    : table … table_adt key_type rng_type.
     42  λtable    : table key_type rng_type.
    4743    tbl_size … table = 0.
    4844
     
    5046  λkey_type : Type[0].
    5147  λrng_type : Type[0].
    52   λorder    : ordered key_type.
    53   λtable_adt: table_adt key_type rng_type order.
    5448  λkey      : key_type.
    5549  λrng      : rng_type.
    56     tbl_insert … table_adt key rng (tbl_empty …).
     50    tbl_insert … key rng (tbl_empty …).
    5751
    5852definition tbl_from_list ≝
    5953  λkey_type : Type[0].
    6054  λrng_type : Type[0].
    61   λorder    : ordered key_type.
    62   λtable_adt: table_adt key_type rng_type order.
    6355  λthe_list : list (key_type × rng_type).
    6456    foldr … (λkey_rng.
    6557      let 〈key, rng〉 ≝ key_rng in
    66         tbl_insert … table_adt key rng) (tbl_empty …) the_list.
     58        tbl_insert … key rng) (tbl_empty …) the_list.
    6759
Note: See TracChangeset for help on using the changeset viewer.