Commit 7a810882 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make levels of judgments consistent.

parent c242af05
......@@ -35,47 +35,47 @@ Section compatibility.
by iApply wp_value.
Qed.
Lemma Val_sem_typed Γ v A : ( v : A) - Γ v : A.
Lemma Val_sem_typed Γ v A : v : A - Γ v : A.
Proof.
iIntros "#Hv" (vs) "!# #HΓ /=".
iApply wp_value. iApply "Hv".
Qed.
Lemma Pair_sem_typed Γ e1 e2 A1 A2 :
(Γ e1 : A1) - (Γ e2 : A2) - Γ (e1,e2) : A1 * A2.
Γ e1 : A1 - Γ e2 : A2 - Γ (e1,e2) : A1 * A2.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA2".
wp_apply (wp_wand with "(H1 [//])"); iIntros (w1) "#HA1".
wp_pures. iExists w1, w2. auto.
Qed.
Lemma Fst_sem_typed Γ e A1 A2 : (Γ e : A1 * A2) - Γ Fst e : A1.
Lemma Fst_sem_typed Γ e A1 A2 : Γ e : A1 * A2 - Γ Fst e : A1.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
Lemma Snd_sem_typed Γ e A1 A2 : (Γ e : A1 * A2) - Γ Snd e : A2.
Lemma Snd_sem_typed Γ e A1 A2 : Γ e : A1 * A2 - Γ Snd e : A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w).
iDestruct 1 as (w1 w2 ->) "[??]". by wp_pures.
Qed.
Lemma InjL_sem_typed Γ e A1 A2 : (Γ e : A1) - Γ InjL e : A1 + A2.
Lemma InjL_sem_typed Γ e A1 A2 : Γ e : A1 - Γ InjL e : A1 + A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iLeft. iExists w. auto.
Qed.
Lemma InjR_sem_typed Γ e A1 A2 : (Γ e : A2) - Γ InjR e : A1 + A2.
Lemma InjR_sem_typed Γ e A1 A2 : Γ e : A2 - Γ InjR e : A1 + A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HA".
wp_pures. iRight. iExists w. auto.
Qed.
Lemma Case_sem_typed Γ e e1 e2 A1 A2 B :
(Γ e : A1 + A2) - (Γ e1 : A1 B) - (Γ e2 : A2 B) -
Γ e : A1 + A2 - Γ e1 : (A1 B) - Γ e2 : (A2 B) -
Γ Case e e1 e2 : B.
Proof.
iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
......@@ -87,8 +87,8 @@ Section compatibility.
Qed.
Lemma Rec_sem_typed Γ f x e A1 A2 :
(binder_insert f (A1 A2)%sem_ty (binder_insert x A1 Γ) e : A2) -
Γ (rec: f x := e) : A1 A2.
binder_insert f (A1 A2)%sem_ty (binder_insert x A1 Γ) e : A2 -
Γ (rec: f x := e) : (A1 A2).
Proof.
iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH".
iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
......@@ -97,7 +97,7 @@ Section compatibility.
Qed.
Lemma App_sem_typed Γ e1 e2 A1 A2 :
(Γ e1 : A1 A2) - (Γ e2 : A1) - Γ e1 e2 : A2.
Γ e1 : (A1 A2) - Γ e2 : A1 - Γ e1 e2 : A2.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w) "#HA1".
......@@ -115,7 +115,7 @@ Section compatibility.
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iApply ("HB" $! A).
Qed.
Lemma Pack_sem_typed Γ e C A : (Γ e : C A) - Γ e : A, C A.
Lemma Pack_sem_typed Γ e C A : Γ e : C A - Γ e : A, C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (w) "#HB". by iExists A.
......@@ -132,7 +132,7 @@ Section compatibility.
auto.
Qed.
Lemma Alloc_sem_typed Γ e A : (Γ e : A) - Γ ref e : ref A.
Lemma Alloc_sem_typed Γ e A : Γ e : A - Γ ref e : ref A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w) "HA".
......@@ -141,7 +141,7 @@ Section compatibility.
{ iExists w. iFrame. }
iModIntro. iExists l; auto.
Qed.
Lemma Load_sem_typed Γ e A : (Γ e : ref A) - Γ ! e : A.
Lemma Load_sem_typed Γ e A : Γ e : ref A - Γ ! e : A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_bind (subst_map _ e). iApply (wp_wand with "(H [//])"); iIntros (w).
......@@ -149,7 +149,7 @@ Section compatibility.
iInv (tyN.@l) as (v) "[>Hl HA]". wp_load. eauto 10.
Qed.
Lemma Store_sem_typed Γ e1 e2 A :
(Γ e1 : ref A) - (Γ e2 : A) - Γ (e1 <- e2) : ().
Γ e1 : ref A - Γ e2 : A - Γ (e1 <- e2) : ().
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA".
......@@ -157,7 +157,7 @@ Section compatibility.
iInv (tyN.@l) as (v) "[>Hl _]". wp_store. eauto 10.
Qed.
Lemma FAA_sem_typed Γ e1 e2 :
(Γ e1 : ref sem_ty_int) - (Γ e2 : sem_ty_int) - Γ FAA e1 e2 : sem_ty_int.
Γ e1 : ref sem_ty_int - Γ e2 : sem_ty_int - Γ FAA e1 e2 : sem_ty_int.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w2); iDestruct 1 as (n) "->".
......@@ -167,7 +167,8 @@ Section compatibility.
Qed.
Lemma CmpXchg_sem_typed Γ A e1 e2 e3 :
SemTyUnboxed A
(Γ e1 : ref A) - (Γ e2 : A) - (Γ e3 : A) - Γ CmpXchg e1 e2 e3 : A * sem_ty_bool.
Γ e1 : ref A - Γ e2 : A - Γ e3 : A -
Γ CmpXchg e1 e2 e3 : A * sem_ty_bool.
Proof.
intros. iIntros "#H1 #H2 #H3" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H3 [//])"); iIntros (w3) "HA3".
......@@ -179,14 +180,14 @@ Section compatibility.
Qed.
Lemma UnOp_sem_typed Γ e op A B :
SemTyUnOp op A B (Γ e : A) - Γ UnOp op e : B.
SemTyUnOp op A B Γ e : A - Γ UnOp op e : B.
Proof.
intros ?. iIntros "#H" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H [//])"); iIntros (v) "#HA".
iDestruct (sem_ty_un_op with "HA") as (w ?) "#HB". by wp_unop.
Qed.
Lemma BinOp_sem_typed Γ e1 e2 op A1 A2 B :
SemTyBinOp op A1 A2 B (Γ e1 : A1) - (Γ e2 : A2) - Γ BinOp op e1 e2 : B.
SemTyBinOp op A1 A2 B Γ e1 : A1 - Γ e2 : A2 - Γ BinOp op e1 e2 : B.
Proof.
intros. iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (v2) "#HA2".
......@@ -195,7 +196,7 @@ Section compatibility.
Qed.
Lemma If_sem_typed Γ e e1 e2 B :
(Γ e : sem_ty_bool) - (Γ e1 : B) - (Γ e2 : B) -
Γ e : sem_ty_bool - Γ e1 : B - Γ e2 : B -
Γ (if: e then e1 else e2) : B.
Proof.
iIntros "#H #H1 #H2" (vs) "!# #HΓ /=".
......@@ -203,7 +204,7 @@ Section compatibility.
wp_apply (wp_wand with "(H [//])"); iIntros (w). iDestruct 1 as ([]) "->"; by wp_if.
Qed.
Lemma Fork_sem_typed Γ e : (Γ e : ()) - Γ Fork e : ().
Lemma Fork_sem_typed Γ e : Γ e : () - Γ Fork e : ().
Proof.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply wp_fork; last done. by iApply (wp_wand with "(H [//])").
......@@ -217,20 +218,20 @@ Section compatibility.
Proof. by iExists n. Qed.
Lemma PairV_sem_typed v1 v2 τ1 τ2 :
( v1 : τ1) - ( v2 : τ2) -
v1 : τ1 - v2 : τ2 -
PairV v1 v2 : (τ1 * τ2).
Proof. iIntros "#H1 #H2". iExists v1, v2. auto. Qed.
Lemma InjLV_sem_typed v τ1 τ2 :
( v : τ1) -
v : τ1 -
InjLV v : (τ1 + τ2).
Proof. iIntros "H". iLeft. auto. Qed.
Lemma InjRV_sem_typed v τ1 τ2 :
( v : τ2) -
v : τ2 -
InjRV v : (τ1 + τ2).
Proof. iIntros "H". iRight. auto. Qed.
Lemma RecV_sem_typed f x e A B :
(binder_insert f (A B)%sem_ty (binder_insert x A ) e : B) -
binder_insert f (A B)%sem_ty (binder_insert x A ) e : B -
RecV f x e : (A B).
Proof.
iIntros "#H". iLöb as "IH".
......
......@@ -31,13 +31,13 @@ Definition sem_typed `{heapG Σ}
tc_opaque ( vs, env_sem_typed Γ vs - WP subst_map vs e {{ A }})%I.
Instance: Params (@sem_typed) 2 := {}.
Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
(at level 100, e at next level, A at level 200).
(at level 74, e, A at next level).
Definition sem_val_typed `{heapG Σ} (v : val) (A : sem_ty Σ) : iProp Σ :=
tc_opaque (A v).
Instance: Params (@sem_val_typed) 3 := {}.
Notation "⊨ᵥ v : A" := (sem_val_typed v A)
(at level 20, v at next level, A at level 200).
(at level 20, v, A at next level).
Arguments sem_val_typed : simpl never.
(** A few useful lemmas about the semantic typing judgment. The first
......
......@@ -139,7 +139,7 @@ where "Γ ⊢ₜ e : τ" := (typed Γ e τ)
and "⊢ᵥ v : τ" := (val_typed v τ).
Lemma Lam_typed Γ x e τ1 τ2 :
(binder_insert x τ1 Γ e : τ2)
binder_insert x τ1 Γ e : τ2
Γ (λ: x, e) : TArr τ1 τ2.
Proof.
intros He.
......@@ -149,7 +149,7 @@ Proof.
Qed.
Lemma LamV_typed x e τ1 τ2 :
(binder_insert x τ1 e : τ2)
binder_insert x τ1 e : τ2
(λ: x, e) : TArr τ1 τ2.
Proof.
intros He.
......@@ -159,8 +159,8 @@ Proof.
Qed.
Lemma Let_typed Γ x e1 e2 τ1 τ2 :
(Γ e1 : τ1)
(binder_insert x τ1 Γ e2 : τ2)
Γ e1 : τ1
binder_insert x τ1 Γ e2 : τ2
Γ (let: x := e1 in e2) : τ2.
Proof.
intros He1 He2.
......@@ -170,8 +170,8 @@ Proof.
Qed.
Lemma Seq_typed Γ e1 e2 τ1 τ2 :
(Γ e1 : τ1)
(Γ e2 : τ2)
Γ e1 : τ1
Γ e2 : τ2
Γ (e1;; e2) : τ2.
Proof.
intros He1 He2.
......
......@@ -8,7 +8,7 @@ Section unsafe.
Definition unsafe_pure : val := λ: <>,
if: #true then #13 else #13 #37.
Lemma sem_typed_unsafe_pure : unsafe_pure : () sem_ty_int.
Lemma sem_typed_unsafe_pure : unsafe_pure : (() sem_ty_int).
Proof.
iIntros (vs) "!# HΓ"; simpl.
iApply wp_value.
......@@ -23,7 +23,7 @@ Section unsafe.
Definition unsafe_ref : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l".
Lemma sem_typed_unsafe_ref : unsafe_ref : () sem_ty_bool.
Lemma sem_typed_unsafe_ref : unsafe_ref : (() sem_ty_bool).
Proof.
iIntros (vs) "!# HΓ"; simpl.
iApply wp_value.
......@@ -44,7 +44,7 @@ Section unsafe.
(λ: <>, assert: !"l" #0)).
Lemma sem_typed_unsafe_ref_ne_0 :
unsafe_ref_ne_0 : () (sem_ty_int ()) * (() ()).
unsafe_ref_ne_0 : (() (sem_ty_int ()) * (() ())).
Proof.
iIntros (vs) "!# HΓ"; simpl.
iApply wp_value.
......@@ -93,7 +93,7 @@ Section unsafe.
λ: <>, let: "l" := ref #0 in λ: <>, "l" <- #true;; !"l".
Lemma sem_typed_unsafe_ref_reuse `{two_stateG Σ}:
unsafe_ref_reuse : () (() sem_ty_bool).
unsafe_ref_reuse : (() (() sem_ty_bool)).
Proof.
iIntros (vs) "!# HΓ"; simpl.
iApply wp_value.
......
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