Theory Sepref_Graph

header ‹Imperative Graph Representation›
theory Sepref_Graph
imports 
  "../Sepref"
  "../../../DFS_Framework/Misc/DFS_Framework_Refine_Aux"
begin
(*<*)
(* TODO: Move to Misc *)
lemma succs_empty_dom_conv: "R``{x} = {} <-> x∉Domain R"
  by auto

lemma ne_dom_imp_succs_empty: "x∉Domain R ==> R``{x} = {}"
  by auto
(*>*)

text ‹Nodes are identified by numbers from ${0..<n}$, graphs are
  represented as adjacency lists›
type_synonym graph_impl = "(nat list) Heap.array"

definition [to_relAPP]: "is_graph R G Gi ≡ 
    ∃⇩Al. Gi \<mapsto>⇩a l * \<up>(
      R = nat_rel ∧
      Domain G ⊆ {0..<length l} ∧
      (∀v<length l. (l!v,G``{v})∈⟨nat_rel⟩list_set_rel)
    )"

definition succi :: "graph_impl => nat => nat list Heap"
where "succi G v = do {
  l \<leftarrow> Array.len G;
  if v<l then do { 
    r \<leftarrow> Array.nth G v;
    return r
  } else return []
}"

lemma succi_rule[sep_heap_rules]: "
  < is_graph R G Gi > 
    succi Gi v 
  < λr. is_graph R G Gi * \<up>((r,G``{v})∈⟨nat_rel⟩list_set_rel) >"
  unfolding is_graph_def succi_def
  apply (sep_auto)
  apply (subst ne_dom_imp_succs_empty)
  apply (auto simp: list_set_autoref_empty)
  done

term slg_succs

lemma hnr_op_succi[sepref_fr_rules]: " 
  hn_refine 
    (hn_ctxt (is_graph R) G Gi * hn_val nat_rel v vi) 
    (succi Gi vi) 
    (hn_ctxt (is_graph R) G Gi * hn_val nat_rel v vi) 
    (pure (⟨nat_rel⟩list_set_rel)) 
    (RETURN$(slg_succs$G$v))"
  apply rule
  unfolding hn_ctxt_def pure_def 
  by (sep_auto simp: list_set_autoref_empty)

definition cr_graph 
  :: "nat => (nat × nat) list => graph_impl Heap"
where
  "cr_graph numV Es ≡ do {
    a \<leftarrow> Array.new numV [];
    a \<leftarrow> imp_nfoldli Es (λ_. return True) (λ(u,v) a. do {
      l \<leftarrow> Array.nth a u;
      let l = v#l;
      a \<leftarrow> Array.upd u l a;
      return a
    }) a;
    return a
  }"

(* TODO: Show correctness property for cr_graph *)

export_code cr_graph checking SML_imp


end