search

UCSD-PL / refscript

Refinement Types for Scripting Languages
BSD 3-Clause "New" or "Revised" License
65 stars 3 forks source link

Fixes for fb tests. #63

Closed panagosg7 closed 10 years ago

panagosg7 commented 10 years ago

Created this to address #62 . It should also address #61

Added mseq in consWhile, which removed the pattern match issue.

Also, dead casts override other casts when necessary, given that we don't support multiple casts on the same expression.

About removing the bounds check in body in: https://github.com/UCSD-PL/RefScript/blob/fb_fixes/tests/pos/fb/min-index-01.ts

I can't seem to get K-var inference to work (i.e. not have to spell out the refinement for reduce)

ranjitjhala commented 10 years ago

See the updated file, I think the issue has to do with qualifier scraping. When I give the qual it seems to work...?

panagosg7 commented 10 years ago

Aha, it was because I was using: 

/*@ qualif Len(v: a, n: number)  : n < (len v) */

instead of:

/*@ qualif Len(n: a, arr: b)     : n < (len arr) */
ranjitjhala commented 10 years ago

Yes, but the question is why is it NOT scraping it automatically from the SPEC for reduce?

I get this:

qualif Auto(VV#689 : int, fix##126#A0 : Array Immutable T): (VV#689 < len([fix##126#A0]))

but I wonder why this does not suffice, and why the more general thing is written...

On Mon, Oct 13, 2014 at 5:40 PM, Panagiotis Vekris <notifications@github.com

wrote:

Aha, it was because I was using:

/@ qualif Len(v: a, n: number) : n < (len v) /

instead of:

/@ qualif Len(n: a, arr: b) : n < (len arr) /

Reply to this email directly or view it on GitHub https://github.com/UCSD-PL/RefScript/pull/63#issuecomment-58959012.

Ranjit.