UCSD-PL / refscript

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

Non-linear arithmetic #91

Closed BenjaminCosman closed 9 years ago

BenjaminCosman commented 9 years ago

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/non-linear.ts

ranjitjhala commented 9 years ago

Thanks Ben! This

http://rise4fun.com/Z3/xopl3

gives me cause for optimism. I can't duplicate that on my own machine yet, perhaps due to some z3 parameter trickery, but nevertheless there is hope.

On Thu, Jan 15, 2015 at 9:38 AM, bmcfluff notifications@github.com wrote:

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/non-linear.ts

Reply to this email directly or view it on GitHub https://github.com/UCSD-PL/RefScript/issues/91.

Ranjit.

ranjitjhala commented 9 years ago

See the branch "real" -- but we need a way to pass runtime options...

On Jan 15, 2015, at 9:38 AM, bmcfluff notifications@github.com wrote:

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/non-linear.ts

— Reply to this email directly or view it on GitHub.

panagosg7 commented 9 years ago

I just pushed a mechanism to add options:

/*@  option <OPTION SECTION> */ 

Whatever is in

You may want to change: https://github.com/UCSD-PL/RefScript/blob/master/src/Language/Nano/Program.hs#L122 and: https://github.com/UCSD-PL/RefScript/blob/master/src/Language/Nano/Typecheck/Parse.hs#L137

ranjitjhala commented 9 years ago

so where will I see this in the Nano world?

On Fri, Jan 16, 2015 at 3:57 PM, Panagiotis Vekris <notifications@github.com

wrote:

I just pushed a mechanism to add options:

/@ option /

Whatever is in will be parsed as string.

You may want to change:

https://github.com/UCSD-PL/RefScript/blob/master/src/Language/Nano/Program.hs#L122 and:

https://github.com/UCSD-PL/RefScript/blob/master/src/Language/Nano/Typecheck/Parse.hs#L137

Reply to this email directly or view it on GitHub https://github.com/UCSD-PL/RefScript/issues/91#issuecomment-70342018.

Ranjit.

panagosg7 commented 9 years ago

The first link is where it appears in the program and the second the parsing phase

ranjitjhala commented 9 years ago

Got it thanks!

On Jan 16, 2015, at 4:04 PM, Panagiotis Vekris notifications@github.com wrote:

It's part of the program: https://github.com/UCSD-PL/RefScript/blob/master/src/Language/Nano/Program.hs#L122

— Reply to this email directly or view it on GitHub.

panagosg7 commented 9 years ago

This seems to be supported now. Closing.