src/HOL/Tools/string_syntax.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 21775 8be8da44ee56
child 24712 64ed05609568
permissions -rw-r--r--
Some hacks for SPASS format
     1 (*  Title:      HOL/Tools/string_syntax.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Concrete syntax for hex chars and strings.
     6 *)
     7 
     8 signature STRING_SYNTAX =
     9 sig
    10   val setup: theory -> theory
    11 end;
    12 
    13 structure StringSyntax: STRING_SYNTAX =
    14 struct
    15 
    16 
    17 (* nibble *)
    18 
    19 val mk_nib =
    20   Syntax.Constant o unprefix "List.nibble." o
    21   fst o Term.dest_Const o HOLogic.mk_nibble;
    22 
    23 fun dest_nib (Syntax.Constant c) =
    24   HOLogic.dest_nibble (Const ("List.nibble." ^ c, dummyT))
    25     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 "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 "Char", c1, c2]) = dest_chr c1 c2
    44   | dest_char _ = raise Match;
    45 
    46 fun syntax_xstr cs =
    47   Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
    48 
    49 
    50 fun char_ast_tr [Syntax.Variable xstr] =
    51     (case Syntax.explode_xstr xstr of
    52       [c] => mk_char c
    53     | _ => error ("Single character expected: " ^ xstr))
    54   | char_ast_tr asts = raise AST ("char_ast_tr", asts);
    55 
    56 fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_xstr [dest_chr c1 c2]]
    57   | char_ast_tr' _ = raise Match;
    58 
    59 
    60 (* string *)
    61 
    62 fun mk_string [] = Syntax.Constant "Nil"
    63   | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
    64 
    65 fun string_ast_tr [Syntax.Variable xstr] =
    66     (case Syntax.explode_xstr xstr of
    67       [] => Syntax.Appl
    68         [Syntax.Constant Syntax.constrainC, Syntax.Constant "Nil", Syntax.Constant "string"]
    69     | cs => mk_string cs)
    70   | string_ast_tr asts = raise AST ("string_tr", asts);
    71 
    72 fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
    73         syntax_xstr (map dest_char (Syntax.unfold_ast "_args" args))]
    74   | list_ast_tr' ts = raise Match;
    75 
    76 
    77 (* theory setup *)
    78 
    79 val setup =
    80   Theory.add_trfuns
    81     ([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [],
    82       [("Char", char_ast_tr'), ("@list", list_ast_tr')]);
    83 
    84 end;