Module AcyGraph

From Coq Require Import String.
From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

From Coq Require Import RelationClasses.
Import Coq.Relations.Relation_Operators.
From Coq Require Import Arith.Arith.
From Coq Require Import Setoid.

From Velus Require Import Common.
From Velus Require Import Environment.

Vertices and arcs

Definition V_set : Type := PS.t.

Definition A_set : Type := Env.t PS.t.

Definition empty_arc_set : A_set := Env.empty _.

Definition has_arc (a : A_set) (x y : ident) :=
  exists s, Env.MapsTo x s a /\ PS.In y s.

Definition has_arcb (a : A_set) (x y : ident) :=
  match (Env.find x a) with
  | Some s => PS.mem y s
  | None => false
  end.

Lemma has_arcb_spec : forall a x y,
    has_arcb a x y = true <-> has_arc a x y.

Lemma nhas_arc_empty : forall x y,
    ~has_arc empty_arc_set x y.

Definition add_arc (x y : ident) (a : A_set) :=
  match (Env.find x a) with
  | Some s => Env.add x (PS.add y s) a
  | None => Env.add x (PS.singleton y) a
  end.

Lemma add_arc_spec : forall a x y x' y',
    has_arc (add_arc x y a) x' y' <->
    has_arc a x' y' \/
    (x = x' /\ y = y').

Definition has_trans_arc a := clos_trans_n1 _ (has_arc a).

Global Hint Constructors clos_trans_n1 : acygraph.
Global Hint Unfold has_trans_arc : acygraph.

Global Instance has_trans_arc_Transitive : forall a,
    Transitive (has_trans_arc a).

Lemma nhas_trans_arc_empty : forall x y,
    ~has_trans_arc empty_arc_set x y.

Fact add_arc_has_trans_arc1 : forall a x y,
    has_trans_arc (add_arc x y a) x y.

Fact add_arc_has_trans_arc2 : forall a x y x' y',
    has_trans_arc a x' y' ->
    has_trans_arc (add_arc x y a) x' y'.
Global Hint Resolve add_arc_has_trans_arc1 add_arc_has_trans_arc2 : acygraph.

Lemma add_arc_spec2 : forall a x y x' y',
    has_trans_arc (add_arc x y a) x' y' <->
    has_trans_arc a x' y' \/
    (x = x' /\ y = y') \/
    (x = x' /\ has_trans_arc a y y') \/
    (has_trans_arc a x' x /\ y = y') \/
    (has_trans_arc a x' x /\ has_trans_arc a y y').

Acyclic graph

Inductive AcyGraph : V_set -> A_set -> Prop :=
| AGempty : AcyGraph PS.empty empty_arc_set
| AGaddv : forall v a x,
    AcyGraph v a ->
    AcyGraph (PS.add x v) a
| AGadda : forall v a x y,
    AcyGraph v a ->
    x <> y ->
    PS.In x v ->
    PS.In y v ->
    ~has_trans_arc a y x ->
    AcyGraph v (add_arc x y a).
Global Hint Constructors AcyGraph : acygraph.

Definition vertices {v a} (g : AcyGraph v a) : V_set := v.
Definition arcs {v a} (g : AcyGraph v a) : A_set := a.

Definition is_vertex {v a} (g : AcyGraph v a) (x : ident) : Prop :=
  PS.In x v.

Definition is_arc {v a} (g : AcyGraph v a) x y : Prop :=
  has_arc a x y.

Lemma nis_arc_Gempty : forall x y,
  ~is_arc AGempty x y.

Definition is_trans_arc {v a} (g : AcyGraph v a) x y : Prop :=
  has_trans_arc a x y.

Lemma nis_trans_arc_Gempty : forall x y,
    ~is_trans_arc AGempty x y.

Major properties of is_arc : transitivity, irreflexivity, asymmetry

Global Instance is_trans_arc_Transitive {v a} (g : AcyGraph v a) :
    Transitive (is_trans_arc g).

Lemma has_arc_irrefl : forall v a,
    AcyGraph v a ->
    Irreflexive (has_arc a).

Global Instance is_arc_Irreflexive {v a} (g : AcyGraph v a) :
    Irreflexive (is_arc g).

Global Instance is_trans_arc_Asymmetric {v a} (g : AcyGraph v a) :
    Asymmetric (is_trans_arc g).

Global Instance is_trans_arc_Irreflexive {v a} (g : AcyGraph v a) :
  Irreflexive (is_trans_arc g).

Lemma is_arc_is_vertex : forall {v a} (g : AcyGraph v a) x y,
    is_arc g x y ->
    is_vertex g x /\ is_vertex g y.

Corollary is_trans_arc_is_vertex : forall {v a} (g : AcyGraph v a) x y,
    is_trans_arc g x y ->
    is_vertex g x /\ is_vertex g y.

Lemma is_trans_arc_neq : forall {v a} (g : AcyGraph v a) x y,
    is_trans_arc g x y ->
    x <> y.

