src/HOL/String.thy
author haftmann
Tue May 19 16:54:55 2009 +0200 (2009-05-19)
changeset 31205 98370b26c2ce
parent 31176 92e0ed53db25
child 31484 cabcb95fde29
permissions -rw-r--r--
String.literal replaces message_string, code_numeral replaces (code_)index
     1 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Character and string types *}
     4 
     5 theory String
     6 imports List
     7 uses
     8   "Tools/string_syntax.ML"
     9   ("Tools/string_code.ML")
    10 begin
    11 
    12 subsection {* Characters *}
    13 
    14 datatype nibble =
    15     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    16   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    17 
    18 lemma UNIV_nibble:
    19   "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    20     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
    21 proof (rule UNIV_eq_I)
    22   fix x show "x \<in> ?A" by (cases x) simp_all
    23 qed
    24 
    25 instance nibble :: finite
    26   by default (simp add: UNIV_nibble)
    27 
    28 datatype char = Char nibble nibble
    29   -- "Note: canonical order of character encoding coincides with standard term ordering"
    30 
    31 lemma UNIV_char:
    32   "UNIV = image (split Char) (UNIV \<times> UNIV)"
    33 proof (rule UNIV_eq_I)
    34   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
    35 qed
    36 
    37 instance char :: finite
    38   by default (simp add: UNIV_char)
    39 
    40 lemma size_char [code, simp]:
    41   "size (c::char) = 0" by (cases c) simp
    42 
    43 lemma char_size [code, simp]:
    44   "char_size (c::char) = 0" by (cases c) simp
    45 
    46 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
    47   "nibble_pair_of_char (Char n m) = (n, m)"
    48 
    49 declare nibble_pair_of_char.simps [code del]
    50 
    51 setup {*
    52 let
    53   val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
    54   val thms = map_product
    55    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    56       nibbles nibbles;
    57 in
    58   PureThy.note_thmss Thm.definitionK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
    59   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    60 end
    61 *}
    62 
    63 lemma char_case_nibble_pair [code, code inline]:
    64   "char_case f = split f o nibble_pair_of_char"
    65   by (simp add: expand_fun_eq split: char.split)
    66 
    67 lemma char_rec_nibble_pair [code, code inline]:
    68   "char_rec f = split f o nibble_pair_of_char"
    69   unfolding char_case_nibble_pair [symmetric]
    70   by (simp add: expand_fun_eq split: char.split)
    71 
    72 syntax
    73   "_Char" :: "xstr => char"    ("CHR _")
    74 
    75 
    76 subsection {* Strings *}
    77 
    78 types string = "char list"
    79 
    80 syntax
    81   "_String" :: "xstr => string"    ("_")
    82 
    83 setup StringSyntax.setup
    84 
    85 
    86 subsection {* Strings as dedicated datatype *}
    87 
    88 datatype literal = STR string
    89 
    90 lemmas [code del] = literal.recs literal.cases
    91 
    92 lemma [code]: "size (s\<Colon>literal) = 0"
    93   by (cases s) simp_all
    94 
    95 lemma [code]: "literal_size (s\<Colon>literal) = 0"
    96   by (cases s) simp_all
    97 
    98 
    99 subsection {* Code generator *}
   100 
   101 use "Tools/string_code.ML"
   102 
   103 code_type literal
   104   (SML "string")
   105   (OCaml "string")
   106   (Haskell "String")
   107 
   108 setup {*
   109   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
   110 *}
   111 
   112 code_instance literal :: eq
   113   (Haskell -)
   114 
   115 code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   116   (SML "!((_ : string) = _)")
   117   (OCaml "!((_ : string) = _)")
   118   (Haskell infixl 4 "==")
   119 
   120 code_reserved SML string
   121 code_reserved OCaml string
   122 
   123 
   124 types_code
   125   "char" ("string")
   126 attach (term_of) {*
   127 val term_of_char = HOLogic.mk_char o ord;
   128 *}
   129 attach (test) {*
   130 fun gen_char i =
   131   let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
   132   in (chr j, fn () => HOLogic.mk_char j) end;
   133 *}
   134 
   135 setup {*
   136 let
   137 
   138 fun char_codegen thy defs dep thyname b t gr =
   139   let
   140     val i = HOLogic.dest_char t;
   141     val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
   142       (fastype_of t) gr;
   143   in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
   144   end handle TERM _ => NONE;
   145 
   146 in Codegen.add_codegen "char_codegen" char_codegen end
   147 *}
   148 
   149 hide (open) type literal
   150 
   151 end