Theory Gabow_SCC.Gabow_Skeleton_Code

section ‹Code Generation for the Skeleton Algorithm \label{sec:skel_code}›
theory Gabow_Skeleton_Code
imports 
  Gabow_Skeleton
  CAVA_Automata.Digraph_Impl
  CAVA_Base.CAVA_Code_Target
begin

section ‹Statistics›
text ‹
  In this section, we do the ML setup that gathers statistics about the 
  algorithm's execution.
›

code_printing
  code_module Gabow_Skeleton_Statistics  (SML) ‹
    structure Gabow_Skeleton_Statistics = struct
      val active = Unsynchronized.ref false
      val num_vis = Unsynchronized.ref 0

      val time = Unsynchronized.ref Time.zeroTime

      fun is_active () = !active
      fun newnode () =
      (
        num_vis := !num_vis + 1;
        if !num_vis mod 10000 = 0 then tracing (IntInf.toString (!num_vis) ^ "\n") else ()
      )

      fun start () = (active := true; time := Time.now ())
      fun stop () = (time := Time.- (Time.now (), !time))

      fun to_string () = let
        val t = Time.toMilliseconds (!time)
        val states_per_ms = real (!num_vis) / real t
        val realStr = Real.fmt (StringCvt.FIX (SOME 2))
      in
        "Required time: " ^ IntInf.toString (t) ^ "ms\n"
      ^ "States per ms: " ^ realStr states_per_ms ^ "\n"
      ^ "# states: " ^ IntInf.toString (!num_vis) ^ "\n"
      end
        
      val _ = Statistics.register_stat ("Gabow-Skeleton",is_active,to_string)

    end
›
code_reserved SML Gabow_Skeleton_Statistics

code_printing
  constant stat_newnode  (SML) "Gabow'_Skeleton'_Statistics.newnode"
| constant stat_start  (SML) "Gabow'_Skeleton'_Statistics.start"
| constant stat_stop  (SML) "Gabow'_Skeleton'_Statistics.stop"

section ‹Automatic Refinement Setup›
consts i_node_state :: interface

definition "node_state_rel  {(-1::int,DONE)}  {(int k,STACK k) | k. True }"
lemma node_state_rel_simps[simp]:
  "(i,DONE)node_state_rel  i=-1"
  "(i,STACK n)node_state_rel  i = int n"
  unfolding node_state_rel_def
  by auto

lemma node_state_rel_sv[simp,intro!,relator_props]:
  "single_valued node_state_rel"
  unfolding node_state_rel_def
  by (auto intro: single_valuedI)

lemmas [autoref_rel_intf] = REL_INTFI[of node_state_rel i_node_state]

primrec is_DONE where
  "is_DONE DONE = True"
| "is_DONE (STACK _) = False"

lemma node_state_rel_refine[autoref_rules]:
  "(-1,DONE)node_state_rel"
  "(int,STACK)nat_relnode_state_rel"
  "(λi. i<0,is_DONE)node_state_relbool_rel"
  "((λf g i. if i0 then f (nat i) else g),case_node_state)
    (nat_rel  R)  R  node_state_rel  R"
  unfolding node_state_rel_def 
    apply auto [3]
    apply (fastforce dest: fun_relD)
    done

lemma [autoref_op_pat]: 
  "(x=DONE)  is_DONE x"
  "(DONE=x)  is_DONE x"
  apply (auto intro!: eq_reflection)
  apply ((cases x, simp_all) [])+
  done

(* TODO: Make changing the Autoref-config simpler, by concentrating
    everything here *)
consts i_node :: interface

