Skip to content
Snippets Groups Projects
Verified Commit 06e7a80b authored by Lennard Gäher's avatar Lennard Gäher
Browse files

fix

parent d7e4fcfa
No related branches found
No related tags found
No related merge requests found
Pipeline #117224 failed
lib_load_paths = ["../"]
generate_dune_project = false
extra_specs = "extra_specs.v"
Section trans.
Fixpoint IteratorNextFusedTrans {Self_rt Item_rt : Type}
(attrs : traits_iterator_Iterator_spec_attrs Self_rt Item_rt)
(s1 : Self_rt) (els : list (Item_rt)) (s2 : Self_rt) : iProp Σ
:=
match els with
| [] => s1 = s2
| (e1 :: els) =>
s1',
attrs.(traits_iterator_Iterator_Next) s1 (Some e1) s1'
IteratorNextFusedTrans attrs s1' els s2
end.
(* Steps for loops with iterators:
- set a variable with the initial state in the context
(we need a special identifier for that, I guess?)
- add invariant using IteratorNextFusedTrans from the initial state to the current iterator state.
Frontend:
- identify that we have a for loop
- find the iterator variable
- add it to the set of variables we need an invariant on
- etc.
*)
(* TODO: we might need some Lithium instances to automate the SL reasoning here.
Is Next opaque for us? I guess it should unfold. Let's just see how it works.
*)
End trans.
......@@ -81,3 +81,29 @@ pub trait Iterator {
// Basically, we should have a common interface for types implementing the Iterator trait, and
// when we generate a specific instantiation, we want to instantiate that interface.
}
#[rr::export_as(core::iter::IntoIterator)]
#[rr::exists("into_iter" : "{rt_of Self} → {rt_of IntoIter}")]
pub trait IntoIterator {
/// The type of the elements being iterated over.
type Item;
/// Which kind of iterator are we turning this into?
type IntoIter: Iterator<Item = Self::Item>;
#[rr::exists("res")]
#[rr::ensures("$# res = {into_iter} ($# self)")]
#[rr::returns("res")]
fn into_iter(self) -> Self::IntoIter;
}
#[rr::instantiate("into_iter" := "id")]
impl<I> IntoIterator for I where I: Iterator {
type Item = <I as Iterator>::Item;
type IntoIter = I;
#[rr::default_spec]
fn into_iter(self) -> I {
self
}
}
From refinedrust Require Import typing.
(*
iteration state for vector:
- (index)
- remaining vector elements that will be output
- (for mut: information to resolve previous elements)
next for vec::IterMut:
it_state: (x :: remaining_els, vars)
γi,
it_state: (remaining_els, vars ++ [γi])
returns (#x, γi)
put into our generic interface:
Define type
Record VecIterMutState (T_rt : Type) := {
vec_iter_mut_state_remaining : list T_rt;
vec_iter_mut_state_vars : list gname;
}.
Refine vec::IterMut by VecIterMutState
Define an instance of Iterator,
Definition vec_iterator (T_rt : Type) := {|
iterator_state := VecIterMutState T_rt;
iterator_next s1 elem s2 :=
remaining, s1.(vec_iter_mut_state_remaining) = elem :: remaining
γi, ....
|}.
If I drop vec::IterMut:
then I get an observation of the whole vector having the vars elements
Note: iterator_next needs to be a relation, as it may allocate new ghost resources
This relation is pure, but we need to prove the reflection of it into Iris when proving the spec
Important: the class should be indexed by the state type, not by the elem type, as that is relevant for inference and avoiding ambiguity.
*)
Class Iterator (it_state : Type) (it_elem : Type) := {
iterator_next : it_state it_elem it_state Prop;
iterator_done : it_state Prop;
iterator_done_dec x : Decision (iterator_done x);
}.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment