Commit b81bb3dd authored by Glen Mével's avatar Glen Mével
Browse files

remove some obsolete TODOs

parent 7aed832c
...@@ -3,8 +3,8 @@ From iris.base_logic Require Import invariants. ...@@ -3,8 +3,8 @@ From iris.base_logic Require Import invariants.
From cosmo.program_logic Require Export proofmode. From cosmo.program_logic Require Export proofmode.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(* This must NOT be a value since it may be open. *) (* This must NOT be a value since it may be open.
(* FIXME: this notation captures the variable "_while". *) Note: this notation captures the variable "_while". *)
Notation While cond body := Notation While cond body :=
((rec: "_while" <> := ((rec: "_while" <> :=
if: cond then if: cond then
......
...@@ -4,8 +4,8 @@ From cosmo.program_logic Require Export proofmode. ...@@ -4,8 +4,8 @@ From cosmo.program_logic Require Export proofmode.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Open Scope Z. Open Scope Z.
(* This must NOT be a value since it may be open. *) (* This must NOT be a value since it may be open.
(* FIXME: this notation captures the variable "_while". *) Note: this notation captures the variable "_while". *)
Notation While cond body := Notation While cond body :=
((rec: "_while" <> := ((rec: "_while" <> :=
if: cond then if: cond then
...@@ -565,7 +565,7 @@ Section proof. ...@@ -565,7 +565,7 @@ Section proof.
{{{ unlocked lk }}} acquire lk {{{ RET #() ; locked lk P }}} {{{ unlocked lk }}} acquire lk {{{ RET #() ; locked lk P }}}
{{{ locked lk P }}} release lk {{{ RET #() ; unlocked lk }}} {{{ locked lk P }}} release lk {{{ RET #() ; unlocked lk }}}
}}}. }}}.
Proof using PetersonG0 N. (* FIXME: Why is this required here? *) Proof using PetersonG0 N.
iIntros (Φ) "HP Post". iIntros (Φ) "HP Post".
wp_apply (make_spec with "HP"). iIntros (lk0 lk1 γ0 γ1) "(% & Hunlk0 & Hunlk1)". wp_apply (make_spec with "HP"). iIntros (lk0 lk1 γ0 γ1) "(% & Hunlk0 & Hunlk1)".
(* because we cannot index things with respect to the threads ID (0 or 1), (* because we cannot index things with respect to the threads ID (0 or 1),
......
...@@ -143,7 +143,7 @@ Section Spec. ...@@ -143,7 +143,7 @@ Section Spec.
{{{ locked P }}} release #lk {{{ RET #() ; True }}} {{{ locked P }}} release #lk {{{ RET #() ; True }}}
(locked - locked - False) (locked - locked - False)
}}}. }}}.
Proof using slockG0. (* FIXME: Why is this required here? *) Proof using slockG0.
iIntros (Φ) "HP Post". iIntros (Φ) "HP Post".
wp_apply (make_spec with "HP"). wp_apply (make_spec with "HP").
iIntros (γ lk) "#Hlock". iApply ("Post" $! lk locked γ⎤%I). iIntros (γ lk) "#Hlock". iApply ("Post" $! lk locked γ⎤%I).
......
...@@ -188,7 +188,7 @@ Section proof. ...@@ -188,7 +188,7 @@ Section proof.
{{{ locked P }}} release lk {{{ RET #() ; True }}} {{{ locked P }}} release lk {{{ RET #() ; True }}}
(locked - locked - False) (locked - locked - False)
}}}. }}}.
Proof using tlockG0 N. (* FIXME: Why is this required here? *) Proof using tlockG0 N.
iIntros (Φ) "HP Post". iIntros (Φ) "HP Post".
wp_apply (newlock_spec with "HP"). wp_apply (newlock_spec with "HP").
iIntros (lk γ) "#Hlock". iApply ("Post" $! lk (locked γ)). iIntros (lk γ) "#Hlock". iApply ("Post" $! lk (locked γ)).
...@@ -204,10 +204,3 @@ Section proof. ...@@ -204,10 +204,3 @@ Section proof.
End proof. End proof.
Typeclasses Opaque is_lock issued locked. Typeclasses Opaque is_lock issued locked.
(* TODO: copied from HeapLang *)
(*
Canonical Structure ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
{| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
*)
...@@ -194,7 +194,6 @@ Section definitions. ...@@ -194,7 +194,6 @@ Section definitions.
Definition has_length_eq : @has_length = @has_length_def := seal_eq has_length_aux. Definition has_length_eq : @has_length = @has_length_def := seal_eq has_length_aux.
End definitions. End definitions.
(* TODO: notation for mapsto predicate with and a list of values (whole arrays) *)
Notation "ℓi ↦{ q } v" := (mapsto_na i v q) Notation "ℓi ↦{ q } v" := (mapsto_na i v q)
(at level 20, q at level 50, format "ℓi ↦{ q } v") : bi_scope. (at level 20, q at level 50, format "ℓi ↦{ q } v") : bi_scope.
Notation "ℓi ↦ v" := (mapsto_na i v 1) Notation "ℓi ↦ v" := (mapsto_na i v 1)
......
Markdown is supported
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