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×rAset_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)  Agraph_rel  A  Aset_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  jl!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  Idset_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 (Idlist_set_rel))"

definition "adjg_assn A  hr_comp (hr_comp assn2 graph_rel1) (the_pure Agraph_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))" :: "(assn2k*aid_assnk a pure (Idlist_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 Ak a pure (the_pure Alist_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