Commit 798043e4 authored by Dan Frumin's avatar Dan Frumin

Add exsitentials to the context typings

parent 514a9059
...@@ -2,9 +2,17 @@ From iris_logrel.F_mu_ref_conc Require Export fundamental_binary. ...@@ -2,9 +2,17 @@ From iris_logrel.F_mu_ref_conc Require Export fundamental_binary.
From iris.proofmode Require Import tactics classes. From iris.proofmode Require Import tactics classes.
Inductive ctx_item := Inductive ctx_item :=
(* λ-rec *)
| CTX_Rec (f x: binder) | CTX_Rec (f x: binder)
| CTX_AppL (e2 : expr) | CTX_AppL (e2 : expr)
| CTX_AppR (e1 : expr) | CTX_AppR (e1 : expr)
(* Bin op *)
| CTX_BinOpL (op : binop) (e2 : expr)
| CTX_BinOpR (op : binop) (e1 : expr)
(* If *)
| CTX_IfL (e1 : expr) (e2 : expr)
| CTX_IfM (e0 : expr) (e2 : expr)
| CTX_IfR (e0 : expr) (e1 : expr)
(* Products *) (* Products *)
| CTX_PairL (e2 : expr) | CTX_PairL (e2 : expr)
| CTX_PairR (e1 : expr) | CTX_PairR (e1 : expr)
...@@ -16,19 +24,16 @@ Inductive ctx_item := ...@@ -16,19 +24,16 @@ Inductive ctx_item :=
| CTX_CaseL (e1 : expr) (e2 : expr) | CTX_CaseL (e1 : expr) (e2 : expr)
| CTX_CaseM (e0 : expr) (e2 : expr) | CTX_CaseM (e0 : expr) (e2 : expr)
| CTX_CaseR (e0 : expr) (e1 : expr) | CTX_CaseR (e0 : expr) (e1 : expr)
(* Bin op *)
| CTX_BinOpL (op : binop) (e2 : expr)
| CTX_BinOpR (op : binop) (e1 : expr)
(* If *)
| CTX_IfL (e1 : expr) (e2 : expr)
| CTX_IfM (e0 : expr) (e2 : expr)
| CTX_IfR (e0 : expr) (e1 : expr)
(* Recursive Types *) (* Recursive Types *)
| CTX_Fold | CTX_Fold
| CTX_Unfold | CTX_Unfold
(* Polymorphic Types *) (* Polymorphic Types *)
| CTX_TLam | CTX_TLam
| CTX_TApp | CTX_TApp
(* Existential types *)
| CTX_Pack
| CTX_UnpackL (e' : expr)
| CTX_UnpackR (e : expr)
(* Concurrency *) (* Concurrency *)
| CTX_Fork | CTX_Fork
(* Reference Types *) (* Reference Types *)
...@@ -64,6 +69,9 @@ Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr := ...@@ -64,6 +69,9 @@ Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
| CTX_Unfold => Unfold e | CTX_Unfold => Unfold e
| CTX_TLam => TLam e | CTX_TLam => TLam e
| CTX_TApp => TApp e | CTX_TApp => TApp e
| CTX_Pack => Pack e
| CTX_UnpackL e1 => Unpack e e1
| CTX_UnpackR e0 => Unpack e0 e
| CTX_Fork => Fork e | CTX_Fork => Fork e
| CTX_Alloc => Alloc e | CTX_Alloc => Alloc e
| CTX_Load => Load e | CTX_Load => Load e
...@@ -145,6 +153,14 @@ Inductive typed_ctx_item : ...@@ -145,6 +153,14 @@ Inductive typed_ctx_item :
typed_ctx_item CTX_TLam (subst (ren (+1)) <$> Γ) τ Γ (TForall τ) typed_ctx_item CTX_TLam (subst (ren (+1)) <$> Γ) τ Γ (TForall τ)
| TP_CTX_TApp Γ τ τ' : | TP_CTX_TApp Γ τ τ' :
typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/] typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
| TP_CTX_Pack Γ τ τ' :
typed_ctx_item CTX_Pack Γ τ.[τ'/] Γ (TExists τ)
| TP_CTX_UnpackL e2 Γ τ τ2 :
typed (subst (ren (+1)) <$> Γ) e2 (TArrow τ (subst (ren (+1)) τ2))
typed_ctx_item (CTX_UnpackL e2) Γ (TExists τ) Γ τ2
| TP_CTX_UnpackR e1 Γ τ τ2 :
typed Γ e1 (TExists τ)
typed_ctx_item (CTX_UnpackR e1) (subst (ren (+1)) <$> Γ) (TArrow τ (subst (ren (+1)) τ2)) Γ τ2
| TP_CTX_Fork Γ : | TP_CTX_Fork Γ :
typed_ctx_item CTX_Fork Γ TUnit Γ TUnit typed_ctx_item CTX_Fork Γ TUnit Γ TUnit
| TPCTX_Alloc Γ τ : | TPCTX_Alloc Γ τ :
...@@ -194,7 +210,8 @@ Proof. ...@@ -194,7 +210,8 @@ Proof.
split_and?; destruct_and?; split_and?; destruct_and?;
rewrite ?cons_binder_union; eauto; rewrite ?cons_binder_union; eauto;
try match goal with H : typed _ _ _ |- _ => eapply (typed_X_closed _ _ _ H) end. try match goal with H : typed _ _ _ |- _ => eapply (typed_X_closed _ _ _ H) end.
rewrite -(dom_fmap (subst (ren (+1))) Γ). eauto. all: rewrite -(dom_fmap (subst (ren (+1))) Γ); eauto.
by eapply typed_X_closed.
Qed. Qed.
Definition ctx_refines (Γ : stringmap type) Definition ctx_refines (Γ : stringmap type)
...@@ -345,6 +362,12 @@ Section bin_log_related_under_typed_ctx. ...@@ -345,6 +362,12 @@ Section bin_log_related_under_typed_ctx.
iApply (IHK with "[Hrel]"); auto. iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_tapp' with "[]"); try fundamental. + iApply (bin_log_related_tapp' with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto. iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_pack'.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_unpack; try by (iIntros; fundamental).
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_unpack; try by (iIntros; fundamental).
iIntros. iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_fork with "[]"); try fundamental. + iApply (bin_log_related_fork with "[]"); try fundamental.
iApply (IHK with "[Hrel]"); auto. iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_alloc with "[]"); try fundamental. + iApply (bin_log_related_alloc with "[]"); try fundamental.
......
...@@ -17,9 +17,10 @@ Module lang. ...@@ -17,9 +17,10 @@ Module lang.
Inductive Literal := Unit | Nat (n : nat) | Bool (b : bool). Inductive Literal := Unit | Nat (n : nat) | Bool (b : bool).
Inductive expr := Inductive expr :=
| Var (x : string) | Var (x : string)
(* λ-rec *)
| Rec (f x : binder) (e : expr) | Rec (f x : binder) (e : expr)
| App (e1 e2 : expr) | App (e1 e2 : expr)
(* Base Types *) (* Constants *)
| Lit (l : Literal) | Lit (l : Literal)
| BinOp (op : binop) (e1 e2 : expr) | BinOp (op : binop) (e1 e2 : expr)
(* If then else *) (* If then else *)
...@@ -44,7 +45,7 @@ Module lang. ...@@ -44,7 +45,7 @@ Module lang.
(* Concurrency *) (* Concurrency *)
| Fork (e : expr) | Fork (e : expr)
(* Reference Types *) (* Reference Types *)
| Loc (l : loc) | Loc (l : loc) (* Should not be present in the surface syntax *)
| Alloc (e : expr) | Alloc (e : expr)
| Load (e : expr) | Load (e : expr)
| Store (e1 : expr) (e2 : expr) | Store (e1 : expr) (e2 : expr)
......
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