src/HOL/String.thy
author wenzelm
Tue Jan 16 00:30:06 2001 +0100 (2001-01-16)
changeset 10909 2bbb1797bbe2
parent 10732 d4fda7d05ce5
permissions -rw-r--r--
improved string syntax (allow translation rules);
     1 (*  Title:      HOL/String.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Hex chars and strings.
     7 *)
     8 
     9 theory String = List:
    10 
    11 datatype nibble =
    12     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    13   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    14 
    15 datatype char = Char nibble nibble
    16   -- "Note: canonical order of character encoding coincides with standard term ordering"
    17 
    18 types string = "char list"
    19 
    20 syntax
    21   "_Char" :: "xstr => char"    ("CHR _")
    22   "_String" :: "xstr => string"    ("_")
    23 
    24 parse_ast_translation {*
    25   let
    26     val constants = Syntax.Appl o map Syntax.Constant;
    27 
    28     fun mk_nib n = "Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10));
    29     fun mk_char c =
    30       if Symbol.is_ascii c andalso Symbol.is_printable c then
    31         constants ["Char", mk_nib (ord c div 16), mk_nib (ord c mod 16)]
    32       else error ("Printable ASCII character expected: " ^ quote c);
    33 
    34     fun mk_string [] = Syntax.Constant "Nil"
    35       | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
    36 
    37     fun char_ast_tr [Syntax.Variable xstr] =
    38         (case Syntax.explode_xstr xstr of
    39           [c] => mk_char c
    40         | _ => error ("Single character expected: " ^ xstr))
    41       | char_ast_tr asts = raise AST ("char_ast_tr", asts);
    42 
    43     fun string_ast_tr [Syntax.Variable xstr] =
    44         (case Syntax.explode_xstr xstr of
    45           [] => constants [Syntax.constrainC, "Nil", "string"]
    46         | cs => mk_string cs)
    47       | string_ast_tr asts = raise AST ("string_tr", asts);
    48   in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end;
    49 *}
    50 
    51 print_ast_translation {*
    52   let
    53     fun dest_nib (Syntax.Constant c) =
    54         (case explode c of
    55           ["N", "i", "b", "b", "l", "e", h] =>
    56             if "0" <= h andalso h <= "9" then ord h - ord "0"
    57             else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
    58             else raise Match
    59         | _ => raise Match)
    60       | dest_nib _ = raise Match;
    61 
    62     fun dest_chr c1 c2 =
    63       let val c = chr (dest_nib c1 * 16 + dest_nib c2)
    64       in if Symbol.is_printable c then c else raise Match end;
    65 
    66     fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
    67       | dest_char _ = raise Match;
    68 
    69     fun xstr cs = Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
    70 
    71     fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", xstr [dest_chr c1 c2]]
    72       | char_ast_tr' _ = raise Match;
    73 
    74     fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
    75             xstr (map dest_char (Syntax.unfold_ast "_args" args))]
    76       | list_ast_tr' ts = raise Match;
    77   in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
    78 *}
    79 
    80 end