src/HOL/String.thy
author haftmann
Wed May 06 19:09:31 2009 +0200 (2009-05-06)
changeset 31055 2cf6efca6c71
parent 31051 4d9b52e0a48c
child 31174 f1f1e9b53c81
permissions -rw-r--r--
proper structures for list and string code generation stuff
     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.lemmaK [((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 message_string = STR string
    89 
    90 lemmas [code del] =
    91   message_string.recs message_string.cases
    92 
    93 lemma [code]: "size (s\<Colon>message_string) = 0"
    94   by (cases s) simp_all
    95 
    96 lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
    97   by (cases s) simp_all
    98 
    99 
   100 subsection {* Code generator *}
   101 
   102 use "Tools/string_code.ML"
   103 
   104 code_type message_string
   105   (SML "string")
   106   (OCaml "string")
   107   (Haskell "String")
   108 
   109 setup {*
   110   fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
   111 *}
   112 
   113 code_instance message_string :: eq
   114   (Haskell -)
   115 
   116 code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
   117   (SML "!((_ : string) = _)")
   118   (OCaml "!((_ : string) = _)")
   119   (Haskell infixl 4 "==")
   120 
   121 code_reserved SML string
   122 code_reserved OCaml string
   123 
   124 
   125 types_code
   126   "char" ("string")
   127 attach (term_of) {*
   128 val term_of_char = HOLogic.mk_char o ord;
   129 *}
   130 attach (test) {*
   131 fun gen_char i =
   132   let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
   133   in (chr j, fn () => HOLogic.mk_char j) end;
   134 *}
   135 
   136 setup {*
   137 let
   138 
   139 fun char_codegen thy defs dep thyname b t gr =
   140   let
   141     val i = HOLogic.dest_char t;
   142     val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
   143       (fastype_of t) gr;
   144   in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
   145   end handle TERM _ => NONE;
   146 
   147 in Codegen.add_codegen "char_codegen" char_codegen end
   148 *}
   149 
   150 end