src/HOL/ex/String.thy
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 3795 e687069e7257
child 4253 901f690e3a58
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/String.thy
     2     ID:         $Id$
     3 
     4 Hex chars. Strings.
     5 *)
     6 
     7 String = List +
     8 
     9 datatype
    10   nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
    11          | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
    12 
    13 datatype
    14   char = Char nibble nibble
    15 
    16 types
    17   string = char list
    18 
    19 syntax
    20   "_Char"       :: xstr => char       ("CHR _")
    21   "_String"     :: xstr => string     ("_")
    22 
    23 end
    24 
    25 
    26 ML
    27 
    28 local
    29   open Syntax;
    30 
    31   val ssquote = enclose "''" "''";
    32 
    33 
    34   (* chars *)
    35 
    36   val zero = ord "0";
    37   val ten = ord "A" - 10;
    38 
    39   fun mk_nib n =
    40     const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    41 
    42   fun dest_nib (Const (c, _)) =
    43         (case explode c of
    44           ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    45         | _ => raise Match)
    46     | dest_nib _ = raise Match;
    47 
    48   fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    49 
    50 
    51   fun mk_char c =
    52     const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    53 
    54   fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    55     | dest_char _ = raise Match;
    56 
    57 
    58   fun char_tr (*"_Char"*) [Free (c, _)] =
    59         if size c = 1 then mk_char c
    60         else error ("Bad character: " ^ quote c)
    61     | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    62 
    63   fun char_tr' (*"Char"*) [t1, t2] =
    64         const "_Char" $ free (ssquote (dest_nibs t1 t2))
    65     | char_tr' (*"Char"*) _ = raise Match;
    66 
    67 
    68   (* strings *)
    69 
    70   fun mk_string [] = const constrainC $ const "[]" $ const "string"
    71     | mk_string (t :: ts) = const "op #" $ t $ mk_string ts;
    72 
    73   fun dest_string (Const ("[]", _)) = []
    74     | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
    75     | dest_string _ = raise Match;
    76 
    77 
    78   fun string_tr (*"_String"*) [Free (txt, _)] =
    79         mk_string (map mk_char (explode txt))
    80     | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    81 
    82   fun cons_tr' (*"op #"*) [c, cs] =
    83         const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs)))
    84     | cons_tr' (*"op #"*) ts = raise Match;
    85 
    86 in
    87   val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
    88   val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
    89 end;
    90