Set Implicit Arguments.
Require Import CFLib.
Require Import DFS_ml.
Require Import Stdlib.
Require Import LibListZ.
Require Import Array_proof.
Require Import List_proof.
Open Scope tag_scope.
Ltac auto_star ::= subst; intuition eauto with maths.



(********************************************************************)
(* ** TODO: Should be generated *)

Instance color__inhab : Inhab color_.
Proof. typeclass. Qed.




(********************************************************************)
(* ** TLC Graph without information on edges *)

Parameter graph : Type.
Parameter nodes : graph -> set int.
Parameter edges : graph -> set (int*int).

Parameter out_edges : graph -> int -> set int.

Definition has_edge (G:graph) x y :=
  (x,y) \in edges G.

Parameter has_edge_nodes : forall (G : graph) x y,
  has_edge G x y -> x \in nodes G /\ y \in nodes G.

Lemma has_edge_in_nodes_l : forall (G : graph) x y,
  has_edge G x y -> x \in nodes G.
Proof using. intros. forwards*: has_edge_nodes. Qed.

Lemma has_edge_in_nodes_r : forall (G : graph) x y,
  has_edge G x y -> y \in nodes G.
Proof using. intros. forwards*: has_edge_nodes. Qed.


Definition path := list (int*int).

Inductive is_path (G:graph) : int -> int -> path -> Prop :=
  | is_path_nil : forall x, 
      x \in nodes G ->
      is_path G x x nil
  | is_path_cons : forall x y z p,
     has_edge G x y ->
     is_path G y z p ->
     is_path G x z ((x,y)::p).

Definition reachable (G:graph) (i j:int) :=
  exists p, is_path G i j p.

Definition reachables (G:graph) (E F:set int) :=
  forall j, j \in F -> exists i, i \in E /\ reachable G i j.



(********************************************************************)
(* ** Facts *)

Implicit Types G : graph.
Implicit Types i j k : int.
Implicit Types p : path.
Implicit Types C : list color_.
Implicit Types R E F : set int.

Lemma reachable_edge : forall G i j,
  has_edge G i j -> 
  reachable G i j.
Proof using.
  skip.
Qed.
 
Lemma reachable_trans : forall G i j k,
  reachable G i j ->
  reachable G j k ->
  reachable G i k.
Proof using.
  skip.
Qed.

Lemma reachables_monotone : forall G E1 E2 F1 F2,
  reachables G E1 F1 ->
  E1 \c E2 ->
  F2 \c F1 ->
  reachables G E2 F2.
Proof using.
  introv R HE HF. rewrite incl_in_eq in HE,HF. skip.
Qed.
 
Lemma reachables_trans : forall G E1 E2 E3,
  reachables G E1 E2 ->
  reachables G E2 E3 ->
  reachables G E1 E3.
Proof using.
  skip.
Qed.


Definition no_black_to_while G C := 
  forall i j, 
  has_edge G i j -> 
  C[i] = Black ->
  C[j] <> White.
    (* i \in blacks C -> j \in (blacks C \u grays C). *)
    (* i \in blacks C -> j \in (blacks C) \/ j \in grays C). *)

Lemma black_to_white_path_goes_through_gray : forall G C,
  no_black_to_while G C ->
  forall i j p, 
  is_path G i j p -> 
  C[i] = Black -> (*i \in blacks C *)
  C[i] = White -> (*i \notin (blacks C \u grays C) *)
  exists i' j', Mem (i',j') p /\ C[i'] = Gray /\ C[j'] = White. 
    (* TODO: what exactly do we need about i' and j'? *)
Proof using.
  skip.
Qed.


(********************************************************************)
(* ** Graph representation predicate *)


(** [nodes_index G n] holds if the nodes in [G] are indexed from
    [0] inclusive to [n] exclusive. *)

Definition nodes_index (G:graph) (n:int) :=
  forall i, i \in nodes G = index n i.

(** [g ~> GraphAdj G] asserts that at pointer [g] is an imperative
    array of pure lists that represents the adjacency lists of [G]. *)

Definition GraphAdj (G:graph) (g:loc) :=
  Hexists N, g ~> Array N
   \* \[nodes_index G (LibListZ.length N) 
   /\ forall i j, i \in nodes G -> 
        Mem j (N[i]) = has_edge G i j].




(********************************************************************)
(* ** Generic hints *)

(** Hints for lists *)

Hint Constructors Forall.
Hint Resolve Forall_last.

(** Hints for indices *)

Lemma graph_adj_index : forall (G:graph) n m x,
  nodes_index G n -> x \in nodes G -> n = m -> index m x.
Proof. introv N Nx L. subst. rewrite~ <- N. Qed.

(*
Hint Resolve @index_array_length_eq @index_make @index_update.
Hint Immediate has_edge_in_nodes_l has_edge_in_nodes_r.
Hint Extern 1 (nodes_index _ _) => congruence.
Hint Extern 1 (index ?n ?x) =>
  eapply graph_adj_index; 
  [ try eassumption 
  | instantiate; try eassumption
  | instantiate; try congruence ].
*)
Hint Extern 1 (nodes_index _ _) => skip. (* TODO *)
Hint Extern 1 (index ?n ?x) => skip. (* TODO *)



