From bf7b1bc43005cdccfd2a64aa0acfd6eb3d879fa0 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 12 Mar 2019 15:30:59 +0100
Subject: [PATCH] move some stuff to the lib folder

---
 _CoqProject                          | 8 +++++---
 theories/examples/generative.v       | 2 +-
 theories/examples/or.v               | 3 ++-
 theories/{examples => lib}/Y.v       | 0
 theories/{examples => lib}/counter.v | 2 +-
 theories/{examples => lib}/lock.v    | 0
 theories/logic/model.v               | 9 +--------
 theories/typing/types.v              | 2 +-
 8 files changed, 11 insertions(+), 15 deletions(-)
 rename theories/{examples => lib}/Y.v (100%)
 rename theories/{examples => lib}/counter.v (99%)
 rename theories/{examples => lib}/lock.v (100%)

diff --git a/_CoqProject b/_CoqProject
index 717d5a6..bb31c07 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,9 +27,11 @@ theories/proofmode.v
 theories/tests/tp_tests.v
 theories/tests/proofmode_tests.v
 
-theories/examples/lock.v
-theories/examples/counter.v
+theories/lib/lock.v
+theories/lib/counter.v
+theories/lib/Y.v
+
 theories/examples/bit.v
-theories/examples/Y.v
 theories/examples/or.v
 theories/examples/generative.v
+
diff --git a/theories/examples/generative.v b/theories/examples/generative.v
index 76573b3..d064b77 100644
--- a/theories/examples/generative.v
+++ b/theories/examples/generative.v
@@ -6,7 +6,7 @@ Those are mostly "generative ADTs". *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Export par.
 From reloc Require Export proofmode prelude.bijections.
-From reloc.examples Require Export counter lock.
+From reloc.lib Require Export counter lock.
 From reloc.typing Require Export interp soundness.
 
 (** Using references for name generation *)
diff --git a/theories/examples/or.v b/theories/examples/or.v
index 4c3e4b1..c7888b3 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -79,6 +79,8 @@ Section rules.
       rel_load_r. repeat rel_pure_r. eauto with iFrame.
   Qed.
 
+  Opaque or.
+
   (** Compatibility rule *)
   Lemma or_compatible e1 e2 e1' e2' A :
     (REL e1 << e1' : () → A) -∗
@@ -89,7 +91,6 @@ Section rules.
     rel_bind_l e2. rel_bind_r e2'.
     iApply (refines_bind with "H2").
     iIntros (v2 v2') "#Hv2".
-    (* ^ TODO the arrow interpretation gets unfolded here *)
     rel_bind_l e1. rel_bind_r e1'.
     iApply (refines_bind with "H1").
     iIntros (v1 v1') "#Hv1". iSimpl.
diff --git a/theories/examples/Y.v b/theories/lib/Y.v
similarity index 100%
rename from theories/examples/Y.v
rename to theories/lib/Y.v
diff --git a/theories/examples/counter.v b/theories/lib/counter.v
similarity index 99%
rename from theories/examples/counter.v
rename to theories/lib/counter.v
index 1fa3816..7b7e231 100644
--- a/theories/examples/counter.v
+++ b/theories/lib/counter.v
@@ -1,7 +1,7 @@
 From reloc Require Export proofmode.
 From reloc.typing Require Export types interp.
 From reloc.logic Require Import compatibility.
-From reloc.examples Require Import lock.
+From reloc.lib Require Import lock.
 From reloc.typing Require Import soundness.
 
 Definition CG_increment : val := λ: "x" "l",
diff --git a/theories/examples/lock.v b/theories/lib/lock.v
similarity index 100%
rename from theories/examples/lock.v
rename to theories/lib/lock.v
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 843a067..08bad25 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -139,7 +139,7 @@ Section semtypes.
 
 End semtypes.
 
-(* Nice notations *)
+(** Nice notations *)
 Notation "()" := lty2_unit : lty_scope.
 Infix "→" := lty2_arr : lty_scope.
 Infix "×" := lty2_prod (at level 80) : lty_scope.
@@ -242,13 +242,6 @@ End related_facts.
 Section monadic.
   Context `{relocG Σ}.
 
-  (* Lemma refines_ret_expr E e1 e2 A : *)
-  (*   interp_expr E e1 e2 A -∗ REL e1 << e2 @ E : A. *)
-  (* Proof. *)
-  (*   iIntros "HA". rewrite refines_eq /refines_def. *)
-  (*   eauto with iFrame. *)
-  (* Qed. *)
-
   Lemma refines_bind K K' E A A' e e' :
     (REL e << e' @ E : A) -∗
     (∀ v v', A v v' -∗
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 8118cce..a4b524c 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -2,7 +2,7 @@
 (** (Syntactic) Typing for System F_mu_ref with existential types and concurrency *)
 From stdpp Require Export stringmap.
 From iris.heap_lang Require Export lang notation metatheory.
-From Autosubst Require Import Autosubst.
+From Autosubst Require Export Autosubst.
 
 (** * Types *)
 Inductive type :=
-- 
GitLab