src/HOL/Tools/string_syntax.ML
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 55108 0b7a0c1fdf7e
child 58822 90a5e981af3e
permissions -rw-r--r--
specialized specification: avoid trivial instances
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@55015
    31
  let
wenzelm@55015
    32
    val c =
wenzelm@55015
    33
      if Symbol.is_ascii s then ord s
wenzelm@55015
    34
      else if s = "\<newline>" then 10
wenzelm@55015
    35
      else error ("Bad character: " ^ quote s);
wenzelm@55015
    36
  in Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (c div 16), mk_nib (c mod 16)] end;
wenzelm@21759
    37
wenzelm@40627
    38
val specials = raw_explode "\\\"`'";
wenzelm@21759
    39
wenzelm@21759
    40
fun dest_chr c1 c2 =
wenzelm@55108
    41
  let val s = chr (dest_nib c1 * 16 + dest_nib c2) in
wenzelm@55108
    42
    if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
wenzelm@55108
    43
    then s
wenzelm@55108
    44
    else if s = "\n" then "\<newline>"
wenzelm@55015
    45
    else raise Match
wenzelm@21759
    46
  end;
wenzelm@21759
    47
wenzelm@42224
    48
fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
wenzelm@21759
    49
  | dest_char _ = raise Match;
wenzelm@21759
    50
wenzelm@55108
    51
fun syntax_string ss =
wenzelm@42290
    52
  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
wenzelm@55108
    53
    Ast.Variable (Lexicon.implode_str ss)];
wenzelm@21759
    54
wenzelm@21759
    55
wenzelm@46483
    56
fun char_ast_tr [Ast.Variable str] =
wenzelm@55108
    57
      (case Lexicon.explode_str (str, Position.none) of
wenzelm@55108
    58
        [(s, _)] => mk_char s
wenzelm@46483
    59
      | _ => error ("Single character expected: " ^ str))
wenzelm@45490
    60
  | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
wenzelm@45490
    61
      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
wenzelm@42224
    62
  | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
wenzelm@21759
    63
wenzelm@35115
    64
fun char_ast_tr' [c1, c2] =
wenzelm@42224
    65
      Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
wenzelm@21759
    66
  | char_ast_tr' _ = raise Match;
wenzelm@21759
    67
wenzelm@21759
    68
wenzelm@21759
    69
(* string *)
wenzelm@21759
    70
wenzelm@42224
    71
fun mk_string [] = Ast.Constant @{const_syntax Nil}
wenzelm@55108
    72
  | mk_string (s :: ss) =
wenzelm@55108
    73
      Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char s, mk_string ss];
wenzelm@21759
    74
wenzelm@46483
    75
fun string_ast_tr [Ast.Variable str] =
wenzelm@55108
    76
      (case Lexicon.explode_str (str, Position.none) of
wenzelm@42224
    77
        [] =>
wenzelm@42224
    78
          Ast.Appl
wenzelm@42248
    79
            [Ast.Constant @{syntax_const "_constrain"},
wenzelm@42224
    80
              Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
wenzelm@55108
    81
      | ss => mk_string (map Symbol_Pos.symbol ss))
wenzelm@45490
    82
  | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
wenzelm@45490
    83
      Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
wenzelm@42224
    84
  | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
wenzelm@21759
    85
wenzelm@35115
    86
fun list_ast_tr' [args] =
wenzelm@42224
    87
      Ast.Appl [Ast.Constant @{syntax_const "_String"},
wenzelm@42224
    88
        syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
haftmann@51160
    89
  | list_ast_tr' _ = raise Match;
wenzelm@21759
    90
wenzelm@21759
    91
wenzelm@21759
    92
(* theory setup *)
wenzelm@21759
    93
wenzelm@21759
    94
val setup =
wenzelm@52143
    95
  Sign.parse_ast_translation
wenzelm@52143
    96
   [(@{syntax_const "_Char"}, K char_ast_tr),
wenzelm@52143
    97
    (@{syntax_const "_String"}, K string_ast_tr)] #>
wenzelm@52143
    98
  Sign.print_ast_translation
wenzelm@52143
    99
   [(@{const_syntax Char}, K char_ast_tr'),
wenzelm@52143
   100
    (@{syntax_const "_list"}, K list_ast_tr')];
wenzelm@21759
   101
wenzelm@21759
   102
end;