src/HOL/String.thy
author wenzelm
Fri Jul 03 17:33:47 1998 +0200 (1998-07-03)
changeset 5121 5c1f89ae8aef
child 6395 5abd0d044adf
permissions -rw-r--r--
moved String theory to main HOL;
     1 (*  Title:      HOL/String.thy
     2     ID:         $Id$
     3 
     4 Hex chars and 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 
    30   (* chars *)
    31 
    32   val zero = ord "0";
    33   val ten = ord "A" - 10;
    34 
    35   fun mk_nib n =
    36     Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    37 
    38   fun dest_nib (Const (c, _)) =
    39         (case explode c of
    40           ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    41         | _ => raise Match)
    42     | dest_nib _ = raise Match;
    43 
    44   fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    45 
    46 
    47   fun mk_char c =
    48     Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    49 
    50   fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    51     | dest_char _ = raise Match;
    52 
    53 
    54   fun char_tr (*"_Char"*) [Free (xstr, _)] =
    55         (case Syntax.explode_xstr xstr of
    56           [c] => mk_char c
    57         | _ => error ("Single character expected: " ^ xstr))
    58     | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    59 
    60   fun char_tr' (*"Char"*) [t1, t2] =
    61         Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
    62     | char_tr' (*"Char"*) _ = raise Match;
    63 
    64 
    65   (* strings *)
    66 
    67   fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
    68     | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts;
    69 
    70   fun dest_string (Const ("[]", _)) = []
    71     | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
    72     | dest_string _ = raise Match;
    73 
    74 
    75   fun string_tr (*"_String"*) [Free (xstr, _)] =
    76         mk_string (map mk_char (Syntax.explode_xstr xstr))
    77     | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    78 
    79   fun cons_tr' (*"op #"*) [c, cs] =
    80         Syntax.const "_String" $
    81           Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs))
    82     | cons_tr' (*"op #"*) ts = raise Match;
    83 
    84 in
    85   val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
    86   val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
    87 end;