|
(* Title: HOL/Tools/SMT/smtlib.ML
Author: Sascha Boehme, TU Muenchen
Parsing and generating SMT-LIB 2.
*)
signature SMTLIB =
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 SMTLIB: SMTLIB =
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 chop_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 ("#" :: "b" :: 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.unformatted_string_of o pretty_tree
end;
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
