From 1a35e3e1ccc23005cb220002ed5e1ec09184f742 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 11 Feb 2022 18:24:02 -0600 Subject: [PATCH] Finished the typechecker for fully type-annotated programs --- prototyping/Everything.agda | 8 ++ prototyping/Luau/Addr.agda | 5 +- prototyping/Luau/AddrCtxt.agda | 5 +- prototyping/Luau/Syntax.agda | 3 +- prototyping/Luau/TypeCheck.agda | 24 ++--- prototyping/Luau/Var.agda | 8 +- prototyping/Luau/VarCtxt.agda | 15 ++- prototyping/Properties.agda | 4 + prototyping/Properties/Contradiction.agda | 9 ++ prototyping/Properties/Dec.agda | 4 +- prototyping/Properties/Equality.agda | 17 +++ prototyping/Properties/TypeCheck.agda | 126 +++++----------------- 12 files changed, 96 insertions(+), 132 deletions(-) create mode 100644 prototyping/Everything.agda create mode 100644 prototyping/Properties/Contradiction.agda create mode 100644 prototyping/Properties/Equality.agda diff --git a/prototyping/Everything.agda b/prototyping/Everything.agda new file mode 100644 index 00000000..d8a1fd5a --- /dev/null +++ b/prototyping/Everything.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --rewriting #-} + +module Everything where + +import Examples +import Properties +import PrettyPrinter +import Interpreter diff --git a/prototyping/Luau/Addr.agda b/prototyping/Luau/Addr.agda index c1978047..b6f989f5 100644 --- a/prototyping/Luau/Addr.agda +++ b/prototyping/Luau/Addr.agda @@ -5,13 +5,14 @@ open import Agda.Builtin.Equality using (_≡_) open import Agda.Builtin.Nat using (Nat; _==_) open import Agda.Builtin.String using (String) open import Agda.Builtin.TrustMe using (primTrustMe) -open import Properties.Dec using (Dec; yes; no; ⊥) +open import Properties.Dec using (Dec; yes; no) +open import Properties.Equality using (_≢_) Addr : Set Addr = Nat _≡ᴬ_ : (a b : Addr) → Dec (a ≡ b) a ≡ᴬ b with a == b -a ≡ᴬ b | false = no p where postulate p : (a ≡ b) → ⊥ +a ≡ᴬ b | false = no p where postulate p : (a ≢ b) a ≡ᴬ b | true = yes primTrustMe diff --git a/prototyping/Luau/AddrCtxt.agda b/prototyping/Luau/AddrCtxt.agda index b19e784e..b3e9cb52 100644 --- a/prototyping/Luau/AddrCtxt.agda +++ b/prototyping/Luau/AddrCtxt.agda @@ -4,6 +4,7 @@ open import Luau.Type using (Type) open import Luau.Addr using (Addr) open import FFI.Data.Vector using (Vector; empty; lookup) open import FFI.Data.Maybe using (Maybe; just; nothing) +open import Luau.VarCtxt using (orNone) AddrCtxt : Set AddrCtxt = Vector Type @@ -11,5 +12,5 @@ AddrCtxt = Vector Type ∅ : AddrCtxt ∅ = empty -_[_] : AddrCtxt → Addr → Maybe Type -_[_] = lookup +_[_] : AddrCtxt → Addr → Type +Σ [ a ] = orNone(lookup Σ a) diff --git a/prototyping/Luau/Syntax.agda b/prototyping/Luau/Syntax.agda index 3707e948..1edfa4d3 100644 --- a/prototyping/Luau/Syntax.agda +++ b/prototyping/Luau/Syntax.agda @@ -1,8 +1,7 @@ module Luau.Syntax where open import Agda.Builtin.Equality using (_≡_) -open import Properties.Dec using (⊥) -open import Luau.Var using (Var; anon) +open import Luau.Var using (Var) open import Luau.Addr using (Addr) open import Luau.Type using (Type) diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda index ad1c8d4e..8818851a 100644 --- a/prototyping/Luau/TypeCheck.agda +++ b/prototyping/Luau/TypeCheck.agda @@ -36,12 +36,12 @@ data _▷_⊢ᴮ_∋_∈_⊣_ where ---------------------------------------------------------- Σ ▷ Γ ⊢ᴮ S ∋ local var x ∈ T ← M ∙ B ∈ V ⊣ (Δ₁ ⋒ (Δ₂ ⊝ x)) - function : ∀ {Σ f x B C S T U V Γ Δ₁ Δ₂} → + function : ∀ {Σ f x B C S T U V W Γ Δ₁ Δ₂} → - Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ any ∋ C ∈ U ⊣ Δ₁ → - Σ ▷ (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ S ∋ B ∈ V ⊣ Δ₂ → + Σ ▷ (Γ ⊕ x ↦ T) ⊢ᴮ U ∋ C ∈ V ⊣ Δ₁ → + Σ ▷ (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ S ∋ B ∈ W ⊣ Δ₂ → --------------------------------------------------------------------------------- - Σ ▷ Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ V ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) + Σ ▷ Γ ⊢ᴮ S ∋ function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B ∈ W ⊣ ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) data _▷_⊢ᴱ_∋_∈_⊣_ where @@ -52,13 +52,13 @@ data _▷_⊢ᴱ_∋_∈_⊣_ where var : ∀ x {Σ S T Γ} → - just T ≡ Γ [ x ]ⱽ → + T ≡ Γ [ x ]ⱽ → ---------------------------- Σ ▷ Γ ⊢ᴱ S ∋ var x ∈ T ⊣ (x ↦ S) addr : ∀ a {Σ S T Γ} → - just T ≡ Σ [ a ]ᴬ → + T ≡ Σ [ a ]ᴬ → ---------------------------- Σ ▷ Γ ⊢ᴱ S ∋ addr a ∈ T ⊣ ∅ @@ -81,18 +81,18 @@ data _▷_⊢ᴱ_∋_∈_⊣_ where ---------------------------------------------------- Σ ▷ Γ ⊢ᴱ S ∋ (block b is B end) ∈ T ⊣ Δ -data _▷_∈_ (Σ : AddrCtxt) : Maybe (HeapValue yes) → (Maybe Type) → Set where +data _▷_∈_ (Σ : AddrCtxt) : Maybe (HeapValue yes) → Type → Set where - nothing : + nothing : ∀ {T} → - --------------------- - Σ ▷ nothing ∈ nothing + --------------- + Σ ▷ nothing ∈ T function : ∀ {f x B T U V W} → Σ ▷ (x ↦ T) ⊢ᴮ U ∋ B ∈ V ⊣ (x ↦ W) → - -------------------------------------------------------------- - Σ ▷ just (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ just (T ⇒ U) + --------------------------------------------------------- + Σ ▷ just (function f ⟨ var x ∈ T ⟩∈ U is B end) ∈ (T ⇒ U) data _▷_✓ (Σ : AddrCtxt) (H : Heap yes) : Set where diff --git a/prototyping/Luau/Var.agda b/prototyping/Luau/Var.agda index a2096975..23d8b56e 100644 --- a/prototyping/Luau/Var.agda +++ b/prototyping/Luau/Var.agda @@ -4,15 +4,13 @@ open import Agda.Builtin.Bool using (true; false) open import Agda.Builtin.Equality using (_≡_) open import Agda.Builtin.String using (String; primStringEquality) open import Agda.Builtin.TrustMe using (primTrustMe) -open import Properties.Dec using (Dec; yes; no; ⊥) +open import Properties.Dec using (Dec; yes; no) +open import Properties.Equality using (_≢_) Var : Set Var = String _≡ⱽ_ : (a b : Var) → Dec (a ≡ b) a ≡ⱽ b with primStringEquality a b -a ≡ⱽ b | false = no p where postulate p : (a ≡ b) → ⊥ +a ≡ⱽ b | false = no p where postulate p : (a ≢ b) a ≡ⱽ b | true = yes primTrustMe - -anon : Var -anon = "(anonymous)" diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda index 4db495c6..04a2718c 100644 --- a/prototyping/Luau/VarCtxt.agda +++ b/prototyping/Luau/VarCtxt.agda @@ -1,10 +1,15 @@ module Luau.VarCtxt where open import Agda.Builtin.Equality using (_≡_) -open import Luau.Type using (Type; _∪_; _∩_) +open import Luau.Type using (Type; none; _∪_; _∩_) open import Luau.Var using (Var) open import FFI.Data.Aeson using (KeyMap; Key; empty; unionWith; singleton; insert; delete; lookup; fromString; lookup-insert) open import FFI.Data.Maybe using (Maybe; just; nothing) +open import Properties.Equality using (cong) + +orNone : Maybe Type → Type +orNone nothing = none +orNone (just T) = T VarCtxt : Set VarCtxt = KeyMap Type @@ -18,8 +23,8 @@ _⋒_ = unionWith _∩_ _⋓_ : VarCtxt → VarCtxt → VarCtxt _⋓_ = unionWith _∪_ -_[_] : VarCtxt → Var → Maybe Type -_[_] Γ x = lookup (fromString x) Γ +_[_] : VarCtxt → Var → Type +_[_] Γ x = orNone (lookup (fromString x) Γ) _⊝_ : VarCtxt → Var → VarCtxt Γ ⊝ x = delete (fromString x) Γ @@ -30,5 +35,5 @@ x ↦ T = singleton (fromString x) T _⊕_↦_ : VarCtxt → Var → Type → VarCtxt Γ ⊕ x ↦ T = insert (fromString x) T Γ --- ⊕-[] : ∀ (Γ : VarCtxt) x T → (((Γ ⊕ x ↦ T) [ x ]) ≡ just T) -⊕-[] = λ (Γ : VarCtxt) x T → lookup-insert (fromString x) T Γ +-- ⊕-[] : ∀ (Γ : VarCtxt) x T → (((Γ ⊕ x ↦ T) [ x ]) ≡ T) +⊕-[] = λ (Γ : VarCtxt) x T → cong orNone (lookup-insert (fromString x) T Γ) diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda index a8b59f30..46feee6e 100644 --- a/prototyping/Properties.agda +++ b/prototyping/Properties.agda @@ -1,5 +1,9 @@ module Properties where +import Properties.Contradiction import Properties.Dec +import Properties.Equality import Properties.Remember import Properties.Step +import Properties.TypeCheck + diff --git a/prototyping/Properties/Contradiction.agda b/prototyping/Properties/Contradiction.agda new file mode 100644 index 00000000..e9a92ad5 --- /dev/null +++ b/prototyping/Properties/Contradiction.agda @@ -0,0 +1,9 @@ +module Properties.Contradiction where + +data ⊥ : Set where + +¬ : Set → Set +¬ A = A → ⊥ + +CONTRADICTION : ∀ {A : Set} → ⊥ → A +CONTRADICTION () diff --git a/prototyping/Properties/Dec.agda b/prototyping/Properties/Dec.agda index d89fd754..77f461f0 100644 --- a/prototyping/Properties/Dec.agda +++ b/prototyping/Properties/Dec.agda @@ -1,8 +1,8 @@ module Properties.Dec where -data ⊥ : Set where +open import Properties.Contradiction using (¬) data Dec(A : Set) : Set where yes : A → Dec A - no : (A → ⊥) → Dec A + no : ¬ A → Dec A diff --git a/prototyping/Properties/Equality.agda b/prototyping/Properties/Equality.agda new file mode 100644 index 00000000..605b690d --- /dev/null +++ b/prototyping/Properties/Equality.agda @@ -0,0 +1,17 @@ +module Properties.Equality where + +open import Agda.Builtin.Equality using (_≡_; refl) +open import Properties.Contradiction using (¬) + +sym : ∀ {A : Set} {a b : A} → (a ≡ b) → (b ≡ a) +sym refl = refl + +trans : ∀ {A : Set} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c) +trans refl refl = refl + +cong : ∀ {A B : Set} {a b : A} (f : A → B) → (a ≡ b) → (f a ≡ f b) +cong f refl = refl + +_≢_ : ∀ {A : Set} → A → A → Set +(a ≢ b) = ¬(a ≡ b) + diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda index f7d09d67..fbbbce69 100644 --- a/prototyping/Properties/TypeCheck.agda +++ b/prototyping/Properties/TypeCheck.agda @@ -3,108 +3,23 @@ module Properties.TypeCheck where open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.Maybe using (Maybe; just; nothing) open import FFI.Data.Either using (Either) -open import Luau.TypeCheck using (_▷_⊢ᴱ_∋_∈_⊣_; _▷_⊢ᴮ_∋_∈_⊣_; nil; var; addr; app) +open import Luau.TypeCheck using (_▷_⊢ᴱ_∋_∈_⊣_; _▷_⊢ᴮ_∋_∈_⊣_; nil; var; addr; app; function; block; done; return; local) open import Luau.Syntax using (Block; Expr; yes; nil; var; addr; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg) open import Luau.Type using (Type; nil; none; _⇒_; src; tgt) -open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; ⊕-[]) renaming (_[_] to _[_]ⱽ) +open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_; ⊕-[]) renaming (_[_] to _[_]ⱽ) open import Luau.Addr using (Addr) open import Luau.Var using (Var; _≡ⱽ_) open import Luau.AddrCtxt using (AddrCtxt) renaming (_[_] to _[_]ᴬ) -open import Properties.Dec using (⊥; yes; no) +open import Properties.Dec using (yes; no) +open import Properties.Equality using (_≢_; sym; trans; cong) open import Properties.Remember using (remember; _,_) -sym : ∀ {A : Set} {a b : A} → (a ≡ b) → (b ≡ a) -sym refl = refl - -trans : ∀ {A : Set} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c) -trans refl refl = refl - -cong : ∀ {A B : Set} {a b : A} (f : A → B) → (a ≡ b) → (f a ≡ f b) -cong f refl = refl - -_⊆_ : ∀ {A : Set} → (A → Set) → (A → Set) → Set -P ⊆ Q = (∀ a → P a → Q a) - -data _⊝_ {A : Set} (P : A → Set) (a b : A) : Set where - _,_ : (P b) → ((a ≡ b) → ⊥) → (P ⊝ a) b - -data _∪_ {A : Set} (P Q : A → Set) (a : A) : Set where - left : (P a) → (P ∪ Q) a - right : (Q a) → (P ∪ Q) a - -∪-⊆ : ∀ {A : Set} {P Q R : A → Set} → (P ⊆ R) → (Q ⊆ R) → ((P ∪ Q) ⊆ R) -∪-⊆ p q a (left r) = p a r -∪-⊆ p q a (right r) = q a r - -⊆-left : {A : Set} {P Q R : A → Set} → ((P ∪ Q) ⊆ R) → (P ⊆ R) -⊆-left p a q = p a (left q) - -⊆-right : {A : Set} {P Q R : A → Set} → ((P ∪ Q) ⊆ R) → (Q ⊆ R) -⊆-right p a q = p a (right q) - -sing : ∀ {A} → A → A → Set -sing = _≡_ - -data emp {A : Set} : A → Set where - -fvᴱ : ∀ {a} → Expr a → Var → Set -fvᴮ : ∀ {a} → Block a → Var → Set - -fvᴱ nil = emp -fvᴱ (var x) = sing x -fvᴱ (addr x) = emp -fvᴱ (M $ N) = fvᴱ M ∪ fvᴱ N -fvᴱ function F is B end = fvᴮ B ⊝ name (arg F) -fvᴱ block b is B end = fvᴮ B - -fvᴮ (function F is C end ∙ B) = (fvᴮ C ⊝ name (arg F)) ∪ (fvᴮ B ⊝ fun F) -fvᴮ (local x ← M ∙ B) = fvᴱ M ∪ (fvᴮ B ⊝ name x) -fvᴮ (return M ∙ B) = fvᴱ M ∪ fvᴮ B -fvᴮ done = emp - -faᴱ : ∀ {a} → Expr a → Addr → Set -faᴮ : ∀ {a} → Block a → Addr → Set - -faᴱ nil = emp -faᴱ (var x) = emp -faᴱ (addr a) = sing a -faᴱ (M $ N) = faᴱ M ∪ faᴱ N -faᴱ function F is B end = faᴮ B -faᴱ block b is B end = faᴮ B - -faᴮ (function F is C end ∙ B) = faᴮ C ∪ faᴮ B -faᴮ (local x ← M ∙ B) = faᴱ M ∪ faᴮ B -faᴮ (return M ∙ B) = faᴱ M ∪ faᴮ B -faᴮ done = emp - -data dv (Γ : VarCtxt) (x : Var) : Set where - just : ∀ T → (just T ≡ Γ [ x ]ⱽ) → dv Γ x - -data da (Σ : AddrCtxt) (a : Addr) : Set where - just : ∀ T → (just T ≡ Σ [ a ]ᴬ) → da Σ a - -⊕-⊆-⊝ : ∀ {Γ P} x T → ((P ⊝ x) ⊆ dv Γ) → (P ⊆ dv (Γ ⊕ x ↦ T)) -⊕-⊆-⊝ x T p y q with x ≡ⱽ y -⊕-⊆-⊝ x T p .x q | yes refl = just T (sym (⊕-[] _ x T)) -⊕-⊆-⊝ x T p y q | no r = {!!} - -orNone : Maybe Type → Type -orNone nothing = none -orNone (just T) = T - -dv-orNone : ∀ {Γ x} → (dv Γ x) → (just (orNone (Γ [ x ]ⱽ)) ≡ Γ [ x ]ⱽ) -dv-orNone (just T p) = trans (sym (cong just (cong orNone p))) p - -da-orNone : ∀ {Σ a} → (da Σ a) → (just (orNone (Σ [ a ]ᴬ)) ≡ Σ [ a ]ᴬ) -da-orNone (just T p) = trans (sym (cong just (cong orNone p))) p - - typeOfᴱ : AddrCtxt → VarCtxt → (Expr yes) → Type typeOfᴮ : AddrCtxt → VarCtxt → (Block yes) → Type typeOfᴱ Σ Γ nil = nil -typeOfᴱ Σ Γ (var x) = orNone(Γ [ x ]ⱽ) -typeOfᴱ Σ Γ (addr a) = orNone(Σ [ a ]ᴬ) +typeOfᴱ Σ Γ (var x) = Γ [ x ]ⱽ +typeOfᴱ Σ Γ (addr a) = Σ [ a ]ᴬ typeOfᴱ Σ Γ (M $ N) = tgt(typeOfᴱ Σ Γ M) typeOfᴱ Σ Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T typeOfᴱ Σ Γ (block b is B end) = typeOfᴮ Σ Γ B @@ -125,16 +40,23 @@ data TypeCheckResultᴮ Σ Γ S B where ok : ∀ Δ → (Σ ▷ Γ ⊢ᴮ S ∋ B ∈ (typeOfᴮ Σ Γ B) ⊣ Δ) → TypeCheckResultᴮ Σ Γ S B -typeCheckᴱ : ∀ Σ Γ S M → (faᴱ M ⊆ da Σ) → (fvᴱ M ⊆ dv Γ) → (TypeCheckResultᴱ Σ Γ S M) -typeCheckᴮ : ∀ Σ Γ S B → (faᴮ B ⊆ da Σ) → (fvᴮ B ⊆ dv Γ) → (TypeCheckResultᴮ Σ Γ S B) +typeCheckᴱ : ∀ Σ Γ S M → (TypeCheckResultᴱ Σ Γ S M) +typeCheckᴮ : ∀ Σ Γ S B → (TypeCheckResultᴮ Σ Γ S B) -typeCheckᴱ Σ Γ S nil p q = ok ∅ nil -typeCheckᴱ Σ Γ S (var x) p q = ok (x ↦ S) (var x (dv-orNone (q x refl))) -typeCheckᴱ Σ Γ S (addr a) p q = ok ∅ (addr a (da-orNone (p a refl))) -typeCheckᴱ Σ Γ S (M $ N) p q with typeCheckᴱ Σ Γ (typeOfᴱ Σ Γ N ⇒ S) M (⊆-left p) (⊆-left q) | typeCheckᴱ Σ Γ (src (typeOfᴱ Σ Γ M)) N (⊆-right p) (⊆-right q) -typeCheckᴱ Σ Γ S (M $ N) p q | ok Δ₁ r | ok Δ₂ s = ok (Δ₁ ⋒ Δ₂) (app r s) -typeCheckᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) p q with typeCheckᴮ Σ (Γ ⊕ x ↦ T) U B p {!q!} -typeCheckᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) p q | R = {!!} -typeCheckᴱ Σ Γ S (block b is B end) p q = {!!} +typeCheckᴱ Σ Γ S nil = ok ∅ nil +typeCheckᴱ Σ Γ S (var x) = ok (x ↦ S) (var x refl) +typeCheckᴱ Σ Γ S (addr a) = ok ∅ (addr a refl) +typeCheckᴱ Σ Γ S (M $ N) with typeCheckᴱ Σ Γ (typeOfᴱ Σ Γ N ⇒ S) M | typeCheckᴱ Σ Γ (src (typeOfᴱ Σ Γ M)) N +typeCheckᴱ Σ Γ S (M $ N) | ok Δ₁ D₁ | ok Δ₂ D₂ = ok (Δ₁ ⋒ Δ₂) (app D₁ D₂) +typeCheckᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) with typeCheckᴮ Σ (Γ ⊕ x ↦ T) U B +typeCheckᴱ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is B end) | ok Δ D = ok (Δ ⊝ x) (function D) +typeCheckᴱ Σ Γ S (block b is B end) with typeCheckᴮ Σ Γ S B +typeCheckᴱ Σ Γ S block b is B end | ok Δ D = ok Δ (block D) -typeCheckᴮ Σ Γ S B = {!!} +typeCheckᴮ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) with typeCheckᴮ Σ (Γ ⊕ x ↦ T) U C | typeCheckᴮ Σ (Γ ⊕ f ↦ (T ⇒ U)) S B +typeCheckᴮ Σ Γ S (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) | ok Δ₁ D₁ | ok Δ₂ D₂ = ok ((Δ₁ ⊝ x) ⋒ (Δ₂ ⊝ f)) (function D₁ D₂) +typeCheckᴮ Σ Γ S (local var x ∈ T ← M ∙ B) with typeCheckᴱ Σ Γ T M | typeCheckᴮ Σ (Γ ⊕ x ↦ T) S B +typeCheckᴮ Σ Γ S (local var x ∈ T ← M ∙ B) | ok Δ₁ D₁ | ok Δ₂ D₂ = ok (Δ₁ ⋒ (Δ₂ ⊝ x)) (local D₁ D₂) +typeCheckᴮ Σ Γ S (return M ∙ B) with typeCheckᴱ Σ Γ S M +typeCheckᴮ Σ Γ S (return M ∙ B) | ok Δ D = ok Δ (return D) +typeCheckᴮ Σ Γ S done = ok ∅ done