search

ucsd-progsys / liquid-fixpoint

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

"_|_" is parsed as 'POr' #298

Closed alanz closed 7 years ago

alanz commented 7 years ago

parsing _|_ results in POr [], not the expected EBot

nikivazou commented 7 years ago

Correct, because disjunction of an empty list is false. Dually true us encoded as a conjunction of an empty list!

On Mar 20, 2017 8:26 AM, "Alan Zimmerman" notifications@github.com wrote:

parsing | results in POr [], not the expected EBot

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/298, or mute the thread https://github.com/notifications/unsubscribe-auth/AArotWWwk-aiTUi-XHi95HJ1IUTP5SKbks5rnnCFgaJpZM4MiXG9 .

alanz commented 7 years ago

Hmm, perhaps it is a result of

pattern EBot          = POr  []
alanz commented 7 years ago

So maybe we should return POr [] in the parser and do away with EBot completely?

ranjitjhala commented 7 years ago

Why do we have this at all? why not just False ?

On Mon, Mar 20, 2017 at 5:32 AM, Alan Zimmerman notifications@github.com wrote:

So maybe we should return POr [] in the parser and do away with EBot completely?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/298#issuecomment-287745997, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOMmiOKUJNJ_Ps_VcieWoOh25LaWTks5rnnHOgaJpZM4MiXG9 .

alanz commented 7 years ago

FWIW, _|_ does not appear in the test suites of either liquidhaskell or liquid-fixpoint.

nikivazou commented 7 years ago

Well, all these _|_, False and POr [] are semantically equivalent and all represented as POr [] internally.

I have never writen _|_ myself, should be there for historical reason (that are described in the original Liquid Types paper).

Ranjit, there is no False data constructor.

gridaphobe commented 7 years ago

Looks like @nikivazou replaced the PFalse and PTrue constructors with the PatternSynonyms in 8eed3ca982a33bb4cafabbee95e23e9e04088958. I vaguely recall having some discussion about it around the time of the Expr/Pred merge, seems reasonable to me..

ranjitjhala commented 7 years ago

What seems reasonable? Removing support for this?

On Mon, Mar 20, 2017 at 7:51 AM Eric Seidel notifications@github.com wrote:

Looks like @nikivazou https://github.com/nikivazou replaced the PFalse and PTrue constructors with the PatternSynonyms in 8eed3ca https://github.com/ucsd-progsys/liquid-fixpoint/commit/8eed3ca982a33bb4cafabbee95e23e9e04088958. I vaguely recall having some discussion about it around the time of the Expr/Pred merge, seems reasonable to me..

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/298#issuecomment-287783071, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOMb6NiHOysFuiYQBDI5ruWPVA0P-ks5rnpJzgaJpZM4MiXG9 .

nikivazou commented 7 years ago

Defining False as POr [] is reasonable