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
wenzelm@21759
     1
(*  Title:      HOL/Tools/string_syntax.ML
wenzelm@21759
     2
    ID:         $Id$
wenzelm@21759
     3
    Author:     Makarius
wenzelm@21759
     4
wenzelm@21759
     5
Concrete syntax for hex chars and strings.
wenzelm@21759
     6
*)
wenzelm@21759
     7
wenzelm@21759
     8
signature STRING_SYNTAX =
wenzelm@21759
     9
sig
wenzelm@21759
    10
  val setup: theory -> theory
wenzelm@21759
    11
end;
wenzelm@21759
    12
wenzelm@21759
    13
structure StringSyntax: STRING_SYNTAX =
wenzelm@21759
    14
struct
wenzelm@21759
    15
wenzelm@21759
    16
wenzelm@21759
    17
(* nibble *)
wenzelm@21759
    18
wenzelm@21759
    19
val mk_nib =
wenzelm@21759
    20
  Syntax.Constant o unprefix "List.nibble." o
wenzelm@21759
    21
  fst o Term.dest_Const o HOLogic.mk_nibble;
wenzelm@21759
    22
wenzelm@21759
    23
fun dest_nib (Syntax.Constant c) =
wenzelm@21759
    24
  HOLogic.dest_nibble (Const ("List.nibble." ^ c, dummyT))
wenzelm@21759
    25
    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@21759
    31
  if Symbol.is_ascii s then
wenzelm@21759
    32
    Syntax.Appl [Syntax.Constant "Char", mk_nib (ord s div 16), mk_nib (ord s mod 16)]
wenzelm@21759
    33
  else error ("Non-ASCII symbol: " ^ quote s);
wenzelm@21759
    34
wenzelm@21775
    35
val specials = explode "\\\"`'";
wenzelm@21759
    36
wenzelm@21759
    37
fun dest_chr c1 c2 =
wenzelm@21759
    38
  let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
wenzelm@21759
    39
    if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
wenzelm@21759
    40
    then c else raise Match
wenzelm@21759
    41
  end;
wenzelm@21759
    42
wenzelm@21759
    43
fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
wenzelm@21759
    44
  | dest_char _ = raise Match;
wenzelm@21759
    45
wenzelm@21759
    46
fun syntax_xstr cs =
wenzelm@21759
    47
  Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
wenzelm@21759
    48
wenzelm@21759
    49
wenzelm@21759
    50
fun char_ast_tr [Syntax.Variable xstr] =
wenzelm@21759
    51
    (case Syntax.explode_xstr xstr of
wenzelm@21759
    52
      [c] => mk_char c
wenzelm@21759
    53
    | _ => error ("Single character expected: " ^ xstr))
wenzelm@21759
    54
  | char_ast_tr asts = raise AST ("char_ast_tr", asts);
wenzelm@21759
    55
wenzelm@21759
    56
fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_xstr [dest_chr c1 c2]]
wenzelm@21759
    57
  | char_ast_tr' _ = raise Match;
wenzelm@21759
    58
wenzelm@21759
    59
wenzelm@21759
    60
(* string *)
wenzelm@21759
    61
wenzelm@21759
    62
fun mk_string [] = Syntax.Constant "Nil"
wenzelm@21759
    63
  | mk_string (c :: cs) = Syntax.Appl [Syntax.Constant "Cons", mk_char c, mk_string cs];
wenzelm@21759
    64
wenzelm@21759
    65
fun string_ast_tr [Syntax.Variable xstr] =
wenzelm@21759
    66
    (case Syntax.explode_xstr xstr of
wenzelm@21759
    67
      [] => Syntax.Appl
wenzelm@21759
    68
        [Syntax.Constant Syntax.constrainC, Syntax.Constant "Nil", Syntax.Constant "string"]
wenzelm@21759
    69
    | cs => mk_string cs)
wenzelm@21759
    70
  | string_ast_tr asts = raise AST ("string_tr", asts);
wenzelm@21759
    71
wenzelm@21759
    72
fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
wenzelm@21759
    73
        syntax_xstr (map dest_char (Syntax.unfold_ast "_args" args))]
wenzelm@21759
    74
  | list_ast_tr' ts = raise Match;
wenzelm@21759
    75
wenzelm@21759
    76
wenzelm@21759
    77
(* theory setup *)
wenzelm@21759
    78
wenzelm@21759
    79
val setup =
wenzelm@21759
    80
  Theory.add_trfuns
wenzelm@21759
    81
    ([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [],
wenzelm@21759
    82
      [("Char", char_ast_tr'), ("@list", list_ast_tr')]);
wenzelm@21759
    83
wenzelm@21759
    84
end;