Commit 10183147 authored by Ralf Jung's avatar Ralf Jung
Browse files

bump Iris, fix for default removal

parent 793688f4
Pipeline #9120 failed with stage
in 12 minutes and 58 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-17.0.0aeb4cdc") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-05-24.0.3bed085d") | (= "dev") }
]
......@@ -265,7 +265,7 @@ Proof.
by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
Qed.
Lemma option_updateP' (P : A Prop) x :
x ~~>: P Some x ~~>: λ my, default False my P.
x ~~>: P Some x ~~>: λ my, from_option P False my.
Proof. eauto using option_updateP. Qed.
Lemma option_update x y : x ~~> y Some x ~~> Some y.
Proof.
......
......@@ -93,7 +93,7 @@ Section delayed_lang.
delayed_expr delayed_state delayed_expr delayed_state option (delayed_expr) Prop :=
| base_step e p σ e' p' σ' ef pf: prim_step e σ e' σ' ef
delayed_prim_step (e, p) σ (e', p') σ'
(default None ef (λ e, Some (e, pf)))
(from_option (λ e, Some (e, pf)) None ef)
| delay_step (e: expr L) p σ e p': plt p' p delayed_prim_step (e, p) σ (e, p') σ None.
Lemma delayed_to_of_val: v, delayed_to_val (delayed_of_val v) = Some v.
......@@ -189,7 +189,7 @@ Section delayed_lang.
(map erase_expr (c.1), c.2).
Lemma erase_prim_step e e' ef' s s':
prim_step (erase_expr e) s (erase_expr e') s' (default None ef' (λ ef, Some (erase_expr ef)))
prim_step (erase_expr e) s (erase_expr e') s' (from_option (λ ef, Some (erase_expr ef)) None ef')
delayed_prim_step e s e' s' ef'.
Proof.
destruct e as (e & p).
......@@ -255,8 +255,8 @@ Section delayed_lang.
nth i (map snd (fst c)) (proj1_sig mini).
Lemma erase_option_list ef p:
map erase_expr (option_list (default None ef (λ e : expr L, Some (e, p)))) =
option_list (default None ef Some).
map erase_expr (option_list (from_option (λ e : expr L, Some (e, p)) None ef)) =
option_list (from_option Some None ef).
Proof.
destruct ef; simpl; auto.
Qed.
......@@ -586,4 +586,4 @@ Section delayed_lang.
- apply ae_ev_estep_intro_all; eauto using delayed_ae_estep, delayed_some_ev_estep.
Qed.
End delayed_lang.
\ No newline at end of file
End delayed_lang.
......@@ -14,7 +14,7 @@ Implicit Types v : val.
Implicit Types e : expr.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Notation wp_fork ef := (default emp ef (flip (wp ) (λ _, uPred_stopped)))%I.
Notation wp_fork ef := (from_option (flip (wp ) (λ _, uPred_stopped)) emp ef)%I.
Lemma wp_ectx_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
......
......@@ -17,7 +17,7 @@ Implicit Types σ : state Λ.
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ iProp Λ Σ.
Notation wp_fork ef := (default emp ef (flip (wp ) (λ _, upred.uPred_stopped)))%I.
Notation wp_fork ef := (from_option (flip (wp ) (λ _, upred.uPred_stopped)) emp ef)%I.
Lemma wp_lift_step E1 E2 Φ e1 :
E2 E1 to_val e1 = None
......
......@@ -38,7 +38,7 @@ Section delayed_lang.
delayed_expr delayed_state delayed_expr delayed_state option (delayed_expr) Prop :=
| base_step e σ e' σ' ef:
prim_step e σ e' σ' ef
delayed_prim_step (e, 0) σ (e', max) σ' (default None ef (λ e, Some (e, fresh_delay e)))
delayed_prim_step (e, 0) σ (e', max) σ' (from_option (λ e, Some (e, fresh_delay e)) None ef)
| delay_step e d σ: delayed_prim_step (e, S d) σ (e, d) σ None.
Lemma delayed_to_of_val: v, delayed_to_val (delayed_of_val v) = Some v.
......@@ -100,20 +100,6 @@ Section delayed_lang.
Definition erase_expr (e: delayed_expr) := fst e.
Definition erase_cfg (c: cfg delayed_lang) : cfg L :=
(map erase_expr (c.1), c.2).
(*
Lemma erase_prim_step e e' ef' s s':
prim_step (erase_expr e) s (erase_expr e') s' (default None ef' (λ ef, Some (erase_expr ef)))
delayed_prim_step e s e' s' ef'.
Proof.
destruct e as (e & p).
destruct e' as (e' & p').
destruct ef' as [(ef&pf)|]; simpl; intros.
- specialize (base_step e s e' s' (Some ef)); auto.
simpl.
- specialize (base_step e p s e' p' s' None p); auto.
Qed.
*)
Lemma map_cons_inv {A B}:
b (lb: list B) (l: list A) (f: A B),
......@@ -188,8 +174,8 @@ Section delayed_lang.
nth i (map snd (fst c)) 0.
Lemma erase_option_list ef p:
map erase_expr (option_list (default None ef (λ e : expr L, Some (e, p)))) =
option_list (default None ef Some).
map erase_expr (option_list (from_option (λ e : expr L, Some (e, p)) None ef)) =
option_list (from_option Some None ef).
Proof.
destruct ef; simpl; auto.
Qed.
......@@ -527,7 +513,7 @@ Section delayed_lang.
intros Hdec e σ. destruct e as (e&[|d]).
* edestruct (Hdec e σ) as [(t&Hstep)|Hn].
** left. destruct t as ((e'&σ')&ef').
exists ((e', max), σ', (default None ef' (λ e, Some (e, fresh_delay e)))).
exists ((e', max), σ', (from_option (λ e, Some (e, fresh_delay e)) None ef')).
econstructor; eauto.
** right. intros (e'&σ'&ef'&Hstep).
inversion Hstep. eapply Hn. do 3 eexists. eauto.
......
......@@ -106,7 +106,7 @@ Proof.
eapply (nsteps_l _ _ _ ((fill K (fst y), Kd), snd y)); eauto.
** rewrite /prim_step_nofork. simpl.
replace (None: option (delayed_expr _)) with
(default None None (λ e, Some (e, @fresh_delay (ectx_lang expr) Fd e))) by auto.
(from_option (λ e, Some (e, @fresh_delay (ectx_lang expr) Fd e)) None None) by auto.
econstructor; eauto using fill_step.
** destruct n as [| n].
*** simpl. simpl.
......@@ -125,7 +125,7 @@ Proof.
econstructor; eauto.
rewrite /prim_step_nofork. simpl.
replace (None: option (delayed_expr _)) with
(default None None (λ e, Some (e, @fresh_delay (ectx_lang expr) Kd e))) by auto.
(from_option (λ e, Some (e, @fresh_delay (ectx_lang expr) Kd e)) None None) by auto.
econstructor.
Qed.
......
......@@ -1292,7 +1292,7 @@ Qed.
Lemma refine_step_disjoint_all_threads' r1 r2 r1':
r1 r2 r1 ## r2 r1 r1' r2 ## r1'
( i, (i < default 0 (last (cfgs (r1 r2))) (length fst)) i (tids r1) (tids r2))
( i, (i < from_option (length fst) 0 (last (cfgs (r1 r2)))) i (tids r1) (tids r2))
cs0 c0 c' csext isext,
(cfgs (r1 r2) = cs0 ++ [c0])
......
......@@ -516,9 +516,9 @@ Qed.
*)
Qed.
Lemma default_id_op {M M': ucmraT} (a b: option M) (Pf: M = M'):
default (a b) (ucmra_transport Pf)
default a (ucmra_transport Pf) default b (ucmra_transport Pf).
Lemma from_option_id_op {M M': ucmraT} (a b: option M) (Pf: M = M'):
from_option (ucmra_transport Pf) (a b)
from_option (ucmra_transport Pf) a from_option (ucmra_transport Pf) b.
Proof.
destruct a, b; simpl;
rewrite ?ucmra_transport_op ?right_id ?left_id; auto.
......@@ -1183,7 +1183,7 @@ Qed.
Qed.
Lemma fold_max_is_last_cfg r:
r
default 0 (last (cfgs sΛ K (validity_car r))) (length fst) =
from_option (length fst) 0 (last (cfgs sΛ K (validity_car r))) =
fold_left Init.Nat.max (map (length fst) (cfgs sΛ K (validity_car r))) 0.
Proof.
destruct r as [r Hval Hprf].
......
......@@ -31,7 +31,7 @@ Program Definition wp_pre
r2 r2',
wsat k (E Ef) σ2 (r2 r2' rf)
wp E e2 Φ k r2
default True ef (λ ef, wp ef (cconst True%I) k r2'))) |}.
from_option (λ ef, wp ef (cconst True%I) k r2') True ef)) |}.
Next Obligation.
intros wp E e1 Φ n r1 r2 Hwp [r3 Hr2] k Ef σ1 rf ??.
rewrite (dist_le _ _ _ _ Hr2); last lia. intros Hws.
......
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