potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
601 stars 79 forks source link

Jorge/assignment #372

Closed jorgefandinno closed 2 years ago

jorgefandinno commented 2 years ago

Hi,

I was looking into the left guard. I am able to parse something of the form

term op &theory_name { ... }

where term is a term (not a theory_term) and op is a theory_op different from :-

I have a question regarding the creation of theory_atoms. They require a theory_term and not a term.

Is there anyway to create a theory_term from a term?

libgringo/tests/left_guard.py

contains a test using the python api

rkaminsk commented 2 years ago

It is very important to me to keep the language clean and uniform. I will not accept a solution that involves a term as left guard and a theory term as right guard. I think that the language extension you are looking for requires a different parser. Something like https://github.com/taocpp/PEGTL might work. Changing the parser would be a quite bit of work. Furthermore, we need to ensure that it is fast enough; we have to ensure that it reads facts fast enough.

I was thinking to rewrite the input module of clingo at some point to provide a nicer API for working with ASTs. Then, I can have a look at parsing too. This is rather a long term project that requires some planning ahead. There is no plan to start right away.

jorgefandinno commented 2 years ago

Ok, a theory term on the left is a requirement requires infinite lookahead, so it seems that a new parser is needed. One can also use a two phase parser, but it seems less clean. For instance, that is the reason why python transition to PEG.

rkaminsk commented 2 years ago

Ok, a theory term on the left is a requirement requires infinite lookahead, so it seems that a new parser is needed. One can also use a two phase parser, but it seems less clean. For instance, that is the reason why python transition to PEG.

PEGs give more control at the expense of more backtracking. I like LR parsers so much because they only accept unambiguous grammars. I don't know of any other parser generator/library that offers this feature. It's the only approach that is fully declarative. :wink: Furthermore, the generated parsers are fast. I don't think that either point will be an issue for clingo. We have a large set of unit tests + a small performance hit should not matter. I'll look into this once I have a bit more time. Your feature request is stacked and I'll keep you in the loop. It still has to wait though.

jorgefandinno commented 2 years ago

You may find interesting the insights of the python transition from LL(1) to PEG. In particular, regarding performance, they say that "we find that the new parser is slightly faster but uses slightly (about 10%) more memory."

https://peps.python.org/pep-0617/

rkaminsk commented 2 years ago

You may find interesting the insights of the python transition from LL(1) to PEG. In particular, regarding performance, they say that "we find that the new parser is slightly faster but uses slightly (about 10%) more memory."

https://peps.python.org/pep-0617/

Funny, how they ruled out LR(1) at the end. As far as I know, it accepts a much larger class of grammars as compared to LL(1). I think they really did not like the tools. For example, we get left and right recursion without any fuzz. For clingo, memory consumption with PEG parsers should not be an issue. We just need a library that allows for marking backtrackable parts, which should be standard.

jorgefandinno commented 2 years ago

One thing that came to my surprise is how bad are both LL and LR algorithms at parsing something that as human is very natural. The problem we have in gringo with left guard is very similar to the problem of assignments mentioned in python. Humans understand infix notation very well and focus on the the infix connective first, while parses seem to have problems if the left part is complex.