adjusted syntax for internal code generation
authorhaftmann
Mon Nov 27 13:42:30 2006 +0100 (2006-11-27)
changeset 2154554cc492d80a9
parent 21544 a9ceeb182cfc
child 21546 268b6bed0cc8
adjusted syntax for internal code generation
NEWS
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
src/HOL/Extraction/Higman.thy
src/HOL/Extraction/Pigeonhole.thy
src/HOL/Extraction/QuotRem.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/ex/Classpackage.thy
src/HOL/ex/CodeCollections.thy
src/HOL/ex/CodeRandom.thy
src/HOL/ex/Codegenerator.thy
     1.1 --- a/NEWS	Mon Nov 27 12:12:18 2006 +0100
     1.2 +++ b/NEWS	Mon Nov 27 13:42:30 2006 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  code for ML and Haskell (including "class"es). A short usage sketch:
     1.5  
     1.6      internal compilation:
     1.7 -        code_gen <list of constants (term syntax)> (SML *)
     1.8 +        code_gen <list of constants (term syntax)> (SML #)
     1.9      writing SML code to a file:
    1.10          code_gen <list of constants (term syntax)> (SML <filename>)
    1.11      writing Haskell code to a bunch of files:
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 27 12:12:18 2006 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 27 13:42:30 2006 +0100
     2.3 @@ -153,7 +153,7 @@
     2.4    This executable specification is now turned to SML code:
     2.5  *}
     2.6  
     2.7 -code_gen fac (*<*)(SML *)(*>*)(SML "examples/fac.ML")
     2.8 +code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML")
     2.9  
    2.10  text {*
    2.11    The @{text "\<CODEGEN>"} command takes a space-separated list of
    2.12 @@ -269,7 +269,7 @@
    2.13    "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
    2.14    by simp
    2.15  
    2.16 -code_gen pick (*<*)(SML *)(*>*)(SML "examples/pick1.ML")
    2.17 +code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML")
    2.18  
    2.19  text {*
    2.20    This theorem is now added to the function equation table:
    2.21 @@ -282,7 +282,7 @@
    2.22  
    2.23  lemmas [code nofunc] = pick.simps 
    2.24  
    2.25 -code_gen pick (*<*)(SML *)(*>*)(SML "examples/pick2.ML")
    2.26 +code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick2.ML")
    2.27  
    2.28  text {*
    2.29    \lstsml{Thy/examples/pick2.ML}
    2.30 @@ -298,7 +298,7 @@
    2.31    "fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)"
    2.32    by (cases n) simp_all
    2.33  
    2.34 -code_gen fac (*<*)(SML *)(*>*)(SML "examples/fac_case.ML")
    2.35 +code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac_case.ML")
    2.36  
    2.37  text {*
    2.38    \lstsml{Thy/examples/fac_case.ML}
    2.39 @@ -377,7 +377,7 @@
    2.40    The whole code in SML with explicit dictionary passing:
    2.41  *}
    2.42  
    2.43 -code_gen dummy (*<*)(SML *)(*>*)(SML "examples/class.ML")
    2.44 +code_gen dummy (*<*)(SML #)(*>*)(SML "examples/class.ML")
    2.45  
    2.46  text {*
    2.47    \lstsml{Thy/examples/class.ML}
    2.48 @@ -557,7 +557,7 @@
    2.49    (SML and and and)
    2.50  (*>*)
    2.51  
    2.52 -code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_literal.ML")
    2.53 +code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML")
    2.54  
    2.55  text {*
    2.56    \lstsml{Thy/examples/bool_literal.ML}
    2.57 @@ -600,7 +600,7 @@
    2.58    After this setup, code looks quite more readable:
    2.59  *}
    2.60  
    2.61 -code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_mlbool.ML")
    2.62 +code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_mlbool.ML")
    2.63  
    2.64  text {*
    2.65    \lstsml{Thy/examples/bool_mlbool.ML}
    2.66 @@ -616,7 +616,7 @@
    2.67  code_const %tt "op \<and>"
    2.68    (SML infixl 1 "andalso")
    2.69  
    2.70 -code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_infix.ML")
    2.71 +code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_infix.ML")
    2.72  
    2.73  text {*
    2.74    \lstsml{Thy/examples/bool_infix.ML}
    2.75 @@ -675,7 +675,7 @@
    2.76      and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    2.77    (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)")
    2.78  
    2.79 -code_gen double_inc (*<*)(SML *)(*>*)(SML "examples/integers.ML")
    2.80 +code_gen double_inc (*<*)(SML #)(*>*)(SML "examples/integers.ML")
    2.81  
    2.82  text {*
    2.83    resulting in:
    2.84 @@ -727,7 +727,7 @@
    2.85    performs an explicit equality check.
    2.86  *}
    2.87  
    2.88 -code_gen collect_duplicates (*<*)(SML *)(*>*)(SML "examples/collect_duplicates.ML")
    2.89 +code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML")
    2.90  
    2.91  text {*
    2.92    \lstsml{Thy/examples/collect_duplicates.ML}
    2.93 @@ -803,7 +803,7 @@
    2.94    Then everything goes fine:
    2.95  *}
    2.96  
    2.97 -code_gen lookup (*<*)(SML *)(*>*)(SML "examples/lookup.ML")
    2.98 +code_gen lookup (*<*)(SML #)(*>*)(SML "examples/lookup.ML")
    2.99  
   2.100  text {*
   2.101    \lstsml{Thy/examples/lookup.ML}
   2.102 @@ -856,7 +856,7 @@
   2.103  *}
   2.104  
   2.105  code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord} \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   2.106 -  (*<*)(SML *)(*>*)(SML "examples/lexicographic.ML")
   2.107 +  (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
   2.108  
   2.109  text {*
   2.110    \lstsml{Thy/examples/lexicographic.ML}
   2.111 @@ -960,7 +960,7 @@
   2.112  lemma [code func]:
   2.113    "insert = insert" ..
   2.114  
   2.115 -code_gen dummy_set foobar_set (*<*)(SML *)(*>*)(SML "examples/dirty_set.ML")
   2.116 +code_gen dummy_set foobar_set (*<*)(SML #)(*>*)(SML "examples/dirty_set.ML")
   2.117  
   2.118  text {*
   2.119    \lstsml{Thy/examples/dirty_set.ML}
   2.120 @@ -1087,7 +1087,7 @@
   2.121  declare dummy_option.simps [code func]
   2.122  (*>*)
   2.123  
   2.124 -code_gen dummy_option (*<*)(SML *)(*>*)(SML "examples/arbitrary.ML")
   2.125 +code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML")
   2.126  
   2.127  text {*
   2.128    \lstsml{Thy/examples/arbitrary.ML}
     3.1 --- a/src/HOL/Extraction/Higman.thy	Mon Nov 27 12:12:18 2006 +0100
     3.2 +++ b/src/HOL/Extraction/Higman.thy	Mon Nov 27 13:42:30 2006 +0100
     3.3 @@ -337,7 +337,7 @@
     3.4  end;
     3.5  *}
     3.6  
     3.7 -code_gen good_prefix (SML *)
     3.8 +code_gen good_prefix (SML #)
     3.9  
    3.10  ML {*
    3.11  local
     4.1 --- a/src/HOL/Extraction/Pigeonhole.thy	Mon Nov 27 12:12:18 2006 +0100
     4.2 +++ b/src/HOL/Extraction/Pigeonhole.thy	Mon Nov 27 13:42:30 2006 +0100
     4.3 @@ -316,7 +316,7 @@
     4.4  definition
     4.5    "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
     4.6  
     4.7 -code_gen test test' "op !" (SML *)
     4.8 +code_gen test test' "op !" (SML #)
     4.9  
    4.10  ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
    4.11  ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
     5.1 --- a/src/HOL/Extraction/QuotRem.thy	Mon Nov 27 12:12:18 2006 +0100
     5.2 +++ b/src/HOL/Extraction/QuotRem.thy	Mon Nov 27 13:42:30 2006 +0100
     5.3 @@ -49,6 +49,6 @@
     5.4  contains
     5.5    test = "division 9 2"
     5.6  
     5.7 -code_gen division (SML *)
     5.8 +code_gen division (SML #)
     5.9  
    5.10  end
     6.1 --- a/src/HOL/Library/ExecutableRat.thy	Mon Nov 27 12:12:18 2006 +0100
     6.2 +++ b/src/HOL/Library/ExecutableRat.thy	Mon Nov 27 13:42:30 2006 +0100
     6.3 @@ -137,7 +137,7 @@
     6.4    "inverse \<Colon> rat \<Rightarrow> rat"
     6.5    "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
     6.6    "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
     6.7 -  (SML *)
     6.8 +  (SML #)
     6.9  
    6.10  
    6.11  section {* type serializations *}
     7.1 --- a/src/HOL/ex/Classpackage.thy	Mon Nov 27 12:12:18 2006 +0100
     7.2 +++ b/src/HOL/ex/Classpackage.thy	Mon Nov 27 13:42:30 2006 +0100
     7.3 @@ -320,7 +320,7 @@
     7.4  definition "y2 = Y (1::int) 2 3"
     7.5  
     7.6  code_gen "op \<otimes>" \<one> inv
     7.7 -code_gen X Y (SML *) (Haskell -)
     7.8 -code_gen x1 x2 y2 (SML *) (Haskell -)
     7.9 +code_gen X Y (SML #) (Haskell -)
    7.10 +code_gen x1 x2 y2 (SML #) (Haskell -)
    7.11  
    7.12  end
     8.1 --- a/src/HOL/ex/CodeCollections.thy	Mon Nov 27 12:12:18 2006 +0100
     8.2 +++ b/src/HOL/ex/CodeCollections.thy	Mon Nov 27 13:42:30 2006 +0100
     8.3 @@ -198,7 +198,7 @@
     8.4  
     8.5  code_gen test3
     8.6  
     8.7 -code_gen (SML *)
     8.8 +code_gen (SML #)
     8.9  code_gen (Haskell -)
    8.10  
    8.11  end
    8.12 \ No newline at end of file
     9.1 --- a/src/HOL/ex/CodeRandom.thy	Mon Nov 27 12:12:18 2006 +0100
     9.2 +++ b/src/HOL/ex/CodeRandom.thy	Mon Nov 27 13:42:30 2006 +0100
     9.3 @@ -187,7 +187,7 @@
     9.4    (SML "case _ (Random.seed ()) of (x, '_) => x")
     9.5  
     9.6  code_gen select select_weight
     9.7 -  (SML *)
     9.8 +  (SML #)
     9.9  
    9.10  code_gen (SML -)
    9.11  
    10.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Nov 27 12:12:18 2006 +0100
    10.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Nov 27 13:42:30 2006 +0100
    10.3 @@ -188,6 +188,6 @@
    10.4    "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    10.5    "op = :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
    10.6  
    10.7 -code_gen (SML *) (Haskell -)
    10.8 +code_gen (SML #) (Haskell -)
    10.9  
   10.10  end
   10.11 \ No newline at end of file