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