(*************************************************************************)
(** Set of list predicate : TODO: move *)

Definition set_of_list A (L : list A) :=
  LibList.fold (monoid_ (union : _ -> _ -> set A) (\{}:set A)) (fun x => \{x}) L.

Section SetOfList.
Variables (A:Type).
Implicit Types l : list A.
Lemma set_of_list_nil : 
  set_of_list (@nil A) = \{}.
Proof using. auto. Qed.
Lemma set_of_list_cons : forall x l,
  set_of_list (x::l) = \{x} \u (set_of_list l).
Proof using. intros. unfold set_of_list. rewrite~ fold_cons. Qed.
Lemma set_of_list_last : forall x l,
  set_of_list (l&x) = (set_of_list l) \u \{x}.
Proof using. intros. unfold set_of_list. rewrite~ fold_last. skip. (* TODO *) Qed.

(*
Lemma fold_app : forall l1 l2,
  Monoid m ->
  fold m f (l1 ++ l2) = monoid_oper m (fold m f l1) (fold m f l2).
Proof using.
  unfold fold. intros. rewrite fold_right_app. gen l2.
  induction l1; intros.
  repeat rewrite fold_right_nil. rewrite~ monoid_neutral_l.
  repeat rewrite fold_right_cons. rewrite <- monoid_assoc. fequals.
Qed.
Lemma fold_last : forall x l,
  Monoid m ->
  fold m f (l & x) = monoid_oper m (fold m f l) (f x).
Proof using.
  intros. rewrite~ fold_app. rewrite fold_cons.
  rewrite fold_nil. rewrite monoid_neutral_r. auto.
Qed.
*)
End SetOfList.



(*************************************************************************)
(** Graph representation by adjacency lists *)

(* Import Graph_ml. *)

Lemma nb_nodes_spec : forall (G:graph) g,
  app Graph_ml.nb_nodes [g]
    PRE (g ~> GraphAdj G) 
    POST (fun n => \[nodes_index G n]).
Proof using.
  xcf. xunfold GraphAdj. xpull ;=> N (HN1&HN2).
  xapp. xsimpl*.
Qed.

Hint Extern 1 (RegisterSpec Graph_ml.nb_nodes) => Provide nb_nodes_spec.

Lemma iter_edges_spec : forall (I:set int->hprop) (G:graph) g f i,
  i \in nodes G ->
  (forall j js, j \notin js -> has_edge G i j -> 
     (app f [j] (I js) (# I (\{j} \u js)))) -> 
  app Graph_ml.iter_edges [f g i]
    PRE (g ~> GraphAdj G \* I \{}) 
    POST (# g ~> GraphAdj G \* I (out_edges G i)).
Proof.
  introv Gi Sf. xcf. xunfold GraphAdj. xpull ;=> N (GI&GN).
  xapps~. xfun. xapp (fun (L:list int) => I (set_of_list L)).
  { introv EN. rewrite set_of_list_last. xapp. xapp.
    { skip. (* needs no duplicate *) }
    { rewrite~ <- GN. rewrite EN. skip. (* mem *) }
    { xsimpl. }
    { rewrite union_comm. xsimpl. } }
  { xsimpl.
    { skip. (* set_of_list // out_edges *) }
    { split~. } }
Qed. 
   
Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec.




(*************************************************************************)
(** DFS *)

(* TODO / FIX
Open Scope set_scope.
Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
 (at level 0, x ident, A at level 0, P at level 200) : set_scope.
*)

Definition blacks C :=
  set_st (fun i:int => index C i /\ C[i] = Black).
  (* \set{ i:int | index C i /\ C[i] = Black }. *)

Definition grays C :=
  set_st (fun i:int => index C i /\ C[i] = Gray).


Definition inv G R C :=
     length C = card (nodes G)
  /\ R \c nodes G
  /\ no_black_to_while G C
  /\ reachables G (R \u blacks C) (blacks C).

Definition hinv G R C g c :=
     g ~> GraphAdj G 
  \* c ~> Array C
  \* \[ inv G R C ].

Lemma dfs_from_spec : forall G R C g c i,
  C[i] = White ->
  app dfs_from [g c i]
    PRE (hinv G R C g c) 
    POST (# Hexists C', hinv G R C' g c
       \* \[ C'[i] = Black
          /\ (blacks C) \c (blacks C') ]).
Proof using.
  xcf. skip.
Qed.

Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec.

Lemma dfs_main_spec : forall (G:graph) g (r:list int),
  app dfs_main [g r] 
    PRE (g ~> GraphAdj G) 
    POST (fun c => Hexists C,
      c ~> Array C \* 
      g ~> GraphAdj G \*
      \[ reachables G (set_of_list r) (blacks C) ]).
Proof using.  
  xcf. skip. (* xunfold GraphAdj at 1. xpull ;=> HI. *)
  
Qed.

Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.