Theory HelloWorld

theory HelloWorld
  imports IO
begin

section‹Hello, World!›

text‹
  The idea of a \<^term>‹main :: unit io› function is that, upon start of your program, you will be
  handed a value of type \<^typ>‹🌐›. You can pass this world through your code and modify it.
  Be careful with the \<^typ>‹🌐›, it's the only one we have.
›


text‹The main function, defined in Isabelle. It should have the right type in Haskell.›
definition main :: "unit io" where
  "main ≡ do {
               _ ← println (STR ''Hello World! What is your name?'');
               name ← getLine;
               println (STR ''Hello, '' + name + STR ''!'')
             }"


section‹Generating Code›

text‹Checking that the generated code compiles.›

export_code main checking Haskell? SML

(*<*)
setup ‹
let
  val parser =
    Scan.repeat (Args.const {proper = true, strict = true}) --
      Scan.lift (\<^keyword>‹in› |-- Parse.name -- (\<^keyword>‹module_name› |-- Parse.name))

  fun action ctxt (consts, (target, module)) =
    Code_Target.produce_code ctxt false consts target module NONE []
    |> fst
    |> map (Bytes.content o snd) |> String.concatWith "\n"
in
  Document_Output.antiquotation_verbatim @{binding code} parser action
end›
(*>*)

subsection‹Haskell›

text‹The generated code in Haskell (including the prelude) is shown below.›

text_raw‹@{code main in Haskell module_name HelloWorld}›

subsection‹SML›

text‹The generated code in SML (including the prelude) is shown below.›

text_raw‹@{code main in SML module_name HelloWorld}›

end