Theory Sepref_WGraph

section ‹Imperative Weighted Graphs›
theory Sepref_WGraph
imports 
  "../Sepref_ICF_Bindings"
  Dijkstra_Shortest_Path.Graph
begin
  
  type_synonym 'w graph_impl = "(('w×nat) list) Heap.array"

  abbreviation (input) "node_rel ≡ nbn_rel"
  abbreviation (input) "node_assn ≡ nbn_assn"

  definition "is_graph n R G Gi ≡ 
      ∃⇩Al. Gi ↦⇩a l * ↑(
        valid_graph G ∧
        n = length l ∧
        nodes G = {0..<length l} ∧
        (∀v∈nodes G. (l!v, succ G v) ∈ ⟨R ×⇩r node_rel (length l)⟩list_set_rel)
      )"
  
  definition succi :: "'w::heap graph_impl ⇒ nat ⇒ ('w×nat) list Heap"
  where "succi G v = do {
    l ← Array.len G;
    if v<l then do { ― ‹TODO: Alternatively, require ‹v› to be a valid node as precondition!›
      r ← Array.nth G v;
      return r
    } else return []
  }"

  lemma "
    < is_graph n R G Gi * ↑(v∈nodes G) > 
      succi Gi v 
    < λr. is_graph n R G Gi * ↑((r,succ G v)∈⟨R ×⇩r node_rel n⟩list_set_rel) >"
    unfolding is_graph_def succi_def
    by sep_auto
  
  lemma (in valid_graph) succ_no_node_empty: "v∉V ⟹ succ G v = {}"
    unfolding succ_def using E_valid
    by auto
  
  lemma [sepref_fr_rules]: " 
    hn_refine 
      (hn_ctxt (is_graph n R) G Gi * hn_ctxt (node_assn n) v vi) 
      (succi Gi vi) 
      (hn_ctxt (is_graph n R) G Gi * hn_ctxt (node_assn n) v vi) 
      (pure (⟨R ×⇩r node_rel n⟩list_set_rel))
      (RETURN$(succ$G$v))"
    apply rule
    unfolding hn_ctxt_def pure_def is_graph_def succi_def
    by (sep_auto simp: valid_graph.succ_no_node_empty list_set_autoref_empty)
  
  definition nodes_impl :: "'w::heap graph_impl ⇒ nat list Heap"
    where "nodes_impl Gi ≡ do {
    l ← Array.len Gi;
    return [0..<l]
  }"
  
  lemma node_list_rel_id: "∀x∈set l. x<n ⟹ (l,l)∈⟨node_rel n⟩list_rel"
    by (induction l) auto

  lemma [sepref_fr_rules]: "hn_refine 
    (hn_ctxt (is_graph n R) G Gi) 
    (nodes_impl Gi) 
    (hn_ctxt (is_graph n R) G Gi) 
    (pure (⟨node_rel n⟩list_set_rel))
    (RETURN$(nodes$G))"
    apply rule
    unfolding hn_ctxt_def pure_def is_graph_def nodes_impl_def
    apply (sep_auto simp: list_set_rel_def br_def intro!: relcompI node_list_rel_id)
    done
  
  sepref_register succ nodes  

  
  definition cr_graph 
    :: "nat ⇒ (nat × nat × 'w) list ⇒ 'w::heap graph_impl Heap"
  where
    "cr_graph numV Es ≡ do {
      a ← Array.new numV [];
      a ← imp_nfoldli Es (λ_. return True) (λ(u,v,w) a. do {
        l ← Array.nth a u;
        let l = (w,v)#l;
        a ← Array.upd u l a;
        return a
      }) a;
      return a
    }"
  
  export_code cr_graph checking SML_imp


end