Commit 7e5afceb authored by Michael Sammler's avatar Michael Sammler
Browse files

update queue with version from master

parent 4e538af3
Pipeline #43569 passed with stage
in 14 minutes and 32 seconds
This diff is collapsed.
......@@ -65,13 +65,12 @@ Section spec.
(* Definition of type [queue]. *)
Definition queue_rec : ((list type) -d> typeO) ((list type) -d> typeO) := (λ self tys,
(&own (
tyexists (λ p : loc,
(tyexists (λ p, own_constrained (&own (
struct struct_queue [@{type}
(tyfold ((λ ty x, ty @ queue_elem x) <$> tys) (place (p))) ;
(p @ (&own (null)))
])
))
(&own (place (p)))
]
)) (tyown_constraint (p) (null))))
)%I.
Typeclasses Opaque queue_rec.
......@@ -85,13 +84,12 @@ Section spec.
Lemma queue_unfold (tys : list type) :
(tys @ queue)%I @{type} (
(&own (
tyexists (λ p : loc,
(tyexists (λ p, own_constrained (&own (
struct struct_queue [@{type}
(tyfold ((λ ty x, ty @ queue_elem x) <$> tys) (place (p))) ;
(p @ (&own (null)))
])
))
(&own (place (p)))
]
)) (tyown_constraint (p) (null))))
)%I.
Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
......
......@@ -13,12 +13,11 @@ queue_elem {
} *queue_elem_t;
typedef struct [[rc::refined_by("tys: {list type}")]]
[[rc::ptr_type("queue : &own<...>")]]
[[rc::exists("p : loc")]]
[[rc::ptr_type("queue : ∃ p. own_constrained<&own<...>, tyown_constraint<p, null>>")]]
queue {
[[rc::field("tyfold<{(λ ty x, ty @ queue_elem x) <$> tys}, place<p>>")]]
queue_elem_t head;
[[rc::field("p @ &own<null>")]]
[[rc::field("&own<place<p>>")]]
queue_elem_t *tail;
} *queue_t;
......@@ -36,7 +35,6 @@ queue_t init_queue() {
[[rc::returns("{bool_decide (tys ≠ [])} @ boolean<bool_it>")]]
[[rc::ensures("own p : {tys} @ queue")]]
bool is_empty(queue_t *q) {
rc_unfold(*(*q)->tail);
return (*q)->head != NULL;
}
......@@ -58,7 +56,6 @@ void enqueue(queue_t *q, void *v) {
[[rc::returns("{maybe2 cons tys} @ optionalO<λ (ty, _). &own<ty>>")]]
[[rc::ensures("own p : {tail tys} @ queue")]]
void *dequeue(queue_t *q) {
rc_unfold(*(*q)->tail);
if ((*q)->head == NULL) {
return NULL;
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment