refined HOL string theories and corresponding ML fragments
authorhaftmann
Wed May 06 16:01:06 2009 +0200 (2009-05-06)
changeset 31048ac146fc38b51
parent 31047 c13b0406c039
child 31049 396d4d6a1594
refined HOL string theories and corresponding ML fragments
src/HOL/Code_Eval.thy
src/HOL/Code_Message.thy
src/HOL/IsaMakefile
src/HOL/List.thy
src/HOL/Tools/hologic.ML
src/HOL/Tools/string_syntax.ML
src/HOL/Typerep.thy
     1.1 --- a/src/HOL/Code_Eval.thy	Wed May 06 16:01:05 2009 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Wed May 06 16:01:06 2009 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  struct
     1.5  
     1.6  fun mk_term f g (Const (c, ty)) =
     1.7 -      @{term Const} $ Message_String.mk c $ g ty
     1.8 +      @{term Const} $ HOLogic.mk_message_string c $ g ty
     1.9    | mk_term f g (t1 $ t2) =
    1.10        @{term App} $ mk_term f g t1 $ mk_term f g t2
    1.11    | mk_term f g (Free v) = f v
    1.12 @@ -154,7 +154,9 @@
    1.13    (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)")
    1.14  
    1.15  code_const "term_of \<Colon> message_string \<Rightarrow> term"
    1.16 -  (Eval "Message'_String.mk")
    1.17 +  (Eval "HOLogic.mk'_message'_string")
    1.18 +
    1.19 +code_reserved Eval HOLogic
    1.20  
    1.21  
    1.22  subsection {* Evaluation setup *}
     2.1 --- a/src/HOL/Code_Message.thy	Wed May 06 16:01:05 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,56 +0,0 @@
     2.4 -(* Author: Florian Haftmann, TU Muenchen *)
     2.5 -
     2.6 -header {* Monolithic strings (message strings) for code generation *}
     2.7 -
     2.8 -theory Code_Message
     2.9 -imports Plain "~~/src/HOL/List"
    2.10 -begin
    2.11 -
    2.12 -subsection {* Datatype of messages *}
    2.13 -
    2.14 -datatype message_string = STR string
    2.15 -
    2.16 -lemmas [code del] = message_string.recs message_string.cases
    2.17 -
    2.18 -lemma [code]: "size (s\<Colon>message_string) = 0"
    2.19 -  by (cases s) simp_all
    2.20 -
    2.21 -lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
    2.22 -  by (cases s) simp_all
    2.23 -
    2.24 -subsection {* ML interface *}
    2.25 -
    2.26 -ML {*
    2.27 -structure Message_String =
    2.28 -struct
    2.29 -
    2.30 -fun mk s = @{term STR} $ HOLogic.mk_string s;
    2.31 -
    2.32 -end;
    2.33 -*}
    2.34 -
    2.35 -
    2.36 -subsection {* Code serialization *}
    2.37 -
    2.38 -code_type message_string
    2.39 -  (SML "string")
    2.40 -  (OCaml "string")
    2.41 -  (Haskell "String")
    2.42 -
    2.43 -setup {*
    2.44 -  fold (fn target => add_literal_message @{const_name STR} target)
    2.45 -    ["SML", "OCaml", "Haskell"]
    2.46 -*}
    2.47 -
    2.48 -code_reserved SML string
    2.49 -code_reserved OCaml string
    2.50 -
    2.51 -code_instance message_string :: eq
    2.52 -  (Haskell -)
    2.53 -
    2.54 -code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
    2.55 -  (SML "!((_ : string) = _)")
    2.56 -  (OCaml "!((_ : string) = _)")
    2.57 -  (Haskell infixl 4 "==")
    2.58 -
    2.59 -end
     3.1 --- a/src/HOL/IsaMakefile	Wed May 06 16:01:05 2009 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Wed May 06 16:01:06 2009 +0200
     3.3 @@ -206,7 +206,6 @@
     3.4  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
     3.5    ATP_Linkup.thy \
     3.6    Code_Eval.thy \
     3.7 -  Code_Message.thy \
     3.8    Equiv_Relations.thy \
     3.9    Groebner_Basis.thy \
    3.10    Hilbert_Choice.thy \
    3.11 @@ -220,6 +219,7 @@
    3.12    Presburger.thy \
    3.13    Recdef.thy \
    3.14    SetInterval.thy \
    3.15 +  String.thy \
    3.16    $(SRC)/Provers/Arith/assoc_fold.ML \
    3.17    $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
    3.18    $(SRC)/Provers/Arith/cancel_numerals.ML \
     4.1 --- a/src/HOL/List.thy	Wed May 06 16:01:05 2009 +0200
     4.2 +++ b/src/HOL/List.thy	Wed May 06 16:01:06 2009 +0200
     4.3 @@ -6,7 +6,6 @@
     4.4  
     4.5  theory List
     4.6  imports Plain Presburger Recdef ATP_Linkup
     4.7 -uses "Tools/string_syntax.ML"
     4.8  begin
     4.9  
    4.10  datatype 'a list =
    4.11 @@ -3433,77 +3432,6 @@
    4.12  by (auto simp add: set_Cons_def intro: listrel.intros) 
    4.13  
    4.14  
    4.15 -subsection{*Miscellany*}
    4.16 -
    4.17 -subsubsection {* Characters and strings *}
    4.18 -
    4.19 -datatype nibble =
    4.20 -    Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    4.21 -  | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    4.22 -
    4.23 -lemma UNIV_nibble:
    4.24 -  "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    4.25 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
    4.26 -proof (rule UNIV_eq_I)
    4.27 -  fix x show "x \<in> ?A" by (cases x) simp_all
    4.28 -qed
    4.29 -
    4.30 -instance nibble :: finite
    4.31 -  by default (simp add: UNIV_nibble)
    4.32 -
    4.33 -datatype char = Char nibble nibble
    4.34 -  -- "Note: canonical order of character encoding coincides with standard term ordering"
    4.35 -
    4.36 -lemma UNIV_char:
    4.37 -  "UNIV = image (split Char) (UNIV \<times> UNIV)"
    4.38 -proof (rule UNIV_eq_I)
    4.39 -  fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
    4.40 -qed
    4.41 -
    4.42 -instance char :: finite
    4.43 -  by default (simp add: UNIV_char)
    4.44 -
    4.45 -lemma size_char [code, simp]:
    4.46 -  "size (c::char) = 0" by (cases c) simp
    4.47 -
    4.48 -lemma char_size [code, simp]:
    4.49 -  "char_size (c::char) = 0" by (cases c) simp
    4.50 -
    4.51 -primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
    4.52 -  "nibble_pair_of_char (Char n m) = (n, m)"
    4.53 -
    4.54 -declare nibble_pair_of_char.simps [code del]
    4.55 -
    4.56 -setup {*
    4.57 -let
    4.58 -  val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
    4.59 -  val thms = map_product
    4.60 -   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    4.61 -      nibbles nibbles;
    4.62 -in
    4.63 -  PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
    4.64 -  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    4.65 -end
    4.66 -*}
    4.67 -
    4.68 -lemma char_case_nibble_pair [code, code inline]:
    4.69 -  "char_case f = split f o nibble_pair_of_char"
    4.70 -  by (simp add: expand_fun_eq split: char.split)
    4.71 -
    4.72 -lemma char_rec_nibble_pair [code, code inline]:
    4.73 -  "char_rec f = split f o nibble_pair_of_char"
    4.74 -  unfolding char_case_nibble_pair [symmetric]
    4.75 -  by (simp add: expand_fun_eq split: char.split)
    4.76 -
    4.77 -types string = "char list"
    4.78 -
    4.79 -syntax
    4.80 -  "_Char" :: "xstr => char"    ("CHR _")
    4.81 -  "_String" :: "xstr => string"    ("_")
    4.82 -
    4.83 -setup StringSyntax.setup
    4.84 -
    4.85 -
    4.86  subsection {* Size function *}
    4.87  
    4.88  lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
    4.89 @@ -3527,10 +3455,38 @@
    4.90    "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
    4.91  by (induct xs) force+
    4.92  
    4.93 +
    4.94  subsection {* Code generator *}
    4.95  
    4.96  subsubsection {* Setup *}
    4.97  
    4.98 +code_type list
    4.99 +  (SML "_ list")
   4.100 +  (OCaml "_ list")
   4.101 +  (Haskell "![_]")
   4.102 +
   4.103 +code_const Nil
   4.104 +  (SML "[]")
   4.105 +  (OCaml "[]")
   4.106 +  (Haskell "[]")
   4.107 +
   4.108 +code_const Cons
   4.109 +  (SML infixr 7 "::")
   4.110 +  (OCaml infixr 6 "::")
   4.111 +  (Haskell infixr 5 ":")
   4.112 +
   4.113 +code_instance list :: eq
   4.114 +  (Haskell -)
   4.115 +
   4.116 +code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   4.117 +  (Haskell infixl 4 "==")
   4.118 +
   4.119 +code_reserved SML
   4.120 +  list
   4.121 +
   4.122 +code_reserved OCaml
   4.123 +  list
   4.124 +
   4.125  types_code
   4.126    "list" ("_ list")
   4.127  attach (term_of) {*
   4.128 @@ -3546,181 +3502,9 @@
   4.129     (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
   4.130  and gen_list aG aT i = gen_list' aG aT i i;
   4.131  *}
   4.132 -  "char" ("string")
   4.133 -attach (term_of) {*
   4.134 -val term_of_char = HOLogic.mk_char o ord;
   4.135 -*}
   4.136 -attach (test) {*
   4.137 -fun gen_char i =
   4.138 -  let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
   4.139 -  in (chr j, fn () => HOLogic.mk_char j) end;
   4.140 -*}
   4.141 -
   4.142 -consts_code "Cons" ("(_ ::/ _)")
   4.143 -
   4.144 -code_type list
   4.145 -  (SML "_ list")
   4.146 -  (OCaml "_ list")
   4.147 -  (Haskell "![_]")
   4.148 -
   4.149 -code_reserved SML
   4.150 -  list
   4.151 -
   4.152 -code_reserved OCaml
   4.153 -  list
   4.154 -
   4.155 -code_const Nil
   4.156 -  (SML "[]")
   4.157 -  (OCaml "[]")
   4.158 -  (Haskell "[]")
   4.159 -
   4.160 -ML {*
   4.161 -local
   4.162 -
   4.163 -open Basic_Code_Thingol;
   4.164 -
   4.165 -fun implode_list naming t = case pairself
   4.166 -  (Code_Thingol.lookup_const naming) (@{const_name Nil}, @{const_name Cons})
   4.167 -   of (SOME nil', SOME cons') => let
   4.168 -          fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
   4.169 -                if c = cons'
   4.170 -                then SOME (t1, t2)
   4.171 -                else NONE
   4.172 -            | dest_cons _ = NONE;
   4.173 -          val (ts, t') = Code_Thingol.unfoldr dest_cons t;
   4.174 -        in case t'
   4.175 -         of IConst (c, _) => if c = nil' then SOME ts else NONE
   4.176 -          | _ => NONE
   4.177 -        end
   4.178 -    | _ => NONE
   4.179 -
   4.180 -fun decode_char naming (IConst (c1, _), IConst (c2, _)) = (case map_filter
   4.181 -  (Code_Thingol.lookup_const naming)[@{const_name Nibble0}, @{const_name Nibble1},
   4.182 -   @{const_name Nibble2}, @{const_name Nibble3},
   4.183 -   @{const_name Nibble4}, @{const_name Nibble5},
   4.184 -   @{const_name Nibble6}, @{const_name Nibble7},
   4.185 -   @{const_name Nibble8}, @{const_name Nibble9},
   4.186 -   @{const_name NibbleA}, @{const_name NibbleB},
   4.187 -   @{const_name NibbleC}, @{const_name NibbleD},
   4.188 -   @{const_name NibbleE}, @{const_name NibbleF}]
   4.189 -   of nibbles' as [_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] => let
   4.190 -          fun idx c = find_index (curry (op =) c) nibbles';
   4.191 -          fun decode ~1 _ = NONE
   4.192 -            | decode _ ~1 = NONE
   4.193 -            | decode n m = SOME (chr (n * 16 + m));
   4.194 -        in decode (idx c1) (idx c2) end
   4.195 -    | _ => NONE)
   4.196 - | decode_char _ _ = NONE
   4.197 -   
   4.198 -fun implode_string naming mk_char mk_string ts = case
   4.199 -  Code_Thingol.lookup_const naming @{const_name Char}
   4.200 -   of SOME char' => let
   4.201 -        fun implode_char (IConst (c, _) `$ t1 `$ t2) =
   4.202 -              if c = char' then decode_char naming (t1, t2) else NONE
   4.203 -          | implode_char _ = NONE;
   4.204 -        val ts' = map implode_char ts;
   4.205 -      in if forall is_some ts'
   4.206 -        then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
   4.207 -        else NONE
   4.208 -      end
   4.209 -    | _ => NONE;
   4.210 -
   4.211 -fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
   4.212 -  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
   4.213 -    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
   4.214 -    Code_Printer.str target_cons,
   4.215 -    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
   4.216 -  ];
   4.217 -
   4.218 -fun pretty_list literals =
   4.219 -  let
   4.220 -    val mk_list = Code_Printer.literal_list literals;
   4.221 -    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
   4.222 -      case Option.map (cons t1) (implode_list naming t2)
   4.223 -       of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
   4.224 -        | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   4.225 -  in (2, pretty) end;
   4.226 -
   4.227 -fun pretty_list_string literals =
   4.228 -  let
   4.229 -    val mk_list = Code_Printer.literal_list literals;
   4.230 -    val mk_char = Code_Printer.literal_char literals;
   4.231 -    val mk_string = Code_Printer.literal_string literals;
   4.232 -    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
   4.233 -      case Option.map (cons t1) (implode_list naming t2)
   4.234 -       of SOME ts => (case implode_string naming mk_char mk_string ts
   4.235 -           of SOME p => p
   4.236 -            | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
   4.237 -        | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   4.238 -  in (2, pretty) end;
   4.239 -
   4.240 -fun pretty_char literals =
   4.241 -  let
   4.242 -    val mk_char = Code_Printer.literal_char literals;
   4.243 -    fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
   4.244 -      case decode_char naming (t1, t2)
   4.245 -       of SOME c => (Code_Printer.str o mk_char) c
   4.246 -        | NONE => Code_Printer.nerror thm "Illegal character expression";
   4.247 -  in (2, pretty) end;
   4.248 -
   4.249 -fun pretty_message literals =
   4.250 -  let
   4.251 -    val mk_char = Code_Printer.literal_char literals;
   4.252 -    val mk_string = Code_Printer.literal_string literals;
   4.253 -    fun pretty _ naming thm _ _ [(t, _)] =
   4.254 -      case implode_list naming t
   4.255 -       of SOME ts => (case implode_string naming mk_char mk_string ts
   4.256 -           of SOME p => p
   4.257 -            | NONE => Code_Printer.nerror thm "Illegal message expression")
   4.258 -        | NONE => Code_Printer.nerror thm "Illegal message expression";
   4.259 -  in (1, pretty) end;
   4.260 -
   4.261 -in
   4.262 -
   4.263 -fun add_literal_list target thy =
   4.264 -  let
   4.265 -    val pr = pretty_list (Code_Target.the_literals thy target);
   4.266 -  in
   4.267 -    thy
   4.268 -    |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
   4.269 -  end;
   4.270 -
   4.271 -fun add_literal_list_string target thy =
   4.272 -  let
   4.273 -    val pr = pretty_list_string (Code_Target.the_literals thy target);
   4.274 -  in
   4.275 -    thy
   4.276 -    |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
   4.277 -  end;
   4.278 -
   4.279 -fun add_literal_char target thy =
   4.280 -  let
   4.281 -    val pr = pretty_char (Code_Target.the_literals thy target);
   4.282 -  in
   4.283 -    thy
   4.284 -    |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
   4.285 -  end;
   4.286 -
   4.287 -fun add_literal_message str target thy =
   4.288 -  let
   4.289 -    val pr = pretty_message (Code_Target.the_literals thy target);
   4.290 -  in
   4.291 -    thy
   4.292 -    |> Code_Target.add_syntax_const target str (SOME pr)
   4.293 -  end;
   4.294 -
   4.295 -end;
   4.296 -*}
   4.297 -
   4.298 -setup {*
   4.299 -  fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
   4.300 -*}
   4.301 -
   4.302 -code_instance list :: eq
   4.303 -  (Haskell -)
   4.304 -
   4.305 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   4.306 -  (Haskell infixl 4 "==")
   4.307 +
   4.308 +consts_code Nil ("[]")
   4.309 +consts_code Cons ("(_ ::/ _)")
   4.310  
   4.311  setup {*
   4.312  let
   4.313 @@ -3734,18 +3518,7 @@
   4.314        (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
   4.315    in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
   4.316  
   4.317 -fun char_codegen thy defs dep thyname b t gr =
   4.318 -  let
   4.319 -    val i = HOLogic.dest_char t;
   4.320 -    val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
   4.321 -      (fastype_of t) gr;
   4.322 -  in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
   4.323 -  end handle TERM _ => NONE;
   4.324 -
   4.325 -in
   4.326 -  Codegen.add_codegen "list_codegen" list_codegen
   4.327 -  #> Codegen.add_codegen "char_codegen" char_codegen
   4.328 -end;
   4.329 +in Codegen.add_codegen "list_codegen" list_codegen end
   4.330  *}
   4.331  
   4.332  
     5.1 --- a/src/HOL/Tools/hologic.ML	Wed May 06 16:01:05 2009 +0200
     5.2 +++ b/src/HOL/Tools/hologic.ML	Wed May 06 16:01:06 2009 +0200
     5.3 @@ -116,6 +116,9 @@
     5.4    val stringT: typ
     5.5    val mk_string: string -> term
     5.6    val dest_string: term -> string
     5.7 +  val message_stringT: typ
     5.8 +  val mk_message_string: string -> term
     5.9 +  val dest_message_string: term -> string
    5.10  end;
    5.11  
    5.12  structure HOLogic: HOLOGIC =
    5.13 @@ -510,44 +513,6 @@
    5.14  val realT = Type ("RealDef.real", []);
    5.15  
    5.16  
    5.17 -(* nibble *)
    5.18 -
    5.19 -val nibbleT = Type ("List.nibble", []);
    5.20 -
    5.21 -fun mk_nibble n =
    5.22 -  let val s =
    5.23 -    if 0 <= n andalso n <= 9 then chr (n + ord "0")
    5.24 -    else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10)
    5.25 -    else raise TERM ("mk_nibble", [])
    5.26 -  in Const ("List.nibble.Nibble" ^ s, nibbleT) end;
    5.27 -
    5.28 -fun dest_nibble t =
    5.29 -  let fun err () = raise TERM ("dest_nibble", [t]) in
    5.30 -    (case try (unprefix "List.nibble.Nibble" o fst o Term.dest_Const) t of
    5.31 -      NONE => err ()
    5.32 -    | SOME c =>
    5.33 -        if size c <> 1 then err ()
    5.34 -        else if "0" <= c andalso c <= "9" then ord c - ord "0"
    5.35 -        else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
    5.36 -        else err ())
    5.37 -  end;
    5.38 -
    5.39 -
    5.40 -(* char *)
    5.41 -
    5.42 -val charT = Type ("List.char", []);
    5.43 -
    5.44 -fun mk_char n =
    5.45 -  if 0 <= n andalso n <= 255 then
    5.46 -    Const ("List.char.Char", nibbleT --> nibbleT --> charT) $
    5.47 -      mk_nibble (n div 16) $ mk_nibble (n mod 16)
    5.48 -  else raise TERM ("mk_char", []);
    5.49 -
    5.50 -fun dest_char (Const ("List.char.Char", _) $ t $ u) =
    5.51 -      dest_nibble t * 16 + dest_nibble u
    5.52 -  | dest_char t = raise TERM ("dest_char", [t]);
    5.53 -
    5.54 -
    5.55  (* list *)
    5.56  
    5.57  fun listT T = Type ("List.list", [T]);
    5.58 @@ -570,11 +535,60 @@
    5.59    | dest_list t = raise TERM ("dest_list", [t]);
    5.60  
    5.61  
    5.62 +(* nibble *)
    5.63 +
    5.64 +val nibbleT = Type ("String.nibble", []);
    5.65 +
    5.66 +fun mk_nibble n =
    5.67 +  let val s =
    5.68 +    if 0 <= n andalso n <= 9 then chr (n + ord "0")
    5.69 +    else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10)
    5.70 +    else raise TERM ("mk_nibble", [])
    5.71 +  in Const ("String.nibble.Nibble" ^ s, nibbleT) end;
    5.72 +
    5.73 +fun dest_nibble t =
    5.74 +  let fun err () = raise TERM ("dest_nibble", [t]) in
    5.75 +    (case try (unprefix "String.nibble.Nibble" o fst o Term.dest_Const) t of
    5.76 +      NONE => err ()
    5.77 +    | SOME c =>
    5.78 +        if size c <> 1 then err ()
    5.79 +        else if "0" <= c andalso c <= "9" then ord c - ord "0"
    5.80 +        else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
    5.81 +        else err ())
    5.82 +  end;
    5.83 +
    5.84 +
    5.85 +(* char *)
    5.86 +
    5.87 +val charT = Type ("String.char", []);
    5.88 +
    5.89 +fun mk_char n =
    5.90 +  if 0 <= n andalso n <= 255 then
    5.91 +    Const ("String.char.Char", nibbleT --> nibbleT --> charT) $
    5.92 +      mk_nibble (n div 16) $ mk_nibble (n mod 16)
    5.93 +  else raise TERM ("mk_char", []);
    5.94 +
    5.95 +fun dest_char (Const ("String.char.Char", _) $ t $ u) =
    5.96 +      dest_nibble t * 16 + dest_nibble u
    5.97 +  | dest_char t = raise TERM ("dest_char", [t]);
    5.98 +
    5.99 +
   5.100  (* string *)
   5.101  
   5.102 -val stringT = Type ("List.string", []);
   5.103 +val stringT = Type ("String.string", []);
   5.104  
   5.105  val mk_string = mk_list charT o map (mk_char o ord) o explode;
   5.106  val dest_string = implode o map (chr o dest_char) o dest_list;
   5.107  
   5.108 +
   5.109 +(* message_string *)
   5.110 +
   5.111 +val message_stringT = Type ("String.message_string", []);
   5.112 +
   5.113 +fun mk_message_string s = Const ("String.message_string.STR", stringT --> message_stringT)
   5.114 +      $ mk_string s;
   5.115 +fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
   5.116 +      dest_string t
   5.117 +  | dest_message_string t = raise TERM ("dest_message_string", [t]);
   5.118 +
   5.119  end;
     6.1 --- a/src/HOL/Tools/string_syntax.ML	Wed May 06 16:01:05 2009 +0200
     6.2 +++ b/src/HOL/Tools/string_syntax.ML	Wed May 06 16:01:06 2009 +0200
     6.3 @@ -15,12 +15,14 @@
     6.4  
     6.5  (* nibble *)
     6.6  
     6.7 +val nib_prefix = "String.nibble.";
     6.8 +
     6.9  val mk_nib =
    6.10 -  Syntax.Constant o unprefix "List.nibble." o
    6.11 +  Syntax.Constant o unprefix nib_prefix o
    6.12    fst o Term.dest_Const o HOLogic.mk_nibble;
    6.13  
    6.14  fun dest_nib (Syntax.Constant c) =
    6.15 -  HOLogic.dest_nibble (Const ("List.nibble." ^ c, dummyT))
    6.16 +  HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))
    6.17      handle TERM _ => raise Match;
    6.18  
    6.19  
     7.1 --- a/src/HOL/Typerep.thy	Wed May 06 16:01:05 2009 +0200
     7.2 +++ b/src/HOL/Typerep.thy	Wed May 06 16:01:06 2009 +0200
     7.3 @@ -1,11 +1,9 @@
     7.4 -(*  Title:      HOL/Typerep.thy
     7.5 -    Author:     Florian Haftmann, TU Muenchen
     7.6 -*)
     7.7 +(* Author: Florian Haftmann, TU Muenchen *)
     7.8  
     7.9  header {* Reflecting Pure types into HOL *}
    7.10  
    7.11  theory Typerep
    7.12 -imports Plain List Code_Message
    7.13 +imports Plain String
    7.14  begin
    7.15  
    7.16  datatype typerep = Typerep message_string "typerep list"
    7.17 @@ -42,7 +40,7 @@
    7.18  struct
    7.19  
    7.20  fun mk f (Type (tyco, tys)) =
    7.21 -      @{term Typerep} $ Message_String.mk tyco
    7.22 +      @{term Typerep} $ HOLogic.mk_message_string tyco
    7.23          $ HOLogic.mk_list @{typ typerep} (map (mk f) tys)
    7.24    | mk f (TFree v) =
    7.25        f v;