search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 60 forks source link

Allow to write predicates without question marks #682

Open facundominguez opened 6 months ago

facundominguez commented 6 months ago

Recently #678 introduced the ability to write predicates inside other expressions by using a question mark.

This issue is to investigate if we can remove the question mark.

facundominguez commented 6 months ago

I'm guessing we could use some insight on why liquid-fixpoint has separate parsers for predicates and expressions.

Is the difference between a predicate and an expression only about the operators that they use?

I think that by removing the question mark, the grammar becomes left recursive via: expr0P -> predP -> pred0P -> predrP -> exprP -> expr1P -> expr0P. But I'd like to understand better the motivation of the current implementation ahead of considering changes.

ranjitjhala commented 6 months ago

@facundominguez the honest answer is it is just a quirk of history. Originally we had separate types Expr and Pred and the former were not supposed to be bool valued, but over time this became untenable and so they are all really just a single type BUT the parser somehow still kept this (needless) stratification… so really no good technical reason!

facundominguez commented 6 months ago

Thanks @ranjitjhala. That is helpful to know. In that case, probably we should try consolidating the parsers.

ranjitjhala commented 6 months ago

indeed though even better may be to switch over to a full SMTLIB style prefix-parens syntax …

facundominguez commented 6 months ago

... yes, Ranjit, please start a new issue if you want to change the user interface that far :)

Please correct me if I'm wrong: if Liquid Haskell continues to use the current language, only removing the question mark might still worth the trouble.

ranjitjhala commented 6 months ago

Yup, you’re right! :-)