moved code generation pretty integers and characters to separate theories
authorhaftmann
Thu Apr 26 13:32:59 2007 +0200 (2007-04-26)
changeset 22799ed7d53db2170
parent 22798 e3962371f568
child 22800 eaf5e7ef35d9
moved code generation pretty integers and characters to separate theories
NEWS
src/HOL/IsaMakefile
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/Library.thy
src/HOL/Library/MLString.thy
src/HOL/Library/Pretty_Char.thy
src/HOL/List.thy
src/HOL/ex/Random.thy
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/NEWS	Thu Apr 26 13:32:55 2007 +0200
     1.2 +++ b/NEWS	Thu Apr 26 13:32:59 2007 +0200
     1.3 @@ -515,6 +515,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
     1.8 +    when generating code.
     1.9 +
    1.10 +* Library/Pretty_Char.thy: maps HOL characters on target language character literals
    1.11 +    when generating code.
    1.12 +
    1.13  * Library/Commutative_Ring.thy: switched from recdef to function package;
    1.14      constants add, mul, pow now curried.  Infix syntax for algebraic operations.
    1.15  
     2.1 --- a/src/HOL/IsaMakefile	Thu Apr 26 13:32:55 2007 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Thu Apr 26 13:32:59 2007 +0200
     2.3 @@ -204,7 +204,7 @@
     2.4    Library/Nested_Environment.thy Library/Zorn.thy\
     2.5    Library/Library/ROOT.ML Library/Library/document/root.tex \
     2.6    Library/Library/document/root.bib Library/While_Combinator.thy \
     2.7 -  Library/Product_ord.thy Library/Char_ord.thy \
     2.8 +  Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
     2.9    Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
    2.10    Library/Coinductive_List.thy Library/AssocList.thy \
    2.11    Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
    2.12 @@ -212,7 +212,8 @@
    2.13    Library/SCT_Definition.thy Library/SCT_Theorem.thy Library/SCT_Interpretation.thy \
    2.14    Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
    2.15    Library/SCT_Examples.thy Library/sct.ML \
    2.16 -  Library/Pure_term.thy Library/Eval.thy
    2.17 +  Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \
    2.18 +  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy
    2.19  	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    2.20  
    2.21  
     3.1 --- a/src/HOL/Lambda/WeakNorm.thy	Thu Apr 26 13:32:55 2007 +0200
     3.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Thu Apr 26 13:32:59 2007 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  header {* Weak normalization for simply-typed lambda calculus *}
     3.5  
     3.6  theory WeakNorm
     3.7 -imports Type
     3.8 +imports Type Pretty_Int
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Char_nat.thy	Thu Apr 26 13:32:59 2007 +0200
     4.3 @@ -0,0 +1,202 @@
     4.4 +(*  Title:      HOL/Library/Char_nat.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Norbert Voelker, Florian Haftmann
     4.7 +*)
     4.8 +
     4.9 +header {* Mapping between characters and natural numbers *}
    4.10 +
    4.11 +theory Char_nat
    4.12 +imports List
    4.13 +begin
    4.14 +
    4.15 +text {* Conversions between nibbles and natural numbers in [0..15]. *}
    4.16 +
    4.17 +fun
    4.18 +  nat_of_nibble :: "nibble \<Rightarrow> nat" where
    4.19 +  "nat_of_nibble Nibble0 = 0"
    4.20 +  | "nat_of_nibble Nibble1 = 1"
    4.21 +  | "nat_of_nibble Nibble2 = 2"
    4.22 +  | "nat_of_nibble Nibble3 = 3"
    4.23 +  | "nat_of_nibble Nibble4 = 4"
    4.24 +  | "nat_of_nibble Nibble5 = 5"
    4.25 +  | "nat_of_nibble Nibble6 = 6"
    4.26 +  | "nat_of_nibble Nibble7 = 7"
    4.27 +  | "nat_of_nibble Nibble8 = 8"
    4.28 +  | "nat_of_nibble Nibble9 = 9"
    4.29 +  | "nat_of_nibble NibbleA = 10"
    4.30 +  | "nat_of_nibble NibbleB = 11"
    4.31 +  | "nat_of_nibble NibbleC = 12"
    4.32 +  | "nat_of_nibble NibbleD = 13"
    4.33 +  | "nat_of_nibble NibbleE = 14"
    4.34 +  | "nat_of_nibble NibbleF = 15"
    4.35 +
    4.36 +definition
    4.37 +  nibble_of_nat :: "nat \<Rightarrow> nibble" where
    4.38 +  "nibble_of_nat x = (let y = x mod 16 in
    4.39 +    if y = 0 then Nibble0 else
    4.40 +    if y = 1 then Nibble1 else
    4.41 +    if y = 2 then Nibble2 else
    4.42 +    if y = 3 then Nibble3 else
    4.43 +    if y = 4 then Nibble4 else
    4.44 +    if y = 5 then Nibble5 else
    4.45 +    if y = 6 then Nibble6 else
    4.46 +    if y = 7 then Nibble7 else
    4.47 +    if y = 8 then Nibble8 else
    4.48 +    if y = 9 then Nibble9 else
    4.49 +    if y = 10 then NibbleA else
    4.50 +    if y = 11 then NibbleB else
    4.51 +    if y = 12 then NibbleC else
    4.52 +    if y = 13 then NibbleD else
    4.53 +    if y = 14 then NibbleE else
    4.54 +    NibbleF)"
    4.55 +
    4.56 +lemma nibble_of_nat_norm:
    4.57 +  "nibble_of_nat (n mod 16) = nibble_of_nat n"
    4.58 +  unfolding nibble_of_nat_def Let_def by auto
    4.59 +
    4.60 +lemmas [code func] = nibble_of_nat_norm [symmetric]
    4.61 +
    4.62 +lemma nibble_of_nat_simps [simp]:
    4.63 +  "nibble_of_nat  0 = Nibble0"
    4.64 +  "nibble_of_nat  1 = Nibble1"
    4.65 +  "nibble_of_nat  2 = Nibble2"
    4.66 +  "nibble_of_nat  3 = Nibble3"
    4.67 +  "nibble_of_nat  4 = Nibble4"
    4.68 +  "nibble_of_nat  5 = Nibble5"
    4.69 +  "nibble_of_nat  6 = Nibble6"
    4.70 +  "nibble_of_nat  7 = Nibble7"
    4.71 +  "nibble_of_nat  8 = Nibble8"
    4.72 +  "nibble_of_nat  9 = Nibble9"
    4.73 +  "nibble_of_nat 10 = NibbleA"
    4.74 +  "nibble_of_nat 11 = NibbleB"
    4.75 +  "nibble_of_nat 12 = NibbleC"
    4.76 +  "nibble_of_nat 13 = NibbleD"
    4.77 +  "nibble_of_nat 14 = NibbleE"
    4.78 +  "nibble_of_nat 15 = NibbleF"
    4.79 +  unfolding nibble_of_nat_def Let_def by auto
    4.80 +
    4.81 +lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
    4.82 +  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_BIT if_False add_0 add_Suc]
    4.83 +
    4.84 +lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
    4.85 +  by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
    4.86 +
    4.87 +lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
    4.88 +proof -
    4.89 +  have nibble_nat_enum: "n mod 16 \<in> {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}"
    4.90 +  proof -
    4.91 +    have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
    4.92 +    have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
    4.93 +      (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))}" by simp
    4.94 +    from this [simplified set_unfold atLeastAtMost_singleton]
    4.95 +    show ?thesis by auto
    4.96 +  qed
    4.97 +  then show ?thesis unfolding nibble_of_nat_def Let_def
    4.98 +  by auto
    4.99 +qed
   4.100 +
   4.101 +lemma inj_nat_of_nibble: "inj nat_of_nibble"
   4.102 +  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
   4.103 +
   4.104 +lemma nat_of_nibble_eq: "nat_of_nibble n = nat_of_nibble m \<longleftrightarrow> n = m"
   4.105 +  by (rule inj_eq) (rule inj_nat_of_nibble)
   4.106 +
   4.107 +lemma nat_of_nibble_less_16: "nat_of_nibble n < 16"
   4.108 +  by (cases n) auto
   4.109 +
   4.110 +lemma nat_of_nibble_div_16: "nat_of_nibble n div 16 = 0"
   4.111 +  by (cases n) auto
   4.112 +
   4.113 +
   4.114 +text {* Conversion between chars and nats. *}
   4.115 +
   4.116 +definition
   4.117 +  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble"
   4.118 +where
   4.119 +  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
   4.120 +
   4.121 +lemma nibble_of_pair [code func]:
   4.122 +  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
   4.123 +  unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
   4.124 +
   4.125 +fun
   4.126 +  nat_of_char :: "char \<Rightarrow> nat" where
   4.127 +  "nat_of_char (Char n m) = nat_of_nibble n * 16 + nat_of_nibble m"
   4.128 +
   4.129 +lemmas [simp del] = nat_of_char.simps
   4.130 +
   4.131 +definition
   4.132 +  char_of_nat :: "nat \<Rightarrow> char" where
   4.133 +  char_of_nat_def: "char_of_nat n = split Char (nibble_pair_of_nat n)"
   4.134 +
   4.135 +lemma Char_char_of_nat:
   4.136 +  "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
   4.137 +  unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
   4.138 +  by (auto simp add: div_add1_eq mod_add1_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
   4.139 +
   4.140 +lemma char_of_nat_of_char:
   4.141 +  "char_of_nat (nat_of_char c) = c"
   4.142 +  by (cases c) (simp add: nat_of_char.simps, simp add: Char_char_of_nat)
   4.143 +
   4.144 +lemma nat_of_char_of_nat:
   4.145 +  "nat_of_char (char_of_nat n) = n mod 256"
   4.146 +proof -
   4.147 +  from mod_div_equality [of n, symmetric, of 16]
   4.148 +  have mod_mult_self3: "\<And>m k n \<Colon> nat. (k * n + m) mod n = m mod n"
   4.149 +  proof -
   4.150 +    fix m k n :: nat
   4.151 +    show "(k * n + m) mod n = m mod n"
   4.152 +    by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
   4.153 +  qed
   4.154 +  from mod_div_decomp [of n 256] obtain k l where n: "n = k * 256 + l"
   4.155 +    and k: "k = n div 256" and l: "l = n mod 256" by blast
   4.156 +  have 16: "(0::nat) < 16" by auto
   4.157 +  have 256: "(256 :: nat) = 16 * 16" by auto
   4.158 +  have l_256: "l mod 256 = l" using l by auto
   4.159 +  have l_div_256: "l div 16 * 16 mod 256 = l div 16 * 16"
   4.160 +    using l by auto
   4.161 +  have aux2: "(k * 256 mod 16 + l mod 16) div 16 = 0"
   4.162 +    unfolding 256 mult_assoc [symmetric] mod_mult_self_is_0 by simp
   4.163 +  have aux3: "(k * 256 + l) div 16 = k * 16 + l div 16"
   4.164 +    unfolding div_add1_eq [of "k * 256" l 16] aux2 256
   4.165 +      mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
   4.166 +  have aux4: "(k * 256 + l) mod 16 = l mod 16"
   4.167 +    unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
   4.168 +  show ?thesis
   4.169 +  by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair nat_of_nibble_of_nat mod_mult_distrib
   4.170 +    n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
   4.171 +qed
   4.172 +
   4.173 +lemma nibble_pair_of_nat_char:
   4.174 +  "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"
   4.175 +proof -
   4.176 +  have nat_of_nibble_256:
   4.177 +    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 = nat_of_nibble n * 16 + nat_of_nibble m"
   4.178 +  proof -
   4.179 +    fix n m
   4.180 +    have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
   4.181 +    using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: nat_number)
   4.182 +    have less_eq_240: "nat_of_nibble n * 16 \<le> 240" using nat_of_nibble_less_eq_15 by auto
   4.183 +    have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
   4.184 +    by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
   4.185 +    then have "nat_of_nibble n * 16 + nat_of_nibble m < 256" (is "?rhs < _") by auto
   4.186 +    then show "?rhs mod 256 = ?rhs" by auto
   4.187 +  qed
   4.188 +  show ?thesis
   4.189 +  unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
   4.190 +  by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
   4.191 +qed
   4.192 +
   4.193 +
   4.194 +text {* Code generator setup *}
   4.195 +
   4.196 +code_modulename SML
   4.197 +  Char_nat List
   4.198 +
   4.199 +code_modulename OCaml
   4.200 +  Char_nat List
   4.201 +
   4.202 +code_modulename Haskell
   4.203 +  Char_nat List
   4.204 +
   4.205 +end
   4.206 \ No newline at end of file
     5.1 --- a/src/HOL/Library/Library.thy	Thu Apr 26 13:32:55 2007 +0200
     5.2 +++ b/src/HOL/Library/Library.thy	Thu Apr 26 13:32:59 2007 +0200
     5.3 @@ -24,6 +24,8 @@
     5.4    OptionalSugar
     5.5    Parity
     5.6    Permutation
     5.7 +  Pretty_Char_chr
     5.8 +  Pretty_Int
     5.9    Primes
    5.10    Quotient
    5.11    Ramsey
     6.1 --- a/src/HOL/Library/MLString.thy	Thu Apr 26 13:32:55 2007 +0200
     6.2 +++ b/src/HOL/Library/MLString.thy	Thu Apr 26 13:32:59 2007 +0200
     6.3 @@ -18,9 +18,7 @@
     6.4    be represented as list of characters which
     6.5    is awkward to read. This theory provides a distinguished
     6.6    datatype for strings which then by convention
     6.7 -  are serialized as monolithic ML strings. Note
     6.8 -  that in Haskell these strings are identified
     6.9 -  with Haskell strings.
    6.10 +  are serialized as monolithic ML strings.
    6.11  *}
    6.12  
    6.13  
    6.14 @@ -28,11 +26,10 @@
    6.15  
    6.16  datatype ml_string = STR string
    6.17  
    6.18 -fun
    6.19 -  explode :: "ml_string \<Rightarrow> string"
    6.20 -where
    6.21 -  "explode (STR s) = s"
    6.22 +lemmas [code nofunc] = ml_string.recs ml_string.cases
    6.23  
    6.24 +lemma [code func]: "size (s\<Colon>ml_string) = 0"
    6.25 +  by (cases s) simp_all
    6.26  
    6.27  subsection {* ML interface *}
    6.28  
    6.29 @@ -50,34 +47,27 @@
    6.30  
    6.31  code_type ml_string
    6.32    (SML "string")
    6.33 -  (Haskell "String")
    6.34 -
    6.35 -code_const STR
    6.36 -  (Haskell "_")
    6.37  
    6.38  setup {*
    6.39 +let
    6.40 +  val charr = @{const_name Char}
    6.41 +  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    6.42 +    @{const_name Nibble2}, @{const_name Nibble3},
    6.43 +    @{const_name Nibble4}, @{const_name Nibble5},
    6.44 +    @{const_name Nibble6}, @{const_name Nibble7},
    6.45 +    @{const_name Nibble8}, @{const_name Nibble9},
    6.46 +    @{const_name NibbleA}, @{const_name NibbleB},
    6.47 +    @{const_name NibbleC}, @{const_name NibbleD},
    6.48 +    @{const_name NibbleE}, @{const_name NibbleF}];
    6.49 +in
    6.50    CodegenSerializer.add_pretty_ml_string "SML"
    6.51 -    @{const_name Nil} @{const_name Cons} @{const_name STR}
    6.52 -    ML_Syntax.print_char ML_Syntax.print_string "String.implode"
    6.53 +    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
    6.54 +end
    6.55  *}
    6.56  
    6.57 -code_const explode
    6.58 -  (SML "String.explode")
    6.59 -  (Haskell "_")
    6.60 -
    6.61 -code_reserved SML string explode
    6.62 +code_reserved SML string
    6.63  
    6.64  code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
    6.65    (SML "!((_ : string) = _)")
    6.66 -  (Haskell infixl 4 "==")
    6.67 -
    6.68 -code_instance ml_string :: eq (Haskell -)
    6.69 -
    6.70 -text {* disable something ugly *}
    6.71 -
    6.72 -code_const "ml_string_rec" and "ml_string_case" and "size \<Colon> ml_string \<Rightarrow> nat"
    6.73 -  (SML "!((_); (_); raise Fail \"ml'_string'_rec\")"
    6.74 -    and "!((_); (_); raise Fail \"ml'_string'_case\")"
    6.75 -    and "!((_); raise Fail \"size'_ml'_string\")")
    6.76  
    6.77  end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Library/Pretty_Char.thy	Thu Apr 26 13:32:59 2007 +0200
     7.3 @@ -0,0 +1,50 @@
     7.4 +(*  Title:      HOL/Library/Pretty_Char.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Florian Haftmann
     7.7 +*)
     7.8 +
     7.9 +header {* Code generation of pretty characters (and strings) *}
    7.10 +
    7.11 +theory Pretty_Char
    7.12 +imports List
    7.13 +begin
    7.14 +
    7.15 +code_type char
    7.16 +  (SML "char")
    7.17 +  (OCaml "char")
    7.18 +  (Haskell "Char")
    7.19 +
    7.20 +setup {*
    7.21 +let
    7.22 +  val charr = @{const_name Char}
    7.23 +  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    7.24 +    @{const_name Nibble2}, @{const_name Nibble3},
    7.25 +    @{const_name Nibble4}, @{const_name Nibble5},
    7.26 +    @{const_name Nibble6}, @{const_name Nibble7},
    7.27 +    @{const_name Nibble8}, @{const_name Nibble9},
    7.28 +    @{const_name NibbleA}, @{const_name NibbleB},
    7.29 +    @{const_name NibbleC}, @{const_name NibbleD},
    7.30 +    @{const_name NibbleE}, @{const_name NibbleF}];
    7.31 +in
    7.32 +  fold (fn target => CodegenSerializer.add_pretty_char target charr nibbles)
    7.33 +    ["SML", "OCaml", "Haskell"]
    7.34 +  #> CodegenSerializer.add_pretty_list_string "Haskell"
    7.35 +    @{const_name Nil} @{const_name Cons} charr nibbles
    7.36 +end
    7.37 +*}
    7.38 +
    7.39 +code_instance char :: eq
    7.40 +  (Haskell -)
    7.41 +
    7.42 +code_reserved SML
    7.43 +  char
    7.44 +
    7.45 +code_reserved OCaml
    7.46 +  char
    7.47 +
    7.48 +code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    7.49 +  (SML "!((_ : char) = _)")
    7.50 +  (OCaml "!((_ : char) = _)")
    7.51 +  (Haskell infixl 4 "==")
    7.52 +
    7.53 +end
     8.1 --- a/src/HOL/List.thy	Thu Apr 26 13:32:55 2007 +0200
     8.2 +++ b/src/HOL/List.thy	Thu Apr 26 13:32:59 2007 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  header {* The datatype of finite lists *}
     8.5  
     8.6  theory List
     8.7 -imports PreList
     8.8 +imports PreList Recdef
     8.9  uses "Tools/string_syntax.ML"
    8.10  begin
    8.11  
    8.12 @@ -2653,55 +2653,29 @@
    8.13    (OCaml "_ list")
    8.14    (Haskell "![_]")
    8.15  
    8.16 +code_reserved SML
    8.17 +  list
    8.18 +
    8.19 +code_reserved OCaml
    8.20 +  list
    8.21 +
    8.22  code_const Nil
    8.23    (SML "[]")
    8.24    (OCaml "[]")
    8.25    (Haskell "[]")
    8.26  
    8.27 -code_type char
    8.28 -  (SML "char")
    8.29 -  (OCaml "char")
    8.30 -  (Haskell "Char")
    8.31 -
    8.32 -code_const Char and char_rec
    8.33 -    and char_case and "size \<Colon> char \<Rightarrow> nat"
    8.34 -  (Haskell "error/ \"Char\""
    8.35 -    and "error/ \"char_rec\"" and "error/ \"char_case\"" and "error/ \"size_char\"")
    8.36 -
    8.37  setup {*
    8.38 -  fold (uncurry (CodegenSerializer.add_undefined "SML")) [
    8.39 -      ("List.char.Char", "(raise Fail \"Char\")"),
    8.40 -      ("List.char.char_rec", "(raise Fail \"char_rec\")"),
    8.41 -      ("List.char.char_case", "(raise Fail \"char_case\")")
    8.42 -    ]
    8.43 -  #> fold (uncurry (CodegenSerializer.add_undefined "OCaml")) [
    8.44 -      ("List.char.Char", "(failwith \"Char\")"),
    8.45 -      ("List.char.char_rec", "(failwith \"char_rec\")"),
    8.46 -      ("List.char.char_case", "(failwith \"char_case\")")
    8.47 -    ]    
    8.48 +  fold (fn target => CodegenSerializer.add_pretty_list target
    8.49 +    @{const_name Nil} @{const_name Cons}
    8.50 +  ) ["SML", "OCaml", "Haskell"]
    8.51  *}
    8.52  
    8.53 -code_const "size \<Colon> char \<Rightarrow> nat"
    8.54 -  (SML "!(_;/ raise Fail \"size'_char\")")
    8.55 -  (OCaml "!(_;/ failwith \"size'_char\")")
    8.56 -
    8.57 -code_instance list :: eq and char :: eq
    8.58 -  (Haskell - and -)
    8.59 +code_instance list :: eq
    8.60 +  (Haskell -)
    8.61  
    8.62  code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
    8.63    (Haskell infixl 4 "==")
    8.64  
    8.65 -code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    8.66 -  (SML "!((_ : char) = _)")
    8.67 -  (OCaml "!((_ : char) = _)")
    8.68 -  (Haskell infixl 4 "==")
    8.69 -
    8.70 -code_reserved SML
    8.71 -  list char nil
    8.72 -
    8.73 -code_reserved OCaml
    8.74 -  list char
    8.75 -
    8.76  setup {*
    8.77  let
    8.78  
    8.79 @@ -2716,18 +2690,8 @@
    8.80      | NONE => NONE;
    8.81  
    8.82  in
    8.83 -
    8.84    Codegen.add_codegen "list_codegen" list_codegen
    8.85    #> Codegen.add_codegen "char_codegen" char_codegen
    8.86 -  #> CodegenSerializer.add_pretty_list "SML" "List.list.Nil" "List.list.Cons"
    8.87 -       (Pretty.enum "," "[" "]") NONE (7, "::")
    8.88 -  #> CodegenSerializer.add_pretty_list "OCaml" "List.list.Nil" "List.list.Cons"
    8.89 -       (Pretty.enum ";" "[" "]") NONE (6, "::")
    8.90 -  #> CodegenSerializer.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons"
    8.91 -       (Pretty.enum "," "[" "]") (SOME (ML_Syntax.print_char, ML_Syntax.print_string)) (5, ":")
    8.92 -  #> CodegenPackage.add_appconst
    8.93 -       ("List.char.Char", CodegenPackage.appgen_char (try HOLogic.dest_char))
    8.94 -
    8.95  end;
    8.96  *}
    8.97  
    8.98 @@ -2801,8 +2765,7 @@
    8.99    "x mem xs \<longleftrightarrow> x \<in> set xs"
   8.100    by (induct xs) auto
   8.101  
   8.102 -lemmas in_set_code [code unfold] =
   8.103 -  mem_iff [symmetric, THEN eq_reflection]
   8.104 +lemmas in_set_code [code unfold] = mem_iff [symmetric]
   8.105  
   8.106  lemma empty_null [code inline]:
   8.107    "xs = [] \<longleftrightarrow> null xs"
   8.108 @@ -2819,8 +2782,7 @@
   8.109    "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
   8.110    by (induct xs) auto
   8.111  
   8.112 -lemmas list_ball_code [code unfold] =
   8.113 -  list_all_iff [symmetric, THEN eq_reflection]
   8.114 +lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
   8.115  
   8.116  lemma list_all_append [simp]:
   8.117    "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
   8.118 @@ -2839,7 +2801,7 @@
   8.119    by (induct xs) simp_all
   8.120  
   8.121  lemmas list_bex_code [code unfold] =
   8.122 -  list_ex_iff [symmetric, THEN eq_reflection]
   8.123 +  list_ex_iff [symmetric]
   8.124  
   8.125  lemma list_ex_length:
   8.126    "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
   8.127 @@ -2857,60 +2819,51 @@
   8.128    "map_filter f P xs = map f (filter P xs)"
   8.129    by (induct xs) auto
   8.130  
   8.131 -lemma rev_code [code func, code unfold, code noinline]:
   8.132 -  "rev xs == itrev xs []"
   8.133 +lemma rev_code [code func]:
   8.134 +  "rev xs = itrev xs []"
   8.135    by simp
   8.136  
   8.137 +
   8.138  text {* code for bounded quantification over nats *}
   8.139  
   8.140 -lemma atMost_upto [code inline]:
   8.141 +lemma atMost_upto [code unfold]:
   8.142    "{..n} = set [0..n]"
   8.143    by auto
   8.144 -lemmas atMost_upto' [code unfold] = atMost_upto [THEN eq_reflection]
   8.145 -
   8.146 -lemma atLeast_upt [code inline]:
   8.147 +
   8.148 +lemma atLeast_upt [code unfold]:
   8.149    "{..<n} = set [0..<n]"
   8.150    by auto
   8.151 -lemmas atLeast_upt' [code unfold] = atLeast_upt [THEN eq_reflection]
   8.152 -
   8.153 -lemma greaterThanLessThan_upd [code inline]:
   8.154 +
   8.155 +lemma greaterThanLessThan_upd [code unfold]:
   8.156    "{n<..<m} = set [Suc n..<m]"
   8.157    by auto
   8.158 -lemmas greaterThanLessThan_upd' [code unfold] = greaterThanLessThan_upd [THEN eq_reflection]
   8.159 -
   8.160 -lemma atLeastLessThan_upd [code inline]:
   8.161 +
   8.162 +lemma atLeastLessThan_upd [code unfold]:
   8.163    "{n..<m} = set [n..<m]"
   8.164    by auto
   8.165 -lemmas atLeastLessThan_upd' [code unfold] = atLeastLessThan_upd [THEN eq_reflection]
   8.166 -
   8.167 -lemma greaterThanAtMost_upto [code inline]:
   8.168 +
   8.169 +lemma greaterThanAtMost_upto [code unfold]:
   8.170    "{n<..m} = set [Suc n..m]"
   8.171    by auto
   8.172 -lemmas greaterThanAtMost_upto' [code unfold] = greaterThanAtMost_upto [THEN eq_reflection]
   8.173 -
   8.174 -lemma atLeastAtMost_upto [code inline]:
   8.175 +
   8.176 +lemma atLeastAtMost_upto [code unfold]:
   8.177    "{n..m} = set [n..m]"
   8.178    by auto
   8.179 -lemmas atLeastAtMost_upto' [code unfold] = atLeastAtMost_upto [THEN eq_reflection]
   8.180 -
   8.181 -lemma all_nat_less_eq [code inline]:
   8.182 +
   8.183 +lemma all_nat_less_eq [code unfold]:
   8.184    "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
   8.185    by auto
   8.186 -lemmas all_nat_less_eq' [code unfold] = all_nat_less_eq [THEN eq_reflection]
   8.187 -
   8.188 -lemma ex_nat_less_eq [code inline]:
   8.189 +
   8.190 +lemma ex_nat_less_eq [code unfold]:
   8.191    "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
   8.192    by auto
   8.193 -lemmas ex_nat_less_eq' [code unfold] = ex_nat_less_eq [THEN eq_reflection]
   8.194 -
   8.195 -lemma all_nat_less [code inline]:
   8.196 +
   8.197 +lemma all_nat_less [code unfold]:
   8.198    "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
   8.199    by auto
   8.200 -lemmas all_nat_less' [code unfold] =  all_nat_less [THEN eq_reflection]
   8.201 -
   8.202 -lemma ex_nat_less [code inline]:
   8.203 +
   8.204 +lemma ex_nat_less [code unfold]:
   8.205    "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
   8.206    by auto
   8.207 -lemmas ex_nat_less' [code unfold] = ex_nat_less [THEN eq_reflection]
   8.208 -
   8.209 -end
   8.210 +
   8.211 +end
   8.212 \ No newline at end of file
     9.1 --- a/src/HOL/ex/Random.thy	Thu Apr 26 13:32:55 2007 +0200
     9.2 +++ b/src/HOL/ex/Random.thy	Thu Apr 26 13:32:59 2007 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  header {* A simple random engine *}
     9.5  
     9.6  theory Random
     9.7 -imports State_Monad
     9.8 +imports State_Monad Pretty_Int
     9.9  begin
    9.10  
    9.11  fun
    10.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Apr 26 13:32:55 2007 +0200
    10.2 +++ b/src/Pure/Tools/codegen_package.ML	Thu Apr 26 13:32:59 2007 +0200
    10.3 @@ -16,8 +16,6 @@
    10.4  
    10.5    type appgen;
    10.6    val add_appconst: string * appgen -> theory -> theory;
    10.7 -  val appgen_numeral: (term -> IntInf.int option) -> appgen;
    10.8 -  val appgen_char: (term -> int option) -> appgen;
    10.9    val appgen_case: (theory -> term
   10.10      -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
   10.11      -> appgen;
   10.12 @@ -432,27 +430,6 @@
   10.13  (* parametrized application generators, for instantiation in object logic *)
   10.14  (* (axiomatic extensions of extraction kernel *)
   10.15  
   10.16 -fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns =
   10.17 -  case int_of_numeral (list_comb (Const c, ts))
   10.18 -   of SOME i =>
   10.19 -        trns
   10.20 -        |> pair (CodegenThingol.INum i)
   10.21 -    | NONE =>
   10.22 -        trns
   10.23 -        |> appgen_default thy algbr funcgr strct app;
   10.24 -
   10.25 -fun appgen_char char_to_index thy algbr funcgr strct (app as ((_, ty), _)) trns =
   10.26 -  case (char_to_index o list_comb o apfst Const) app
   10.27 -   of SOME i =>
   10.28 -        trns
   10.29 -        |> exprgen_type thy algbr funcgr strct ty
   10.30 -        |>> (fn _ => IChar (chr i))
   10.31 -    | NONE =>
   10.32 -        trns
   10.33 -        |> appgen_default thy algbr funcgr strct app;
   10.34 -
   10.35 -val debug_term = ref (Bound 0);
   10.36 -
   10.37  fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns =
   10.38    let
   10.39      val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
    11.1 --- a/src/Pure/Tools/codegen_serializer.ML	Thu Apr 26 13:32:55 2007 +0200
    11.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Thu Apr 26 13:32:59 2007 +0200
    11.3 @@ -18,12 +18,15 @@
    11.4    val add_syntax_constP: string -> string -> OuterParse.token list
    11.5      -> (theory -> theory) * OuterParse.token list;
    11.6  
    11.7 -  val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)
    11.8 -   -> ((string -> string) * (string -> string)) option -> int * string
    11.9 -   -> theory -> theory;
   11.10 -  val add_pretty_ml_string: string -> string -> string -> string
   11.11 -   -> (string -> string) -> (string -> string) -> string -> theory -> theory;
   11.12    val add_undefined: string -> string -> string -> theory -> theory;
   11.13 +  val add_pretty_list: string -> string -> string -> theory -> theory;
   11.14 +  val add_pretty_list_string: string -> string -> string
   11.15 +    -> string -> string list -> theory -> theory;
   11.16 +  val add_pretty_char: string -> string -> string list -> theory -> theory
   11.17 +  val add_pretty_numeral: string -> string * typ -> string -> string -> string
   11.18 +    -> string -> string -> theory -> theory;
   11.19 +  val add_pretty_ml_string: string -> string -> string list -> string
   11.20 +    -> string -> string -> theory -> theory;
   11.21    val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;
   11.22  
   11.23    type serializer;
   11.24 @@ -187,7 +190,7 @@
   11.25    in (pr_bind' ((v', pat'), ty), vars'') end;
   11.26  
   11.27  
   11.28 -(* list, string and monad serializers *)
   11.29 +(* list, char, string, numeral and monad abstract syntax transformations *)
   11.30  
   11.31  fun implode_list c_nil c_cons t =
   11.32    let
   11.33 @@ -202,10 +205,42 @@
   11.34      | _ => NONE
   11.35    end;
   11.36  
   11.37 -fun implode_string mk_char mk_string ts =
   11.38 -  if forall (fn IChar _ => true | _ => false) ts
   11.39 -  then (SOME o str o mk_string o implode o map (fn IChar c => mk_char c)) ts
   11.40 -  else NONE;
   11.41 +fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
   11.42 +      let
   11.43 +        fun idx c = find_index (curry (op =) c) c_nibbles;
   11.44 +        fun decode ~1 _ = NONE
   11.45 +          | decode _ ~1 = NONE
   11.46 +          | decode n m = SOME (chr (n * 16 + m));
   11.47 +      in decode (idx c1) (idx c2) end
   11.48 +  | decode_char _ _ = NONE;
   11.49 +
   11.50 +fun implode_string c_char c_nibbles mk_char mk_string ts =
   11.51 +  let
   11.52 +    fun implode_char (IConst (c, _) `$ t1 `$ t2) =
   11.53 +          if c = c_char then decode_char c_nibbles (t1, t2) else NONE
   11.54 +      | implode_char _ = NONE;
   11.55 +    val ts' = map implode_char ts;
   11.56 +  in if forall is_some ts'
   11.57 +    then (SOME o str o mk_string o implode o map_filter I) ts'
   11.58 +    else NONE
   11.59 +  end;
   11.60 +
   11.61 +fun implode_numeral c_bit0 c_bit1 c_pls c_min c_bit =
   11.62 +  let
   11.63 +    fun dest_bit (IConst (c, _)) = if c = c_bit0 then SOME 0
   11.64 +          else if c = c_bit1 then SOME 1
   11.65 +          else NONE
   11.66 +      | dest_bit _ = NONE;
   11.67 +    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
   11.68 +          else if c = c_min then SOME ~1
   11.69 +          else NONE
   11.70 +      | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
   11.71 +          if c = c_bit then case (dest_numeral t1, dest_bit t2)
   11.72 +           of (SOME n, SOME b) => SOME (2 * n + IntInf.fromInt b)
   11.73 +            | _ => NONE
   11.74 +          else NONE
   11.75 +      | dest_numeral _ = NONE;
   11.76 +  in dest_numeral end;
   11.77  
   11.78  fun implode_monad c_mbind c_kbind t =
   11.79    let
   11.80 @@ -222,53 +257,6 @@
   11.81              | NONE => NONE;
   11.82    in CodegenThingol.unfoldr dest_monad t end;
   11.83  
   11.84 -fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode =
   11.85 -  let
   11.86 -    fun pretty pr vars fxy [(t, _)] =
   11.87 -      case implode_list c_nil c_cons t
   11.88 -       of SOME ts => (case implode_string mk_char mk_string ts
   11.89 -           of SOME p => p
   11.90 -            | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr vars BR t])
   11.91 -        | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr vars BR t]
   11.92 -  in (1, pretty) end;
   11.93 -
   11.94 -fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) =
   11.95 -  let
   11.96 -    fun default pr fxy t1 t2 =
   11.97 -      brackify_infix (target_fxy, R) fxy [
   11.98 -        pr (INFX (target_fxy, X)) t1,
   11.99 -        str target_cons,
  11.100 -        pr (INFX (target_fxy, R)) t2
  11.101 -      ];
  11.102 -    fun pretty pr vars fxy [(t1, _), (t2, _)] =
  11.103 -      case Option.map (cons t1) (implode_list c_nil c_cons t2)
  11.104 -       of SOME ts =>
  11.105 -            (case mk_char_string
  11.106 -             of SOME (mk_char, mk_string) =>
  11.107 -                  (case implode_string mk_char mk_string ts
  11.108 -                   of SOME p => p
  11.109 -                    | NONE => mk_list (map (pr vars NOBR) ts))
  11.110 -              | NONE => mk_list (map (pr vars NOBR) ts))
  11.111 -        | NONE => default (pr vars) fxy t1 t2;
  11.112 -  in (2, pretty) end;
  11.113 -
  11.114 -val pretty_imperative_monad_bind =
  11.115 -  let
  11.116 -    fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
  11.117 -          vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
  11.118 -            pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
  11.119 -      | pretty pr vars fxy [(t1, _), (t2, ty2)] =
  11.120 -          let
  11.121 -            (*this code suffers from the lack of a proper concept for bindings*)
  11.122 -            val vs = CodegenThingol.fold_varnames cons t2 [];
  11.123 -            val v = Name.variant vs "x";
  11.124 -            val vars' = CodegenNames.intro_vars [v] vars;
  11.125 -            val var = IVar v;
  11.126 -            val ty = (hd o fst o CodegenThingol.unfold_fun) ty2;
  11.127 -          in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
  11.128 -  in (2, pretty) end;
  11.129 -
  11.130 -
  11.131  
  11.132  (** name auxiliary **)
  11.133  
  11.134 @@ -372,10 +360,6 @@
  11.135                #>> (fn p => concat [str "fn", p, str "=>"]);
  11.136              val (ps, vars') = fold_map pr binds vars;
  11.137            in brackets (ps @ [pr_term vars' NOBR t']) end
  11.138 -      | pr_term vars fxy (INum n) =
  11.139 -          brackets [(str o IntInf.toString) n, str ":", str "IntInf.int"]
  11.140 -      | pr_term vars _ (IChar c) =
  11.141 -          (str o prefix "#" o quote o ML_Syntax.print_char) c
  11.142        | pr_term vars fxy (t as ICase (_, [_])) =
  11.143            let
  11.144              val (binds, t') = CodegenThingol.unfold_let t;
  11.145 @@ -641,19 +625,6 @@
  11.146              fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
  11.147              val (ps, vars') = fold_map pr binds vars;
  11.148            in brackets (str "fun" :: ps @ str "->" @@ pr_term vars' NOBR t') end
  11.149 -      | pr_term vars fxy (INum n) =
  11.150 -          if n > IntInf.fromInt 0 then
  11.151 -            brackify fxy [str "Big_int.big_int_of_int", (str o IntInf.toString) n]
  11.152 -          else
  11.153 -            brackify fxy [str "Big_int.big_int_of_int",
  11.154 -              (str o enclose "(" ")" o prefix "-" o IntInf.toString o op ~) n]
  11.155 -      | pr_term vars _ (IChar c) =
  11.156 -          (str o enclose "'" "'")
  11.157 -            (let val i = ord c
  11.158 -              in if i < 32 orelse i = 39 orelse i = 92
  11.159 -                then prefix "\\" (string_of_int i)
  11.160 -                else c
  11.161 -              end)
  11.162        | pr_term vars fxy (t as ICase (_, [_])) =
  11.163            let
  11.164              val (binds, t') = CodegenThingol.unfold_let t;
  11.165 @@ -976,10 +947,9 @@
  11.166            |> fold (fold (insert (op =)) o Graph.imm_succs code) names
  11.167            |> subtract (op =) names;
  11.168          val (modls, _) = (split_list o map dest_name) names;
  11.169 -        val modl = (the_single o distinct (op =)) modls
  11.170 +        val modl' = (the_single o distinct (op =) o map name_modl) modls
  11.171            handle Empty =>
  11.172              error ("Illegal mutual dependencies: " ^ commas (map labelled_name names));
  11.173 -        val modl' = name_modl modl;
  11.174          val modl_explode = NameSpace.explode modl';
  11.175          fun add_dep name name'' =
  11.176            let
  11.177 @@ -988,13 +958,14 @@
  11.178              map_node modl_explode
  11.179                (Graph.add_edge (name, name''))
  11.180            else let
  11.181 -            val (common, (diff1::_, diff2::_)) = chop_prefix (op =) (modl_explode, NameSpace.explode modl'');
  11.182 +            val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
  11.183 +              (modl_explode, NameSpace.explode modl'');
  11.184            in
  11.185              map_node common
  11.186                (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
  11.187                  handle Graph.CYCLES _ => error ("Dependency "
  11.188 -                  ^ quote name
  11.189 -                  ^ " -> " ^ quote name'' ^ " would result in module dependency cycle"))
  11.190 +                  ^ quote name ^ " -> " ^ quote name''
  11.191 +                  ^ " would result in module dependency cycle"))
  11.192            end end;
  11.193        in
  11.194          nsp_nodes
  11.195 @@ -1155,18 +1126,6 @@
  11.196              fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
  11.197              val (ps, vars') = fold_map pr binds vars;
  11.198            in brackets (str "\\" :: ps @ str "->" @@ pr_term vars' NOBR t') end
  11.199 -      | pr_term vars fxy (INum n) =
  11.200 -          if n > IntInf.fromInt 0 then
  11.201 -            (str o IntInf.toString) n
  11.202 -          else
  11.203 -            (str o enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) n
  11.204 -      | pr_term vars fxy (IChar c) =
  11.205 -          (str o enclose "'" "'")
  11.206 -            (let val i = (Char.ord o the o Char.fromString) c
  11.207 -              in if i < 32 orelse i = 39 orelse i = 92
  11.208 -                then Library.prefix "\\" (string_of_int i)
  11.209 -                else c
  11.210 -              end)
  11.211        | pr_term vars fxy (t as ICase (_, [_])) =
  11.212            let
  11.213              val (binds, t) = CodegenThingol.unfold_let t;
  11.214 @@ -1354,7 +1313,7 @@
  11.215    let
  11.216      val _ = Option.map File.check destination;
  11.217      val empty_names = Name.make_context (reserved_haskell @ reserved_user);
  11.218 -    val name_modl = mk_modl_name_tab empty_names module_prefix module_alias code
  11.219 +    val name_modl = mk_modl_name_tab empty_names module_prefix module_alias code;
  11.220      fun add_def (name, (def, deps)) =
  11.221        let
  11.222          val (modl, base) = dest_name name;
  11.223 @@ -1389,7 +1348,7 @@
  11.224              | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
  11.225        in
  11.226          Symtab.map_default (modlname', ([], ([], (empty_names, empty_names))))
  11.227 -              (apfst (fold (insert (op =)) deps))
  11.228 +              (apfst (fold (insert (op = : string * string -> bool)) deps))
  11.229          #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
  11.230          #-> (fn (base', names) =>
  11.231                (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
  11.232 @@ -1500,10 +1459,10 @@
  11.233  (** theory data **)
  11.234  
  11.235  datatype syntax_expr = SyntaxExpr of {
  11.236 -  class: ((string * (string -> string option)) * serial) Symtab.table,
  11.237 +  class: (string * (string -> string option)) Symtab.table,
  11.238    inst: unit Symtab.table,
  11.239 -  tyco: (typ_syntax * serial) Symtab.table,
  11.240 -  const: (term_syntax * serial) Symtab.table
  11.241 +  tyco: typ_syntax Symtab.table,
  11.242 +  const: term_syntax Symtab.table
  11.243  };
  11.244  
  11.245  fun mk_syntax_expr ((class, inst), (tyco, const)) =
  11.246 @@ -1513,10 +1472,10 @@
  11.247  fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
  11.248      SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
  11.249    mk_syntax_expr (
  11.250 -    (Symtab.merge (eq_snd (op =)) (class1, class2),
  11.251 -       Symtab.merge (op =) (inst1, inst2)),
  11.252 -    (Symtab.merge (eq_snd (op =)) (tyco1, tyco2),
  11.253 -       Symtab.merge (eq_snd (op =)) (const1, const2))
  11.254 +    (Symtab.join (K snd) (class1, class2),
  11.255 +       Symtab.join (K snd) (inst1, inst2)),
  11.256 +    (Symtab.join (K snd) (tyco1, tyco2),
  11.257 +       Symtab.join (K snd) (const1, const2))
  11.258    );
  11.259  
  11.260  datatype syntax_modl = SyntaxModl of {
  11.261 @@ -1585,6 +1544,11 @@
  11.262  fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
  11.263  fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x;
  11.264  
  11.265 +fun assert_serializer thy target =
  11.266 +  case Symtab.lookup (CodegenSerializerData.get thy) target
  11.267 +   of SOME data => target
  11.268 +    | NONE => error ("Unknown code target language: " ^ quote target);
  11.269 +
  11.270  fun add_serializer (target, seri) thy =
  11.271    let
  11.272      val _ = case Symtab.lookup (CodegenSerializerData.get thy) target
  11.273 @@ -1601,9 +1565,7 @@
  11.274  
  11.275  fun map_seri_data target f thy =
  11.276    let
  11.277 -    val _ = if is_some (Symtab.lookup (CodegenSerializerData.get thy) target)
  11.278 -      then ()
  11.279 -      else error ("Unknown code target language: " ^ quote target);
  11.280 +    val _ = assert_serializer thy target;
  11.281    in
  11.282      thy
  11.283      |> (CodegenSerializerData.map o Symtab.map_entry target o map_target) f
  11.284 @@ -1631,13 +1593,12 @@
  11.285      val reserved = the_reserved data;
  11.286      val { alias, prolog } = the_syntax_modl data;
  11.287      val { class, inst, tyco, const } = the_syntax_expr data;
  11.288 -    fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;
  11.289      val project = if target = target_diag then I
  11.290        else CodegenThingol.project_code
  11.291          (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
  11.292    in
  11.293      project #> seri args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
  11.294 -      (fun_of class) (fun_of tyco) (fun_of const)
  11.295 +      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
  11.296    end;
  11.297  
  11.298  val eval_verbose = ref false;
  11.299 @@ -1651,7 +1612,6 @@
  11.300      val reserved = the_reserved data;
  11.301      val { alias, prolog } = the_syntax_modl data;
  11.302      val { class, inst, tyco, const } = the_syntax_expr data;
  11.303 -    fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;
  11.304      fun eval p = (
  11.305        reff := NONE;
  11.306        if !eval_verbose then Pretty.writeln p else ();
  11.307 @@ -1672,35 +1632,158 @@
  11.308            (SOME [val_name])
  11.309      |> seri_ml pr_sml pr_sml_modl ML_Syntax.reserved I (labelled_name thy) reserved
  11.310          (Symtab.lookup alias) (Symtab.lookup prolog)
  11.311 -        (fun_of class) (fun_of tyco) (fun_of const)
  11.312 +        (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
  11.313      |> eval
  11.314    end;
  11.315  
  11.316 -fun assert_serializer thy target =
  11.317 -  case Symtab.lookup (CodegenSerializerData.get thy) target
  11.318 -   of SOME data => target
  11.319 -    | NONE => error ("Unknown code target language: " ^ quote target);
  11.320 -
  11.321 -fun has_serialization f thy targets name =
  11.322 +fun const_has_serialization thy targets name =
  11.323    forall (
  11.324 -    is_some o (fn tab => Symtab.lookup tab name) o f o the_syntax_expr o the
  11.325 +    is_some o (fn tab => Symtab.lookup tab name) o #const o the_syntax_expr o the
  11.326        o Symtab.lookup (CodegenSerializerData.get thy)
  11.327    ) targets;
  11.328  
  11.329 -val const_has_serialization = has_serialization #const;
  11.330 +
  11.331 +(** optional pretty serialization **)
  11.332 +
  11.333 +local
  11.334  
  11.335 +val pretty : (string * {
  11.336 +    pretty_char: string -> string,
  11.337 +    pretty_string: string -> string,
  11.338 +    pretty_numeral: IntInf.int -> string,
  11.339 +    pretty_list: Pretty.T list -> Pretty.T,
  11.340 +    infix_cons: int * string
  11.341 +  }) list = [
  11.342 +  ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
  11.343 +      pretty_string = ML_Syntax.print_string,
  11.344 +      pretty_numeral = fn k => "(" ^ IntInf.toString k ^ " : IntInf.int)",
  11.345 +      pretty_list = Pretty.enum "," "[" "]",
  11.346 +      infix_cons = (7, "::")}),
  11.347 +  ("OCaml", { pretty_char = fn c => enclose "'" "'"
  11.348 +        (let val i = ord c
  11.349 +          in if i < 32 orelse i = 39 orelse i = 92
  11.350 +            then prefix "\\" (string_of_int i)
  11.351 +            else c
  11.352 +          end),
  11.353 +      pretty_string = (fn _ => error "OCaml: no pretty strings"),
  11.354 +      pretty_numeral = fn k => if k >= IntInf.fromInt 0 then
  11.355 +            "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
  11.356 +          else
  11.357 +            "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
  11.358 +              o IntInf.toString o op ~) k ^ ")",
  11.359 +      pretty_list = Pretty.enum ";" "[" "]",
  11.360 +      infix_cons = (6, "::")}),
  11.361 +  ("Haskell", { pretty_char = fn c => enclose "'" "'"
  11.362 +        (let val i = ord c
  11.363 +          in if i < 32 orelse i = 39 orelse i = 92
  11.364 +            then Library.prefix "\\" (string_of_int i)
  11.365 +            else c
  11.366 +          end),
  11.367 +      pretty_string = ML_Syntax.print_string,
  11.368 +      pretty_numeral = fn k => if k >= IntInf.fromInt 0 then
  11.369 +            IntInf.toString k
  11.370 +          else
  11.371 +            (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k,
  11.372 +      pretty_list = Pretty.enum "," "[" "]",
  11.373 +      infix_cons = (5, ":")})
  11.374 +];
  11.375 +
  11.376 +in
  11.377 +
  11.378 +fun pr_pretty target = case AList.lookup (op =) pretty target
  11.379 + of SOME x => x
  11.380 +  | NONE => error ("Unknown code target language: " ^ quote target);
  11.381 +
  11.382 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
  11.383 +  brackify_infix (target_fxy, R) fxy [
  11.384 +    pr (INFX (target_fxy, X)) t1,
  11.385 +    str target_cons,
  11.386 +    pr (INFX (target_fxy, R)) t2
  11.387 +  ];
  11.388  
  11.389 +fun pretty_list c_nil c_cons target =
  11.390 +  let
  11.391 +    val pretty_ops = pr_pretty target;
  11.392 +    val mk_list = #pretty_list pretty_ops;
  11.393 +    fun pretty pr vars fxy [(t1, _), (t2, _)] =
  11.394 +      case Option.map (cons t1) (implode_list c_nil c_cons t2)
  11.395 +       of SOME ts => mk_list (map (pr vars NOBR) ts)
  11.396 +        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  11.397 +  in (2, pretty) end;
  11.398  
  11.399 -(** ML and toplevel interface **)
  11.400 +fun pretty_list_string c_nil c_cons c_char c_nibbles target =
  11.401 +  let
  11.402 +    val pretty_ops = pr_pretty target;
  11.403 +    val mk_list = #pretty_list pretty_ops;
  11.404 +    val mk_char = #pretty_char pretty_ops;
  11.405 +    val mk_string = #pretty_string pretty_ops;
  11.406 +    fun pretty pr vars fxy [(t1, _), (t2, _)] =
  11.407 +      case Option.map (cons t1) (implode_list c_nil c_cons t2)
  11.408 +       of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts
  11.409 +           of SOME p => p
  11.410 +            | NONE => mk_list (map (pr vars NOBR) ts)
  11.411 +        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
  11.412 +  in (2, pretty) end;
  11.413 +
  11.414 +fun pretty_char c_char c_nibbles target =
  11.415 +  let
  11.416 +    val mk_char = #pretty_char (pr_pretty target);
  11.417 +    fun pretty _ _ _ [(t1, _), (t2, _)] =
  11.418 +      case decode_char c_nibbles (t1, t2)
  11.419 +       of SOME c => (str o mk_char) c
  11.420 +        | NONE => error "Illegal character expression";
  11.421 +  in (2, pretty) end;
  11.422 +
  11.423 +fun pretty_numeral c_bit0 c_bit1 c_pls c_min c_bit target =
  11.424 +  let
  11.425 +    val mk_numeral = #pretty_numeral (pr_pretty target);
  11.426 +    fun pretty _ _ _ [(t, _)] =
  11.427 +      case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
  11.428 +       of SOME k => (str o mk_numeral) k
  11.429 +        | NONE => error "Illegal numeral expression";
  11.430 +  in (1, pretty) end;
  11.431 +
  11.432 +fun pretty_ml_string c_char c_nibbles c_nil c_cons target =
  11.433 +  let
  11.434 +    val pretty_ops = pr_pretty target;
  11.435 +    val mk_char = #pretty_char pretty_ops;
  11.436 +    val mk_string = #pretty_string pretty_ops;
  11.437 +    fun pretty pr vars fxy [(t, _)] =
  11.438 +      case implode_list c_nil c_cons t
  11.439 +       of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
  11.440 +           of SOME p => p
  11.441 +            | NONE => error "Illegal ml_string expression")
  11.442 +        | NONE => error "Illegal ml_string expression";
  11.443 +  in (1, pretty) end;
  11.444 +
  11.445 +val pretty_imperative_monad_bind =
  11.446 +  let
  11.447 +    fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
  11.448 +          vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
  11.449 +            pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
  11.450 +      | pretty pr vars fxy [(t1, _), (t2, ty2)] =
  11.451 +          let
  11.452 +            (*this code suffers from the lack of a proper concept for bindings*)
  11.453 +            val vs = CodegenThingol.fold_varnames cons t2 [];
  11.454 +            val v = Name.variant vs "x";
  11.455 +            val vars' = CodegenNames.intro_vars [v] vars;
  11.456 +            val var = IVar v;
  11.457 +            val ty = (hd o fst o CodegenThingol.unfold_fun) ty2;
  11.458 +          in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
  11.459 +  in (2, pretty) end;
  11.460 +
  11.461 +end; (*local*)
  11.462 +
  11.463 +(** ML and Isar interface **)
  11.464  
  11.465  local
  11.466  
  11.467  fun map_syntax_exprs target =
  11.468 -  map_seri_data target o (apsnd o apsnd o apfst o map_syntax_expr);
  11.469 +  map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
  11.470  fun map_syntax_modls target =
  11.471 -  map_seri_data target o (apsnd o apsnd o apsnd o map_syntax_modl);
  11.472 +  map_seri_data target o apsnd o apsnd o apsnd o map_syntax_modl;
  11.473  fun map_reserveds target =
  11.474 -  map_seri_data target o (apsnd o apfst o apsnd);
  11.475 +  map_seri_data target o apsnd o apfst o apsnd;
  11.476  
  11.477  fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
  11.478    let
  11.479 @@ -1716,7 +1799,7 @@
  11.480     of SOME (syntax, raw_ops) =>
  11.481        thy
  11.482        |> (map_syntax_exprs target o apfst o apfst)
  11.483 -           (Symtab.update (class, ((syntax, mk_syntax_ops raw_ops), serial ())))
  11.484 +           (Symtab.update (class, (syntax, mk_syntax_ops raw_ops)))
  11.485      | NONE =>
  11.486        thy
  11.487        |> (map_syntax_exprs target o apfst o apfst)
  11.488 @@ -1747,7 +1830,7 @@
  11.489     of SOME syntax =>
  11.490        thy
  11.491        |> (map_syntax_exprs target o apsnd o apfst)
  11.492 -           (Symtab.update (tyco', (check_args syntax, serial ())))
  11.493 +           (Symtab.update (tyco', check_args syntax))
  11.494     | NONE =>
  11.495        thy
  11.496        |> (map_syntax_exprs target o apsnd o apfst)
  11.497 @@ -1765,7 +1848,7 @@
  11.498     of SOME syntax =>
  11.499        thy
  11.500        |> (map_syntax_exprs target o apsnd o apsnd)
  11.501 -           (Symtab.update (c', (check_args syntax, serial ())))
  11.502 +           (Symtab.update (c', check_args syntax))
  11.503     | NONE =>
  11.504        thy
  11.505        |> (map_syntax_exprs target o apsnd o apsnd)
  11.506 @@ -1881,27 +1964,6 @@
  11.507  fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
  11.508  fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
  11.509  
  11.510 -fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
  11.511 -  let
  11.512 -    val (_, nil'') = idfs_of_const thy nill;
  11.513 -    val (cons', cons'') = idfs_of_const thy cons;
  11.514 -    val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons;
  11.515 -  in
  11.516 -    thy
  11.517 -    |> add_syntax_const target cons' (SOME pr)
  11.518 -  end;
  11.519 -
  11.520 -fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy =
  11.521 -  let
  11.522 -    val (_, nil'') = idfs_of_const thy nill;
  11.523 -    val (_, cons'') = idfs_of_const thy cons;
  11.524 -    val (str', _) = idfs_of_const thy str;
  11.525 -    val pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode;
  11.526 -  in
  11.527 -    thy
  11.528 -    |> add_syntax_const target str' (SOME pr)
  11.529 -  end;
  11.530 -
  11.531  fun add_undefined target undef target_undefined thy =
  11.532    let
  11.533      val (undef', _) = idfs_of_const thy undef;
  11.534 @@ -1911,6 +1973,65 @@
  11.535      |> add_syntax_const target undef' (SOME (~1, pr))
  11.536    end;
  11.537  
  11.538 +fun add_pretty_list target nill cons thy =
  11.539 +  let
  11.540 +    val (_, nil'') = idfs_of_const thy nill;
  11.541 +    val (cons', cons'') = idfs_of_const thy cons;
  11.542 +    val pr = pretty_list nil'' cons'' target;
  11.543 +  in
  11.544 +    thy
  11.545 +    |> add_syntax_const target cons' (SOME pr)
  11.546 +  end;
  11.547 +
  11.548 +fun add_pretty_list_string target nill cons charr nibbles thy =
  11.549 +  let
  11.550 +    val (_, nil'') = idfs_of_const thy nill;
  11.551 +    val (cons', cons'') = idfs_of_const thy cons;
  11.552 +    val (_, charr'') = idfs_of_const thy charr;
  11.553 +    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
  11.554 +    val pr = pretty_list_string nil'' cons'' charr'' nibbles'' target;
  11.555 +  in
  11.556 +    thy
  11.557 +    |> add_syntax_const target cons' (SOME pr)
  11.558 +  end;
  11.559 +
  11.560 +fun add_pretty_char target charr nibbles thy =
  11.561 +  let
  11.562 +    val (charr', charr'') = idfs_of_const thy charr;
  11.563 +    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
  11.564 +    val pr = pretty_char charr'' nibbles'' target;
  11.565 +  in
  11.566 +    thy
  11.567 +    |> add_syntax_const target charr' (SOME pr)
  11.568 +  end;
  11.569 +
  11.570 +fun add_pretty_numeral target number_of b0 b1 pls min bit thy =
  11.571 +  let
  11.572 +    val number_of' = CodegenConsts.const_of_cexpr thy number_of;
  11.573 +    val (_, b0'') = idfs_of_const thy b0;
  11.574 +    val (_, b1'') = idfs_of_const thy b1;
  11.575 +    val (_, pls'') = idfs_of_const thy pls;
  11.576 +    val (_, min'') = idfs_of_const thy min;
  11.577 +    val (_, bit'') = idfs_of_const thy bit;
  11.578 +    val pr = pretty_numeral b0'' b1'' pls'' min'' bit'' target;
  11.579 +  in
  11.580 +    thy
  11.581 +    |> add_syntax_const target number_of' (SOME pr)
  11.582 +  end;
  11.583 +
  11.584 +fun add_pretty_ml_string target charr nibbles nill cons str thy =
  11.585 +  let
  11.586 +    val (_, charr'') = idfs_of_const thy charr;
  11.587 +    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
  11.588 +    val (_, nil'') = idfs_of_const thy nill;
  11.589 +    val (_, cons'') = idfs_of_const thy cons;
  11.590 +    val (str', _) = idfs_of_const thy str;
  11.591 +    val pr = pretty_ml_string charr'' nibbles'' nil'' cons'' target;
  11.592 +  in
  11.593 +    thy
  11.594 +    |> add_syntax_const target str' (SOME pr)
  11.595 +  end;
  11.596 +
  11.597  fun add_pretty_imperative_monad_bind target bind thy =
  11.598    let
  11.599      val (bind', _) = idfs_of_const thy bind;
    12.1 --- a/src/Pure/Tools/codegen_thingol.ML	Thu Apr 26 13:32:55 2007 +0200
    12.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Thu Apr 26 13:32:59 2007 +0200
    12.3 @@ -27,8 +27,6 @@
    12.4      | IVar of vname
    12.5      | `$ of iterm * iterm
    12.6      | `|-> of (vname * itype) * iterm
    12.7 -    | INum of IntInf.int
    12.8 -    | IChar of string (*length one!*)
    12.9      | ICase of (iterm * itype) * (iterm * iterm) list;
   12.10          (*(discriminendum term (td), discriminendum type (ty)),
   12.11                  [(selector pattern (p), body term (t))] (bs))*)
   12.12 @@ -128,8 +126,6 @@
   12.13    | IVar of vname
   12.14    | `$ of iterm * iterm
   12.15    | `|-> of (vname * itype) * iterm
   12.16 -  | INum of IntInf.int
   12.17 -  | IChar of string
   12.18    | ICase of (iterm * itype) * (iterm * iterm) list;
   12.19      (*see also signature*)
   12.20  
   12.21 @@ -198,10 +194,6 @@
   12.22        fold_aiterms f t1 #> fold_aiterms f t2
   12.23    | fold_aiterms f (t as _ `|-> t') =
   12.24        f t #> fold_aiterms f t'
   12.25 -  | fold_aiterms f (t as INum _) =
   12.26 -      f t
   12.27 -  | fold_aiterms f (t as IChar _) =
   12.28 -      f t
   12.29    | fold_aiterms f (ICase ((td, _), bs)) =
   12.30        fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs;
   12.31  
   12.32 @@ -228,10 +220,6 @@
   12.33            add vs t1 #> add vs t2
   12.34        | add vs ((v, _) `|-> t) =
   12.35            add (insert (op =) v vs) t
   12.36 -      | add vs (INum _) =
   12.37 -          I
   12.38 -      | add vs (IChar _) =
   12.39 -          I
   12.40        | add vs (ICase ((td, _), bs)) =
   12.41            add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
   12.42    in add [] end;