Unique mutable

[panagosg7]

Special Mutability class UniqueMutability to prolong the phase of initializing objects.

See:

https://github.com/UCSD-PL/RefScript/blob/unique_mutable/tests/pos/classes/init-02.ts

[ranjitjhala]

Nice, can you type this example without the if test but with a suitable signature for createFoo?

On Feb 23, 2015, at 4:36 PM, Panagiotis Vekris notifications@github.com wrote:

Special Mutability class UniqueMutability to prolong the phase of initializing objects.

See:

https://github.com/UCSD-PL/RefScript/blob/unique_mutable/tests/pos/classes/init-02.ts

You can view, comment on, or merge this pull request online at:

https://github.com/UCSD-PL/RefScript/pull/99

Commit Summary

Fix in perdicate alias check Restricting fun ty conversion cleanup Initial support for unique mutable state Fixing up some bitvector issues Adding UniqueMutable examples File Changes

M include/prelude.ts (102) M src/Language/Nano/Annots.hs (3) M src/Language/Nano/Env.hs (3) M src/Language/Nano/Errors.hs (3) M src/Language/Nano/Liquid/Alias.hs (6) M src/Language/Nano/Liquid/CGMonad.hs (8) M src/Language/Nano/Liquid/Liquid.hs (55) M src/Language/Nano/Liquid/Types.hs (5) M src/Language/Nano/Typecheck/Lookup.hs (3) M src/Language/Nano/Typecheck/Sub.hs (4) M src/Language/Nano/Typecheck/TCMonad.hs (7) M src/Language/Nano/Typecheck/Typecheck.hs (97) M src/Language/Nano/Typecheck/Types.hs (73) A tests/neg/classes/init-02.ts (21) M tests/neg/simple/bitvector-02.ts (10) M tests/pos/arrays/arr-04.ts (12) M tests/pos/classes/class-10.ts (3) A tests/pos/classes/init-02.ts (21) M tests/pos/inclusion/forin-00.ts (2) M tests/pos/simple/addEntry.ts (12) R tests/todo/features/bracketref-00.ts (4) Patch Links:

https://github.com/UCSD-PL/RefScript/pull/99.patch https://github.com/UCSD-PL/RefScript/pull/99.diff — Reply to this email directly or view it on GitHub.

[panagosg7]

I pushed two more (not sure if this is what you're asking for): https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/classes/init-03.ts https://github.com/UCSD-PL/RefScript/blob/master/tests/neg/classes/init-03.ts

[ranjitjhala]

No I meant init-02 but with a signature like

/@ createFoo :: () => { Foo | v.f = 10 } /

On Mon, Feb 23, 2015 at 5:39 PM, Panagiotis Vekris <notifications@github.com

wrote:

I pushed two more (not sure if this is what you're asking for):

https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/classes/init-03.ts

https://github.com/UCSD-PL/RefScript/blob/master/tests/neg/classes/init-03.ts

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

Ranjit.

[panagosg7]

We've dropped support for Keyval- like predicates On Feb 23, 2015 6:13 PM, "Ranjit Jhala" notifications@github.com wrote:

No I meant init-02 but with a signature like

/@ createFoo :: () => { Foo | v.f = 10 } /

On Mon, Feb 23, 2015 at 5:39 PM, Panagiotis Vekris < notifications@github.com

wrote:

I pushed two more (not sure if this is what you're asking for):

https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/classes/init-03.ts

https://github.com/UCSD-PL/RefScript/blob/master/tests/neg/classes/init-03.ts

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

Ranjit.

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

[ranjitjhala]

Then what exactly is in the environment after the if test? How does the thing know that the value of the infield equals 10 at assertat?

On Feb 23, 2015, at 6:22 PM, Panagiotis Vekris notifications@github.com wrote:

We've dropped support for Keyval- like predicates On Feb 23, 2015 6:13 PM, "Ranjit Jhala" notifications@github.com wrote:

No I meant init-02 but with a signature like

/@ createFoo :: () => { Foo | v.f = 10 } /

On Mon, Feb 23, 2015 at 5:39 PM, Panagiotis Vekris < notifications@github.com

wrote:

I pushed two more (not sure if this is what you're asking for):

https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/classes/init-03.ts

https://github.com/UCSD-PL/RefScript/blob/master/tests/neg/classes/init-03.ts

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

Ranjit.

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

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

[panagosg7]

It's because there is a separate temp variable added to the environment for each immutable field. So both accesses expose that same variable. On Feb 23, 2015 6:38 PM, "Ranjit Jhala" notifications@github.com wrote:

Then what exactly is in the environment after the if test? How does the thing know that the value of the infield equals 10 at assertat?

On Feb 23, 2015, at 6:22 PM, Panagiotis Vekris notifications@github.com wrote:

We've dropped support for Keyval- like predicates On Feb 23, 2015 6:13 PM, "Ranjit Jhala" notifications@github.com wrote:

No I meant init-02 but with a signature like

/@ createFoo :: () => { Foo | v.f = 10 } /

On Mon, Feb 23, 2015 at 5:39 PM, Panagiotis Vekris < notifications@github.com

wrote:

I pushed two more (not sure if this is what you're asking for):

https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/classes/init-03.ts

https://github.com/UCSD-PL/RefScript/blob/master/tests/neg/classes/init-03.ts

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

Ranjit.

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

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

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