Module SSAfastliveprecomputeTT

Require Import List. Import ListNotations.

Require Import Coqlib.
Require Import Maps.
Require Import Time.

Require Import SSAfastliveutils.
Require Import SSAfastliveprecomputeRT.

Local Open Scope string_scope.

Definition precompute_t_from_t_up_1
   (dom_pre : node -> Z) pre (t : PTree.t (list (node * Z))) (back : list (node * node))
  : PTree.t (list (node * Z)) :=

  let back_targets := List.map snd back in
  let back_targets := PosSortWithIndex.sort pre back_targets in
  List.fold_left (fun (t : PTree.t (list (node * Z))) (u : node) =>
    let s :=
      match t ! u with
      | None => [(u, dom_pre u)]
      | Some s =>
        let s := List.fold_left (fun acc '((u, _) : node * Z) =>
          match t ! u with
          | None => acc
          | Some s => ZSortWithIndex.merge s acc
          end) s []
        in
        ZSortWithIndex.merge [(u, dom_pre u)] s
      end
    in
    PTree.set u s t
  ) back_targets t.

Definition precompute_t_from_t_up_2
  (dom_pre : node -> Z) (t : PTree.t (list (node * Z))) : PTree.t (list node) :=

  PTree.map (fun (u : node) (s : list (node * Z)) =>
    let s :=
      List.fold_left (fun acc '((v, _) : node * Z) =>
        match t ! v with
        | None => acc
        | Some s => ZSortWithIndex.merge s acc
        end) s []
    in
    let s := ZSortWithIndex.merge [(u, dom_pre u)] s in
    List.map fst s
  ) t.

Definition precompute_t_from_t_up dom_pre pre t back :=
  let t := time (Some "precompute_t_from_t_up ") "precompute_t_from_t_up_1 " (fun _ => precompute_t_from_t_up_1 dom_pre pre t back) tt in
  let t := time (Some "precompute_t_from_t_up ") "precompute_t_from_t_up_2 " (fun _ => precompute_t_from_t_up_2 dom_pre t) tt in
  t.