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/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.
Note: See TracChangeset for help on using the changeset viewer.