Skip to content
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

Introduce non-comparable refs #1091

Open
myreen opened this issue Nov 13, 2024 · 0 comments
Open

Introduce non-comparable refs #1091

myreen opened this issue Nov 13, 2024 · 0 comments
Labels
low effort May still assume familiarity

Comments

@myreen
Copy link
Contributor

myreen commented Nov 13, 2024

In the source semantics, reference pointers are Loc values and these can be compared for equality:

do_eq (Loc l1) (Loc l2) = Eq_val (l1 = l2) ∧

When we introduce thunks #1090, we will have Loc values that point to thunks. In order to represent thunks in the most space efficient way we don't want to support equality tests between thunk values.

This issue is about adding a boolean to the Loc constructor. The boolean will indicate whether the Loc can be compared or not. Thus all current Loc n values would be equivalent to Loc T n and all Loc F k values are pointers to heap elements that cannot be compared.

I propose that the semantics of do_eq is changed to:

do_eq (Loc b1 l1) (Loc b2 l2) = (if b1 ∧ b2 then Eq_val (l1 = l2) else Eq_type_error) ∧ 
@myreen myreen added the low effort May still assume familiarity label Nov 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
low effort May still assume familiarity
Projects
None yet
Development

No branches or pull requests

1 participant