Changeset 1210 for src/utilities/adt


Ignore:
Timestamp:
Sep 14, 2011, 4:04:53 PM (9 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/adt
Files:
2 added
3 edited

Legend:

Unmodified
Added
Removed
  • 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.