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