From 11b432e86e7e385041132dfcbb303a8d7a99d470 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 5 Mar 2020 18:16:24 +0100
Subject: [PATCH] clean up the context typing a bit

---
 theories/typing/contextual_refinement.v | 230 +++++++++++++-----------
 1 file changed, 127 insertions(+), 103 deletions(-)

diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index c12db48..d51061c 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -6,14 +6,14 @@ From iris.proofmode Require Import tactics.
 From reloc.typing Require Export types interp fundamental.
 
 Inductive ctx_item :=
-  (* Î»-rec *)
-  | CTX_Rec (f x: binder)
+  (* Base lambda calculus *)
+  | CTX_Rec (f x : binder)
   | CTX_AppL (e2 : expr)
   | CTX_AppR (e1 : expr)
-  (* Bin op *)
+  (* Base types and their operations *)
+  | CTX_UnOp (op : un_op)
   | CTX_BinOpL (op : bin_op) (e2 : expr)
   | CTX_BinOpR (op : bin_op) (e1 : expr)
-  (* If *)
   | CTX_IfL (e1 : expr) (e2 : expr)
   | CTX_IfM (e0 : expr) (e2 : expr)
   | CTX_IfR (e0 : expr) (e1 : expr)
@@ -28,6 +28,20 @@ Inductive ctx_item :=
   | CTX_CaseL (e1 : expr) (e2 : expr)
   | CTX_CaseM (e0 : expr) (e2 : expr)
   | CTX_CaseR (e0 : expr) (e1 : expr)
+  (* Concurrency *)
+  | CTX_Fork
+  (* Heap *)
+  | CTX_Alloc
+  | CTX_Load
+  | CTX_StoreL (e2 : expr)
+  | CTX_StoreR (e1 : expr)
+  (* Compare-exchange and FAA *)
+  | CTX_CmpXchgL (e1 : expr) (e2 : expr)
+  | CTX_CmpXchgM (e0 : expr) (e2 : expr)
+  | CTX_CmpXchgR (e0 : expr) (e1 : expr)
+  | CTX_FAAL (e1 : expr) (e2 : expr)
+  | CTX_FAAM (e0 : expr) (e2 : expr)
+  | CTX_FAAR (e0 : expr) (e1 : expr)
   (* Recursive Types *)
   | CTX_Fold
   | CTX_Unfold
@@ -36,39 +50,49 @@ Inductive ctx_item :=
   | CTX_TApp
   (* Existential types *)
   (* | CTX_Pack *)
