src/HOL/Tools/string_syntax.ML
author boehmes
Sat Mar 27 02:10:00 2010 +0100 (2010-03-27)
changeset 35983 27e2fa7d4ce7
parent 35363 09489d8ffece
child 40627 becf5d5187cc
permissions -rw-r--r--
slightly more general simproc (avoids errors of linarith)
     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 String_Syntax: STRING_SYNTAX =
    13 struct
    14 
    15 
    16 (* nibble *)
    17 
    18 val mk_nib =
    19   Syntax.Constant o Syntax.mark_const o
    20     fst o Term.dest_Const o HOLogic.mk_nibble;
    21 
    22 fun dest_nib (Syntax.Constant s) =
    23   (case try Syntax.unmark_const s of
    24     NONE => raise Match
    25   | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
    26 
    27 
    28 (* char *)
    29 
    30 fun mk_char s =
    31   if Symbol.is_ascii s then
    32     Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
    33   else error ("Non-ASCII symbol: " ^ quote s);
    34 
    35 val specials = explode "\\\"`'";
    36 
    37 fun dest_chr c1 c2 =
    38   let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
    39     if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
    40     then c else raise Match
    41   end;
    42 
    43 fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
    44   | dest_char _ = raise Match;
    45 
    46 fun syntax_string cs =
    47   Syntax.Appl
    48     [Syntax.Constant @{syntax_const "_inner_string"},
    49       Syntax.Variable (Syntax.implode_xstr cs)];
    50 
    51 
    52 fun char_ast_tr [Syntax.Variable xstr] =
    53     (case Syntax.explode_xstr xstr of
    54       [c] => mk_char c
    55     | _ => error ("Single character expected: " ^ xstr))
    56   | char_ast_tr asts = raise AST ("char_ast_tr", asts);
    57 
    58 fun char_ast_tr' [c1, c2] =
    59       Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
    60   | char_ast_tr' _ = raise Match;
    61 
    62 
    63 (* string *)
    64 
    65 fun mk_string [] = Syntax.Constant @{const_syntax Nil}
    66   | mk_string (c :: cs) =
    67       Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
    68 
    69 fun string_ast_tr [Syntax.Variable xstr] =
    70     (case Syntax.explode_xstr xstr of
    71       [] =>
    72         Syntax.Appl
    73           [Syntax.Constant Syntax.constrainC,
    74             Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}]
    75     | cs => mk_string cs)
    76   | string_ast_tr asts = raise AST ("string_tr", asts);
    77 
    78 fun list_ast_tr' [args] =
    79       Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
    80         syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
    81   | list_ast_tr' ts = raise Match;
    82 
    83 
    84 (* theory setup *)
    85 
    86 val setup =
    87   Sign.add_trfuns
    88    ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
    89     [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
    90 
    91 end;