Extend parser to allow boolean function arguments

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types

BSD 3-Clause "New" or "Revised" License

132 stars 60 forks source link

Extend parser to allow boolean function arguments #678

Closed ranjitjhala closed 6 months ago

ranjitjhala commented 7 months ago

So that f ?(x > y) can be parsed as an Expr or Pred.

Ideally, we'd want to do this without the nasty ? but I can't seem to unravel the knots needed to do so :-(

ranjitjhala commented 7 months ago

@facundominguez -- did you want to take a quick look at this, in case you have any suggestions?

facundominguez commented 7 months ago

Hey, I'll be away from the keyboard for a couple of weeks. But yes, this should be doable. If you need this merged, you could open a separate issue to investigate removing the question mark.