Commit e679dae9 authored by Amin Timany's avatar Amin Timany

Change typing rule for μ-types in Fμ,ref,par

With this change, recursive types don't use the context for type variables.
This allows us to assume that all types in typing context are universally
quantified, i.e., they are all polymorphic types.
parent b6db9444
...@@ -53,8 +53,6 @@ Section typed_interp. ...@@ -53,8 +53,6 @@ Section typed_interp.
Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" := (bin_log_related Δ Γ e e' τ) Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" := (bin_log_related Δ Γ e e' τ)
(at level 20) : bin_logrel_scope. (at level 20) : bin_logrel_scope.
Delimit Scope bin_logrel_scope with bin_logrel.
Local Open Scope bin_logrel_scope. Local Open Scope bin_logrel_scope.
Notation "✓✓" := context_interp_Persistent. Notation "✓✓" := context_interp_Persistent.
...@@ -270,10 +268,7 @@ Section typed_interp. ...@@ -270,10 +268,7 @@ Section typed_interp.
Qed. Qed.
Lemma typed_binary_interp_Fold Δ Γ e e' τ {HΔ : ✓✓ Δ} Lemma typed_binary_interp_Fold Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : (IHHtyped : Δ Γ e log e' τ.[(TRec τ)/])
(extend_context_interp ((@interp Σ iS iI (N .@ 1) (TRec τ)) Δ) Δ)
map (λ t : type, t.[ren (+1)]) Γ
e log e' τ)
: :
Δ Γ Fold e log Fold e' TRec τ. Δ Γ Fold e log Fold e' TRec τ.
Proof. Proof.
...@@ -282,14 +277,14 @@ Section typed_interp. ...@@ -282,14 +277,14 @@ Section typed_interp.
iApply wp_wand_l; iSplitR; iApply wp_wand_l; iSplitR;
[|iApply (IHHtyped _ _ _ j (K ++ [FoldCtx])); [|iApply (IHHtyped _ _ _ j (K ++ [FoldCtx]));
rewrite fill_app; simpl; repeat iSplitR; trivial]. rewrite fill_app; simpl; repeat iSplitR; trivial].
+ iIntros {v} "Hv"; iDestruct "Hv" as {w} "[Hv #Hiv]"; iIntros {v} "Hv"; iDestruct "Hv" as {w} "[Hv #Hiv]";
rewrite fill_app. rewrite fill_app.
value_case. iExists (FoldV w); iFrame "Hv". value_case. iExists (FoldV w); iFrame "Hv".
rewrite fixpoint_unfold; cbn. rewrite fixpoint_unfold; cbn.
iAlways. iExists (_, _); iSplit; try iNext; trivial. rewrite -interp_subst; trivial.
+ rewrite zip_with_context_interp_subst; trivial. iAlways; iExists (_, _); iSplit; try iNext; trivial.
(* unshelving *) (* unshelving *)
Unshelve. all: rewrite map_length; trivial. Unshelve. all: trivial.
Qed. Qed.
Lemma typed_binary_interp_Unfold Δ Γ e e' τ {HΔ : ✓✓ Δ} Lemma typed_binary_interp_Unfold Δ Γ e e' τ {HΔ : ✓✓ Δ}
...@@ -534,4 +529,5 @@ Section typed_interp. ...@@ -534,4 +529,5 @@ Section typed_interp.
End typed_interp. End typed_interp.
Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" := (bin_log_related Δ Γ e e' τ) Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" := (bin_log_related Δ Γ e e' τ)
(at level 20) : bin_logrel_scope. (at level 20) : bin_logrel_scope.
\ No newline at end of file Delimit Scope bin_logrel_scope with bin_logrel.
\ No newline at end of file
...@@ -135,18 +135,16 @@ Section typed_interp. ...@@ -135,18 +135,16 @@ Section typed_interp.
iApply wp_mono; [|trivial]. iApply wp_mono; [|trivial].
iIntros {w} "#H". rewrite -interp_subst; trivial. iIntros {w} "#H". rewrite -interp_subst; trivial.
- (* Fold *) - (* Fold *)
rewrite map_length in IHHtyped. specialize (IHHtyped Δ HΔ vs Hlen).
setoid_rewrite <- interp_subst in IHHtyped.
iApply (@wp_bind _ _ _ [FoldCtx]). iApply (@wp_bind _ _ _ [FoldCtx]).
iApply wp_impl_l. iApply wp_impl_l.
iSplit; [eapply (@always_intro _ _ _ _)| iSplit; [eapply (@always_intro _ _ _ _)| iApply IHHtyped; trivial].
iApply (IHHtyped (extend_context_interp ((interp (TRec τ)) Δ) Δ));
trivial].
+ iIntros {v} "#Hv". + iIntros {v} "#Hv".
value_case. value_case.
rewrite fixpoint_unfold; cbn. rewrite fixpoint_unfold; cbn.
auto with itauto. auto with itauto.
+ iRevert "Hheap HΓ"; rewrite zip_with_context_interp_subst; + iFrame "Hheap HΓ"; trivial.
iIntros "#Hheap #HΓ"; auto with itauto.
- (* Unfold *) - (* Unfold *)
iApply (@wp_bind _ _ _ [UnfoldCtx]); iApply (@wp_bind _ _ _ [UnfoldCtx]);
iApply wp_impl_l; iApply wp_impl_l;
......
...@@ -48,7 +48,7 @@ Inductive typed (Γ : list type) : expr → type → Prop := ...@@ -48,7 +48,7 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
| TApp_typed e τ τ': | TApp_typed e τ τ':
typed Γ e (TForall τ) typed Γ (TApp e) (τ.[τ'/]) typed Γ e (TForall τ) typed Γ (TApp e) (τ.[τ'/])
| TFold e τ : | TFold e τ :
typed (map (λ t, t.[ren (+1)]) Γ) e τ typed Γ e (τ.[(TRec τ)/])
typed Γ (Fold e) (TRec τ) typed Γ (Fold e) (TRec τ)
| TUnfold e τ : typed Γ e (TRec τ) typed Γ (Unfold e) (τ.[(TRec τ)/]) | TUnfold e τ : typed Γ e (TRec τ) typed Γ (Unfold e) (τ.[(TRec τ)/])
| TFork e : typed Γ e TUnit typed Γ (Fork e) TUnit | TFork e : typed Γ e TUnit typed Γ (Fork e) TUnit
......
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