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


ML_val‹Isabelle_System.bash "echo ${ISABELLE_TMP} > ${ISABELLE_TMP}/self"›
text‹
During the build of this session, the code generated in the following subsections will be
written to
›
text_raw‹\verbatiminput{${ISABELLE_TMP}/self}›


subsection‹Haskell›

export_code main in Haskell file "$ISABELLE_TMP/exported_hs"

text‹The generated helper module 🗏‹$ISABELLE_TMP/exported_hs/StdIO.hs› is shown below.›
text_raw‹\verbatiminput{$ISABELLE_TMP/exported_hs/StdIO.hs}›
 
text‹The generated main file 🗏‹$ISABELLE_TMP/exported_hs/HelloWorld.hs› is shown below.›
text_raw‹\verbatiminput{$ISABELLE_TMP/exported_hs/HelloWorld.hs}›


subsection‹SML›

export_code main in SML file "$ISABELLE_TMP/exported.sml"

text‹The generated SML code in 🗏‹$ISABELLE_TMP/exported.sml› is shown below.›
text_raw‹\verbatiminput{$ISABELLE_TMP/exported.sml}›


end