1.1 --- a/src/HOL/String.thy	Sat Dec 23 22:49:39 2000 +0100
     1.2 +++ b/src/HOL/String.thy	Sat Dec 23 22:50:19 2000 +0100
     1.3 @@ -1,90 +1,25 @@
     1.4  (*  Title:      HOL/String.thy
     1.5      ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8  
     1.9  Hex chars and strings.
    1.10  *)
    1.11  
    1.12 -String = List +
    1.13 +theory String = List
    1.14 +files "Tools/string_syntax.ML":
    1.15  
    1.16 -datatype
    1.17 -  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
    1.18 -         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
    1.19 +datatype nibble =
    1.20 +    H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
    1.21 +  | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
    1.22  
    1.23 -datatype
    1.24 -  char = Char nibble nibble
    1.25 -
    1.26 -types
    1.27 -  string = char list
    1.28 +datatype char = Char nibble nibble
    1.29 +types string = "char list"
    1.30  
    1.31  syntax
    1.32 -  "_Char"       :: xstr => char       ("CHR _")
    1.33 -  "_String"     :: xstr => string     ("_")
    1.34 +  "_Char" :: "xstr => char"    ("CHR _")
    1.35 +  "_String" :: "xstr => string"    ("_")
    1.36 +
    1.37 +setup StringSyntax.setup
    1.38  
    1.39  end
    1.40 -
    1.41 -
    1.42 -ML
    1.43 -
    1.44 -local
    1.45 -
    1.46 -  (* chars *)
    1.47 -
    1.48 -  fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
    1.49 -
    1.50 -
    1.51 -  val zero = ord "0";
    1.52 -  val ten = ord "A" - 10;
    1.53 -
    1.54 -  fun mk_nib n =
    1.55 -    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    1.56 -
    1.57 -  fun dest_nib (Const (c, _)) =
    1.58 -        (case explode c of
    1.59 -          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    1.60 -        | _ => raise Match)
    1.61 -    | dest_nib _ = raise Match;
    1.62 -
    1.63 -  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    1.64 -
    1.65 -
    1.66 -  fun mk_char c =
    1.67 -    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    1.68 -
    1.69 -  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    1.70 -    | dest_char _ = raise Match;
    1.71 -
    1.72 -
    1.73 -  fun char_tr (*"_Char"*) [Free (xstr, _)] =
    1.74 -        (case Syntax.explode_xstr xstr of
    1.75 -          [c] => mk_char c
    1.76 -        | _ => error ("Single character expected: " ^ xstr))
    1.77 -    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    1.78 -
    1.79 -  fun char_tr' (*"Char"*) [t1, t2] =
    1.80 -        Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
    1.81 -    | char_tr' (*"Char"*) _ = raise Match;
    1.82 -
    1.83 -
    1.84 -  (* strings *)
    1.85 -
    1.86 -  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
    1.87 -    | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
    1.88 -
    1.89 -  fun dest_string (Const ("Nil", _)) = []
    1.90 -    | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
    1.91 -    | dest_string _ = raise Match;
    1.92 -
    1.93 -
    1.94 -  fun string_tr (*"_String"*) [Free (xstr, _)] =
    1.95 -        mk_string (map mk_char (Syntax.explode_xstr xstr))
    1.96 -    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    1.97 -
    1.98 -  fun cons_tr' (*"Cons"*) [c, cs] =
    1.99 -        Syntax.const "_String" $
   1.100 -          syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
   1.101 -    | cons_tr' (*"Cons"*) ts = raise Match;
   1.102 -
   1.103 -in
   1.104 -  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
   1.105 -  val print_translation = [("Char", char_tr'), ("Cons", cons_tr')];
   1.106 -end;