Module SSAfastliveprecomputeRT

Require Import List. Import ListNotations.
Require Import Wellfounded.

Require Import Coqlib.
Require Import Maps.
Require Import Iteration.
Require Import Utils.

Require Import SSAfastliveutils.

Local Open Scope positive_scope.


Definition node: Type := positive.

Definition graph: Type := PTree.t (list node).

Local Notation map := PTree.t (only parsing).
Local Notation update := PTree.set (only parsing).
Local Notation remove := PTree.remove (only parsing).
Local Notation filter := PTree.filter (only parsing).
Local Notation itv := (positive * positive)%type (only parsing).
Local Notation set := (PTree.t unit) (only parsing).
Local Notation empty := (PTree.empty _) (only parsing).
Local Notation is_empty := PTree.bempty (only parsing).
Local Notation add := (fun u => PTree.set u tt) (only parsing).
Local Notation merge := ZSortWithIndex.merge (only parsing).
Local Notation union := (PTree.combine_union_strict option_union) (only parsing).
Definition is_directly_included r u v :=
  match r ! u with
  | None => false
  | Some i =>
    match r ! v with
    | None => false
    | Some i' => test_is_included i' i
    end
  end.
Notation is_cross_included := can_reach (only parsing).


Definition pre : Type := positive.
Definition post : Type := set * list (node * Z).
Record state : Type := mkstate {
  gr: graph;
  wrk: list (node * positive * list node * (set * list (node * Z)));
  next: positive;
  r : map itv;
  c : map set;
  t : map (list (node * Z));
  back : list (node * node)
}.

Definition init_state (g: graph) (root: node) :=
  match g!root with
  | Some succs =>
     {| gr := PTree.remove root g;
        wrk := (root, 1%positive, succs, (PTree.empty _, [])) :: nil;
        r := PTree.empty _;
        c := PTree.empty _;
        t := PTree.empty _;
        next := 2%positive;
        back := [] |}
  | None =>
     {| gr := g;
        wrk := nil;
        r := PTree.empty _;
        c := PTree.empty _;
        t := PTree.empty _;
        next := 1%positive;
        back := [] |}
  end.

Definition result : Type := map itv * map set * map (list (node * Z)) * list (node*node).
Definition transition (dom_pre : node -> Z) (s: state) : result + state :=
  match s.(wrk) with
  | [] => inl (s.(r), s.(c), s.(t), s.(back))
  | (u, n, [], (s_c, s_t)) :: wrk' =>
      let r' := update u (n, Pos.pred s.(next)) s.(r) in
      let s_c' := filter (fun v _ => negb (is_directly_included r' u v)) s_c in
      let s_c'' := add u s_c' in
      let c' := update u s_c'' s.(c) in
      let s_t' := List.filter (fun '(v, _) => negb (is_cross_included r' c' u v)) s_t in
      let t' := update u s_t' s.(t) in
      inr {| gr := s.(gr); wrk := wrk'; next := s.(next); r := r'; c := c'; t := t'; back := s.(back) |}
  | (u, n, v :: succs_u, (s_c, s_t)) :: wrk' =>
      match s.(gr) ! v with
      | None =>
          match s.(r) ! v with
          | None =>
            let s_t' := merge [(v, dom_pre v)] s_t in
            let back' := (u, v) :: s.(back) in
            inr {| gr := s.(gr);
                   wrk := (u, n, succs_u, (s_c, s_t')) :: wrk';
                   next := s.(next);
                   r := s.(r); c := s.(c); t := s.(t); back := back' |}
          | Some (m, _) =>
            let s_c' := match s.(c) ! v with | None => s_c | Some s => union s s_c end in
            let s_t' := match s.(t) ! v with | None => s_t | Some s => merge s s_t end in
            inr {| gr := s.(gr);
                   wrk := (u, n, succs_u, (s_c', s_t')) :: wrk';
                   next := s.(next);
                   r := s.(r); c := s.(c); t := s.(t); back := s.(back) |}
           end
      | Some succs_v =>
          inr {| gr := remove v s.(gr);
                 wrk := (v, s.(next), succs_v, (empty, [])) :: s.(wrk);
                 next := Pos.succ s.(next);
                 r := s.(r); c := s.(c); t := s.(t); back := s.(back) |}
      end
  end.

Section POSTORDER.


Fixpoint size_worklist (w: list (positive * pre * list positive * post)) : nat :=
  match w with
  | nil => 0%nat
  | (x, _, succs, _) :: w' => (S (List.length succs) + size_worklist w')%nat
  end.

Definition lt_state (s1 s2: state) : Prop :=
  lex_ord lt lt (PTree_Properties.cardinal s1.(gr), size_worklist s1.(wrk))
                (PTree_Properties.cardinal s2.(gr), size_worklist s2.(wrk)).

Lemma lt_state_wf: well_founded lt_state.

Lemma transition_decreases :
  forall itvm s s', transition itvm s = inr _ s' -> lt_state s' s.

End POSTORDER.

Definition precompute_r_t_up (g: graph) (root: node) (dom_pre : node -> Z) : result :=
  WfIter.iterate _ _ (transition dom_pre) lt_state lt_state_wf (transition_decreases dom_pre) (init_state g root).