Skip to content

Repeat returns a list of Cons's#180

Merged
gridaphobe merged 18 commits into
masterfrom
repeat
Sep 1, 2014
Merged

Repeat returns a list of Cons's#180
gridaphobe merged 18 commits into
masterfrom
repeat

Conversation

@gridaphobe

Copy link
Copy Markdown
Contributor

We can prove that repeat returns a List with no Nils, and that we can safely take any number of elements from repeat.

The code is somewhat hacky, I've changed refresh to only expand Refs twice so we don't get an infinite loop when trying to expand a recursive Ref. This required changing a few safeZips in Constraint to regular zips because not all instances of an RApp will have the correct number of Refs.. But it works empirically, i.e. none of our existing tests break..

@gridaphobe

Copy link
Copy Markdown
Contributor Author

@nikivazou are you comfortable merging this? The main concern would be the use of zip instead of safeZip in rSplitCIndexed and substPred.

@nikivazou

Copy link
Copy Markdown
Member

I think expanding Ref twice is too hacky. Cann't there be a case that we need to expand Ref more than 2 times?

@gridaphobe

Copy link
Copy Markdown
Contributor Author

Can you remind me why you think we'd have to expand an RType inside a Ref? I actually think a single expansion would suffice in general.

@nikivazou

Copy link
Copy Markdown
Member

You should be right, a single expansion suffices; which is less hacky than 2 expansions.
Do you know why safeZip fails on rsplit? If we replace it with just zip it means that we may loose some constraints which can hide bugs difficult to debug in the future....

If every expansion in Ref is consistent, then safeZip shouldn't fail.

Conflicts:
	src/Language/Haskell/Liquid/Constraint.hs
	src/Language/Haskell/Liquid/Fresh.hs
	src/Language/Haskell/Liquid/GhcMisc.hs
	src/Language/Haskell/Liquid/Parse.hs
	src/Language/Haskell/Liquid/PredType.hs
	src/Language/Haskell/Liquid/Types.hs
@gridaphobe gridaphobe force-pushed the repeat branch 2 times, most recently from b715d79 to cd9676b Compare August 27, 2014 17:11
@gridaphobe

Copy link
Copy Markdown
Contributor Author

@nikivazou if you have time, can you take another look at this and figure out why the safeZips are blowing up, and what needs to be done to fix them?

@nikivazou

Copy link
Copy Markdown
Member

@gridaphobe did you try merging this branch into master?
After all @ranjitjhala's cleaning I think you will not need to hack the code anymore

@gridaphobe

Copy link
Copy Markdown
Contributor Author

I merged master into it, and the two safeZips still blow up unfortunately..

On Wednesday, August 27, 2014, Niki Vazou notifications@github.com wrote:

@gridaphobe https://github.com/gridaphobe did you try merging this
branch into master?
After all @ranjitjhala https://github.com/ranjitjhala's cleaning I
think you will not need to hack the code anymore


Reply to this email directly or view it on GitHub
#180 (comment)
.

Sent from Gmail Mobile

@nikivazou

Copy link
Copy Markdown
Member

Weird... If you need it for your demo you can merge, but I still prefer safeZips to zips

@gridaphobe

Copy link
Copy Markdown
Contributor Author

I don't need it for the demo, and none of us want to remove the safeZips :)

But it would be nice to merge this branch at some point.

On Wednesday, August 27, 2014, Niki Vazou notifications@github.com wrote:

Weird... If you need it for your demo you can merge, but I still prefer
safeZips to zips


Reply to this email directly or view it on GitHub
#180 (comment)
.

Sent from Gmail Mobile

@nikivazou

Copy link
Copy Markdown
Member

Sure, I will take a look when I find some time

@ranjitjhala

Copy link
Copy Markdown
Member

The bug tickled by this is in tests/todo/absref-crash.hs.

Lets not just replace safeZip with zip until the cause is found.

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

also fixes #235
@gridaphobe gridaphobe merged commit 560d3ee into master Sep 1, 2014
@gridaphobe gridaphobe deleted the repeat branch September 1, 2014 19:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants