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
     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   Ast.Constant o Lexicon.mark_const o
    20     fst o Term.dest_Const o HOLogic.mk_nibble;
    21 
    22 fun dest_nib (Ast.Constant s) =
    23   (case try Lexicon.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     Ast.Appl [Ast.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 = raw_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 (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
    44   | dest_char _ = raise Match;
    45 
    46 fun syntax_string cs =
    47   Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
    48     Ast.Variable (Lexicon.implode_str cs)];
    49 
    50 
    51 fun char_ast_tr [Ast.Variable str] =
    52       (case Lexicon.explode_str str of
    53         [c] => mk_char c
    54       | _ => error ("Single character expected: " ^ str))
    55   | char_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
    56       Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, char_ast_tr [ast1], ast2]
    57   | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
    58 
    59 fun char_ast_tr' [c1, c2] =
    60       Ast.Appl [Ast.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 [] = Ast.Constant @{const_syntax Nil}
    67   | mk_string (c :: cs) =
    68       Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
    69 
    70 fun string_ast_tr [Ast.Variable str] =
    71       (case Lexicon.explode_str str of
    72         [] =>
    73           Ast.Appl
    74             [Ast.Constant @{syntax_const "_constrain"},
    75               Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
    76       | cs => mk_string cs)
    77   | string_ast_tr [Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, ast1, ast2]] =
    78       Ast.Appl [Ast.Constant @{syntax_const "_constrain"}, string_ast_tr [ast1], ast2]
    79   | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
    80 
    81 fun list_ast_tr' [args] =
    82       Ast.Appl [Ast.Constant @{syntax_const "_String"},
    83         syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
    84   | list_ast_tr' ts = raise Match;
    85 
    86 
    87 (* theory setup *)
    88 
    89 val setup =
    90   Sign.add_trfuns
    91    ([(@{syntax_const "_Char"}, char_ast_tr), (@{syntax_const "_String"}, string_ast_tr)], [], [],
    92     [(@{const_syntax Char}, char_ast_tr'), (@{syntax_const "_list"}, list_ast_tr')]);
    93 
    94 end;