include "ERTL/ERTL.ma".

definition statement_successors ≝
  λstmt: ertl_statement.
  match stmt with
  [ ertl_st_return _ ⇒ [ ]
  | ertl_st_skip l ⇒ [ l ]
  | ertl_st_comment comment l ⇒ [ l ]
  | ertl_st_cost cost l ⇒ [ l ]
  | ertl_st_set_hdw r1 r2 l ⇒ [ l ]
  | ertl_st_get_hdw r1 r2 l ⇒ [ l ]
  | ertl_st_hdw_to_hdw r1 r2 l ⇒ [ l ]
  | ertl_st_new_frame l ⇒ [ l ]
  | ertl_st_del_frame l ⇒ [ l ]
  | ertl_st_frame_size r l ⇒ [ l ]
  | ertl_st_push r l ⇒ [ l ]
  | ertl_st_pop r l ⇒ [ l ]
  | ertl_st_addr_h r l1 l2 ⇒ [ l2 ]
  | ertl_st_addr_l r l1 l2 ⇒ [ l2 ]
  | ertl_st_int r v l ⇒ [ l ]
  | ertl_st_move r1 r2 l ⇒ [ l ]
  | ertl_st_opaccs opaccs r1 r2 r3 l ⇒ [ l ]
  | ertl_st_op2 op2 r1 r2 r3 l ⇒ [ l ]
  | ertl_st_op1 op1 r1 r2 l ⇒ [ l ]
  | ertl_st_clear_carry l ⇒ [ l ]
  | ertl_st_load r1 r2 r3 l ⇒ [ l ]
  | ertl_st_store r1 r2 r3 l ⇒ [ l ]
  | ertl_st_call_id id v l ⇒ [ l ]
  | ertl_st_cond_acc _ l1 l2 ⇒ [ l1 ] @ [ l2 ]
  ]. 
  
(* dpm: this needs sorting out!  just what exactly is a register? *)

definition set_of_list ≝
  λn: nat.
  λl: list (BitVector n).
    foldr ? ? (set_insert ?) (set_empty ?) l.
    
definition dptr ≝
  set_insert ? (word_of_register RegisterDPL) (set_singleton ? (word_of_register RegisterDPH)).