src/HOL/String.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 7224 e41e64476f9b
child 10732 d4fda7d05ce5
permissions -rw-r--r--
hide many names from Datatype_Universe.
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$
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     3
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     4
Hex chars and strings.
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     5
*)
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     6
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     7
String = List +
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     8
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
     9
datatype
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    10
  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    11
         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    12
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    13
datatype
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    14
  char = Char nibble nibble
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    15
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    16
types
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    17
  string = char list
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    18
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    19
syntax
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    20
  "_Char"       :: xstr => char       ("CHR _")
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    21
  "_String"     :: xstr => string     ("_")
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    22
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    23
end
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    24
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    25
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    26
ML
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    27
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    28
local
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    29
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    30
  (* chars *)
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    31
6395
5abd0d044adf xstr token class;
wenzelm
parents: 5121
diff changeset
    32
  fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
5abd0d044adf xstr token class;
wenzelm
parents: 5121
diff changeset
    33
5abd0d044adf xstr token class;
wenzelm
parents: 5121
diff changeset
    34
5121
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    35
  val zero = ord "0";
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    36
  val ten = ord "A" - 10;
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    37
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    38
  fun mk_nib n =
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    39
    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    40
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    41
  fun dest_nib (Const (c, _)) =
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    42
        (case explode c of
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    43
          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    44
        | _ => raise Match)
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    45
    | dest_nib _ = raise Match;
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    46
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    47
  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    48
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    49
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    50
  fun mk_char c =
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    51
    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    52
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    53
  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    54
    | dest_char _ = raise Match;
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    55
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    56
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    57
  fun char_tr (*"_Char"*) [Free (xstr, _)] =
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    58
        (case Syntax.explode_xstr xstr of
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    59
          [c] => mk_char c
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    60
        | _ => error ("Single character expected: " ^ xstr))
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    61
    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    62
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    63
  fun char_tr' (*"Char"*) [t1, t2] =
6395
5abd0d044adf xstr token class;
wenzelm
parents: 5121
diff changeset
    64
        Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
5121
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    65
    | char_tr' (*"Char"*) _ = raise Match;
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    66
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    67
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    68
  (* strings *)
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    69
7224
e41e64476f9b 'a list: Nil, Cons;
wenzelm
parents: 6395
diff changeset
    70
  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
e41e64476f9b 'a list: Nil, Cons;
wenzelm
parents: 6395
diff changeset
    71
    | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
5121
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    72
7224
e41e64476f9b 'a list: Nil, Cons;
wenzelm
parents: 6395
diff changeset
    73
  fun dest_string (Const ("Nil", _)) = []
e41e64476f9b 'a list: Nil, Cons;
wenzelm
parents: 6395
diff changeset
    74
    | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
5121
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    75
    | dest_string _ = raise Match;
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    76
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    77
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    78
  fun string_tr (*"_String"*) [Free (xstr, _)] =
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    79
        mk_string (map mk_char (Syntax.explode_xstr xstr))
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    80
    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    81
7224
e41e64476f9b 'a list: Nil, Cons;
wenzelm
parents: 6395
diff changeset
    82
  fun cons_tr' (*"Cons"*) [c, cs] =
5121
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    83
        Syntax.const "_String" $
6395
5abd0d044adf xstr token class;
wenzelm
parents: 5121
diff changeset
    84
          syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
7224
e41e64476f9b 'a list: Nil, Cons;
wenzelm
parents: 6395
diff changeset
    85
    | cons_tr' (*"Cons"*) ts = raise Match;
5121
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    86
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    87
in
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    88
  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
7224
e41e64476f9b 'a list: Nil, Cons;
wenzelm
parents: 6395
diff changeset
    89
  val print_translation = [("Char", char_tr'), ("Cons", cons_tr')];
5121
5c1f89ae8aef moved String theory to main HOL;
wenzelm
parents:
diff changeset
    90
end;