src/HOL/Imperative_HOL/ex/Linked_Lists.thy
changeset 37826 4c0a5e35931a
parent 37792 ba0bc31b90d7
child 37828 9e1758c7ff06
equal deleted inserted replaced
37825:adc1143bc1a8 37826:4c0a5e35931a
   989   show ?case by auto
   989   show ?case by auto
   990 qed
   990 qed
   991 
   991 
   992 section {* Code generation *}
   992 section {* Code generation *}
   993 
   993 
   994 export_code merge in SML file -
       
   995 
       
   996 export_code rev in SML file -
       
   997 
       
   998 text {* A simple example program *}
   994 text {* A simple example program *}
   999 
   995 
  1000 definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
   996 definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
  1001 definition test_2 where "test_2 = (do { ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys })"
   997 definition test_2 where "test_2 = (do { ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys })"
  1002 
   998 
  1016 
  1012 
  1017 ML {* @{code test_1} () *}
  1013 ML {* @{code test_1} () *}
  1018 ML {* @{code test_2} () *}
  1014 ML {* @{code test_2} () *}
  1019 ML {* @{code test_3} () *}
  1015 ML {* @{code test_3} () *}
  1020 
  1016 
  1021 export_code test_1 test_2 test_3 in SML_imp module_name QSort file -
  1017 export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell?
  1022 export_code test_1 test_2 test_3 in OCaml module_name QSort file -
       
  1023 export_code test_1 test_2 test_3 in OCaml_imp module_name QSort file -
       
  1024 export_code test_1 test_2 test_3 in Haskell module_name QSort file -
       
  1025 
  1018 
  1026 end
  1019 end