Theory Printer_Isabelle
section‹Instantiating the Printer for Isabelle›
theory Printer_Isabelle
imports Meta_Isabelle
Printer_Pure
Printer_SML
begin
context Print
begin
fun of_semi__typ where "of_semi__typ e = (λ
Typ_base s ⇒ To_string s
| Typ_apply name l ⇒ ‹%s %s› (let s = String_concat ‹, › (List.map of_semi__typ l) in
case l of [_] ⇒ s | _ ⇒ ‹(%s)› s)
(of_semi__typ name)
| Typ_apply_bin s ty1 ty2 ⇒ ‹%s %s %s› (of_semi__typ ty1) (To_string s) (of_semi__typ ty2)
| Typ_apply_paren s1 s2 ty ⇒ ‹%s%s%s› (To_string s1) (of_semi__typ ty) (To_string s2)) e"
definition "of_datatype _ = (λ Datatype n l ⇒
‹datatype %s = %s›
(To_string n)
(String_concat ‹
| ›
(L.map
(λ(n,l).
‹%s %s›
(To_string n)
(String_concat ‹ › (L.map (λx. ‹\"%s\"› (of_semi__typ x)) l))) l) ))"
definition "of_type_synonym _ = (λ Type_synonym n v l ⇒
‹type_synonym %s = \"%s\"› (if v = [] then
To_string n
else
of_semi__typ (Typ_apply (Typ_base n) (L.map Typ_base v)))
(of_semi__typ l))"
fun of_semi__term where "of_semi__term e = (λ
Term_rewrite e1 symb e2 ⇒ ‹%s %s %s› (of_semi__term e1) (To_string symb) (of_semi__term e2)
| Term_basic l ⇒ ‹%s› (String_concat ‹ › (L.map To_string l))
| Term_annot e s ⇒ ‹(%s::%s)› (of_semi__term e) (of_semi__typ s)
| Term_bind symb e1 e2 ⇒ ‹(%s%s. %s)› (To_string symb) (of_semi__term e1) (of_semi__term e2)
| Term_fun_case e_case l ⇒ ‹(%s %s)›
(case e_case of None ⇒ ‹λ›
| Some e ⇒ ‹case %s of› (of_semi__term e))
(String_concat ‹
| › (List.map (λ (s1, s2) ⇒ ‹%s ⇒ %s› (of_semi__term s1) (of_semi__term s2)) l))
| Term_apply e l ⇒ ‹%s %s› (of_semi__term e) (String_concat ‹ › (List.map (λ e ⇒ ‹%s› (of_semi__term e)) l))
| Term_paren p_left p_right e ⇒ ‹%s%s%s› (To_string p_left) (of_semi__term e) (To_string p_right)
| Term_if_then_else e_if e_then e_else ⇒ ‹if %s then %s else %s› (of_semi__term e_if) (of_semi__term e_then) (of_semi__term e_else)
| Term_term l pure ⇒ of_pure_term (L.map To_string l) pure) e"
definition "of_type_notation _ = (λ Type_notation n e ⇒
‹type_notation %s (\"%s\")› (To_string n) (To_string e))"
definition "of_instantiation _ = (λ Instantiation n n_def expr ⇒
let name = To_string n in
‹instantiation %s :: object
begin
definition %s_%s_def : \"%s\"
instance ..
end›
name
(To_string n_def)
name
(of_semi__term expr))"
definition "of_overloading _ = (λ Overloading n_c e_c n e ⇒
‹overloading %s ≡ \"%s\"
begin
definition %s : \"%s\"
end› (To_string n_c) (of_semi__term e_c) (To_string n) (of_semi__term e))"
definition "of_consts _ = (λ Consts n ty symb ⇒
‹consts %s :: \"%s\" (\"%s %s\")› (To_string n) (of_semi__typ ty) (To_string Consts_value) (To_string symb))"
definition "of_definition _ = (λ
Definition e ⇒ ‹definition \"%s\"› (of_semi__term e)
| Definition_where1 name (abbrev, prio) e ⇒ ‹definition %s (\"(1%s)\" %d)
where \"%s\"› (To_string name) (of_semi__term abbrev) (To_nat prio) (of_semi__term e)
| Definition_where2 name abbrev e ⇒ ‹definition %s (\"%s\")
where \"%s\"› (To_string name) (of_semi__term abbrev) (of_semi__term e))"
definition "(of_semi__thm_attribute_aux_gen :: String.literal × String.literal ⇒ _ ⇒ _ ⇒ _) m lacc s =
(let s_base = (λs lacc. ‹%s[%s]› (To_string s) (String_concat ‹, › (L.map (λ(s, x). ‹%s %s› s x) lacc))) in
s_base s (m # lacc))"
definition "of_semi__thm_attribute_aux_gen_where l =
(‹where›, String_concat ‹ and › (L.map (λ(var, expr). ‹%s = \"%s\"›
(To_string var)
(of_semi__term expr)) l))"
definition "of_semi__thm_attribute_aux_gen_of l =
(‹of›, String_concat ‹ › (L.map (λexpr. ‹\"%s\"› (of_semi__term expr)) l))"
fun of_semi__thm_attribute_aux where "of_semi__thm_attribute_aux lacc e =
(λ Thm_thm s ⇒ To_string s
| Thm_thms s ⇒ To_string s
| Thm_THEN (Thm_thm s) e2 ⇒ of_semi__thm_attribute_aux_gen (‹THEN›, of_semi__thm_attribute_aux [] e2) lacc s
| Thm_THEN (Thm_thms s) e2 ⇒ of_semi__thm_attribute_aux_gen (‹THEN›, of_semi__thm_attribute_aux [] e2) lacc s
| Thm_THEN e1 e2 ⇒ of_semi__thm_attribute_aux ((‹THEN›, of_semi__thm_attribute_aux [] e2) # lacc) e1
| Thm_simplified (Thm_thm s) e2 ⇒ of_semi__thm_attribute_aux_gen (‹simplified›, of_semi__thm_attribute_aux [] e2) lacc s
| Thm_simplified (Thm_thms s) e2 ⇒ of_semi__thm_attribute_aux_gen (‹simplified›, of_semi__thm_attribute_aux [] e2) lacc s
| Thm_simplified e1 e2 ⇒ of_semi__thm_attribute_aux ((‹simplified›, of_semi__thm_attribute_aux [] e2) # lacc) e1
| Thm_symmetric (Thm_thm s) ⇒ of_semi__thm_attribute_aux_gen (‹symmetric›, ‹›) lacc s
| Thm_symmetric (Thm_thms s) ⇒ of_semi__thm_attribute_aux_gen (‹symmetric›, ‹›) lacc s
| Thm_symmetric e1 ⇒ of_semi__thm_attribute_aux ((‹symmetric›, ‹›) # lacc) e1
| Thm_where (Thm_thm s) l ⇒ of_semi__thm_attribute_aux_gen (of_semi__thm_attribute_aux_gen_where l) lacc s
| Thm_where (Thm_thms s) l ⇒ of_semi__thm_attribute_aux_gen (of_semi__thm_attribute_aux_gen_where l) lacc s
| Thm_where e1 l ⇒ of_semi__thm_attribute_aux (of_semi__thm_attribute_aux_gen_where l # lacc) e1
| Thm_of (Thm_thm s) l ⇒ of_semi__thm_attribute_aux_gen (of_semi__thm_attribute_aux_gen_of l) lacc s
| Thm_of (Thm_thms s) l ⇒ of_semi__thm_attribute_aux_gen (of_semi__thm_attribute_aux_gen_of l) lacc s
| Thm_of e1 l ⇒ of_semi__thm_attribute_aux (of_semi__thm_attribute_aux_gen_of l # lacc) e1
| Thm_OF (Thm_thm s) e2 ⇒ of_semi__thm_attribute_aux_gen (‹OF›, of_semi__thm_attribute_aux [] e2) lacc s
| Thm_OF (Thm_thms s) e2 ⇒ of_semi__thm_attribute_aux_gen (‹OF›, of_semi__thm_attribute_aux [] e2) lacc s
| Thm_OF e1 e2 ⇒ of_semi__thm_attribute_aux ((‹OF›, of_semi__thm_attribute_aux [] e2) # lacc) e1) e"
definition "of_semi__thm_attribute = of_semi__thm_attribute_aux []"
definition "of_semi__thm = (λ Thms_single thy ⇒ of_semi__thm_attribute thy
| Thms_mult thy ⇒ of_semi__thm_attribute thy)"
definition "of_semi__thm_attribute_l l = String_concat ‹
› (L.map of_semi__thm_attribute l)"
definition "of_semi__thm_attribute_l1 l = String_concat ‹ › (L.map of_semi__thm_attribute l)"
definition "of_semi__thm_l l = String_concat ‹ › (L.map of_semi__thm l)"
definition "of_lemmas _ = (λ Lemmas_simp_thm simp s l ⇒
‹lemmas%s%s = %s›
(if String.is_empty s then ‹› else ‹ %s› (To_string s))
(if simp then ‹[simp,code_unfold]› else ‹›)
(of_semi__thm_attribute_l l)
| Lemmas_simp_thms s l ⇒
‹lemmas%s [simp,code_unfold] = %s›
(if String.is_empty s then ‹› else ‹ %s› (To_string s))
(String_concat ‹
› (L.map To_string l)))"
definition "(of_semi__attrib_genA :: (semi__thm list ⇒ String.literal)
⇒ String.literal ⇒ semi__thm list ⇒ String.literal) f attr l =
(if l = [] then
‹›
else
‹ %s: %s› attr (f l))"
definition "(of_semi__attrib_genB :: (string list ⇒ String.literal)
⇒ String.literal ⇒ string list ⇒ String.literal) f attr l =
(if l = [] then
‹›
else
‹ %s: %s› attr (f l))"
definition "of_semi__attrib = of_semi__attrib_genA of_semi__thm_l"
definition "of_semi__attrib1 = of_semi__attrib_genB (λl. String_concat ‹ › (L.map To_string l))"
definition "of_semi__method_simp (s ::
String.literal) =
(λ Method_simp_only l ⇒ ‹%s only: %s› s (of_semi__thm_l l)
| Method_simp_add_del_split l1 l2 [] ⇒ ‹%s%s%s›
s
(of_semi__attrib ‹add› l1)
(of_semi__attrib ‹del› l2)
| Method_simp_add_del_split l1 l2 l3 ⇒ ‹%s%s%s%s›
s
(of_semi__attrib ‹add› l1)
(of_semi__attrib ‹del› l2)
(of_semi__attrib ‹split› l3))"
fun of_semi__method where "of_semi__method expr = (λ
Method_rule o_s ⇒ ‹rule%s› (case o_s of None ⇒ ‹›
| Some s ⇒ ‹ %s› (of_semi__thm_attribute s))
| Method_drule s ⇒ ‹drule %s› (of_semi__thm_attribute s)
| Method_erule s ⇒ ‹erule %s› (of_semi__thm_attribute s)
| Method_intro l ⇒ ‹intro %s› (of_semi__thm_attribute_l1 l)
| Method_elim s ⇒ ‹elim %s› (of_semi__thm_attribute s)
| Method_subst asm l s =>
let s_asm = if asm then ‹(asm) › else ‹› in
if L.map String.meta_of_logic l = [STR ''0''] then
‹subst %s%s› s_asm (of_semi__thm_attribute s)
else
‹subst %s(%s) %s› s_asm (String_concat ‹ › (L.map To_string l)) (of_semi__thm_attribute s)
| Method_insert l => ‹insert %s› (of_semi__thm_l l)
| Method_plus t ⇒ ‹(%s)+› (String_concat ‹, › (List.map of_semi__method t))
| Method_option t ⇒ ‹(%s)?› (String_concat ‹, › (List.map of_semi__method t))
| Method_or t ⇒ ‹(%s)› (String_concat ‹ | › (List.map of_semi__method t))
| Method_one s ⇒ of_semi__method_simp ‹simp› s
| Method_all s ⇒ of_semi__method_simp ‹simp_all› s
| Method_auto_simp_add_split l_simp l_split ⇒ ‹auto%s%s›
(of_semi__attrib ‹simp› l_simp)
(of_semi__attrib1 ‹split› l_split)
| Method_rename_tac l ⇒ ‹rename_tac %s› (String_concat ‹ › (L.map To_string l))
| Method_case_tac e ⇒ ‹case_tac \"%s\"› (of_semi__term e)
| Method_blast None ⇒ ‹blast›
| Method_blast (Some n) ⇒ ‹blast %d› (To_nat n)
| Method_clarify ⇒ ‹clarify›
| Method_metis l_opt l ⇒ ‹metis %s%s› (if l_opt = [] then ‹›
else
‹(%s) › (String_concat ‹, › (L.map To_string l_opt))) (of_semi__thm_attribute_l1 l)) expr"
definition "of_semi__command_final = (λ Command_done ⇒ ‹done›
| Command_by l_apply ⇒ ‹by(%s)› (String_concat ‹, › (L.map of_semi__method l_apply))
| Command_sorry ⇒ ‹sorry›)"
definition "of_semi__command_state = (
λ Command_apply_end [] ⇒ ‹›
| Command_apply_end l_apply ⇒ ‹ apply_end(%s)
› (String_concat ‹, › (L.map of_semi__method l_apply)))"
definition ‹of_semi__command_proof = (
let thesis = ‹?thesis›
; scope_thesis_gen = λproof show when. ‹ proof - %s show %s%s
› proof
show
(if when = [] then
‹›
else
‹ when %s› (String_concat ‹ › (L.map (λt. ‹"%s"› (of_semi__term t)) when)))
; scope_thesis = λs. scope_thesis_gen s thesis [] in
λ Command_apply [] ⇒ ‹›
| Command_apply l_apply ⇒ ‹ apply(%s)
› (String_concat ‹, › (L.map of_semi__method l_apply))
| Command_using l ⇒ ‹ using %s
› (of_semi__thm_l l)
| Command_unfolding l ⇒ ‹ unfolding %s
› (of_semi__thm_l l)
| Command_let e_name e_body ⇒ scope_thesis (‹let %s = "%s"› (of_semi__term e_name) (of_semi__term e_body))
| Command_have n b e e_last ⇒ scope_thesis (‹have %s%s: "%s" %s› (To_string n) (if b then ‹[simp]› else ‹›) (of_semi__term e) (of_semi__command_final e_last))
| Command_fix_let l l_let o_show _ ⇒
scope_thesis_gen
(‹fix %s%s› (String_concat ‹ › (L.map To_string l))
(String_concat ‹
› (L.map
(λ(e_name, e_body).
‹ let %s = "%s"› (of_semi__term e_name) (of_semi__term e_body))
l_let)))
(case o_show of None ⇒ thesis
| Some (l_show, _) ⇒ ‹"%s"› (String_concat ‹ ⟹ › (L.map of_semi__term l_show)))
(case o_show of None ⇒ [] | Some (_, l_when) ⇒ l_when))›
definition "of_lemma _ =
(λ Lemma n l_spec l_apply tactic_last ⇒
‹lemma %s : \"%s\"
%s%s›
(To_string n)
(String_concat ‹ ⟹ › (L.map of_semi__term l_spec))
(String_concat ‹› (L.map (λ [] ⇒ ‹› | l_apply ⇒ ‹ apply(%s)
›
(String_concat ‹, › (L.map of_semi__method l_apply)))
l_apply))
(of_semi__command_final tactic_last)
| Lemma_assumes n l_spec concl l_apply tactic_last ⇒
‹lemma %s : %s
%s%s %s›
(To_string n)
(String_concat ‹› (L.map (λ(n, b, e).
‹
assumes %s\"%s\"›
(let (n, b) = if b then (‹%s[simp]› (To_string n), False) else (To_string n, String.is_empty n) in
if b then ‹› else ‹%s: › n)
(of_semi__term e)) l_spec
@@@@
[‹
shows \"%s\"› (of_semi__term concl)]))
(String_concat ‹› (L.map of_semi__command_proof l_apply))
(of_semi__command_final tactic_last)
(String_concat ‹ ›
(L.map
(λl_apply_e.
‹%sqed›
(if l_apply_e = [] then
‹›
else
‹
%s ›
(String_concat ‹› (L.map of_semi__command_state l_apply_e))))
(List.map_filter
(λ Command_let _ _ ⇒ Some [] | Command_have _ _ _ _ ⇒ Some [] | Command_fix_let _ _ _ l ⇒ Some l | _ ⇒ None)
(rev l_apply)))))"
definition "of_axiomatization _ = (λ Axiomatization n e ⇒ ‹axiomatization where %s:
\"%s\"› (To_string n) (of_semi__term e))"
definition "of_section _ = (λ Section n section_title ⇒
‹%s ‹%s››
(‹%ssection› (if n = 0 then ‹›
else if n = 1 then ‹sub›
else ‹subsub›))
(To_string section_title))"
definition "of_text _ = (λ Text s ⇒ ‹text ‹%s›› (To_string s))"
definition "of_ML _ = (λ SML e ⇒ ‹ML ‹%s›› (of_semi__term' e))"
definition "of_setup _ = (λ Setup e ⇒ ‹setup ‹%s›› (of_semi__term' e))"
definition "of_thm _ = (λ Thm thm ⇒ ‹thm %s› (of_semi__thm_attribute_l1 thm))"
definition ‹of_interpretation _ = (λ Interpretation n loc_n loc_param tac ⇒
‹interpretation %s: %s%s
%s› (To_string n)
(To_string loc_n)
(String_concat ‹› (L.map (λs. ‹ "%s"› (of_semi__term s)) loc_param))
(of_semi__command_final tac))›
definition "of_semi__theory env =
(λ Theory_datatype dataty ⇒ of_datatype env dataty
| Theory_type_synonym ty_synonym ⇒ of_type_synonym env ty_synonym
| Theory_type_notation ty_notation ⇒ of_type_notation env ty_notation
| Theory_instantiation instantiation_class ⇒ of_instantiation env instantiation_class
| Theory_overloading overloading ⇒ of_overloading env overloading
| Theory_consts consts_class ⇒ of_consts env consts_class
| Theory_definition definition_hol ⇒ of_definition env definition_hol
| Theory_lemmas lemmas_simp ⇒ of_lemmas env lemmas_simp
| Theory_lemma lemma_by ⇒ of_lemma env lemma_by
| Theory_axiomatization axiom ⇒ of_axiomatization env axiom
| Theory_section section_title ⇒ of_section env section_title
| Theory_text text ⇒ of_text env text
| Theory_ML ml ⇒ of_ML env ml
| Theory_setup setup ⇒ of_setup env setup
| Theory_thm thm ⇒ of_thm env thm
| Theory_interpretation thm ⇒ of_interpretation env thm)"
definition "String_concat_map s f l = String_concat s (L.map f l)"
definition ‹of_semi__theories env =
(λ Theories_one t ⇒ of_semi__theory env t
| Theories_locale data l ⇒
‹locale %s =
%s
begin
%s
end› (To_string (HolThyLocale_name data))
(String_concat_map
‹
›
(λ (l_fix, o_assum).
‹%s%s› (String_concat_map ‹
› (λ(e, ty). ‹fixes "%s" :: "%s"› (of_semi__term e) (of_semi__typ ty)) l_fix)
(case o_assum of None ⇒ ‹›
| Some (name, e) ⇒ ‹
assumes %s: "%s"› (To_string name) (of_semi__term e)))
(HolThyLocale_header data))
(String_concat_map ‹
› (String_concat_map ‹
› (of_semi__theory env)) l))›
end
lemmas [code] =
Print.of_datatype_def
Print.of_type_synonym_def
Print.of_type_notation_def
Print.of_instantiation_def
Print.of_overloading_def
Print.of_consts_def
Print.of_definition_def
Print.of_semi__thm_attribute_aux_gen_def
Print.of_semi__thm_attribute_aux_gen_where_def
Print.of_semi__thm_attribute_aux_gen_of_def
Print.of_semi__thm_attribute_def
Print.of_semi__thm_def
Print.of_semi__thm_attribute_l_def
Print.of_semi__thm_attribute_l1_def
Print.of_semi__thm_l_def
Print.of_lemmas_def
Print.of_semi__attrib_genA_def
Print.of_semi__attrib_genB_def
Print.of_semi__attrib_def
Print.of_semi__attrib1_def
Print.of_semi__method_simp_def
Print.of_semi__command_final_def
Print.of_semi__command_state_def
Print.of_semi__command_proof_def
Print.of_lemma_def
Print.of_axiomatization_def
Print.of_section_def
Print.of_text_def
Print.of_ML_def
Print.of_setup_def
Print.of_thm_def
Print.of_interpretation_def
Print.of_semi__theory_def
Print.String_concat_map_def
Print.of_semi__theories_def
Print.of_semi__typ.simps
Print.of_semi__term.simps
Print.of_semi__thm_attribute_aux.simps
Print.of_semi__method.simps
end