Skip to content
Snippets Groups Projects
Commit 4499177d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Make the function type contractive.

Also, changed the way we substitute lists, so that we do not need to to substitute de function name separately.
Parameters get substituted from right to left.
parent 7c4dc90c
No related branches found
No related tags found
No related merge requests found
...@@ -159,18 +159,17 @@ Definition subst' (mx : binder) (es : expr) : expr → expr := ...@@ -159,18 +159,17 @@ Definition subst' (mx : binder) (es : expr) : expr → expr :=
Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr := Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :=
match xl, esl with match xl, esl with
| [], [] => Some e | [], [] => Some e
| x::xl, es::esl => subst_l xl esl (subst' x es e) | x::xl, es::esl => subst' x es <$> subst_l xl esl e
| _, _ => None | _, _ => None
end. end.
Definition subst_v (xl : list binder) (esl : vec expr (length xl)) Definition subst_v (xl : list binder) (vsl : vec val (length xl))
(e : expr) : expr := (e : expr) : expr :=
from_option id (Var "" (* Dummy *)) (subst_l xl esl e). Vector.fold_right2 (λ b, subst' b of_val) e _ (list_to_vec xl) vsl.
Lemma subst_v_eq (xl : list binder) (esl : vec expr (length xl)) e : Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
Some $ subst_v xl esl e = subst_l xl esl e. Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
Proof. Proof.
unfold subst_v. destruct subst_l eqn:EQ; first done. exfalso. revert esl e EQ. revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl.
induction xl=>/= esl; inv_vec esl; first done. simpl. eauto.
Qed. Qed.
(** The stepping relation *) (** The stepping relation *)
...@@ -230,8 +229,8 @@ Inductive head_step : expr → state → expr → state → list expr → Prop : ...@@ -230,8 +229,8 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
| BetaS f xl e e' el σ: | BetaS f xl e e' el σ:
Forall (λ ei, is_Some (to_val ei)) el Forall (λ ei, is_Some (to_val ei)) el
Closed (f :b: xl +b+ []) e Closed (f :b: xl +b+ []) e
subst_l xl el e = Some e' subst_l (f::xl) (Rec f xl e :: el) e = Some e'
head_step (App (Rec f xl e) el) σ (subst' f (Rec f xl e) e') σ [] head_step (App (Rec f xl e) el) σ e' σ []
| ReadScS l n v σ: | ReadScS l n v σ:
σ !! l = Some (RSt n, v) σ !! l = Some (RSt n, v)
head_step (Read ScOrd (Lit $ LitLoc l)) σ (of_val v) σ [] head_step (Read ScOrd (Lit $ LitLoc l)) σ (of_val v) σ []
......
...@@ -146,9 +146,8 @@ Lemma wp_rec E e f xl erec erec' el Φ : ...@@ -146,9 +146,8 @@ Lemma wp_rec E e f xl erec erec' el Φ :
e = Rec f xl erec (* to avoids recursive calls being unfolded *) e = Rec f xl erec (* to avoids recursive calls being unfolded *)
Forall (λ ei, is_Some (to_val ei)) el Forall (λ ei, is_Some (to_val ei)) el
Closed (f :b: xl +b+ []) erec Closed (f :b: xl +b+ []) erec
subst_l xl el erec = Some erec' subst_l (f::xl) (e::el) erec = Some erec'
WP subst' f e erec' @ E {{ Φ }} -∗ WP erec' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
WP App e el @ E {{ Φ }}.
Proof. Proof.
iIntros (-> ???) "?". iApply ownP_lift_pure_det_head_step; subst; eauto. iIntros (-> ???) "?". iApply ownP_lift_pure_det_head_step; subst; eauto.
by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame. by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
......
...@@ -22,7 +22,7 @@ Section typing. ...@@ -22,7 +22,7 @@ Section typing.
Lemma type_cont E L1 L2 C T argsb econt e2 T' kb : Lemma type_cont E L1 L2 C T argsb econt e2 T' kb :
Closed (kb :b: argsb +b+ []) econt Closed (kb :b: []) e2 Closed (kb :b: argsb +b+ []) econt Closed (kb :b: []) e2
( k args, typed_body E L1 (CCtx_iscont k L1 _ T' :: C) (T' args) ( k args, typed_body E L1 (CCtx_iscont k L1 _ T' :: C) (T' args)
(subst' kb k $ subst_v argsb (vmap of_val args) econt)) (subst_v (kb::argsb) (k:::args) econt))
( k, typed_body E L2 (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2)) ( k, typed_body E L2 (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2))
typed_body E L2 C T (let: kb := Rec kb argsb econt in e2). typed_body E L2 C T (let: kb := Rec kb argsb econt in e2).
Proof. Proof.
...@@ -33,7 +33,7 @@ Section typing. ...@@ -33,7 +33,7 @@ Section typing.
iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE *"). iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE *").
iIntros (args) "Htl HL HT". iApply wp_rec; try done. iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. } { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -vec_to_list_map -subst_v_eq. } { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
(* FIXME: iNext here unfolds things in the context. *) (* FIXME: iNext here unfolds things in the context. *)
iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT"). iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT").
by iApply "IH". by iApply "IH".
......
...@@ -12,13 +12,15 @@ Section fn. ...@@ -12,13 +12,15 @@ Section fn.
Program Definition fn {A n} (E : A elctx) Program Definition fn {A n} (E : A elctx)
(tys : A vec type n) (ty : A type) : type := (tys : A vec type n) (ty : A type) : type :=
{| st_own tid vl := ( f, vl = [f] (x : A) (args : vec val n) (k : val), {| st_own tid vl := ( fb kb xb e H,
typed_body (E x) [] vl = [@RecV fb (kb::xb) e H] length xb = n
[CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])] (x : A) (k : val) (xl : vec val (length xb)),
(zip_with (TCtx_hasty of_val) args (tys x)) typed_body (E x) []
(f (of_val <$> (k :: args : list val))))%I |}. [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
(zip_with (TCtx_hasty of_val) xl (tys x))
(subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
Next Obligation. Next Obligation.
iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (f) "[% _]". by subst. iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
Qed. Qed.
Global Instance fn_send {A n} E tys ty : Send (@fn A n E tys ty). Global Instance fn_send {A n} E tys ty : Send (@fn A n E tys ty).
...@@ -34,12 +36,13 @@ Section typing. ...@@ -34,12 +36,13 @@ Section typing.
subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2). subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
Proof. Proof.
intros Htys Hty. apply subtype_simple_type=>//= _ vl. intros Htys Hty. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst. iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE HL HC HT". iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iAlways. iNext.
rewrite /typed_body. iIntros "* #HEAP _ Htl HE HL HC HT".
iDestruct (elctx_interp_persist with "HE") as "#HE'". iDestruct (elctx_interp_persist with "HE") as "#HE'".
iApply ("Hf" with "* HEAP LFT Htl HE HL [HC] [HT]"). iApply ("Hf" with "* HEAP LFT Htl HE HL [HC] [HT]").
- iIntros "HE". unfold cctx_interp. iIntros (e) "He". - iIntros "HE". unfold cctx_interp. iIntros (elt) "Helt".
iDestruct "He" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT". iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
iSpecialize ("HC" with "HE"). unfold cctx_elt_interp. iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
iApply ("HC" $! (CCtx_iscont _ _ _ _) with "[%] * Htl HL >"). iApply ("HC" $! (CCtx_iscont _ _ _ _) with "[%] * Htl HL >").
{ by apply elem_of_list_singleton. } { by apply elem_of_list_singleton. }
...@@ -68,8 +71,9 @@ Section typing. ...@@ -68,8 +71,9 @@ Section typing.
subtype E0 L0 (fn (n:=n) E tys ty) (fn (E σ) (tys σ) (ty σ)). subtype E0 L0 (fn (n:=n) E tys ty) (fn (E σ) (tys σ) (ty σ)).
Proof. Proof.
apply subtype_simple_type=>//= _ vl. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT _ _ Hf". iDestruct "Hf" as (f) "[% #Hf]". subst. iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists f. iSplit. done. rewrite /typed_body. iIntros "!# *". iApply "Hf". iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
rewrite /typed_body. iAlways. iNext. iIntros "*". iApply "Hf".
Qed. Qed.
Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A vec type n) ty : Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A vec type n) ty :
...@@ -77,8 +81,9 @@ Section typing. ...@@ -77,8 +81,9 @@ Section typing.
subtype E0 L0 (fn E' tys ty) (fn E tys ty). subtype E0 L0 (fn E' tys ty) (fn E tys ty).
Proof. Proof.
intros HEE'. apply subtype_simple_type=>//= _ vl. intros HEE'. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT _ _ Hf". iDestruct "Hf" as (f) "[% #Hf]". subst. iIntros "#LFT _ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE #HL HC HT". iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. rewrite /typed_body.
iAlways. iNext. iIntros "* #HEAP _ Htl HE #HL HC HT".
iMod (HEE' x with "[%] HE HL") as (qE') "[HE Hclose]". done. iMod (HEE' x with "[%] HE HL") as (qE') "[HE Hclose]". done.
iApply ("Hf" with "* HEAP LFT Htl HE HL [Hclose HC] HT"). iIntros "HE". iApply ("Hf" with "* HEAP LFT Htl HE HL [Hclose HC] HT"). iIntros "HE".
iApply fupd_cctx_interp. iApply ("HC" with ">"). iApply fupd_cctx_interp. iApply ("HC" with ">").
...@@ -90,8 +95,9 @@ Section typing. ...@@ -90,8 +95,9 @@ Section typing.
subtype E0 L0 (fn (λ x, ELCtx_Incl κ κ' :: E x) tys ty) (fn E tys ty). subtype E0 L0 (fn (λ x, ELCtx_Incl κ κ' :: E x) tys ty) (fn E tys ty).
Proof. Proof.
intros Hκκ'. apply subtype_simple_type=>//= _ vl. intros Hκκ'. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst. iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE #HL HC HT". iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. rewrite /typed_body.
iAlways. iNext. iIntros "* #HEAP _ Htl HE #HL HC HT".
iApply ("Hf" with "* HEAP LFT Htl [HE] HL [HC] HT"). iApply ("Hf" with "* HEAP LFT Htl [HE] HL [HC] HT").
{ rewrite /elctx_interp big_sepL_cons. iFrame. iApply (Hκκ' with "HE0 HL0"). } { rewrite /elctx_interp big_sepL_cons. iFrame. iApply (Hκκ' with "HE0 HL0"). }
rewrite /elctx_interp big_sepL_cons. iIntros "[_ HE]". by iApply "HC". rewrite /elctx_interp big_sepL_cons. iIntros "[_ HE]". by iApply "HC".
...@@ -118,9 +124,14 @@ Section typing. ...@@ -118,9 +124,14 @@ Section typing.
(zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap. (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=". iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $". iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $".
- simpl. iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons. - simpl. change (@length expr ps) with (length ps).
iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (f) "[EQ #Hf]". iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons.
iDestruct "EQ" as %[=->]. iSpecialize ("Hf" $! x vl k). iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl tys.
rewrite <-EQl=>vl tys. iApply wp_rec; try done.
{ rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::k:::vl)) //. }
iNext. iSpecialize ("Hf" $! x k vl).
iMod (HEsat with "[%] HE HL") as (q') "[HE' Hclose]"; first done. iMod (HEsat with "[%] HE HL") as (q') "[HE' Hclose]"; first done.
iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT']"). iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT']").
+ by rewrite /llctx_interp big_sepL_nil. + by rewrite /llctx_interp big_sepL_nil.
...@@ -128,8 +139,8 @@ Section typing. ...@@ -128,8 +139,8 @@ Section typing.
iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN". iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ HT". iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ HT".
iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton). iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
iApply ("HC" $! args with "Htl HL"). rewrite tctx_interp_singleton tctx_interp_cons. iApply ("HC" $! args with "Htl HL").
iFrame. rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
+ rewrite /tctx_interp vec_to_list_map zip_with_fmap_r + rewrite /tctx_interp vec_to_list_map zip_with_fmap_r
(zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap. (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']). iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
...@@ -139,23 +150,21 @@ Section typing. ...@@ -139,23 +150,21 @@ Section typing.
(tys : A vec type (length argsb)) ty (tys : A vec type (length argsb)) ty
T `{!CopyC T, !SendC T} : T `{!CopyC T, !SendC T} :
Closed (fb :b: kb :b: argsb +b+ []) e Closed (fb :b: kb :b: argsb +b+ []) e
( x f k (args : vec val _), ( x (f : val) k (args : vec val _),
typed_body (E' x) [] [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])] typed_body (E' x) [] [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
(TCtx_hasty f (fn E' tys ty) :: (TCtx_hasty f (fn E' tys ty) ::
zip_with (TCtx_hasty of_val) args (tys x) ++ T) zip_with (TCtx_hasty of_val) args (tys x) ++ T)
(subst' fb f $ subst_v (kb :: argsb) (vmap of_val $ k ::: args) e)) (subst_v (fb :: kb :: argsb) (f ::: k ::: args) e))
typed_instruction_ty E L T (Rec fb (kb :: argsb) e) (fn E' tys ty). typed_instruction_ty E L T (Rec fb (kb :: argsb) e) (fn E' tys ty).
Proof. Proof.
iIntros (Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value. iIntros (Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value.
{ simpl. rewrite decide_left. done. } { simpl. rewrite decide_left. done. }
rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit. rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
{ simpl. rewrite decide_left. done. } { simpl. rewrite decide_left. done. }
iExists _. iSplit; first done. iAlways. clear qE. iExists fb, kb, argsb, e, _. iSplit. done. iSplit. done. iAlways. iNext. clear qE.
iIntros (x args k tid' qE) "_ _ Htl HE HL HC HT'". iApply wp_rec; try done. iIntros (x k args tid' qE) "_ _ Htl HE HL HC HT'".
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -vec_to_list_cons -vec_to_list_map -subst_v_eq. }
iApply (Hbody with "* HEAP LFT Htl HE HL HC"). iApply (Hbody with "* HEAP LFT Htl HE HL HC").
rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH". rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
iApply sendc_change_tid. by iNext. by iApply sendc_change_tid.
Qed. Qed.
End typing. End typing.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment