Module Rel

Require Import MoreRTL Util.
Require Import Sorting.Mergesort.
Require Kildall.
Require Liveness.
Import Utf8.
Import Coqlib Maps.
Import Registers RTL.

Module NodeOrder : Orders.TotalLeBool' with Definition t := node.
  Definition t := node.
  Definition leb x y :=
    match (x ?= y)%positive with
    | Eq | Gt => true
    | Lt => false
    end.
  Lemma leb_total x y : leb x y = true ∨ leb y x = true.

End NodeOrder.
Module Import NodeSort := Sort NodeOrder.

Definition list_of_set (n: node_set) : list node :=
  sort (List.map fst (PTree.elements n)).

Module RegOrder : Orders.TotalLeBool' with Definition t := reg.
  Definition t := reg.
  Definition leb := Pos.leb.
  Lemma leb_total x y : leb x y = true ∨ leb y x = true.

End RegOrder.
Module Import RegSort := Sort RegOrder.

Definition list_of_regset (s: Regset.t) : list reg :=
  sort (Regset.elements s).


Definition rel : Type :=
  list (reg * reg).

Fixpoint drop {A B} (a: list A) (b: list B) : list B :=
  match a, b with
  | _ :: a, _ :: b => drop a b
  | _, _ => b
  end.

Definition relate_regsets (x y: Regset.t) : rel :=
  let a := list_of_regset x in
  let b := list_of_regset y in
  fold_left2
    (λ r p q, (p, q) :: r)
    (λ r p, drop p r)
    (λ r q, drop q r)
    a
    b
    nil.

Definition guess (p q: RTL.function) : list ((node * node) * rel) * (node -> list node) * (node -> list node) :=
  let predMp := Kildall.make_predecessors p.(fn_code) RTL.successors_instr in
  let predMq := Kildall.make_predecessors q.(fn_code) RTL.successors_instr in
  let pred M pc := match M ! pc with Some x => x | None => nil end in
  let predp := pred predMp in
  let predq := pred predMq in
  let livep := Liveness.analyze p in
  let liveq := Liveness.analyze q in
  let get_live f P M :=
      match M with
      | None => (λ _, Regset.empty)
      | Some live =>
        λ pc,
        Liveness.transfer f pc (live !! pc)
      end
  in
  let bep := list_of_set (back_edges p.(fn_code)) in
  let beq := list_of_set (back_edges q.(fn_code)) in
  let res :=
    fold_left2
    (λ r pcp pcq,
     ((pcp, pcq), relate_regsets (get_live p predp livep pcp) (get_live q predq liveq pcq)) :: r
    )
    (λ _ _, nil)
    (λ _ _, nil)
    bep
    beq
    nil

  in (res, predp, predq).