src/HOL/Tools/string_syntax.ML
author bulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40905 647142607448
parent 40627 becf5d5187cc
child 42224 578a51fae383
permissions -rw-r--r--
only handle TimeOut exception if used interactively
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/string_syntax.ML
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     3
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     4
Concrete syntax for hex chars and strings.
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     5
*)
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     6
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     7
signature STRING_SYNTAX =
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     8
sig
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
     9
  val setup: theory -> theory
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    10
end;
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    11
35123
e286d5df187a modernized structures;
wenzelm
parents: 35115
diff changeset
    12
structure String_Syntax: STRING_SYNTAX =
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    13
struct
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    14
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    15
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    16
(* nibble *)
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    17
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    18
val mk_nib =
35262
9ea4445d2ccf slightly more abstract syntax mark/unmark operations;
wenzelm
parents: 35256
diff changeset
    19
  Syntax.Constant o Syntax.mark_const o
35123
e286d5df187a modernized structures;
wenzelm
parents: 35115
diff changeset
    20
    fst o Term.dest_Const o HOLogic.mk_nibble;
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    21
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35123
diff changeset
    22
fun dest_nib (Syntax.Constant s) =
35262
9ea4445d2ccf slightly more abstract syntax mark/unmark operations;
wenzelm
parents: 35256
diff changeset
    23
  (case try Syntax.unmark_const s of
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35123
diff changeset
    24
    NONE => raise Match
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35123
diff changeset
    25
  | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    26
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    27
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    28
(* char *)
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    29
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    30
fun mk_char s =
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    31
  if Symbol.is_ascii s then
35115
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    32
    Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    33
  else error ("Non-ASCII symbol: " ^ quote s);
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    34
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 35363
diff changeset
    35
val specials = raw_explode "\\\"`'";
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    36
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    37
fun dest_chr c1 c2 =
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    38
  let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    39
    if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    40
    then c else raise Match
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    41
  end;
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    42
35115
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    43
fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    44
  | dest_char _ = raise Match;
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    45
29317
9faf1dfb4e7c renamed token markup "_xstr" to "_inner_string";
wenzelm
parents: 24712
diff changeset
    46
fun syntax_string cs =
35115
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    47
  Syntax.Appl
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    48
    [Syntax.Constant @{syntax_const "_inner_string"},
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    49
      Syntax.Variable (Syntax.implode_xstr cs)];
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    50
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    51
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    52
fun char_ast_tr [Syntax.Variable xstr] =
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    53
    (case Syntax.explode_xstr xstr of
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    54
      [c] => mk_char c
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    55
    | _ => error ("Single character expected: " ^ xstr))
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    56
  | char_ast_tr asts = raise AST ("char_ast_tr", asts);
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    57
35115
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    58
fun char_ast_tr' [c1, c2] =
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    59
      Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    60
  | char_ast_tr' _ = raise Match;
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    61
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    62
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    63
(* string *)
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    64
35115
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    65
fun mk_string [] = Syntax.Constant @{const_syntax Nil}
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    66
  | mk_string (c :: cs) =
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    67
      Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    68
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    69
fun string_ast_tr [Syntax.Variable xstr] =
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    70
    (case Syntax.explode_xstr xstr of
35115
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    71
      [] =>
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    72
        Syntax.Appl
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    73
          [Syntax.Constant Syntax.constrainC,
35363
09489d8ffece explicit @{type_syntax} markup;
wenzelm
parents: 35262
diff changeset
    74
            Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}]
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    75
    | cs => mk_string cs)
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    76
  | string_ast_tr asts = raise AST ("string_tr", asts);
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    77
35115
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    78
fun list_ast_tr' [args] =
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    79
      Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    80
        syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    81
  | list_ast_tr' ts = raise Match;
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    82
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    83
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    84
(* theory setup *)
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    85
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    86
val setup =
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 21775
diff changeset
    87
  Sign.add_trfuns
35115
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    88
   ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
446c5063e4fd modernized translations;
wenzelm
parents: 31048
diff changeset
    89
    [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
21759
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    90
f4b20360751f Concrete syntax for hex chars and strings.
wenzelm
parents:
diff changeset
    91
end;