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

More support for Array and Slice #252

Merged
merged 21 commits into from
Dec 18, 2022
Merged

More support for Array and Slice #252

merged 21 commits into from
Dec 18, 2022

Conversation

ranjitjhala
Copy link
Contributor

Fixes #184 maybe?

The main big change is factoring Array and Slice as BaseTy to allow refining with size.

Copy link
Member

@nilehmann nilehmann left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My initial reaction was that indexing arrays by the length would cause inconsistencies as you could write an array where the indexed length is different than the const length

#[flux::sig(fn([i32; _][2]))]
fn myarr(a: [i32; 1]) {
    a[1]
}

But if array literal are the only way to construct arrays then I think this should be ok and it just declaring an inhabited type. However, not connecting both lengths makes code cumbersome. For example, it makes it impossible to use the result of a function like https://doc.rust-lang.org/std/primitive.u32.html#method.to_be_bytes without explicitly checking the length, even though you already know the length is 4. Ideally, arrays shouldn’t be indexed but rather we the const length should be automatically reflected into the logic when needed, i.e., the typing rule for Len should be something like

|- a: [T; n]         reflect(n) = a
———————————————————————————--———-——-
          |- Len(a): usize[a]

I’m ok with leaving the implementation like this for now as doing this reflection requires further design.

flux-desugar/src/table_resolver.rs Outdated Show resolved Hide resolved
flux-desugar/src/desugar.rs Outdated Show resolved Hide resolved
@@ -575,6 +567,16 @@ impl BaseTy {
BaseTy::Adt(adt_def, substs.into())
}

pub fn array(ty: Ty, c: Const) -> BaseTy {
BaseTy::Array(ty, c)
// Ty::indexed(BaseTy::Array(ty, c), RefineArgs::empty())
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// Ty::indexed(BaseTy::Array(ty, c), RefineArgs::empty())

flux-middle/src/rty/mod.rs Outdated Show resolved Hide resolved
flux-desugar/src/desugar.rs Outdated Show resolved Hide resolved
flux-typeck/src/checker.rs Show resolved Hide resolved
flux-typeck/src/checker.rs Outdated Show resolved Hide resolved
@ranjitjhala ranjitjhala merged commit a228223 into main Dec 18, 2022
@ranjitjhala ranjitjhala deleted the slice branch December 18, 2022 22:57
@ranjitjhala
Copy link
Contributor Author

Merging this in, let me make a separate issue for the Array thing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Support slice and array indexing
2 participants