String literals, quoting and escaping

[SaswatPadhi]

Hello,

I think I don't understand how quotes are treated by this library, and how to distinguish between Atoms that are sting literals vs. other Atoms -- for example, x below may be a variable and "y" and "(y)" are literals.

─( 10:04:36 )─< command 3 ────────────────────────────────────────────────────
utop # Sexp.of_string "((x) (\"(y)\"))";;
- : Sexp.t =
Core.Sexp.List
 [Core.Sexp.List [Core.Sexp.Atom "x"]; Core.Sexp.List [Core.Sexp.Atom "(y)"]]

─( 10:04:55 )─< command 4 ────────────────────────────────────────────────────
utop # Sexp.of_string "((x) ('(y)'))";;
- : Sexp.t =
Core.Sexp.List
 [Core.Sexp.List [Core.Sexp.Atom "x"];
  Core.Sexp.List
   [Core.Sexp.Atom "'"; Core.Sexp.List [Core.Sexp.Atom "y"];
    Core.Sexp.Atom "'"]]

─( 10:05:14 )─< command 5 ────────────────────────────────────────────────────
utop # Sexp.of_string "((x) ('y'))";;
- : Sexp.t =
Core.Sexp.List
 [Core.Sexp.List [Core.Sexp.Atom "x"]; Core.Sexp.List [Core.Sexp.Atom "'y'"]]

─( 10:05:27 )─< command 6 ────────────────────────────────────────────────────
utop # Sexp.of_string "((x) (\"y\"))";;
- : Sexp.t =
Core.Sexp.List
 [Core.Sexp.List [Core.Sexp.Atom "x"]; Core.Sexp.List [Core.Sexp.Atom "y"]]

I am trying to find a way to quote that works for both y and (y), so that I can distinguish them from x. As seen in the commands above, neither single nor double quotes seem to help with this. Double quotes are simply ignored, and single quotes don't work for (y).

Is there anyway to achieve this?

[ghost]

Note that y and "y" are two different representations of the same s-expression: the atom y. Double quotes are simply used to represent atoms containing special characters such as spaces or parentheses.

[SaswatPadhi]

I see. Thanks. Is there another way to distinguish y and "y" then? Or does Sexplib not support this?

I am trying to parse SMT-LIB2 sexpressions like the following:

(declare-const a String)
(declare-const b String)
(assert (= (str.++ b a) (str.++ "abc" b)))
(check-sat)

where I it's necessary to treat a and b differently than "abc".

[ghost]

Sexplib doesn't support this. Additionally, I don't know SMT-LIB2, but I wouldn't be surprised if the lexical conventions are not the same as Sexplib. You are probably better off writing a specific lexer using ocamllex.

[SaswatPadhi]

Thanks.

[ghost]

I'm closing this issue since this is outside of the scope of sexplib, let us know if you have other questions.