Theory 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_rel→node_state_rel"
"(λi. i<0,is_DONE)∈node_state_rel→bool_rel"
"((λf g i. if i≥0 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
consts i_node :: interface
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_rel⟩g_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
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_rel⟩as_rel
×⇩r ⟨nat_rel⟩as_rel
×⇩r oGSi_rel
×⇩r ⟨nat_rel ×⇩r ⟨node_rel⟩list_set_rel⟩as_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_rel⟩nres_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"]
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"]
shows "(?c,GS.idx_of_impl)∈ GSi_rel → node_rel → ⟨nat_rel⟩nres_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_rel⟩nres_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_rel⟩option_rel ×⇩r GSi_rel⟩nres_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_rel⟩nres_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