src/HOL/String.thy
author wenzelm
Fri Aug 27 17:59:40 2010 +0200 (2010-08-27)
changeset 38808 89ae86205739
parent 37743 0a3fa8fbcdc5
child 38858 1920158cfa17
permissions -rw-r--r--
more antiquotations;
     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 setup {*
    50 let
    51   val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
    52   val thms = map_product
    53    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    54       nibbles nibbles;
    55 in
    56   PureThy.note_thmss Thm.definitionK [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
    57   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    58 end
    59 *}
    60 
    61 lemma char_case_nibble_pair [code, code_unfold]:
    62   "char_case f = split f o nibble_pair_of_char"
    63   by (simp add: expand_fun_eq split: char.split)
    64 
    65 lemma char_rec_nibble_pair [code, code_unfold]:
    66   "char_rec f = split f o nibble_pair_of_char"
    67   unfolding char_case_nibble_pair [symmetric]
    68   by (simp add: expand_fun_eq split: char.split)
    69 
    70 syntax
    71   "_Char" :: "xstr => char"    ("CHR _")
    72 
    73 
    74 subsection {* Strings *}
    75 
    76 types string = "char list"
    77 
    78 syntax
    79   "_String" :: "xstr => string"    ("_")
    80 
    81 use "Tools/string_syntax.ML"
    82 setup String_Syntax.setup
    83 
    84 definition chars :: string where
    85   "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
    86   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
    87   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
    88   Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
    89   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
    90   Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
    91   Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
    92   Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
    93   Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
    94   Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
    95   Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
    96   Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
    97   Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
    98   CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
    99   CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
   100   CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
   101   CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
   102   CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   103   CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
   104   CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
   105   CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
   106   CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
   107   CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
   108   CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   109   CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
   110   Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
   111   Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
   112   Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
   113   Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
   114   Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
   115   Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
   116   Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
   117   Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
   118   Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
   119   Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
   120   Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
   121   Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
   122   Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
   123   Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
   124   Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
   125   Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
   126   Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
   127   Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
   128   Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
   129   Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
   130   Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
   131   Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
   132   Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
   133   Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
   134   Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
   135   Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
   136   Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
   137   Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
   138   Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
   139   Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
   140   Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
   141   Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
   142   Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
   143   Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
   144   Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
   145   Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
   146   Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
   147   Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
   148   Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
   149   Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
   150   Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
   151   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   152   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   153 
   154 
   155 subsection {* Strings as dedicated datatype *}
   156 
   157 datatype literal = STR string
   158 
   159 declare literal.cases [code del] literal.recs [code del]
   160 
   161 lemma [code]: "size (s\<Colon>literal) = 0"
   162   by (cases s) simp_all
   163 
   164 lemma [code]: "literal_size (s\<Colon>literal) = 0"
   165   by (cases s) simp_all
   166 
   167 
   168 subsection {* Code generator *}
   169 
   170 use "Tools/string_code.ML"
   171 
   172 code_reserved SML string
   173 code_reserved OCaml string
   174 code_reserved Scala string
   175 
   176 code_type literal
   177   (SML "string")
   178   (OCaml "string")
   179   (Haskell "String")
   180   (Scala "String")
   181 
   182 setup {*
   183   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
   184 *}
   185 
   186 code_instance literal :: eq
   187   (Haskell -)
   188 
   189 code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   190   (SML "!((_ : string) = _)")
   191   (OCaml "!((_ : string) = _)")
   192   (Haskell infixl 4 "==")
   193   (Scala infixl 5 "==")
   194 
   195 types_code
   196   "char" ("string")
   197 attach (term_of) {*
   198 val term_of_char = HOLogic.mk_char o ord;
   199 *}
   200 attach (test) {*
   201 fun gen_char i =
   202   let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
   203   in (chr j, fn () => HOLogic.mk_char j) end;
   204 *}
   205 
   206 setup {*
   207 let
   208 
   209 fun char_codegen thy defs dep thyname b t gr =
   210   let
   211     val i = HOLogic.dest_char t;
   212     val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
   213       (fastype_of t) gr;
   214   in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
   215   end handle TERM _ => NONE;
   216 
   217 in Codegen.add_codegen "char_codegen" char_codegen end
   218 *}
   219 
   220 hide_type (open) literal
   221 
   222 
   223 text {* Code generator setup *}
   224 
   225 code_modulename SML
   226   String String
   227 
   228 code_modulename OCaml
   229   String String
   230 
   231 code_modulename Haskell
   232   String String
   233 
   234 end