diverging_static can now be checked in the type system

_CoqProject

@@ -62,7 +62,6 @@ theories/typing/lib/fake_shared.v
 theories/typing/lib/cell.v
 theories/typing/lib/spawn.v
 theories/typing/lib/join.v
-theories/typing/lib/diverging_static.v
 theories/typing/lib/take_mut.v
 theories/typing/lib/rc/rc.v
 theories/typing/lib/rc/weak.v
@@ -88,3 +87,4 @@ theories/typing/examples/unbox.v
 theories/typing/examples/init_prod.v
 theories/typing/examples/lazy_lft.v
 theories/typing/examples/nonlexical.v
+theories/typing/examples/diverging_static.v

theories/typing/lib/diverging_static.v → theories/typing/examples/diverging_static.v

@@ -27,30 +27,14 @@ Section diverging_static.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x f. simpl_subst.
     iApply type_let; [apply Hf|solve_typing|]. iIntros (call); simpl_subst.
-    (* Drop to Iris *)
-    iIntros (tid) "#LFT #HE Hna HL Hk (Hcall & Hx & Hf & _)".
-    (* We need a ϝ token to show that we can call F despite it being non-'static. *)
-    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (qϝ) "(Hϝ & HL & _)";
-      [solve_typing..|].
-    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "(Hα & _ & _)";
-      [solve_typing..|].
-    iMod (lft_eternalize with "Hα") as "#Hα".
-    iAssert (type_incl (box (&shr{α} T)) (box (&shr{static} T))) as "#[_ [Hincl _]]".
-    { iApply box_type_incl. iNext. iApply shr_type_incl; first done.
-      iApply type_incl_refl. }
-    wp_let. rewrite tctx_hasty_val.
-    iApply (type_call_iris _ [ϝ] () [_; _] with "LFT HE Hna [Hϝ] Hcall [Hx Hf]").
-    - solve_typing.
-    - by rewrite /= (right_id static).
-    - simpl. iFrame. iSplit; last done. rewrite !tctx_hasty_val.
-      iApply "Hincl". done.
-    - iClear "Hα Hincl". iIntros (r) "Htl Hϝ1 Hret". wp_rec.
-      (* Go back to the type system. *)
-      iApply (type_type _ [] _ [] with "[] LFT HE Htl [] Hk [-]"); last first.
-      { rewrite /tctx_interp /=. done. }
-      { rewrite /llctx_interp /=. done. }
-      iApply (type_cont [] [] (λ _, [])).
-      + iIntros (?). simpl_subst. iApply type_jump; solve_typing.
-      + iIntros "!#" (? args). inv_vec args. simpl_subst. iApply type_jump; solve_typing.
+    iApply (type_cont [_] [] (λ r, [(r!!!0%fin:val) ◁ box (unit)])).
+    { iIntros (k). simpl_subst.
+      iApply type_equivalize_lft_static.
+      iApply (type_call [ϝ] ()); solve_typing. }
+    iIntros "!# *". inv_vec args=>r. simpl_subst.
+    iApply (type_cont [] [] (λ r, [])).
+    { iIntros (kloop). simpl_subst. iApply type_jump; solve_typing. }
+    iIntros "!# *". inv_vec args. simpl_subst.
+    iApply type_jump; solve_typing.
   Qed.
 End diverging_static.

theories/typing/function.v

@@ -333,13 +333,13 @@ Section typing.
     rewrite tctx_interp_cons tctx_hasty_val. iFrame.
   Qed.
 
-  (* Specialized type_call':  Adapted for use by solve_typing; fixed "list of
-     alive lifetimes" to be the local ones. *)
-  Lemma type_call {A} x E L C T T' T'' p (ps : list path)
+  (* Specialized type_call':  Adapted for use by solve_typing.
+     κs is still expected to be given manually. *)
+  Lemma type_call {A} κs x E L C T T' T'' p (ps : list path)
                         (fp : A → fn_params (length ps)) k :
     p ◁ fn fp ∈ T →
-    Forall (lctx_lft_alive E L) (L.*1) →
-    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> (L.*1)) ++ E) L ((fp x).(fp_E) ϝ)) →
+    Forall (lctx_lft_alive E L) κs →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
                                    (box <$> vec_to_list (fp x).(fp_tys))) T T' →
     k ◁cont(L, T'') ∈ C →