(* TODO: Move generic part of this locale to Digraph_impl *)
locale fr_graph_impl_loc = fr_graph G
  for mrel and node_rel :: "('vi × 'v) set" 
    and node_eq_impl :: "'vi  'vi  bool"
    and node_hash_impl :: "nat  'vi  nat"
    and node_def_hash_size :: nat
    and G_impl and G :: "('v,'more) graph_rec_scheme"
     
  +
  assumes G_refine: "(G_impl,G)mrel,node_relg_impl_rel_ext"
      and node_eq_refine: "(node_eq_impl, (=))  node_rel  node_rel  bool_rel"
      and node_hash: "is_bounded_hashcode node_rel node_eq_impl node_hash_impl"
      and node_hash_def_size: "(is_valid_def_hm_size TYPE('vi) node_def_hash_size)"
begin
  (*abbreviation "node_rel ≡ Id :: ('v × _) set"*)
  lemmas [autoref_rel_intf] = REL_INTFI[of node_rel i_node]

  lemmas [autoref_rules] = G_refine node_eq_refine

  lemmas [autoref_ga_rules] = node_hash node_hash_def_size
  
  
  lemma locale_this: "fr_graph_impl_loc mrel node_rel node_eq_impl node_hash_impl node_def_hash_size G_impl G"
    by unfold_locales

  abbreviation "oGSi_rel  node_rel,node_state_rel(ahm_rel node_hash_impl)"

  abbreviation "GSi_rel  
    node_relas_rel 
    ×r nat_relas_rel 
    ×r oGSi_rel
    ×r nat_rel ×r node_rellist_set_relas_rel"

  lemmas [autoref_op_pat] = GS.S_def GS.B_def GS.I_def GS.P_def

end

section ‹Generating the Code›


thm autoref_ga_rules


