Theory Same_Register

section‹Same Register›
text‹The \texttt{same\_register} heuristic aims to replace registers which are used in the same way.›

theory Same_Register
  imports "../Inference"
begin

definition replace_with :: "iEFSM ⇒ nat ⇒ nat ⇒ iEFSM" where
  "replace_with e r1 r2 = (fimage (λ(u, tf, t). (u, tf,Transition.rename_regs (id(r1:=r2)) t)) e)"

fun merge_if_same :: "iEFSM ⇒ (transition_matrix ⇒ bool) ⇒ (nat × nat) list ⇒ iEFSM" where
  "merge_if_same e _ [] = e" |
  "merge_if_same e check ((r1, r2)#rs) = (
    let transitions = fimage (snd ∘ snd) e in
    if ∃(t1, t2) |∈| ffilter (λ(t1, t2). t1 < t2) (transitions |×| transitions).
      same_structure t1 t2 ∧ r1 ∈ enumerate_regs t1 ∧ r2 ∈ enumerate_regs t2
    then
      let newE = replace_with e r1 r2 in
      if check (tm newE) then
        merge_if_same newE check rs
      else
        merge_if_same e check rs
    else
      merge_if_same e check rs
  )"

definition merge_regs :: "iEFSM ⇒ (transition_matrix ⇒ bool) ⇒ iEFSM" where
  "merge_regs e check = (
    let
      regs = all_regs e;
      reg_pairs = sorted_list_of_set (Set.filter (λ(r1, r2). r1 < r2) (regs × regs))
    in
    merge_if_same e check reg_pairs
  )"

fun same_register :: update_modifier where
  "same_register t1ID t2ID s new _ old check = (
    let new' = merge_regs new check in
    if new' = new then None else Some new'
   )"

end