+  (* TODO: Unpack contexts are still relevant *)
   (* | CTX_UnpackL (e' : expr) *)
   (* | CTX_UnpackR (e : expr) *)
-  (* Concurrency *)
-  | CTX_Fork
-  (* Reference Types *)
-  | CTX_Alloc
-  | CTX_Load
-  | CTX_StoreL (e2 : expr)
-  | CTX_StoreR (e1 : expr)
-  (* Compare-exchange used for fine-grained concurrency *)
-  | CTX_CmpXchg_L (e1 : expr) (e2 : expr)
-  | CTX_CmpXchg_M (e0 : expr) (e2 : expr)
-  | CTX_CmpXchg_R (e0 : expr) (e1 : expr).
+.
 
 Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   match ctx with
+  (* Base lambda calculus *)
   | CTX_Rec f x => Rec f x e
   | CTX_AppL e2 => App e e2
   | CTX_AppR e1 => App e1 e
+  (* Base types and operations *)
+  | CTX_UnOp op => UnOp op e
+  | CTX_BinOpL op e2 => BinOp op e e2
+  | CTX_BinOpR op e1 => BinOp op e1 e
+  | CTX_IfL e1 e2 => If e e1 e2
+  | CTX_IfM e0 e2 => If e0 e e2
+  | CTX_IfR e0 e1 => If e0 e1 e
+  (* Products *)
   | CTX_PairL e2 => Pair e e2
   | CTX_PairR e1 => Pair e1 e
   | CTX_Fst => Fst e
   | CTX_Snd => Snd e
+  (* Sums *)
   | CTX_InjL => InjL e
   | CTX_InjR => InjR e
   | CTX_CaseL e1 e2 => Case e e1 e2
   | CTX_CaseM e0 e2 => Case e0 e e2
   | CTX_CaseR e0 e1 => Case e0 e1 e
-  | CTX_BinOpL op e2 => BinOp op e e2
-  | CTX_BinOpR op e1 => BinOp op e1 e
-  | CTX_IfL e1 e2 => If e e1 e2
-  | CTX_IfM e0 e2 => If e0 e e2
-  | CTX_IfR e0 e1 => If e0 e1 e
+  (* Concurrency *)
+  | CTX_Fork => Fork e
+  (* Heap & atomic CAS/FAA *)
+  | CTX_Alloc => Alloc e
+  | CTX_Load => Load e
+  | CTX_StoreL e2 => Store e e2
+  | CTX_StoreR e1 => Store e1 e
+  | CTX_CmpXchgL e1 e2 => CmpXchg e e1 e2
+  | CTX_CmpXchgM e0 e2 => CmpXchg e0 e e2
+  | CTX_CmpXchgR e0 e1 => CmpXchg e0 e1 e
+  | CTX_FAAL e1 e2 => FAA e e1 e2
+  | CTX_FAAM e0 e2 => FAA e0 e e2
+  | CTX_FAAR e0 e1 => FAA e0 e1 e
+  (* Recursive & polymorphic types *)
   | CTX_Fold => e
   | CTX_Unfold => rec_unfold e
   | CTX_TLam => Î›: e
@@ -76,14 +100,6 @@ Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
   (* | CTX_Pack => Pack e *)
   (* | CTX_UnpackL e1 => Unpack e e1 *)
   (* | CTX_UnpackR e0 => Unpack e0 e *)
-  | CTX_Fork => Fork e
-  | CTX_Alloc => Alloc e
-  | CTX_Load => Load e
-  | CTX_StoreL e2 => Store e e2
-  | CTX_StoreR e1 => Store e1 e
-  | CTX_CmpXchg_L e1 e2 => CmpXchg e e1 e2
-  | CTX_CmpXchg_M e0 e2 => CmpXchg e0 e e2
-  | CTX_CmpXchg_R e0 e1 => CmpXchg e0 e1 e
   end.
 
 Definition ctx := list ctx_item.
@@ -94,6 +110,7 @@ Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K.
 (** typed ctx *)
 Inductive typed_ctx_item :
     ctx_item â†’ stringmap type â†’ type â†’ stringmap type â†’ type â†’ Prop :=
+  (* Base lambda calculus *)
   | TP_CTX_Rec Î“ Ï„ Ï„' f x :
      typed_ctx_item (CTX_Rec f x) (<[f:=TArrow Ï„ Ï„']>(<[x:=Ï„]>Î“)) Ï„' Î“ (TArrow Ï„ Ï„')
   | TP_CTX_AppL Î“ e2 Ï„ Ï„' :
@@ -102,6 +119,33 @@ Inductive typed_ctx_item :
   | TP_CTX_AppR Î“ e1 Ï„ Ï„' :
      typed Î“ e1 (TArrow Ï„ Ï„') â†’
      typed_ctx_item (CTX_AppR e1) Î“ Ï„ Î“ Ï„'
+  (* Base types and operations *)
+  | TP_CTX_BinOpL_Nat op Î“ e2 Ï„ :
+     typed Î“ e2 TNat â†’
+     binop_nat_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpL op e2) Î“ TNat Î“ Ï„
+  | TP_CTX_BinOpR_Nat op e1 Î“ Ï„ :
+     typed Î“ e1 TNat â†’
+     binop_nat_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpR op e1) Î“ TNat Î“ Ï„
+  | TP_CTX_BinOpL_Bool op Î“ e2 Ï„ :
+     typed Î“ e2 TBool â†’
+     binop_bool_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpL op e2) Î“ TBool Î“ Ï„
+  | TP_CTX_BinOpR_Bool op e1 Î“ Ï„ :
+     typed Î“ e1 TBool â†’
+     binop_bool_res_type op = Some Ï„ â†’
+     typed_ctx_item (CTX_BinOpR op e1) Î“ TBool Î“ Ï„
+  | TP_CTX_IfL Î“ e1 e2 Ï„ :
+     typed Î“ e1 Ï„ â†’ typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_IfL e1 e2) Î“ (TBool) Î“ Ï„
+  | TP_CTX_IfM Î“ e0 e2 Ï„ :
+     typed Î“ e0 (TBool) â†’ typed Î“ e2 Ï„ â†’
+     typed_ctx_item (CTX_IfM e0 e2) Î“ Ï„ Î“ Ï„
+  | TP_CTX_IfR Î“ e0 e1 Ï„ :
+     typed Î“ e0 (TBool) â†’ typed Î“ e1 Ï„ â†’
+     typed_ctx_item (CTX_IfR e0 e1) Î“ Ï„ Î“ Ï„
+  (* Products *)
   | TP_CTX_PairL Î“ e2 Ï„ Ï„' :
      typed Î“ e2 Ï„' â†’
      typed_ctx_item (CTX_PairL e2) Î“ Ï„ Î“ (TProd Ï„ Ï„')
@@ -112,6 +156,7 @@ Inductive typed_ctx_item :
      typed_ctx_item CTX_Fst Î“ (TProd Ï„ Ï„') Î“ Ï„
   | TP_CTX_Snd Î“ Ï„ Ï„' :
      typed_ctx_item CTX_Snd Î“ (TProd Ï„ Ï„') Î“ Ï„'
+  (* Sums *)
   | TP_CTX_InjL Î“ Ï„ Ï„' :
      typed_ctx_item CTX_InjL Î“ Ï„ Î“ (TSum Ï„ Ï„')
   | TP_CTX_InjR Î“ Ï„ Ï„' :
@@ -125,49 +170,10 @@ Inductive typed_ctx_item :
   | TP_CTX_CaseR Î“ e0 e1 Ï„1 Ï„2 Ï„' :
      typed Î“ e0 (TSum Ï„1 Ï„2) â†’ typed Î“ e1 (TArrow Ï„1 Ï„') â†’
      typed_ctx_item (CTX_CaseR e0 e1) Î“ (TArrow Ï„2 Ï„') Î“ Ï„'
-  | TP_CTX_IfL Î“ e1 e2 Ï„ :
-     typed Î“ e1 Ï„ â†’ typed Î“ e2 Ï„ â†’
-     typed_ctx_item (CTX_IfL e1 e2) Î“ (TBool) Î“ Ï„
-  | TP_CTX_IfM Î“ e0 e2 Ï„ :
-     typed Î“ e0 (TBool) â†’ typed Î“ e2 Ï„ â†’
-     typed_ctx_item (CTX_IfM e0 e2) Î“ Ï„ Î“ Ï„
-  | TP_CTX_IfR Î“ e0 e1 Ï„ :
-     typed Î“ e0 (TBool) â†’ typed Î“ e1 Ï„ â†’
-     typed_ctx_item (CTX_IfR e0 e1) Î“ Ï„ Î“ Ï„
-  | TP_CTX_BinOpL_Nat op Î“ e2 Ï„ :
-     typed Î“ e2 TNat â†’
-     binop_nat_res_type op = Some Ï„ â†’
-     typed_ctx_item (CTX_BinOpL op e2) Î“ TNat Î“ Ï„
-  | TP_CTX_BinOpR_Nat op e1 Î“ Ï„ :
-     typed Î“ e1 TNat â†’
-     binop_nat_res_type op = Some Ï„ â†’
-     typed_ctx_item (CTX_BinOpR op e1) Î“ TNat Î“ Ï„
-  | TP_CTX_BinOpL_Bool op Î“ e2 Ï„ :
-     typed Î“ e2 TBool â†’
-     binop_bool_res_type op = Some Ï„ â†’
-     typed_ctx_item (CTX_BinOpL op e2) Î“ TBool Î“ Ï„
-  | TP_CTX_BinOpR_Bool op e1 Î“ Ï„ :
-     typed Î“ e1 TBool â†’
-     binop_bool_res_type op = Some Ï„ â†’
-     typed_ctx_item (CTX_BinOpR op e1) Î“ TBool Î“ Ï„
-  | TP_CTX_Fold Î“ Ï„ :
-     typed_ctx_item CTX_Fold Î“ Ï„.[(TRec Ï„)/] Î“ (TRec Ï„)
-  | TP_CTX_Unfold Î“ Ï„ :
-     typed_ctx_item CTX_Unfold Î“ (TRec Ï„) Î“ Ï„.[(TRec Ï„)/]
-  | TP_CTX_TLam Î“ Ï„ :
-     typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Î“) Ï„ Î“ (TForall Ï„)
-  | TP_CTX_TApp Î“ Ï„ Ï„' :
-     typed_ctx_item CTX_TApp Î“ (TForall Ï„) Î“ Ï„.[Ï„'/]
-  (* | TP_CTX_Pack Î“ Ï„ Ï„' : *)
-  (*    typed_ctx_item CTX_Pack Î“ Ï„.[Ï„'/] Î“ (TExists Ï„) *)
-  (* | TP_CTX_UnpackL e2 Î“ Ï„ Ï„2 : *)
-  (*    typed (subst (ren (+1)) <$> Î“) e2 (TArrow Ï„ (subst (ren (+1)) Ï„2)) â†’ *)
-  (*    typed_ctx_item (CTX_UnpackL e2) Î“ (TExists Ï„) Î“ Ï„2 *)
-  (* | TP_CTX_UnpackR e1 Î“ Ï„ Ï„2 : *)
-  (*    typed Î“ e1 (TExists Ï„) â†’ *)
-  (*    typed_ctx_item (CTX_UnpackR e1) (subst (ren (+1)) <$> Î“) (TArrow Ï„ (subst (ren (+1)) Ï„2))  Î“ Ï„2 *)
+  (* Concurrency *)
   | TP_CTX_Fork Î“ :
      typed_ctx_item CTX_Fork Î“ TUnit Î“ TUnit
+  (* Heap *)
   | TPCTX_Alloc Î“ Ï„ :
      typed_ctx_item CTX_Alloc Î“ Ï„ Î“ (Tref Ï„)
   | TP_CTX_Load Î“ Ï„ :
@@ -180,15 +186,33 @@ Inductive typed_ctx_item :
   | TP_CTX_CasL Î“ e1  e2 Ï„ :
      EqType Ï„ â†’ UnboxedType Ï„ â†’
      typed Î“ e1 Ï„ â†’ typed Î“ e2 Ï„ â†’
-     typed_ctx_item (CTX_CmpXchg_L e1 e2) Î“ (Tref Ï„) Î“ (TProd Ï„ TBool)
+     typed_ctx_item (CTX_CmpXchgL e1 e2) Î“ (Tref Ï„) Î“ (TProd Ï„ TBool)
   | TP_CTX_CasM Î“ e0 e2 Ï„ :
      EqType Ï„ â†’ UnboxedType Ï„ â†’
      typed Î“ e0 (Tref Ï„) â†’ typed Î“ e2 Ï„ â†’
-     typed_ctx_item (CTX_CmpXchg_M e0 e2) Î“ Ï„ Î“ (TProd Ï„ TBool)
+     typed_ctx_item (CTX_CmpXchgM e0 e2) Î“ Ï„ Î“ (TProd Ï„ TBool)
   | TP_CTX_CasR Î“ e0 e1 Ï„ :
      EqType Ï„ â†’ UnboxedType Ï„ â†’
      typed Î“ e0 (Tref Ï„) â†’ typed Î“ e1 Ï„ â†’
-     typed_ctx_item (CTX_CmpXchg_R e0 e1) Î“ Ï„ Î“ (TProd Ï„ TBool).
+     typed_ctx_item (CTX_CmpXchgR e0 e1) Î“ Ï„ Î“ (TProd Ï„ TBool)
+  (* Polymorphic & recursive types *)
+  | TP_CTX_Fold Î“ Ï„ :
+     typed_ctx_item CTX_Fold Î“ Ï„.[(TRec Ï„)/] Î“ (TRec Ï„)
+  | TP_CTX_Unfold Î“ Ï„ :
+     typed_ctx_item CTX_Unfold Î“ (TRec Ï„) Î“ Ï„.[(TRec Ï„)/]
+  | TP_CTX_TLam Î“ Ï„ :
+     typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Î“) Ï„ Î“ (TForall Ï„)
+  | TP_CTX_TApp Î“ Ï„ Ï„' :
+     typed_ctx_item CTX_TApp Î“ (TForall Ï„) Î“ Ï„.[Ï„'/]
+  (* | TP_CTX_Pack Î“ Ï„ Ï„' : *)
+  (*    typed_ctx_item CTX_Pack Î“ Ï„.[Ï„'/] Î“ (TExists Ï„) *)
+  (* | TP_CTX_UnpackL e2 Î“ Ï„ Ï„2 : *)
+  (*    typed (subst (ren (+1)) <$> Î“) e2 (TArrow Ï„ (subst (ren (+1)) Ï„2)) â†’ *)
+  (*    typed_ctx_item (CTX_UnpackL e2) Î“ (TExists Ï„) Î“ Ï„2 *)
+  (* | TP_CTX_UnpackR e1 Î“ Ï„ Ï„2 : *)
+  (*    typed Î“ e1 (TExists Ï„) â†’ *)
+  (*    typed_ctx_item (CTX_UnpackR e1) (subst (ren (+1)) <$> Î“) (TArrow Ï„ (subst (ren (+1)) Ï„2))  Î“ Ï„2 *)
+.
 
 Inductive typed_ctx: ctx â†’ stringmap type â†’ type â†’ stringmap type â†’ type â†’ Prop :=
   | TPCTX_nil Î“ Ï„ :
@@ -288,6 +312,27 @@ Section bin_log_related_under_typed_ctx.
       + iApply (bin_log_related_app _ _ _ _ _ _ Ï„2 with "[]").
         by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_nat_binop with "[]");
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_nat_binop with "[]");
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_bool_binop with "[]");
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_bool_binop with "[]");
+          try (by iApply fundamental); eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_if with "[] []");
+          try by iApply fundamental.
+        iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_pair with "[]").
         iApply (IHK with "[Hrel]"); auto.
         by iApply fundamental.
@@ -314,25 +359,25 @@ Section bin_log_related_under_typed_ctx.
         by iApply fundamental.
         by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_if with "[] []");
-          try by iApply fundamental.
+      + iApply (bin_log_related_fork with "[]").
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_if with "[] []");
-          try by iApply fundamental.
+      + iApply (bin_log_related_alloc with "[]").
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_if with "[] []");
+      + iApply (bin_log_related_load with "[]").
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_store with "[]");
           try by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_nat_binop with "[]");
-          try (by iApply fundamental); eauto.
+      + iApply (bin_log_related_store with "[]");
+          try by iApply fundamental.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_nat_binop with "[]");
+      + iApply (bin_log_related_CmpXchg with "[] []");
           try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_bool_binop with "[]");
+      + iApply (bin_log_related_CmpXchg with "[] []");
           try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_bool_binop with "[]");
+      + iApply (bin_log_related_CmpXchg with "[] []");
           try (by iApply fundamental); eauto.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_fold with "[]").
@@ -350,26 +395,5 @@ Section bin_log_related_under_typed_ctx.
       (*   iApply (IHK with "[Hrel]"); auto. *)
       (* + iApply bin_log_related_unpack; try by (iIntros; fundamental). *)
       (*   iIntros. iApply (IHK with "[Hrel]"); auto. *)
-      + iApply (bin_log_related_fork with "[]").
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_alloc with "[]").
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_load with "[]").
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_store with "[]");
-          try by iApply fundamental.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_store with "[]");
-          try by iApply fundamental.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_CmpXchg with "[] []");
-          try (by iApply fundamental); eauto.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_CmpXchg with "[] []");
-          try (by iApply fundamental); eauto.
-        iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_CmpXchg with "[] []");
-          try (by iApply fundamental); eauto.
-        iApply (IHK with "[Hrel]"); auto.
   Qed.
 End bin_log_related_under_typed_ctx.
-- 
GitLab