Issue parsing s-expression from SerAPI

[brando90]

I had an unexpected error when parsing a (string) SerAPI response into a nested array/lists representing the AST. @ejgallego can you take a look at the serapi response? It is a valid s-expression right?

Trying to figure out what the issue is, if its from our side or from the parsing library (https://github.com/jd-boyd/sexpdata):

sexp = b'(Answer 3(ObjList((CoqGoal((fg_goals(((name 3)(ty(App(Ind(((Mutind(MPfile(DirPath((Id Logic)(Id Init)(Id Coq))))(DirPath())(Id eq))0)(Instance())))((Ind(((Mutind(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(DirPath())(Id bool))0)(Instance())))(App(Const((Constant(MPfile(DirPath((Id Nat)(Id Init)(Id Coq))))(DirPath())(Id odd))(Instance())))((App(Construct((((Mutind(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(DirPath())(Id nat))0)2)(Instance())))((Construct((((Mutind(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(DirPath())(Id nat))0)1)(Instance())))))))(Construct((((Mutind(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(DirPath())(Id bool))0)1)(Instance()))))))(hyp()))))(bg_goals())(shelved_goals())(given_up_goals()))))))\n'

the error message:

train(policy,optimizer,env,gamma,nb_episodes=nb_episodes,ema_alpha=ema_alpha)
  File "main.py", line 88, in train
    state, reward, done, _ = env.step('Example test_oddb1: Nat.odd 1 = true.')
  File "/Users/brandomiranda/home_simulation_research/coq-serapi-python/python_api/coq_env.py", line 120, in step
    state = self.state_embedder(state)
  File "/Users/brandomiranda/home_simulation_research/coq-serapi-python/python_api/ai_mathematician.py", line 33, in __call__
    psexp = loads(str(sexp))
  File "/Users/brandomiranda/miniconda3/envs/rltp/lib/python3.6/site-packages/sexpdata.py", line 243, in loads
    obj = parse(string, **kwds)
  File "/Users/brandomiranda/miniconda3/envs/rltp/lib/python3.6/site-packages/sexpdata.py", line 675, in parse
    return Parser(string, **kwds).parse()
  File "/Users/brandomiranda/miniconda3/envs/rltp/lib/python3.6/site-packages/sexpdata.py", line 655, in parse
    (i, sexp) = self.parse_sexp(0)
  File "/Users/brandomiranda/miniconda3/envs/rltp/lib/python3.6/site-packages/sexpdata.py", line 641, in parse_sexp
    (i, subsexp) = self.parse_sexp(i + 1)
  File "/Users/brandomiranda/miniconda3/envs/rltp/lib/python3.6/site-packages/sexpdata.py", line 642, in parse_sexp
    append(Quoted(subsexp[0]))
IndexError: list index out of range

[brando90]

I made an issue to the library too: https://github.com/jd-boyd/sexpdata/issues/18

[ejgallego]

Yup indeed it does look fine, I was working on the Json backend tho, so maybe we can switch to it soon, and should provide some relief.

[brando90]

Cool. Do you have an estimate of around when we will switch to json? :) just so I can see if its worth fixing this issue or not.

Sent from my iPhone

On Apr 20, 2019, at 7:47 PM, Emilio Jesús Gallego Arias notifications@github.com wrote:

Yup indeed it does look fine, I was working on the Json backend tho, so maybe we can switch to it soon, and should provide some relief.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub, or mute the thread.

[ejgallego]

From 2 to 4 weeks as not to give you a too optimisitic estimate.

[brando90]

Sounds good! As always no pressure :)

Sent from my iPhone

On Apr 21, 2019, at 8:43 AM, Emilio Jesús Gallego Arias notifications@github.com wrote:

From 2 to 4 weeks as not to give you a too optimisitic estimate.

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub, or mute the thread.

[brando90]

one way to fix this is by using a s-exp parser implemented by pyparsing:

library: https://github.com/pyparsing/pyparsing parser: http://www.ccp4.ac.uk/dist/checkout/pyparsing-2.0.1/examples/sexpParser.py https://stackoverflow.com/questions/3182594/parsing-s-expressions-in-python

---

Question asking for advantages/disadvantages:

https://github.com/jd-boyd/sexpdata/issues/20

[brando90]

@ejgallego ok I think I figured out what the issue is. It seems that serapi gives python 3 a byte array and then to convert that to a string I need to explicitly say the encoding. Using utf-8 works. If you have a preferred encoding (because of something you know about Coq), feel free to tell me.

For now this works:

def buffer_encoding_test():
    print('buffer_encoding_test')
    sexp = b'(Answer 3(ObjList((CoqGoal((fg_goals(((name 3)(ty(Prod(Name(Id n))(Ind(((Mutind(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(DirPath())(Id nat))0)(Instance())))(App(Ind(((Mutind(MPfile(DirPath((Id Logic)(Id Init)(Id Coq))))(DirPath())(Id eq))0)(Instance())))((Ind(((Mutind(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(DirPath())(Id nat))0)(Instance())))(App(Const((Constant(MPfile(DirPath((Id Nat)(Id Init)(Id Coq))))(DirPath())(Id add))(Instance())))((Construct((((Mutind(MPfile(DirPath((Id Datatypes)(Id Init)(Id Coq))))(DirPath())(Id nat))0)1)(Instance())))(Rel 1)))(Rel 1)))))(hyp()))))(bg_goals())(shelved_goals())(given_up_goals()))))))\n'
    sexp = sexp.decode("utf-8")
    print(f'sexp = {sexp}')
    psexp = loads(sexp)

[brando90]

yes asscii is a subset of utf-8 so its fine.

[ejgallego]

Actually there will be some problems with the current API and utf-8, in particular I think that Coq miscalculates file positions some times; so while nothing serious we should keep an eye on potential problems when using non ASCII files.