Verified Commit e9851f64 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Add coercive subtyping

parent 2deb5e0d
......@@ -105,6 +105,12 @@ Definition ltyped `{heapG Σ}
Notation "Γ ⊨ e : A" := (ltyped Γ e A)
(at level 100, e at next level, A at level 200).
Definition lsubtyped `{heapG Σ}
(c : val) (A : lty Σ) (B : lty Σ) : iProp Σ :=
( v, A v - WP c v {{ B }})%I.
Notation "c ⊨s A <: B" := (lsubtyped c A B)
(at level 100, A, B at level 80).
(* To unfold a recursive type, we need to take a step. We thus define the
unfold operator to be the identity function. *)
Definition rec_unfold : val := λ: "x", "x".
......@@ -241,6 +247,58 @@ Section types_properties.
iEval (rewrite lty_rec_unfold /lty_car /=) in "HB". by wp_lam.
Qed.
Lemma ltyC_to_ltyped (A : ltyC Σ) (v : val) : A v - v : A.
Proof.
iIntros "#H !>" (vs) "#_ /=". by rewrite -wp_value.
Qed.
Lemma env_ltyped_empty: True env_ltyped .
Proof. exact: big_sepM2_empty'. Qed.
Lemma lsubtyped_unfold_rec (B : ltyC Σ -n> ltyC Σ) :
rec_unfold s lty_rec B <: B (lty_rec B).
Proof.
iIntros "!>" (v) "H". rewrite ltyC_to_ltyped.
iApply (ltyped_unfold v B with "H").
by iApply env_ltyped_empty.
Qed.
Definition fun_coerce (c1 c2 : val) : val :=
λ: "f" "x", c2 ("f" (c1 "x")).
Lemma lsubtyped_arr c1 c2 A1 A2 B1 B2:
c1 s B1 <: A1 -
c2 s A2 <: B2 -
fun_coerce c1 c2 s (A1 A2) <: (B1 B2).
Proof.
rewrite /fun_coerce; iIntros "#Hs1 #Hs2 !>" (v) "#HvA".
wp_pures; iIntros "!>" (w) "HwB1"; wp_pures.
iRevert "Hs1 Hs2 HvA"; iIntros "Hs1 Hs2 HvA".
wp_apply (wp_wand with "(Hs1 HwB1)"); iIntros (w1) "HwA1".
wp_apply (wp_wand with "(HvA HwA1)"); iIntros (w2) "HwA2".
wp_apply (wp_wand with "(Hs2 HwA2)"); iIntros (w3) "HwB2".
done.
Qed.
Definition prod_coerce (c1 c2 : val) : val :=
λ: "x", (c1 (Fst "x"), c2 (Snd "x")).
Lemma lsubtyped_prod c1 c2 A1 A2 B1 B2:
c1 s A1 <: B1 -
c2 s A2 <: B2 -
prod_coerce c1 c2 s (A1 * A2) <: (B1 * B2).
Proof.
rewrite /prod_coerce; iIntros "#Hs1 #Hs2 !>" (v).
iDestruct 1 as (v1 v2 ->) "[HvA1 HvA2]".
iRevert "Hs1 Hs2"; iIntros "Hs1 Hs2".
wp_pures.
wp_apply (wp_wand with "(Hs2 HvA2)"); iIntros (w2) "HwB2"; wp_pures.
wp_apply (wp_wand with "(Hs1 HvA1)"); iIntros (w1) "HwB1"; wp_pures.
iEval (info_eauto).
Show.
(iEval (rewrite /lty_car /=)); eauto.
Qed.
Lemma ltyped_tlam Γ e C : ( A, Γ e : C A) - Γ (λ: <>, e) : A, C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=". wp_pures.
......
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