Local Ltac destruct_conj_disj :=
    match goal with
    | H : _ /\ _ |- _ => destruct H
    | H : _ \/ _ |- _ => destruct H
    end; subst.

Lemma is_trans_arc_dec : forall {v a} (g : AcyGraph v a),
    forall x y, (is_trans_arc g x y) \/ (~ is_trans_arc g x y).

Building an acyclic graph

From compcert Require Import common.Errors.

Definition add_after (preds : PS.t) (x : ident) (a : A_set) : A_set :=
  PS.fold (fun p a => add_arc p x a) preds a.

Lemma add_after_spec : forall a preds y x' y',
    has_arc (add_after preds y a) x' y' <->
    has_arc a x' y' \/
    (PS.In x' preds /\ y = y').

Corollary add_after_has_arc1 : forall a x y x' preds,
    has_arc a x y ->
    has_arc (add_after preds x' a) x y.

Corollary add_after_has_arc2 : forall a x y preds,
    PS.In y preds ->
    has_arc (add_after preds x a) y x.

Lemma add_after_AcyGraph : forall v a x preds,
    PS.In x v ->
    ~PS.In x preds ->
    PS.For_all (fun x => PS.In x v) preds ->
    PS.For_all (fun p => ~has_trans_arc a x p) preds ->
    AcyGraph v a ->
    AcyGraph v (add_after preds x a) /\
    PS.For_all (fun p => ~has_trans_arc (add_after preds x a) x p) preds.

Definition acgraph_of_graph g v a :=
  (forall x, Env.In x g <-> PS.In x v) /\
  (forall x y, (exists xs, Env.find y g = Some xs /\ In x xs) -> has_arc a x y).

Section Dfs.

  Variable graph : Env.t (list positive).

  Definition dfs_state := { p | forall x, PS.In x p -> Env.In x graph }.
  Definition proj1_dfs_state (s : dfs_state) := proj1_sig s.
  Coercion proj1_dfs_state : dfs_state >-> PS.t.
  Extraction Inline proj1_dfs_state.

  Program Definition empty_dfs_state : dfs_state :=
    exist _ PS.empty _.
  Extraction Inline empty_dfs_state.

  Lemma cardinals_in_progress_le_graph:
    forall (a : dfs_state),
      PS.cardinal a <= Env.cardinal graph.

  Definition num_remaining (s : dfs_state) : nat :=
    Env.cardinal graph - PS.cardinal s.

  Definition deeper : dfs_state -> dfs_state -> Prop :=
    ltof _ num_remaining.

  Lemma add_deeper:
    forall x (s : dfs_state) P,
      ~ PS.In x s ->
      deeper (exist _ (PS.add x s) P) s.

  Definition visited (p : PS.t) (v : PS.t) : Prop :=
    (forall x, PS.In x p -> ~PS.In x v)
    /\ exists a, AcyGraph v a
           /\ (forall x, PS.In x v ->
                   exists zs, Env.find x graph = Some zs
                         /\ (forall y, In y zs -> has_arc a y x)).

  Definition none_visited : { v | visited PS.empty v }.
  Extraction Inline none_visited.

  Definition pre_visited_add:
    forall {inp} x
      (v : { v | visited inp v }),
      ~PS.In x (proj1_sig v) ->
      { v' | visited (PS.add x inp) v' & v' = (proj1_sig v) }.
  Extraction Inline pre_visited_add.

  Fact fold_dfs_props : forall zs p (v: {v | visited p v}) v'
      (dfs : forall (x : positive) (v : {v | visited p v}), res {v' | visited p v' & In_ps [x] v' /\ PS.Subset (proj1_sig v) v'}),
      fold_left (fun v w => Errors.bind v (fun v => Errors.bind (dfs w v) (fun v' => OK (sig_of_sig2 v')))) zs (OK v) = OK v' ->
      In_ps zs (proj1_sig v') /\ PS.Subset (proj1_sig v) (proj1_sig v').

  Section msg_of.
    Variable msgs : Env.t errmsg.

    Definition msg_of_label (x : ident) :=
      match Env.find x msgs with
      | Some msg => msg
      | None => msg "?"
      end.

    Fixpoint msg_of_cycle' (stop: ident) (s : list ident) :=
      match s with
      | [] => []
      | x::tl =>
          if ident_eq_dec x stop then msg_of_label x
          else (msg_of_label x ++ MSG " -> " :: msg_of_cycle' stop tl)
      end.
    Definition msg_of_cycle (s : list ident) :=
      match s with
      | [] => []
      | x::tl => msg_of_label x ++ MSG " -> " :: msg_of_cycle' x tl
      end.
  End msg_of.

  Variable get_msgs : unit -> Env.t errmsg.

  Program Fixpoint dfs' (s : dfs_state) (stack : list positive) (x : positive) (v : { v | visited s v })
    {measure (num_remaining s)} :
    res { v' | visited s v' & In_ps [x] v' /\ PS.Subset (proj1_sig v) v' } :=
      match PS.mem x s with
      | true => Error (MSG "dependency cycle : " :: msg_of_cycle (get_msgs tt) stack)
      | false =>
          match PS.mem x (proj1_sig v) with
          | true => OK (sig2_of_sig v _)
          | false =>
              match (Env.find x graph) with
              | None => Error (CTX x :: msg " not found")
              | Some zs =>
                  let s' := exist _ (PS.add x s) _ in
                  match fold_left (fun v w => Errors.bind v (fun v => Errors.bind (dfs' s' (w::stack) w v) (fun v' => OK (sig_of_sig2 v')))) zs (OK v) with
                  | Error msg => Error msg
                  | OK (exist _ v' (conj P1 _)) => OK (exist2 _ _ (PS.add x v') _ _)
                  end
              end
          end
      end.

  Definition dfs
    : forall x (v : { v | visited PS.empty v }),
      res { v' | visited PS.empty v' &
                    (In_ps [x] v'
                     /\ PS.Subset (proj1_sig v) v') }
    := fun x => dfs' empty_dfs_state [x] x.

End Dfs.

Program Definition build_acyclic_graph (graph : Env.t (list positive)) (get_msgs : unit -> Env.t errmsg) : res PS.t :=
  bind (Env.fold (fun x _ vo =>
                    bind vo
                         (fun v => match dfs graph get_msgs x v with
                                | Error msg => Error msg
                                | OK v => OK (sig_of_sig2 v)
                                end))
                         graph (OK (none_visited graph)))
                 (fun v => OK _).

Lemma build_acyclic_graph_spec : forall graph msgs v,
    build_acyclic_graph graph msgs = OK v ->
    exists a, acgraph_of_graph graph v a /\ AcyGraph v a.

Extracting a prefix

Definition TopoOrder {v a} (g : AcyGraph v a) (xs : list ident) :=
  Forall' (fun xs x => ~In x xs
                    /\ is_vertex g x
                    /\ (forall y, is_trans_arc g y x -> In y xs)) xs.

Definition TopoOrder' {v a} (g : AcyGraph v a) (xs : list ident) :=
  Forall' (fun xs x => ~In x xs
                    /\ is_vertex g x
                    /\ (forall y, is_arc g y x -> In y xs)) xs.
