Module KildallComp

Require Import Coqlib.
Require Import Iteration.
Require Import Maps.
Require Import Lattice.
Require Import Kildall.
Require Import Classical.

Section CORRECTNESS.

Lemma add_successors_correct2:
  forall tolist from pred n s,
    ~ (In n pred!!!s) -> (~In s tolist \/ n<>from) ->
    ~ In n (add_successors pred from tolist)!!!s.
          
Context {A: Type}.
Variable code: PTree.t A.
Variable successors: A -> list positive.

Definition make_preds : PTree.t (list positive) :=
  make_predecessors code successors.

Lemma make_predecessors_correct2_aux :
  forall n i s,
    code ! n = Some i ->
    ~In s (successors i) ->
    ~In n make_preds!!!s.

Lemma make_predecessors_correct2 :
  forall n i s,
    code ! n = Some i ->
    In n make_preds!!!s ->
    In s (successors i).

Lemma make_predecessors_some : forall s l,
  make_preds ! s = Some l ->
  forall p, In p l -> exists i, code ! p = Some i.

End CORRECTNESS.

Section Pred_Succs.

Lemma same_successors_same_predecessors_aux0 {A B} :
  forall f1 (f2:B->list positive) (m1:PTree.t A) t a,
 (forall i, m1! i = None) ->
  PTree.xfold
    (fun pred pc instr => add_successors pred pc (f1 instr)) a m1 t = t.

Lemma same_successors_same_predecessors_aux1 {A B} :
  forall f1 f2 (m1:PTree.t A) (m2:PTree.t B) t a,
 (forall i,
    (PTree.map1 f1 m1) ! i =
    (PTree.map1 f2 m2) ! i) ->
  PTree.xfold
    (fun pred pc instr => add_successors pred pc (f1 instr)) a m1 t =
  PTree.xfold
    (fun pred pc instr => add_successors pred pc (f2 instr)) a m2 t.

Lemma same_successors_same_predecessors {A B} : forall f1 f2 (m1:PTree.t A) (m2:PTree.t B),
 (forall i,
    (PTree.map1 f1 m1) ! i =
    (PTree.map1 f2 m2) ! i) ->
  make_predecessors m1 f1 = make_predecessors m2 f2.

End Pred_Succs.