# 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
```