include "ASM/Util.ma".
include "ERTL/ERTL.ma".

definition list_set_union ≝
  λA: Type[0].
  λeq_a: A → A → bool.
  λl: list A.
  λr: list A.
    nub_by A eq_a (l @ r).

definition list_set_add ≝
  λA: Type[0].
  λeq_a: A → A → bool.
  λa: A.
  λs: list A.
    nub_by A eq_a (a :: s).

definition list_set_diff ≝
  λA: Type[0].
  λeq_a: A → A → bool.
  λl: list A.
  λr: list A.
    filter A (λx. member A eq_a x r) l.

definition list_set_equal ≝
  λA: Type[0].
  λeq_a: A → A → bool.
  λl: list A.
  λr: list A.
    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).

definition list_set_member ≝ member.

definition list_set_fold ≝ foldr.

definition statement_successors ≝
  λs: ertl_statement.
  match s with
  [ ertl_st_return ⇒ [ ]
  | ertl_st_skip l ⇒ [ l ]
  | ertl_st_comment c l ⇒ [ l ]
  | ertl_st_cost c l ⇒ [ l ]
  | ertl_st_set_hdw _ _ l ⇒ [ l ]
  | ertl_st_get_hdw _ _ l ⇒ [ l ]
  | ertl_st_hdw_to_hdw _ _ l ⇒ [ l ]
  | ertl_st_new_frame l ⇒ [ l ]
  | ertl_st_del_frame l ⇒ [ l ]
  | ertl_st_frame_size _ l ⇒ [ l ]
  | ertl_st_push _ l ⇒ [ l ]
  | ertl_st_pop _ l ⇒ [ l ]
  | ertl_st_addr _ _ _ l ⇒ [ l ]
  | ertl_st_int _ _ l ⇒ [ l ]
  | ertl_st_move _ _ l ⇒ [ l ]
  | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
  | ertl_st_op1 _ _ _ l ⇒ [ l ]
  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
  | ertl_st_clear_carry l ⇒ [ l ]
  | ertl_st_set_carry l ⇒ [ l ]
  | ertl_st_load _ _ _ l ⇒ [ l ]
  | ertl_st_store _ _ _ l ⇒ [ l ]
  | ertl_st_call_id _ _ l ⇒ [ l ]
  | ertl_st_cond _ l1 l2 ⇒
      list_set_add ? (eq_identifier ?) l1 [ l2 ]
  ].

definition register_lattice ≝ (list register) × (list Register).
definition lattice_property ≝ register_lattice.
definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
definition lattice_psingleton: register → register_lattice ≝
  λr.
    〈[ r ], [ ]〉.
definition lattice_hsingleton: Register → register_lattice ≝
  λr.
    〈[ ], [ r ]〉.

definition lattice_join: register_lattice → register_lattice → register_lattice ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.

definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.

definition lattice_equal: register_lattice → register_lattice → bool ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).

definition lattice_is_maximal: register_lattice → bool ≝ λl. false.

record lattice_property_sig: Type[1] ≝
{
  lp_type      : Type[0];
  lp_property  : Type[0];
  lp_bottom    : lp_type;
  lp_psingleton: register → lp_type;
  lp_hsingleton: Register → lp_type;
  lp_join      : lp_type → lp_type → lp_type;
  lp_diff      : lp_type → lp_type → lp_type;
  lp_equal     : lp_type → lp_type → bool;
  lp_is_maximal: lp_type → bool
}.

definition property ≝
  mk_lattice_property_sig
    ((list register) × (list Register))
    lattice_property
    lattice_bottom
    lattice_psingleton
    lattice_hsingleton
    lattice_join
    lattice_diff
    lattice_equal
    lattice_is_maximal.

