--- a/src/HOL/String.thy Sat Nov 03 01:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: HOL/String.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
- License: GPL (GNU GENERAL PUBLIC LICENSE)
-
-Hex chars and strings.
-*)
-
-theory String = List:
-
-datatype nibble =
- Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
- | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
-
-datatype char = Char nibble nibble
- -- "Note: canonical order of character encoding coincides with standard term ordering"
-
-types string = "char list"
-
-syntax
- "_Char" :: "xstr => char" ("CHR _")
- "_String" :: "xstr => string" ("_")
-
-parse_ast_translation {*
- let
- val constants = Syntax.Appl o map Syntax.Constant;
-
- fun mk_nib n = "Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10));
- fun mk_char c =
- if Symbol.is_ascii c andalso Symbol.is_printable c then
- constants ["Char", mk_nib (ord c div 16), mk_nib (ord c mod 16)]
- else error ("Printable ASCII character expected: " ^ quote c);
-
- fun mk_string [] = Syntax.Constant "Nil"
- | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
-
- fun char_ast_tr [Syntax.Variable xstr] =
- (case Syntax.explode_xstr xstr of
- [c] => mk_char c
- | _ => error ("Single character expected: " ^ xstr))
- | char_ast_tr asts = raise AST ("char_ast_tr", asts);
-
- fun string_ast_tr [Syntax.Variable xstr] =
- (case Syntax.explode_xstr xstr of
- [] => constants [Syntax.constrainC, "Nil", "string"]
- | cs => mk_string cs)
- | string_ast_tr asts = raise AST ("string_tr", asts);
- in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end;
-*}
-
-print_ast_translation {*
- let
- fun dest_nib (Syntax.Constant c) =
- (case explode c of
- ["N", "i", "b", "b", "l", "e", h] =>
- if "0" <= h andalso h <= "9" then ord h - ord "0"
- else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
- else raise Match
- | _ => raise Match)
- | dest_nib _ = raise Match;
-
- fun dest_chr c1 c2 =
- let val c = chr (dest_nib c1 * 16 + dest_nib c2)
- in if Symbol.is_printable c then c else raise Match end;
-
- fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
- | dest_char _ = raise Match;
-
- fun xstr cs = Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
-
- fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", xstr [dest_chr c1 c2]]
- | char_ast_tr' _ = raise Match;
-
- fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
- xstr (map dest_char (Syntax.unfold_ast "_args" args))]
- | list_ast_tr' ts = raise Match;
- in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
-*}
-
-end