From a7ce476ffa6464cc7541a5ac5c46f426e2e79cbd Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sat, 12 Jan 2019 19:54:13 +0100
Subject: [PATCH] Semantic interpretation of types

---
 _CoqProject              |  1 +
 theories/logic/model.v   |  6 +--
 theories/typing/interp.v | 94 ++++++++++++++++++++++++++++++++++++++++
 theories/typing/types.v  |  2 +-
 4 files changed, 99 insertions(+), 4 deletions(-)
 create mode 100644 theories/typing/interp.v

diff --git a/_CoqProject b/_CoqProject
index 1a5639a..f62cee0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -11,6 +11,7 @@ theories/logic/derived.v
 theories/logic/proofmode/tactics.v
 
 theories/typing/types.v
+theories/typing/interp.v
 
 theories/tests/tp_tests.v
 theories/tests/proofmode_tests.v
diff --git a/theories/logic/model.v b/theories/logic/model.v
index db1f683..29f9539 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -25,8 +25,8 @@ Existing Instance lty2_persistent.
 Section lty2_ofe.
   Context `{relocG Σ}.
 
-  Instance lty2_equiv : Equiv lty2 := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
-  Instance lty2_dist : Dist lty2 := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
+  Global Instance lty2_equiv : Equiv lty2 := λ A B, ∀ w1 w2, A w1 w2 ≡ B w1 w2.
+  Global Instance lty2_dist : Dist lty2 := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
   Lemma lty2_ofe_mixin : OfeMixin lty2.
   Proof. by apply (iso_ofe_mixin (lty2_car : lty2 → (val -c> val -c> iProp Σ))). Qed.
   Canonical Structure lty2C := OfeT lty2 lty2_ofe_mixin.
@@ -60,7 +60,7 @@ Section semtypes.
     ={E,⊤}=∗ WP e {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ A v v' }})%I.
 
   Global Instance interp_expr_ne E n :
-    Proper ((=) ==> (=) ==> (=) ==> dist n) (interp_expr E).
+    Proper ((=) ==> (=) ==> (dist n) ==> dist n) (interp_expr E).
   Proof. solve_proper. Qed.
 
   Definition lty2_unit : lty2 := Lty2 (λ w1 w2, ⌜ w1 = #() ∧ w2 = #() ⌝%I).
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
new file mode 100644
index 0000000..ab2777f
--- /dev/null
+++ b/theories/typing/interp.v
@@ -0,0 +1,94 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Interpretations for System F_mu_ref types *)
+From iris.algebra Require Import list.
+From reloc.typing Require Export types.
+From reloc.logic Require Import model.
+From Autosubst Require Import Autosubst.
+
+Section semtypes.
+  Context `{relocG Σ}.
+
+  (** Type-level lambdas are interpreted as closures *)
+
+  Definition lty2_forall (C : lty2 → lty2) : lty2 := Lty2 (λ w1 w2,
+    □ ∀ A : lty2, interp_expr ⊤ (TApp w1) (TApp w2) (C A))%I.
+
+  Definition lty2_exists (C : lty2 → lty2) : lty2 := Lty2 (λ w1 w2,
+    ∃ A : lty2, C A w1 w2)%I.
+
+  Definition lty2_true : lty2 := Lty2 (λ w1 w2, True)%I.
+
+  Program Definition ctx_lookup (x : var) : listC lty2C -n> lty2C := λne Δ,
+    (from_option id lty2_true (Δ !! x))%I.
+  Next Obligation.
+    intros x n Δ Δ' HΔ.
+    destruct (Δ !! x) as [P|] eqn:HP; cbn in *.
+    - eapply (Forall2_lookup_l _ _ _ x P) in HΔ; last done.
+      destruct HΔ as (Q & HQ & HΔ).
+      rewrite HQ /= //.
+    - destruct (Δ' !! x) as [Q|] eqn:HQ; last reflexivity.
+      eapply (Forall2_lookup_r _ _ _ x Q) in HΔ; last done.
+      destruct HΔ as (P & HP' & HΔ). exfalso.
+      rewrite HP in HP'. inversion HP'.
+  Qed.
+
+  Instance lty2_prod_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_prod.
+  Proof.
+    intros A A' HA B B' HB.
+    intros w1 w2. cbn.
+    unfold lty2_prod, lty2_car. cbn.
+    (* TODO: why do we have to unfold lty2_car here? *)
+    repeat f_equiv; eauto.
+  Qed.
+
+  Instance lty2_sum_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_sum.
+  Proof.
+    intros A A' HA B B' HB.
+    intros w1 w2. cbn.
+    unfold lty2_sum, lty2_car. cbn.
+    (* TODO: why do we have to unfold lty2_car here? *)
+    repeat f_equiv; eauto.
+  Qed.
+
+  Instance lty2_arr_ne n : Proper (dist n ==> (dist n ==> dist n)) lty2_arr.
+  Proof.
+    intros A A' HA B B' HB.
+    intros w1 w2. cbn.
+    unfold lty2_sum, lty2_car. cbn.
+    (* TODO: why do we have to unfold lty2_car here? *)
+    repeat f_equiv; eauto.
+  Qed.
+
+  Instance lty2_rec_ne n : Proper (dist n ==> dist n)
+                                   (lty2_rec : (lty2C -n> lty2C) -> lty2C).
+  Proof.
+    intros F F' HF.
+    unfold lty2_rec, lty2_car.
+    apply fixpoint_ne=> X w1 w2.
+    unfold lty2_rec1, lty2_car. cbn.
+    f_equiv.
+    apply lty2_car_ne; eauto.
+  Qed.
+
+  Program Fixpoint interp (Ï„ : type) : listC lty2C -n> lty2C :=
+    match Ï„ as _ return _ with
+    | TUnit => λne _, lty2_unit
+    | TNat => λne _, lty2_int
+    | TBool => λne _, lty2_bool
+    | TProd τ1 τ2 => λne Δ, lty2_prod (interp τ1 Δ) (interp τ2 Δ)
+    | TSum τ1 τ2 => λne Δ, lty2_sum (interp τ1 Δ) (interp τ2 Δ)
+    | TArrow τ1 τ2 => λne Δ, lty2_arr (interp τ1 Δ) (interp τ2 Δ)
+    | TRec τ' => λne Δ, lty2_rec (λne τ, interp τ' (τ::Δ))
+    | TVar x => ctx_lookup x
+    | TForall τ' => λne Δ, lty2_forall (λ τ, interp τ' (τ::Δ))
+    | TExists τ' => λne Δ, lty2_exists (λ τ, interp τ' (τ::Δ))
+    | Tref τ => λne Δ, lty2_ref (interp τ Δ)
+    end.
+  Solve Obligations with (intros I τ τ' n Δ Δ' HΔ' ??; solve_proper).
+  Next Obligation.
+    intros I τ τ' n Δ Δ' HΔ' ??.
+    apply lty2_rec_ne=> X /=.
+    apply I. by f_equiv.
+  Defined.
+
+End semtypes.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index c466404..e90783e 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -1,7 +1,7 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Typing for System F_mu_ref with existential types and concurrency *)
 From stdpp Require Export stringmap.
-From iris.heap_lang Require Import lang notation.
+From iris.heap_lang Require Export lang notation.
 From Autosubst Require Import Autosubst.
 
 (** * Types *)
-- 
GitLab