[cutsolver] "named expression already defined with this name"

[BenjaminCosman]

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/cutsolver/tests/todo/overwrite-names.fq

(excerpt from LH https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/Overwrite.hs)

If you change the name of the constant, the test will pass. How do we avoid this kind of name conflict?

[ranjitjhala]

@bmcfluff I can fix this (the fix is to just memoize names of function symbols so we don't define the same symbol twice in SMT land...

[ranjitjhala]

Fixed by https://github.com/ucsd-progsys/liquid-fixpoint/pull/78

[BenjaminCosman]

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/cutsolver/tests/todo/overwrite-names2.fq

Renaming Set_emp makes it pass.

[ranjitjhala]

note to self @ranjitjhala:

This test ALSO passes if we replace FAppTy Set_set X with Set_set X. Wonder why.

[ranjitjhala]

@bmcfluff -- what is the original haskell source that generates this .fq file? Can you re-run it? The .fq file should not have FAppTy Set X it should just have have Set X.

[ranjitjhala]

1. NEVER EVER print out FAppTy (however it is used internally to denote type application),
2. Port the ocaml app_of_t so that it eliminates the FAppTy BEFORE converting to Z3,
3. Hide all "set" related stuff inside Theories.hs (it should not appear in Serialize.hs)
4. LATER Fix OCAML parser to account for (@(0) @(1)) (type variable application, because now, these are NOT explicit)

[ranjitjhala]

This should be addressed by PR #103

Strangely, all LH tests are passing (hopefully no strange caching taking place!) so I didn't (yet) have to do step 4 above.

[ranjitjhala]

@bmcfluff can you check the above (and the original overwrite.hs and confirm before we close this?) Thanks!

[BenjaminCosman]

Looks like it works; closing and merging PR #103