Theory SemanticsSnippets

theory SemanticsSnippets
  imports
    Semantics.IRStepObj Semantics.Form Proofs.Stuttering Snippets.Snipping
begin

declare [[show_types=false]]

(*notation (latex)
  NoNode ("ε")
*)
notation (latex)
  kind ("_⟪_⟫")

notation (latex)
  stamp_expr ("\<^latex>‹\\pitchfork› _")

notation (latex)
  val_to_bool ("_\<^latex>‹\\ensuremath{_{\\mathit{›bool\<^latex>‹}}}›")


syntax (spaced_type_def output)
  "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)

snipbegin ‹isbinary›
text ‹\begin{center}
@{term_type[mode=spaced_type_def] is_BinaryArithmeticNode}
\end{center}›
snipend -

(* figure out how to export a subset of IRNode!!! *)

snipbegin ‹inputsof›
text_raw ‹
@{term_type[mode=spaced_type_def] inputs_of}

@{thm inputs_of_ConstantNode}

@{thm inputs_of_ParameterNode}

@{thm inputs_of_ValuePhiNode}

@{thm inputs_of_AddNode}

@{thm inputs_of_IfNode}›
snipend -

snipbegin ‹graphdefnostamp›
text_raw ‹
@{bold ‹typedef›} @{term[source] ‹IRGraph = {g :: ID ⇀ IRNode . finite (dom g)}›}
›
snipend -

fun ids_fake :: "(ID ⇀ IRNode) ⇒ ID set" where
  "ids_fake g = {nid ∈ dom g . g nid ≠ (Some NoNode)}"

fun kind_fake :: "(ID ⇀ IRNode) ⇒ (ID ⇒ IRNode)" where
  "kind_fake g = (λnid. (case g nid of None ⇒ NoNode | Some v ⇒ v))"

snipbegin ‹helpersdisplay›
text_raw ‹
@{term_type[mode=spaced_type_def] ids_fake}

@{thm ids_fake.simps}\\[0.75em]

@{term_type[mode=spaced_type_def] kind_fake}

@{thm kind_fake.simps}\\[0.75em]

@{term_type[mode=spaced_type_def] inputs}

@{thm inputs.simps}\\[0.75em]

@{term_type[mode=spaced_type_def] succ}

@{thm succ.simps}\\[0.75em]

@{term_type[mode=spaced_type_def] input_edges}

@{thm input_edges.simps}\\[0.75em]

@{term_type[mode=spaced_type_def] usages}

@{thm usages.simps}\\[0.75em]

@{term_type[mode=spaced_type_def] successor_edges}

@{thm successor_edges.simps}\\[0.75em]

@{term_type[mode=spaced_type_def] predecessors}

@{thm predecessors.simps}\\[0.75em]
›
snipend -

snipbegin ‹wf_start_def›
text_raw ‹
@{thm[display,margin=40] wf_start_def}
›
snipend -
snipbegin ‹wf_closed_def›
text_raw ‹
@{thm[display,margin=40] wf_closed_def}
› 
snipend -
snipbegin ‹wf_phis_def›
text_raw ‹
@{thm[display,margin=40] wf_phis_def}
›
snipend -
snipbegin ‹wf_ends_def›
text_raw ‹
@{thm[display,margin=40] wf_ends_def}
›
snipend -

snipbegin ‹wf_graph_def›
text_raw ‹
@{term_type[mode=spaced_type_def] wf_graph}

@{thm wf_graph.simps}
›
snipend -

text_raw ‹@{bold ‹type-synonym›} Signature = @{typ string}›

snipbegin ‹programdef›
text_raw ‹
@{bold ‹type-synonym›} Program = @{typ "Signature ⇀ IRGraph"}
›
snipend -

print_antiquotations

