src/HOL/Tools/SMT/smtlib.ML
author blanchet
Thu Aug 28 00:40:38 2014 +0200 (2014-08-28)
changeset 58061 3d060f43accb
parent 57704 src/HOL/Tools/SMT2/smtlib2.ML@c0da3fc313e3
child 61877 276ad4354069
permissions -rw-r--r--
renamed new SMT module from 'SMT2' to 'SMT'
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/smtlib.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Parsing and generating SMT-LIB 2.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
signature SMTLIB =
blanchet@56078
     8
sig
blanchet@56078
     9
  exception PARSE of int * string
blanchet@56078
    10
  datatype tree = 
blanchet@56078
    11
    Num of int |
blanchet@56078
    12
    Dec of int * int |
blanchet@56078
    13
    Str of string |
blanchet@56078
    14
    Sym of string |
blanchet@56078
    15
    Key of string |
blanchet@56078
    16
    S of tree list
blanchet@56078
    17
  val parse: string list -> tree
blanchet@56078
    18
  val pretty_tree: tree -> Pretty.T
blanchet@56078
    19
  val str_of: tree -> string
blanchet@57229
    20
end;
blanchet@56078
    21
blanchet@58061
    22
structure SMTLIB: SMTLIB =
blanchet@56078
    23
struct
blanchet@56078
    24
blanchet@56078
    25
(* data structures *)
blanchet@56078
    26
blanchet@56078
    27
exception PARSE of int * string
blanchet@56078
    28
blanchet@56078
    29
datatype tree = 
blanchet@56078
    30
  Num of int |
blanchet@56078
    31
  Dec of int * int |
blanchet@56078
    32
  Str of string |
blanchet@56078
    33
  Sym of string |
blanchet@56078
    34
  Key of string |
blanchet@56078
    35
  S of tree list
blanchet@56078
    36
blanchet@56078
    37
datatype unfinished = None | String of string | Symbol of string
blanchet@56078
    38
blanchet@56078
    39
blanchet@56078
    40
(* utilities *)
blanchet@56078
    41
blanchet@56078
    42
fun read_raw pred l cs =
blanchet@56078
    43
  (case take_prefix pred cs of
blanchet@56078
    44
    ([], []) => raise PARSE (l, "empty token")
blanchet@56078
    45
  | ([], c :: _) => raise PARSE (l, "unexpected character " ^ quote c)
blanchet@56078
    46
  | x => x)
blanchet@56078
    47
blanchet@56078
    48
blanchet@56078
    49
(* numerals and decimals *)
blanchet@56078
    50
blanchet@56078
    51
fun int_of cs = fst (read_int cs)
blanchet@56078
    52
blanchet@56078
    53
