Theory Haskell_Show

section ‹ Show class for code generation ›

theory Haskell_Show
  imports "HOL-Library.Code_Target_Int" "HOL-Library.Code_Target_Nat"
begin

text ‹ The aim of this theory is support code generation of serialisers for datatypes using the
  Haskell show class. We take inspiration from 🌐‹https://www.isa-afp.org/entries/Show.html›, but
  we are more interested in code generation than being able to derive the show function for 
  any algebraic datatype. Sometimes we give actual instance that can reasoned about in Isabelle,
  but mostly opaque types and code printing to Haskell instance is sufficient. ›

subsection ‹ Show class ›

text ‹ The following class should correspond to the Haskell type class Show, but currently it
       has only part of the signature. ›

class "show" =
  fixes "show" :: "'a ⇒ String.literal" ― ‹ We use @{typ String.literal} for code generation ›

text ‹ We set up code printing so that this class, and the constants therein, are mapped to the
  Haskell Show class. ›

code_printing
  type_class "show" ⇀ (Haskell) "Prelude.Show"
| constant "show" ⇀ (Haskell) "Prelude.show"

subsection ‹ Instances ›

text ‹ We create an instance for bool, that generates an Isabelle function. ›

instantiation bool :: "show"
begin

fun show_bool :: "bool ⇒ String.literal" where
"show_bool True = STR ''True''" |
"show_bool False = STR ''False''"

instance ..

end

text ‹ We map the instance for bool to the built-in Haskell show, and have the code generator
  use the built-in class instance. ›

code_printing
  constant "show_bool_inst.show_bool" ⇀ (Haskell) "Prelude.show"
| class_instance "bool" :: "show" ⇀ (Haskell) -

instantiation unit :: "show"
begin

fun show_unit :: "unit ⇒ String.literal" where
"show_unit () = STR ''()''"

instance ..

end

code_printing
  constant "show_unit_inst.show_unit" ⇀ (Haskell) "Prelude.show"
| class_instance "unit" :: "show" ⇀ (Haskell) -

text ‹ Actually, we don't really need to create the show function if all we're interested in is
  code generation. Here, for the @{typ integer} instance, we omit the definition. This is
  because @{typ integer} is set up to correspond to the built-in Haskell type Integer, which
  already has a Show instance. ›

instantiation integer :: "show"
begin

instance ..

end

text ‹ For the code generator, the crucial line follows. This maps the (unspecified) Isabelle show
  function to the Haskell show function, which is built-in. We also specify that no instance of
  Show should be generated for integer, as it exists already. ›

code_printing
  constant "show_integer_inst.show_integer" ⇀ (Haskell) "Prelude.show"
| class_instance "integer" :: "show" ⇀ (Haskell) -

text ‹ For @{typ int}, we are effectively dealing with a packaged version of @{typ integer} in
  the code generation set up. So, we simply define show in terms of the "underlying" integer
  using @{const integer_of_int}. ›

instantiation int :: "show"
begin

definition show_int :: "int ⇒ String.literal" where
"show_int x = show (integer_of_int x)"

instance ..

end

text ‹ As a result, we can prove a code equation that will mean that our show instance for @{typ int}
  simply calls the built-in show function for @{typ integer}. ›

lemma show_int_of_integer [code]: "show (int_of_integer x) = show x" 
  by (simp add: show_int_def)

instantiation nat :: "show"
begin

definition show_nat :: "nat ⇒ String.literal" where
"show_nat x = show (integer_of_nat x)"

instance ..

end

lemma show_Nat: "show (Nat x) = show (max 0 x)"
  using Code_Target_Nat.Nat_def integer_of_nat_eq_of_nat nat_of_integer_def of_nat_of_integer show_nat_def by presburger
  
instantiation String.literal :: "show"
begin

definition show_literal :: "String.literal ⇒ String.literal" where
"show_literal x = STR ''\"'' + x + STR ''\"''"

instance ..

end

code_printing
  constant "show_literal_inst.show_literal" ⇀ (Haskell) "Prelude.show"
| class_instance "String.literal" :: "show" ⇀ (Haskell) -


instantiation prod :: ("show", "show") "show"
begin

instance ..

end

code_printing
  constant "show_prod_inst.show_prod" ⇀ (Haskell) "Prelude.show"
| class_instance "prod" :: "show" ⇀ (Haskell) -

instantiation list :: ("show") "show"
begin

instance ..

end

code_printing
  constant "show_list_inst.show_list" ⇀ (Haskell) "Prelude.show"
| class_instance "list" :: "show" ⇀ (Haskell) -

end