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} 
        (vnodes 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 * (vnodes G) > 
      succi Gi v 
    < λr. is_graph n R G Gi * ((r,succ G v)R ×r node_rel nlist_set_rel) >"
    unfolding is_graph_def succi_def
    by sep_auto
  
  lemma (in valid_graph) succ_no_node_empty: "vV  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 nlist_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: "xset l. x<n  (l,l)node_rel nlist_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 nlist_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