include "ASM/I8051.ma".
include "common/Registers.ma".

record register_set: Type[1] ≝
{
  rs_set: Type[0];
  rs_empty: rs_set;
  rs_singleton: Register → rs_set;
  rs_fold: ∀A: Type[0]. (Register → A → A) → rs_set → A → A;
  rs_insert: Register → rs_set → rs_set;
  rs_exists: Register → rs_set → bool;
  rs_union: rs_set → rs_set → rs_set;
  rs_to_list: rs_set → list Register;
  rs_from_list: list Register → rs_set
}.

(* dpm: horrendously inefficient, but will do for now *)

definition rs_list_set_empty: list Register ≝ [ ].

definition rs_list_set_singleton: Register → list Register ≝ λr. [ r ].

definition rs_list_set_fold ≝
  λA: Type[0].
  λf: Register → A → A.
  λl: list Register.
  λa: A.
    foldr ? ? f a l.
    
definition rs_list_set_insert ≝
  λr: Register.
  λs: list Register.
  match member ? eq_Register r s with
  [ true ⇒ r :: s
  | false ⇒ s
  ].
  
definition rs_list_set_exists ≝
  λr: Register.
  λs: list Register.
    member ? eq_Register r s.
    
definition rs_list_set_union ≝
  λr: list Register.
  λs: list Register.
    nub_by ? eq_Register (r @ s).
  
definition rs_list_set_from_list ≝
  λr: list Register.
    nub_by ? eq_Register r.
  
definition register_list_set: register_set ≝
  mk_register_set (list Register) rs_list_set_empty
                  rs_list_set_singleton rs_list_set_fold
                  rs_list_set_insert rs_list_set_exists
                  rs_list_set_union
                  (λx. x) rs_list_set_from_list.