Changeset 1075 for src/utilities/RegisterSet.ma
 Timestamp:
 Jul 18, 2011, 5:21:14 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/RegisterSet.ma
r782 r1075 6 6 rs_set: Type[0]; 7 7 rs_empty: rs_set; 8 rs_singleton: register → rs_set;9 rs_fold: ∀A: Type[0]. ( register → A → A) → rs_set → A → A;10 rs_insert: register → rs_set → rs_set;11 rs_exists: register → rs_set → bool;8 rs_singleton: Register → rs_set; 9 rs_fold: ∀A: Type[0]. (Register → A → A) → rs_set → A → A; 10 rs_insert: Register → rs_set → rs_set; 11 rs_exists: Register → rs_set → bool; 12 12 rs_union: rs_set → rs_set → rs_set; 13 rs_to_list: rs_set → list register;14 rs_from_list: list register → rs_set13 rs_to_list: rs_set → list Register; 14 rs_from_list: list Register → rs_set 15 15 }. 16 16 17 17 (* dpm: horrendously inefficient, but will do for now *) 18 18 19 definition rs_list_set_empty: list register ≝ [ ].19 definition rs_list_set_empty: list Register ≝ [ ]. 20 20 21 definition rs_list_set_singleton: register → list register ≝ λr. [ r ].21 definition rs_list_set_singleton: Register → list Register ≝ λr. [ r ]. 22 22 23 23 definition rs_list_set_fold ≝ 24 24 λA: Type[0]. 25 λf: register → A → A.26 λl: list register.25 λf: Register → A → A. 26 λl: list Register. 27 27 λa: A. 28 28 foldr ? ? f a l. 29 29 30 30 definition rs_list_set_insert ≝ 31 λr: register.32 λs: list register.33 match member ? (eq_identifier ?)r s with31 λr: Register. 32 λs: list Register. 33 match member ? eq_Register r s with 34 34 [ true ⇒ r :: s 35 35  false ⇒ s … … 37 37 38 38 definition rs_list_set_exists ≝ 39 λr: register.40 λs: list register.41 member ? (eq_identifier ?)r s.39 λr: Register. 40 λs: list Register. 41 member ? eq_Register r s. 42 42 43 43 definition rs_list_set_union ≝ 44 λr: list register.45 λs: list register.46 nub_by ? (eq_identifier ?)(r @ s).44 λr: list Register. 45 λs: list Register. 46 nub_by ? eq_Register (r @ s). 47 47 48 48 definition rs_list_set_from_list ≝ 49 λr: list register.50 nub_by ? (eq_identifier ?)r.49 λr: list Register. 50 nub_by ? eq_Register r. 51 51 52 52 definition register_list_set: register_set ≝ 53 mk_register_set (list register) rs_list_set_empty53 mk_register_set (list Register) rs_list_set_empty 54 54 rs_list_set_singleton rs_list_set_fold 55 55 rs_list_set_insert rs_list_set_exists
Note: See TracChangeset
for help on using the changeset viewer.