context fr_graph_impl_loc
begin
  schematic_goal push_code_aux: "(?c,push_impl)node_rel  GSi_rel  GSi_rel"
    unfolding push_impl_def_opt[abs_def]
    using [[autoref_trace_failed_id]]
    apply (autoref (keep_goal))
    done
  concrete_definition (in -) push_code uses fr_graph_impl_loc.push_code_aux
  lemmas [autoref_rules] = push_code.refine[OF locale_this]
  
  schematic_goal pop_code_aux: "(?c,pop_impl)GSi_rel  GSi_relnres_rel"
    unfolding pop_impl_def_opt[abs_def]
    unfolding GS.mark_as_done_def
    using [[autoref_trace_failed_id]]
    apply (autoref (keep_goal))
    done
  concrete_definition (in -) pop_code uses fr_graph_impl_loc.pop_code_aux
  lemmas [autoref_rules] = pop_code.refine[OF locale_this]

  schematic_goal S_idx_of_code_aux: 
    notes [autoref_rules] = IdI[of "undefined::nat"] (* TODO: hack!*)
    shows "(?c,GS.S_idx_of)GSi_rel  node_rel  nat_rel"
    unfolding GS.S_idx_of_def[abs_def]
    using [[autoref_trace_failed_id]]
    apply (autoref (keep_goal))
    done
  concrete_definition (in -) S_idx_of_code 
    uses fr_graph_impl_loc.S_idx_of_code_aux
  lemmas [autoref_rules] = S_idx_of_code.refine[OF locale_this] 

  schematic_goal idx_of_code_aux:
    notes [autoref_rules] = IdI[of "undefined::nat"] (* TODO: hack!*)
    shows "(?c,GS.idx_of_impl) GSi_rel  node_rel  nat_relnres_rel"
    unfolding 
      GS.idx_of_impl_def[abs_def, unfolded GS.find_seg_impl_def GS.S_idx_of_def,
        THEN opt_GSdef, unfolded GS_sel_simps, abs_def]
    using [[autoref_trace_failed_id]]
    apply (autoref (keep_goal))
    done
  concrete_definition (in -) idx_of_code uses fr_graph_impl_loc.idx_of_code_aux
  lemmas [autoref_rules] = idx_of_code.refine[OF locale_this] 

  schematic_goal collapse_code_aux: 
    "(?c,collapse_impl)node_rel  GSi_rel  GSi_relnres_rel"
    unfolding collapse_impl_def_opt[abs_def] 
    using [[autoref_trace_failed_id]]
    apply (autoref (keep_goal))
    done
  concrete_definition (in -) collapse_code 
    uses fr_graph_impl_loc.collapse_code_aux
  lemmas [autoref_rules] = collapse_code.refine[OF locale_this] 

  term select_edge_impl
  schematic_goal select_edge_code_aux:
    "(?c,select_edge_impl) 
       GSi_rel  node_reloption_rel ×r GSi_relnres_rel"
    unfolding select_edge_impl_def_opt[abs_def] 

    using [[autoref_trace_failed_id]]
    using [[goals_limit=1]]
    apply (autoref (keep_goal,trace))
    done
  concrete_definition (in -) select_edge_code 
    uses fr_graph_impl_loc.select_edge_code_aux
  lemmas [autoref_rules] = select_edge_code.refine[OF locale_this] 

  context begin interpretation autoref_syn .

    term fr_graph.pop_impl
    lemma [autoref_op_pat]: 
      "push_impl  OP push_impl"
      "collapse_impl  OP collapse_impl"
      "select_edge_impl  OP select_edge_impl"
      "pop_impl  OP pop_impl"
      by simp_all
  
  end

  schematic_goal skeleton_code_aux:
    "(?c,skeleton_impl)  oGSi_relnres_rel"
    unfolding skeleton_impl_def[abs_def] initial_impl_def GS_initial_impl_def
    unfolding path_is_empty_impl_def is_on_stack_impl_def is_done_impl_def 
      is_done_oimpl_def
    unfolding GS.is_on_stack_impl_def GS.is_done_impl_def
    using [[autoref_trace_failed_id]]
    apply (autoref (keep_goal,trace))
    done
    
    
    
  concrete_definition (in -) skeleton_code 
    for node_eq_impl G_impl
    uses fr_graph_impl_loc.skeleton_code_aux
    
  thm   skeleton_code.refine
    
  lemmas [autoref_rules] = skeleton_code.refine[OF locale_this] 
  

  schematic_goal pop_tr_aux: "RETURN ?c  pop_code node_eq_impl node_hash_impl s"
    unfolding pop_code_def by refine_transfer
  concrete_definition (in -) pop_tr uses fr_graph_impl_loc.pop_tr_aux
  lemmas [refine_transfer] = pop_tr.refine[OF locale_this]

  schematic_goal select_edge_tr_aux: "RETURN ?c  select_edge_code node_eq_impl s"
    unfolding select_edge_code_def by refine_transfer
  concrete_definition (in -) select_edge_tr 
    uses fr_graph_impl_loc.select_edge_tr_aux
  lemmas [refine_transfer] = select_edge_tr.refine[OF locale_this]

  schematic_goal idx_of_tr_aux: "RETURN ?c  idx_of_code node_eq_impl node_hash_impl v s"
    unfolding idx_of_code_def by refine_transfer
  concrete_definition (in -) idx_of_tr uses fr_graph_impl_loc.idx_of_tr_aux
  lemmas [refine_transfer] = idx_of_tr.refine[OF locale_this]

  schematic_goal collapse_tr_aux: "RETURN ?c  collapse_code node_eq_impl node_hash_impl v s"
    unfolding collapse_code_def by refine_transfer
  concrete_definition (in -) collapse_tr uses fr_graph_impl_loc.collapse_tr_aux
  lemmas [refine_transfer] = collapse_tr.refine[OF locale_this]

  schematic_goal skeleton_tr_aux: "RETURN ?c  skeleton_code node_hash_impl node_def_hash_size node_eq_impl g"
    unfolding skeleton_code_def by refine_transfer
  concrete_definition (in -) skeleton_tr uses fr_graph_impl_loc.skeleton_tr_aux
  lemmas [refine_transfer] = skeleton_tr.refine[OF locale_this]

end

term skeleton_tr

export_code skeleton_tr checking SML

end