--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/smtlib2.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,199 @@
+(* Title: HOL/Tools/SMT2/smtlib2.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Parsing and generating SMT-LIB 2.
+*)
+
+signature SMTLIB2 =
+sig
+ exception PARSE of int * string
+ datatype tree =
+ Num of int |
+ Dec of int * int |
+ Str of string |
+ Sym of string |
+ Key of string |
+ S of tree list
+ val parse: string list -> tree
+ val pretty_tree: tree -> Pretty.T
+ val str_of: tree -> string
+end
+
+structure SMTLIB2: SMTLIB2 =
+struct
+
+(* data structures *)
+
+exception PARSE of int * string
+
+datatype tree =
+ Num of int |
+ Dec of int * int |
+ Str of string |
+ Sym of string |
+ Key of string |
+ S of tree list
+
+datatype unfinished = None | String of string | Symbol of string
+
+
+
+(* utilities *)
+
+fun read_raw pred l cs =
+ (case take_prefix pred cs of
+ ([], []) => raise PARSE (l, "empty token")
+ | ([], c :: _) => raise PARSE (l, "unexpected character " ^ quote c)
+ | x => x)
+
+
+
+(* numerals and decimals *)
+
+fun int_of cs = fst (read_int cs)
+
+fun read_num l cs =
+ (case read_raw Symbol.is_ascii_digit l cs of
+ (cs1, "." :: cs') =>
+ let val (cs2, cs'') = read_raw Symbol.is_ascii_digit l cs'
+ in (Dec (int_of cs1, int_of cs2), cs'') end
+ | (cs1, cs2) => (Num (int_of cs1), cs2))
+
+
+
+(* binary numbers *)
+
+fun is_bin c = (c = "0" orelse c = "1")
+
+fun read_bin l cs = read_raw is_bin l cs |>> Num o fst o read_radix_int 2
+
+
+
+(* hex numbers *)
+
+val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF")
+
+fun within c1 c2 c = (ord c1 <= ord c andalso ord c <= ord c2)
+
+fun unhex i [] = i
+ | unhex i (c :: cs) =
+ if within "0" "9" c then unhex (i * 16 + (ord c - ord "0")) cs
+ else if within "a" "f" c then unhex (i * 16 + (ord c - ord "a" + 10)) cs
+ else if within "A" "F" c then unhex (i * 16 + (ord c - ord "A" + 10)) cs
+ else raise Fail ("bad hex character " ^ quote c)
+
+fun read_hex l cs = read_raw is_hex l cs |>> Num o unhex 0
+
+
+
+(* symbols *)
+
+val symbol_chars = raw_explode "~!@$%^&*_+=<>.?/-"
+
+fun is_sym c =
+ Symbol.is_ascii_letter c orelse
+ Symbol.is_ascii_digit c orelse
+ member (op =) symbol_chars c
+
+fun read_sym f l cs = read_raw is_sym l cs |>> f o implode
+
+
+
+(* quoted tokens *)
+
+fun read_quoted stop (escape, replacement) cs =
+ let
+ fun read _ [] = NONE
+ | read rs (cs as (c :: cs')) =
+ if is_prefix (op =) stop cs then
+ SOME (implode (rev rs), drop (length stop) cs)
+ else if not (null escape) andalso is_prefix (op =) escape cs then
+ read (replacement :: rs) (drop (length escape) cs)
+ else read (c :: rs) cs'
+ in read [] cs end
+
+fun read_string cs = read_quoted ["\\", "\""] (["\\", "\\"], "\\") cs
+fun read_symbol cs = read_quoted ["|"] ([], "") cs
+
+
+
+(* core parser *)
+
+fun read _ [] rest tss = (rest, tss)
+ | read l ("(" :: cs) None tss = read l cs None ([] :: tss)
+ | read l (")" :: cs) None (ts1 :: ts2 :: tss) =
+ read l cs None ((S (rev ts1) :: ts2) :: tss)
+ | read l ("#" :: "x" :: cs) None (ts :: tss) =
+ token read_hex l cs ts tss
+ | read l ("#" :: cs) None (ts :: tss) =
+ token read_bin l cs ts tss
+ | read l (":" :: cs) None (ts :: tss) =
+ token (read_sym Key) l cs ts tss
+ | read l ("\"" :: cs) None (ts :: tss) =
+ quoted read_string String Str l "" cs ts tss
+ | read l ("|" :: cs) None (ts :: tss) =
+ quoted read_symbol Symbol Sym l "" cs ts tss
+ | read l ((c as "!") :: cs) None (ts :: tss) =
+ token (fn _ => pair (Sym c)) l cs ts tss
+ | read l (c :: cs) None (ts :: tss) =
+ if Symbol.is_ascii_blank c then read l cs None (ts :: tss)
+ else if Symbol.is_digit c then token read_num l (c :: cs) ts tss
+ else token (read_sym Sym) l (c :: cs) ts tss
+ | read l cs (String s) (ts :: tss) =
+ quoted read_string String Str l s cs ts tss
+ | read l cs (Symbol s) (ts :: tss) =
+ quoted read_symbol Symbol Sym l s cs ts tss
+ | read l _ _ [] = raise PARSE (l, "bad parser state")
+
+and token f l cs ts tss =
+ let val (t, cs') = f l cs
+ in read l cs' None ((t :: ts) :: tss) end
+
+and quoted r f g l s cs ts tss =
+ (case r cs of
+ NONE => (f (s ^ implode cs), ts :: tss)
+ | SOME (s', cs') => read l cs' None ((g (s ^ s') :: ts) :: tss))
+
+
+
+(* overall parser *)
+
+fun read_line l line = read l (raw_explode line)
+
+fun add_line line (l, (None, tss)) =
+ if size line = 0 orelse nth_string line 0 = ";" then (l + 1, (None, tss))
+ else (l + 1, read_line l line None tss)
+ | add_line line (l, (unfinished, tss)) =
+ (l + 1, read_line l line unfinished tss)
+
+fun finish (_, (None, [[t]])) = t
+ | finish (l, _) = raise PARSE (l, "bad nesting")
+
+fun parse lines = finish (fold add_line lines (1, (None, [[]])))
+
+
+
+(* pretty printer *)
+
+fun pretty_tree (Num i) = Pretty.str (string_of_int i)
+ | pretty_tree (Dec (i, j)) =
+ Pretty.str (string_of_int i ^ "." ^ string_of_int j)
+ | pretty_tree (Str s) =
+ raw_explode s
+ |> maps (fn "\"" => ["\\", "\""] | "\\" => ["\\", "\\"] | c => [c])
+ |> implode
+ |> enclose "\"" "\""
+ |> Pretty.str
+ | pretty_tree (Sym s) =
+ if String.isPrefix "(" s (* for bit vector functions *) orelse
+ forall is_sym (raw_explode s) then
+ Pretty.str s
+ else
+ Pretty.str ("|" ^ s ^ "|")
+ | pretty_tree (Key s) = Pretty.str (":" ^ s)
+ | pretty_tree (S trees) =
+ Pretty.enclose "(" ")" (Pretty.separate "" (map pretty_tree trees))
+
+val str_of = Pretty.str_of o pretty_tree
+
+end