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_identifier ?) r s with
  [ true ⇒ r :: s
  | false ⇒ s
  ].
  
definition rs_list_set_exists ≝
  λr: register.
  λs: list register.
    member ? (eq_identifier ?) r s.
    
definition rs_list_set_union ≝
  λr: list register.
  λs: list register.
    nub_by ? (eq_identifier ?) (r @ s).
  
definition rs_list_set_from_list ≝
  λr: list register.
    nub_by ? (eq_identifier ?) 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.