fun read_num l cs =
blanchet@56078
    54
  (case read_raw Symbol.is_ascii_digit l cs of
blanchet@56078
    55
    (cs1, "." :: cs') =>
blanchet@56078
    56
      let val (cs2, cs'') = read_raw Symbol.is_ascii_digit l cs'
blanchet@56078
    57
      in (Dec (int_of cs1, int_of cs2), cs'') end
blanchet@56078
    58
  | (cs1, cs2) => (Num (int_of cs1), cs2))
blanchet@56078
    59
blanchet@56078
    60
blanchet@56078
    61
(* binary numbers *)
blanchet@56078
    62
blanchet@56078
    63
fun is_bin c = (c = "0" orelse c = "1")
blanchet@56078
    64
blanchet@56078
    65
fun read_bin l cs = read_raw is_bin l cs |>> Num o fst o read_radix_int 2
blanchet@56078
    66
blanchet@56078
    67
blanchet@56078
    68
(* hex numbers *)
blanchet@56078
    69
blanchet@56078
    70
val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF")
blanchet@56078
    71
blanchet@56078
    72
fun within c1 c2 c = (ord c1 <= ord c andalso ord c <= ord c2)
blanchet@56078
    73
blanchet@56078
    74
fun unhex i [] = i
blanchet@56078
    75
  | unhex i (c :: cs) =
blanchet@56078
    76
      if within "0" "9" c then unhex (i * 16 + (ord c - ord "0")) cs
blanchet@56078
    77
      else if within "a" "f" c then unhex (i * 16 + (ord c - ord "a" + 10)) cs
blanchet@56078
    78
      else if within "A" "F" c then unhex (i * 16 + (ord c - ord "A" + 10)) cs
blanchet@56078
    79
      else raise Fail ("bad hex character " ^ quote c)
blanchet@56078
    80
blanchet@56078
    81
fun read_hex l cs = read_raw is_hex l cs |>> Num o unhex 0
blanchet@56078
    82
blanchet@56078
    83
blanchet@56078
    84
(* symbols *)
blanchet@56078
    85
blanchet@56078
    86
val symbol_chars = raw_explode "~!@$%^&*_+=<>.?/-" 
blanchet@56078
    87
blanchet@56078
    88
fun is_sym c =
blanchet@56078
    89
  Symbol.is_ascii_letter c orelse
blanchet@56078
    90
  Symbol.is_ascii_digit c orelse
blanchet@56078
    91
  member (op =) symbol_chars c
blanchet@56078
    92
blanchet@56078
    93
fun read_sym f l cs = read_raw is_sym l cs |>> f o implode
blanchet@56078
    94
blanchet@56078
    95
blanchet@56078
    96
(* quoted tokens *)
blanchet@56078
    97
blanchet@56078
    98
fun read_quoted stop (escape, replacement) cs =
blanchet@56078
    99
  let
blanchet@56078
   100
    fun read _ [] = NONE
blanchet@56078
   101
      | read rs (cs as (c :: cs')) =
blanchet@56078
   102
          if is_prefix (op =) stop cs then
blanchet@56078
   103
            SOME (implode (rev rs), drop (length stop) cs)
blanchet@56078
   104
          else if not (null escape) andalso is_prefix (op =) escape cs then
blanchet@56078
   105
            read (replacement :: rs) (drop (length escape) cs)
blanchet@56078
   106
          else read (c :: rs) cs'
blanchet@56078
   107
  in read [] cs end
blanchet@56078
   108
blanchet@56078
   109
fun read_string cs = read_quoted ["\\", "\""] (["\\", "\\"], "\\") cs
blanchet@56078
   110
fun read_symbol cs = read_quoted ["|"] ([], "") cs
blanchet@56078
   111
blanchet@56078
   112
blanchet@56078
   113
(* core parser *)
blanchet@56078
   114
blanchet@56078
   115
fun read _ [] rest tss = (rest, tss)
blanchet@56078
   116
  | read l ("(" :: cs) None tss = read l cs None ([] :: tss)
blanchet@56078
   117
  | read l (")" :: cs) None (ts1 :: ts2 :: tss) =
blanchet@56078
   118
      read l cs None ((S (rev ts1) :: ts2) :: tss)
blanchet@56078
   119
  | read l ("#" :: "x" :: cs) None (ts :: tss) =
blanchet@56078
   120
      token read_hex l cs ts tss
fleury@57704
   121
  | read l ("#" :: "b" :: cs) None (ts :: tss) =
blanchet@56078
   122
      token read_bin l cs ts tss
blanchet@56078
   123
  | read l (":" :: cs) None (ts :: tss) =
blanchet@56078
   124
      token (read_sym Key) l cs ts tss
blanchet@56078
   125
  | read l ("\"" :: cs) None (ts :: tss) =
blanchet@56078
   126
      quoted read_string String Str l "" cs ts tss
blanchet@56078
   127
  | read l ("|" :: cs) None (ts :: tss) =
blanchet@56078
   128
      quoted read_symbol Symbol Sym l "" cs ts tss
blanchet@56078
   129
  | read l ((c as "!") :: cs) None (ts :: tss) =
blanchet@56078
   130
      token (fn _ => pair (Sym c)) l cs ts tss
blanchet@56078
   131
  | read l (c :: cs) None (ts :: tss) =
blanchet@56078
   132
      if Symbol.is_ascii_blank c then read l cs None (ts :: tss)
blanchet@56078
   133
      else if Symbol.is_digit c then token read_num l (c :: cs) ts tss
blanchet@56078
   134
      else token (read_sym Sym) l (c :: cs) ts tss
blanchet@56078
   135
  | read l cs (String s) (ts :: tss) =
blanchet@56078
   136
      quoted read_string String Str l s cs ts tss
blanchet@56078
   137
  | read l cs (Symbol s) (ts :: tss) =
blanchet@56078
   138
      quoted read_symbol Symbol Sym l s cs ts tss
blanchet@56078
   139
  | read l _ _ [] = raise PARSE (l, "bad parser state")
blanchet@56078
   140
blanchet@56078
   141
and token f l cs ts tss =
blanchet@56078
   142
  let val (t, cs') = f l cs
blanchet@56078
   143
  in read l cs' None ((t :: ts) :: tss) end
blanchet@56078
   144
blanchet@56078
   145
and quoted r f g l s cs ts tss =
blanchet@56078
   146
  (case r cs of
blanchet@56078
   147
    NONE => (f (s ^ implode cs), ts :: tss)
blanchet@56078
   148
  | SOME (s', cs') => read l cs' None ((g (s ^ s') :: ts) :: tss))
blanchet@56078
   149
  
blanchet@56078
   150
blanchet@56078
   151
blanchet@56078
   152
(* overall parser *)
blanchet@56078
   153
blanchet@56078
   154
fun read_line l line = read l (raw_explode line)
blanchet@56078
   155
blanchet@56078
   156
fun add_line line (l, (None, tss)) =
blanchet@56078
   157
      if size line = 0 orelse nth_string line 0 = ";" then (l + 1, (None, tss))
blanchet@56078
   158
      else (l + 1, read_line l line None tss)
blanchet@56078
   159
  | add_line line (l, (unfinished, tss)) =
blanchet@56078
   160
      (l + 1, read_line l line unfinished tss)
blanchet@56078
   161
blanchet@56078
   162
fun finish (_, (None, [[t]])) = t
blanchet@56078
   163
  | finish (l, _) = raise PARSE (l, "bad nesting")
blanchet@56078
   164
blanchet@56078
   165
fun parse lines = finish (fold add_line lines (1, (None, [[]])))
blanchet@56078
   166
blanchet@56078
   167
blanchet@56078
   168
(* pretty printer *)
blanchet@56078
   169
blanchet@56078
   170
fun pretty_tree (Num i) = Pretty.str (string_of_int i)
blanchet@56078
   171
  | pretty_tree (Dec (i, j)) =
blanchet@56078
   172
      Pretty.str (string_of_int i ^ "." ^ string_of_int j)
blanchet@56078
   173
  | pretty_tree (Str s) =
blanchet@56078
   174
      raw_explode s
blanchet@56078
   175
      |> maps (fn "\"" => ["\\", "\""] | "\\" => ["\\", "\\"] | c => [c])
blanchet@56078
   176
      |> implode
blanchet@56078
   177
      |> enclose "\"" "\""
blanchet@56078
   178
      |> Pretty.str
blanchet@56078
   179
  | pretty_tree (Sym s) =
blanchet@56078
   180
      if String.isPrefix "(" s (* for bit vector functions *) orelse
blanchet@56078
   181
         forall is_sym (raw_explode s) then
blanchet@56078
   182
        Pretty.str s
blanchet@56078
   183
      else
blanchet@56078
   184
        Pretty.str ("|" ^ s ^ "|")
blanchet@56078
   185
  | pretty_tree (Key s) = Pretty.str (":" ^ s)
blanchet@56078
   186
  | pretty_tree (S trees) =
blanchet@56078
   187
      Pretty.enclose "(" ")" (Pretty.separate "" (map pretty_tree trees))
blanchet@56078
   188
blanchet@56078
   189
val str_of = Pretty.str_of o pretty_tree
blanchet@56078
   190
blanchet@57229
   191
end;