Skip to content

Commit

Permalink
bloop
Browse files Browse the repository at this point in the history
  • Loading branch information
ranjitjhala committed Nov 23, 2024
1 parent 8001e53 commit 6156c6e
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 24 deletions.
10 changes: 8 additions & 2 deletions crates/flux-refineck/src/type_env/place_ty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ impl LookupKey for Path {
pub(super) struct LookupResult<'a> {
pub ty: Ty,
pub is_strg: bool,
pub is_constant_index: bool, // doesn't feel right...
pub _is_constant_index: bool, // doesn't feel right...
cursor: Cursor,
bindings: &'a mut PlacesTree,
}
Expand Down Expand Up @@ -236,7 +236,13 @@ impl PlacesTree {
}
}
cursor.reset();
Ok(LookupResult { ty, is_strg, is_constant_index, cursor, bindings: self })
Ok(LookupResult {
ty,
is_strg,
_is_constant_index: is_constant_index,
cursor,
bindings: self,
})
}

pub(crate) fn lookup_unfolding(
Expand Down
11 changes: 0 additions & 11 deletions tests/tests/neg/surface/issue-431.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,17 +18,6 @@ fn normal(x: &RVec<f32>, w: usize) -> RVec<f32> {
res
}

#[flux::sig(fn (n: usize, centers: &mut RVec<RVec<f32>[n]>[@k], new_centers: RVec<(usize{v: v < k}, (RVec<f32>[n], usize))>))]
pub fn update_centers(
_n: usize,
centers: &mut RVec<RVec<f32>>,
new_centers: RVec<(usize, (RVec<f32>, usize))>,
) {
for (i, (x, size)) in new_centers {
centers[i] = normal(&x, size)
}
}

#[flux::sig(fn (n: usize, centers: &mut RVec<RVec<f32>[n]>[@k], new_centers: RVec<(usize{v: v < k}, (RVec<f32>, usize))>))]
pub fn update_centers_bad(
_n: usize,
Expand Down
11 changes: 0 additions & 11 deletions tests/tests/pos/surface/issue-431.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,14 +28,3 @@ pub fn update_centers(
centers[i] = normal(&x, size)
}
}

#[flux::sig(fn (n: usize, centers: &mut RVec<RVec<f32>[n]>[@k], new_centers: RVec<(usize{v: v < k}, (RVec<f32>, usize))>))]
pub fn update_centers_bad(
_n: usize,
centers: &mut RVec<RVec<f32>>,
new_centers: RVec<(usize, (RVec<f32>, usize))>,
) {
for (i, (x, size)) in new_centers {
centers[i] = normal(&x, size) //~ ERROR refinement type
}
}

0 comments on commit 6156c6e

Please sign in to comment.