definition defined: ertl_statement → register_lattice ≝
  λs.
  match s with
  [ ertl_st_skip _ ⇒ lattice_bottom
  | ertl_st_comment _ _ ⇒ lattice_bottom
  | ertl_st_cost _ _ ⇒ lattice_bottom
  | ertl_st_push _ _⇒ lattice_bottom
  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
  | ertl_st_cond _ _ _ ⇒ lattice_bottom
  | ertl_st_return ⇒ lattice_bottom
  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
  | ertl_st_op2 op2 r _ _ _ ⇒
    match op2 with
    [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    | _ ⇒ lattice_psingleton r
    ]
  | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
  | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
  | ertl_st_frame_size r _ ⇒ lattice_psingleton r
  | ertl_st_pop r _ ⇒ lattice_psingleton r
  | ertl_st_int r _ _ ⇒ lattice_psingleton r
  | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
  | ertl_st_move r _ _ ⇒ lattice_psingleton r
  (* XXX: change from o'caml *)
  | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
  | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
  (* Potentially destroys all caller-save hardware registers. *)
  | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
  ].

definition list_set_of_list ≝
  λrl.
    foldr ? ? (list_set_add Register eq_Register) rl [ ].

definition list_set_of_list2 ≝
  let f ≝ λset. λr. list_set_add Register eq_Register r set in
    foldl ? ? f [ ].

definition ret_regs ≝ list_set_of_list RegisterRets.

definition used: ertl_statement → register_lattice ≝
  λstmt.
  match stmt with
  [ ertl_st_skip _ ⇒ lattice_bottom
  | ertl_st_cost _ _ ⇒ lattice_bottom
  | ertl_st_comment _ _ ⇒ lattice_bottom
  | ertl_st_frame_size _ _ ⇒ lattice_bottom
  | ertl_st_pop _ _ ⇒ lattice_bottom
  | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
  | ertl_st_int _ _ _ ⇒ lattice_bottom
  | ertl_st_clear_carry _ ⇒ lattice_bottom
  | ertl_st_set_carry _ ⇒ lattice_bottom
    (* Reads the hardware registers that are used to pass parameters. *)
  | ertl_st_call_id _ nparams _ ⇒
    〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
  | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
  | ertl_st_push r _ ⇒ lattice_psingleton r
  | ertl_st_move _ r _ ⇒ lattice_psingleton r
  | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
  | ertl_st_cond r _ _ ⇒ lattice_psingleton r
  | ertl_st_op2 op2 _ r1 r2 _ ⇒
    match op2 with
    [ Addc ⇒
      lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    ]
  | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
  | ertl_st_store r1 r2 r3 _ ⇒
    lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
  | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
  ].

definition eliminable: register_lattice → ertl_statement → option label ≝
  λl.
  λstmt.
  let 〈pliveafter, hliveafter〉 ≝ l in
  match stmt with
  [ ertl_st_skip _ ⇒ None ?
  | ertl_st_comment _ _ ⇒ None ?
  | ertl_st_cost _ _ ⇒ None ?
  | ertl_st_new_frame _ ⇒ None ?
  | ertl_st_del_frame _ ⇒ None ?
  | ertl_st_pop _ _ ⇒ None ?
  | ertl_st_push _ _ ⇒ None ?
  | ertl_st_clear_carry _  ⇒ None ?
  | ertl_st_set_carry _  ⇒ None ?
  | ertl_st_store _ _ _ _ ⇒ None ?
  | ertl_st_call_id _ _ _ ⇒ None ?
  | ertl_st_cond _ _ _ ⇒ None ?
  | ertl_st_return ⇒ None ?
  | ertl_st_get_hdw r _ l ⇒
    if list_set_member register (eq_identifier ?) r pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_frame_size r l ⇒
    if list_set_member register (eq_identifier ?) r pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_int r _ l ⇒
    if list_set_member register (eq_identifier ?) r pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_addr r1 r2 _ l ⇒
    if list_set_member register (eq_identifier ?) r1 pliveafter ∨
       list_set_member register (eq_identifier ?) r2 pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_move r _ l ⇒
    if list_set_member register (eq_identifier ?) r pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_opaccs _ d1 d2 _ _ l ⇒
    if list_set_member register (eq_identifier ?) d1 pliveafter ∨
       list_set_member register (eq_identifier ?) d2 pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_op1 _ r _ l ⇒
    if list_set_member register (eq_identifier ?) r pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_op2 _ r _ _ l ⇒
    if list_set_member register (eq_identifier ?) r pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_load r _ _ l ⇒
    if list_set_member register (eq_identifier ?) r pliveafter ∨
       list_set_member Register eq_Register RegisterCarry hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_set_hdw r _ l ⇒
    if list_set_member Register eq_Register r hliveafter then
      None ?
    else
      Some ? l
  | ertl_st_hdw_to_hdw r _ l ⇒
    if list_set_member Register eq_Register r hliveafter then
      None ?
    else
      Some ? l
  ].

definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
  λstmt.
  λliveafter.
  match eliminable liveafter stmt with
  [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
  | Some l ⇒ liveafter
  ].

definition valuation ≝ label → register_lattice.
definition rhs ≝ valuation → lattice_property.
definition equations ≝ label → rhs.

axiom fix_lfp: equations → valuation.

definition livebefore ≝
  λint_fun.
  λlabel.
  λliveafter: valuation.
  match lookup ? ? (ertl_if_graph int_fun) label with
  [ None      ⇒ ?
  | Some stmt ⇒ statement_semantics stmt (liveafter label)
  ].
  cases not_implemented (* XXX *)
qed.

definition liveafter ≝
  λint_fun.
  λlivebefore.
  λlabel.
  λliveafter: valuation.
  match lookup ? ? (ertl_if_graph int_fun) label with
  [ None      ⇒ ?
  | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
      lattice_join (livebefore successor liveafter) accu)
      lattice_bottom (statement_successors stmt)
  ].
  cases not_implemented (* XXX *)
qed.

definition analyse: ertl_internal_function → valuation ≝
  λint_fun.
    fix_lfp (liveafter int_fun (livebefore int_fun)).