Skip to content

Commit b1d5d2b

Browse files
KaptchKaptch
committed
exceptions example upstream
1 parent 2453bbf commit b1d5d2b

3 files changed

Lines changed: 1010 additions & 965 deletions

File tree

‎theories/effects/exceptions.v‎

Lines changed: 70 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -68,11 +68,16 @@ Module Exc (Errors : ExcSig).
6868
Definition exceptE := @[regE;popE;throwE].
6969

7070
(** Register a handler : Push the handler and current context on the stack **)
71-
Definition reify_reg X `{Cofe X} : excO * (laterO X -n> laterO X) * (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X) → option (laterO X * (stateF ♯ X)) :=
72-
λ '(e, h, b, σ, k), Some (b, (e,h,k)::σ).
71+
Definition reify_reg X `{Cofe X} :
72+
excO * (laterO X -n> laterO X) * (laterO X)
73+
* (stateF ♯ X) * (laterO X -n> laterO X) →
74+
option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
75+
λ '(e, h, b, σ, k), Some (b, (e,h,k)::σ, []).
7376

74-
#[export] Instance reify_reg_ne X `{Cofe X}: NonExpansive (reify_reg X : excO * (laterO X -n> laterO X) * (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X) → option (laterO X * (stateF ♯ X))
75-
).
77+
#[export] Instance reify_reg_ne X `{Cofe X}
78+
: NonExpansive (reify_reg X : excO * (laterO X -n> laterO X)
79+
* (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X)
80+
→ option (laterO X * (stateF ♯ X) * listO (laterO X))).
7681
Proof.
7782
solve_proper_prepare.
7883
destruct x as [[[[? ?] ?] ?] ?].
@@ -83,16 +88,21 @@ Module Exc (Errors : ExcSig).
8388
Qed.
8489

8590
(** Unregister a handler : Remove the topmost handler, restore the ambient context from when it was registered **)
86-
Definition reify_pop X `{Cofe X} : excO * (stateF ♯ X) * (unitO -n> laterO X) → option (laterO X * (stateF ♯ X)) :=
91+
Definition reify_pop X `{Cofe X} :
92+
excO * (stateF ♯ X) * (unitO -n> laterO X)
93+
→ option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
8794
λ '(err, σ, k), match σ with
8895
| [] => None
8996
| (err', h, k')::σ' =>
9097
(if (eq_dec err err')
91-
then Some (k' (k ()), σ')
92-
else None) end.
98+
then Some (k' (k ()), σ', [])
99+
else None)
100+
end.
93101