Global Hint Unfold TopoOrder : acygraph.

Lemma TopoOrder_weaken : forall {v a} (g : AcyGraph v a) xs,
    TopoOrder g xs ->
    Forall (fun x => forall y, is_trans_arc g y x -> In y xs) xs.

Lemma TopoOrder_equiv {v a} (g : AcyGraph v a) : forall xs,
    TopoOrder g xs <-> TopoOrder' g xs.

Lemma TopoOrder_NoDup : forall {v a} (g : AcyGraph v a) xs,
    TopoOrder g xs ->
    NoDup xs.

Fact TopoOrder_AGaddv : forall {v a} (g : AcyGraph v a) x xs,
    TopoOrder g xs ->
    TopoOrder (AGaddv v a x g) xs.

Lemma TopoOrder_insert : forall {v a} (g : AcyGraph v a) xs1 xs2 x,
    is_vertex g x ->
    ~In x (xs1++xs2) ->
    (forall y, is_trans_arc g y x -> In y xs2) ->
    TopoOrder g (xs1 ++ xs2) ->
    TopoOrder g (xs1 ++ x :: xs2).

Definition Before (x y : ident) l :=
  Forall' (fun xs x' => x' = y -> In x xs) l.

Lemma Before_middle : forall xs1 xs2 x y,
    x <> y ->
    ~In y xs1 ->
    ~In y xs2 ->
    Before x y (xs1 ++ y :: x :: xs2).

Lemma Before_In : forall xs x y,
    Before x y xs ->
    In y xs ->
    In x xs.

Import Permutation.

Fact TopoOrder_Partition_split : forall {v a} (g : AcyGraph v a) xs1 xs2 xs1l xs1r y,
    Partition (fun z => is_trans_arc g y z) xs1 xs1l xs1r ->
    TopoOrder g (xs1 ++ y :: xs2) ->
    TopoOrder g (xs1l ++ y :: xs1r ++ xs2).

Lemma TopoOrder_reorganize : forall {v a} (g : AcyGraph v a) xs x y,
    x <> y ->
    In x xs ->
    In y xs ->
    TopoOrder g xs ->
    ~is_trans_arc g y x ->
    exists xs', Permutation.Permutation xs' xs /\
           TopoOrder g xs' /\
           Before x y xs'.

Lemma TopoOrder_AGadda : forall {v a} (g : AcyGraph v a) xs x y Hneq Hin1 Hin2 Hna,
    Before x y xs ->
    TopoOrder g xs ->
    TopoOrder (AGadda _ _ x y g Hneq Hin1 Hin2 Hna) xs.

Lemma has_TopoOrder {v a} :
  forall g : AcyGraph v a,
  exists xs,
    PS.Equal (vertices g) (PSP.of_list xs)
    /\ TopoOrder g xs.