src/HOL/String.thy
author wenzelm
Mon Aug 16 22:07:12 1999 +0200 (1999-08-16)
changeset 7224 e41e64476f9b
parent 6395 5abd0d044adf
child 10732 d4fda7d05ce5
permissions -rw-r--r--
'a list: Nil, Cons;
     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   fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
    33 
    34 
    35   val zero = ord "0";
    36   val ten = ord "A" - 10;
    37 
    38   fun mk_nib n =
    39     Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    40 
    41   fun dest_nib (Const (c, _)) =
    42         (case explode c of
    43           ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    44         | _ => raise Match)
    45     | dest_nib _ = raise Match;
    46 
    47   fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    48 
    49 
    50   fun mk_char c =
    51     Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    52 
    53   fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    54     | dest_char _ = raise Match;
    55 
    56 
    57   fun char_tr (*"_Char"*) [Free (xstr, _)] =
    58         (case Syntax.explode_xstr xstr of
    59           [c] => mk_char c
    60         | _ => error ("Single character expected: " ^ xstr))
    61     | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    62 
    63   fun char_tr' (*"Char"*) [t1, t2] =
    64         Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
    65     | char_tr' (*"Char"*) _ = raise Match;
    66 
    67 
    68   (* strings *)
    69 
    70   fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
    71     | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
    72 
    73   fun dest_string (Const ("Nil", _)) = []
    74     | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
    75     | dest_string _ = raise Match;
    76 
    77 
    78   fun string_tr (*"_String"*) [Free (xstr, _)] =
    79         mk_string (map mk_char (Syntax.explode_xstr xstr))
    80     | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    81 
    82   fun cons_tr' (*"Cons"*) [c, cs] =
    83         Syntax.const "_String" $
    84           syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
    85     | cons_tr' (*"Cons"*) ts = raise Match;
    86 
    87 in
    88   val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
    89   val print_translation = [("Char", char_tr'), ("Cons", cons_tr')];
    90 end;