Theory Sepref_Graph

section ‹Imperative Graph Representation›
theory Sepref_Graph
imports 
  "../Sepref"
  "../Sepref_ICF_Bindings"
  "../IICF/IICF"
  (*"../../../DFS_Framework/Misc/DFS_Framework_Refine_Aux"*)
begin

text ‹Graph Interface›
sepref_decl_intf 'a i_graph is "('a×'a) set"

definition op_graph_succ :: "('v×'v) set ⇒ 'v ⇒ 'v set" 
  where [simp]: "op_graph_succ E u ≡ E``{u}"
sepref_register op_graph_succ :: "'a i_graph ⇒ 'a ⇒ 'a set"

thm intf_of_assnI

lemma [pat_rules]: "((``))$E$(insert$u${}) ≡ op_graph_succ$E$u" by simp

definition [to_relAPP]: "graph_rel A ≡ ⟨A×⇩rA⟩set_rel"

text ‹Adjacency List Implementation›
lemma param_op_graph_succ[param]: 
  "⟦IS_LEFT_UNIQUE A; IS_RIGHT_UNIQUE A⟧ ⟹ (op_graph_succ, op_graph_succ) ∈ ⟨A⟩graph_rel → A → ⟨A⟩set_rel"
  unfolding op_graph_succ_def[abs_def] graph_rel_def
  by parametricity

context begin
private definition "graph_α1 l ≡ { (i,j). i<length l ∧ j∈l!i } "

private definition "graph_rel1 ≡ br graph_α1 (λ_. True)"

private definition "succ1 l i ≡ if i<length l then l!i else {}"

private lemma succ1_refine: "(succ1,op_graph_succ) ∈ graph_rel1 → Id → ⟨Id⟩set_rel"
  by (auto simp: graph_rel1_def graph_α1_def br_def succ1_def split: if_split_asm intro!: ext)

private definition "assn2 ≡ array_assn (pure (⟨Id⟩list_set_rel))"

definition "adjg_assn A ≡ hr_comp (hr_comp assn2 graph_rel1) (⟨the_pure A⟩graph_rel)"

context
  notes [sepref_import_param] = list_set_autoref_empty[folded op_set_empty_def]
  notes [fcomp_norm_unfold] = adjg_assn_def[symmetric]
begin
sepref_definition succ2 is "(uncurry (RETURN oo succ1))" :: "(assn2⇧k*⇩aid_assn⇧k →⇩a pure (⟨Id⟩list_set_rel))"
  unfolding succ1_def[abs_def] assn2_def
  by sepref

lemma adjg_succ_hnr[sepref_fr_rules]: "⟦CONSTRAINT (IS_PURE IS_LEFT_UNIQUE) A; CONSTRAINT (IS_PURE IS_RIGHT_UNIQUE) A⟧ 
  ⟹ (uncurry succ2, uncurry (RETURN ∘∘ op_graph_succ)) ∈ (adjg_assn A)⇧k *⇩a A⇧k →⇩a pure (⟨the_pure A⟩list_set_rel)"
  using succ2.refine[FCOMP succ1_refine, FCOMP param_op_graph_succ, simplified, of A]
  by (simp add: IS_PURE_def list_set_rel_compp)

end

end

lemma [intf_of_assn]: 
  "intf_of_assn A (i::'I itself) ⟹ intf_of_assn (adjg_assn A) TYPE('I i_graph)" by simp

definition cr_graph 
  :: "nat ⇒ (nat × nat) list ⇒ nat list Heap.array Heap"
where
  "cr_graph numV Es ≡ do {
    a ← Array.new numV [];
    a ← imp_nfoldli Es (λ_. return True) (λ(u,v) a. do {
      l ← Array.nth a u;
      let l = v#l;
      a ← 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