src/HOL/String.thy
changeset 5121 5c1f89ae8aef
child 6395 5abd0d044adf
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/String.thy	Fri Jul 03 17:33:47 1998 +0200
     1.3 @@ -0,0 +1,87 @@
     1.4 +(*  Title:      HOL/String.thy
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +Hex chars and strings.
     1.8 +*)
     1.9 +
    1.10 +String = List +
    1.11 +
    1.12 +datatype
    1.13 +  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
    1.14 +         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
    1.15 +
    1.16 +datatype
    1.17 +  char = Char nibble nibble
    1.18 +
    1.19 +types
    1.20 +  string = char list
    1.21 +
    1.22 +syntax
    1.23 +  "_Char"       :: xstr => char       ("CHR _")
    1.24 +  "_String"     :: xstr => string     ("_")
    1.25 +
    1.26 +end
    1.27 +
    1.28 +
    1.29 +ML
    1.30 +
    1.31 +local
    1.32 +
    1.33 +  (* chars *)
    1.34 +
    1.35 +  val zero = ord "0";
    1.36 +  val ten = ord "A" - 10;
    1.37 +
    1.38 +  fun mk_nib n =
    1.39 +    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    1.40 +
    1.41 +  fun dest_nib (Const (c, _)) =
    1.42 +        (case explode c of
    1.43 +          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    1.44 +        | _ => raise Match)
    1.45 +    | dest_nib _ = raise Match;
    1.46 +
    1.47 +  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    1.48 +
    1.49 +
    1.50 +  fun mk_char c =
    1.51 +    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    1.52 +
    1.53 +  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    1.54 +    | dest_char _ = raise Match;
    1.55 +
    1.56 +
    1.57 +  fun char_tr (*"_Char"*) [Free (xstr, _)] =
    1.58 +        (case Syntax.explode_xstr xstr of
    1.59 +          [c] => mk_char c
    1.60 +        | _ => error ("Single character expected: " ^ xstr))
    1.61 +    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    1.62 +
    1.63 +  fun char_tr' (*"Char"*) [t1, t2] =
    1.64 +        Syntax.const "_Char" $ Syntax.free (Syntax.implode_xstr [dest_nibs t1 t2])
    1.65 +    | char_tr' (*"Char"*) _ = raise Match;
    1.66 +
    1.67 +
    1.68 +  (* strings *)
    1.69 +
    1.70 +  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
    1.71 +    | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts;
    1.72 +
    1.73 +  fun dest_string (Const ("[]", _)) = []
    1.74 +    | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
    1.75 +    | dest_string _ = raise Match;
    1.76 +
    1.77 +
    1.78 +  fun string_tr (*"_String"*) [Free (xstr, _)] =
    1.79 +        mk_string (map mk_char (Syntax.explode_xstr xstr))
    1.80 +    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    1.81 +
    1.82 +  fun cons_tr' (*"op #"*) [c, cs] =
    1.83 +        Syntax.const "_String" $
    1.84 +          Syntax.free (Syntax.implode_xstr (dest_char c :: dest_string cs))
    1.85 +    | cons_tr' (*"op #"*) ts = raise Match;
    1.86 +
    1.87 +in
    1.88 +  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
    1.89 +  val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
    1.90 +end;