Changeset 1223 for src/utilities/adt
 Timestamp:
 Sep 16, 2011, 5:15:35 PM (9 years ago)
 Location:
 src/utilities/adt
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/adt/priority_set_adt.ma
r1218 r1223 4 4 include "common/Integers.ma". 5 5 6 include "utilities/adt/ordering.ma".7 6 include "ASM/Util.ma". 8 7 
src/utilities/adt/register_table.ma
r1211 r1223 1 1 include "ASM/I8051.ma". 2 2 include "common/Registers.ma". 3 include "utilities/adt/ordering.ma".4 3 include "utilities/adt/set_adt.ma". 5 4 6 5 definition vertex ≝ nat. (* XXX: int in o'caml *) 7 6 7 (* 8 8 axiom Register_ordered: ordered Register. 9 9 axiom register_ordered: ordered register. 10 10 axiom vertex_ordered: ordered vertex. 11 *) 11 12 12 13 axiom register_table: Type[0]. 13 14 14 15 axiom rt_empty : register_table. 16 17 axiom rt_insert: vertex → set Register → register_table → register_table. 15 18 16 19 axiom rt_forward : vertex → register_table → set Register. 
src/utilities/adt/set_adt.ma
r1218 r1223 3 3 include "arithmetics/nat.ma". 4 4 include "ASM/Util.ma". 5 6 include "utilities/adt/ordering.ma".7 5 8 6 axiom set: Type[0] → Type[0]. … … 13 11 axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type. 14 12 axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type. 15 axiom set_member: ∀elt_type. elt_type → set elt_type → bool.13 axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool. 16 14 axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool. 17 15 axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool. 18 16 axiom 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.20 17 axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a. 21 18 axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type → a → a. 19 axiom 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 *) 23 axiom set_diff: ∀elt_type: Type[0]. set elt_type → set elt_type → set elt_type. 22 24 23 25 definition set_is_empty ≝ … … 47 49 definition set_subset ≝ 48 50 λelt_type: Type[0]. 51 λeq : elt_type → elt_type → bool. 49 52 λleft : set elt_type. 50 53 λright : set elt_type. 51 set_forall elt_type (λelt. set_member elt_type e lt right) left.54 set_forall elt_type (λelt. set_member elt_type eq elt right) left. 52 55 53 56 definition set_subseteq ≝ 54 57 λelt_type: Type[0]. 58 λeq : elt_type → elt_type → bool. 55 59 λleft : set elt_type. 56 60 λright : set elt_type. 57 set_equal elt_type left right ∧ (set_subset elt_typeleft right).61 set_equal elt_type eq left right ∧ (set_subset elt_type eq left right). 58 62 59 63 definition set_union ≝ … … 65 69 definition set_intersection ≝ 66 70 λelt_type: Type[0]. 71 λeq : elt_type → elt_type → bool. 67 72 λleft : set elt_type. 68 73 λright : set elt_type. 69 set_filter elt_type (λelt. set_member elt_type e lt 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 3 3 include "utilities/adt/set_adt.ma". 4 4 include "utilities/adt/table_adt.ma". 5 include "utilities/adt/ordering.ma".6 5 7 6 axiom set_table: Type[0] → Type[0] → Type[0]. … … 22 21 → set_table key_type a > b > b. 23 22 axiom 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). 25 24 26 25 
src/utilities/adt/table_adt.ma
r1218 r1223 5 5 include "arithmetics/nat.ma". 6 6 7 include "utilities/adt/ordering.ma".8 7 include "utilities/adt/equal.ma". 9 8
Note: See TracChangeset
for help on using the changeset viewer.