Commit f114bed5 authored by Benedikt Becker's avatar Benedikt Becker

Custom s-expr printer to escape single quotes and brackets

parent 791cd93b
......@@ -500,7 +500,7 @@ let () =
let f = Filename.(chop_extension (basename filename)) in
deps_file std_formatter true f mlw_file
| Sexp, None, 0 ->
Why3pp_sexp.why3pp_sexp mlw_file
Why3pp_sexp.why3pp_sexp stdout mlw_file
| _, _, _ ->
Getopt.handle_exn Sys.argv "invalid arguments"
)
......
let why3pp_sexp _ =
let why3pp_sexp _ _ =
output_string stderr "error: S-expression output unsupported\n";
exit 1
let why3pp_sexp mlw_file =
Why3.Ptree.sexp_of_mlw_file mlw_file |>
Sexplib.Sexp.output_hum_indent 2 stdout
open Format
open Sexplib.Sexp
(* Check if a string contains only characters [a-zA-Z0-9_-] *)
let is_simple_token s =
let rec loop i =
if i < 0 then
true
else match s.[i] with
| 'a'..'z' | 'A'..'Z' | '0'..'9' | '_' | '-' ->
loop (i-1)
| _ -> false in
loop (String.length s-1)
let rec output fmt = function
| Atom s ->
if is_simple_token s then
fprintf fmt "%s" s
else
fprintf fmt "%S" s
| List l ->
let pp_sep fmt () = fprintf fmt "@ " in
fprintf fmt "@[<hv2>(%a)@]" (pp_print_list ~pp_sep output) l
let why3pp_sexp out mlw_file =
let sexp = Why3.Ptree.sexp_of_mlw_file mlw_file in
output (Format.formatter_of_out_channel out) sexp
(* Functions [Sexplib.Sexp.output*] do not escape brackets and quotes in tokens *)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment