src/HOL/Tools/string_syntax.ML
author wenzelm
Sat Feb 13 23:24:57 2010 +0100 (2010-02-13)
changeset 35123 e286d5df187a
parent 35115 446c5063e4fd
child 35256 b73ae1a8fe7e
permissions -rw-r--r--
modernized structures;
wenzelm@21759
     1
(*  Title:      HOL/Tools/string_syntax.ML
wenzelm@21759
     2
    Author:     Makarius
wenzelm@21759
     3
wenzelm@21759
     4
Concrete syntax for hex chars and strings.
wenzelm@21759
     5
*)
wenzelm@21759
     6
wenzelm@21759
     7
signature STRING_SYNTAX =
wenzelm@21759
     8
sig
wenzelm@21759
     9
  val setup: theory -> theory
wenzelm@21759
    10
end;
wenzelm@21759
    11
wenzelm@35123
    12
structure String_Syntax: STRING_SYNTAX =
wenzelm@21759
    13
struct
wenzelm@21759
    14
wenzelm@21759
    15
wenzelm@21759
    16
(* nibble *)
wenzelm@21759
    17
haftmann@31048
    18
val nib_prefix = "String.nibble.";
haftmann@31048
    19
wenzelm@21759
    20
val mk_nib =
haftmann@31048
    21
  Syntax.Constant o unprefix nib_prefix o
wenzelm@35123
    22
    fst o Term.dest_Const o HOLogic.mk_nibble;
wenzelm@21759
    23
wenzelm@21759
    24
fun dest_nib (Syntax.Constant c) =
haftmann@31048
    25
  HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))
wenzelm@21759
    26
    handle TERM _ => raise Match;
wenzelm@21759
    27
wenzelm@21759
    28
wenzelm@21759
    29
(* char *)
wenzelm@21759
    30
wenzelm@21759
    31
fun mk_char s =
wenzelm@21759
    32
  if Symbol.is_ascii s then
wenzelm@35115
    33
    Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
wenzelm@21759
    34
  else error ("Non-ASCII symbol: " ^ quote s);
wenzelm@21759
    35
wenzelm@21775
    36
val specials = explode "\\\"`'";
wenzelm@21759
    37
wenzelm@21759
    38
fun dest_chr c1 c2 =
wenzelm@21759
    39
  let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
wenzelm@21759
    40
    if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
wenzelm@21759
    41
    then c else raise Match
wenzelm@21759
    42
  end;
wenzelm@21759
    43
wenzelm@35115
    44
fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
wenzelm@21759
    45
  | dest_char _ = raise Match;
wenzelm@21759
    46
wenzelm@29317
    47
fun syntax_string cs =
wenzelm@35115
    48
  Syntax.Appl
wenzelm@35115
    49
    [Syntax.Constant @{syntax_const "_inner_string"},
wenzelm@35115
    50
      Syntax.Variable (Syntax.implode_xstr cs)];
wenzelm@21759
    51
wenzelm@21759
    52
wenzelm@21759
    53
fun char_ast_tr [Syntax.Variable xstr] =
wenzelm@21759
    54
    (case Syntax.explode_xstr xstr of
wenzelm@21759
    55
      [c] => mk_char c
wenzelm@21759
    56
    | _ => error ("Single character expected: " ^ xstr))
wenzelm@21759
    57
  | char_ast_tr asts = raise AST ("char_ast_tr", asts);
wenzelm@21759
    58
wenzelm@35115
    59
fun char_ast_tr' [c1, c2] =
wenzelm@35115
    60
      Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
wenzelm@21759
    61
  | char_ast_tr' _ = raise Match;
wenzelm@21759
    62
wenzelm@21759
    63
wenzelm@21759
    64
(* string *)
wenzelm@21759
    65
wenzelm@35115
    66
fun mk_string [] = Syntax.Constant @{const_syntax Nil}
wenzelm@35115
    67
  | mk_string (c :: cs) =
wenzelm@35115
    68
      Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
wenzelm@21759
    69
wenzelm@21759
    70
fun string_ast_tr [Syntax.Variable xstr] =
wenzelm@21759
    71
    (case Syntax.explode_xstr xstr of
wenzelm@35115
    72
      [] =>
wenzelm@35115
    73
        Syntax.Appl
wenzelm@35115
    74
          [Syntax.Constant Syntax.constrainC,
wenzelm@35115
    75
            Syntax.Constant @{const_syntax Nil}, Syntax.Constant "string"]  (* FIXME @{type_syntax} *)
wenzelm@21759
    76
    | cs => mk_string cs)
wenzelm@21759
    77
  | string_ast_tr asts = raise AST ("string_tr", asts);
wenzelm@21759
    78
wenzelm@35115
    79
fun list_ast_tr' [args] =
wenzelm@35115
    80
      Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
wenzelm@35115
    81
        syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
wenzelm@21759
    82
  | list_ast_tr' ts = raise Match;
wenzelm@21759
    83
wenzelm@21759
    84
wenzelm@21759
    85
(* theory setup *)
wenzelm@21759
    86
wenzelm@21759
    87
val setup =
wenzelm@24712
    88
  Sign.add_trfuns
wenzelm@35115
    89
   ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
wenzelm@35115
    90
    [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
wenzelm@21759
    91
wenzelm@21759
    92
end;