Library iris.chan2heap.chan2heap

From iris.chan_lang Require Export lang notation.
From iris.heap_lang Require Import lang notation.
From iris.prelude Require Import gmap stringmap mapset.


Definition alloc : heap_lang.expr :=
  let: "l" := ref (InjR #()) in
    ("l", "l").

Definition recv : heap_lang.expr :=
  rec: "recv" "l" :=
    match: !"l" with
      InjR "_" ⇒ ("recv": heap_lang.expr) "l"
    | InjL "x" ⇒ "x"
    end.

Definition send l v : heap_lang.expr :=
  letp: "l" "v" := (l, v) in
        let: "lnew" := ref (InjR #()) in
        "l" <- InjL (("lnew", "v"));; "lnew".

Section translate.
Import chan_lang.
Import iris.chan_lang.derived.
Import iris.chan_lang.notation.

Fixpoint c2h (ec: chan_lang.expr) : heap_lang.expr :=
  (match ec with
   | Var x ⇒ x
   | Rec f x e ⇒ rec: f x := c2h e
   | App e1 e2 ⇒ (c2h e1) (c2h e2)
   | Lit l ⇒
     match l with
     | LitInt n ⇒ #n
     | LitBool b ⇒ #b
     | LitUnit ⇒ heap_lang.Lit heap_lang.LitUnit
     
     | LitLoc l _ ⇒ heap_lang.Lit (heap_lang.LitLoc l)
     end
   | Pair e1 e2 ⇒ (c2h e1, c2h e2)
   | Fork e ⇒ heap_lang.Fork (c2h e)
   | Letp x y e eb ⇒ heap_lang.Letp x y (c2h e) (c2h eb)
   | Recv e ⇒ recv (c2h e)
   | Send e1 e2 ⇒ send (c2h e1) (c2h e2)
   | Alloc ⇒ alloc
   | _ ⇒ (heap_lang.Lit heap_lang.LitUnit)
   end)%E.

Lemma c2h_closed ec l: is_closed l ec → heap_lang.is_closed l (c2h ec).
Proof.
  revert l; induction ec; simpl; try (naive_solver; eauto).
  intros. case_match; auto.
Qed.

End translate.