New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make primitive types in prims as eqtype #1514

Closed
aseemr opened this Issue Aug 19, 2018 · 4 comments

Comments

Projects
None yet
2 participants
@aseemr
Contributor

aseemr commented Aug 19, 2018

We generate unnecessary SMT queries for hasEq int, hasEq bool, hasEq nat, etc. I tried marking these as eqtype in prims, but got some regressions. Will try to squash it in this cycle.

@aseemr aseemr self-assigned this Aug 19, 2018

@s-zanella s-zanella changed the title from Make primtiive types in prims as eqtype to Make primitive types in prims as eqtype Aug 20, 2018

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Aug 20, 2018

Contributor

Another option we discussed in the call is simplifying hasEq in the normalizer. For instance, adding reduction such as:

hasEq int -> True
hasEq (x:int{_}) -> True
hasEq nat -> True
hasEq (list a) -> hasEq a

I find it a bit less elegant than the annotating in prims, but has the advantage that it could reduce hasEq (list int) to True, which annotations won't do. On the other hand, I think this would fail:

let test (a:Type) (_ : squash (hasEq (list a))) =
    assert (hasEq (list a))

since the assertion would be simplified to hasEq a, and there's no way of proving that. Probably not too serious in practice, but worth keeping in mind.

EDIT: Thinking about that again, we should make sure to simplify things to equivalent ones. Turning hasEq (list a) into hasEq a might not be sound, as it can appear on a LHS.

Contributor

mtzguido commented Aug 20, 2018

Another option we discussed in the call is simplifying hasEq in the normalizer. For instance, adding reduction such as:

hasEq int -> True
hasEq (x:int{_}) -> True
hasEq nat -> True
hasEq (list a) -> hasEq a

I find it a bit less elegant than the annotating in prims, but has the advantage that it could reduce hasEq (list int) to True, which annotations won't do. On the other hand, I think this would fail:

let test (a:Type) (_ : squash (hasEq (list a))) =
    assert (hasEq (list a))

since the assertion would be simplified to hasEq a, and there's no way of proving that. Probably not too serious in practice, but worth keeping in mind.

EDIT: Thinking about that again, we should make sure to simplify things to equivalent ones. Turning hasEq (list a) into hasEq a might not be sound, as it can appear on a LHS.

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 8, 2018

Contributor

I have Aseem's version of the fix in the PR above, and Aseem has my version on a branch of his. I messed up and forgot to sync with him before starting to work on this, but seems we got lucky :).

Contributor

mtzguido commented Oct 8, 2018

I have Aseem's version of the fix in the PR above, and Aseem has my version on a branch of his. I messed up and forgot to sync with him before starting to work on this, but seems we got lucky :).

aseemr added a commit that referenced this issue Oct 9, 2018

normalizing hasEq in the normalizer for assumed types in prims, also …
…stripping down the refinemenets from the type argument, cf. #1514

aseemr added a commit that referenced this issue Oct 9, 2018

@aseemr

This comment has been minimized.

Show comment
Hide comment
@aseemr

aseemr Oct 9, 2018

Contributor

I pushed the normalizer changes to master. Since it changes the wps, also made sure that there is no verification impact on Everest.

Contributor

aseemr commented Oct 9, 2018

I pushed the normalizer changes to master. Since it changes the wps, also made sure that there is no verification impact on Everest.

@mtzguido

This comment has been minimized.

Show comment
Hide comment
@mtzguido

mtzguido Oct 9, 2018

Contributor

They are now also eqtypes in prims, closing.

Contributor

mtzguido commented Oct 9, 2018

They are now also eqtypes in prims, closing.

@mtzguido mtzguido closed this Oct 9, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment