src/HOL/String.thy
author haftmann
Wed May 06 16:01:23 2009 +0200 (2009-05-06)
changeset 31051 4d9b52e0a48c
child 31055 2cf6efca6c71
permissions -rw-r--r--
refined HOL string theories and corresponding ML fragments
     1 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Character and string types *}
     4 
     5 theory String
     6 imports List
     7 uses "Tools/string_syntax.ML"
     8 begin
     9 
    10 subsection {* Characters *}
    11 
    12 datatype nibble =
    13     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    14   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    15 
    16 lemma UNIV_nibble:
    17   "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    18     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
    19 proof (rule UNIV_eq_I)
    20   fix x show "x \<in> ?A" by (cases x) simp_all
    21 qed
    22 
    23 instance nibble :: finite
    24   by default (simp add: UNIV_nibble)
    25 
    26 datatype char = Char nibble nibble
    27   -- "Note: canonical order of character encoding coincides with standard term ordering"
    28 
    29 lemma UNIV_char:
    30   "UNIV = image (split Char) (UNIV \<times> UNIV)"
    31 proof (rule UNIV_eq_I)
    32   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
    33 qed
    34 
    35 instance char :: finite
    36   by default (simp add: UNIV_char)
    37 
    38 lemma size_char [code, simp]:
    39   "size (c::char) = 0" by (cases c) simp
    40 
    41 lemma char_size [code, simp]:
    42   "char_size (c::char) = 0" by (cases c) simp
    43 
    44 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
    45   "nibble_pair_of_char (Char n m) = (n, m)"
    46 
    47 declare nibble_pair_of_char.simps [code del]
    48 
    49 setup {*
    50 let
    51   val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
    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.lemmaK [((Binding.name "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 inline]:
    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 inline]:
    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 setup StringSyntax.setup
    82 
    83 
    84 subsection {* Strings as dedicated datatype *}
    85 
    86 datatype message_string = STR string
    87 
    88 lemmas [code del] =
    89   message_string.recs message_string.cases
    90 
    91 lemma [code]: "size (s\<Colon>message_string) = 0"
    92   by (cases s) simp_all
    93 
    94 lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
    95   by (cases s) simp_all
    96 
    97 
    98 subsection {* Code generator *}
    99 
   100 text {* This also covers pretty syntax for list literals. *}
   101 
   102 ML {*
   103 local
   104 
   105 open Basic_Code_Thingol;
   106 
   107 fun implode_list naming t = case pairself
   108   (Code_Thingol.lookup_const naming) (@{const_name Nil}, @{const_name Cons})
   109    of (SOME nil', SOME cons') => let
   110           fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
   111                 if c = cons'
   112                 then SOME (t1, t2)
   113                 else NONE
   114             | dest_cons _ = NONE;
   115           val (ts, t') = Code_Thingol.unfoldr dest_cons t;
   116         in case t'
   117          of IConst (c, _) => if c = nil' then SOME ts else NONE
   118           | _ => NONE
   119         end
   120     | _ => NONE
   121 
   122 fun decode_char naming (IConst (c1, _), IConst (c2, _)) = (case map_filter
   123   (Code_Thingol.lookup_const naming)[@{const_name Nibble0}, @{const_name Nibble1},
   124    @{const_name Nibble2}, @{const_name Nibble3},
   125    @{const_name Nibble4}, @{const_name Nibble5},
   126    @{const_name Nibble6}, @{const_name Nibble7},
   127    @{const_name Nibble8}, @{const_name Nibble9},
   128    @{const_name NibbleA}, @{const_name NibbleB},
   129    @{const_name NibbleC}, @{const_name NibbleD},
   130    @{const_name NibbleE}, @{const_name NibbleF}]
   131    of nibbles' as [_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] => let
   132           fun idx c = find_index (curry (op =) c) nibbles';
   133           fun decode ~1 _ = NONE
   134             | decode _ ~1 = NONE
   135             | decode n m = SOME (chr (n * 16 + m));
   136         in decode (idx c1) (idx c2) end
   137     | _ => NONE)
   138  | decode_char _ _ = NONE
   139    
   140 fun implode_string naming mk_char mk_string ts = case
   141   Code_Thingol.lookup_const naming @{const_name Char}
   142    of SOME char' => let
   143         fun implode_char (IConst (c, _) `$ t1 `$ t2) =
   144               if c = char' then decode_char naming (t1, t2) else NONE
   145           | implode_char _ = NONE;
   146         val ts' = map implode_char ts;
   147       in if forall is_some ts'
   148         then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
   149         else NONE
   150       end
   151     | _ => NONE;
   152 
   153 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
   154   Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
   155     pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
   156     Code_Printer.str target_cons,
   157     pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
   158   ];
   159 
   160 fun pretty_list literals =
   161   let
   162     val mk_list = Code_Printer.literal_list literals;
   163     fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
   164       case Option.map (cons t1) (implode_list naming t2)
   165        of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
   166         | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   167   in (2, pretty) end;
   168 
   169 fun pretty_list_string literals =
   170   let
   171     val mk_list = Code_Printer.literal_list literals;
   172     val mk_char = Code_Printer.literal_char literals;
   173     val mk_string = Code_Printer.literal_string literals;
   174     fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
   175       case Option.map (cons t1) (implode_list naming t2)
   176        of SOME ts => (case implode_string naming mk_char mk_string ts
   177            of SOME p => p
   178             | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
   179         | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   180   in (2, pretty) end;
   181 
   182 fun pretty_char literals =
   183   let
   184     val mk_char = Code_Printer.literal_char literals;
   185     fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
   186       case decode_char naming (t1, t2)
   187        of SOME c => (Code_Printer.str o mk_char) c
   188         | NONE => Code_Printer.nerror thm "Illegal character expression";
   189   in (2, pretty) end;
   190 
   191 fun pretty_message literals =
   192   let
   193     val mk_char = Code_Printer.literal_char literals;
   194     val mk_string = Code_Printer.literal_string literals;
   195     fun pretty _ naming thm _ _ [(t, _)] =
   196       case implode_list naming t
   197        of SOME ts => (case implode_string naming mk_char mk_string ts
   198            of SOME p => p
   199             | NONE => Code_Printer.nerror thm "Illegal message expression")
   200         | NONE => Code_Printer.nerror thm "Illegal message expression";
   201   in (1, pretty) end;
   202 
   203 in
   204 
   205 fun add_literal_list target thy =
   206   let
   207     val pr = pretty_list (Code_Target.the_literals thy target);
   208   in
   209     thy
   210     |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
   211   end;
   212 
   213 fun add_literal_list_string target thy =
   214   let
   215     val pr = pretty_list_string (Code_Target.the_literals thy target);
   216   in
   217     thy
   218     |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
   219   end;
   220 
   221 fun add_literal_char target thy =
   222   let
   223     val pr = pretty_char (Code_Target.the_literals thy target);
   224   in
   225     thy
   226     |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
   227   end;
   228 
   229 fun add_literal_message str target thy =
   230   let
   231     val pr = pretty_message (Code_Target.the_literals thy target);
   232   in
   233     thy
   234     |> Code_Target.add_syntax_const target str (SOME pr)
   235   end;
   236 
   237 end;
   238 *}
   239 
   240 setup {*
   241   fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
   242 *}
   243 
   244 code_type message_string
   245   (SML "string")
   246   (OCaml "string")
   247   (Haskell "String")
   248 
   249 setup {*
   250   fold (fn target => add_literal_message @{const_name STR} target)
   251     ["SML", "OCaml", "Haskell"]
   252 *}
   253 
   254 code_instance message_string :: eq
   255   (Haskell -)
   256 
   257 code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
   258   (SML "!((_ : string) = _)")
   259   (OCaml "!((_ : string) = _)")
   260   (Haskell infixl 4 "==")
   261 
   262 code_reserved SML string
   263 code_reserved OCaml string
   264 
   265 
   266 types_code
   267   "char" ("string")
   268 attach (term_of) {*
   269 val term_of_char = HOLogic.mk_char o ord;
   270 *}
   271 attach (test) {*
   272 fun gen_char i =
   273   let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
   274   in (chr j, fn () => HOLogic.mk_char j) end;
   275 *}
   276 
   277 setup {*
   278 let
   279 
   280 fun char_codegen thy defs dep thyname b t gr =
   281   let
   282     val i = HOLogic.dest_char t;
   283     val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
   284       (fastype_of t) gr;
   285   in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
   286   end handle TERM _ => NONE;
   287 
   288 in Codegen.add_codegen "char_codegen" char_codegen end
   289 *}
   290 
   291 end