94-
#[export] Instance reify_pop_ne X `{Cofe X}: NonExpansive (reify_pop X :
95-
excO * (stateF ♯ X) * (unitO -n> laterO X) → option (laterO X * (stateF ♯ X))).
102+
#[export] Instance reify_pop_ne X `{Cofe X} :
103+
NonExpansive (reify_pop X :
104+
excO * (stateF ♯ X) * (unitO -n> laterO X)
105+
→ option (laterO X * (stateF ♯ X) * listO (laterO X))).
96106
Proof.
97107
intros n [[e σ] k] [[e' σ'] k'] Hequiv.
98108
rewrite pair_dist in Hequiv.
@@ -113,7 +123,8 @@ Module Exc (Errors : ExcSig).
113123
+ reflexivity.
114124
Qed.
115125

116-
Fixpoint _cut_when {A : ofe} (p : (A -n> boolO)) (l : listO A) : optionO (A * listO A)%type :=
126+
Fixpoint _cut_when {A : ofe} (p : (A -n> boolO)) (l : listO A) :
127+
optionO (A * listO A)%type :=
117128
match l with
118129
| [] => None
119130
| x::t => if p x then Some (x, t) else _cut_when p t
@@ -189,14 +200,19 @@ Module Exc (Errors : ExcSig).
189200
Qed.
190201

191202
(** Raise an error : Find the most recent handler handling this error and remove all handlers registered after it from the stack then invoke the handler inside the context from when it was registered **)
192-
Definition reify_throw X `{Cofe X} : (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X) → option (laterO X * (stateF ♯ X)) :=
203+
Definition reify_throw X `{Cofe X} :
204+
(excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X)
205+
→ option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
193206
λ '(x, σ, _), let (err,v) := x in
194207
match cut_when (aux err) σ with
195208
| None => None
196-
| Some (_, h, k, σ') => Some (k (h v), σ')
209+
| Some (_, h, k, σ') => Some (k (h v), σ', [])
197210
end.
198211

199-
#[export] Instance reify_throw_ne X `{Cofe X} : NonExpansive (reify_throw X : (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X) → option (laterO X * (stateF ♯ X))).
212+
#[export] Instance reify_throw_ne X `{Cofe X} :
213+
NonExpansive (reify_throw X :
214+
(excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X)
215+
→ option (laterO X * (stateF ♯ X) * listO (laterO X))).
200216
Proof.
201217
solve_proper_prepare.
202218
destruct x as [[[e v] σ] k].
@@ -222,8 +238,7 @@ Module Exc (Errors : ExcSig).
222238
* rewrite HEq.
223239
exact (IHσ σ'' Hσ'').
224240
* rewrite Herr -He. reflexivity.
225-
Qed.
226-
241+
Qed.
227242

228243
Canonical Structure reify_exc : sReifier CtxDep.
229244
Proof.
@@ -242,16 +257,19 @@ Module Exc (Errors : ExcSig).
242257
Context {subEff0 : subEff exceptE Eff}.
243258
Context {SubOfe0 : SubOfe unitO A}.
244259
Notation IT := (IT Eff A).
245-
Notation ITV := (ITV Eff A).
246-
260+
Notation ITV := (ITV Eff A).
247261

248262
Program Definition _REG : excO -n> (laterO IT -n> laterO IT) -n> laterO IT -n> IT :=
249-
λne e h b, Vis (E:=Eff) (subEff_opid (inl ())) (subEff_ins (F:=exceptE) (op:=(inl ())) (e,h,b)) ((λne x, x) ◎ (subEff_outs (F:=exceptE) (op:=(inl ())))^-1).
263+
λne e h b, Vis (E:=Eff) (subEff_opid (inl ()))
264+
(subEff_ins (F:=exceptE) (op:=(inl ())) (e,h,b))
265+
((λne x, x) ◎ (subEff_outs (F:=exceptE) (op:=(inl ())))^-1).
250266
Solve All Obligations with solve_proper.
251267

252268

253269
Program Definition _POP : excO -n> IT :=
254-
λne e, Vis (E:=Eff) (subEff_opid (inr (inl ()))) (subEff_ins (F:=exceptE) (op:=(inr(inl ()))) e) ((λne _, Next $ Ret ()) ◎ (subEff_outs (F:=exceptE) (op:=(inr(inl ()))))^-1).
270+
λne e, Vis (E:=Eff) (subEff_opid (inr (inl ())))
271+
(subEff_ins (F:=exceptE) (op:=(inr(inl ()))) e)
272+
((λne _, Next $ Ret ()) ◎ (subEff_outs (F:=exceptE) (op:=(inr(inl ()))))^-1).
255273
Solve All Obligations with solve_proper.
256274

257275
Program Definition CATCH : excO -n> (laterO IT -n> laterO IT) -n> IT -n> IT :=
@@ -269,7 +287,7 @@ Module Exc (Errors : ExcSig).
269287
Qed.
270288
Next Obligation.
271289
solve_proper_prepare.
272-
repeat f_equiv.
290+
apply get_val_ne.
273291
solve_proper.
274292
Qed.
275293
Next Obligation.
@@ -282,12 +300,16 @@ Module Exc (Errors : ExcSig).
282300
Qed.
283301
Next Obligation.
284302
solve_proper_prepare.
285-
repeat f_equiv; solve_proper.
303+
repeat f_equiv; first done.
304+
apply get_val_ne.
305+
solve_proper.
286306
Qed.
287307

288308
Program Definition _THROW : excO -n> laterO IT -n> IT :=
289309
λne e v,
290-
Vis (E:=Eff) (subEff_opid (inr (inr (inl ())))) (subEff_ins (F:=exceptE) (op:=(inr(inr(inl ())))) (e,v)) (λne x, Empty_setO_rec _ ((subEff_outs (F:=exceptE) (op:=(inr(inr(inl ())))))^-1 x)).
310+
Vis (E:=Eff) (subEff_opid (inr (inr (inl ()))))
311+
(subEff_ins (F:=exceptE) (op:=(inr(inr(inl ())))) (e,v))
312+
(λne x, Empty_setO_rec _ ((subEff_outs (F:=exceptE) (op:=(inr(inr(inl ())))))^-1 x)).
291313
Next Obligation.
292314
solve_proper_prepare.
293315
destruct ((subEff_outs ^-1) x).
@@ -301,7 +323,7 @@ Module Exc (Errors : ExcSig).
301323
Next Obligation.
302324
Proof.
303325
solve_proper_prepare.
304-
repeat f_equiv.
326+
apply get_val_ne.
305327
solve_proper.
306328
Qed.
307329

@@ -318,10 +340,11 @@ Module Exc (Errors : ExcSig).
318340
Context {SubOfe1 : SubOfe natO R}.
319341
Notation IT := (IT F R).
320342
Notation ITV := (ITV F R).
321-
Context `{!invGS Σ, !stateG rs R Σ}.
343+
Context `{!gitreeGS_gen rs R Σ}.
322344
Notation iProp := (iProp Σ).
323345

324-
Lemma wp_reg (σ : stateF ♯ IT) (err : excO) (h : laterO IT -n> laterO IT) (k : IT -n> IT) {Hk : IT_hom k} b β s Φ :
346+
Lemma wp_reg (σ : stateF ♯ IT) (err : excO) (h : laterO IT -n> laterO IT) (k : IT -n> IT)
347+
{Hk : IT_hom k} b β s Φ :
325348
b ≡ Next β →
326349
has_substate σ -∗
327350
▷ (£ 1 -∗ has_substate ((err, h, laterO_map k) :: σ) -∗ WP@{rs} β @ s {{ β, Φ β }}) -∗
@@ -330,17 +353,22 @@ Module Exc (Errors : ExcSig).
330353
iIntros (Hβ) "Hσ Ha".
331354
unfold _REG. simpl.
332355
rewrite hom_vis.
333-
iApply (wp_subreify_ctx_dep with "Hσ").
356+
iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ _ _ _ _ _ [] with "Hσ").
334357
- simpl.
335358
rewrite /ccompose /compose /=.
336-
repeat f_equiv.
359+
f_equiv.
360+
split; simpl; last reflexivity.
361+
split; simpl; first reflexivity.
337362
apply cons_equiv; last done.
338363
apply pair_equiv.
339364
split; first done.
340365
trans (laterO_map k : laterO IT -n> laterO IT); last reflexivity.
341366
intro. simpl. f_equiv. apply ofe_iso_21.
342-
- done.
343-
- iAssumption.
367+
- apply Hβ.
368+
- rewrite /weakestpre.wptp big_sepL2_nil.
369+
iNext. iIntros "H1 H2".
370+
iSplit; last done.
371+
iApply ("Ha" with "H1 H2").
344372
Qed.
345373

