src/HOL/Tools/string_syntax.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 46483 10a9c31a22b4
child 51160 599ff65b85e2
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
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
wenzelm@21759
    18
val mk_nib =
wenzelm@42290
    19
  Ast.Constant o Lexicon.mark_const o
wenzelm@35123
    20
    fst o Term.dest_Const o HOLogic.mk_nibble;
wenzelm@21759
    21
wenzelm@42224
    22
fun dest_nib (Ast.Constant s) =
wenzelm@42290
    23
  (case try Lexicon.unmark_const s of
wenzelm@35256
    24
    NONE => raise Match
wenzelm@35256
    25
  | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
wenzelm@21759
    26
wenzelm@21759
    27
wenzelm@21759
    28
(* char *)
wenzelm@21759
    29
wenzelm@21759
    30
fun mk_char s =
wenzelm@21759
    31
  if Symbol.is_ascii s then
wenzelm@42224
    32
    Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
wenzelm@21759
    33
  else error ("Non-ASCII symbol: " ^ quote s);
wenzelm@21759
    34
wenzelm@40627
    35
val specials = raw_explode "\\\"`'";
wenzelm@21759
    36
wenzelm@21759
    37
fun dest_chr c1 c2 =
wenzelm@21759
    38
  let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
wenzelm@21759
    39
    if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
wenzelm@21759
    40
    then c else raise Match
wenzelm@21759
    41
  end;
wenzelm@21759
    42
wenzelm@42224
    43
fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
wenzelm@21759
    44
  | dest_char _ = raise Match;
wenzelm@21759
    45
wenzelm@29317
    46
fun syntax_string cs =
wenzelm@42290
    47
  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
wenzelm@46483
    48
    Ast.Variable (Lexicon.implode_str cs)];
wenzelm@21759
    49
wenzelm@21759
    50
wenzelm@46483
    51
fun char_ast_tr [Ast.Variable str] =
wenzelm@46483
    52
      (case Lexicon.explode_str str of
wenzelm@42224
    53
        [c] => mk_char c
wenzelm@46483
    54
      | _ => error ("Single character expected: " ^ str))
wenzelm@45490
    55
  | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
wenzelm@45490
    56
      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
wenzelm@42224
    57
  | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
wenzelm@21759
    58
wenzelm@35115
    59
fun char_ast_tr' [c1, c2] =
wenzelm@42224
    60
      Ast.Appl [Ast.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@42224
    66
fun mk_string [] = Ast.Constant @{const_syntax Nil}
wenzelm@35115
    67
  | mk_string (c :: cs) =
wenzelm@42224
    68
      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
wenzelm@21759
    69
wenzelm@46483
    70
fun string_ast_tr [Ast.Variable str] =
wenzelm@46483
    71
      (case Lexicon.explode_str str of
wenzelm@42224
    72
        [] =>
wenzelm@42224
    73
          Ast.Appl
wenzelm@42248
    74
            [Ast.Constant @{syntax_const "_constrain"},
wenzelm@42224
    75
              Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
wenzelm@42224
    76
      | cs => mk_string cs)
wenzelm@45490
    77
  | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
wenzelm@45490
    78
      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
wenzelm@42224
    79
  | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
wenzelm@21759
    80
wenzelm@35115
    81
fun list_ast_tr' [args] =
wenzelm@42224
    82
      Ast.Appl [Ast.Constant @{syntax_const "_String"},
wenzelm@42224
    83
        syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
wenzelm@21759
    84
  | list_ast_tr' ts = raise Match;
wenzelm@21759
    85
wenzelm@21759
    86
wenzelm@21759
    87
(* theory setup *)
wenzelm@21759
    88
wenzelm@21759
    89
val setup =
wenzelm@24712
    90
  Sign.add_trfuns
wenzelm@35115
    91
   ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
wenzelm@35115
    92
    [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
wenzelm@21759
    93
wenzelm@21759
    94
end;