ex/String.thy
author nipkow
Fri, 03 Feb 1995 16:19:45 +0100
changeset 208 deec279dda0a
permissions -rw-r--r--
Added Markus Wenzel's string representation.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
208
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/String.thy
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     3
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     4
Hex chars. Strings.
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     5
*)
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     6
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     7
String = List +
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     8
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
     9
datatype
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    10
  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    11
         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    12
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    13
datatype
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    14
  char = Char (nibble, nibble)
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    15
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    16
types
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    17
  string = "char list"
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    18
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    19
syntax
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    20
  "_Char"       :: "xstr => char"       ("CHR _")
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    21
  "_String"     :: "xstr => string"     ("_")
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    22
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    23
end
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    24
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    25
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    26
ML
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    27
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    28
local
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    29
  open Syntax;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    30
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    31
  val ssquote = enclose "''" "''";
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    32
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    33
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    34
  (* chars *)
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    35
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    36
  val zero = ord "0";
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    37
  val ten = ord "A" - 10;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    38
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    39
  fun mk_nib n =
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    40
    const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    41
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    42
  fun dest_nib (Const (c, _)) =
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    43
        (case explode c of
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    44
          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    45
        | _ => raise Match)
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    46
    | dest_nib _ = raise Match;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    47
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    48
  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    49
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    50
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    51
  fun mk_char c =
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    52
    const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    53
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    54
  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    55
    | dest_char _ = raise Match;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    56
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    57
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    58
  fun char_tr (*"_Char"*) [Free (c, _)] =
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    59
        if size c = 1 then mk_char c
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    60
        else error ("Bad character: " ^ quote c)
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    61
    | char_tr (*"_Char"*) ts = raise_term "char_tr" ts;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    62
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    63
  fun char_tr' (*"Char"*) [t1, t2] =
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    64
        const "_Char" $ free (ssquote (dest_nibs t1 t2))
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    65
    | char_tr' (*"Char"*) _ = raise Match;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    66
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    67
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    68
  (* strings *)
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    69
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    70
  fun mk_string [] = const constrainC $ const "[]" $ const "string"
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    71
    | mk_string (t :: ts) = const "op #" $ t $ mk_string ts;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    72
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    73
  fun dest_string (Const ("[]", _)) = []
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    74
    | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    75
    | dest_string _ = raise Match;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    76
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    77
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    78
  fun string_tr (*"_String"*) [Free (txt, _)] =
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    79
        mk_string (map mk_char (explode txt))
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    80
    | string_tr (*"_String"*) ts = raise_term "string_tr" ts;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    81
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    82
  fun cons_tr' (*"op #"*) [c, cs] =
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    83
        const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs)))
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    84
    | cons_tr' (*"op #"*) ts = raise Match;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    85
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    86
in
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    87
  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    88
  val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    89
end;
deec279dda0a Added Markus Wenzel's string representation.
nipkow
parents:
diff changeset
    90