# HG changeset patch # User haftmann # Date 1162283336 -3600 # Node ID 5b76e541cc0afd8ea2f9813de4066aec99c31de0 # Parent c9e068f994ba28bc9b767adaf30ecaea1a7895e4 adapted to new serializer syntax diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/Integ/IntArith.thy --- 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 \ int \ 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) diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/Integ/IntDef.thy --- 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 \ int \ int \ bool" - (SML "(op =) (_ : IntInf.int, _)") + (SML "!((_ : IntInf.int) = _)") (Haskell infixl 4 "==") code_const "op <= \ int \ int \ bool" @@ -940,8 +940,8 @@ (Haskell infixl 7 "*") code_const "uminus \ int \ int" - (SML target_atom "IntInf.~") - (Haskell target_atom "negate") + (SML "IntInf.~") + (Haskell "negate") code_reserved SML IntInf code_reserved Haskell Integer negate diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/Library/EfficientNat.thy --- 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") diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/Library/MLString.thy --- 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 diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/List.thy --- 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 diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/MicroJava/BV/BVExample.thy --- 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 diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/MicroJava/JVM/JVMListExample.thy --- 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 \ 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_ \ 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_ \ bool) \ (loc_ \ 'a) \ loc_ \ 'a" where @@ -155,13 +155,13 @@ definition new_addr' :: "(loc \ (cname \ (vname \ cname \ val option)) option) \ loc \ val option" "new_addr' hp = - test_loc (\i. is_none (hp (Loc i) )) (\i. (Loc i, None)) zero_loc" + test_loc (\i. hp (Loc i) = None) (\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 \ new_addr' diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/ex/CodeEmbed.thy --- 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 diff -r c9e068f994ba -r 5b76e541cc0a src/HOL/ex/CodeRandom.thy --- 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 \ randseed" + +axiomatization random_seed :: "randseed \ 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 \ 'a * randseed) \ '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 -)