--- a/src/HOL/Integ/IntArith.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/Integ/IntArith.thy Tue Oct 31 09:28:56 2006 +0100
@@ -424,27 +424,27 @@
*}
code_type bit
- (SML target_atom "bool")
- (Haskell target_atom "Bool")
+ (SML "bool")
+ (Haskell "Bool")
code_const "Numeral.bit.B0" and "Numeral.bit.B1"
- (SML target_atom "false" and target_atom "true")
- (Haskell target_atom "False" and target_atom "True")
+ (SML "false" and "true")
+ (Haskell "False" and "True")
code_const "number_of \<Colon> int \<Rightarrow> int"
and "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
and "Numeral.succ" and "Numeral.pred"
(SML "_"
- and target_atom "(0 : IntInf.int)"
- and target_atom "(~1 : IntInf.int)"
- and target_atom "(_; _; raise FAIL \"BIT\")"
- and target_atom "(IntInf.+ (_, 1))"
- and target_atom "(IntInf.- (_, 1))")
+ and "0/ :/ IntInf.int"
+ and "~1/ :/ IntInf.int"
+ and "(_; _; raise FAIL \"BIT\")"
+ and "IntInf.+/ (_,/ 1)"
+ and "IntInf.-/ (_,/ 1))")
(Haskell "_"
- and target_atom "0"
- and target_atom "(negate 1)"
- and target_atom "(error \"BIT\")"
- and target_atom "(_ + 1)"
- and target_atom "(_ - 1)")
+ and "0"
+ and "negate/ 1"
+ and "error/ \"BIT\""
+ and "(+)/ 1"
+ and "(-)/ _/ 1")
setup {*
CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_numeral Numeral.int_of_numeral)
--- a/src/HOL/Integ/IntDef.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Tue Oct 31 09:28:56 2006 +0100
@@ -909,14 +909,14 @@
instance int :: eq ..
code_type int
- (SML target_atom "IntInf.int")
- (Haskell target_atom "Integer")
+ (SML "IntInf.int")
+ (Haskell "Integer")
code_instance int :: eq
(Haskell -)
code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- (SML "(op =) (_ : IntInf.int, _)")
+ (SML "!((_ : IntInf.int) = _)")
(Haskell infixl 4 "==")
code_const "op <= \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
@@ -940,8 +940,8 @@
(Haskell infixl 7 "*")
code_const "uminus \<Colon> int \<Rightarrow> int"
- (SML target_atom "IntInf.~")
- (Haskell target_atom "negate")
+ (SML "IntInf.~")
+ (Haskell "negate")
code_reserved SML IntInf
code_reserved Haskell Integer negate
--- a/src/HOL/Library/EfficientNat.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Tue Oct 31 09:28:56 2006 +0100
@@ -129,12 +129,12 @@
*}
code_const "0::nat"
- (SML target_atom "(0 : IntInf.int)")
- (Haskell target_atom "0")
+ (SML "!(0 : IntInf.int)")
+ (Haskell "0")
code_const "Suc"
- (SML "IntInf.op + (__ + 1)")
- (Haskell "(__ + 1)")
+ (SML "IntInf.+ (__, 1)")
+ (Haskell "!(__ + 1)")
setup {*
CodegenData.del_datatype "nat"
@@ -153,8 +153,8 @@
*}
code_type nat
- (SML target_atom "IntInf.int")
- (Haskell target_atom "Integer")
+ (SML "IntInf.int")
+ (Haskell "Integer")
consts_code
"HOL.zero" :: nat ("0")
--- a/src/HOL/Library/MLString.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/Library/MLString.thy Tue Oct 31 09:28:56 2006 +0100
@@ -59,8 +59,8 @@
subsection {* Code serialization *}
code_type ml_string
- (SML target_atom "string")
- (Haskell target_atom "String")
+ (SML "string")
+ (Haskell "String")
code_const STR
(Haskell "_")
@@ -71,7 +71,7 @@
*}
code_const explode
- (SML target_atom "String.explode")
+ (SML "String.explode")
(Haskell "_")
code_reserved SML string explode
--- a/src/HOL/List.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/List.thy Tue Oct 31 09:28:56 2006 +0100
@@ -2651,19 +2651,19 @@
code_type list
(SML "_ list")
- (Haskell target_atom "[_]")
+ (Haskell "![_]")
code_const Nil
- (SML target_atom "[]")
- (Haskell target_atom "[]")
+ (SML "[]")
+ (Haskell "[]")
code_type char
- (SML target_atom "char")
- (Haskell target_atom "Char")
+ (SML "char")
+ (Haskell "Char")
code_const Char
- (SML target_atom "(__,/ __)")
- (Haskell target_atom "(__,/ __)")
+ (SML "!(__,/ __)")
+ (Haskell "!(__,/ __)")
code_instance list :: eq and char :: eq
(Haskell - and -)
@@ -2815,7 +2815,7 @@
lemmas list_bex_code [code unfold] =
list_ex_iff [symmetric, THEN eq_reflection]
-lemma itrev [simp]:
+lemma itrev [simp, normal post]:
"itrev xs ys = rev xs @ ys"
by (induct xs arbitrary: ys) simp_all
@@ -2831,7 +2831,4 @@
"rev xs == itrev xs []"
by simp
-lemmas itrev_rev [normal post] =
- rev_code [symmetric]
-
end
--- a/src/HOL/MicroJava/BV/BVExample.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Tue Oct 31 09:28:56 2006 +0100
@@ -449,7 +449,7 @@
"some_elem" ("hd")
code_const some_elem
- (SML target_atom "hd")
+ (SML "hd")
lemma JVM_sup_unfold [code]:
"JVMType.sup S m n = lift2 (Opt.sup
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Oct 31 09:28:56 2006 +0100
@@ -113,7 +113,7 @@
"next_nam" ("\"next\"")
code_type cnam and vnam and mname and loc_
- (SML target_atom "string" and target_atom "string" and target_atom "string" and target_atom "IntInf.int")
+ (SML "string" and "string" and "string" and "IntInf.int")
instance cnam :: eq
and cname :: eq
@@ -138,15 +138,15 @@
arbitrary_cname \<equiv> object'
code_const list_nam and test_nam and append_name and makelist_name and val_nam and next_nam
- (SML target_atom "\"list\"" and target_atom "\"test\"" and target_atom "\"append\""
- and target_atom "\"makelist\"" and target_atom "\"val\"" and target_atom "\"next\"")
+ (SML "\"list\"" and "\"test\"" and "\"append\""
+ and "\"makelist\"" and "\"val\"" and "\"next\"")
axiomatization
incr_loc :: "loc_ \<Rightarrow> loc_"
and zero_loc :: "loc_"
code_const incr_loc and zero_loc
- (SML target_atom "(_ + 1)" and target_atom "0")
+ (SML "(op +)/ (_, 1)" and "0")
axiomatization
test_loc :: "(loc_ \<Rightarrow> bool) \<Rightarrow> (loc_ \<Rightarrow> 'a) \<Rightarrow> loc_ \<Rightarrow> 'a" where
@@ -155,13 +155,13 @@
definition
new_addr' :: "(loc \<Rightarrow> (cname \<times> (vname \<times> cname \<Rightarrow> val option)) option) \<Rightarrow> loc \<times> val option"
"new_addr' hp =
- test_loc (\<lambda>i. is_none (hp (Loc i) )) (\<lambda>i. (Loc i, None)) zero_loc"
+ test_loc (\<lambda>i. hp (Loc i) = None) (\<lambda>i. (Loc i, None)) zero_loc"
lemma [code func]:
"wf_class = wf_class" ..
code_const
- wf_class (SML target_atom "(fn _ => true)")
+ wf_class (SML "(fn `_ => true)")
code_axioms
new_Addr \<equiv> new_addr'
--- a/src/HOL/ex/CodeEmbed.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/ex/CodeEmbed.thy Tue Oct 31 09:28:56 2006 +0100
@@ -78,7 +78,7 @@
subsection {* Code serialization setup *}
code_type "typ" and "term"
- (SML target_atom "Term.typ" and target_atom "Term.term")
+ (SML "Term.typ" and "Term.term")
code_const Type and TFix
and Const and App and Fix
--- a/src/HOL/ex/CodeRandom.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy Tue Oct 31 09:28:56 2006 +0100
@@ -23,8 +23,10 @@
typedecl randseed
-consts
+axiomatization
random_shift :: "randseed \<Rightarrow> randseed"
+
+axiomatization
random_seed :: "randseed \<Rightarrow> nat"
definition
@@ -124,6 +126,9 @@
"random n s = (let (m, s') = random_int (int n) s in (nat m, s'))"
unfolding random_int_def Let_def split_def random_def by simp
+axiomatization
+ run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a"
+
ML {*
signature RANDOM =
sig
@@ -168,10 +173,13 @@
*}
code_type randseed
- (SML target_atom "Random.seed")
+ (SML "Random.seed")
code_const random_int
- (SML target_atom "Random.value")
+ (SML "Random.value")
+
+code_const run_random
+ (SML "case _ (Random.seed ()) of (x, '_) => x")
code_gen select select_weight
(SML -)