Skip to content

Absref bugfix#235

Merged
gridaphobe merged 5 commits into
masterfrom
absref-bugfix
Sep 1, 2014
Merged

Absref bugfix#235
gridaphobe merged 5 commits into
masterfrom
absref-bugfix

Conversation

@ranjitjhala

Copy link
Copy Markdown
Member

Potential bug fix for tests/todo/absref-crash.hs

Still slightly queasy about it it -- it pads missing RProp using top which is ok, I guess. But the question is WHY are those missing?

TODO:

  1. check if it breaks any tests (unlikely)
  2. check if it actually suffices for Repeat.hs and IcfpDemo.hs

@gridaphobe: can you check the TODO items above? I can't run it as they require your tweaks to the parser.
Perhaps you can merge this with your Repeat branch and see if the tests succeed? If so we could merge...

@gridaphobe

Copy link
Copy Markdown
Contributor

@ranjitjhala travis says it doesn't break any tests, which I believe. Unfortunately it does not suffice for Repeat.hs or IcfpDemo.hs.

Furthermore, I can trivially re-break absref-crash.hs by replacing C (foo x) with C $ foo x :(

@gridaphobe

Copy link
Copy Markdown
Contributor

@ranjitjhala I added a couple more pads (e394934) and things seem to be working now, but you should take a look at the commit to make sure those extra pads are OK..

@ranjitjhala

Copy link
Copy Markdown
Member Author

@gridaphobe I simplified the whole pad thing a bit -- so at least its not LENGTH but the fact that one or the other is empty. This seems to work for the $ thing, can you try it on the Repeat.hs ?

@ranjitjhala

Copy link
Copy Markdown
Member Author

@nikivazou I think the bug here is probably that at various places, probably in Bare, we create Type or RefType from Bare but without adding the appropriate [Ref] to each Rapp. That is why, at a bunch of places, we get RApp where the rs are just [] instead of being a list of Top rs for the corresponding predicate. Thats my theory right now, and this simplified pad just accounts for the cases where one or other side has NO rs.

@gridaphobe

Copy link
Copy Markdown
Contributor

@ranjitjhala nice, it works for Repeat.hs and IcfpDemo.hs. If travis says everything else passes, I'll go ahead and merge my branch, which now includes this one.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ranjitjhala we've got a bunch of failing neg-tests now, and I suspect they're due to this line. Seems to me we should return both lists as is if they have equal length.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Duh! Of course! Obvious typo and my bad. pretty shocked that ALL tests didn't fail.

Thank god for tests. ;)

On Aug 29, 2014, at 8:38 AM, Eric Seidel notifications@github.com wrote:

In src/Language/Haskell/Liquid/Misc.hs:

@@ -61,3 +61,16 @@ mapNs ns f xs = foldl (\xs n -> mapN n f xs) xs ns
mapN 0 f (x:xs) = f x : xs
mapN n f (x:xs) = x : mapN (n-1) f xs
mapN _ _ [] = []
+
+

+pad _ f [] ys = (f <$> ys, ys)
+pad _ f xs [] = (xs, f <$> xs)
+pad msg f xs ys

  • | nxs == nys = (xs, f <$> xs)
    @ranjitjhala we've got a bunch of failing neg-tests now, and I suspect they're due to this line. Seems to me we should return both lists as is if they have equal length.


Reply to this email directly or view it on GitHub.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that this whole business is actually a perfect use case for LH: add a 'numRef' parameter to the tycon and specify that the lenght of the refs equals numRef...

On Aug 29, 2014, at 8:46 AM, Ranjit Jhala rjhala@eng.ucsd.edu wrote:

Duh! Of course! Obvious typo and my bad. pretty shocked that ALL tests didn't fail.

Thank god for tests. ;)

On Aug 29, 2014, at 8:38 AM, Eric Seidel notifications@github.com wrote:

In src/Language/Haskell/Liquid/Misc.hs:

@@ -61,3 +61,16 @@ mapNs ns f xs = foldl (\xs n -> mapN n f xs) xs ns
mapN 0 f (x:xs) = f x : xs
mapN n f (x:xs) = x : mapN (n-1) f xs
mapN _ _ [] = []
+
+

+pad _ f [] ys = (f <$> ys, ys)
+pad _ f xs [] = (xs, f <$> xs)
+pad msg f xs ys

  • | nxs == nys = (xs, f <$> xs)
    @ranjitjhala we've got a bunch of failing neg-tests now, and I suspect they're due to this line. Seems to me we should return both lists as is if they have equal length.


Reply to this email directly or view it on GitHub.

@gridaphobe gridaphobe merged commit f5a8ec7 into master Sep 1, 2014
gridaphobe added a commit that referenced this pull request Sep 1, 2014
Repeat returns a list of Cons's

also fixes #235
@gridaphobe gridaphobe deleted the absref-bugfix branch September 1, 2014 19:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants