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