Tools/string_syntax.ML;
authorwenzelm
Sat Dec 23 22:50:19 2000 +0100 (2000-12-23)
changeset 10732d4fda7d05ce5
parent 10731 f44ab3108202
child 10733 59f82484e000
Tools/string_syntax.ML;
src/HOL/IsaMakefile
src/HOL/String.thy
src/HOL/Tools/string_syntax.ML
     1.1 --- a/src/HOL/IsaMakefile	Sat Dec 23 22:49:39 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Sat Dec 23 22:50:19 2000 +0100
     1.3 @@ -94,8 +94,8 @@
     1.4    Tools/datatype_package.ML Tools/datatype_prop.ML \
     1.5    Tools/datatype_rep_proofs.ML Tools/induct_attrib.ML Tools/induct_method.ML \
     1.6    Tools/inductive_package.ML Tools/meson.ML Tools/numeral_syntax.ML \
     1.7 -  Tools/primrec_package.ML Tools/recdef_package.ML \
     1.8 -  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
     1.9 +  Tools/primrec_package.ML Tools/recdef_package.ML Tools/record_package.ML \
    1.10 +  Tools/string_syntax.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
    1.11    Transitive_Closure.ML Transitive_Closure.thy Wellfounded_Recursion.ML \
    1.12    Wellfounded_Recursion.thy Wellfounded_Relations.ML \
    1.13    Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
     2.1 --- a/src/HOL/String.thy	Sat Dec 23 22:49:39 2000 +0100
     2.2 +++ b/src/HOL/String.thy	Sat Dec 23 22:50:19 2000 +0100
     2.3 @@ -1,90 +1,25 @@
     2.4  (*  Title:      HOL/String.thy
     2.5      ID:         $Id$
     2.6 +    Author:     Markus Wenzel, TU Muenchen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8  
     2.9  Hex chars and strings.
    2.10  *)
    2.11  
    2.12 -String = List +
    2.13 -
    2.14 -datatype
    2.15 -  nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
    2.16 -         | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
    2.17 +theory String = List
    2.18 +files "Tools/string_syntax.ML":
    2.19  
    2.20 -datatype
    2.21 -  char = Char nibble nibble
    2.22 +datatype nibble =
    2.23 +    H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07
    2.24 +  | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F
    2.25  
    2.26 -types
    2.27 -  string = char list
    2.28 +datatype char = Char nibble nibble
    2.29 +types string = "char list"
    2.30  
    2.31  syntax
    2.32 -  "_Char"       :: xstr => char       ("CHR _")
    2.33 -  "_String"     :: xstr => string     ("_")
    2.34 +  "_Char" :: "xstr => char"    ("CHR _")
    2.35 +  "_String" :: "xstr => string"    ("_")
    2.36 +
    2.37 +setup StringSyntax.setup
    2.38  
    2.39  end
    2.40 -
    2.41 -
    2.42 -ML
    2.43 -
    2.44 -local
    2.45 -
    2.46 -  (* chars *)
    2.47 -
    2.48 -  fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
    2.49 -
    2.50 -
    2.51 -  val zero = ord "0";
    2.52 -  val ten = ord "A" - 10;
    2.53 -
    2.54 -  fun mk_nib n =
    2.55 -    Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    2.56 -
    2.57 -  fun dest_nib (Const (c, _)) =
    2.58 -        (case explode c of
    2.59 -          ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    2.60 -        | _ => raise Match)
    2.61 -    | dest_nib _ = raise Match;
    2.62 -
    2.63 -  fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    2.64 -
    2.65 -
    2.66 -  fun mk_char c =
    2.67 -    Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    2.68 -
    2.69 -  fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    2.70 -    | dest_char _ = raise Match;
    2.71 -
    2.72 -
    2.73 -  fun char_tr (*"_Char"*) [Free (xstr, _)] =
    2.74 -        (case Syntax.explode_xstr xstr of
    2.75 -          [c] => mk_char c
    2.76 -        | _ => error ("Single character expected: " ^ xstr))
    2.77 -    | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    2.78 -
    2.79 -  fun char_tr' (*"Char"*) [t1, t2] =
    2.80 -        Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
    2.81 -    | char_tr' (*"Char"*) _ = raise Match;
    2.82 -
    2.83 -
    2.84 -  (* strings *)
    2.85 -
    2.86 -  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
    2.87 -    | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
    2.88 -
    2.89 -  fun dest_string (Const ("Nil", _)) = []
    2.90 -    | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
    2.91 -    | dest_string _ = raise Match;
    2.92 -
    2.93 -
    2.94 -  fun string_tr (*"_String"*) [Free (xstr, _)] =
    2.95 -        mk_string (map mk_char (Syntax.explode_xstr xstr))
    2.96 -    | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    2.97 -
    2.98 -  fun cons_tr' (*"Cons"*) [c, cs] =
    2.99 -        Syntax.const "_String" $
   2.100 -          syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
   2.101 -    | cons_tr' (*"Cons"*) ts = raise Match;
   2.102 -
   2.103 -in
   2.104 -  val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
   2.105 -  val print_translation = [("Char", char_tr'), ("Cons", cons_tr')];
   2.106 -end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/string_syntax.ML	Sat Dec 23 22:50:19 2000 +0100
     3.3 @@ -0,0 +1,84 @@
     3.4 +(*  Title:      HOL/Tools/string_syntax.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.8 +
     3.9 +Concrete syntax for hex chars and strings.  Assumes consts and syntax
    3.10 +of theory HOL/String.
    3.11 +*)
    3.12 +
    3.13 +signature STRING_SYNTAX =
    3.14 +sig
    3.15 +  val setup: (theory -> theory) list
    3.16 +end;
    3.17 +
    3.18 +structure StringSyntax: STRING_SYNTAX =
    3.19 +struct
    3.20 +
    3.21 +
    3.22 +(* chars *)
    3.23 +
    3.24 +fun syntax_xstr x = Syntax.const "_xstr" $ Syntax.free x;
    3.25 +
    3.26 +
    3.27 +val zero = ord "0";
    3.28 +val ten = ord "A" - 10;
    3.29 +
    3.30 +fun mk_nib n =
    3.31 +  Syntax.const ("H0" ^ chr (n + (if n <= 9 then zero else ten)));
    3.32 +
    3.33 +fun dest_nib (Const (c, _)) =
    3.34 +      (case explode c of
    3.35 +        ["H", "0", h] => ord h - (if h <= "9" then zero else ten)
    3.36 +      | _ => raise Match)
    3.37 +  | dest_nib _ = raise Match;
    3.38 +
    3.39 +fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2);
    3.40 +
    3.41 +
    3.42 +fun mk_char c =
    3.43 +  Syntax.const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16);
    3.44 +
    3.45 +fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2
    3.46 +  | dest_char _ = raise Match;
    3.47 +
    3.48 +
    3.49 +fun char_tr (*"_Char"*) [Free (xstr, _)] =
    3.50 +      (case Syntax.explode_xstr xstr of
    3.51 +        [c] => mk_char c
    3.52 +      | _ => error ("Single character expected: " ^ xstr))
    3.53 +  | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
    3.54 +
    3.55 +fun char_tr' (*"Char"*) [t1, t2] =
    3.56 +      Syntax.const "_Char" $ syntax_xstr (Syntax.implode_xstr [dest_nibs t1 t2])
    3.57 +  | char_tr' (*"Char"*) _ = raise Match;
    3.58 +
    3.59 +
    3.60 +(* strings *)
    3.61 +
    3.62 +fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
    3.63 +  | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
    3.64 +
    3.65 +fun dest_string (Const ("Nil", _)) = []
    3.66 +  | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
    3.67 +  | dest_string _ = raise Match;
    3.68 +
    3.69 +
    3.70 +fun string_tr (*"_String"*) [Free (xstr, _)] =
    3.71 +      mk_string (map mk_char (Syntax.explode_xstr xstr))
    3.72 +  | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
    3.73 +
    3.74 +fun cons_tr' (*"Cons"*) [c, cs] =
    3.75 +      Syntax.const "_String" $
    3.76 +        syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
    3.77 +  | cons_tr' (*"Cons"*) ts = raise Match;
    3.78 +
    3.79 +
    3.80 +(* theory setup *)
    3.81 +
    3.82 +val setup =
    3.83 +  [Theory.add_trfuns
    3.84 +    ([], [("_Char", char_tr), ("_String", string_tr)],
    3.85 +    [("Char", char_tr'), ("Cons", cons_tr')], [])];
    3.86 +
    3.87 +end;