Changeset 1223 for src/utilities/adt


Ignore:
Timestamp:
Sep 16, 2011, 5:15:35 PM (9 years ago)
Author:
mulligan
Message:

changes

Location:
src/utilities/adt
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/adt/priority_set_adt.ma

    r1218 r1223  
    44include "common/Integers.ma".
    55
    6 include "utilities/adt/ordering.ma".
    76include "ASM/Util.ma".
    87
  • src/utilities/adt/register_table.ma

    r1211 r1223  
    11include "ASM/I8051.ma".
    22include "common/Registers.ma".
    3 include "utilities/adt/ordering.ma".
    43include "utilities/adt/set_adt.ma".
    54
    65definition vertex ≝ nat. (* XXX: int in o'caml *)
    76
     7(*
    88axiom Register_ordered: ordered Register.
    99axiom register_ordered: ordered register.
    1010axiom vertex_ordered: ordered vertex.
     11*)
    1112
    1213axiom register_table: Type[0].
    1314 
    1415axiom rt_empty : register_table.
     16
     17axiom rt_insert: vertex → set Register → register_table → register_table.
    1518 
    1619axiom rt_forward : vertex → register_table → set Register.
  • src/utilities/adt/set_adt.ma

    r1218 r1223  
    33include "arithmetics/nat.ma".
    44include "ASM/Util.ma".
    5 
    6 include "utilities/adt/ordering.ma".
    75
    86axiom set: Type[0] → Type[0].
     
    1311axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type.
    1412axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type.
    15 axiom set_member: ∀elt_type. elt_type → set elt_type → bool.
     13axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool.
    1614axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool.
    1715axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool.
    1816axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type.
    19 axiom set_equal: ∀elt_type. set elt_type → set elt_type → bool.
    2017axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a.
    2118axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type  → a → a.
     19axiom set_equal: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
     20  set elt_type → set elt_type → bool.
     21
     22(* XXX: define in terms of primitives *)
     23axiom set_diff: ∀elt_type: Type[0]. set elt_type → set elt_type → set elt_type.
    2224
    2325definition set_is_empty ≝
     
    4749definition set_subset ≝
    4850  λelt_type: Type[0].
     51  λeq      : elt_type → elt_type → bool.
    4952  λleft    : set elt_type.
    5053  λright   : set elt_type.
    51     set_forall elt_type (λelt. set_member elt_type elt right) left.
     54    set_forall elt_type (λelt. set_member elt_type eq elt right) left.
    5255
    5356definition set_subseteq ≝
    5457  λelt_type: Type[0].
     58  λeq      : elt_type → elt_type → bool.
    5559  λleft    : set elt_type.
    5660  λright   : set elt_type.
    57     set_equal elt_type left right ∧ (set_subset elt_type left right).
     61    set_equal elt_type eq left right ∧ (set_subset elt_type eq left right).
    5862
    5963definition set_union ≝
     
    6569definition set_intersection ≝
    6670  λelt_type: Type[0].
     71  λeq      : elt_type → elt_type → bool.
    6772  λleft    : set elt_type.
    6873  λright   : set elt_type.
    69     set_filter elt_type (λelt. set_member elt_type elt right) left.
     74    set_filter elt_type (λelt. set_member elt_type eq elt right) left.
  • src/utilities/adt/set_table_adt.ma

    r1218 r1223  
    33include "utilities/adt/set_adt.ma".
    44include "utilities/adt/table_adt.ma".
    5 include "utilities/adt/ordering.ma".
    65
    76axiom set_table: Type[0] → Type[0] → Type[0].
     
    2221                      → set_table key_type a -> b -> b.
    2322axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
    24                       (key_type → a → bool) → option (key_type × a).
     23                      ((key_type × a) → bool) → option (key_type × a).
    2524
    2625
  • src/utilities/adt/table_adt.ma

    r1218 r1223  
    55include "arithmetics/nat.ma".
    66
    7 include "utilities/adt/ordering.ma".
    87include "utilities/adt/equal.ma".
    98
Note: See TracChangeset for help on using the changeset viewer.