346374
Lemma wp_pop (σ σ': stateF ♯ IT) (err : excO) h k (k' : IT -n> IT) {Hk' : IT_hom k'} β Φ :
@@ -359,13 +387,16 @@ Module Exc (Errors : ExcSig).
359387
destruct (eq_dec err err); last done.
360388
reflexivity.
361389
- exact Hβ.
362-
- done.
390+
- rewrite /weakestpre.wptp big_sepL2_nil.
391+
iNext. iIntros "H1 H2".
392+
iSplit; last done.
393+
iApply ("Ha" with "H1 H2").
363394
Qed.
364395

365396
Lemma wp_catch_v σ (v : IT) Φ err h (k : IT -n> IT) {Hk : IT_hom k} `{!AsVal v} β :
366397
k v ≡ β →
367398
has_substate σ -∗
368-
▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} β {{ Φ }}) -∗
399+
▷ (£ 2 -∗ has_substate σ -∗ WP@{rs} β {{ Φ }}) -∗
369400
WP@{rs} k (CATCH err h v) {{ Φ }}.
370401
Proof.
371402
iIntros (Hβ) "Hσ Ha".
@@ -377,7 +408,9 @@ Module Exc (Errors : ExcSig).
377408
iApply (wp_pop with "Hσ").
378409
- reflexivity.
379410
- simpl. unfold later_map. simpl. rewrite get_val_ret. simpl. rewrite Hβ. reflexivity.
380-
- iAssumption.
411+
- iNext. iIntros "H1 H2".
412+
iApply ("Ha" with "[H1 Hcr] H2").
413+
iSplitL "H1"; done.
381414
Qed.
382415

383416
Global Instance throw_hom {err : exc} : IT_hom (THROW err : IT -n> IT).
@@ -387,8 +420,7 @@ Module Exc (Errors : ExcSig).
387420
- rewrite hom_vis. do 3 f_equiv. intro. simpl. done.
388421
- by rewrite hom_err.
389422
Qed.
390-
391-
423+
392424
Definition wp_throw (σ pre post : stateF ♯ IT) (err : excO) (h k : laterO IT -n> laterO IT) (k' : IT -n> IT) {Hk : IT_hom k'} (v : IT) `{!AsVal v} β Φ :
393425
(Forall (λ '(err',_,_), err <> err') pre) →
394426
k (h (Next v)) ≡ Next β →
@@ -413,7 +445,10 @@ Module Exc (Errors : ExcSig).
413445
destruct x as [[err' _] _] . simpl in *.
414446
destruct (eq_dec err err'); done.
415447
- exact Hβ.
416-
- iAssumption.
448+
- iNext. iIntros "H1 H2".
449+
rewrite /weakestpre.wptp big_sepL2_nil.
450+
iSplit; last done.
451+
iApply ("Ha" with "H1 H2").
417452
Qed.
418453

419454
Lemma wp_catch_throw σ (v : IT) `{!AsVal v} (k k': IT -n> IT) {Hk : IT_hom k} {Hk' : IT_hom k'} Φ err (h : laterO IT -n> laterO IT) β :

0 commit comments

Comments
 (0)