src/HOL/Tools/SMT/smtlib.ML
changeset 58061 3d060f43accb
parent 57704 c0da3fc313e3
child 61877 276ad4354069
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/SMT/smtlib.ML	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -0,0 +1,191 @@
     1.4 +(*  Title:      HOL/Tools/SMT/smtlib.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +Parsing and generating SMT-LIB 2.
     1.8 +*)
     1.9 +
    1.10 +signature SMTLIB =
    1.11 +sig
    1.12 +  exception PARSE of int * string
    1.13 +  datatype tree = 
    1.14 +    Num of int |
    1.15 +    Dec of int * int |
    1.16 +    Str of string |
    1.17 +    Sym of string |
    1.18 +    Key of string |
    1.19 +    S of tree list
    1.20 +  val parse: string list -> tree
    1.21 +  val pretty_tree: tree -> Pretty.T
    1.22 +  val str_of: tree -> string
    1.23 +end;
    1.24 +
    1.25 +structure SMTLIB: SMTLIB =
    1.26 +struct
    1.27 +
    1.28 +(* data structures *)
    1.29 +
    1.30 +exception PARSE of int * string
    1.31 +
    1.32 +datatype tree = 
    1.33 +  Num of int |
    1.34 +  Dec of int * int |
    1.35 +  Str of string |
    1.36 +  Sym of string |
    1.37 +  Key of string |
    1.38 +  S of tree list
    1.39 +
    1.40 +datatype unfinished = None | String of string | Symbol of string
    1.41 +
    1.42 +
    1.43 +(* utilities *)
    1.44 +
    1.45 +fun read_raw pred l cs =
    1.46 +  (case take_prefix pred cs of
    1.47 +    ([], []) => raise PARSE (l, "empty token")
    1.48 +  | ([], c :: _) => raise PARSE (l, "unexpected character " ^ quote c)
    1.49 +  | x => x)
    1.50 +
    1.51 +
    1.52 +(* numerals and decimals *)
    1.53 +
    1.54 +fun int_of cs = fst (read_int cs)
    1.55 +
    1.56 +fun read_num l cs =
    1.57 +  (case read_raw Symbol.is_ascii_digit l cs of
    1.58 +    (cs1, "." :: cs') =>
    1.59 +      let val (cs2, cs'') = read_raw Symbol.is_ascii_digit l cs'
    1.60 +      in (Dec (int_of cs1, int_of cs2), cs'') end
    1.61 +  | (cs1, cs2) => (Num (int_of cs1), cs2))
    1.62 +
    1.63 +
    1.64 +(* binary numbers *)
    1.65 +
    1.66 +fun is_bin c = (c = "0" orelse c = "1")
    1.67 +
    1.68 +fun read_bin l cs = read_raw is_bin l cs |>> Num o fst o read_radix_int 2
    1.69 +
    1.70 +
    1.71 +(* hex numbers *)
    1.72 +
    1.73 +val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF")
    1.74 +
    1.75 +fun within c1 c2 c = (ord c1 <= ord c andalso ord c <= ord c2)
    1.76 +
    1.77 +fun unhex i [] = i
    1.78 +  | unhex i (c :: cs) =
    1.79 +      if within "0" "9" c then unhex (i * 16 + (ord c - ord "0")) cs
    1.80 +      else if within "a" "f" c then unhex (i * 16 + (ord c - ord "a" + 10)) cs
    1.81 +      else if within "A" "F" c then unhex (i * 16 + (ord c - ord "A" + 10)) cs
    1.82 +      else raise Fail ("bad hex character " ^ quote c)
    1.83 +
    1.84 +fun read_hex l cs = read_raw is_hex l cs |>> Num o unhex 0
    1.85 +
    1.86 +
    1.87 +(* symbols *)
    1.88 +
    1.89 +val symbol_chars = raw_explode "~!@$%^&*_+=<>.?/-" 
    1.90 +
    1.91 +fun is_sym c =
    1.92 +  Symbol.is_ascii_letter c orelse
    1.93 +  Symbol.is_ascii_digit c orelse
    1.94 +  member (op =) symbol_chars c
    1.95 +
    1.96 +fun read_sym f l cs = read_raw is_sym l cs |>> f o implode
    1.97 +
    1.98 +
    1.99 +(* quoted tokens *)
   1.100 +
   1.101 +fun read_quoted stop (escape, replacement) cs =
   1.102 +  let
   1.103 +    fun read _ [] = NONE
   1.104 +      | read rs (cs as (c :: cs')) =
   1.105 +          if is_prefix (op =) stop cs then
   1.106 +            SOME (implode (rev rs), drop (length stop) cs)
   1.107 +          else if not (null escape) andalso is_prefix (op =) escape cs then
   1.108 +            read (replacement :: rs) (drop (length escape) cs)
   1.109 +          else read (c :: rs) cs'
   1.110 +  in read [] cs end
   1.111 +
   1.112 +fun read_string cs = read_quoted ["\\", "\""] (["\\", "\\"], "\\") cs
   1.113 +fun read_symbol cs = read_quoted ["|"] ([], "") cs
   1.114 +
   1.115 +
   1.116 +(* core parser *)
   1.117 +
   1.118 +fun read _ [] rest tss = (rest, tss)
   1.119 +  | read l ("(" :: cs) None tss = read l cs None ([] :: tss)
   1.120 +  | read l (")" :: cs) None (ts1 :: ts2 :: tss) =
   1.121 +      read l cs None ((S (rev ts1) :: ts2) :: tss)
   1.122 +  | read l ("#" :: "x" :: cs) None (ts :: tss) =
   1.123 +      token read_hex l cs ts tss
   1.124 +  | read l ("#" :: "b" :: cs) None (ts :: tss) =
   1.125 +      token read_bin l cs ts tss
   1.126 +  | read l (":" :: cs) None (ts :: tss) =
   1.127 +      token (read_sym Key) l cs ts tss
   1.128 +  | read l ("\"" :: cs) None (ts :: tss) =
   1.129 +      quoted read_string String Str l "" cs ts tss
   1.130 +  | read l ("|" :: cs) None (ts :: tss) =
   1.131 +      quoted read_symbol Symbol Sym l "" cs ts tss
   1.132 +  | read l ((c as "!") :: cs) None (ts :: tss) =
   1.133 +      token (fn _ => pair (Sym c)) l cs ts tss
   1.134 +  | read l (c :: cs) None (ts :: tss) =
   1.135 +      if Symbol.is_ascii_blank c then read l cs None (ts :: tss)
   1.136 +      else if Symbol.is_digit c then token read_num l (c :: cs) ts tss
   1.137 +      else token (read_sym Sym) l (c :: cs) ts tss
   1.138 +  | read l cs (String s) (ts :: tss) =
   1.139 +      quoted read_string String Str l s cs ts tss
   1.140 +  | read l cs (Symbol s) (ts :: tss) =
   1.141 +      quoted read_symbol Symbol Sym l s cs ts tss
   1.142 +  | read l _ _ [] = raise PARSE (l, "bad parser state")
   1.143 +
   1.144 +and token f l cs ts tss =
   1.145 +  let val (t, cs') = f l cs
   1.146 +  in read l cs' None ((t :: ts) :: tss) end
   1.147 +
   1.148 +and quoted r f g l s cs ts tss =
   1.149 +  (case r cs of
   1.150 +    NONE => (f (s ^ implode cs), ts :: tss)
   1.151 +  | SOME (s', cs') => read l cs' None ((g (s ^ s') :: ts) :: tss))
   1.152 +  
   1.153 +
   1.154 +
   1.155 +(* overall parser *)
   1.156 +
   1.157 +fun read_line l line = read l (raw_explode line)
   1.158 +
   1.159 +fun add_line line (l, (None, tss)) =
   1.160 +      if size line = 0 orelse nth_string line 0 = ";" then (l + 1, (None, tss))
   1.161 +      else (l + 1, read_line l line None tss)
   1.162 +  | add_line line (l, (unfinished, tss)) =
   1.163 +      (l + 1, read_line l line unfinished tss)
   1.164 +
   1.165 +fun finish (_, (None, [[t]])) = t
   1.166 +  | finish (l, _) = raise PARSE (l, "bad nesting")
   1.167 +
   1.168 +fun parse lines = finish (fold add_line lines (1, (None, [[]])))
   1.169 +
   1.170 +
   1.171 +(* pretty printer *)
   1.172 +
   1.173 +fun pretty_tree (Num i) = Pretty.str (string_of_int i)
   1.174 +  | pretty_tree (Dec (i, j)) =
   1.175 +      Pretty.str (string_of_int i ^ "." ^ string_of_int j)
   1.176 +  | pretty_tree (Str s) =
   1.177 +      raw_explode s
   1.178 +      |> maps (fn "\"" => ["\\", "\""] | "\\" => ["\\", "\\"] | c => [c])
   1.179 +      |> implode
   1.180 +      |> enclose "\"" "\""
   1.181 +      |> Pretty.str
   1.182 +  | pretty_tree (Sym s) =
   1.183 +      if String.isPrefix "(" s (* for bit vector functions *) orelse
   1.184 +         forall is_sym (raw_explode s) then
   1.185 +        Pretty.str s
   1.186 +      else
   1.187 +        Pretty.str ("|" ^ s ^ "|")
   1.188 +  | pretty_tree (Key s) = Pretty.str (":" ^ s)
   1.189 +  | pretty_tree (S trees) =
   1.190 +      Pretty.enclose "(" ")" (Pretty.separate "" (map pretty_tree trees))
   1.191 +
   1.192 +val str_of = Pretty.str_of o pretty_tree
   1.193 +
   1.194 +end;