(*
type_synonym ('a, 'b) Heap = "'a ⇒ 'b ⇒ Value"
type_synonym Free = "nat"
type_synonym ('a, 'b) DynamicHeap = "('a, 'b) Heap × Free"

fun h_load_field :: "'a ⇒ 'b ⇒ ('a, 'b) DynamicHeap ⇒ Value" where
  "h_load_field f r (h, n) = h f r"

fun h_store_field :: "'a ⇒ 'b ⇒ Value ⇒ ('a, 'b) DynamicHeap ⇒ ('a, 'b) DynamicHeap" where
  "h_store_field f r v (h, n) = (h(f := ((h f)(r := v))), n)"

fun h_new_inst :: "('a, 'b) DynamicHeap ⇒ ('a, 'b) DynamicHeap × Value" where
  "h_new_inst (h, n) = ((h,n+1), (ObjRef (Some n)))"

type_synonym FieldRefHeap = "(string, objref) DynamicHeap"
*)

(* TODO: add heap here *)
snipbegin ‹heapdef›
type_synonym Heap = "string ⇒ objref ⇒ Value"
type_synonym Free = "nat"
type_synonym DynamicHeap = "Heap × Free"

text_raw ‹
\\[0.75em]

@{text ‹h_load_field :: ›} @{typ[source] "string ⇒ objref ⇒ DynamicHeap ⇒ Value"}

@{thm h_load_field.simps}\\[0.75em]

@{text ‹h_store_field :: ›} @{typ[source] "string ⇒ objref ⇒ Value ⇒ DynamicHeap ⇒ DynamicHeap"}

@{thm h_store_field.simps}\\[0.75em]

@{text ‹h_new_inst :: ›} @{typ[source] "DynamicHeap ⇒ (DynamicHeap × Value)"}

@{thm h_new_inst.simps}
›
snipend -

(* Deprecated expression semantics *)
(*
text_raw ‹\Snip{ExpressionSemantics}%›
text ‹
\begin{center}
\induct{@{thm[mode=Rule] eval.ConstantNode [no_vars]}}{eval:const}
\induct{@{thm[mode=Rule] eval.AddNode [no_vars]}}{eval:add}
\induct{@{thm[mode=Rule] eval.ParameterNode [no_vars]}}{eval:param}
\induct{@{thm[mode=Rule] eval.ValuePhiNode [no_vars]}}{eval:phi}
\induct{@{thm[mode=Rule] eval.InvokeNodeEval [no_vars]}}{eval:invoke}
\induct{@{thm[mode=Rule] eval.NewInstanceNode [no_vars]}}{eval:invoke}
\induct{@{thm[mode=Rule] eval.LoadFieldNode [no_vars]}}{eval:load}
\end{center}
›
text_raw ‹\EndSnip›

text_raw ‹\Snip{EvalAll}%›
text ‹
\begin{center}
@{thm[mode=Rule] eval_all.Base [no_vars]}\\[8px]
@{thm[mode=Rule] eval_all.Transitive [no_vars]}
\end{center}
›
text_raw ‹\EndSnip›
*)


snipbegin ‹StepSemantics›
text ‹
\begin{center}
\induct{@{thm[mode=Rule] step.SequentialNode [no_vars]}}{step:seq}
\induct{@{thm[mode=Rule] step.IfNode [no_vars]}}{step:if}
\induct{@{thm[mode=Rule] step.EndNodes [no_vars]}}{step:end}
\induct{@{thm[mode=Rule] step.NewInstanceNode [no_vars]}}{step:newinst}
\induct{@{thm[mode=Rule] step.LoadFieldNode [no_vars]}}{step:load}
\induct{@{thm[mode=Rule] step.StoreFieldNode [no_vars]}}{step:store}
\induct{@{thm[mode=Rule] step.StaticLoadFieldNode [no_vars]}}{step:load-static}
\induct{@{thm[mode=Rule] step.StaticStoreFieldNode [no_vars]}}{step:store-static}
\end{center}
›
snipend -

