Theory Printer_Toy_extended
section‹Instantiating the Printer for Toy (II)›
theory Printer_Toy_extended
imports Meta_Toy_extended
Printer_Toy
begin
context Print
begin
definition "To_oid = (λOid n ⇒ To_nat n)"
definition ‹of_toy_def_base = (λ ToyDefInteger i ⇒ To_string i
| ToyDefReal (i1, i2) ⇒ ‹%s.%s› (To_string i1) (To_string i2)
| ToyDefString s ⇒ ‹"%s"› (To_string s))›
fun of_toy_data_shallow where
"of_toy_data_shallow e = (λ ShallB_term b ⇒ of_toy_def_base b
| ShallB_str s ⇒ To_string s
| ShallB_self s ⇒ ‹self %d› (To_oid s)
| ShallB_list l ⇒ ‹[ %s ]› (String_concat ‹, › (List.map of_toy_data_shallow l))) e"
fun of_toy_list_attr where
"of_toy_list_attr f e = (λ ToyAttrNoCast x ⇒ f x
| ToyAttrCast ty (ToyAttrNoCast x) _ ⇒ ‹(%s :: %s)› (f x) (To_string ty)
| ToyAttrCast ty l _ ⇒ ‹%s → toyAsType( %s )› (of_toy_list_attr f l) (To_string ty)) e"
definition ‹of_toy_instance_single toyi =
(let (s_left, s_right) =
case Inst_name toyi of
None ⇒ (case Inst_ty toyi of Some ty ⇒ (‹(›, ‹ :: %s)› (To_string ty)))
| Some s ⇒
( ‹%s%s = ›
(To_string s)
(case Inst_ty toyi of None ⇒ ‹› | Some ty ⇒ ‹ :: %s› (To_string ty))
, ‹›) in
‹%s%s%s›
s_left
(of_toy_list_attr
(λl. ‹[ %s ]›
(String_concat ‹, ›
(L.map (λ(pre_post, attr, v).
‹%s"%s" = %s› (case pre_post of None ⇒ ‹›
| Some (s1, s2) ⇒ ‹("%s", "%s") |= › (To_string s1) (To_string s2))
(To_string attr)
(of_toy_data_shallow v))
l)))
(Inst_attr toyi))
s_right)›
definition "of_toy_instance _ = (λ ToyInstance l ⇒
‹Instance %s› (String_concat ‹
and › (L.map of_toy_instance_single l)))"
definition "of_toy_def_state_core l =
String_concat ‹, › (L.map (λ ToyDefCoreBinding s ⇒ To_string s
| ToyDefCoreAdd toyi ⇒ of_toy_instance_single toyi) l)"
definition "of_toy_def_state _ (floor ::
String.literal) = (λ ToyDefSt n l ⇒
‹State%s %s = [ %s ]›
floor
(To_string n)
(of_toy_def_state_core l))"
definition "of_toy_def_pp_core = (λ ToyDefPPCoreBinding s ⇒ To_string s
| ToyDefPPCoreAdd l ⇒ ‹[ %s ]› (of_toy_def_state_core l))"
definition "of_toy_def_pre_post _ (floor ::
String.literal) = (λ ToyDefPP n s_pre s_post ⇒
‹PrePost%s %s%s%s›
floor
(case n of None ⇒ ‹› | Some n ⇒ ‹%s = › (To_string n))
(of_toy_def_pp_core s_pre)
(case s_post of None ⇒ ‹› | Some s_post ⇒ ‹ %s› (of_toy_def_pp_core s_post)))"
end
lemmas [code] =
Print.To_oid_def
Print.of_toy_def_base_def
Print.of_toy_instance_single_def
Print.of_toy_instance_def
Print.of_toy_def_state_core_def
Print.of_toy_def_state_def
Print.of_toy_def_pp_core_def
Print.of_toy_def_pre_post_def
Print.of_toy_list_attr.simps
Print.of_toy_data_shallow.simps
end