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

File:
1 edited

Legend:

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