snipbegin ‹TopStepSemantics›
text ‹
\begin{center}
\induct{@{thm[mode=Rule] step_top.Lift [no_vars]}}{top:lift}
\induct{@{thm[mode=Rule] step_top.InvokeNodeStep [no_vars]}}{top:invoke}
\induct{@{thm[mode=Rule] step_top.ReturnNode [no_vars]}}{top:return}
\induct{@{thm[mode=Rule] step_top.ReturnNodeVoid [no_vars]}}{top:return-void}
\induct{@{thm[mode=Rule] step_top.UnwindNode [no_vars]}}{top:unwind}
\end{center}
›
snipend -

(* Deprecated canonicalization rules *)
(*
text_raw ‹\Snip{AddNodeRules}%
\begin{center}
@{thm[mode=Rule] CanonicalizeAdd.add_both_const [no_vars]}\\[8px]
@{thm[mode=Rule] CanonicalizeAdd.add_xzero [no_vars]}\\[8px]
@{thm[mode=Rule] CanonicalizeAdd.add_yzero [no_vars]}
\end{center}
\EndSnip›

text_raw ‹\Snip{AddNodeProof}%
@{thm CanonicalizeAddProof}
\EndSnip›
*)

snipbegin ‹Stutter›
text ‹
\begin{center}
@{thm[mode=Rule] stutter.StutterStep [no_vars]}\\[8px]
@{thm[mode=Rule] stutter.Transitive [no_vars]}
\end{center}
›
snipend -

(*
text_raw ‹\Snip{CanonicalizeIfNodeRules}%
\begin{center}
@{thm[mode=Rule] CanonicalizeIf.trueConst}\\[8px]
@{thm[mode=Rule] CanonicalizeIf.falseConst}\\[8px]
@{thm[mode=Rule] CanonicalizeIf.eqBranch}
\end{center}
\EndSnip›
definition replace_node_fake :: "ID ⇒ IRNode ⇒ IRGraph ⇒ IRGraph" where
  "replace_node_fake nid node g = replace_node nid (node,default_stamp) g"
lemma CanonicalizeIfProof_fake:
  fixes m::MapState and h::FieldRefHeap
  assumes "kind g nid = before"
  assumes "CanonicalizeIf g before after"
  assumes "g' = replace_node_fake nid after g"
  assumes "g, p ⊢ (nid, m, h) → (nid', m, h)"
  shows "nid | g ∼ g'"
  by (metis CanonicalizeIfProof assms(1) assms(2) assms(3) assms(4) replace_node_fake_def)

text_raw ‹\Snip{CanonicalizeIfNodeProof}%
\begin{center}
@{thm[display] CanonicalizeIfProof_fake}
\end{center}
\EndSnip›
*)

(* EXPERIMENTAL *)
notation (latex output)
  filtered_inputs ("inputs\<^latex>‹\\ensuremath{^{\\mathit{›_⟪_⟫\<^latex>‹}}}›\<^latex>‹\\ensuremath{_{\\mathit{›_\<^latex>‹}}}›")
notation (latex output)
  filtered_successors ("succ\<^latex>‹\\ensuremath{^{\\mathit{›_⟪_⟫\<^latex>‹}}}›\<^latex>‹\\ensuremath{_{\\mathit{›_\<^latex>‹}}}›")
notation (latex output)
  filtered_usages ("usages\<^latex>‹\\ensuremath{^{\\mathit{›_⟪_⟫\<^latex>‹}}}›\<^latex>‹\\ensuremath{_{\\mathit{›_\<^latex>‹}}}›")

snipbegin ‹example2›
text_raw ‹
@{term[display] ‹filtered_inputs g nid f›}
›
snipend -

notation (latex output)
  Pure.dummy_pattern ("-")

(* take out bits from intvals - changes if we change to deal with bits *)
notation (latex output)
  IntVal ("IntVal (2 _)")

end