Commit 46771a6a authored by David Swasey's avatar David Swasey

Add existential types (unary logrel only).

parent de2c8673
......@@ -44,14 +44,14 @@ theories/logrel/F_mu_ref_conc/typing.v
theories/logrel/F_mu_ref_conc/logrel_unary.v
theories/logrel/F_mu_ref_conc/fundamental_unary.v
theories/logrel/F_mu_ref_conc/rules_binary.v
theories/logrel/F_mu_ref_conc/logrel_binary.v
theories/logrel/F_mu_ref_conc/fundamental_binary.v
#theories/logrel/F_mu_ref_conc/logrel_binary.v
#theories/logrel/F_mu_ref_conc/fundamental_binary.v
theories/logrel/F_mu_ref_conc/soundness_unary.v
theories/logrel/F_mu_ref_conc/context_refinement.v
theories/logrel/F_mu_ref_conc/soundness_binary.v
#theories/logrel/F_mu_ref_conc/context_refinement.v
#theories/logrel/F_mu_ref_conc/soundness_binary.v
theories/logrel/F_mu_ref_conc/examples/lock.v
theories/logrel/F_mu_ref_conc/examples/counter.v
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
#theories/logrel/F_mu_ref_conc/examples/counter.v
#theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
#theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
#theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
#theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
......@@ -87,6 +87,22 @@ Section typed_interp.
smart_wp_bind TAppCtx v "#Hv" IHtyped; cbn.
iApply wp_wand_r; iSplitL; [iApply ("Hv" $! ( τ' Δ)); iPureIntro; apply _|]; cbn.
iIntros (w) "?". by iApply interp_subst.
- (* Pack *)
smart_wp_bind PackCtx v "#Hv" IHtyped; cbn.
iApply wp_value. iAlways. iExists v, ( τ' Δ).
iSplit; first done. iSplit; first by iPureIntro=>?; apply _.
by iApply interp_subst.
- (* Unpack *)
smart_wp_bind (UnpackCtx _) v "#Hv" IHtyped1; cbn.
iDestruct "Hv" as (w τi) "(%&%&Hw)"; subst.
iApply wp_pure_step_later; auto 1 using to_of_val; asimpl.
rewrite -/of_val. iNext.
iDestruct (interp_env_length with "HΓ") as %?.
erewrite typed_subst_head_simpl; [|done|solve_length].
iApply interp_expr_unused.
iApply (IHtyped2 (τi :: Δ) (w :: vs)).
iApply interp_env_cons. rewrite (interp_env_ren Δ Γ vs τi).
by iFrame "#".
- (* Fold *)
iApply (wp_bind (fill [FoldCtx]));
iApply wp_wand_l; iSplitL; [|iApply (IHtyped Δ vs); auto].
......
......@@ -38,6 +38,9 @@ Module F_mu_ref_conc.
(* Polymorphic Types *)
| TLam (e : expr)
| TApp (e : expr)
(* Existential Types *)
| Pack (e : expr)
| Unpack (e0 : expr) (e1 : {bind expr})
(* Concurrency *)
| Fork (e : expr)
(* Reference Types *)
......@@ -71,6 +74,7 @@ Module F_mu_ref_conc.
| InjLV (v : val)
| InjRV (v : val)
| FoldV (v : val)
| PackV (v : val)
| LocV (l : loc).
(* Notation for bool and nat *)
......@@ -102,6 +106,7 @@ Module F_mu_ref_conc.
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
| FoldV v => Fold (of_val v)
| PackV v => Pack (of_val v)
| LocV l => Loc l
end.
......@@ -116,6 +121,7 @@ Module F_mu_ref_conc.
| InjL e => InjLV <$> to_val e
| InjR e => InjRV <$> to_val e
| Fold e => v to_val e; Some (FoldV v)
| Pack e => v to_val e; Some (PackV v)
| Loc l => Some (LocV l)
| _ => None
end.
......@@ -137,6 +143,8 @@ Module F_mu_ref_conc.
| IfCtx (e1 : {bind expr}) (e2 : {bind expr})
| FoldCtx
| UnfoldCtx
| PackCtx
| UnpackCtx (e1 : {bind expr})
| AllocCtx
| LoadCtx
| StoreLCtx (e2 : expr)
......@@ -163,6 +171,8 @@ Module F_mu_ref_conc.
| IfCtx e1 e2 => If e e1 e2
| FoldCtx => Fold e
| UnfoldCtx => Unfold e
| PackCtx => Pack e
| UnpackCtx e1 => Unpack e e1
| AllocCtx => Alloc e
| LoadCtx => Load e
| StoreLCtx e2 => Store e e2
......@@ -208,7 +218,11 @@ Module F_mu_ref_conc.
head_step (Unfold (Fold e)) σ e σ []
(* Polymorphic Types *)
| TBeta e σ :
head_step (TApp (TLam e)) σ e σ []
head_step (TApp (TLam e)) σ e σ []
(* Existential Types *)
| Unpack_Pack e0 v0 e1 σ :
to_val e0 = Some v0
head_step (Unpack (Pack e0) e1) σ e1.[e0/] σ []
(* Concurrency *)
| ForkS e σ:
head_step (Fork e) σ Unit σ [e]
......
......@@ -44,6 +44,12 @@ Section logrel.
⌜∀ v, Persistent (τi v) WP TApp (of_val w) {{ interp (τi :: Δ) }})%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_exist
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
( w1 (τi : D),
w = PackV w1 ⌜∀ v, Persistent (τi v) interp (τi :: Δ) w1)%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Definition interp_rec1
(interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
( ( v, w = FoldV v interp (τi :: Δ) v))%I.
......@@ -77,6 +83,7 @@ Section logrel.
| TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2)
| TVar x => env_lookup x
| TForall τ' => interp_forall (interp τ')
| TExist τ' => interp_exist (interp τ')
| TRec τ' => interp_rec (interp τ')
| Tref τ' => interp_ref (interp τ')
end.
......@@ -130,6 +137,7 @@ Section logrel.
{ by rewrite !lookup_app_l. }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros w; simpl; properness; auto. by apply IHτ.
Qed.
......@@ -150,9 +158,19 @@ Section logrel.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
- intros w; simpl; properness; auto. by apply IHτ.
Qed.
Lemma interp_unused Δ τ τi : τ.[ren (+1)] (τi :: Δ) τ Δ.
Proof. apply (interp_weaken [] [τi] Δ τ). Qed.
Lemma interp_expr_unused Δ τ τi e :
interp_expr (τ.[ren (+1)]) (τi :: Δ) e interp_expr τ Δ e.
Proof.
rewrite/interp_expr. apply wp_proper=>/= v. by rewrite interp_unused.
Qed.
Lemma interp_subst Δ2 τ τ' : τ ( τ' Δ2 :: Δ2) τ.[τ'/] Δ2.
Proof. apply (interp_subst_up []). Qed.
......
......@@ -147,6 +147,10 @@ Section lang_rules.
Global Instance pure_tlam e : PureExec True (TApp (TLam e)) e.
Proof. solve_pure_exec. Qed.
Global Instance pure_unpack e1 e2 `{!AsVal e1} :
PureExec True (Unpack (Pack e1) e2) e2.[e1 /].
Proof. solve_pure_exec. Qed.
Global Instance pure_fold e `{!AsVal e}:
PureExec True (Unfold (Fold e)) e.
Proof. solve_pure_exec. Qed.
......
......@@ -10,6 +10,7 @@ Inductive type :=
| TRec (τ : {bind 1 of type})
| TVar (x : var)
| TForall (τ : {bind 1 of type})
| TExist (τ : {bind 1 of type})
| Tref (τ : type).
Instance Ids_type : Ids type. derive. Defined.
......@@ -56,6 +57,10 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
| TLam_typed e τ :
subst (ren (+1)) <$> Γ ⊢ₜ e : τ Γ ⊢ₜ TLam e : TForall τ
| TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ Γ ⊢ₜ TApp e : τ.[τ'/]
| TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] Γ ⊢ₜ Pack e : TExist τ
| TUnpack e0 e1 τ τ1 :
Γ ⊢ₜ e0 : TExist τ τ :: (subst (ren(+1)) <$> Γ) ⊢ₜ e1 : τ1.[ren(+1)]
Γ ⊢ₜ Unpack e0 e1 : τ1
| TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/] Γ ⊢ₜ Fold e : TRec τ
| TUnfold e τ : Γ ⊢ₜ e : TRec τ Γ ⊢ₜ Unfold e : τ.[TRec τ/]
| TFork e : Γ ⊢ₜ e : TUnit Γ ⊢ₜ Fork e : TUnit
......@@ -79,6 +84,7 @@ Proof.
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
Qed.
Lemma n_closed_invariant n (e : expr) s1 s2 :
( f, e.[upn n f] = e) ( x, x < n s1 x = s2 x) e.[s1] = e.[s2].
Proof.
......@@ -110,6 +116,12 @@ Proof.
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|x] H2; [by cbv |].
asimpl; rewrite H1; auto with omega.
- change (e1.[up (upn m (ren (+1)))]) with
(e1.[iter (S m) up (ren (+1))]) in *.
apply (IHe0 (S m)).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|x] H2; [by cbv |].
asimpl; rewrite H1; auto with omega.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
......@@ -121,6 +133,7 @@ Proof.
- apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with omega.
- f_equal. apply IHtyped.
- by f_equal; rewrite map_length in IHtyped.
- f_equal. by apply IHtyped1. by rewrite map_length in IHtyped2.
Qed.
Lemma n_closed_subst_head_simpl n e w ws :
......@@ -181,6 +194,11 @@ Proof.
asimpl in *. rewrite ?map_length in IHtyped.
repeat rewrite fmap_app. apply IHtyped.
by repeat rewrite fmap_app.
- econstructor; eauto.
specialize (IHtyped2
(τ :: (subst (ren (+1)) <$> Γ1)) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
asimpl in *. rewrite !map_length fmap_app in IHtyped2.
rewrite !fmap_app. by apply IHtyped2.
Qed.
Lemma context_weakening ξ Γ e τ :
......
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