File ‹Transform_Data.ML›
signature TRANSFORM_DATA =
sig
type dp_info = {
old_head: term,
new_head': term,
new_headT: term,
old_defs: thm list,
new_defT: thm,
new_def': thm list
}
type cmd_info = {
scope: binding,
head: term,
locale: string option,
dp_info: dp_info option
}
val get_dp_info: string -> Proof.context -> term -> dp_info option
val get_last_cmd_info: Proof.context -> cmd_info
val commit_dp_info: string -> dp_info -> local_theory -> local_theory
val add_tmp_cmd_info: binding * term * string option -> local_theory -> local_theory
val get_or_last_cmd_info: Proof.context -> (string * term) option -> cmd_info
end
structure Transform_Data : TRANSFORM_DATA =
struct
type dp_info = {
old_head: term,
new_head': term,
new_headT: term,
old_defs: thm list,
new_defT: thm,
new_def': thm list
}
type cmd_info = {
scope: binding,
head: term,
locale: string option,
dp_info: dp_info option
}
fun map_cmd_info f0 f1 f2 f3 {scope, head, locale, dp_info} =
{scope = f0 scope, head = f1 head, locale = f2 locale, dp_info = f3 dp_info}
fun map_cmd_dp_info f = map_cmd_info I I I f
structure Data = Generic_Data (
type T = {
monadified_terms: (string * cmd_info Item_Net.T) list,
last_cmd_info: cmd_info option
}
val empty = {
monadified_terms =
["state", "heap"]
~~ replicate 2 (Item_Net.init (op aconv o apply2 #head) (single o #head)),
last_cmd_info = NONE
}
fun merge (
{monadified_terms = m0, ...},
{monadified_terms = m1, ...}
) =
let
val keys0 = map fst m0
val keys1 = map fst m1
val _ = @{assert} (keys0 = keys1)
val vals = map Item_Net.merge (map snd m0 ~~ map snd m1)
val ms = keys0 ~~ vals
in
{monadified_terms = ms, last_cmd_info = NONE}
end
)
fun transform_dp_info phi {old_head, new_head', new_headT, old_defs, new_defT, new_def'} =
{
old_head = Morphism.term phi old_head,
new_head' = Morphism.term phi new_head',
new_headT = Morphism.term phi new_headT,
old_defs = Morphism.fact phi old_defs,
new_def' = Morphism.fact phi new_def',
new_defT = Morphism.thm phi new_defT
}
fun get_monadified_terms_generic monad_name context =
Data.get context
|> #monadified_terms
|> (fn l => AList.lookup op= l monad_name)
|> the
fun get_monadified_terms monad_name ctxt =
get_monadified_terms_generic monad_name (Context.Proof ctxt)
fun map_data f0 f1 = Data.map (fn {monadified_terms, last_cmd_info} =>
{monadified_terms = f0 monadified_terms, last_cmd_info = f1 last_cmd_info})
fun map_monadified_terms f = map_data f I
fun map_last_cmd_info f = map_data I f
fun put_monadified_terms_generic monad_name new_terms context =
context |> map_monadified_terms (AList.update op= (monad_name, new_terms))
fun map_monadified_terms_generic monad_name f context =
context |> map_monadified_terms (AList.map_entry op= monad_name f)
fun put_last_cmd_info cmd_info_opt context =
map_last_cmd_info (K cmd_info_opt) context
fun get_cmd_info monad_name ctxt tm =
get_monadified_terms monad_name ctxt
|> (fn net => Item_Net.retrieve net tm)
fun get_dp_info monad_name ctxt tm =
get_cmd_info monad_name ctxt tm
|> (fn result => case result of
{dp_info = SOME dp_info', ...} :: _ => SOME dp_info'
| _ => NONE)
fun get_last_cmd_info_generic context =
Data.get context
|> #last_cmd_info
|> the
fun get_last_cmd_info ctxt =
get_last_cmd_info_generic (Context.Proof ctxt)
fun commit_dp_info monad_name dp_info =
Local_Theory.declaration
{pervasive = false, syntax = false, pos = ⌂}
(fn phi => fn context =>
let
val old_cmd_info = get_last_cmd_info_generic context
val new_dp_info = transform_dp_info phi dp_info
val new_cmd_info = old_cmd_info |> map_cmd_dp_info (K (SOME new_dp_info))
in
context
|> map_monadified_terms_generic monad_name (Item_Net.update new_cmd_info)
|> put_last_cmd_info (SOME new_cmd_info)
end)
fun add_tmp_cmd_info (scope, head, locale_opt) =
Local_Theory.declaration
{pervasive = false, syntax = false, pos = ⌂}
(fn phi => fn context =>
let
val new_cmd_info = {
scope = Morphism.binding phi scope,
head = Morphism.term phi head,
locale = locale_opt,
dp_info = NONE
}
in
context |> put_last_cmd_info (SOME new_cmd_info)
end )
fun get_or_last_cmd_info ctxt monad_name_tm_opt =
case monad_name_tm_opt of
NONE => get_last_cmd_info ctxt
| SOME (monad_name, tm) => get_cmd_info monad_name ctxt tm |> the_single
end