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;
wenzelm@5121
     1
(*  Title:      HOL/String.thy
wenzelm@5121
     2
    ID:         $Id$
wenzelm@5121
     3
wenzelm@5121
     4
Hex chars and strings.
wenzelm@5121
     5
*)
wenzelm@5121
     6
wenzelm@5121
     7
String = List +
wenzelm@5121
     8
wenzelm@5121
     9
datatype
wenzelm@5121
    10
  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
wenzelm@5121
    11
         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
wenzelm@5121
    12
wenzelm@5121
    13
datatype
wenzelm@5121
    14
  char = Char nibble nibble
wenzelm@5121
    15
wenzelm@5121
    16
types
wenzelm@5121
    17
  string = char list
wenzelm@5121
    18
wenzelm@5121
    19
syntax
wenzelm@5121
    20
  "_Char"       :: xstr => char       ("CHR _")
wenzelm@5121
    21
  "_String"     :: xstr => string     ("_")
wenzelm@5121
    22
wenzelm@5121
    23
end
wenzelm@5121
    24
wenzelm@5121
    25
wenzelm@5121
    26
ML
wenzelm@5121
    27
wenzelm@5121
    28
local
wenzelm@5121
    29
wenzelm@5121
    30
  (* chars *)
wenzelm@5121
    31
wenzelm@5121
    32
  val zero = ord "0";
wenzelm@5121
    33
  val ten = ord "A" - 10;
wenzelm@5121
    34
wenzelm@5121
    35
  fun mk_nib n =
wenzelm@5121
    36
    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
wenzelm@5121
    37
wenzelm@5121
    38
  fun dest_nib (Const (c, _)) =
wenzelm@5121
    39
        (case explode c of
wenzelm@5121
    40
          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
wenzelm@5121
    41
        | _ => raise Match)
wenzelm@5121
    42
    | dest_nib _ = raise Match;
wenzelm@5121
    43
wenzelm@5121
    44
  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
wenzelm@5121
    45
wenzelm@5121
    46
wenzelm@5121
    47
  fun mk_char c =
wenzelm@5121
    48
    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
wenzelm@5121
    49
wenzelm@5121
    50
  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
wenzelm@5121
    51
    | dest_char _ = raise Match;
wenzelm@5121
    52
wenzelm@5121
    53
wenzelm@5121
    54
  fun char_tr (*"_Char"*) [Free (xstr, _)] =
wenzelm@5121
    55
        (case Syntax.explode_xstr xstr of
wenzelm@5121
    56
          [c] => mk_char c
wenzelm@5121
    57
        | _ => error ("Single character expected: " ^ xstr))
wenzelm@5121
    58
    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
wenzelm@5121
    59
wenzelm@5121
    60
  fun char_tr' (*"Char"*) [t1, t2] =
wenzelm@5121
    61
        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
wenzelm@5121
    62
    | char_tr' (*"Char"*) _ = raise Match;
wenzelm@5121
    63
wenzelm@5121
    64
wenzelm@5121
    65
  (* strings *)
wenzelm@5121
    66
wenzelm@5121
    67
  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
wenzelm@5121
    68
    | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts;
wenzelm@5121
    69
wenzelm@5121
    70
  fun dest_string (Const ("[]", _)) = []
wenzelm@5121
    71
    | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
wenzelm@5121
    72
    | dest_string _ = raise Match;
wenzelm@5121
    73
wenzelm@5121
    74
wenzelm@5121
    75
  fun string_tr (*"_String"*) [Free (xstr, _)] =
wenzelm@5121
    76
        mk_string (map mk_char (Syntax.explode_xstr xstr))
wenzelm@5121
    77
    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
wenzelm@5121
    78
wenzelm@5121
    79
  fun cons_tr' (*"op #"*) [c, cs] =
wenzelm@5121
    80
        Syntax.const "_String" $
wenzelm@5121
    81
          Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs))
wenzelm@5121
    82
    | cons_tr' (*"op #"*) ts = raise Match;
wenzelm@5121
    83
wenzelm@5121
    84
in
wenzelm@5121
    85
  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
wenzelm@5121
    86
  val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
wenzelm@5121
    87
end;