add example CCParse-based Sexpr parser, and a test

This commit is contained in:
Simon Cruanes 2021-06-06 18:50:28 -04:00
parent 88fe234a4c
commit 7bdc3cff24
3 changed files with 96 additions and 3 deletions

66
examples/ccparse_sexp.ml Normal file
View file

@ -0,0 +1,66 @@
open CCParse
type sexp = Atom of string | List of sexp list
let rec pp_sexpr out (s:sexp) : unit = match s with
| Atom s -> Format.fprintf out "%S" s
| List l ->
Format.fprintf out "(@[";
List.iteri (fun i s -> if i>0 then Format.fprintf out "@ "; pp_sexpr out s) l;
Format.fprintf out "@])"
let str_of_sexp = CCFormat.to_string pp_sexpr
let skip_white_and_comments =
fix @@ fun self ->
skip_white *>
( try_or (char ';')
~f:(fun _ -> skip_chars (function '\n' -> false | _ -> true) *> self)
~else_:(return ())
)
let atom =
chars_fold_map `Start
~f:(fun acc c ->
match acc, c with
| `Start, '"' -> `Continue `In_quote
| `Start, (' ' | '\t' | '\n' | '(' | ')' | ';') -> `Fail "atom"
| `Normal, (' ' | '\t' | '\n' | '(' | ')' | ';') -> `Stop
| `Done, _ -> `Stop
| `In_quote, '"' -> `Continue `Done (* consume *)
| `In_quote, '\\' -> `Continue `Escape
| `In_quote, c -> `Yield (`In_quote, c)
| `Escape, 'n' -> `Yield (`In_quote, '\n')
| `Escape, 't' -> `Yield (`In_quote, '\t')
| `Escape, '"' -> `Yield (`In_quote, '"')
| `Escape, '\\' -> `Yield (`In_quote, '\\')
| `Escape, c -> `Fail (Printf.sprintf "unknown escape code \\%c" c)
| (`Start | `Normal), c -> `Yield (`Normal, c)
| _ -> `Fail "invalid atom"
)
>>= function
| `In_quote, _ -> fail "unclosed \""
| `Escape, _ -> fail "unfinished escape sequence"
| _, "" -> fail "expected non-empty atom"
| _, s -> return (Atom s)
let psexp =
fix @@ fun self ->
skip_white_and_comments *>
try_or (char '(')
~f:(fun _ ->
(sep ~by:skip_white_and_comments self
<* skip_white_and_comments <* char ')') >|= fun l -> List l)
~else_:atom
let psexp_l =
many_until ~until:(skip_white_and_comments *> eoi) psexp
let () =
let s = CCIO.File.read_exn Sys.argv.(1) in
match parse_string psexp_l s with
| Ok l ->
Format.printf "parsed:@.";
List.iter (Format.printf "%a@." pp_sexpr) l
| Error e ->
Format.printf "parse error: %s@." e; exit 1

View file

@ -1,8 +1,22 @@
(executable (executables
(name id_sexp) (names id_sexp ccparse_sexp)
(libraries containers) (libraries containers)
(modules id_sexp) ;(modules id_sexp)
(flags :standard -warn-error -a+8 -safe-string -color always) (flags :standard -warn-error -a+8 -safe-string -color always)
(ocamlopt_flags :standard -O3 -color always (ocamlopt_flags :standard -O3 -color always
-unbox-closures -unbox-closures-factor 20)) -unbox-closures -unbox-closures-factor 20))
(alias
(name runtest)
(locks /ctest)
(action
(ignore-stdout
(run ./id_sexp.exe test_data/benchpress.sexp))))
(alias
(name runtest)
(locks /ctest)
(action
(ignore-stdout
(run ./ccparse_sexp.exe test_data/benchpress.sexp))))

View file

@ -0,0 +1,13 @@
(prover
(name msat)
(synopsis "msat for pure sat problems")
(version "git:.")
(sat "^Sat")
(unsat "^Unsat")
(cmd "$cur_dir/../msat.exe -time $timeout $file"))
(dir
(path $cur_dir)
(pattern ".*\\.cnf")
(expect (const unknown)))