From 354cf991b561ba97035ec74781433df7949ccefe Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Jun 2020 00:30:29 +0200
Subject: [PATCH] More type notations.

---
 theories/examples/bit.v                 |  3 +--
 theories/examples/cell.v                |  4 +--
 theories/examples/coinflip.v            |  4 +--
 theories/examples/namegen.v             |  3 +--
 theories/examples/or.v                  | 34 ++++++++++++-------------
 theories/examples/stack/refinement.v    |  4 +--
 theories/examples/symbol.v              |  8 +++---
 theories/examples/ticket_lock.v         |  4 +--
 theories/examples/various.v             |  4 +--
 theories/lib/counter.v                  |  2 +-
 theories/typing/contextual_refinement.v |  6 ++---
 theories/typing/fundamental.v           | 10 ++++----
 theories/typing/types.v                 | 32 ++++++++++++-----------
 13 files changed, 55 insertions(+), 63 deletions(-)

diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index 8138d01..50fce0a 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -15,8 +15,7 @@ Definition flip_nat : val := λ: "n",
 Definition bit_nat : expr :=
   (#1, flip_nat, (λ: "b", "b" = #1)).
 
-Definition bitτ : type :=
-  ∃: (TVar 0) * (TVar 0 → TVar 0) * (TVar 0 → TBool).
+Definition bitτ : type := ∃: #0 * (#0 → #0) * (#0 → TBool).
 
 Section bit_refinement.
   Context `{!relocG Σ}.
diff --git a/theories/examples/cell.v b/theories/examples/cell.v
index 9936ba5..bbdbc55 100644
--- a/theories/examples/cell.v
+++ b/theories/examples/cell.v
@@ -7,9 +7,7 @@ From reloc.lib Require Export lock.
 (** A type of cells -- basically an abstract type of references. *)
 (* ∀ α, ∃ β, (α → β) × (β → α) × (β → α → ())  *)
 Definition cellτ : type :=
-  ∀: ∃: (TVar 1 → TVar 0)
-       * (TVar 0 → TVar 1)
-       * (TVar 0 → TVar 1 → TUnit).
+  ∀: ∃: (#1 → #0) * (#0 → #1) * (#0 → #1 → ()).
 (** We show that the canonical implementation `cell1` is equivalent to
 an implementation using two alternating slots *)
 
diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index eed47d8..659d043 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -333,7 +333,7 @@ Section proofs.
 End proofs.
 
 Theorem coin_lazy_eager_ctx_refinement :
-  ∅ ⊨ coin2 ≤ctx≤ coin1 : (TUnit → TBool) * (TUnit → TUnit).
+  ∅ ⊨ coin2 ≤ctx≤ coin1 : (() → TBool) * (() → ()).
 Proof.
   eapply (ctx_refines_transitive ∅ _).
   - eapply (refines_sound #[relocΣ; lockΣ]).
@@ -343,7 +343,7 @@ Proof.
 Qed.
 
 Theorem coin_eager_lazy_ctx_refinement :
-  ∅ ⊨ coin1 ≤ctx≤ coin2 : (TUnit → TBool) * (TUnit → TUnit).
+  ∅ ⊨ coin1 ≤ctx≤ coin2 : (() → TBool) * (() → ()).
 Proof.
   eapply (ctx_refines_transitive ∅ _).
   - eapply (refines_sound #[relocΣ; lockΣ]).
diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index aa759d1..2f86e68 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -11,8 +11,7 @@ version uses integers. *)
 (*       ^ new name  ^                            *)
 (*                   | compare names for equality *)
 Definition nameGenTy : type :=
-  ∃: (TUnit → TVar 0)
-   * (TVar 0 → TVar 0 → TBool).
+  ∃: (() → #0) * (#0 → #0 → TBool).
 
 (* TODO: cannot be a value *)
 Definition nameGen1 : expr :=
diff --git a/theories/examples/or.v b/theories/examples/or.v
index 2b70b28..f09352a 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -292,16 +292,16 @@ End rules.
 (** Separately, we prove that the ordering induced by ⊕ conincides with
     contextual refinement. *)
 Lemma Seq_typed Γ e1 e2 τ :
-  Γ ⊢ₜ e1 : TUnit →
+  Γ ⊢ₜ e1 : () →
   Γ ⊢ₜ e2 : τ →
   Γ ⊢ₜ (e1;;e2) : τ.
 Proof. by repeat (econstructor; eauto). Qed.
 
 Lemma or_equiv_refines_1 e t :
-  (∅ ⊢ₜ e : TUnit) →
-  (∅ ⊢ₜ t : TUnit) →
-  (∅ ⊨ e ≤ctx≤ t : TUnit) →
-  (∅ ⊨ (e ⊕ t) =ctx= t : TUnit).
+  (∅ ⊢ₜ e : ()) →
+  (∅ ⊢ₜ t : ()) →
+  (∅ ⊨ e ≤ctx≤ t : ()) →
+  (∅ ⊨ (e ⊕ t) =ctx= t : ()).
 Proof.
   intros Te Tt Het. split; last first.
   - eapply (ctx_refines_transitive _ _ _ (t ⊕ e)%V).
@@ -311,11 +311,11 @@ Proof.
       by iApply refines_typed.
     + eapply (refines_sound relocΣ).
       iIntros (? Δ). rel_pures_r.
-      iApply or_comm; by iApply (refines_typed TUnit []).
+      iApply or_comm; by iApply (refines_typed () []).
   - eapply (ctx_refines_transitive _ _ _ (t ⊕ t)%E).
     + ctx_bind_l e.
       ctx_bind_r t.
-      eapply (ctx_refines_congruence ∅ _ _ TUnit);
+      eapply (ctx_refines_congruence ∅ _ _ ());
         last eassumption.
       { cbn.
         econstructor; cbn; eauto.
@@ -337,26 +337,26 @@ Proof.
           + econstructor; cbn; eauto.
             2:{ econstructor; cbn; eauto. }
             enough (typed_ctx_item (CTX_Rec <> <>)
-                       (binder_insert BAnon (TUnit → TUnit)%ty
-                                      (binder_insert BAnon TUnit (∅ : stringmap type)))
-                       TUnit ∅ (TUnit → TUnit)).
+                       (binder_insert BAnon (() → ())%ty
+                                      (binder_insert BAnon ()%ty (∅ : stringmap type)))
+                       () ∅ (() → ())).
             { by simpl in *. }
-            eapply (TP_CTX_Rec ∅ TUnit TUnit BAnon BAnon). }
+            eapply (TP_CTX_Rec ∅ () () BAnon BAnon). }
     + eapply (refines_sound relocΣ).
       iIntros (? Δ). rel_pures_l.
-      iApply or_idemp_l. by iApply (refines_typed TUnit []).
+      iApply or_idemp_l. by iApply (refines_typed () []).
 Qed.
 
 Lemma or_equiv_refines_2 e t :
-  (∅ ⊢ₜ e : TUnit) →
-  (∅ ⊢ₜ t : TUnit) →
-  (∅ ⊨ (e ⊕ t) =ctx= t : TUnit) →
-  (∅ ⊨ e ≤ctx≤ t : TUnit).
+  (∅ ⊢ₜ e : ()) →
+  (∅ ⊢ₜ t : ()) →
+  (∅ ⊨ (e ⊕ t) =ctx= t : ()) →
+  (∅ ⊨ e ≤ctx≤ t : ()).
 Proof.
   intros Te Tt [Het1 Het2].
   eapply (ctx_refines_transitive _ _ _ (e ⊕ t)%E); last assumption.
   eapply (refines_sound relocΣ).
   iIntros (? Δ).
   rel_pures_r. iApply or_choice_1_r.
-  by iApply (refines_typed TUnit []).
+  by iApply (refines_typed () []).
 Qed.
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index a26b596..c810915 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -208,9 +208,7 @@ End proof.
 Open Scope nat.
 Theorem stack_ctx_refinement :
   ∅ ⊨ FG_stack ≤ctx≤ CG_stack :
-    ∀: ∃: (TUnit → TVar 0)
-         * (TVar 0 → TUnit + TVar 1)
-         * (TVar 0 → TVar 1 → TUnit).
+      ∀: ∃: (() → #0) * (#0 → () + #1) * (#0 → #1 → ()).
 Proof.
   eapply (refines_sound relocΣ).
   iIntros (? ?).
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 5d173f2..d5eace0 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -376,12 +376,10 @@ End proof.
 
 Open Scope nat.
 Definition symbolτ : type :=
-  ∃: (TVar 0 → TVar 0 → TBool)
-   * (TNat → TVar 0)
-   * (TVar 0 → TNat).
+  ∃: (#0 → #0 → TBool) * (TNat → #0) * (#0 → TNat).
 
 Theorem symbol_ctx_refinement1 :
-  ∅ ⊨ symbol1 ≤ctx≤ symbol2 : TUnit → symbolτ.
+  ∅ ⊨ symbol1 ≤ctx≤ symbol2 : () → symbolτ.
 Proof.
   pose (Σ := #[relocΣ;msizeΣ;lockΣ]).
   eapply (refines_sound Σ).
@@ -389,7 +387,7 @@ Proof.
 Qed.
 
 Theorem symbol_ctx_refinement2 :
-  ∅ ⊨ symbol2 ≤ctx≤ symbol1 : TUnit → symbolτ.
+  ∅ ⊨ symbol2 ≤ctx≤ symbol1 : () → symbolτ.
 Proof.
   pose (Σ := #[relocΣ;msizeΣ;lockΣ]).
   eapply (refines_sound Σ).
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 3230b98..d3eef81 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -357,9 +357,7 @@ End refinement.
 
 Open Scope nat.
 Definition lockT : type :=
-  ∃: (TUnit → TVar 0)
-   * (TVar 0 → TUnit)
-   * (TVar 0 → TUnit).
+  ∃: (() → #0) * (#0 → ()) * (#0 → ()).
 
 Lemma ticket_lock_ctx_refinement :
   ∅ ⊨   (newlock, acquire, release)
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 26dc81d..1bae627 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -350,8 +350,8 @@ Section proofs.
   Qed.
 
   (** Higher-order profiling *)
-  Definition Ï„g := TArrow TUnit TUnit.
-  Definition Ï„f := TArrow Ï„g TUnit.
+  Definition Ï„g := TArrow () ().
+  Definition Ï„f := TArrow Ï„g ().
   Definition p : val := λ: "g", let: "c" := ref #0 in
                                 (λ: <>, FG_increment "c";; "g" #(), λ: <>, !"c").
   (** The idea for the invariant is that we have to states:
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index 9e65ae7..b35129a 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -226,7 +226,7 @@ End CG_Counter.
 
 Theorem counter_ctx_refinement :
   ∅ ⊨ FG_counter ≤ctx≤ CG_counter :
-         TUnit → ((TUnit → TNat) * (TUnit → TNat)).
+         () → ((() → TNat) * (() → TNat)).
 Proof.
   eapply (refines_sound relocΣ).
   iIntros (? Δ). iApply FG_CG_counter_refinement.
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index ea12f0c..d92f934 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -168,17 +168,17 @@ Inductive typed_ctx_item :
      typed_ctx_item (CTX_CaseR e0 e1) Γ (TArrow τ2 τ') Γ τ'
   (* Concurrency *)
   | TP_CTX_Fork Γ :
-     typed_ctx_item CTX_Fork Γ TUnit Γ TUnit
+     typed_ctx_item CTX_Fork Γ () Γ ()
   (* Heap *)
   | TPCTX_Alloc Γ τ :
      typed_ctx_item CTX_Alloc Γ τ Γ (Tref τ)
   | TP_CTX_Load Γ τ :
      typed_ctx_item CTX_Load Γ (Tref τ) Γ τ
   | TP_CTX_StoreL Γ e2 τ :
-     typed Γ e2 τ → typed_ctx_item (CTX_StoreL e2) Γ (Tref τ) Γ TUnit
+     typed Γ e2 τ → typed_ctx_item (CTX_StoreL e2) Γ (Tref τ) Γ ()
   | TP_CTX_StoreR Γ e1 τ :
      typed Γ e1 (Tref τ) →
-     typed_ctx_item (CTX_StoreR e1) Γ τ Γ TUnit
+     typed_ctx_item (CTX_StoreR e1) Γ τ Γ ()
   | TP_CTX_FAAL Γ e2 :
      Γ ⊢ₜ e2 : TNat →
      typed_ctx_item (CTX_FAAL e2) Γ (Tref TNat) Γ TNat
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 2eec8e2..e60a907 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -36,7 +36,7 @@ Section fundamental.
     by iApply refines_ret.
   Qed.
 
-  Lemma bin_log_related_unit Δ Γ : ⊢ {Δ;Γ} ⊨ #() ≤log≤ #() : TUnit.
+  Lemma bin_log_related_unit Δ Γ : ⊢ {Δ;Γ} ⊨ #() ≤log≤ #() : ().
   Proof. value_case. Qed.
 
   Lemma bin_log_related_nat Δ Γ (n : nat) : ⊢ {Δ;Γ} ⊨ #n ≤log≤ #n : TNat.
@@ -125,8 +125,8 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_fork Δ Γ e e' :
-    ({Δ;Γ} ⊨ e ≤log≤ e' : TUnit) -∗
-    {Δ;Γ} ⊨ Fork e ≤log≤ Fork e' : TUnit.
+    ({Δ;Γ} ⊨ e ≤log≤ e' : ()) -∗
+    {Δ;Γ} ⊨ Fork e ≤log≤ Fork e' : ().
   Proof.
     iIntros "IH".
     intro_clause.
@@ -166,7 +166,7 @@ Section fundamental.
     {τi::Δ;⤉Γ} ⊨ (TApp e) ≤log≤ (TApp e') : τ.
   Proof.
     iIntros "IH". intro_clause.
-    iApply (bin_log_related_app _ _ e #() e' #() TUnit Ï„ with "[IH] [] Hvs").
+    iApply (bin_log_related_app _ _ e #() e' #() () Ï„ with "[IH] [] Hvs").
     - iClear (vs) "Hvs". intro_clause.
       rewrite interp_ren.
       iSpecialize ("IH" with "Hvs").
@@ -265,7 +265,7 @@ Section fundamental.
   Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
     ({Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ) -∗
     ({Δ;Γ} ⊨ e2 ≤log≤ e2' : τ) -∗
-    {Δ;Γ} ⊨ Store e1 e2 ≤log≤ Store e1' e2' : TUnit.
+    {Δ;Γ} ⊨ Store e1 e2 ≤log≤ Store e1' e2' : ().
   Proof.
     iIntros "IH1 IH2".
     intro_clause.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index a3c6ded..6df35ff 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -53,6 +53,8 @@ Fixpoint binop_bool_res_type (op : bin_op) : option type :=
 
 Delimit Scope FType_scope with ty.
 Bind Scope FType_scope with type.
+Notation "()" := TUnit : FType_scope.
+Notation "# x" := (TVar x) : FType_scope.
 Infix "*" := TProd : FType_scope.
 Notation "(*)" := TProd (only parsing) : FType_scope.
 Infix "+" := TSum : FType_scope.
@@ -107,7 +109,7 @@ Inductive typed : stringmap type → expr → type → Prop :=
       ⊢ᵥ v : τ →
       Γ ⊢ₜ Val v : τ
   | Unit_typed Γ :
-      Γ ⊢ₜ #() : TUnit
+      Γ ⊢ₜ #() : ()
   | Nat_typed Γ (n : nat) :
       Γ ⊢ₜ #n : TNat
   | Bool_typed Γ (b : bool) :
@@ -121,7 +123,7 @@ Inductive typed : stringmap type → expr → type → Prop :=
      binop_bool_res_type op = Some τ →
      Γ ⊢ₜ BinOp op e1 e2 : τ
   | RefEq_typed Γ e1 e2 τ :
-     Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : Tref τ →
+     Γ ⊢ₜ e1 : ref τ → Γ ⊢ₜ e2 : ref τ →
      Γ ⊢ₜ BinOp EqOp e1 e2 : TBool
   | Pair_typed Γ e1 e2 τ1 τ2 :
       Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 →
@@ -174,38 +176,38 @@ Inductive typed : stringmap type → expr → type → Prop :=
       Γ ⊢ₜ e1 : (∃: τ) →
       <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (Autosubst_Classes.subst (ren (+1)) τ2) →
       Γ ⊢ₜ (unpack: x := e1 in e2) : τ2
-  | TFork Γ e : Γ ⊢ₜ e : TUnit → Γ ⊢ₜ Fork e : TUnit
-  | TAlloc Γ e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ
-  | TLoad Γ e τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ Load e : τ
-  | TStore Γ e e' τ : Γ ⊢ₜ e : Tref τ → Γ ⊢ₜ e' : τ → Γ ⊢ₜ Store e e' : TUnit
+  | TFork Γ e : Γ ⊢ₜ e : () → Γ ⊢ₜ Fork e : ()
+  | TAlloc Γ e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : ref τ
+  | TLoad Γ e τ : Γ ⊢ₜ e : ref τ → Γ ⊢ₜ Load e : τ
+  | TStore Γ e e' τ : Γ ⊢ₜ e : ref τ → Γ ⊢ₜ e' : τ → Γ ⊢ₜ Store e e' : ()
   | TFAA Γ e1 e2 :
-     Γ ⊢ₜ e1 : Tref TNat →
+     Γ ⊢ₜ e1 : ref TNat →
      Γ ⊢ₜ e2 : TNat →
      Γ ⊢ₜ FAA e1 e2 : TNat
   | TCmpXchg Γ e1 e2 e3 τ :
      EqType τ → UnboxedType τ →
-     Γ ⊢ₜ e1 : Tref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
-     Γ ⊢ₜ CmpXchg e1 e2 e3 : TProd τ TBool
+     Γ ⊢ₜ e1 : ref τ → Γ ⊢ₜ e2 : τ → Γ ⊢ₜ e3 : τ →
+     Γ ⊢ₜ CmpXchg e1 e2 e3 : τ * TBool
 with val_typed : val → type → Prop :=
-  | Unit_val_typed : ⊢ᵥ #() : TUnit
+  | Unit_val_typed : ⊢ᵥ #() : ()
   | Nat_val_typed (n : nat) : ⊢ᵥ #n : TNat
   | Bool_val_typed (b : bool) : ⊢ᵥ #b : TBool
   | Pair_val_typed v1 v2 Ï„1 Ï„2 :
       ⊢ᵥ v1 : τ1 →
       ⊢ᵥ v2 : τ2 →
-      ⊢ᵥ PairV v1 v2 : TProd τ1 τ2
+      ⊢ᵥ PairV v1 v2 : (τ1 * τ2)
   | InjL_val_typed v Ï„1 Ï„2 :
       ⊢ᵥ v : τ1 →
-      ⊢ᵥ InjLV v : TSum τ1 τ2
+      ⊢ᵥ InjLV v : (τ1 + τ2)
   | InjR_val_typed v Ï„1 Ï„2 :
       ⊢ᵥ v : τ2 →
-      ⊢ᵥ InjRV v : TSum τ1 τ2
+      ⊢ᵥ InjRV v : (τ1 + τ2)
   | Rec_val_typed f x e Ï„1 Ï„2 :
      <[f:=TArrow τ1 τ2]>(<[x:=τ1]>∅) ⊢ₜ e : τ2 →
-     ⊢ᵥ RecV f x e : TArrow τ1 τ2
+     ⊢ᵥ RecV f x e : (τ1 → τ2)
   | TLam_val_typed e Ï„ :
      ∅ ⊢ₜ e : τ →
-     ⊢ᵥ (Λ: e) : TForall τ
+     ⊢ᵥ (Λ: e) : (∀: τ)
 where "Γ ⊢ₜ e : τ" := (typed Γ e τ)
 and "⊢ᵥ e : τ" := (val_typed e τ).
 
-- 
GitLab